echeneis

Stopping the world to find world-stoppers

Echeneis is a controlled model-checking tool designed specifically to detect blocking code in concurrent Rust programs. It systematically explores execution paths to verify whether one thread could block another.

Why echeneis?

Many concurrent algorithms expect a specific sequence of operations to complete without interruption. If a thread is preempted at a critical operation, such as right after updating a state flag, it can inadvertently leave the rest of the system completely stalled.

Exhaustive model checkers like loom may face runtime problems on complex systems in practice, limiting there use for exhaustivce checking of these systems somewhat. Echeneis tries to solve this by foxusing only on a small subset of bugs (pairwise blocks) and searchign for them by checking if some thread blocks given another is preempted at some point. This crate also makes no assumption about the memory model, delegating this layer to native atomic implementations.

Focusing on pairwise blocking interactions allows fast and simple checking with informative errors of concurrent models.

Quick Start

Using echeneis::check_pairwise, you can orchestrate an initial state, a preemptible worker thread, and a checking thread to ensure that the checker can always make progress regardless of when the worker is interrupted.

First add echeneis to your dependencies:

[target.'cfg(echeneis)'.dependencies]
echeneis = "0.1"

Next, create a test file and add a test:

  use echeneis::sync::atomic::{AtomicUsize, AtomicBool, Ordering};
  #[test]
  #[should_panic]
  fn blocking_concurrent() {
    echeneis::check_pairwise(
        || (AtomicBool::new(true), AtomicUsize::new(0)),
        |(b, v)| {
            for _ in 0..3 {
                if v.fetch_add(1, Ordering::AcqRel) == 2 {
                    b.store(false, Ordering::Release);
                    // if we get preempted here, it should block
                    b.store(true, Ordering::Release);
                }
            }
        },
        |(b, _)| {
            while ! b.load(Ordering::Acquire) {}
        },
    );
  }

Then, run the test with

RUSTFLAGS="--cfg echeneis" cargo test --test blocking_concurrent

Writing tests

Echeneis intrusively redirects all calls to synchronization primitives in order to check preemption permutations systematically. This means that all tested functionality should use the synchronization primitives exported in this crate.

One way to do so easily is to use an echeneis cfg flag and conditionally use echeneis synchronization primitives for test runs by conditionally exporting them in some central module:

 #[cfg(echeneis)]
 pub(crate) use echeneis::sync::atomic::AtomicUsize;

 #[cfg(not(echeneis))]
 pub(crate) use std::sync::atomic::AtomicUsize;

Then, elsewhere:

 use crate::sync::AtomicUsize;

Limitations

Echeneis currently only supports check_pairwise. In other words, blocks depending on n-way scheduling decisions can currently not be detected. Further, check_pairwise currently does not reistantiate the init state created by init_fn. If the code in preempt or checked mutate the state in a way that changes the execution, blocking code-paths may be missed or falsely detected.

Feature Flags