A pragmatic approach to stateful partial order reduction

DOI10.1007/978-3-031-24950-1_7zbMATH Open1529.68156arXiv2211.11942OpenAlexW4316662751MaRDI QIDQ6132490FDOQ6132490

Authors: Berk Çirisci, Constantin Enea, Azadeh Farzan, Suha Orhun Mutluergil 

Publication date: 17 August 2023

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Abstract: Partial order reduction (POR) is a classic technique for dealing with the state explosion problem in model checking of concurrent programs. Theoretical optimality, i.e., avoiding enumerating equivalent interleavings, does not necessarily guarantee optimal overall performance of the model checking algorithm. The computational overhead required to guarantee optimality may by far cancel out any benefits that an algorithm may have from exploring a smaller state space of interleavings. With a focus on overall performance, we propose new algorithms for stateful POR based on the recently proposed source sets, which are less precise but more efficient than the state of the art in practice. We evaluate efficiency using an implementation that extends Java Pathfinder in the context of verifying concurrent data structures.

Full work available at URL: https://arxiv.org/abs/2211.11942

Recommendations

• Optimal dynamic partial order reduction
• Source sets: a foundation for optimal dynamic partial order reduction
• Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique
• scientific article; zbMATH DE number 1507206
• Dynamic partial-order reduction for model checking software

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• LCF considered as a programming language
• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• Dynamic partial-order reduction for model checking software
• Title not available (Why is that?)
• From invariant checking to invariant inference using randomized search
• Title not available (Why is that?)
• Prespecification in data refinement
• Tools and Algorithms for the Construction and Analysis of Systems
• State space reduction using partial order techniques
• Title not available (Why is that?)
• Title not available (Why is that?)
• Delay-bounded scheduling
• Using partial orders for the efficient verification of deadlock freedom and safety properties
• Comparing Source Sets and Persistent Sets for Partial Order Reduction
• Stateless model checking for TSO and PSO
• Bounded phase analysis of message-passing programs
• Automated hypersafety verification
• Verification of distributed programs using representative interleaving sequences
• Source sets: a foundation for optimal dynamic partial order reduction

Cited In (4)

• Partial Order Reduction for State/Event LTL
• Unfolding-based dynamic partial order reduction of asynchronous distributed programs
• What's wrong with on-the-fly partial order reduction
• Reconciling preemption bounding with DPOR

This page was built for publication: A pragmatic approach to stateful partial order reduction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6132490)