Sie haben Javascript deaktiviert!
Sie haben versucht eine Funktion zu nutzen, die nur mit Javascript möglich ist. Um sämtliche Funktionalitäten unserer Internetseite zu nutzen, aktivieren Sie bitte Javascript in Ihrem Browser.

Jan Haltermann, Manuel Töws, Felix Pauck, Cedric Richter, Heike Wehrheim, Jürgen König, Arnab Sharma, Steffen Beringer, Oleksandra Koslova, Elisabeth Schlatt (left to right) Show image information

Jan Haltermann, Manuel Töws, Felix Pauck, Cedric Richter, Heike Wehrheim, Jürgen König, Arnab Sharma, Steffen Beringer, Oleksandra Koslova, Elisabeth Schlatt (left to right)

Software Transactional Memory

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

VaST - Validation of Software Transactional Memory

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).


, , , , : FastLane Is Opaque - a Case Study in Mechanized Proofs of Opacity. In International Conference on Software Engineering and Formal Methods (2018).

 J. König, H. Wehrheim: Value-Based or Conflict-Based? Opacity Definitions for STMs. In Dang Van Hung and Deepak Kapur (eds.): Theoretical Aspects of Computing - ICTAC 2017 - 14th International Colloquium, Hanoi, Vietnam, October 23-27, 2017, Proceedings. Springer, LNCS, vol. 10580, pp. 118-135 (2017)

J. Derrick, S. Doherty, B. Dongol, G. Schellhorn, O. Travkin, H. Wehrheim: Mechanized proofs of opacity: a comparison of two techniques. In Formal Aspects of Computing. (2017)

S. Doherty, B. Dongol, J. Derrick, G. Schellhorn, H. Wehrheim: Proving Opacity of a Pessimistic STM. In Panagiota Fatourou, Ernesto Jiménez, Fernando Pedone (eds.): 20th International Conference on Principles of Distributed Systems, OPODIS 2016, December 13-16, 2016, Madrid, Spain. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, LIPIcs, vol. 70 (2016)

J. Derrick, B. Dongol, G. Schellhorn, O. Travkin, H. Wehrheim: Verifying Opacity of a Transactional Mutex Lock. In Nikolaj Bjørner and Frank S. de Boer (eds.): FM 2015: Formal Methods - 20th International Symposium, Oslo, Norway. , LNCS, vol. 9109, pp. 161 - 177 (2015)


Prof. Dr. Heike Wehrheim

Specification and Modelling of Software Systems

Heike Wehrheim
+49 5251 60-4331

Jürgen König

Specification and Modelling of Software Systems

Jürgen König
+49 5251 60-1715

The University for the Information Society