兼具性能和正确性的异步系统代码很难编写。因此,工程师通常使用状态机符号设计异步代码,使用建模和验证工具来确保他们已经涵盖了极端情况,然后使用 C 等语言实现设计。他们使用各种性能技巧,因此结构状态机在无数细节中丢失了。随着实际代码的发展,最初写下的干净状态机图会随着实际代码的发展而过时,并且由此产生的系统变得难以理解和发展。
在 Windows 8 的开发过程中,微软的 USB 团队在 Windows 8.1 和 Windows 手机中推出 USB 3.0 时迈出了大胆的一步,并决定统一建模和编程。 USB 驱动程序堆栈的各种组件被指定为状态机,异步驱动程序代码是从这些状态机自动生成的。他们能够直接在状态机上使用模型检查技术来查找和修复设计错误。由于可执行代码是从源代码自动生成的,他们可以在状态机级别进行更改,并根据一个描述执行验证和编译。此方法用于为 Windows 8 附带的 USB 堆栈设计、验证和生成代码。生成的驱动程序堆栈不仅更可靠,而且性能更高,并将此方法的显着方面呈现为领域特定语言P 。
什么是P编程语言?
P 是一种编程语言,用于在异步事件驱动应用程序中建模和指定协议。它旨在解决异步计算的挑战,例如 asynchony 和 Heisenbugs。
它是如何工作的?
P 程序员在高层编写协议及其规范。 AP程序是机器的集合。机器通过事件异步地相互通信。事件排队,但机器需要以响应方式处理它们。 P 编译器提供用于运行协议的自动化测试和可执行代码。 P 为并发建模、指定安全性和使用系统搜索检查程序是否满足其规范提供一流的支持。 AP程序也可以编译成可执行的C代码。此功能弥合了高级模型和低级实现之间的差距,并消除了程序员接受形式化建模和规范的巨大障碍。
P 语言的扩展
P 正在改变 Azure 中云基础架构的开发。 Azure 与其他云提供商类似,它们面临由意外竞争条件和软件或硬件故障引起的 Heisenbugs 的挑战。这些错误会导致实时服务中断,这对云服务的客户和提供商来说都是一个巨大的问题。 P 用于在已部署的服务中查找和调试 Heisenbug,并在部署前设计和验证新服务。 P 允许工程师精确建模大型 Azure 服务中组件之间的异步接口。它还允许工程师在他们的桌面上发现和调试问题,否则这些问题在部署服务后需要数月甚至数年才能显现出来。
重要功能
P 的一个重要特性使其特别适合验证容错分布式服务,它能够执行彻底的故障转移测试,即在发生意外故障时验证服务是否恢复并恢复运行。网络消息丢失和单个状态机故障都被建模为事件。在 P 中将故障建模为事件完全自动化了故障注入,并且能够在大量事件排序和故障下系统地测试故障转移,而无需程序员的努力。
限制:
它在处理显式数据输入方面的能力是有限的,特别是当该输入跨越大域时,这使得很难将 P 应用于机器人等应用,在这些应用中,复杂性的重要来源是不确定输入下的决策制定。处理大型和不确定的输入域是一项正在进行的研究调查。
图片参考: www.microsoft.com
重要链接:
- 下载
- 使用 P 进行安全异步编程