Discrete-event network simulation

Exact and fast.Not a trade.

Days runs on one CPU thread, a multicore pool, Apple Metal, or NVIDIA CUDA, and every backend produces the complete state of a serial run, byte for byte. The parallel backends earn their speed under a safe horizon proved in Lean.

Get started GitHub

record=days_result

fattree_k4 · tcp cubic · smoke

Result fingerprint per backend for configs/benchmarks/tcp/fattree_k4_tcp_cubic_f16_smoke.toml
Engine	result_bytes	result_fnv1a64
ScalarApple M1 Max	101690	d7de73ee33579682
CPUApple M1 Max	101690	d7de73ee33579682
MetalApple M5 Max	101690	d7de73ee33579682
CUDANVIDIA GB10	101690	d7de73ee33579682

› Raw lines

days --engine scalar · Apple M1 Max

record=days_result engine=scalar lowering_ns=3788125 run_ns=2520250 result_bytes=101690 result_fnv1a64=d7de73ee33579682 pending_events=0 resident_packets=0 sourced_packets=512 departed_packets=2816 received_packets=256 dropped_packets=0

days --engine cpu --workers 2 --repetitions 1 · Apple M1 Max

record=days_result engine=cpu lowering_ns=627625 run_ns=1520375 result_bytes=101690 result_fnv1a64=d7de73ee33579682 pending_events=0 resident_packets=0 sourced_packets=512 departed_packets=2816 received_packets=256 dropped_packets=0

days --engine metal · Apple M5 Max

record=days_result engine=metal lowering_ns=2337667 run_ns=37172584 result_bytes=101690 result_fnv1a64=d7de73ee33579682 pending_events=0 resident_packets=0 sourced_packets=512 departed_packets=2816 received_packets=256 dropped_packets=0

days --engine cuda · NVIDIA GB10

record=days_result engine=cuda lowering_ns=2407006 run_ns=13609552 result_bytes=101690 result_fnv1a64=d7de73ee33579682 pending_events=0 resident_packets=0 sourced_packets=512 departed_packets=2816 received_packets=256 dropped_packets=0

4 captured runs, one fingerprint: d7de73ee33579682

Every backend ends the same scenario with the same fingerprint. These are real runs of the quick-start fixture: Scalar and CPU on an Apple M1 Max, Metal on an Apple M5 Max, CUDA on an NVIDIA GB10.

Up to1,279×

faster than sequential ns-3. UDP, CUDA backend, native clocks, RTX 4090 host

Up to81×

faster than Unison at 24 threads. Same experiment and clocks

3,918×

faster than GeDES on TCP run to full completion. Native clocks, same RTX 4090

0.563 s vs 0.565 s

Days vs GeDES in the densest TCP phase: statistically even on GeDES's own clock

4 backends

Scalar, CPU, Metal, CUDA: one byte-identical complete state

5 theorems

about the scheduling model, proved in Lean on standard axioms only

01Exact

One answer, to the byte.

Every event in Days carries a canonical key: time in integer nanoseconds, then a phase, then the sending process and its sequence number. The key orders every pair of events, simultaneous ones included. The reference result is what you get by always executing the pending event with the least key.

Every backend must produce that result exactly. That means the complete final state, not a set of summary statistics. It must hold at any worker count and any assignment of processes to workers. No floating point appears anywhere in the semantics. Fractional quantities, such as Weighted Fair Queueing finish tags, are computed as exact rationals. Each run ends with an FNV-1a-64 fingerprint of the complete state. Equal fingerprints mean byte-identical results.

On one long open-loop run, six independently configured runs across all four backends and two CUDA architectures returned the same 70,900,544-byte state. That run covered 132,988,928 packets and 2.53 billion transitions.

Why it matters

