Software transactional memory (STM) is a synchronous mechanism for concurrent programs with shared memroy. STM provides programmers with a high-level, easy to use abstraction of concurrency control, freeing them from explicit usage of synchronisation concepts like locks or semaphores. Basically, an STM allows a programmer to put code into a transaction, and let the STM algorithm guarantee execution of the transaction atomically in all-or-nothing fashion.

Participants: Heike Wehrheim, Jürgen König, John Derrick (University of Sheffield), Brijesh Dongol (Brunel University London), Gerhard Schellhorn (Universität Augsburg)

Former Participants: Oleg Travkin

Up to now, a large number of transactional memory concepts have been proposed, implementing TMs in hardware, in software or in a combination (hybrid TMs), and these have found their way into mainstream programming language and processor design. To achieve high performance even in the face of thousands of parallel processes, STMs try to allow for as much concurrency as possible, restricting synchronization to the minimal amount necessary for correctness. Correctness of STMs is typicall formalized in a notion called opacity, stating "seemingly atomic" execution of transactions; in particular enhancing it with meaning for aborting transactions.

The key objective of this project is the development of a validation toolbox for STMs. It will include three main ingredients:

1. a method (and tool) for testing STMs,
2. a method (and tool) for model checking STMs and
3. a method for mechanically proving correctness of STMs.

Thereby, this project shall support the whole lifecycle of STM design, from rapid prototyping in early design stages to the final product of a high performant, formally verified STM algorithm.

This project is funded by the German Research Council DFG (VaST, 2018 - 2020).