Message Chains for Distributed System Verification

Federico Mora, Ankush Desai, Elizabeth Polgreen, Sanjit A. Seshia

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

Verification of asynchronous distributed programs is challenging due to the need to reason about numerous control paths resulting from the myriad interleaving of messages and failures. In this paper, we propose an automated bookkeeping method based on message chains. Message chains reveal structure in asynchronous distributed system executions and can help programmers verify their systems at the message passing level of abstraction. To evaluate our contributions empirically we build a verification prototype for the P programming language that integrates message chains. We use it to verify 16 benchmarks from related work, one new benchmark that exemplifies the kinds of systems our method focuses on, and two industrial benchmarks. We find that message chains are able to simplify existing proofs and our prototype performs comparably to existing work in terms of runtime. We extend our work with support for specification mining and find that message chains provide enough structure to allow existing learning and program synthesis tools to automatically infer meaningful specifications using only execution examples.
Original languageEnglish
Article number300
Pages (from-to)1-27
Number of pages27
JournalProceedings of the ACM on Programming Languages
Volume7
Issue numberOOPSLA2
DOIs
Publication statusPublished - 16 Oct 2023
Event2023 ACM SIGPLAN International Conference on Object-Oriented Programming Systems, Languages, and Applications - Cascais, Portugal
Duration: 25 Oct 202327 Oct 2023
https://2023.splashcon.org/

Keywords / Materials (for Non-textual outputs)

  • Formal verification
  • message passing
  • distributed systems

Fingerprint

Dive into the research topics of 'Message Chains for Distributed System Verification'. Together they form a unique fingerprint.

Cite this