Logical Time in Weft — Unified Model (Phase 4)
Problem Statement
Phases 1–3 each handle time independently:
- Phase 1: Virtual clock (
AtomicU64nanoseconds). Monotonic starts at 0, everyreadadvances by 1 µs. Realtime = 2000-01-01 + seed-offset + monotonic. - Phase 2: Scheduler token model. One thread runs at a time; which one is a function of seed. Time advances only via yield points.
- Phase 3: Broker ordering key. Network delays are modeled as entries in a
BinaryHeap<(delay, insertion_index)>. “Delay is an ordering key, not wall time” — the broker has no synchronization with the virtual clock or cross-process time base.
Phase 4 unifies these by establishing a single logical timeline that governs:
- When network messages are delivered (Phase 3)
- When file I/O operations complete (Phase 4 new)
- When clock skew applies to each node (Phase 4 new)
- When process crashes and restarts occur (Phase 4 new)
- Virtual clock reads in each process (Phase 1 extension)
Key Insight: Logical Time is Scheduling Order
A logical time T is an entry point into a deterministic event queue. The key realization:
- The broker’s BinaryHeap already implements this: events are ordered by
(delay_key, insertion_order), and the queue is traversed deterministically. - Virtual clock reads are observations of logical time, not a separate clock.
- File I/O delays, network latencies, and clock skew are all scheduled events, drawn from the same seeded PRNG stream as everything else.
The Model
Global Event Queue (Broker-wide)
The broker maintains a BinaryHeap<ScheduledEvent> where ScheduledEvent is:
#![allow(unused)]
fn main() {
pub struct ScheduledEvent {
pub time_key: (u64, u64), // (logical_time_ns, insertion_order)
pub event_type: EventType,
}
pub enum EventType {
NetDeliver { src, dst, seq, payload },
FileIoComplete { node, fd, result },
ClockSkewChange { node, offset_ns },
ProcessCrash { node_id },
ProcessStart { node_id },
FaultActivate { node_id, fault_id }, // e.g., activate partition
}
}
Per-Node Virtual Clock
Each node process has a virtual clock that is a view into the global timeline:
virtual_clock[node_i] = global_base_time + node_clock_offset[node_i]
Where node_clock_offset[node_i] is:
- Initially 0 (or seed-derived to make realtime dates differ)
- Changed by
ClockSkewChangeevents - Visible to the node’s
clock_gettime()calls
Determinism: Per-Timeline Seeding
The source of every time value is a seeded PRNG stream, not a shared pool:
- Network message delays: seeded by
f(seed, src, dst, seq)(Phase 3, unchanged) - File I/O delays: seeded by
f(seed, node_id, fd, op_type, seq_on_fd)— same per-fd sequence determinism as network - Clock skew changes: seeded by
f(seed, node_id, skew_index)— one sequence per node - Process crash timing: seeded by
f(seed, node_id, crash_index)— one sequence per node
Atomicity and Isolation
The broker is single-threaded (Phase 3 current design). Within one broker round-trip:
- Node calls broker with (operation, details)
- Broker looks up timing via seeded fate function
- Broker enqueues the result with absolute
time_key - Broker returns immediately (no waiting for delay)
- Next receiver of that result sees it at the right logical position
Cross-process ordering is OS-scheduled (Phase 3 honest limitation). But once an event is enqueued, its position is deterministic.
Examples
Single-fault: Network latency causes reordering
Seed 42, --net "latency=uniform:1000-5000"
Monotonic timeline (insertion order):
0. Node-0 sends PING to Node-1 (seq=0)
→ fate(42, 0, 1, 0) = delay=3200ns
→ enqueue at time_key=(3200, 0)
1. Node-1 receives nothing; yields
2. Node-0 sends PING to Node-1 (seq=1)
→ fate(42, 0, 1, 1) = delay=1200ns
→ enqueue at time_key=(1200, 1)
3. Next Node-1 recv:
→ dequeue (1200, 1) first → seq=1 arrives before seq=0
→ seq=0 still pending at (3200, 0)
→ reordering!
Multi-fault: Network loss + file sync-lies
Node writes a message to disk (“value=42”), then sends it to the replica.
Scenario:
- latency=fixed:100ns (deterministic delivery timing)
- loss=0.5 (50% drop, seeded)
- fsync-lies: every other fsync returns success but drops recent writes
Execution (seed S):
1. Node-0 write("value=42") → local file (unsynced)
2. Node-0 fsync() → fsync-lies returns success but doesn't actually persist
3. Node-0 send("I have value=42") to Node-1
- fate(S, 0, 1, seq) = {delay: 100ns, drop: no}
- Replica receives "value=42"
4. Node-0 crashes (scheduled event)
5. Node-0 restarts
6. Node-0 read("value=42") → EOF or old value (because fsync lied)
7. Node-0 send("I have <old value>") to Node-1
- Replica sees conflicting updates — bug surface!
Without fsync-lies or without crash: bug never manifests.
Honest Limitations (Phase 4)
- Cross-process ordering remains OS-scheduled. Which process’s syscall reaches the broker first is timing-dependent. But once in the queue, position is deterministic.
- Per-fd I/O delay independence. File descriptor delays are seeded per-fd, so an fd’s delays are reproducible but concurrent writes to different fds have timing that may interleave differently per run (like network, until Phase 2 scheduler is extended to file I/O).
- Crash-and-restart granularity. Crashes are modeled as instantaneous events. Real OS crash recovery (log replay, state consistency) is out of scope — the scenario author must model what remains.
- File-system consistency model is simplified. No true journaling, crash atomicity, or order-of-durability constraints beyond what fsync-lies and ENOSPC model.
Scenario DSL (Phase 4)
Timed fault event sequences are written in a JSON scenario configuration
(the implemented format — see examples/scenarios/ for runnable files):
{
"name": "file-sync-reordering",
"description": "Replica divergence when fsync lies and network reorders",
"seed": 42,
"nodes": [
{"node_id": 0, "program": "./target", "args": ["--role=writer"]},
{"node_id": 1, "program": "./target", "args": ["--role=replica"]}
],
"network": { "latency": "uniform:100-10000", "loss": 0.2 },
"filesystem": {
"0": { "fsync_lies": true, "enospc_after_bytes": null }
},
"time_skew": {},
"events": [
{ "time_ns": 1000000, "action": { "type": "crash", "node_id": 0 } },
{ "time_ns": 2000000, "action": { "type": "start", "node_id": 0 } }
]
}
Validation and Testing (Phase 4)
- Parser property tests: generated scenario JSON (valid and deliberately malformed) never panics; parse always returns
Result<Scenario, ParseError>. - Per-fault-type isolation: each fault type (network loss, fsync-lies, ENOSPC, crash) is tested in isolation with a minimal scenario.
- Multi-fault interaction: at least one scenario demonstrates a bug that manifests only when two or more fault types are active together.
What Changes, What Stays the Same
Changes
- Broker’s
BinaryHeapbecomes the global logical timeline - Virtual clock becomes a per-process view (with optional skew offset)
- New crate:
weft-scenariofor DSL parsing and validation - File I/O hooks in shim for torn write, ENOSPC, fsync-lies
Stays the Same
- Phase 1 determinism guarantees (same seed → same values)
- Phase 2 scheduler token model (extends to file I/O yield points)
- Phase 3 network per-message fate (integrated into global timeline)
- Interception architecture (hooks + engine)