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