BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Formalising and Analysing Transactional Consistency Models  - Andr
 ea Cerone
DTSTART:20160105T110000Z
DTEND:20160105T120000Z
UID:TALK63131@talks.cam.ac.uk
CONTACT:44515
DESCRIPTION:To boost performance\, modern transactional systems provide we
 aker consistency guarantees than those defined by serialisability. Suchtra
 nsactional systems exhibit subtle behaviours that make it difficult for pr
 ogrammers to write correct applications.  This problem is complicated by t
 he fact that consistency models specifications are often informal\, or the
 y use disparate formalisms. \n\nI 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: th
 e first one checks whether an application running on a weaker consistency 
 model\, Parallel Snapshot Isolation\, still behaves as though as it were r
 unning on Snapshot Isolation\; the second one is transaction chopping for 
 Snapshot Isolation.\n
LOCATION:Auditorium\, Microsoft Research Ltd\, 21 Station Road\, Cambridge
 \, CB1 2FB
END:VEVENT
END:VCALENDAR