中國科大在并發(fā)程序驗證研究中取得進(jìn)展

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

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

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

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