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.

Info-Icon Diese Seite ist nicht in Deutsch verfügbar
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) Bildinformationen anzeigen

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


Liste im Research Information System öffnen

Verifying Opacity of a Transactional Mutex Lock

J. Derrick, B. Dongol, G. Schellhorn, O. Travkin, H. Wehrheim, in: {FM} 2015: Formal Methods - 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings, 2015, pp. 161--177

Proving Opacity of a Pessimistic {STM}

S. Doherty, B. Dongol, J. Derrick, G. Schellhorn, H. Wehrheim, in: 20th International Conference on Principles of Distributed Systems, {OPODIS} 2016, December 13-16, 2016, Madrid, Spain, 2016, pp. 35:1--35:17

Value-Based or Conflict-Based? Opacity Definitions for STMs

J. König, H. Wehrheim, in: Theoretical Aspects of Computing - {ICTAC} 2017 - 14th International Colloquium, Hanoi, Vietnam, October 23-27, 2017, Proceedings, 2017, pp. 118--135

FastLane Is Opaque – a Case Study in Mechanized Proofs of Opacity

G. Schellhorn, M. Wedel, O. Travkin, J. König, H. Wehrheim, in: Software Engineering and Formal Methods, Springer International Publishing, 2018, pp. 105-120

Verifying Correctness of Persistent Concurrent Data Structures

J. Derrick, S. Doherty, B. Dongol, G. Schellhorn, H. Wehrheim, in: Formal Methods - The Next 30 Years - Third World Congress, {FM} 2019, Porto, Portugal, October 7-11, 2019, Proceedings, 2019, pp. 179-195

Data Independence for Software Transactional Memory

J. König, H. Wehrheim, in: {NASA} Formal Methods - 11th International Symposium, {NFM} 2019, Houston, TX, USA, May 7-9, 2019, Proceedings, Springer, 2019, pp. 263-279

Verifying C11 programs operationally

S. Doherty, B. Dongol, H. Wehrheim, J. Derrick, in: Proceedings of the 24th {ACM} {SIGPLAN} Symposium on Principles and Practice of Parallel Programming, PPoPP 2019, Washington, DC, USA, February 16-20, 2019, {ACM}, 2019, pp. 355-365

Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory

E. Bila, S. Doherty, B. Dongol, J. Derrick, G. Schellhorn, H. Wehrheim, in: Formal Techniques for Distributed Objects, Components, and Systems - 40th {IFIP} {WG} 6.1 International Conference, {FORTE} 2020, Held as Part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Valletta, Malta, June 15-19, 2020, Proceedings, Springer, 2020, pp. 39-58

Liste im Research Information System öffnen


Jürgen König

Spezifikation und Modellierung von Softwaresystemen

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

Die Universität der Informationsgesellschaft