微软开源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