Achtung:

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.

Funding

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

Publications


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

DOI


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

DOI


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

DOI


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

DOI


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

DOI


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

DOI


Liste im Research Information System öffnen

Kontakt

Prof. Dr. Heike Wehrheim

Spezifikation und Modellierung von Softwaresystemen

Heike Wehrheim
Telefon:
+49 5251 60-4331
Büro:
O4.225
Web:

Jürgen König

Spezifikation und Modellierung von Softwaresystemen

Jürgen König
Telefon:
+49 5251 60-1715
Büro:
O4.134
Web:

Die Universität der Informationsgesellschaft