Proving the Correctness of Abstract Concurrency Control and Recovery

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

• Eliot Moss - University of Massachusetts Amherst
• Monday 09 November 2009, 14:00-15:00
• Small public lecture room, Microsoft Research Ltd, 7 J J Thomson Avenue (Off Madingley Road), Cambridge.

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

Abstract: Transactional programming is an attractive paradigm for concurrent programming. However, standard closed nesting is insufficiently flexible. Conservative conflict detection can cause spurious aborts, which negatively impact performance; and integration with concurrent, but non-transactional, code is problematic. Extensions to closed nesting to address these problems have been proposed (such as open nesting and transactional 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 specifications 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 for the data structure in question as well as the proposed conflict predicates and the proposed compensating actions. Our system translates this description into a SAT problem which is then automatically verified by a stock SAT solver. Our tool allows the programmer to reason about their data structure in an abstract context, divorced from implementation details, thus removing much of the burden that transactional extensions impose. Note: This present work that is part of the dissertation research of Trek Palmer, a graduate student in Computer Science at UMass under my direction. I offer the talk with his knowledge and encouragement.

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)
• 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
• Small public lecture room, Microsoft Research Ltd, 7 J J Thomson Avenue (Off Madingley Road), Cambridge
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• ob366-ai4er
• personal list
• rp587

Note that ex-directory lists are not shown.