近日，我校188滚球网
、188金宝慱体育版
－耶魯高可信軟件聯合研究中心梁紅瑾特任副研究員和馮新宇教授在並發程序驗證領域取得重要進展，首次設計出了一種驗證並發對象無饑餓性與無死鎖性的程序邏輯。該研究成果以“A Program Logic for Concurrent Objects under Fair Scheduling”為題發表在第43屆編程語言原理國際會議（ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages，簡稱POPL）上。該論文是本年度唯一來自中國大陸研究機構的論文。此前，中國大陸研究機構作為第一署名單位僅在POPL上發表過3篇論文，其中第一篇便是由梁紅瑾、馮新宇課題組在第39屆POPL會議上發表的。
多處理器係統上的並發程序在執行時，有多個線程同時共享係統資源。當對共享資源的管理和使用不當時，常常會出現饑餓、死鎖、活鎖等活性問題，造成一個或多個線程無限期等待資源而不再響應。由於並發係統自身的複雜性，程序測試難以找出全部問題。梁紅瑾等提出了一個新的程序邏輯，能夠嚴格證明一個並發係統不可能出現饑餓、死鎖、活鎖等問題。該研究工作將並發環境的各種行為分為兩類，稱為“阻塞”和“延遲”，饑餓、死鎖等問題分別對應於這兩類並發環境的不同組合。然後，針對阻塞與延遲，分別設計出特定的程序規範和推理規則，保證並發係統最終一定會響應並有所進展。這樣得到的程序邏輯具有很好的通用性，可定製為對各個單一性質的驗證。該程序邏輯已應用於一些經典並發算法驗證，例如，該工作在國際上首次形式化驗證了鎖耦合鏈表算法的無饑餓性，以及樂觀鏈表算法和惰性鏈表算法的無死鎖性等。該研究成果為驗證實際並發程序的無饑餓性、無死鎖性等活性性質提供了理論基礎。
POPL是編程語言領域曆史最久、水平最高的國際會議，它是討論編程語言和編程係統最新突破的最主要論壇，內容涵蓋編程語言的理論、編程語言的設計、編譯器技術、程序分析、程序驗證、可信軟件等眾多研究領域。國際期刊和會議的各種分區方法都把POPL放在該領域的最高區域中。
第43屆POPL會議於1月20日至1月23日在美國佛羅裏達州聖彼德斯堡召開，梁紅瑾應邀報告了該研究成果，與會專家給與了很高評價。
該研究工作得到了國家自然科學基金的資助。
論文鏈接：http://dl.acm.org/citation.cfm?id=2837635
（計算機學院、188金宝慱体育版 －耶魯高可信軟件聯合研究中心）
