Abstract

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.