微軟近日發(fā)布了一篇研究報告，介紹了一種為異步性、容錯性和不確定性而設計的P語言，實現(xiàn)安全的異步事件驅(qū)動編程。該語言基于事件進行通信，能夠很好的解決并發(fā)操作所帶來的問題，并能夠在軟件的構建、測試和調(diào)試等各個階段發(fā)揮作用。雷鋒網(wǎng)(公眾號：雷鋒網(wǎng))編譯如下。
新型軟件的復雜性導致了編程人員需要新的方法來理解，并有效地構建、測試和調(diào)試這些系統(tǒng)。如今的軟件通常使用云資源，嵌入在物理世界的設備中，并采用人工智能技術。這三個因素使得今天的軟件系統(tǒng)難以發(fā)展。
通常現(xiàn)代應用需要異步性來提高性能，比如在下面這種情形：操作的請求者在發(fā)起操作后繼續(xù)運行，而不需要等待操作完成。異步不可避免的會導致并發(fā)，以及臭名昭著的競爭現(xiàn)象和Heisenbug(一種奇怪的軟件bug，通常是時變的，平時會出現(xiàn)bug，而當你要研究這個問題的時候，bug就消失了，或者每次研究的時候bug的結果都是在變化的)。
為了解決異步計算的挑戰(zhàn)，微軟開發(fā)了P語言，這是一種用于異步事件驅(qū)動型應用程序中建模和指定協(xié)議的編程語言。該項目是微軟研究人員和工程師與加州大學伯克利分校以及倫敦帝國學院的學術研究人員一起合作開發(fā)的。
圖1：P語言工具鏈流程圖
P語言編程人員在高層編寫協(xié)議及其規(guī)范。P編譯器提供用于并發(fā)相關競爭條件的自動測試和運行協(xié)議的可執(zhí)行代碼。P語言對建模并發(fā)性(modeling concurrency)、指定安全性(specifying safety)和活性屬性(liveness property)提供一流的支持，并使用系統(tǒng)級搜索檢查程序是否滿足規(guī)范。
在這些方面，P語言與Leslie Lamport的TLA +和Gerard Holzmann的SPIN相似。與TLA +和SPIN不同的是，P程序也可以被編譯成可執(zhí)行的C代碼。這種能力搭建了高級模型和低級實現(xiàn)之間的橋梁，并消除了程序員之間接受形式化建模和規(guī)范的巨大障礙。
圖2：通信狀態(tài)機
P中的編程模型基于并發(fā)執(zhí)行狀態(tài)機，通過事件進行通信，每個事件伴隨一個有類型的負載值。基于線性輸入和獨特指針的內(nèi)存管理系統(tǒng)提供安全的內(nèi)存管理和無數(shù)據(jù)競爭的并發(fā)執(zhí)行。在這方面，P類似于現(xiàn)代系統(tǒng)編程語言，例如Rust。
P在微軟的軟件開發(fā)中，最初被用在Windows 8.1和Windows Phone中運送USB3.0驅(qū)動程序。這些驅(qū)動程序處理著Windows生態(tài)系統(tǒng)中眾多最重要的周邊設備，如今已經(jīng)在數(shù)億臺設備上運行。P在驅(qū)動程序設計初期就啟用了數(shù)百種競爭條件和Heisenbugs的檢測和調(diào)試，現(xiàn)在廣泛應用于Windows中的驅(qū)動程序開發(fā)。P在Windows內(nèi)核中早期積累的經(jīng)驗導致了P#的開發(fā)，P#是通過C#拓展提供狀態(tài)機和系統(tǒng)測試的框架。與P相反，P#中的方法是最小化語法拓展，并最大限度的利用庫提供建模，規(guī)范和測試功能。
P正在改變Azure的云基礎架構的發(fā)展。Azure類似于其他云提供商，面臨著由意料之外的并發(fā)競爭條件或軟硬件故障引起的Heisenbug的挑戰(zhàn)。這些錯誤導致實時服務的中斷，這是云服務的客戶和提供商所面臨的巨大問題。P和P#正用于在已部署的服務中查找和調(diào)試Heisenbug，并在部署前設計和驗證新服務。P允許工程師在大型Azure服務中的組件之間精確的模擬異步接口。它還允許工程師發(fā)現(xiàn)和調(diào)試他們桌面設備上的問題，否則這些問題在部署服務幾個月甚至幾年之后都難以找到根源。
使P特別適用于驗證容錯的分布式服務的一個重要特征，是它能夠進行徹底的失效恢復(failover)測試，即在意外故障發(fā)生時保證服務能夠恢復，并繼續(xù)之前的操作。網(wǎng)絡信息丟失和單個狀態(tài)機故障都被建模為事件。將故障建模為P中的一個事件，可以完全自動化完成故障注入，并可以在大量事件排序和故障的情況下對失效恢復進行測試，而程序員并不需要做太多的工作。
P的系統(tǒng)測試能力能夠徹底地搜索由并發(fā)發(fā)送事件的非確定性排序引起的選擇。然而，其能力主要應用在處理明確數(shù)據(jù)輸入方面，尤其是對大范圍輸入的搜索。這種限制使得難以將P應用到復雜性來源主要是不確定的輸入下進行決策這樣的應用中，例如機器人技術。微軟正在研究如何處理大量不確定的輸入域，主要通過研究符號和概率技術來應對這一挑戰(zhàn)。
京公網(wǎng)安備 11010502049343號