62 lines
2.0 KiB
Markdown
62 lines
2.0 KiB
Markdown
# 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:
|
||
|
||
```text
|
||
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
|
||
|
||
```sh
|
||
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.
|
||
|