dpor

A vibe-coded C++20 DPOR model-checking library inspired by Must.

There are some initial examples of use in the examples/ folder. See docs/api.md for a public API summary and docs/architecture.md for the high-level design.

For a more realistic example, see this integration with stellar-core: https://github.com/nano-o/stellar-core/tree/skip-ledgers-p25-dpor-2

Current scope

• Supported communication models are Async and FifoP2P.
• The set of threads is fixed at program construction time — there is no dynamic thread creation during exploration.
• Supports blocking and non-blocking receives. Non-blocking receives may observe bottom (⊥), which is useful for timeout-style modeling such as the 2PC example.
• Event kinds are send, receive, nondeterministic choice, block, and error. block is an internal DPOR event; user thread functions should not emit it.
• Receive compatibility is predicate-based, with helpers for both arbitrary matchers and finite accepted-value sets.

Public API

• Main exploration entry points: dpor::algo::verify() and experimental dpor::algo::verify_parallel().
• Programs are modeled as dpor::algo::ProgramT<ValueT> collections of deterministic thread functions.
• Published terminal executions are exposed to observers as dpor::algo::TerminalExecutionT<ValueT>, which carries an ExplorationGraphT<ValueT> plus a terminal kind (Full, Error, or DepthLimit).
• Manual graph validation is available through dpor::model::AsyncConsistencyCheckerT, FifoP2PConsistencyCheckerT, and ConsistencyCheckerT.
• The user-facing API is summarized in docs/api.md.

DPOR exploration parameters

Both exploration entry points use the same base configuration:

VerifyResult verify(const DporConfigT<ValueT>& config);
VerifyResult verify_parallel(const DporConfigT<ValueT>& config,
                             ParallelVerifyOptions options = {});

Shared DporConfigT<ValueT> parameters:

• program: the modeled program. This is required.
• max_depth{1000}: maximum explored DPOR tree depth. When DPOR reaches dpor_tree_depth >= max_depth, it publishes a DepthLimit terminal execution and does not explore that branch further. This bounds logical search-tree depth, not current graph size or implementation stack depth.
• communication_model{Async}: communication semantics for consistency checking and revisit generation. Supported values are Async and FifoP2P.
• on_terminal_execution{}: optional callback invoked for each published terminal execution (Full, Error, or DepthLimit). The callback may return TerminalExecutionAction::Continue or Stop; void callbacks are treated as Continue.
• on_progress{}: optional progress callback that receives ProgressSnapshots. If this callback is not set, DPOR does not do progress-related time checks or progress scheduling.
• progress_report_interval{1s}: throttles live on_progress callbacks. > 0 means at most one live snapshot per interval. 0 means report at every internal progress checkpoint, which can be expensive in parallel mode. In parallel mode, this controls callback frequency, while progress_counter_flush_interval controls how fresh the live execution counts are when a snapshot is emitted, and progress_poll_interval_steps controls how often workers even check whether a throttled report is due. A progress checkpoint currently happens when the explorer enters a DPOR state/frame, so it is roughly per explored execution prefix/state, not per terminal execution found.

Parallel exploration adds ParallelVerifyOptions:

• max_workers{0}: worker-thread budget. 0 means use std::thread::hardware_concurrency(), falling back to 1 if the platform does not report a value.
• max_queued_tasks{0}: maximum number of queued spawned tasks. 0 derives a small default queue budget of max_workers * 2.
• spawn_depth_cutoff{0}: DPOR tree-depth gate for task spawning. 0 means no cutoff. Otherwise, a branch is only considered for remote execution when child_dpor_tree_depth <= spawn_depth_cutoff.
• min_fanout{2}: spawn threshold for branch fanout. If the current choice point has fewer than min_fanout alternatives, DPOR keeps the work local.
• sync_steps{512}: stop-polling interval. 0 enables the strict mode, where terminal publication serializes stop checks more aggressively. > 0 is a relaxed mode where each worker refreshes the shared stop flag only every sync_steps internal stop polls. This reduces synchronization overhead, but workers may publish additional terminal executions after a callback has requested Stop.
• progress_counter_flush_interval{1024}: progress-counter batching threshold. Workers keep terminal counters locally and flush them into shared progress counters after this many local terminal publications. 0 uses the default (1024), 1 gives exact live progress counts, and larger values reduce overhead at the cost of staler live progress snapshots.
• progress_poll_interval_steps{64}: progress-poll batching threshold for interval-throttled progress reporting in parallel mode. 0 and 1 both mean poll at every progress checkpoint; larger values reduce hot-path clock checks and report-claim traffic at the cost of coarser callback timing.

For long-running runs, a practical rule of thumb is:

• leave on_progress unset if you want no progress overhead at all
• use a large progress_report_interval together with larger progress_poll_interval_steps and progress_counter_flush_interval values if you only want occasional updates

For example, minute-scale progress reporting can use values like progress_report_interval = 60000ms, progress_poll_interval_steps = 4096, and progress_counter_flush_interval = 65536. Thirty-minute reporting can push those batching values much higher. The benchmark CLI examples in benchmarks/README.md show concrete command lines.

