Concurrency Reasoning for Weak Memory

弱内存的并发推理

• 批准号: 467386514
• 负责人: Professorin Dr. Heike Wehrheim
• 金额: --
• 依托单位: Department für Informatik
• 依托单位国家: 德国
• 项目类别: Research Grants
• 资助国家: 德国
• 项目状态: 未结题
• 来源: https://gepris.dfg.de/gepris/projekt/467386514?language=en
• 关键词: Concurrency; Reasoning; 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.

程序验证旨在正式证明程序在指定属性方面的正确性。对于并行程序来说，正确性不仅取决于程序本身，还取决于执行硬件的内存模型。许多多核架构都拥有所谓的弱（或宽松）内存模型，这些模型显着影响并行程序的语义。迄今为止开发的大多数验证技术都是专门针对这样一种内存模型的。该项目的目标是开发一种通用验证技术，该技术允许生成独立于内存模型的正确性证明，然后能够将证明转移到某些特定模型。为此，我们希望在公理基础上进行验证，捕获内存模型常见的并行程序的操作行为，同时抽象出它们的技术差异。在此基础上，我们将开发（a）属性规范语言和（b）并行程序的证明演算。通过示例性地展示我们的公理对于三种内存模型的有效性以及许多证明案例研究的实现，我们打算证明该方法的通用性。