Exactness makes approximation measurable. We aligned Days and GeDES on identical scenarios, with the same sources, routes, and queue capacities, and compared the results. GeDES reports 3.7× the acknowledgment losses and 9.5× the retransmission timeouts, and its completion instant is 11× removed from the exact account of the same workload. Because everything else was equalized, these gaps come from batching events into fixed slots.

Other simulators also depart from their references. Unison departs from sequential ns-3's trajectory even when it runs single-threaded. In drop-free tests, legacy Days in multi-threaded mode returns different packet counts from run to run.

With Days, a misbehaving flow at hour three reappears at hour three on any backend. Bisecting a regression compares two states that are either equal or not. Continuous integration pins the complete final state of every test scenario, so any one-byte change in behavior fails visibly.

GeDES ÷ exact account · aligned TCP workload

GeDES factor
Exact account (1×)

GeDES against the exact account, same TCP workload, aligned configuration. All drops: 721 vs 549 (1.31×). ACK losses: 259 vs 70 (3.7×). Retransmission timeouts: 19 vs 2 (9.5×). Completion instant: 11.0 s vs 1.0 s simulated (11×).

› Data table

Metric	Days (exact)	GeDES	GeDES ÷ Days	Unit
All drops	549	721	1.313297	count
ACK losses	70	259	3.7	count
Retransmission timeouts	2	19	9.5	count
Completion instant	1,000,362,708	11,000,362,024	10.996374	simulated ns

02Fast

A horizon that moves with the traffic.

Parallelism comes from lookahead. No packet can cross a link faster than the smallest packet's serialization plus propagation delay. The validator certifies that bound for every channel before the run starts. Each round, Days computes a safe horizon:

No event a process has not yet seen can arrive before H. A round then takes three steps:

Safe horizon

H equals the minimum of S and the minimum over i of N sub i plus L

Nᵢ is process i's earliest pending event, L is the smallest certified channel bound, and S is the stop time.

01
Drain. Every process executes its events below H in key order, in parallel. Messages for other processes go to a private outbox.
02
Exchange. One deterministic exchange delivers every outbox, merged in key order.
03
Advance. The next horizon is computed from what is now pending.

Fixed 1,000 ns slots vs adaptive safe horizon · L = 1,000 ns · time in ns

slot 13 of 13 · [12,000, 13,000) ns · 1 event

round 8 of 8 · H = min(13,000, 12,000 + 1,000) = 13,000 ns · advance 5,996 ns

Top: fixed slots run every stage on every slot, busy or idle, and an ACK waits for the next boundary. Bottom: each adaptive round ends where lookahead says it must, and an idle stretch is one round.

The contrast with a fixed slot. GeDES advances simulated time in fixed 1,000 ns slots. An acknowledgment that arrives 4 ns into a slot cannot influence anything until the next slot boundary. Days, instead, ends the round 4 ns in and honors the causal chain exactly. The cost is visible as more rounds, and the result is unchanged. When the network is idle, the horizon crosses the dead time in a single round, while a slot pipeline runs its full kernel sequence on every slot.

In short, a slot engine pays for each slot of simulated time, and Days pays for each round and each event of actual work.

What each engine pays for · runtime vs span, and horizon advance per round

Days (CUDA)
GeDES
F-HET (tiered delays)
F-BURST (bursty coflows)

Left: what each engine pays for simulated time on the TCP experiment. GeDES's runtime grows in proportion to span, from 0.565 s at its active frontier to 2,252.5 s at full completion. Days levels off at 0.575 s once the fabric is idle. Right: how far each round advances. In the tiered-delay scenario, 229 rounds cover 893 slots' worth of time. In the bursty scenario, the 462 idle slots between bursts cost three rounds.

› Data table

Series	Framing	Simulated span (ms)	Runtime (s)
Days CUDA	active	0.640628	0.56314
Days CUDA	full configured horizon	3,000	0.574902
GeDES	active	1.082	0.565158
GeDES	full configured horizon	3,000	2,252.5

03Proved

The parallelism is licensed by proof.

