Lina4WM Linearizability Proofs for Weak Memory Models

• Applicant: Professorin Dr. Heike Wehrheim
• Subject Area: Software Engineering and Programming Languages
• Term: from 2010 to 2018
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 163003744

Today, parallel programs are often actually run on multi-core machines and therefore executed truly concurrent. This can considerably improve the performance of parallel programs. The increased performance does however come at some price: the memory models of multi-core machines are much weaker than the commonly assumed sequentially consistent memory models. This leads to unexpected executions of parallel programs and ultimately to errors. The project Lina4WM investigates the correctness of a specific class of parallel programs on weak memory models. The class of programs consists of so-called concurrent data structures, i.e., algorithms which allow for a concurrent access to data structures like stacks, queues or hash tables. Such algorithms are highly optimized for concurrency and also contain data races. They are therefore particularly vulnerable to weak memory model effects. The project aims at the development of a proof methodology for the correctness of concurrent data structures on weak memory models. The key correctness criterion for parallel data structures is linearizability. The basis of the proof methodology are machine assisted simulation proofs. The project will thus work on simulation based proofs of linearizability of concurrent data structures on multi-core machines.

• DFG Programme: Research Grants