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

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的共享变量多核并发程序的模型检测理论与方法。首先，以轻量级的并发为基始，研究多核并发程序设计语言中的轻量级并发在MSVL中的表达理论与方法。其次，研究多核并发程序设计语言到MSVL的抽象理论与方法。进而，研究基于抽象精化的MSVL多核并发程序的模型检测理论与方法。最后，研究基于MSVL的多核并发程序模型检测在：(1)多核环境下的弱内存模型的正确性验证，(2)多核环境下轻量级并发算法的正确性验证，等具体问题中的应用。

多（众）核时代的到来，为并发程序设计的发展带来了新的机遇和挑战。在多核计算环境下，如何保障并发程序的正确性和可靠性，成为计算机科学领域所面临的新挑战。本项目通过基于MSVL的共享变量多核并发程序的模型检测理论与方法，保障了并发程序的正确性和可靠性。为此，项目首先研究了多核并发程序设计语言的轻量级并发在MSVL中的表达理论与方法。接着研究了多核并发程序设计语言到MSVL的抽象理论与方法。在此基础上，研究了基于抽象精化的MSVL多核并发程序的模型检测理论与方法。取得了扩展的MSVL语言、基于抽象精化的模型检测理论与方法、扩展的实时MSVL语言等重要成果。最后，应用本项目所建立的理论与方法对一些实际并发程序进行了验证，并开发了相应的工具。总体来说，项目在Journal of Combinatorial Optimization，Theoretical Computer Science，Formal Aspects of Computing等著名国际期刊以及ICSE，COCOON，COCOA等重要国际会议发表或录用论文44篇，获得专利授权19项，申请专利15项，培养博士3名、硕士研究生10名。田聪教授获得了优青资助。项目期内组织国内会议1次，合作组织国际会议1次、参加国际会议13次；获得教育部自然科学一等奖1项、陕西省科学技术进步一等奖1项。