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.

Show image information

VaST - Validation of 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. 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.

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

Funding

This project is funded by the German Research Council DFG (VaST, 2018 - 2020) and extends former projects (LINA4WM, 2015 - 2017) and (LINA, 2010 - 2013).

Publications

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)
[DOI]

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)
[DOI]

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)

[DOI]

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)

[PDF] [DOI]

Contact

Prof. Dr. Heike Wehrheim

Specification and Modelling of Software Systems

Heike Wehrheim
Phone:
+49 5251 60-4331
Office:
O4.225
Web:

Jürgen König

Specification and Modelling of Software Systems

Jürgen König
Phone:
+49 5251 60-1715
Office:
O4.134
Web:

The University for the Information Society