SOSP，全稱ACM Symposium on Operating Systems Principles，是ACM組織在計(jì)算機(jī)系統(tǒng)領(lǐng)域的旗艦型會(huì)議，也是目前國(guó)際計(jì)算機(jī)系統(tǒng)領(lǐng)域的頂級(jí)會(huì)議。SOSP頂會(huì)對(duì)論文的質(zhì)量和數(shù)量要求極高，每年只錄用30-40篇左右正式會(huì)議論文，通常錄取率約19%（今年錄取率是 18.78%），要求投稿方具有基礎(chǔ)性貢獻(xiàn)、領(lǐng)導(dǎo)性影響和堅(jiān)實(shí)的系統(tǒng)背景。阿里云入選論文主要介紹了云基礎(chǔ)設(shè)施網(wǎng)絡(luò)自研DNS權(quán)威解析的形式化驗(yàn)證工作，該工作對(duì)于提升阿里云DNS產(chǎn)品穩(wěn)定性、正確性具有重要意義。DNS全稱Domain Name System，即域名解析系統(tǒng)。它將用戶輸入的網(wǎng)址（例如：www.example.com）翻譯為網(wǎng)絡(luò)設(shè)備可以讀懂的地址（例如：1.2.3.4），從而引導(dǎo)用戶連接到正確的網(wǎng)絡(luò)服務(wù)器。DNS系統(tǒng)的正確性和穩(wěn)定性，是網(wǎng)絡(luò)可否成功服務(wù)廣大互聯(lián)網(wǎng)用戶的先決條件。

針對(duì)解析程序，傳統(tǒng)的測(cè)試技術(shù)只能保證測(cè)試用例部分正確性，并不能完整的、無死角的確保程序沒有 bug，阿里云形式化驗(yàn)證工作則實(shí)現(xiàn)了無死角發(fā)現(xiàn)程序中全部bug，并降低了對(duì)人工輔助的大量依賴，目前，該驗(yàn)證技術(shù)在業(yè)界已首次實(shí)際應(yīng)用于規(guī)?；渴鸬漠a(chǎn)品代碼程序中，并高效完成了2000多行代碼的DNS權(quán)威解析程序的驗(yàn)證，為云上客戶提供了真實(shí)有力的穩(wěn)定性保障。

論文鏈接參考：https://dl.acm.org/doi/10.1145/3600006.3613153

xiesc