微软开源P语言,解决异步计算的挑战问题

微软近日发布了一篇研究报告,介绍了一种为异步性、容错性和不确定性而设计的P语言,实现安全的异步事件驱动编程。该语言基于事件进行通信,能够很好的解决并发操作所带来的问题,并能够在软件的构建、测试和调试等各个阶段发挥作用。雷锋网(公众号:雷锋网)编译如下。

新型软件的复杂性导致了编程人员需要新的方法来理解,并有效地构建、测试和调试这些系统。如今的软件通常使用云资源,嵌入在物理世界的设备中,并采用人工智能技术。这三个因素使得今天的软件系统难以发展。

通常现代应用需要异步性来提高性能,比如在下面这种情形:操作的请求者在发起操作后继续运行,而不需要等待操作完成。异步不可避免的会导致并发,以及臭名昭著的竞争现象和Heisenbug(一种奇怪的软件bug,通常是时变的,平时会出现bug,而当你要研究这个问题的时候,bug就消失了,或者每次研究的时候bug的结果都是在变化的)。

为了解决异步计算的挑战,微软开发了P语言,这是一种用于异步事件驱动型应用程序中建模和指定协议的编程语言。该项目是微软研究人员和工程师与加州大学伯克利分校以及伦敦帝国学院的学术研究人员一起合作开发的。

 


 

图1:P语言工具链流程图

P语言编程人员在高层编写协议及其规范。P编译器提供用于并发相关竞争条件的自动测试和运行协议的可执行代码。P语言对建模并发性(modeling concurrency)、指定安全性(specifying safety)和活性属性(liveness property)提供一流的支持,并使用系统级搜索检查程序是否满足规范。

在这些方面,P语言与Leslie Lamport的TLA +和Gerard Holzmann的SPIN相似。与TLA +和SPIN不同的是,P程序也可以被编译成可执行的C代码。这种能力搭建了高级模型和低级实现之间的桥梁,并消除了程序员之间接受形式化建模和规范的巨大障碍。

 


 

图2:通信状态机

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应用到复杂性来源主要是不确定的输入下进行决策这样的应用中,例如机器人技术。微软正在研究如何处理大量不确定的输入域,主要通过研究符号和概率技术来应对这一挑战。

本文转自d1net(转载)

时间: 2024-10-22 11:52:06

微软开源P语言,解决异步计算的挑战问题的相关文章

Facebook、微信团队、Twitter、微软开源软件列表一览

  编者按:本文来自微信公众号"InfoQ"(ID:infoqchina),编辑小智:36氪经授权发布. 对于为什么要发布开源项目,Facebook开源项目负责人曾经解释过:一是开源能够帮助他人更快地开发软件,促进世界创新,主要是社会价值层面的考虑.二是开源能够倒逼Facebook的工程师写出更好的代码.三是开源能够更有效利用社区的力量,帮助Facebook一起解决难题.开源,让世界更美好,不是吗? Facebook开源软件列表 从Facebook的GitHub账户中可以看到,Face

微软爱开源?| 启路CTO朱永光为你讲解微软开源的那些事

编者按:随着微软的股价节节攀升,同时在最近的硬件大战中力克老对手苹果,大家熟知的那个微软又回到了大家的视野,本文给很多不熟悉微软开源技术的朋友普及一下微软最近几年在开源方面所做的努力和成效,毕竟很多人对微软的技术还停留在10年前的认知上,自从微软新CEO上任后,进行了一系列的大刀阔斧的改革,其中拥抱Linux是浓墨重彩的一笔.本文选自于启路CTO朱永光大神在中生代十月十城成都的分享,朱老师在讲解干货的同时,也不忘现场写代码演示如何搭建简单的Hello World,欢迎大家观看视频! 过去几年中微

TensorFlow 1.0 正式发布;微软开源无人机虚拟训练平台 AirSim | AI开发者头条

TensorFlow 1.0  正式发布! 在昨晚揭幕的 TensorFlow 开发者峰会上,谷歌正式发布了 TensorFlow 1.0 版本.新版本带来三大主要优化: 大幅提升的运算速度,尤其是对于多 GPU.分布式计算场景. 对高级别 API 有更好的兼容性,尤其完全兼容 Keras 改进 API 稳定性  注:本次峰会是 TensorFlow 史上第一届开发者峰会,在加州山景城举行,颇值得大家关注.详情请关注雷锋网后续报道. TensorFlow 1.0 详情:http://www.le

