University of Cambridge > > Microsoft Research Cambridge, public talks > Proving the Correctness of Abstract Concurrency Control and Recovery

Proving the Correctness of Abstract Concurrency Control and Recovery

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


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