《基於共享變數的多核並發程式模型檢測》是依託西安電子科技大學，由田聰擔任項目負責人的面上項目。
基本介紹
- 中文名：基於共享變數的多核並發程式模型檢測
- 項目類別：面上項目
- 項目負責人：田聰
- 依託單位：西安電子科技大學
中文摘要,結題摘要,
中文摘要
多(眾)核時代的到來，為並發程式設計的發展帶來了新的機遇和挑戰。在多核計算環境下，如何保障並發程式的正確性和可靠性，成為計算機科學領域所面臨的新挑戰。本項目擬研究基於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項。
