Using Formal Methods to Verify Transactional Abstract Concurrency Control

10 Jun
Tuesday, 06/10/2014 10:00am to 12:00pm
Ph.D. Thesis Defense

Trek Palmer

Computer Science Building, Room 142

Concurrent application design and implementation is more important than ever in today's multi-core processor world.  Transaction Memory (TM) has emerged as a promising technique for vastly simplifying the task of implementing concurrent applications.  Transactional semantics in a programming language context has the potential to greatly improve the correctness of concurrent code, and imprive the productivity of those that write it.  However, standard transactional memory systems have several deficiencies.  It is difficult to integrate transactional and non-transactional code, the TM runtime may make sub-optimal decisions that can significantly impact performance, and some actions (such as I/O) are inherently non-transactional.  To remedy these shortcomings, several extensions to ordinary closed-nested TM have been proposed (Open Nesting & Transactional Boosting).  Each has its own particular advantages and disadvantages; however, these techniques each need some extra information to "glue" the non-transactional operation into a transactional context.  At the most general level, non-transactional code must be decorated in such a way that the TM runtime and determine how those non-transactional operations commute with one another, and how to "undo" these operations in case the runtime needs to abort a software transaction.

The TM runtime trusts that these programmer-provided annotations are correct.  Therefore, if an implementor needs to employ one of these transactional "escape hatches", it is crucially important that their concurrency control annotations be correct.  However, reasoning about the commutativity of data structure operations is often challenging, and increasing the burden on the programmer with a proof requirement does not simplify the task of concurrent programming.  There is a way to leverage the structure that these TM extensions require such as to reduce greatly the burden on the programmer.  If the programmer could describe the abstract state of the data structure and then reason about it with as much machine assistance as possible, then there would be much less opportunity for error.  Abstract state is preferable to a more concrete state, because it permits the programmer to use different concrete implementations of the same abstract data type. Also, some TM extensions such as Open Nesting can handle concrete state conflicts without programmer intervention (making the abstract state the appropriate one for reasoning about commutativity).  A solution to the problem of specifying and verifying the concurrency properties of abstract data structures is the subject of this thesis.

This thesis describes a new language, ACCLAM, for describing the abstract state of a data structure and reasoning about its concurrency control properties.  This thesis also describes a tool that can process ACCLAM descriptions into a machine-verifiable form (they are converted to a SAT problem).  This thesis also provides a more detailed overview of transactional memory and the more popular extensions, a detailed semantic description of ACCLAM, and a set of example data structure models and the results of processing those examples with the language processing tool.

Advisor: J. Eliot Moss