DEOS Determinism Model
Version 1.0, December 2025
Two claims, not one
People use the word "determinism" loosely. DEOS actually makes two separate claims that are easy to conflate, and the difference matters when you're reasoning about what the system does and does not guarantee.
The first is replay determinism. Given the same event log, DEOS replays execution to a bit-identical final state. This is the weaker of the two claims. The event log captures every source of nondeterminism the kernel can see: syscall results, interrupt timing (TSC values), RDTSC and RDRAND values, and network packet contents. During replay, those values are injected from the log rather than recomputed from the environment. So the kernel produces the same sequence of operations, the same scheduling decisions, and the same final state. Verification is a hash chain check.
The second is fresh-run determinism. Given the same kernel, same initial state, and same inputs, two separate runs produce identical event logs and identical final state. This is the harder claim. It demands not just that we can play back a recorded log, but that two independent executions of the same program would produce the same log in the first place. That requires deterministic scheduling, deterministic memory allocation, and determinism all the way down. Verification is running twice and comparing log hashes.
Fresh-run determinism implies replay determinism. The reverse is not true. If you can reproduce a run from a recorded log, that does not by itself show you could have produced the same log on a fresh run, because the log already encodes the choices the environment made.
DEOS claims both.
Scheduling versus atomics
A reasonable question came back during review: if atomics are logged, why do you need deterministic scheduling at all? And if scheduling is deterministic, why bother logging atomics?
The answer is that scheduling is primary and atomics are forensic.
Deterministic scheduling is sufficient for replay correctness. DEOS schedules from a single global ready queue rather than per-CPU queues that could diverge, preempts at fixed tick intervals, breaks ties by thread ID, and never adjusts priorities dynamically. Under these rules, thread interleavings are deterministic, lock acquisition order is deterministic, and atomic operation sequences are deterministic. The replay does not need an atomics log to be correct; the scheduling alone is enough.
The atomics log exists for visibility, not for replay. When something goes wrong, or when an auditor wants to see what actually happened, the log shows the contention, the lock order, the CAS retry sequence. None of that is needed to reproduce execution. All of it is needed to understand it.
| Purpose | Atomics log needed? |
|---|---|
| Replay correctness | No, scheduling handles it |
| Debugging race conditions | Yes, shows what happened |
| Root cause analysis | Yes, shows lock contention |
| Audit trail | Yes, proves execution order |
The clarified one-line claim is: DEOS achieves replay determinism through deterministic scheduling. Atomics are logged for forensic auditability, not for replay injection.
How the scheduler stays deterministic
Four rules cover it.
One global ready queue. All CPUs pull from the same queue in FIFO order. There are no per-CPU queues that could fall out of sync.
static READY_QUEUE: Mutex<VecDeque<ThreadId>> = ...;
fn schedule_next() -> Option<ThreadId> {
READY_QUEUE.lock().pop_front()
}
Fixed-tick preemption. Each thread runs for the same number of ticks before being preempted. No adaptive quanta, no boost for interactive workloads, no per-task budget tracking. Same tick count, every time.
const TICKS_PER_PREEMPT: u64 = 10; // ~10ms quantum
fn timer_interrupt() {
if current_thread.ticks >= TICKS_PER_PREEMPT {
yield_current();
}
}
Deterministic tie-breaking. When two threads are equally eligible, pick the one with the lowest thread ID. Always. The actual ordering criterion does not matter; what matters is that it is fixed and reproducible.
fn choose_thread(candidates: &[ThreadId]) -> ThreadId {
*candidates.iter().min().unwrap()
}
No dynamic priority. No priority inheritance, no priority boost, no adaptive scheduling. Simple FIFO with fixed quantum. The complexity those features buy in throughput costs you reproducibility, and DEOS does not make that trade.
What the atomics log actually records
pub struct AtomicEvent {
pub thread_id: u32,
pub address: u64,
pub operation: AtomicOp, // Load, Store, CAS, FetchAdd, etc.
pub old_value: u64,
pub new_value: u64,
pub timestamp: u64,
}
Logged on every compare_exchange, fetch_add, fetch_sub, and swap. Optionally on loads and stores with SeqCst ordering, controlled by a build flag because the volume can be large.
During replay, these values are not injected. Scheduling is already deterministic, so the same thread interleaving produces the same atomic results without help. Injection would be redundant and would add a class of bug where the injected value disagrees with what the deterministic scheduler would have computed.
Training versus replay
Two different scenarios for AI workloads, both covered by the same model.
Training determinism (fresh-run):
Run 1: random_seed=42 -> train -> weights_hash = 0xABC123
Run 2: random_seed=42 -> train -> weights_hash = 0xABC123
^ must match
This works because the RNG is seeded deterministically, scheduling is deterministic, floating-point uses a fixed reduction discipline, and all I/O is deterministic.
Replay determinism (from log):
Original: execute -> event_log -> weights_hash = 0xABC123
Replay: inject(log) -> weights_hash = 0xABC123
^ must match
This works because the event log captures everything non-deterministic, replay injects the logged values, and the computation itself is pure.
Implementation status
The pieces that have to be true for the model to hold:
- Single global ready queue
- Fixed tick quantum
- Deterministic tie-breaking
- No dynamic priority
- Atomics logging for forensics
- TSC and RDRAND trapping and logging
- Syscall result logging
- Event log hash chain
How to verify yourself
Run the same workload twice. Compare the event log hashes. They should match.
./test.sh 30
cp /tmp/deos-events.log /tmp/run1.log
./test.sh 30
cp /tmp/deos-events.log /tmp/run2.log
blake3 /tmp/run1.log /tmp/run2.log
If they do not match, the model is wrong or the implementation has a bug. Both are interesting cases to learn about.
Related papers
- DEOS Floating-Point Determinism Specification:
/whitepapers/fp-determinism - Cryptographic Verification of Deterministic Replay in Multi-Core Operating Systems:
/whitepapers/replay-proof - DEOS Phase Kernel-4: Scientific Proof of Deterministic Replay:
/whitepapers/scientific-proof