Prove Lamport Clock Causality and Its Limitation - The Timekeeper

                      TASK
                    

Implementation

Lamport clocks guarantee: if event A happened-before event B, then L(A) < L(B). But the converse is NOT true - L(A) < L(B) does NOT mean A caused B. Events may be concurrent (neither caused the other).

Your task is to build a system that:

Records events with Lamport timestamps
Tracks the actual causal chain (send/receive links)
Compares what Lamport timestamps tell us vs actual causality

Implement:

Request:  {"type": "record_event", "msg_id": 1, "event_id": "e1", "caused_by": null}
Response: {"type": "record_event_ok", "in_reply_to": 1, "clock": 1}

Request:  {"type": "record_event", "msg_id": 2, "event_id": "e2", "caused_by": "e1"}
Response: {"type": "record_event_ok", "in_reply_to": 2, "clock": 2}

Request:  {"type": "check_causality", "msg_id": 3, "event_a": "e1", "event_b": "e2"}
Response: {"type": "check_causality_ok", "in_reply_to": 3,
           "lamport_says": "a_before_b", "actual": "a_before_b", "correct": true}

Sample Test Cases

Record two causal eventsTimeout: 5000ms

Input

{"src":"c0","dest":"n1","body":{"type":"init","msg_id":1,"node_id":"n1","node_ids":["n1"]}}
{"src":"c1","dest":"n1","body":{"type":"record_event","msg_id":2,"event_id":"e1","caused_by":null}}
{"src":"c1","dest":"n1","body":{"type":"record_event","msg_id":3,"event_id":"e2","caused_by":"e1"}}

Expected Output

{"src": "n1", "dest": "c0", "body": {"type": "init_ok", "in_reply_to": 1, "msg_id": 0}}
{"src": "n1", "dest": "c1", "body": {"type": "record_event_ok", "in_reply_to": 2, "clock": 1, "msg_id": 1}}
{"src": "n1", "dest": "c1", "body": {"type": "record_event_ok", "in_reply_to": 3, "clock": 2, "msg_id": 2}}

Check causality of causal pairTimeout: 5000ms

Input

{"src":"c0","dest":"n1","body":{"type":"init","msg_id":1,"node_id":"n1","node_ids":["n1"]}}
{"src":"c1","dest":"n1","body":{"type":"record_event","msg_id":2,"event_id":"e1","caused_by":null}}
{"src":"c1","dest":"n1","body":{"type":"record_event","msg_id":3,"event_id":"e2","caused_by":"e1"}}
{"src":"c1","dest":"n1","body":{"type":"check_causality","msg_id":4,"event_a":"e1","event_b":"e2"}}

Expected Output

{"src": "n1", "dest": "c0", "body": {"type": "init_ok", "in_reply_to": 1, "msg_id": 0}}
{"src": "n1", "dest": "c1", "body": {"type": "record_event_ok", "in_reply_to": 2, "clock": 1, "msg_id": 1}}
{"src": "n1", "dest": "c1", "body": {"type": "record_event_ok", "in_reply_to": 3, "clock": 2, "msg_id": 2}}
{"src": "n1", "dest": "c1", "body": {"type": "check_causality_ok", "in_reply_to": 4, "lamport_says": "a_before_b", "actual": "a_before_b", "correct": true, "msg_id": 3}}

Hints

Hint 1▾

If A happened-before B, then L(A) < L(B) - this is guaranteed

Hint 2▾

The converse is NOT true: L(A) < L(B) does NOT imply A happened-before B

Hint 3▾

Construct a counterexample with two independent nodes that never communicate

Hint 4▾

Node n1 ticks once (L=1), node n2 ticks twice (L=2) - L(n1) < L(n2) but they are concurrent

Hint 5▾

Report whether two events are causal or concurrent based on Lamport timestamps alone

Resources

Happened-Before Relation

Wikipedia explanation of the happened-before partial order

                      OVERVIEW
                    

Theoretical Hub

Concept overview coming soon

Key Concepts

happened-beforecausalityconcurrent eventsLamport limitation

main.py

python