Result reporting:

• VerifyResult.kind is AllExplored or Stopped.
• VerifyResult also reports aggregate terminal counts via executions_explored, full_executions_explored, error_executions_explored, and depth_limit_executions_explored.
• Parallel callback order is unspecified across workers. Final VerifyResult counts are exact; live ProgressSnapshot counts may lag local worker state when progress_counter_flush_interval > 1.

Build

cmake --preset debug
cmake --build --preset debug
ctest --preset debug

CTest vs Catch filtering:

• ctest -R ... matches CTest test names, not Catch tags.
• Catch-discovered tests are prefixed with their executable name, so ctest --preset debug -R dpor_dpor_test runs the tests discovered from dpor_dpor_test, and ctest --preset debug -R dpor_two_phase_commit_timeout_test runs the 2PC example tests.
• Catch tag expressions such as [paper] or [two_phase_commit] only work on the test binaries themselves, for example ./build/debug/examples/two_phase_commit_timeout/dpor_two_phase_commit_timeout_test "[two_phase_commit]".

Tests are written with Catch2 (v3). CMake uses a system Catch2 package if available. Paper-derived examples in current scope are in tests/dpor_test.cpp and tagged [paper]. tests/dpor_test.cpp and tests/dpor_stress_test.cpp also cross-check DPOR against an independent exhaustive async oracle in tests/support/oracle.hpp. When max_depth truncates exploration, DPOR publishes depth-limit terminal executions and counts them in VerifyResult::depth_limit_executions_explored. max_depth is a DPOR tree-depth limit rather than a graph-size limit. The current exploration core is iterative, so deep explorations no longer grow the process stack with search depth.

If Catch2 is not installed and your environment has internet access, enable fetching:

cmake --preset debug-fetch-catch2
cmake --build --preset debug-fetch-catch2
ctest --preset debug-fetch-catch2

Static analysis

The project includes configuration for three integrated static-analysis tools, all off by default: clang-tidy, cppcheck, and IWYU. The lint preset enables clang-tidy and cppcheck with enforcing settings (WarningsAsErrors: '*', --error-exitcode=1):

cmake --preset lint
cmake --build --preset lint

The lint preset is self-contained (fetches Catch2 automatically). clang-tidy requires version 16+ for C++20 structured binding capture support; older versions are detected at configure time and skipped with a warning. For the header-only library itself, these checks run through the internal dpor_header_check target, which compiles a translation unit that includes the public headers.

Individual tools can be enabled on any preset:

cmake --preset debug -DDPOR_ENABLE_CLANG_TIDY=ON
cmake --preset debug -DDPOR_ENABLE_CPPCHECK=ON
cmake --preset debug -DDPOR_ENABLE_IWYU=ON

A clang-format check script is also provided. By default it checks only files changed relative to main:

scripts/run_clang_format.sh          # check changed files
scripts/run_clang_format.sh --fix    # fix changed files
scripts/run_clang_format.sh --all    # check all project files

Editor setup (clangd)

All presets export compile_commands.json. Symlink it to the project root so clangd can find it:

ln -sf build/debug/compile_commands.json .

Install

cmake --preset release
cmake --build --preset release
cmake --install build/release --prefix /tmp/dpor-install

Consume from another CMake project

find_package(dpor CONFIG REQUIRED)
target_link_libraries(my_target PRIVATE dpor::dpor)

If installed to a non-default prefix, add it to CMAKE_PREFIX_PATH.

Performance: lazy PorfCache with vector clocks

ExplorationGraphT uses a lazy, shared vector-clock cache (PorfCache) to accelerate hot-path reachability and warm-cache cycle queries:

Operation	Without cache	With cache
porf_contains(from, to)	O(N+E) per call	O(1) amortized
has_causal_cycle()	O(N+E) per call	O(1) amortized

The cache is built on demand via Kahn's topological sort and stores a per-event vector clock (one entry per thread). Subsequent porf_contains calls compare a single clock entry. Cycle detection is a byproduct of the topological sort (incomplete sort = cycle). The consistency checker can also use the cheaper has_causal_cycle_without_cache() path when it only needs a cycle answer and the cache is still cold.

Key properties:

• Lazy: vector clocks are only built when porf_contains() or the cache-backed has_causal_cycle() path needs them.
• Shared across copies: the cache is held via std::shared_ptr, so graph copies (from with_rf, with_nd_value, etc.) share the parent's cache until they mutate.
• Auto-invalidated: any call to add_event or set_reads_from resets the cache to null, triggering a rebuild on the next query.
• Cycle-safe for DPOR: porf_contains() throws on cyclic graphs. The DPOR engine only calls it on consistent graphs, and consistency checking prunes causal cycles before those queries.

Layout

• include/dpor/model: core model types (events, relations, execution/exploration graphs)
• include/dpor/algo: DPOR engine and program representation
• src: internal build helpers only (for example, the header-check translation unit)
• tests: unit/integration tests with CTest
• examples: two_phase_commit_timeout/
• cmake: packaging and build helper modules
• docs: API and architecture notes