user
108 lines
3.6 KiB
Markdown
108 lines
3.6 KiB
Markdown
# 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
|
||
```
|
||
|