Concurrency Reasoning for Weak Memory

程序验证的目的是形式化证明程序的正确性与指定的属性。对于并行程序，正确性不仅取决于程序本身，还取决于执行硬件的内存模型。多核和多核体系结构具有所谓的弱（或松弛）内存模型，这显着影响并行程序的语义。大多数验证技术开发到目前为止，专门针对一个这样的内存模型。该项目的目标是开发一种通用的验证技术，该技术允许生成独立于内存模型的正确性证明，然后能够将证明转移到某些特定的模型。为此，我们要设置验证公理的基础上捕获的操作行为的并行程序常见的内存模型，同时从他们的技术差异抽象。在此基础上，我们将开发（a）一种用于属性说明的语言和（B）一种用于并行程序的证明演算。通过举例说明我们的公理的有效性为三个内存模型和实现的一些证明案例研究，我们打算证明的方法的通用性。

Program verification aims at formal proofs of program correctness with respect to specified properties. For parallel programs, correctness does not only depend on the program itself, but also on the memory model of the executing hardware. Many and multi core architectures possess so called weak (or relaxed) memory models which significantly influence the semantics of parallel programs. The majority of verification techniques developed so far are specialized to one such memory model. The objective of this project is the development of a generic verification technique which allows to generate correctness proofs independent of a memory model and is then able to transfer a proof to some specific model. To this end, we want to set verification on an axiomatic basis capturing the operational behaviour of parallel programs common to memory models while abstracting from their technical differences. Based on this, we will develop (a) a language for property specification and (b) a proof calculus for parallel programs. By exemplarily showing the validity of our axioms for three memory models and the realization of a number of proof case studies, we intend to demonstrate the genericity of the approach.