Verifying concurrent, crash-safe systems with Perennial
Verifying concurrent, crash-safe systems with Perennial
复制标题
使用 Perennial 验证并发、防碰撞系统
DOI：
10.1145/3341301.3359632
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Zeldovich, Nickolai
中科院分区：
文献类型：
--
作者：
Chajed, Tej;Tassarotti, Joseph;Kaashoek, Frans;Zeldovich, Nickolai
本文介绍了一个用于验证并发碰撞安全系统的框架Perennial。Perennial使用三种技术扩展了Iris并发框架，以支持崩溃安全推理：恢复租约、恢复帮助和版本内存。为了简化应用程序的开发和部署，Perennial提供了Goose， Go的一个子集，以及从该子集到Perennial模型的转换器，支持Go线程、数据结构和文件系统原语的推理。我们使用Perennial和Goose实现并验证了一个崩溃安全的并发邮件服务器，它在多核上实现了加速。Perennial和Iris都使用Coq证明助手，邮件服务器和框架的证明都是机器检查的。
This paper introduces Perennial, a framework for verifying concurrent, crash-safe systems. Perennial extends the Iris concurrency framework with three techniques to enable crash-safety reasoning: recovery leases, recovery helping, and versioned memory. To ease development and deployment of applications, Perennial provides Goose, a subset of Go and a translator from that subset to a model in Perennial with support for reasoning about Go threads, data structures, and file-system primitives. We implemented and verified a crash-safe, concurrent mail server using Perennial and Goose that achieves speedup on multiple cores. Both Perennial and Iris use the Coq proof assistant, and the mail server and the framework's proofs are machine checked.
登录
查看更多内容
DOI：
10.1145/3314221.3314585
发表时间：
2019-06
期刊：
Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation
影响因子：
--
作者：
Tej Chajed;Joseph Tassarotti;M. Kaashoek;Nickolai Zeldovich
通讯作者：
Tej Chajed;Joseph Tassarotti;M. Kaashoek;Nickolai Zeldovich
通过崩溃优化对文件系统进行一键式验证
DOI：
--
发表时间：
2016
期刊：
USENIX Annual Technical Conference
影响因子：
--
作者：
Helgi Sigurbjarnarson;James Bornholt;Nicolas Christin;L. Cranor
通讯作者：
L. Cranor
使用 CSPEC 中的移动器验证并发软件
DOI：
--
发表时间：
2018
期刊：
USENIX Symposium on Operating Systems Design and Implementation
影响因子：
--
作者：
Tej Chajed;Frans Kaashoek;Mit Csail;Microsoft Butler Lampson;Nickolai Zeldovich;M. Kaashoek;Microsoft Research
通讯作者：
Microsoft Research
Nickel：信息流控制系统的设计和验证框架
DOI：
--
发表时间：
2018
期刊：
Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI
影响因子：
--
作者：
Sigurbjarnarson, Helgi;Nelson, Luke;Castro-Karney, Bruno;Bornholt, James;Torlak, Emina;Wang, Xi
通讯作者：
Wang, Xi
带有子机的 ASM 的模块化、防碰撞改进
DOI：
10.1016/j.scico.2016.04.009
发表时间：
2016
期刊：
Sci. Comput. Program.
影响因子：
--
作者：
G. Ernst;J. Pfähler;G. Schellhorn;W. Reif
通讯作者：
W. Reif