Verifying concurrent software using movers in CSPEC

Authors: 

Tej Chajed and Frans Kaashoek, MIT CSAIL; Butler Lampson, Microsoft; Nickolai Zeldovich, MIT CSAIL

Abstract: 

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.

Open Access Media

USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.

Presentation Audio

BibTeX
@inproceedings {222565,
author = {Tej Chajed and Frans Kaashoek and Butler Lampson and Nickolai Zeldovich},
title = {Verifying concurrent software using movers in {CSPEC}},
booktitle = {13th {USENIX} Symposium on Operating Systems Design and Implementation ({OSDI} 18)},
year = {2018},
isbn = {978-1-931971-47-8},
address = {Carlsbad, CA},
pages = {306--322},
url = {https://www.usenix.org/conference/osdi18/presentation/chajed},
publisher = {{USENIX} Association},
}