Lina4WM Linearizability Proofs for Weak Memory Models

今天，并行程序实际上通常在多核机器上运行，因此可以真正并发地执行。这可以显著提高并行程序的性能。然而，性能的提高确实是要付出一些代价的：多核机器的内存模型比通常假设的顺序一致的内存模型弱得多。这会导致并行程序的意外执行，并最终导致错误。Lina4WM项目调查了一类特定的并行程序在弱内存模型上的正确性。这类程序由所谓的并发数据结构组成，即允许对堆栈、队列或哈希表等数据结构进行并发访问的算法。这类算法针对并发性进行了高度优化，还包含数据竞争。因此，他们特别容易受到弱记忆模型效应的影响。该项目旨在开发一种证明弱内存模型上并发数据结构正确性的方法。并行数据结构的关键正确性标准是可线性化。证明方法论的基础是机器辅助模拟证明。因此，该项目将致力于基于模拟的多核机器上并发数据结构的线性化证明。

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.