C语言解决百钱买百鸡问题_C 语言

我国古代数学家张丘建在<算经>一书中曾提出过著名的"百钱买百鸡"问题,该问题叙述如下:鸡翁一,值钱五:鸡母一,值钱三:鸡雏三,值钱一:百钱买百鸡,则翁.母.雏各几何? 翻译过来,意思是公鸡一个五块钱,母鸡一个三块钱,小鸡三个一块钱,现在要用一百块钱买一百只鸡,问公鸡.母鸡.小鸡各多少只? 题目分析 如果用数学的方法解决百钱买百鸡问题,可将该问题抽象成方程式组.设公鸡x只,母鸡y只,小鸡z只,得到以下方程式组: A:5x+3y+1/3z = 100 B:x+y+z = 100

c语言-算法训练 未名湖边的烦恼 怎么用C语言解决

问题描述 算法训练 未名湖边的烦恼 怎么用C语言解决 问题描述 每年冬天,北大未名湖上都是滑冰的好地方.北大体育组准备了许多冰鞋,可是人太多了,每天下午收工后,常常一双冰鞋都不剩. 每天早上,租鞋窗口都会排起长龙,假设有还鞋的m个,有需要租鞋的n个.现在的问题是,这些人有多少种排法,可以避免出现体育组没有冰鞋可租的尴尬场面.(两个同样需求的人(比如都是租鞋或都是还鞋)交换位置是同一种排法) 输入格式 两个整数,表示m和n 输出格式 一个整数,表示队伍的排法的方案数. 样例输入 3 2 样例输出

赛门铁克误报微软系统文件病毒事件+解决方法_常用工具

赛门铁克误报微软系统文件病毒事件+解决方法 赛门铁克发出的LiveUpdate更新定义错误地把微软简体中文Windows XP中的2个系统文件当作Backdoor.Haxdoor进行了删除,从而造成Windows系统在根据错误检测重启后无法运行. 受到影响的是应用了微软KB924270安全更新的微软简体中文Windows XP Service Pack 2 系统,应用微软安全更新KB924270.而受影响的文件是netapi32.dll(5.1.2600.2976版本)和lsasrv.dll (

《R的极客理想——高级开发篇 A》一一1.5 R语言的导数计算

1.5 R语言的导数计算 问题 如何用R语言进行导数计算? 引言 高等数学是每个大学生都要学习的一门数学基础课,同时也可能是考完试后最容易忘记的一门知识.我在学习高数的时候绞尽脑汁,但始终都不知道为何而学,生活和工作基本用不到,就算是在计算机行业和金融行业,能直接用到高数的地方也少之又少,学术和实际应用真是相差太远了. 不过,R语言为我打开了一扇高数应用的大门,R语言不仅能方便地实现高等数学的计算,还可以很容易地把一篇论文中的高数公式应用于产品的实践中.因为R语言我重新学习了高数,让生活中充满数

c语言-用C语言实现一个计算100以内质数的程序,要求使用递归实现

问题描述 用C语言实现一个计算100以内质数的程序,要求使用递归实现 用C语言实现一个计算100以内质数的程序,要求使用递归实现 解决方案 http://zhidao.baidu.com/link?url=QMxaTs3t-q6cRPNsugPAqUX6KEl1_Ew12ljvr8G1HJlKKJXnuaYyFDONqGFNS6w-b5dOo0eSn8i5hwn4LjE3kq

《程序设计解题策略》——1.3 利用线段树解决区间计算问题

1.3 利用线段树解决区间计算问题 在现实生活中,我们经常遇到与区间有关的问题,例如,记录一个区间的最值(最大或最小值)和总量,并在区间的插入.删除.修改中维护这些最值和总量:再如,统计若干矩形并的面积.线段树拥有良好的树形二分特征,我们可以从其定义和结构中发现,在线段树的基础上完成这些问题的计算操作,是十分简捷和高效的.1.3.1 线段树的基本概念 一棵二叉树,记为T(a,b),参数a.b表示该节点表示区间[a,b].区间的长度b-a记为L.递归定义T[a,b]: 若区间长度L>1:区间[a,