FC03 — Tick, Priorities, Preemption and Time Slicing

FC03 is a freestanding C11 FreeRTOS card for RV32I/Hazard3. It turns the scheduler rules from Chapter 4 of the official FreeRTOS Kernel Book into one bounded, replayable experiment.

The program proves two independent facts:

equal priorities:  peer A -> peer B -> peer A
priority change:   before_raise -> HIGH -> after_raise

The first trace is produced by two CPU-bound tasks at priority 2 with preemption and time slicing enabled. The second trace is produced when peer A raises a Ready task from priority 0 to priority 3. That task must run before vTaskPrioritySet() returns to peer A.

Book mapping

• Chapter 4.5 — task priorities;
• Chapter 4.6 — time measurement and the tick;
• Chapter 4.9 — changing task priority;
• Chapter 4.12 — time slicing.

The order of the FreeRTOS C series is curated for the laboratory. It is not a claim that every optional chapter or API variant appears in the first fifteen cards.

Build and checks

make task1
make host-test
make check-abi
./scripts/run_sim.sh
./scripts/check_determinism.sh

check-abi rejects C++ runtime dependencies. The deterministic replay uses application-owned records and public FreeRTOS APIs. Kernel internals may be inspected in GDB, but they are never required by the application assertions.

Evidence contract

• E01–E05: configuration, handles, priorities and scheduler start;
• E06: first bounded tick-hook observation;
• E07: committed A-B-A task-change trace;
• E08–E10: immediate-preemption marker projection;
• E11: peer self-deletion complete;
• E12: low-priority verifier publishes PASS.

The tick hook writes only a bounded diagnostic record and calls a dedicated ISR-safe checkpoint sink. It does not print, allocate, block or use task-only APIs.

Generated material

json/card_source.json is the single card source. Rendering produces HTML and TeX only; PDF generation and commits are separate, explicit operations.