微软开源 P 语言,实现安全的异步事件驱动编程

简介:

微软最近开源了P语言,致力于在Linux、macOS和Windows上编写安全的异步事件驱动程序。

微软将P描述为一种领域特定语言,对异步系统的组件间通信进行建模,例如嵌入式、网络或分布式系统。P程序是通过有限状态机(finite state machine)来定义的,这些状态机会并发运行。每个状态机都有一个输入队列、状态、转换、机器本地存储,并且可以发送异步信息给其他状态机。在P中的基本操作要么是更新本地存储,发送消息,要么就是创建新的状态机。如下的代码片段展示了如何使用P来描述一个状态及其转换。除此之外,它还展现了如何发送消息或创建新的状态机:

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程序能够使用模型检查功能来进行核实。这样的话,就允许开发人员确保所有的事件均能得到及时地处理。对于P程序来说,要想保证响应性,它的状态机就要处理每个状态上所有可以出队(dequeue)的事件。这种做法并不一定总是可行,因此对一些事件可能会进行延迟处理。在这种情况下,语言能够确保某个事件不会无限期延迟。P编译器能够核实程序的状态,还可以生成C代码,并交给C编译器执行,另外,它还可以输出Zing模型,用于系统测试。Zing是一个针对并发程序的开源模型检查器,它能够系统性地暴露一个模型所有可能出现的状态。

微软使用P语言实现和检验了Windows 8 USB设备驱动栈的核心功能。按照微软的说法,工程师使用P来序列化大量来自硬件、操作系统、功能驱动以及其他驱动组件的不同事件,提升了性能和可靠性。他们尤其指出,在新的USB hub驱动中,非法内存访问和竞态条件的数量不那么明显了,同时,枚举时间快了30%,也没有观察到worker条目饿死的现象。

文章转载自 开源中国社区 [http://www.oschina.net]

目录
相关文章
|
JavaScript 前端开发 Dubbo
注册中心设计 Ap 与 CP 区别|学习笔记
快速学习注册中心设计 Ap 与 CP 区别
1092 0
注册中心设计 Ap 与 CP 区别|学习笔记
|
新零售 供应链 监控
蒙牛集团信息技术助理副总裁、CIO张决:双中台助力蒙牛数字化转型 | 阿里CIO学院名人堂
12月3日,2020阿里CIO学院在杭州举行。400位企业CEO、CTO、CIO齐聚一堂,共同探讨企业数字化转型经验。今年新冠 疫情爆发,给企业带来不小挑战,到场嘉宾表示,数字化已经成为企业未来发展最大的确定性。 本次峰会由阿里CIO学院主办。据阿里CIO学院院长洪英介绍,400位嘉宾分别来自央企、国企、民企,都是企业信息化建设的领导者。
蒙牛集团信息技术助理副总裁、CIO张决:双中台助力蒙牛数字化转型  | 阿里CIO学院名人堂
|
12月前
|
测试技术
提升软件测试效率的五大策略
【10月更文挑战第13天】 本文将探讨如何通过优化测试流程、引入自动化测试、加强测试用例设计、培养高素质测试团队和持续反馈改进等五大策略,来显著提升软件测试的效率。这些方法不仅适用于不同类型的软件项目,还能有效降低测试成本,提高软件质量。
1039 0
|
Dart 监控 算法
Flutter性能优化分析
使用工具来分析Flutter的性能瓶颈
749 0
|
搜索推荐 算法 数据挖掘
推荐系统概念和应用场景|学习笔记
快速学习推荐系统概念和应用场景
781 0
推荐系统概念和应用场景|学习笔记
|
存储 算法 安全
|
数据采集 存储 算法
央视网的融媒体数据中台实践
作为中央电视台新媒体平台,央视网在不断升级建设“一网(中央重点新闻网站)+一端(移动客户端)+新媒体集成播控平台(IPTV、手机电视、互联网电视)+市场端口连接”的全新传播格局,打造“无处不在”新入口的同时也深刻认识到,需要让大数据成为驱动整个企业发展的核心动能。
3496 0
央视网的融媒体数据中台实践
|
存储 缓存 运维
案例解析 | 高效上云,助力垂直电商降本增效
今天,人们通过天猫、淘宝、苏宁进行网络购物,不仅方便,而且快乐,通过盒马、饿了么享受更加快捷的本地生活服务,与此同时,家电、食品等垂直领域的电商平台,也越来越有特色。本篇文章将以A公司全面上云为案例,详解上云带来的核心价值以及上云方案和步骤,希望能给您的业务带来一定帮助。
858 0
案例解析 | 高效上云,助力垂直电商降本增效
|
缓存 测试技术 Linux
《Linux内核精髓:精通Linux内核必会的75个绝技》一HACK #20 使用fio进行I/O的基准测试
本节书摘来自华章出版社《Linux内核精髓:精通Linux内核必会的75个绝技》一书中的第3章,第3.4节,作者 竹部 晶雄、平松 雅巳,更多章节内容可以访问云栖社区“华章计算机”公众号查看
2223 0
《Linux内核精髓:精通Linux内核必会的75个绝技》一HACK #20 使用fio进行I/O的基准测试
|
程序员 C++
【误区】技术部经理vs技术经理 —— 一字之差谬以千里
  技术部经理、技术经理,就差了一个字,但是含义、职责、侧重却是差了很远。我们先查查他们都是什么含义。     技术经理:技术经理负责组织制定各种技术标准和技术规范并保证实施,他们既是精通某个领域专业的精英,又是擅长团队领导的管理者。
1852 0