Concurrency Reasoning for Weak Memory

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

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.