Lina4WM Linearizability Proofs for Weak Memory Models

点击翻译按钮获取中文摘要

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.