feat: add lab-rv32i-freertos-scheduler-states card

2026-07-21 19:14:20 +02:00
commit 71ddd87301
66 changed files with 34187 additions and 0 deletions
@@ -0,0 +1,107 @@
+# K04 — FreeRTOS C++: scheduler states, priorities and typed ticks
+
+K04 turns the scheduler into an observable experiment. Two worker tasks start
+at priority 2. The program proves three separate mechanisms on the real
+FreeRTOS kernel and Hazard3/RV32I:
+
+1. equal-priority ready tasks alternate when time slicing is enabled;
+2. `vTaskDelay(3)` moves A to `eBlocked`, so B runs even though it has no
+   higher priority;
+3. raising B from priority 2 to 3 makes B run before A returns from
+   `vTaskPrioritySet()`.
+
+The C++ layer is deliberately small. [`Ticks`](include/freertos/ticks.hpp) and
+[`TickPoint`](include/freertos/ticks.hpp) separate durations from time points.
+[`TaskRef`](include/freertos/task_ref.hpp) is a non-owning view of a
+`TaskHandle_t`; it can inspect state and priority but never deletes a task.
+
+## Evidence sequence
+
+The executable stores eight records in `g_snapshots`:
+
+| Event | A | B | Current | Meaning |
+| --- | --- | --- | --- | --- |
+| 1 | READY | READY | startup | scheduler is running; both workers can run |
+| 2 | RUNNING | READY | A | A is about to request a three-tick delay |
+| 3 | BLOCKED | RUNNING | B | B observes A on the delayed list |
+| 4 | RUNNING | READY | A | A wakes exactly three ticks later |
+| 5 | RUNNING | READY | A | marker `BEFORE=1`, just before raising B |
+| 6 | READY | RUNNING, p=3 | B | marker `HIGH=2`, immediate preemption |
+| 7 | RUNNING | READY, p=2 | A | marker `AFTER=3`, API call finally returned |
+| 8 | DELETED | DELETED | verifier | both workers completed; PASS can be checked |
+
+The first record is intentionally taken by a short highest-priority startup
+task *after* `vTaskStartScheduler()`. Calling `eTaskGetState()` before the
+scheduler starts can expose the kernel's selected current TCB and is not a
+sound way to claim that a task has already run.
+
+## Relative and periodic delay
+
+- `vTaskDelay(Ticks{3}.count())` blocks relative to the tick at which the call
+  is made.
+- `xTaskDelayUntil(&next, Ticks{1}.count())` advances a stored wake reference;
+  the verifier uses it for periodic checks without accumulating its own work
+  time as drift.
+
+A tick is not inherently one millisecond. In this laboratory
+`configTICK_RATE_HZ == 1000`, so it happens to be 1 ms, but the code and the
+student's reasoning use tick counts rather than a hidden wall-clock unit.
+
+## Build and verify
+
+The local fallback obtains Hazard3 startup support and the simulator from the
+neighboring FreeRTOS C scheduler card. They can also be supplied explicitly
+with `RV_ENV_ROOT` and `TB`.
+
+```sh
+make check
+```
+
+Expected summary:
+
+```text
+PASS host: typed ticks and non-owning TaskRef
+PASS ABI: zero-cost Tick/TaskRef wrappers and stable evidence symbols
+PASS task01: states + time slicing + priority preemption
+00000001
+00000002
+00000001
+00000003
+00000001
+00000002
+00000003
+```
+
+The alternating task IDs may be `1,2,1` or `2,1,2`; the contract checks the
+relation, not which equal-priority task happens to start first. The final four
+values must always be delay `3` and priority markers `1,2,3`.
+
+## Debugger evidence
+
+```gdb
+p g_switch_count
+p g_alternating_tasks
+p g_alternating_ticks
+p g_snapshot_count
+p g_snapshots
+p g_delay_start_tick
+p g_delay_observed_tick
+p g_delay_end_tick
+p g_delay_elapsed
+p g_priority_order
+p g_scheduler_states_pass
+```
+
+## Scope boundary
+
+This card does not introduce an owning task class or a scheduler facade.
+`TaskRef` becomes invalid when the referenced task's TCB is deleted. Event 8
+therefore records the known terminal state without dereferencing stale worker
+handles. Static/dynamic task ownership and deletion policy belong to K07–K09.
+
+Render the printable worksheet with:
+
+```sh
+make pdf
+```
+