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

LINA4WM – Linearizability Proofs for Weak Memory Models

Linearizability is the quasi-standard correctness criterion for concurrent data structure implementations. Many approaches for the verification of linearizability have been proposed over the last decade, including our own work. However, existing verification methods for concurrent programs tend to ignore the influence of weak memory models (e.g., out-of-order execution) as provided by common multi-core processor architectures like the x86 or ARM. Thus, there is a gap between the behavior that is considered in verification and the behavior that actually possible on real architectures. In our project, we aim at closing this gap.

Participants: Heike Wehrheim, Oleg Travkin, John Derrick (University of Sheffield), Brijesh Dongol (Brunel University London), Gerhard Schellhorn (Universität Augsburg)

Description

Linearizability is a correctness criterion for algorithms, which allow parallel access to data structures like stacks, queues or sets. Linearizability guarantees that parallel, interleaved accesses of a number of processes behave as if they were sequential. Linearizability is in particular important (and non-trivial to show) for lock-free algorithms, which dispense with locking the whole data structure during access. To show linearizability, we have developed a number of refinement concepts, which formulate conditions on lock-free algorithms. Basically, a lock-free algorithm is proven to be a refinement (in the sense of data refinement) of an abstract data type, which realises an atomic access to the data structure.

With the advent of multi-core processors, a new challenge for verifying concurrent programs, and particularly concurrent data structures, emerges. Most verification techniques, including the original definition of Linearizability, assume processors to provide sequentially consistent execution semantics, i.e., processes perform instructions in program order while the overall behavior is a non-deterministic interleaving of all processes. However, actual multicore processors, e.g., x86, ARM, POWER, provide execution semantics weaker than sequential consistency: instructions are not guaranteed to execute in program order and written values can be observed in different orders by different processes. Thus, programs can exhibit more behavior on real architectures than what is usually assumed by existing verification techniques.

The main objective of this project is to improve verification of concurrent programs under influence of weak memory models. Particularly, we are interested in verification methods for linearizability and related correctness criteria. We are following two strands of research: The first strand aims at reusing and extending verification techniques for sequential consistency, e.g., by applying reduction techniques. The second strand considers the execution semantics of relaxed memory models directly in the correctness proofs, e.g., by modelling store buffers explicitly.

Funding

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

Publications

G. Schellhorn, O. Travkin, H. Wehrheim: Towards a Thread-Local Proof Technique for Starvation Freedom. In Erika Ábrahám and Marieke Huisman (eds.): Integrated Formal Methods - 12th International Conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016, Proceedings. , LNCS, vol. 9681 (2016)
[PDF] [DOI]

H. Wehrheim, O. Travkin: TSO to SC via Symbolic Execution. In Nir Piterman (eds.): Hardware and Software: Verification and Testing - 11th International Haifa Verification Conference, HVC 2015, Haifa, Israel. , LNCS, vol. 9434, pp. 104 - 119 (2015)
[PDF] [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]

G. Schellhorn, J. Derrick, H. Wehrheim: A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures. In ACM Transactions on Computational Logic. , vol. 15, no. 31 (2014)
[DOI]

B. Tofan, O. Travkin, G. Schellhorn, H. Wehrheim: Two approaches for proving linearizability of multiset. In . Science of Computer Programming, vol. 96, pp. 297-314 (2014)

O. Travkin, H. Wehrheim: Handling TSO in Mechanized Linearizability Proofs. In Eran Yahaf (eds.): Hardware and Software: Verification and Testing. Springer, LNCS, vol. 8855, pp. 132-147 (2014)
[DOI]

J. Derrick, B. Dongol, G. Schellhorn, B. Tofan, O. Travkin, H. Wehrheim: Quiescent Consistency: Defining and Verifying Relaxed Linearizability. In FM 2014: Formal Methods. Springer, LNCS, vol. 8442, pp. 200-214 (2014)
[PDF] [DOI]

O. Travkin, A. Mütze, H. Wehrheim: SPIN as a Linearizability Checker under Weak Memory Models. In Valeria Bertacco, Alex Legay (eds.): Hardware and Software: Verification and Testing. Springer International Publishing, Lecture Notes in Computer Science, vol. 8244, pp. 311-326 (2013)
[PDF] [DOI] [URL]

B. Dongol, O. Travkin, J. Derrick, H. Wehrheim: A High-Level Semantics for Program Execution under Total Store Order Memory. In Z. Liu, J. Woodcock, H. Zhu (eds.): Theoretical Aspects of Computing – ICTAC 2013. Springer Berlin/Heidelberg, LNCS, vol. 8049, pp. 177-194 (2013)
[PDF] [DOI] [URL]

O. Travkin, G. Schellhorn, H. Wehrheim: Proving Linearizability of Multiset with Local Proof Obligations. In G. Lüttgen, S. Merz (eds.): Proceedings of the 12th International Workshop on Automated Verification of Critical Systems (AVoCS 2012). ECEASST, vol. 53 (2012)

G. Schellhorn, H. Wehrheim, J. Derrick: How to Prove Algorithms Linearisable. In Computer Aided Verification. Springer Berlin/Heidelberg, LNCS, vol. 7358/2012, pp. 243-259 (2012)
[PDF] [DOI] [URL]

J. Derrick, G. Schellhorn, H. Wehrheim: Mechanically verified proof obligations for linearizability. In ACM Transactions on Programming Languages and Systems (TOPLAS)., vol. 33, no. 1, pp. 4 (2011)
[DOI] [URL]

J. Derrick, G. Schellhorn, H. Wehrheim: Verifying Linearisability with Potential Linearisation Points. In Michael Butler, Wolfram Schulte (eds.): . Springer Berlin/Heidelberg, LNCS, vol. 6664/2011, pp. 323-327 (2011)
[PDF] [DOI]

J. Derrick, G. Schellhorn, H. Wehrheim: Mechanizing a Correctness Proof for a Lock-Free Concurrent Stack. In Gilles Barthe and Frank S. de Boer (eds.): Formal Methods for Open Object-Based Distributed Systems, 10th IFIP WG 6.1 International Conference, FMOODS 2008. Springer, Lecture Notes in Computer Science, vol. 5051, pp. 78-95 (2008)
[PDF] [DOI]

J. Derrick, G. Schellhorn, H. Wehrheim: Proving Linearizability Via Non-atomic Refinement. In Jim Davies and Jeremy Gibbons (eds.): Integrated Formal Methods, 6th International Conference, IFM 2007. Springer, LNCS, pp. 195-214 (2007)
[PDF] [DOI]

Contact

Prof. Dr. Heike Wehrheim

Specification and Modelling of Software Systems

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

Oleg Travkin

Specification and Modelling of Software Systems

Oleg Travkin
Phone:
+49 5251 60-1766
Fax:
+49 5251 60-3993
Office:
O4.119
Web:

The University for the Information Society