天天看點

微軟開源P語言,解決異步計算的挑戰問題

微軟近日釋出了一篇研究報告,介紹了一種為異步性、容錯性和不确定性而設計的p語言,實作安全的異步事件驅動程式設計。該語言基于事件進行通信,能夠很好的解決并發操作所帶來的問題,并能夠在軟體的建構、測試和調試等各個階段發揮作用。雷鋒網(公衆号:雷鋒網)編譯如下。

新型軟體的複雜性導緻了程式設計人員需要新的方法來了解,并有效地建構、測試和調試這些系統。如今的軟體通常使用雲資源,嵌入在實體世界的裝置中,并采用人工智能技術。這三個因素使得今天的軟體系統難以發展。

通常現代應用需要異步性來提高性能,比如在下面這種情形:操作的請求者在發起操作後繼續運作,而不需要等待操作完成。異步不可避免的會導緻并發,以及臭名昭著的競争現象和heisenbug(一種奇怪的軟體bug,通常是時變的,平時會出現bug,而當你要研究這個問題的時候,bug就消失了,或者每次研究的時候bug的結果都是在變化的)。

為了解決異步計算的挑戰,微軟開發了p語言,這是一種用于異步事件驅動型應用程式中模組化和指定協定的程式設計語言。該項目是微軟研究人員和工程師與加州大學伯克利分校以及倫敦帝國學院的學術研究人員一起合作開發的。

微軟開源P語言,解決異步計算的挑戰問題

圖1:p語言工具鍊流程圖

p語言程式設計人員在高層編寫協定及其規範。p編譯器提供用于并發相關競争條件的自動測試和運作協定的可執行代碼。p語言對模組化并發性(modeling concurrency)、指定安全性(specifying safety)和活性屬性(liveness property)提供一流的支援,并使用系統級搜尋檢查程式是否滿足規範。

在這些方面,p語言與leslie lamport的tla +和gerard holzmann的spin相似。與tla +和spin不同的是,p程式也可以被編譯成可執行的c代碼。這種能力搭建了進階模型和低級實作之間的橋梁,并消除了程式員之間接受形式化模組化和規範的巨大障礙。

微軟開源P語言,解決異步計算的挑戰問題

圖2:通信狀态機

p中的程式設計模型基于并發執行狀态機,通過事件進行通信,每個事件伴随一個有類型的負載值。基于線性輸入和獨特指針的記憶體管理系統提供安全的記憶體管理和無資料競争的并發執行。在這方面,p類似于現代系統程式設計語言,例如rust。

p在微軟的軟體開發中,最初被用在windows 8.1和windows phone中運送usb3.0驅動程式。這些驅動程式處理着windows生态系統中衆多最重要的周邊裝置,如今已經在數億台裝置上運作。p在驅動程式設計初期就啟用了數百種競争條件和heisenbugs的檢測和調試,現在廣泛應用于windows中的驅動程式開發。p在windows核心中早期積累的經驗導緻了p#的開發,p#是通過c#拓展提供狀态機和系統測試的架構。與p相反,p#中的方法是最小化文法拓展,并最大限度的利用庫提供模組化,規範和測試功能。

p正在改變azure的雲基礎架構的發展。azure類似于其他雲提供商,面臨着由意料之外的并發競争條件或軟硬體故障引起的heisenbug的挑戰。這些錯誤導緻實時服務的中斷,這是雲服務的客戶和提供商所面臨的巨大問題。p和p#正用于在已部署的服務中查找和調試heisenbug,并在部署前設計和驗證新服務。p允許工程師在大型azure服務中的元件之間精确的模拟異步接口。它還允許工程師發現和調試他們桌面裝置上的問題,否則這些問題在部署服務幾個月甚至幾年之後都難以找到根源。

使p特别适用于驗證容錯的分布式服務的一個重要特征,是它能夠進行徹底的失效恢複(failover)測試,即在意外故障發生時保證服務能夠恢複,并繼續之前的操作。網絡資訊丢失和單個狀态機故障都被模組化為事件。将故障模組化為p中的一個事件,可以完全自動化完成故障注入,并可以在大量事件排序和故障的情況下對失效恢複進行測試,而程式員并不需要做太多的工作。

p的系統測試能力能夠徹底地搜尋由并發發送事件的非确定性排序引起的選擇。然而,其能力主要應用在處理明确資料輸入方面,尤其是對大範圍輸入的搜尋。這種限制使得難以将p應用到複雜性來源主要是不确定的輸入下進行決策這樣的應用中,例如機器人技術。微軟正在研究如何處理大量不确定的輸入域,主要通過研究符号和機率技術來應對這一挑戰。

本文轉自d1net(轉載)

繼續閱讀