Natural proofs for asynchronous programs using almost-synchronous reductions

Ankush Desai, Pranav Garg, P. Madhusudan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We consider the problem of provably verifying that an asynchronous message-passing system satisfies its local assertions. We present a novel reduction scheme for asynchronous event-driven programs that finds almost-synchronous invariants- invariants consisting of global states where message buffers are close to empty. The reduction finds almostsynchronous invariants and simultaneously argues that they cover all local states. We show that asynchronous programs often have almost-synchronous invariants and that we can exploit this to build natural proofs that they are correct. We implement our reduction strategy, which is sound and complete, and show that it is more effective in proving programs correct as well as more efficient in finding bugs in several programs, compared to current search strategies which almost always diverge. The high point of our experiments is that our technique can prove the Windows Phone USB Driver written in P [9] correct for the responsiveness property, which was hitherto not provable using state-of-the-art model-checkers.

Original languageEnglish (US)
Title of host publicationProceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA
PublisherAssociation for Computing Machinery
Pages709-725
Number of pages17
ISBN (Electronic)9781450325851
DOIs
StatePublished - Oct 15 2014
Event2014 ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2014 - Portland, United States
Duration: Oct 20 2014Oct 24 2014

Publication series

NameProceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA

Conference

Conference2014 ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2014
CountryUnited States
CityPortland
Period10/20/1410/24/14

Keywords

  • Almost-synchronous reductions
  • Asynchronous programs
  • Concurrency
  • Distributed programs
  • Natural proofs
  • Reductions

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Natural proofs for asynchronous programs using almost-synchronous reductions'. Together they form a unique fingerprint.

Cite this