Formalising and Analysing Transactional Consistency Models

Add to your list(s) Download to your calendar using vCal

• Andrea Cerone
• Tuesday 05 January 2016, 11:00-12:00
• Auditorium, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB.

If you have a question about this talk, please contact lecturescam.

Please be aware that this event may be recorded. Microsoft will own the copyright of any recording and reserves the right to distribute it as required

To boost performance, modern transactional systems provide weaker consistency guarantees than those defined by serialisability. Suchtransactional systems exhibit subtle behaviours that make it difficult for programmers to write correct applications. This problem is complicated by the fact that consistency models specifications are often informal, or they use disparate formalisms.

I will present a framework for specifying transactional consistency model. Then I will focus on Snapshot Isolation, a well-known consistency model, and show how a thorough analysis of its formal specification leads to deriving two static analysis techniques: the first one checks whether an application running on a weaker consistency model, Parallel Snapshot Isolation, still behaves as though as it were running on Snapshot Isolation; the second one is transaction chopping for Snapshot Isolation.

This talk is part of the Microsoft Research Cambridge, public talks series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Auditorium, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Guy Emerson's list
• Interested Talks
• Microsoft Research Cambridge, public talks
• Optics for the Cloud
• PMRFPS's
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• ob366-ai4er
• personal list
• rp587

Note that ex-directory lists are not shown.