Stateless Model Checking Under a Reads-Value-From Equivalence

Pratyush Agarwal, Krishnendu Chatterjee, Shreya Pathak, Andreas Pavlogiannis, Viktor Toman

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

12 Citations (Scopus)
236 Downloads (Pure)

Abstract

Stateless model checking (SMC) is one of the standard approaches to the verification of concurrent programs. As scheduling non-determinism creates exponentially large spaces of thread interleavings, SMC attempts to partition this space into equivalence classes and explore only a few representatives from each class. The efficiency of this approach depends on two factors: (a) the coarseness of the partitioning, and (b) the time to generate representatives in each class. For this reason, the search for coarse partitionings that are efficiently explorable is an active research challenge. In this work we present RVF-SMC, a new SMC algorithm that uses a novel reads-value-from (RVF) partitioning. Intuitively, two interleavings are deemed equivalent if they agree on the value obtained in each read event, and read events induce consistent causal orderings between them. The RVF partitioning is provably coarser than recent approaches based on Mazurkiewicz and “reads-from” partitionings. Our experimental evaluation reveals that RVF is quite often a very effective equivalence, as the underlying partitioning is exponentially coarser than other approaches. Moreover, RVF-SMC generates representatives very efficiently, as the reduction in the partitioning is often met with significant speed-ups in the model checking task.

Original languageEnglish
Title of host publicationComputer Aided Verification - 33rd International Conference, CAV 2021, Proceedings : Proceedings
EditorsAlexandra Silva, K. Rustan, M. Leino
Number of pages26
Volume1
Place of publicationCham
PublisherSpringer
Publication date2021
Pages341-366
ISBN (Print)978-3-030-81684-1
ISBN (Electronic)978-3-030-81685-8
DOIs
Publication statusPublished - 2021
Event33rd International Conference, CAV 2021 - Virtual event
Duration: 20 Jul 202123 Jul 2021

Conference

Conference33rd International Conference, CAV 2021
LocationVirtual event
Period20/07/202123/07/2021
SeriesLecture Notes in Computer Science
Volume12759
ISSN0302-9743

Fingerprint

Dive into the research topics of 'Stateless Model Checking Under a Reads-Value-From Equivalence'. Together they form a unique fingerprint.

Cite this