Lockstep.Checker.Causal (Lockstep v0.1.0)

Copy Markdown View Source

Per-process causal consistency check for register-shaped models.

A history is causally consistent here iff every process's projection — the subsequence of events on that process plus the writes whose values that process actually observed — is linearizable on its own. Different processes may have different perceived orders over concurrent writes; that's the whole point of weakening from sequential consistency.

This isn't the strongest possible causal model. Pure causal+ consistency (Mahajan et al.) also enforces "writes-follow-reads" across process boundaries, which requires graph-based analysis beyond per-process projection. But the simpler per-process formulation catches the most common violations:

  • Monotonic reads: a process never observes an OLDER value after observing a NEWER one (caught: the projection's sequence of reads must be model-consistent).
  • Read-your-writes: a process always sees its own writes after it issues them (caught: the writes are part of the projection).
  • Causal staleness: a read sees a value such that no consistent history of writes leading to it exists.

Stronger than eventual consistency, weaker than sequential consistency. Useful for systems that don't claim global ordering but DO promise per-process consistency.

Algorithm

For each process P:

  1. Take the subsequence of events where event.process == P. This includes P's invokes and completions.
  2. Take all WRITES (any process) whose value appears in P's reads, plus P's own writes. These are the writes P "saw".
  3. Run Lockstep.Checker.SequentialConsistency.check/2 on the combined projection.

We use SequentialConsistency not Linearizable because causal doesn't enforce real-time across processes — it only requires each process's program order be preserved within its own perceived history. Linearizable would over-reject by demanding the cross-process real-time order.

If every process's projection is SC-consistent, the history is causally consistent.

Returns

  • {:ok, %{per_process_orders: %{pid() => [Op.t()]}}}
  • {:error, %{process: pid(), violation: ...}} — the first process whose projection isn't SC-consistent, plus the checker's error info.

Summary

Functions

check(events, model)

Check per-process causal consistency. See module doc.

Functions

check(events, model)

@spec check([Lockstep.History.Event.t()], module()) ::
  {:ok, %{per_process_orders: %{required(pid()) => list()}}}
  | {:error, %{process: pid(), violation: any()}}

Check per-process causal consistency. See module doc.