Diagnose a consistency violation in a toy replicated log

Step through five operations across three clients (c0, c1, c2), each carrying its own vector clock — built exactly the way time-clocks-and-ordering built one: bump your own component, and on a "read-from" a write, take the componentwise max with that write's vector. Watch the three components grow unevenly, client by client.

This trace reuses three ideas directly:

1. From consistency-models: linearizability

   A history is linearizable iff some total order respects both real time and program semantics — isTraceLinearizable runs the exact same check this capstone's TRACE.

2. From time-clocks-and-ordering: vector clocks

   Each op's vc is a 3-component vector, one slot per client, built with the same rule: your own component increments; a "read-from" link takes the componentwise max with the write's vector, the same way a message receive does.

3. From causality-and-happened-before: happened-before vs. concurrent

   $a \to b \iff a \le b$ componentwise, $a \neq b$; otherwise, if neither dominates, $a$ and $b$ are concurrent. Both checks are imported and reused directly here, unchanged.

• real-time prior write — the write with the latest end-time that finished before an op started.
• causal prior write — the most recent write an op's vector clock actually dominates.

The insight this capstone is built to demonstrate: these two "prior writes" don't have to be the same write — and when they aren't, you get a linearizability violation that a causal-consistency checker would wave right through.

Pick any operation and compare it against op3 (the write of x=2) using the exact happenedBefore / isConcurrent functions from causality-and-happened-before. Notice which operations are concurrent with op3 — meaning no message chain ever told them about it.

1. Confirm the violation exists

   isTraceLinearizable(TRACE) is false — and removing exactly one operation restores it, so there's a single culprit.

2. Find the culprit

   diagnoseViolation(TRACE) names op5: a read by client c1, returning x=1, starting at t=10.

3. What real time demanded

   findRealTimePriorWrite(TRACE, op5) returns op3 — the write of x=2, finished at t=7, well before op5 starts at t=10. Linearizability's real-time rule says op5 must reflect it.

4. What op5 actually knew about

   Building each op's vector clock (own component bumps, read-from takes the componentwise max):

   • op1 (c0 write): bumps its own slot from $[0,0,0]$ → $[1,0,0]$
   • op2 (c1 read-from op1): bumps its own slot to $[0,1,0]$, merges with op1's $[1,0,0]$ → $[1,1,0]$
   • op3 (c0 write): bumps its own slot from $[1,0,0]$ (c0's state after op1) → $[2,0,0]$
   • op5 (c1 read-from op1 only): bumps its own slot from $[1,1,0]$ (c1's state after op2) → $[1,2,0]$, merges with op1's $[1,0,0]$ → still $[1,2,0]$

   So op5's vector clock is $[1,2,0]$ and op3's is $[2,0,0]$. Neither dominates the other: isViolationMerelyConcurrent(op5, op3) is true. op5 only ever read-from op1; no chain of messages ever told client c1 about op3's write. findCausallyPriorWrite(TRACE, op5) accordingly returns op1, not op3.

5. The gap

   A causal-consistency checker only asks "did you violate something you actually knew about?" — and by that standard, op5 did nothing wrong, since it was never causally informed of op3. Linearizability asks a stricter question: "did you violate something that had already happened in real time?" — and by that standard, op5 is the violation. A linearizability violation doesn't have to be a causality violation too.