微軟開源P語言,實現(xiàn)安全的異步事件驅動編程

責任編輯:editor004

作者:Sergio De Simone

2016-10-17 12:14:45

摘自:INFOQ

微軟最近開源了P語言,致力于在Linux、macOS和Windows上編寫安全的異步事件驅動程序。微軟將P描述為一種領域特定語言,對異步系統(tǒng)的組件間通信進行建模,例如嵌入式、網絡或分布式系統(tǒng)。

微軟最近開源了P語言,致力于在Linux、macOS和Windows上編寫安全的異步事件驅動程序。

微軟將P描述為一種領域特定語言,對異步系統(tǒng)的組件間通信進行建模,例如嵌入式、網絡或分布式系統(tǒng)。P程序是通過有限狀態(tài)機(finite state machine)來定義的,這些狀態(tài)機會并發(fā)運行。每個狀態(tài)機都有一個輸入隊列、狀態(tài)、轉換、機器本地存儲,并且可以發(fā)送異步信息給其他狀態(tài)機。在P中的基本操作要么是更新本地存儲,發(fā)送消息,要么就是創(chuàng)建新的狀態(tài)機。如下的代碼片段展示了如何使用P來描述一個狀態(tài)及其轉換。除此之外,它還展現(xiàn)了如何發(fā)送消息或創(chuàng)建新的狀態(tài)機:

...start state Init { entry { server = new Server(); raise SUCCESS; } on SUCCESS goto SendPing;state SendPing { entry { send server, PING, this; raise SUCCESS; } on SUCCESS goto WaitPong;}...

按照微軟的說法,P程序能夠使用模型檢查功能來進行核實。這樣的話,就允許開發(fā)人員確保所有的事件均能得到及時地處理。對于P程序來說,要想保證響應性,它的狀態(tài)機就要處理每個狀態(tài)上所有可以出隊(dequeue)的事件。這種做法并不一定總是可行,因此對一些事件可能會進行延遲處理。在這種情況下,語言能夠確保某個事件不會無限期延遲。P編譯器能夠核實程序的狀態(tài),還可以生成C代碼,并交給C編譯器執(zhí)行,另外,它還可以輸出Zing模型,用于系統(tǒng)測試。Zing是一個針對并發(fā)程序的開源模型檢查器,它能夠系統(tǒng)性地暴露一個模型所有可能出現(xiàn)的狀態(tài)。

微軟使用P語言實現(xiàn)和檢驗了Windows 8 USB設備驅動棧的核心功能。按照微軟的說法,工程師使用P來序列化大量來自硬件、操作系統(tǒng)、功能驅動以及其他驅動組件的不同事件,提升了性能和可靠性。他們尤其指出,在新的USB hub驅動中,非法內存訪問和競態(tài)條件的數量不那么明顯了,同時,枚舉時間快了30%,也沒有觀察到worker條目餓死的現(xiàn)象。

查看英文原文:Microsoft Open-Sources P Language for Safe Async Event-Driven Programming

鏈接已復制,快去分享吧

企業(yè)網版權所有?2010-2024 京ICP備09108050號-6京公網安備 11010502049343號