The theorems are about a model of the executor defined in Lean: a transition system whose moves are the executor's moves. Every definition in the model is annotated with the executor source location it formalizes. Together, the five theorems say that every execution the parallel machinery may perform ends in the same complete state as canonical serial execution.

17,247

lines of Lean

1,179

declarations across 31 modules, checked by an audit driver

standard axioms, and nothing more: no placeholders, no native_decide

01
Remote lower bound. The horizon rule the executor ships is safe: no unseen event can arrive below it.
02
Round serializability. Running one round in parallel gives exactly the state that running its events one at a time, in canonical order, would give.
03
Run composition. A whole run of such rounds ends in the serial result at the stop time. It does not prove that the run terminates.
04
Decision-point scope. The one rule queue disciplines must follow: choose a packet only when service actually starts, and never change, drop, or duplicate a packet in service. Four executable countermodels show that each clause is necessary.
05
Intra-round reordering license. Within a round, events need to keep their order only on the same packet's causal chain or at the same process's queues. Any other order gives the same result, and this is the freedom a GPU needs.

From the model to the backends

A proof is about the model, not about a compiled binary. Testing closes that gap, and a backend passes only when its bytes match. The CPU pool and every device backend must reproduce the serial oracle's complete state in four-backend agreement tests. The GPU kernels must report no races under the vendor's race detector on both kinds of GPU. Byte-identity is a precondition of every timed configuration we report, so nothing is timed unless its state matches.

04Programming model

Write a process once. Run it on a GPU.

In Days, every network element, whether a host or a switch egress port, is an isolated sequential process. It holds private state, reacts to timestamped messages, and affects other processes only by sending messages. It is a loop that receives, updates, and sends. It is not a set of callbacks against a global event queue.

Private state. No two processes share mutable state, so the CPU pool needs no locks.
Messages only. Processes interact only through the round's exchange, whose merge order is fixed by the canonical key.
Written once. Protocol logic is defined once, by the serial oracle, against a fixed vocabulary of seven mechanisms. The Metal and CUDA kernels are ported from it in the same per-element form. The reordering theorem, not the protocol author, absorbs what the hardware demands.

GeDES gets uniform GPU work by organizing execution around protocol stages: one kernel per stage, every slot. As a result, a protocol's logic is spread across those kernels, and adding a protocol means editing the whole pipeline.

The process model dates to Conway's coroutines and SIMULA's processes, more than six decades ago. Days carries it onto GPUs.

Byte-identity makes this checkable. Every new protocol, backend port, and measurement campaign in the paper was produced by coding agents and accepted only when the bytes matched.

05Evaluation

Measured against ns-3, Unison, legacy Days, and GeDES.

Three machines: an Apple M5 Max, an i7-13700K with an RTX 4090, and an NVIDIA DGX Spark (GB10). Every cross-simulator ratio was measured on the i7-13700K + RTX 4090 machine. Each sample records two clocks: the native clock (the simulation itself) and the process wall (end to end, including compilation, upload, and readback). Results from the paper, which is under review.

(a)TCP

TCP: even where slots are strongest, far ahead at the finish

FatTree-32, 8,192 closed-loop TCP Reno flows of 1 MiB each, run until every flow finishes, losses and retransmissions included. We report two framings of the same runs. The active frontier ends at the last data-bearing instant. Full completion ends when the last flow finishes.

