基于共享变量的多核并发程序模型检测

项目名称： 基于共享变量的多核并发程序模型检测

项目编号： No.61272117

项目类型： 面上项目

立项/批准年度： 2013

项目学科： 自动化技术、计算机技术

项目作者： 田聪

作者单位： 西安电子科技大学

项目金额： 80万元

中文摘要： 多(众)核时代的到来，为并发程序设计的发展带来了新的机遇和挑战。在多核计算环境下，如何保障并发程序的正确性和可靠性，成为计算机科学领域所面临的新挑战。本项目拟研究基于MSVL的共享变量多核并发程序的模型检测理论与方法。首先，以轻量级的并发为基始，研究多核并发程序设计语言中的轻量级并发在MSVL中的表达理论与方法。其次，研究多核并发程序设计语言到MSVL的抽象理论与方法。进而，研究基于抽象精化的MSVL多核并发程序的模型检测理论与方法。最后，研究基于MSVL的多核并发程序模型检测在：(1)多核环境下的弱内存模型的正确性验证，(2)多核环境下轻量级并发算法的正确性验证，等具体问题中的应用。

中文关键词： MSVL；并发程序；抽象精化；模型检测；形式化验证

英文摘要： The emergence of the multi-core (many-core) era brings new challenges and opportunities to concurrent programming.How to ensure the correctness and reliability of multi-core concurrent programs has been a new challenge in computer science. Therefore, we are motivated to investigate MSVL based model checking approach for multi-core concurrent programs in this project. First,how to express low-level concurrency in MSVL will be exployed. Further, abstraction of MSVL programs from general multi-core concurrent prgorams will be studied. Morever, abstraction-refinement based MSVL programs model checking approach will be establised and implemented. Finally, How the developed approach will be used in conquering the specific problems,such as (1) verification of the weak memory models, and (2) verification of the low-level concurrent algorithms, will be carried out.

英文关键词： MSVL；Concurrent program；Abstraction-refinement；Model checking；Formal verification