BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Proving the Correctness of Abstract Concurrency Control and Recove
 ry - Eliot Moss - University of Massachusetts Amherst
DTSTART:20091109T140000Z
DTEND:20091109T150000Z
UID:TALK21485@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:*Abstract:* Transactional programming is an attractive paradig
 m for concurrent programming. However\, standard closed nesting is insuffi
 ciently flexible. Conservative conflict detection can cause spurious abort
 s\, which negatively impact performance\; and integration with concurrent\
 , but non-transactional\, code is problematic. Extensions to closed nestin
 g to address these problems have been proposed (such as open nesting and t
 ransactional boosting)\, however such solutions require the programmer to 
 annotate code with locking information and compensating actions (undo code
  to execute in the case of an abort). It is vital that these specification
 s be correct\, but there are subtleties that can make concurrency control 
 and recovery difficult to reason about. Our work addresses the correctness
  concerns by allowing the programmer to specify an abstract state model fo
 r the data structure in question as well as the proposed conflict predicat
 es and the proposed compensating actions. Our system translates this descr
 iption into a SAT problem which is then automatically verified by a stock 
 SAT solver. Our tool allows the programmer to reason about their data stru
 cture in an abstract context\, divorced from implementation details\, thus
  removing much of the burden that transactional extensions impose. Note: T
 his present work that is part of the dissertation research of Trek Palmer\
 , a graduate student in Computer Science at UMass under my direction. I of
 fer the talk with his knowledge and encouragement. \n\n
LOCATION:Small public lecture room\, Microsoft Research Ltd\, 7 J J Thomso
 n Avenue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR