1月20日至23日，第43屆編程語言原理國際會議（簡稱POPL）在美國佛羅里達州圣彼德斯堡召開。中國科學技術大學特任副研究員梁紅瑾和教授馮新宇在并發程序驗證領域取得新進展，首次設計出一種驗證并發對象無饑餓性與無死鎖性的程序邏輯，該研究成果發表在第43屆POPL上。

　　多處理器系統上的并發程序在執行時，有多個線程同時共享系統資源。當對共享資源的管理和使用不當時，常常會出現饑餓、死鎖、活鎖等活性問題，造成一個或多個線程無限期等待資源而不再響應。由于并發系統自身的復雜性，程序測試難以找出全部問題。梁紅瑾等提出了一個新的程序邏輯，能夠嚴格證明一個并發系統不可能出現饑餓、死鎖、活鎖等問題。研究人員將并發環境的各種行為分為兩類，稱為“阻塞”和“延遲”，饑餓、死鎖等問題分別對應于這兩類并發環境的不同組合。然后，針對阻塞與延遲，分別設計出特定的程序規范和推理規則，保證并發系統最終一定會響應并有所進展。這樣得到的程序邏輯具有很好的通用性，可定制為對各個單一性質的驗證。該程序邏輯已應用于一些經典并發算法驗證，例如，該工作在國際上首次形式化驗證了鎖耦合鏈表算法的無饑餓性，以及樂觀鏈表算法和惰性鏈表算法的無死鎖性等。該研究成果為驗證實際并發程序的無饑餓性、無死鎖性等活性性質提供了理論基礎。

　　POPL是討論編程語言和編程系統最新突破的主要論壇，內容涵蓋編程語言的理論、編程語言的設計、編譯器技術、程序分析、程序驗證、可信軟件等眾多研究領域。該論文是本年度唯一來自中國大陸研究機構的論文。此前，中國大陸研究機構作為第一署名單位僅在POPL上發表過3篇論文，其中第一篇便是由梁紅瑾、馮新宇課題組在第39屆POPL會議上發表的。

    該研究工作得到國家自然科學基金的資助。