Densest phase, vs GeDES: 0.563 s vs 0.565 s on the native clock, statistically even (a 0.4% median edge, inside GeDES's own run-to-run spread). On the process wall, Days is 1.9× faster (2.75 s vs 5.19 s).
Full completion, vs GeDES: 3,918× on native clocks and 821× on the process wall. GeDES spends 2,252 s stepping slots through a stretch of simulated time that includes a retransmission after a full 1-second timeout. The adaptive horizon crosses it in milliseconds.
CPU pool (22 workers), full-completion native clocks: 82.6× faster than sequential ns-3, 15.4× than ns-3 MPI at 8 ranks, and 9.0× than Unison at 24 threads. The CUDA backend is a further 8.7× faster.
One thread against one: the serial oracle is 3.3× faster than sequential ns-3.
The one loss: legacy Days at 24 workers beats the serial oracle on the native clock (0.84×), and loses on the wall clock.
Unison does not reproduce sequential ns-3's trajectory, even single-threaded, so its times measure speed on a divergent computation.

TCP experiment · native clock, seconds (log)

Active frontier
Full completion
Days
GeDES
Other

Native-clock seconds for every configuration, log scale. Days (CUDA) and GeDES are even at the active frontier; run through completion, they separate by 3,918×. Legacy Days and ns-3 MPI have no supported active-frontier clock, so they show full completion only.

› Data table

Configuration	Active (s)	Full (s)	Clock
Days, Scalar (serial oracle)	125.355489	126.224843	run_ns
Days, CPU (22 workers)	5.002304	5.006736	backend_ns
Days, CUDA (RTX 4090)	0.56314	0.574902	device_ns
Legacy Days, 1 thread	n/a	356.836233	Nexosim total
Legacy Days, 24 workers	n/a	106.110999	Nexosim total
GeDES (ported)	0.565158	2,252.5	Simulation Duration
ns-3, sequential	413.260065	413.40148	E5_CLOCK runS
ns-3 MPI, 8 ranks	n/a	77.001764	rank-0 E5_CLOCK runS
Unison, 24 threads	43.139538	44.89506	E5_CLOCK runS
Unison, 1 thread	401.564964	404.575131	E5_CLOCK runS

(b)UDP

UDP: where the curves cross

Same FatTree-32 fabric, constant-bit-rate traffic at 1%, 10%, 30%, and 60% offered load, 5,000 ns propagation, 60–126 million packets per load. GeDES executes 90,000 down to 2,000 slots as the simulated span shrinks. Days executes 17,046 down to 391 rounds, a count set by the traffic and identical on every backend.

On the RTX 4090's native clocks, Days (CUDA) is 6.1× faster at 1% load and 1.45× faster at 10%. At 30% and 60%, where the slots are full, GeDES leads, by 1.06× and 1.07×. On the process wall, Days is faster at every load on this machine, from 6.3× at 1% down to 1.2× at 60%.

On the DGX Spark's GB10, the crossover moves earlier. Days is 4.1× faster at 1%. GeDES leads on the native clock at 10%, 30%, and 60%, by 1.04×, 1.61×, and 1.89×. On the process wall, Days is faster at the first three loads and 6% slower at 60%.

Against the CPU simulators, the gaps are wider. Days (CUDA) runs 467–1,279× ahead of sequential ns-3 and 47–81× ahead of Unison at 24 threads, on native clocks on the RTX 4090 host.

UDP load sweep · seconds (log) vs offered load (log), RTX 4090 host

Days (CUDA)
Days (CPU, 22 workers)
GeDES

Fixed slots pay for simulated time and events pay for work. On native clocks (left), the curves cross between 10% and 30% load, and GeDES leads at 30% and 60%. On the end-to-end process wall (right), Days (CUDA) is faster at every load on the RTX 4090 host.

› Data table

Panel	Load	Series	Seconds	Clock
Native	1%	Days CUDA	3.039444	cuda_device_ns
Native	10%	Days CUDA	3.476381	cuda_device_ns
Native	30%	Days CUDA	1.936836	cuda_device_ns
Native	60%	Days CUDA	1.414949	cuda_device_ns
Native	1%	Days CPU	43.216664	executor_backend_ns
Native	10%	Days CPU	42.532565	executor_backend_ns
Native	30%	Days CPU	27.189576	executor_backend_ns
Native	60%	Days CPU	21.573915	executor_backend_ns
Native	1%	GeDES	18.4784	gedes_simulation_duration_ns
Native	10%	GeDES	5.04364	gedes_simulation_duration_ns
Native	30%	GeDES	1.8306	gedes_simulation_duration_ns
Native	60%	GeDES	1.31632	gedes_simulation_duration_ns
Process wall	1%	Days CUDA	3.88	GNU time -p real
Process wall	10%	Days CUDA	4.82	GNU time -p real
Process wall	30%	Days CUDA	4.43	GNU time -p real
Process wall	60%	Days CUDA	5.95	GNU time -p real
Process wall	1%	Days CPU	44.25	GNU time -p real
Process wall	10%	Days CPU	43.68	GNU time -p real
Process wall	30%	Days CPU	29.32	GNU time -p real
Process wall	60%	Days CPU	25.73	GNU time -p real
Process wall	1%	GeDES	24.45	wrapper-monotonic process_elapsed_ns
Process wall	10%	GeDES	11	wrapper-monotonic process_elapsed_ns
Process wall	30%	GeDES	7.78	wrapper-monotonic process_elapsed_ns
Process wall	60%	GeDES	7.26	wrapper-monotonic process_elapsed_ns

Native clock, seconds, RTX 4090 host
Load	1%	10%	30%	60%
Days (CUDA)	3.039	3.476	1.937	1.415
GeDES	18.48	5.044	1.831	1.316
Faster	Days 6.1×	Days 1.45×	GeDES 1.06×	GeDES 1.07×
Days rounds / GeDES slots	17,046 / 90,000	3,707 / 19,000	781 / 4,000	391 / 2,000

(c)Propagation

More lookahead, fewer rounds

The horizon is set by link delay, so Days should gain as propagation grows, and it does. At 1% load, sweeping propagation through 1, 2.5, 5, and 10 µs moves the native-clock ratio from 3.06× through 4.12× and 6.07× to 8.72× in Days' favor. Days' rounds fall from 51,138 to 8,767. GeDES keeps its 1,000 ns slot and runs the same 90,000 slots at every point, flat at about 18.5 s.

Propagation sweep, 1% load · native seconds, RTX 4090

Days (CUDA)
GeDES

Propagation sensitivity at 1% load, RTX 4090 native clocks. The GeDES-to-Days ratio grows with lookahead because Days' round count falls (annotated), while GeDES executes 90,000 slots at every point.

› Data table

Propagation (µs)	Days CUDA (s)	GeDES (s)	Ratio	Days rounds	GeDES slots
1	6.040599	18.4752	3.058505	51,138	90,000
2.5	4.482034	18.4811	4.123373	29,222	90,000
5	3.045635	18.4867	6.0699	17,046	90,000
10	2.122161	18.5145	8.724361	8,767	90,000

(d)Width

A GPU needs width

Width is the number of processes with pending work in a round. At 918 active processes, no GPU wins a single paired sample: the round offers too little parallelism to pay for the dispatch. Near 10,000, the CUDA devices take the lead. Metal never beats its own M5 Max CPU at any width we tested. It comes within 4.4% and stays behind.

Device over own host's CPU pool · per-round speedup (log)

RTX 4090 (vs i7, 24 workers)
GB10 (vs Grace, 20 workers)
Metal (vs M5 Max, 16 workers)
262,144 flows

Each GPU against its own host's CPU pool, per-round native clocks. The CUDA devices cross parity near 10⁴ active processes, and Metal stays below parity at every width. The open symbols mark the 262,144-flow run, measured on device clocks in a separate session.

› Data table

x	x basis	Device	Speedup	Point
918	mean active LPs	Metal	0.193	curve
918	mean active LPs	RTX 4090	0.846	curve
918	mean active LPs	GB10	0.676	curve
10,132	mean active LPs	Metal	0.956	curve
10,132	mean active LPs	RTX 4090	3.21	curve
10,132	mean active LPs	GB10	1.372	curve
23,739	mean active LPs	Metal	0.955	curve
23,739	mean active LPs	RTX 4090	2.79	curve
23,739	mean active LPs	GB10	1.206	curve
262,144	flow count	RTX 4090	13.11	frontier
262,144	flow count	GB10	6.12	frontier

Each device over its own host's CPU pool, same experiment; above 1.00 favors the device
Mean active processes	Metal (vs M5 Max, 16 workers)	RTX 4090 (vs i7, 24 workers)	GB10 (vs Grace, 20 workers)
918, closed-loop TCP	0.193	0.846	0.676
10,132, sustained	0.956	3.21	1.37
23,739, FatTree-48 sustained	0.955	2.79	1.21

(e)Largest run

262,144 flows, one state

Our largest experiment runs 262,144 closed-loop TCP Reno flows on FatTree-32: 1,151 rounds and 675 million transitions. It ends in one 2,274,074,943-byte state that is identical on both hosts and both GPUs.

On the GPU clock alone, the RTX 4090 is 13.1× faster than its own 24-worker CPU, and the GB10 is 6.1× faster than its Grace host. End to end, a first run gains only 1.92× and 1.11×, because host-side memory planning and readback dominate. The memory plan a run settles on is deterministic, so a later run can reuse it. That raises the end-to-end gain to 3.21× and 2.11×, with no change to the GPU time or the result.

(f)Cost model

Two constants predict the winner

time = A · rounds + B · transitions

A run costs a fixed amount per round plus a fixed amount per event executed: time = A · rounds + B · transitions. Fit per machine from its UDP runs, the model reproduces all fourteen measured runs with a median error of 0.4% (worst 9.6%). On the RTX 4090, A = 0.093 ms per round and B = 1.28 ns per event. The same form fits GeDES, at about 172 µs per slot plus 16 ns per packet, against about 27 ns per packet for Days. That is why the curves cross: GeDES does less work per packet, but it pays for every slot, whether or not any packet is in flight.

06Backends

Four backends, one image.

A scenario compiles once into an immutable image. The validator admits the image before anything runs. Any backend then executes it to the same byte-identical state. A backend that can't run a scenario faithfully refuses it up front.

Backends, where they run, and their role
Backend	Where it runs	Role
Scalar	One CPU thread	The reference oracle. It defines the semantics, and every other backend is checked against its bytes.
CPU	A multicore worker pool	Safe-horizon rounds across workers with no shared mutable state and no locks. It is byte-identical at every width.
Metal	Apple GPUs (not the M1 family)	The round loop runs on the device in waves, with a per-element design licensed by the reordering theorem.
CUDA	NVIDIA GPUs (built for sm_86, sm_89, and sm_121)	The kernels of a round form a fixed sequence that is captured as a CUDA Graph and replayed in bounded waves. Tested on a discrete RTX 4090, a discrete RTX A4500, and a unified-memory GB10.

What it models

Topologies: fat-tree, torus, dragonfly, and custom graphs.
Transport: closed-loop TCP Reno and CUBIC, rate-paced sources, and DCQCN with CNP.
Switches: FIFO, strict-priority, DRR, WRR, and exact-rational WFQ scheduling; TailDrop, ECN-threshold, RED, and RED-with-ECN admission; PFC.
Collectives: ring all-reduce and all-gather over TCP, with delay-only compute stages.

07Quick start

Run one scenario on every backend.

From the repository root. Every run uses the same small TCP smoke fixture.

01Scalar reference run

cargo run --release --bin days -- \
  configs/benchmarks/tcp/fattree_k4_tcp_cubic_f16_smoke.toml --engine scalar

02Multicore CPU run

cargo run --release --bin days -- \
  configs/benchmarks/tcp/fattree_k4_tcp_cubic_f16_smoke.toml \
  --engine cpu --workers 2 --repetitions 1

03GPU run on Apple Metal

cargo run --release --features metal --bin days -- \
  configs/benchmarks/tcp/fattree_k4_tcp_cubic_f16_smoke.toml --engine metal

04GPU run on NVIDIA

cargo run --release --features cuda --bin days -- \
  configs/benchmarks/tcp/fattree_k4_tcp_cubic_f16_smoke.toml --engine cuda

Every engine ends with a record=days_result line that carries the complete state's byte length and its FNV-1a fingerprint. If two runs have equal fingerprints, their results are byte-identical.

--engine metal and --engine cuda need their Cargo feature, and asking for either without it is an error. CUDA builds need a CUDA 13 toolkit. Install guide →

08Lineage

Legacy Days

Days began as an actor-model simulator on Nexosim coroutines, published at IEEE INFOCOM 2026. Its network elements were already processes with private state that communicate by messages. The new executor keeps that model and replaces the engine underneath it.

Legacy Days (up to version 0.4.3) is frozen in legacy/ as the days-legacy crate. It receives no new features, but CI still builds, tests, and runs it:

cargo run --release -p days-legacy --bin days-legacy -- configs/simple.toml

Read the legacy Days paper (PDF)Legacy docs

TCP experiment: the new CPU pool is 71.3× faster than legacy Days single-threaded and 21.2× faster than its 24-worker mode, on native clocks.
Per event: on UDP, the serial oracle spends about 360 ns per event, against about 1.3 µs for legacy Days single-threaded on the same work. That puts legacy Days 3.1–3.6× behind at the same machine and clock.
Determinism: legacy Days' multi-threaded mode returns different packet counts from run to run, so its clocks are reported but its counts are not.

09FAQ

Questions researchers ask

Is Days faster than GeDES?

It depends on the workload, and we report both sides. On TCP run to completion, Days (CUDA) is 3,918× faster on native clocks, because GeDES steps through every slot of idle simulated time. In the densest TCP phase, the two are statistically even. On UDP at 30% and 60% load, GeDES is 1.06× and 1.07× faster on the RTX 4090's native clock. On the GB10, GeDES leads at 10% through 60%. On the process wall, Days is faster at every load on the RTX 4090 host.

Which backend should I use?

Use Scalar to debug and as the reference. Use CPU for everything else, and for any scenario with RED, collectives, or compute stages. Use CUDA when rounds are wide: in our measurements the NVIDIA GPUs overtake their host CPUs near 10,000 active processes. Metal gives the same answer, but at no width we tested did it beat its own M5 Max CPU. Because every backend returns the same bytes, choosing one is purely a question of speed, and the cost model estimates it.

What does byte-identical buy me?

A bug seen on one backend reproduces at the same instant on every backend. A regression either changes the state or it doesn't, so no statistical judgment call is involved. CI can pin the complete final state of every scenario. And you can measure another simulator's approximation against an exact reference at the same scale.

Can I run DCQCN on a GPU?

Yes. DCQCN, including its controller and CNP state, runs on Metal and CUDA, and so does PFC. Every device run returns the same bytes as Scalar. A scenario with DCQCN or PFC runs on a separate round kernel with those mechanisms compiled in, reported as round_kernel=mechanisms in the record=days_device line. Other scenarios keep the plain kernel. RED, collectives, and compute stages still run on Scalar and CPU only. Metal and CUDA reject those scenarios at validation, with a message naming the backend, for example backend Metal does not support RED admission; use Scalar or Cpu. They never fall back silently.

Are the proofs about the code I run?

They are about a Lean model of the executor, in which each definition is annotated with the executor source location it formalizes. The link from model to binary is conformance testing: every backend must reproduce the serial oracle's complete state byte for byte, and nothing is timed unless it does.

What happened to the old Days?

It is frozen in legacy/ as days-legacy and still runs. Its paper is here. The new executor keeps its process model and is 21–71× faster on the TCP experiment.

What is the license?

AGPL-3.0-only.