Source-linked AI summary
Beyond Lemma Sharing -- Novel Parallelization Strategies for Property Directed Reachability
Verner Vlačić
TL;DR
PDR is widely used for automated hardware model checking, but exploiting parallelism within it remains difficult. The paper introduces preemptive propagation and ARPOS in an asynchronous MPI framework for rIC3, finding that preemptive propagation significantly improves performance for lemma-sharing strategies at higher processor counts.
Problem
Efficiently parallelizing PDR is difficult because its control flow is complex and offers limited data-parallelism opportunities.
Method
The paper introduces preemptive propagation and ARPOS, implemented through asynchronous MPI messaging and integrated with the rIC3 hardware model checker.
Results
At 16 processes, preemptive propagation increased speed-up from 1.16× to 2.23×, with this configuration also best-performing for the largest number of benchmarks.
Takeaways & Limitations
Preemptive propagation significantly boosts classical Lemma Sharing and ARPOS performance at higher processor counts.
Takeaways & Limitations
ARPOS was not competitive with Lemma Sharing in speed-ups, and the authors lacked a convincing explanation for this performance gap.
Abstract
from arXiv · showhide
Property Directed Reachability (PDR) is a commonly used technique for automated hardware model checking, yet efficiently parallelizing it remains a significant challenge. Existing approaches, such as lemma sharing, often suffer from limited scalability as processor counts increase. In this work, we present two novel sharing-based parallelization strategies, preemptive propagation and ARPOS, and compare their performance with classical lemma sharing. To this end, we develop an asynchronous MPI-based message passing framework for the state-of-the-art rIC3 hardware model checker. Experimental results on the 2025 Hardware Model Checking competition benchmark demonstrate that our preemptive propagation strategy yields a significant performance boost over classical lemma sharing.
1 Introduction
PDR is a central technique for automated model checking, including hardware safety verification, but exploiting parallelism within it remains difficult. This paper introduces and evaluates preemptive propagation and ARPOS using an asynchronous MPI framework integrated with rIC3.
- PDR incrementally constructs an inductive proof that fault states are unreachable and is central to modern hardware safety-checking tools.
- PDR-based tools have expanded beyond hardware model checking to software verification, automated planning, and scheduling.
- rIC3 is a state-of-the-art Rust implementation of PDR using the specialized GipSAT solver and won the 2025 Hardware Model Checking Competition.
- Parallelizing PDR remains challenging because its control-flow logic is complex and offers limited opportunities for data parallelism.
- The paper introduces preemptive propagation and ARPOS, implements them through asynchronous MPI messaging for rIC3, and evaluates them on the 2025 benchmark.
2 Related Work
Prior PDR parallelization ranges from independent portfolios to tightly coupled lemma sharing and fine-grained coordinator-worker designs. Existing approaches differ in how they divide search and share information across workers.
- Portfolio parallelization runs independently configured PDR or other safety-checking engines and stops when one returns Safe or Unsafe.
- Lemma-sharing approaches exchange inductive clauses between workers to reduce redundant work while preserving separate engine traces.
- ARPOS builds on lemma-sharing research as a new sharing-based strategy for PDR.
- Property partitioning decomposes an unrolled safety property into sub-properties that different workers verify while sharing information.
- PD-PDR distributes individual SAT queries from a central coordinator to workers, but was primarily evaluated for automated planning rather than hardware or software model checking.
3 Property Directed Reachability
PDR verifies safety by constructing frames that over-approximate reachable states and by blocking proof obligations through SAT queries. It returns Safe when frames converge or Unsafe when a bad state is reachable from an initial state.
- Transition systems and safety: A finite-state transition system is specified by Init(X) for initial states and T(X, X′) for possible transitions.
- Transition systems and safety: A system is P-invariant when every state reachable from an initial state along a path satisfies the safety property P(X).
- Frames: A PDR trace consists of CNF frames, each over-approximating states reachable within a given number of transitions; their clauses are lemmas.
- Frames: PDR seeks a fixed point Fn−1 = Fn, which implies an inductive strengthening and establishes that P is invariant; otherwise it produces a counterexample trace.
- Proof obligations: A proof obligation ⟨s, ℓ⟩ records a state cube and level whose states must be blocked from frames Fi for i ≥ ℓ.
- Blocking: PDR uses SAT queries to block obligations, generalizes successful blocks into clauses, and creates lower-level obligations when a predecessor is found.
- Blocking: The blocking phase maintains a priority queue Q, repeatedly processes obligations, reschedules successful ones at higher levels, and may terminate with Unsafe.
- Propagation: During propagation, clauses that pass an inductiveness query move to the next frame; equality of consecutive frames yields Safe.
4 Portfolio and Lemma Sharing
PDR portfolios exploit runtime variability across independent configurations, while lemma sharing couples engines by exchanging lemmas to reduce redundant work. The paper motivates further optimization of this sharing-based setting.
- Portfolio: Portfolio execution runs multiple sequential PDR instances independently and terminates when any instance returns Safe or Unsafe.
- Portfolio: Portfolio methods are effective because sequential PDR runtimes vary substantially across configurations on the same problem.
- Portfolio: Portfolio approaches are widely used in the Hardware Model Checking Competition, including the 2025 winning rIC3 entry.
- Lemma Sharing: Lemma Sharing runs multiple engines with separate traces and proof-obligation queues while communicating newly derived lemmas to other engines.
- Lemma Sharing: Sharing lemmas is intended to reduce redundant work from related proof obligations and keep engine traces closely aligned.
- Motivation for optimization: The paper introduces an optimization of the propagation phase for the lemma-sharing setting.
5 Preemptive propagation
Preemptive propagation extends lemma sharing so engines communicate both successful and failed propagation results, skipping redundant SAT queries. A controller-worker architecture preserves propagation semantics despite asynchronous traces.
- Motivation: Standard lemma sharing leaves satisfiable propagation queries unshared, forcing every engine to repeat results that are frequent and expensive in practice.This redundancy motivates communicating failed as well as successful propagation outcomes.
- Optimization: Preemptive propagation sends each solved propagation result to other engines, allowing them to skip the corresponding SAT query.The message includes a Boolean success flag; successful propagation also adds the clause to the receiving engine’s next frame.
- Limitation: Asynchronous traces can cause preemptive propagation to suppress a useful propagation when one engine reports failure before another issues its query.The described case sends a false result even though the second engine would have propagated the clause successfully.
- Limitation: Missing propagated lemmas preserves soundness but can increase top-level iterations needed to establish safety.The performance loss arises because later PDR stages may lack lemmas needed to fulfill the safety condition.
- Correction: A controller buffers shared lemmas and orders phase entry so engines receive the necessary earlier trace lemmas before propagation.This ensures each engine obtains at least the lemmas that would result from propagating the first engine’s trace without preemption.
- Load balancing: Different deterministic clause orders distribute propagation work across engines and reduce simultaneous attempts on the same clause.Engines use a hash-based priority ordering, with traversal positions spaced apart on average.
6 ARPOS – Asynchronous Rescheduled Proof Obligation Sharing
ARPOS parallelizes PDR by sharing and rescheduling proof obligations through a controller-managed priority queue. It uses recursive local blocking before global rescheduling so lower-level work can produce lemmas that remove obsolete top-level obligations.
- Motivation: ARPOS addresses a limitation of lemma sharing in which engines block lower-level obligations while another engine searches for a new top-level bad state.Lower-level blocking can produce inductive lemmas that exclude that state or its predecessors if propagated before the top-level search proceeds.
- Motivation: ARPOS prioritizes already discovered proof obligations across levels instead of immediately searching for new top-level obligations.This reallocates available parallel resources toward work already generated by the blocking process.
- Design requirements: ARPOS requires local progress, reduced redundant computation, and non-blocking communication in the distributed implementation.These requirements guide the design of its asynchronous controller-worker coordination.
- Scheduling: The parallel strategy replaces local proof-obligation rescheduling with insertion into a shared priority queue assigned dynamically to available processors.The queue is motivated by viewing recursive blocking as a depth-first traversal whose nodes are proof obligations.
- Architecture: The controller maintains a shared priority queue and worker pool, assigning obligations to idle workers and handling success, unsafe results, and worker availability.Workers receive obligations or top-level search requests and return status messages to the controller.
- Worker behavior: Workers recursively block generated obligations locally before sending them to the controller for rescheduling at a higher level.This preserves the recursive blocking structure while exposing completed obligations to the global queue.
- Integration: Preemptive propagation integrates naturally with ARPOS because both use a controller-worker architecture.The shared architecture supports their combined implementation.
- Comparison: ARPOS combines shared-queue scheduling with immediate reassignment of idle workers, distinguishing it from both PS-PDR and classical lemma sharing.Unlike PS-PDR, an ARPOS worker performs recursive blocking; unlike a purely local scheme, idle workers receive new tasks immediately.
7 Implementation
The implementation uses asynchronous MPI point-to-point communication integrated with the Rust-based rIC3 hardware model checker. Configurable message aggregation and probing allow communication to overlap with computation.
- Framework: Classical lemma sharing and ARPOS with preemptive propagation are implemented using a Rust framework for distributed point-to-point MPI communication.The framework is integrated with rIC3, a recent high-performance PDR engine and 2025 HWMCC winning entry.
- Communication: Non-blocking MPI primitives overlap communication with computation, while message aggregation reduces communication initiation overhead.Processes probe for incoming messages at designated computation points.
- Configuration: Message size and probing frequency are configurable in the asynchronous communication framework.These parameters control how communication is aggregated and when processes check for incoming messages.
8 Experiments
Experiments on the HWMCC 2025 bit-level safety suite compare rIC3 portfolios, Lemma Sharing, and ARPOS under fixed runtime and memory limits. Preemptive propagation substantially improves Lemma Sharing, while ARPOS does not achieve competitive speedups against Lemma Sharing.
- Experimental setup: The evaluation covers 319 instances using rIC3-based sequential, portfolio, Lemma Sharing, and ARPOS strategies under 3600-second and 16GB per-engine limits.Comparisons use the HWMCC 2025 bit-level safety benchmark on a two-node cluster.
- Experimental setup: The over10 subset contains 153 instances where Portfolio exceeded 10 seconds or timed out, while at least one evaluated strategy solved each within the limit.This subset focuses comparisons away from small instances disadvantaged by MPI initialization and communication overhead.
- Preemptive propagation: Both Lemma Sharing and ARPOS substantially outperform Portfolio without preemptive propagation, but preemptive propagation adds almost 2× speedup for Lemma Sharing and none for ARPOS at 16 processes.The first series compares all strategies with 16 processes on one node using cumulative solved-instance curves and speedup relative to Portfolio.
- Scaling to larger process counts: For larger distributed configurations, Lemma Sharing benefits from preemptive propagation at every process count, with speedup rising from 1.16× to 2.23× at 16 processes.The 16-process configuration also solved the largest number of benchmarks in this comparison.
- Scaling to larger process counts: The overall largest speedup is 2.55× for Lemma Sharing on 64 processes with preemptive propagation enabled.ARPOS does not produce speedups competitive with Lemma Sharing, despite performing best on some benchmarks, and the performance gap remains unexplained.
9 Conclusion and Future Work
The paper presents ARPOS as a sharing-based PDR parallelization strategy implemented in rIC3 through asynchronous MPI messaging. It identifies message aggregation and evaluation beyond HWMCC as future directions for understanding scalable parallel PDR.
- Conclusion: ARPOS maintains a global queue of rescheduled proof obligations so parallel resources address them instead of searching for new top-level obligations.The strategy is presented as improving scalability to large processor counts compared with classical Lemma Sharing on hardware model-checking problems.
- Conclusion: ARPOS is implemented on the rIC3 hardware model checker using an MPI-based asynchronous message-passing framework.The implementation supports the paper’s parallelization strategies within the state-of-the-art rIC3 engine.
- Future work: Future work includes studying aggregated lemma and proof-obligation message sizes to reduce communication-initiation overhead.The proposed investigation applies to both Lemma Sharing and ARPOS.
- Future work: Evaluating ARPOS on benchmarks beyond HWMCC could test whether problem type affects the relative performance of different methods.This is identified as an immediate direction for assessing the scope of the reported findings.
Acnknowledgments
The acknowledgments thank Kiril Dichev, Petro Lutsyk, Bill McColl, and Jonas Oberhauser for helpful discussions.
- The authors acknowledge helpful discussions with Kiril Dichev, Petro Lutsyk, Bill McColl, and Jonas Oberhauser.