Using Formal Methods to Verify and Derive Open Nested Locking Protocols

Transactional memory systems (TM) offer an alternative to standard lock-based programming. However, the convenience and composability of a transactional memory system often come at the price of efficiency. TM systems detect and repair conflicts at the memory level, which can lead to spurious aborts (and expensive rollbacks). Open nesting is an extension to standard closed nesting TM that raises the level of abstraction and repair in order to avoid costly spurious rollbacks. However, much of the work that was automatically done by the TM system must now be performed by the programmer. In particular, the programmer will have to specify a locking protocol as well as compensating actions (to undo in case of an abort). Although this looks no better than standard lock-based programming, it is a far more structured approach. This structure can be exploited (I claim) to verify automatically and derive locking protocols for open nested data structures. This structure may be rich enough, in fact, to be able to verify and propose simple compensating actions (i.e., proving that inverse actions are actually inverses). I propose that an abstract state specification will allow automatic verification of concurrency control and compensating actions and furthermore may enable heuristic derivation of locking protocols and inverse actions.