P語(yǔ)言是一款由微軟、加州大學(xué)伯克利分校和倫敦帝國(guó)學(xué)院共同研發(fā)完成的編程語(yǔ)言，它在處理并發(fā)、故障切換等方面具有很強(qiáng)的優(yōu)勢(shì)。本文介紹了P語(yǔ)言的起源、特性及其使用場(chǎng)景。以下是譯文。

　　新興應(yīng)用程序的復(fù)雜性需要使用新興的方式去理解，然后才能高效地去構(gòu)建、測(cè)試和調(diào)試?，F(xiàn)在的應(yīng)用程序常常會(huì)使用云資源，采用人工智能技術(shù)，并嵌入到物理設(shè)備中。這三個(gè)因素的結(jié)合使得軟件開(kāi)發(fā)變得非常困難。

　　通常來(lái)說(shuō)，這些現(xiàn)代應(yīng)用程序都具有異步性，主要表現(xiàn)在：為了提高性能，請(qǐng)求者在當(dāng)前操作完成之前可繼續(xù)執(zhí)行后面的操作。異步不可避免地會(huì)產(chǎn)生并發(fā)，并帶來(lái)一些臭名昭著的坑，例如競(jìng)態(tài)條件和海森堡bug（軟件錯(cuò)誤，通常與時(shí)序相關(guān)，但在調(diào)查其原因的時(shí)候該錯(cuò)誤可能會(huì)消失，這是因?yàn)楫?dāng)前環(huán)境已經(jīng)產(chǎn)生了變化）。為了應(yīng)對(duì)異步計(jì)算帶來(lái)的挑戰(zhàn)，我們開(kāi)發(fā)了P，一種用于在異步事件驅(qū)動(dòng)應(yīng)用程序中建模和制定協(xié)議的編程語(yǔ)言。該項(xiàng)目是微軟研發(fā)人員以及加州大學(xué)伯克利分校和倫敦帝國(guó)學(xué)院的學(xué)術(shù)研究人員之間通力合作的結(jié)果。

　　P語(yǔ)言工具鏈流程圖

　　P的程序員在上層編寫(xiě)協(xié)議及其規(guī)范。P編譯器提供針對(duì)競(jìng)態(tài)條件的自動(dòng)化測(cè)試和承載了指定協(xié)議的可執(zhí)行程序。P在如下這幾個(gè)方面提供了一流的支持，包括：對(duì)并發(fā)進(jìn)行建模、指定安全和活性屬性、系統(tǒng)性的搜索并檢查程序是否滿(mǎn)足其規(guī)范。對(duì)于這些功能來(lái)說(shuō)，P與Leslie Lamport的TLA+和Gerard Holzmann的SPIN相似。但與TLA+和SPIN不同的是，P程序也可以編譯成可執(zhí)行的C代碼。這種能力在高級(jí)模型和低級(jí)實(shí)現(xiàn)之間起到了橋梁的作用，也讓程序員可以更容易地接受正式的建模模型和規(guī)范。