DeterV: Verifying Deterministic Parallel Execution
TL;DR
DeterV is a deterministic parallel runtime which uses Verus to verify its correctness and equivalence to serial execution in the input order and attains a 3:1 proof-to-code ratio and incurs only trivial runtime overhead compared to an unverified baseline.
Abstract
Deterministic execution is a critical component for replicated systems, where each replica is required to advance its state deterministically in an agreed-upon order even in the presence of concurrent execution. Despite the extensive efforts on the design space, the correctness of deterministic parallel execution engines is not yet backed by provable guarantees. We close this gap with DeterV, a deterministic parallel runtime which uses Verus to verify its correctness and equivalence to serial execution in the input order. DeterV establishes determinism via per-object local reasoning, an effect-boundary contract which limits the determinism enforcement to a single point, and a series of refinements that compose these local guarantees globally. DeterV attains a 3:1 proof-to-code ratio and incurs only trivial runtime overhead compared to an unverified baseline. Despite being a single system implementation, we discuss how DeterV's ideas can generalize to other usecases and designs.