Crate rusty_rtos_demo 

rusty_rtos_demo — The FreeRTOS standard demo tasks (Demo/Common/Minimal) remade in Rust as the Kairos conformance corpus: every scenario self-checks like the C original and, on the sim port, diffs its trace against the C kernel’s.

This is the facade: it re-exports the no_std core. Depend on this crate; reach into the sub-crates only when you are building a port or a backend.

Part of Kairos (Remade With Rust). Plan: docs/plans/rusty_rtos_demo.md.

Modules

abortdelay

AbortDelay — xTaskAbortDelay against every blocking surface.

apisweep

ApiSweep — six public APIs that no upstream demo reaches.

blockq

BlockQ — blocking sends and receives, three task pairs.

blocktim

blocktim — block times, honoured to the tick.

countsem

countsem — counting semaphores, driven to both ends of their range.

death

death — the scenario that deletes tasks.

dynamic

dynamic — the first scenario of the conformance corpus.

eventgroups

EventGroupsDemo — four tasks around one event group, and an interrupt around another.

genqtest

GenQTest — send-to-front, send-to-back, peek, and priority inheritance.

intqueue

IntQueue — two queues, six tasks and two interrupt handlers.

intsem

IntSemTest — semaphores given from an interrupt, mutexes shared with one.

mbamp

MessageBufferAMP — one message buffer per “core”, and a send that wakes the reader the long way round.

messagebuffer

MessageBufferDemo — the message buffer, which is a stream buffer that keeps its lengths.

pins

The pinned corpus: what the C kernel printed, in one place.

pollq

PollQ — a queue polled from both ends, never blocking.

pollq_async

PollQ a third time, with the task bodies as async fn (K2.2).

pollq_typed

PollQ, written against the Rust face instead of the C-shaped one.

prelude

The names a firmware wants in scope.

qoverwrite

QueueOverwrite — a queue of one, written to whether or not it is full.

qpeek

QPeek — four priorities peeking at one queue, and the order they wake in.

qset

QueueSet — three queues in one set, written by a task and an interrupt.

qsetpoll

QueueSetPolling — a queue set polled by a task, written by an interrupt.

recmutex

recmutex — a recursive mutex, and the priority inheritance around it.

runner

The sim runner: what plays the part the pthreads play in the C harness.

sbint

StreamBufferInterrupt — a string sent from the tick, read a byte at a time.

semtest

semtest — two binary semaphores, four tasks, one shared variable each.

streambuffer

StreamBufferDemo — the stream buffer tortured from every side.

tasknotify

TaskNotify — every notification method, checked against itself.

timerdemo

TimerDemo — software timers, checked against the tick they fire on.

trace

The trace sink: one line per kernel event, in the contract’s format.

Structs

Digest

A sink that digests as it goes, so the whole trace never has to be held in RAM — which is what lets a 780 KB trace be checked on a chip with far less than that.

LineTrace

A Trace that writes the contract’s lines to W.

Pin

One scenario’s pinned verdict and trace digest.

Runner

The runner: a kernel, one body per task, and the scenario’s statics.

Shared

What every task body can reach: the scenario’s statics, plus the two things the harness owns.

Verdict

What a finished run reports — the C harness’s KAIROS_RESULT line.

Enums

Body

One task body. An enum rather than a dyn object so the runner needs no allocator and a firmware can hold the whole corpus in .bss. It is not Copy, and cannot be: Body::Async holds a pinned borrow of a future, and a future is exactly the thing that must not be duplicated. Nothing needed it to be.

Scenario

The scenarios this crate can run.

Step

What one step of a task body reports back to the runner.

Constants

DEFAULT_STEP_LIMIT

The limit for the C harness’s default run length.

PIN_TICKS

The DEFAULT length of a pinned run. The check task ends the run at the first wake-up on or after this, so a scenario can report a tick or two more.

VERSION

Crate version, for manifests and logs.

Functions

pins

The pinned corpus, over any sink.

step_limit_for

The runner’s safety net: the most steps a scenario may take before the run is called a runaway.

Type Aliases

SimKernel

The kernel every scenario runs on: the Posix_GCC demo’s configuration (the one the oracle runs), the deterministic sim port, and a sink that writes the contract’s lines.