University of Cambridge > Talks.cam > Microsoft Research Cambridge, public talks > Formalising and Analysing Transactional Consistency Models

Formalising and Analysing Transactional Consistency Models

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2020 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity