ArchSummit全球架构师峰会门票9折倒计时中~ 了解详情
写点什么

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

  • 2016 年 10 月 16 日
  • 本文字数:831 字

    阅读完需:约 3 分钟

微软最近开源了 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 条目饿死的现象。

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

2016 年 10 月 16 日 19:004326

评论

发布
暂无评论
发现更多内容

小熊派开发板实践:智慧路灯沙箱实验之真实设备接入

华为云开发者联盟

物联网 IoT 路灯

面经手册 · 第16篇《码农会锁,ReentrantLock之公平锁讲解和实现》

小傅哥

Java 面试 小傅哥 ReentrantLock 公平锁

vivo 云服务海量数据存储架构演进与实践

vivo互联网技术

数据库 架构 云服务 数据存储

JDK8中的新时间API:Duration Period和ChronoUnit介绍

程序那些事

java8 jdk8 新特性 程序那些事 时间API

网易云音乐基于 Flink + Kafka 的实时数仓建设实践

Apache Flink

flink

一场关于FLV是否要支持HEVC的争论

wangwei1237

技术文化

环球易购数据平台如何做到既提速又省钱?

苏锐

大数据 hdfs S3 CDH 成本优化

Linux-技术专题-Linux命令如何进行查看进程

浩宇の天尚

给萌新HTML5 入门指南(二)

葡萄城技术团队

redis的stream类型命令详解

LLLibra146

redis stream 消息队列

程序人急速变富指南(一)

陆陆通通

程序员 职业 财富 认知 眼界

架构师训练营 W03 总结

Geek_f06ede

架构师训练

开源技术够用了么?我的 NAS 选型与搭建过程

LeanCloud

开源 NAS

CloudQuery V1.2.0 版本发布

CloudQuery社区

数据库 sql 编辑器 工具软件

甲方日常 44

句子

工作 随笔杂谈 日常

深度解读智能推荐系统搭建之路 | 会展云技术揭秘

京东科技开发者

人工智能 推荐系统

Worktile旗下智能化研发管理工具PingCode 宣布25人以下免费

PingCode

团队管理 程序人生 敏捷开发 研发管理 研发管理工具

第一届“多模态自然语言处理研讨会”精彩回顾(免费获取PPT)

京东科技开发者

人工智能 自然语言处理

TensorFlow 篇 | TensorFlow 数据输入格式之 TFRecord

Alex

tensorflow keras dataset tfrecord

央视呼吁电商双十一少一些套路:应该严打网店套路营销

石头IT视角

「排序算法」图解双轴快排

bigsai

排序算法 快速排序 双轴快排

英特尔独显终于来了!锐炬®Xe MAX为非凡S3x带来设计师级创作体验

新闻科技资讯

腾讯内容首发:分布式核心原理解析笔记+分布式消息中间件实践笔记PDF版

Java架构追梦

Java 架构 面试 分布式 消息中间件

23张图!万字详解「链表」,从小白到大佬!

王磊

Java 数据结构与算法

Linux高级编程常用的系统调用函数汇总

哒宰的自我修养

Linux 线程 网络编程 进程 MySQL数据库

5G时代的到来对直播的影响

anyRTC开发者

5G 音视频 WebRTC 直播 RTC

如何在面试中解释关键机器学习算法

计算机与AI

学习 数据科学

接口测试用例编写和测试关注点

测试人生路

接口测试 测试用例

架构师训练营 W03 作业

Geek_f06ede

架构师训练

Redis-缓存雪崩,缓存击穿,缓存穿透

topsion

redis

推进AI融合 2020 LF AI & DATA DAY(AI开源日)即将召开

AI在游戏反外挂中的应用与实践

AI在游戏反外挂中的应用与实践

微软开源P语言,实现安全的异步事件驱动编程_微软_Sergio De Simone_InfoQ精选文章