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:
- Take the subsequence of
eventswhereevent.process == P. This includes P's invokes and completions. - Take all WRITES (any process) whose value appears in P's reads, plus P's own writes. These are the writes P "saw".
- Run
Lockstep.Checker.SequentialConsistency.check/2on 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 per-process causal consistency. See module doc.