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)

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.

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.

Additionally we were concerned with verifiying a correctness criterion related to linearizability for Software Transactional Memory, called opacity. Building on the proof techniques for linearizability we proved the opacity of several Software Transactional Memory algorithms. The research concerning these algorithms is continued in the DFG Project VaST.

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

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)

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)

O. Travkin, H. Wehrheim: Verification of Concurrent Programs on Weak Memory Models. In Augusto Sampaio and Farn Wang (eds.): Theoretical Aspects of Computing - ICTAC 2016 - 13 th International Colloquium, Taipei, Taiwan, ROC, October 24-31, 2016, Proceedings. , LNCS, vol. 9965, pp. 3 - 24 (2016)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)