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

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

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

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