Description

Software transactional memory is an alternative concurrency control mechanism, which can be used instead of lock-based mechanisms. In STM, concurrent code is executing transactions, which are sequences of read and write transactions. Transactions can be succesfully committed to main memory if no conflicting writes happened simultaneously.

In the literature, various implementations of software transactional memory exist. The standard correctness property for software transactional memory is opacity: an extension of the classical database serializability property with the additional requirement that even non-committed transactions are prevented from accessing inconsistent states. A standard technique to prove opacity is to create an input/output automaton that models the implementation, and then to prove that this input/output automaton refines a standard input/output automaton called TMS2. However, this approach has a manual step: namely from the implementation to the input/output automaton.

Within the VerCors project, we have developed a reasoning approach to reason about abstract model behaviour of concurrent programs. In this project, you are asked to investigate if this technique can be used to prove opacity of an STM implementation directly (instead of only proving it for the manually constructed input/output automaton that models the implementation).

The project will consist of the following steps:
- investigate different STM implementations
- understand opacity, and how to prove opacity using input/output automaton
- understand abstraction-based reasoning in VerCors
- develop an approach to use VerCors' abstraction-based reasoning technique to prove opacity of one or more STM implementations