Emberchip logo

Rust ยท deterministic RTOS simulator

Watch priority inversion,
then watch it lose.

Emberchip is a deterministic RTOS simulator on a small emulated microcontroller, written in pure Rust std. It models a preemptive fixed-priority scheduler, mutexes with priority inheritance, semaphores, queues, and memory-mapped peripherals, a GPIO LED, a UART, and a timer. Every run is a pure function of a seed, so its correctness gates make hard claims and check them. Pick a scenario and step it tick by tick.

Open the scheduler View on GitHub
How to use this playground

Every control, and what to look for.

Guided tour

  1. Leave the scenario on Priority inversion with inheritance on. Press Run.
  2. Watch low take the mutex (green L), then high arrive and block (amber cell, and a red BLOCK line in the log).
  3. See the purple INHERIT line: low is boosted to high's priority, so medium cannot steal the CPU. Low finishes its short critical section and hands the mutex straight to high.
  4. Note the high blocked readout. It is small, bounded by the critical section.
  5. Now turn inheritance off and press Run again. This time medium preempts low while high waits, and the high blocked readout balloons. That is unbounded priority inversion.
  6. Switch to Blinky and Run. Watch the LED toggle from the GPIO task, UART text stream, and higher-priority tasks preempt the workers, all with zero deadline misses.

Live scheduler

Pick a scenario, then step tick by tick or let it run. The Gantt shows which task holds the CPU each tick, who is merely ready, and who is blocked.

tick 0
running idle
deadline misses 0
invariant holds
running ready blocked cell letter: C compute, L lock, U unlock, G gpio, T uart
EMBER-1
GPIO0 → LED
UART output

      

Event log

kernel events

    

Where it sits

Emberchip is a teaching-accurate model, not firmware you can flash. Nothing here talks to real hardware. It fills the gap between a real board and a textbook. This is an honest positioning, not a benchmark.

A real board

FreeRTOS or Zephyr on a physical MCU is the real thing, but timing jitter, a debugger that changes the timing it measures, and a hundred vendor registers sit between you and the idea you are trying to understand.

A textbook

Describes the mechanism precisely, rate-monotonic bounds, priority inheritance, but you cannot poke it, step it, or watch the timeline move.

Emberchip

The middle. A model small enough to read end to end and precise enough that the scheduling theory shows up in the output exactly as predicted. Because every run is a pure function of a seed, you can step it tick by tick and get the same timeline every time.

what the model is built from

The RTOS mechanisms, each one you can watch

These are the real primitives an RTOS is built on, modeled on a tiny emulated MCU and checked by the correctness gates.

scheduler preemptive fixed-priority

A tick timer drives the scheduler; the highest-priority ready task runs one quantum at a time, and a higher-priority release preempts a running task.

inversion priority inheritance

A mutex holder is boosted to the highest waiter's priority so a medium task cannot stretch the blocking. The boost propagates down a chain of held mutexes, then is restored.

sync mutexes, semaphores, queues

Mutual exclusion that is never doubly held, counting semaphores that never lose or duplicate a signal, and message queues that deliver every value once and in order.

peripherals an emulated MCU

A memory-mapped GPIO with an LED, a UART, a timer, and an interrupt controller with ISR dispatch, all in ordinary Rust std.

analysis rate-monotonic schedulability

A utilization bound test and exact per-task worst-case response times give a schedulable verdict that the simulator then confirms on the same task set.

determinism a pure function of a seed

A seeded SplitMix64 PRNG makes every run byte-identical, which is what lets the gates make hard claims and check them across thousands of randomized task sets.

It is proven, not asserted

Because every run is a pure function of a seed and a task set, the correctness gates can make hard claims and check them. They are committed as tests and run in CI on every push. Every gate asserts the contention it depends on actually happened, so none can pass vacuously.

# the four correctness gates (cargo test)
tests/preemption.rs            the task that ran had the highest ready priority, every tick
tests/priority_inheritance.rs  on: high blocked no longer than the critical section
                               off: medium stretches the blocking well past it
tests/synchronization.rs       mutual exclusion, no lost or duplicated signals,
                               and a byte-identical event timeline across runs
tests/schedulability.rs        response-time analysis matches the simulated run

The inversion contrast you can trigger above is the same one gate 2 proves: with inheritance the high task is bounded by the low task's short critical section, and with it off the medium task pushes the blocking well beyond. Same seed, same task set, byte-identical timeline, every time.

Use it

A small CLI, a library you can drive from Rust, the four correctness gates, and a separate max-scale stress harness.

CLI

demo runs the blinky scenario, run a random schedulable set, inversion on|off the priority-inversion contrast, and analyze the response-time analysis against the simulated run.

Library API

Build a Kernel, add mutexes and Tasks described by a program of Ops, call run, and render the event timeline. The whole core is pure Rust std.

Correctness gates

Four gates committed as tests and run in CI. Set EMBERCHIP_FUZZ_OPS to widen the randomized runs; every gate checks the contention it depends on actually happened.

Stress harness

src/bin/stress.rs drives the kernel hard, checking invariants incrementally over log chunks so memory stays flat, with sizes read from environment knobs.

# the whole thing is pure Rust std, so it builds and runs anywhere
cargo run -- demo                # blinky, sensor, two workers sharing a mutex
cargo run -- run 300 --seed 7    # a random schedulable set, zero misses
cargo run -- inversion on        # priority inheritance bounds the blocking
cargo run -- inversion off       # unbounded inversion appears
cargo run -- analyze --seed 7    # response-time analysis vs the simulated run

# the correctness gates, widen the fuzzed runs with an env knob
cargo test
EMBERCHIP_FUZZ_OPS=2000 cargo test