Verifying concurrent software using movers in CSPEC
Verifying concurrent software using movers in CSPEC
复制标题
使用 CSPEC 中的移动器验证并发软件
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Microsoft Research
中科院分区：
文献类型：
--
作者：
Tej Chajed;Frans Kaashoek;Mit Csail;Microsoft Butler Lampson;Nickolai Zeldovich;M. Kaashoek;Microsoft Research
编写并发系统软件容易出错，因为多个过程或线程可以在许多方面交织，并且很容易忘记本文介绍CSPEC，这是一个正式验证并发软件的框架案件是遗漏的通过使用图层进行模块化，并提供可重复使用的证明模式来评估CSPEC，我们实现并证明了CMAIL的正确性，这是一个简单的同步邮件服务器，该结果表明了SMTP和POP3的结果。 CSPEC的动作和模式允许有关CMAIL中复杂的并发样式的推理。
Writing concurrent systems software is error-prone, because multiple processes or threads can interleave in many ways, and it is easy to forget about a subtle corner case. This paper introduces CSPEC, a framework for formal verification of concurrent software, which ensures that no corner cases are missed. The key challenge is to reduce the number of interleavings that developers must consider. CSPEC uses mover types to re-order commutative operations so that usually it’s enough to reason about only sequential executions rather than all possible interleavings. CSPEC also makes proofs easier by making them modular using layers, and by providing a library of reusable proof patterns. To evaluate CSPEC, we implemented and proved the correctness of CMAIL, a simple concurrent Maildir-like mail server that speaks SMTP and POP3. The results demonstrate that CSPEC’s movers and patterns allow reasoning about sophisticated concurrency styles in CMAIL.
影响因子：
--
作者：
Ilya Sergey;James R. Wilcox;Zachary Tatlock
通讯作者：
Ilya Sergey;James R. Wilcox;Zachary Tatlock