微軟剛開源的這種開發語言，竟然是個 P

編者按：微軟近日發布了一篇研究報告，介紹了一種為非同步性、容錯性和不確定性而設計的 P 語言，實現安全的非同步事件驅動編程。該語言基於事件進行通信，能夠很好的解決並發操作所帶來的問題，並能夠在軟體的構建、測試和調試等各個階段發揮作用。AI 研習社編譯如下。文中相關鏈接詳見「閱讀原文」。

新型軟體的複雜性導致了編程人員需要新的方法來理解，並有效地構建、測試和調試這些系統。如今的軟體通常使用雲資源，嵌入在物理世界的設備中，並採用人工智慧技術。這三個因素使得今天的軟體系統難以發展。

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

為了解決非同步計算的挑戰，微軟開發了P語言，這是一種用於非同步事件驅動型應用程序中建模和指定協議的編程語言。該項目是微軟研究人員和工程師與加州大學伯克利分校以及倫敦帝國學院的學術研究人員一起合作開發的。

圖1：P語言工具鏈流程圖

P語言編程人員在高層編寫協議及其規範。P編譯器提供用於並發相關競爭條件的自動測試和運行協議的可執行代碼。P語言對建模並發性（modeling concurrency）、指定安全性(specifying safety)和活性屬性(liveness property)提供一流的支持，並使用系統級搜索檢查程序是否滿足規範。

在這些方面，P語言與Leslie Lamport的TLA +和Gerard Holzmann的SPIN相似。與TLA +和SPIN不同的是，P程序也可以被編譯成可執行的C代碼。這種能力搭建了高級模型和低級實現之間的橋樑，並消除了程序員之間接受形式化建模和規範的巨大障礙。

圖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應用到複雜性來源主要是不確定的輸入下進行決策這樣的應用中，例如機器人技術。微軟正在研究如何處理大量不確定的輸入域，主要通過研究符號和概率技術來應對這一挑戰。

微軟在github上開源了P語言：

https://github.com/p-org/P

更多的P語言配套工具參見此鏈接：

https://github.com/p-org

點擊展開全文

喜歡這篇文章嗎？立刻分享出去讓更多人知道吧！