A pragmatic approach to stateful partial order reduction

DOI10.1007/978-3-031-24950-1_7MaRDI QIDQ6132490zbMATHOpenAlexFDO

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)

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

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)

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.

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

Cites work

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

Cited in

(5)

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

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)