Skip to main content

Logical clocks and causal evidence

This required 20–30-hour package supplies guided Lab 2's executable core: lessons and predictions 5–7, implementation and experiments 9–15, assessment and repair 6–8. Reuse its event graph and timestamps rather than repeat the lab. Original failure-detector, Raft and retry-safe API work remains required. Estimates await learner pilots; see the reconciled semester workload.

Prerequisite bridge​

Review directed graphs, reachability, partial orders and componentwise comparison. From Module 3, recall why positions from unrelated histories cannot be compared as global progress. From Module 4, distinguish event ordering from duplicate-effect suppression. Neither a timestamp nor a total sort makes a business operation atomic.

Sequence and runnable work​

  1. Causality from event edges.
  2. Timestamp snapshots and comparison.
  3. Evidence limits and distributed guarantees.
  4. Prediction practice, then DS1–DS6 gates.

Download logical-clock-contracts.zip. Python 3 standard library only. Implement starter.py from the README and run python3 -B check.py starter. Use python3 -B check.py reference for calibration after attempting independently.

The model has fixed process membership, unique event/message IDs, one receive per send, no restarts and complete tracked local/message edges. Messages can remain undelivered. A topological input list specifies local process order but does not create edges between unrelated processes. Each result is an immutable Lamport/vector snapshot. Vector comparison has four outcomes: before, after, concurrent and equal.

Verification and evidence​

The harness constructs ancestry independently using graph edges. It checks 100 seeded 20-event histories and a worked trace: 40,036 ordered event pairs. It verifies vector-order equivalence to graph reachability and the forward Lamport implication, plus a scalar-order/concurrency counterexample. Five faulty implementations are rejected. These finite checks are not a universal proof.

Keep event graph, hand predictions, actual timestamps, a minimal counterexample and three independently designed traces. Include an undelivered message and an equivalent reordering of independent events. Complete original failure detection, consensus and retry work separately; this lab has no networking, physical clock, election or failure detector.