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

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

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

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

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

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

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