187 lines
10 KiB
Markdown
187 lines
10 KiB
Markdown
# FC03 Plan — Tick, Priorities, Preemption and Time Slicing
|
||
|
||
Status: implementation started after completed FC02. Language: freestanding
|
||
C11 only. Primary source: FreeRTOS Kernel Book sections 4.5, 4.6, 4.9 and
|
||
4.12.
|
||
|
||
## Learning contract
|
||
|
||
The student must distinguish four scheduler facts:
|
||
|
||
1. the highest-priority Ready task is selected;
|
||
2. equal-priority Ready tasks may time-slice when the option is enabled;
|
||
3. the tick provides a scheduling opportunity, not per-task fairness;
|
||
4. making a higher-priority task Ready can preempt the caller immediately.
|
||
|
||
The card does not teach delays, queues, semaphores, ISR-safe APIs or C++.
|
||
|
||
## Controlled experiment
|
||
|
||
```text
|
||
priority 0→3 high_probe Ready but initially below the verifier
|
||
priority 2 peer_A CPU-bound trace producer
|
||
priority 2 peer_B CPU-bound trace producer
|
||
priority 1 verifier final invariant checker
|
||
```
|
||
|
||
The program creates `high_probe` Ready at priority 0. The two peers then run
|
||
at equal priority 2 until the trace contains A→B→A. Peer A commits a
|
||
`before_raise` marker and raises the probe to priority 3 with
|
||
`vTaskPrioritySet`. With preemption enabled, `high_probe` must commit its
|
||
marker before peer A can commit `after_raise`. The probe self-deletes. After
|
||
the call returns, peer A commits `after_raise`, requests both peers to stop,
|
||
and each peer clears its own public handle before self-deleting. Only then can
|
||
the priority-1 verifier run and publish PASS.
|
||
|
||
This produces two independent scheduler proofs in one bounded trace:
|
||
|
||
```text
|
||
equal priority: A → B → A time slicing
|
||
priority change: A.before → HIGH → A.after immediate preemption
|
||
```
|
||
|
||
## Applicable viewpoints
|
||
|
||
| View | Status | Purpose |
|
||
|---|---|---|
|
||
| A1 CONTEXT | enabled | `mtime/mtimecmp` → tick ISR → scheduler → tasks |
|
||
| A2 STRUCTURE | enabled | task contexts, priorities, handles and trace buffers |
|
||
| A3 DISPATCH | unavailable | callback/context dispatch was proved in FC02 and is unchanged |
|
||
| A4 APPLICATION | enabled | four-task experiment topology and invariants |
|
||
| A5 FLOW | enabled | ordered time-slice and preemption checkpoints |
|
||
| A6 STATE | enabled | Ready/Running lanes and priority-change selection |
|
||
| A7 RUNTIME | enabled | tick hook, `mcause`, PC/SP, current handle and trace |
|
||
| A8 PATTERNS | unavailable | scheduler policy is a kernel configuration, not an application design pattern |
|
||
|
||
## Canonical tree
|
||
|
||
```text
|
||
Series · FreeRTOS C
|
||
└── Card FC03 · Tick, Priorities, Preemption and Time Slicing
|
||
└── Task01 · Controlled scheduler experiment
|
||
├── Block · A1 CONTEXT
|
||
│ └── Phase · TICK / SCHEDULER BOUNDARY
|
||
│ ├── Step 01 · Hazard3 mtime reaches mtimecmp [CODE]
|
||
│ ├── Step 02 · port tick handler enters the kernel [CODE]
|
||
│ ├── Step 03 · scheduler selects a Ready task [CODE]
|
||
│ └── Step 04 · application records public evidence [CODE]
|
||
├── Block · A2 STRUCTURE
|
||
│ └── Phase · TASKS / TRACE
|
||
│ ├── Step 01 · peer contexts have equal priority [CODE]
|
||
│ ├── Step 02 · high probe priority contract is 0 → 3 [CODE]
|
||
│ ├── Step 03 · verifier has priority 1 [CODE]
|
||
│ ├── Step 04 · switch trace stores task and tick [CODE]
|
||
│ └── Step 05 · before/high/after order is explicit [CODE]
|
||
├── Block · A4 APPLICATION
|
||
│ └── Phase · EXPERIMENT TOPOLOGY
|
||
│ ├── Step 01 · high probe starts Ready at priority 0 [RUN E02]
|
||
│ ├── Step 02 · peers compete at priority 2 [RUN E04]
|
||
│ ├── Step 03 · peer A raises high probe to priority 3 [RUN E08]
|
||
│ └── Step 04 · verifier is intentionally lowest [RUN E12]
|
||
├── Block · A5 FLOW
|
||
│ ├── Phase · PREPARE / TIME SLICE
|
||
│ │ ├── Step 01 · contexts and config committed [RUN E01]
|
||
│ │ ├── Step 02 · high probe created at priority 0 [RUN E02]
|
||
│ │ ├── Step 03 · all handles and priorities verified [RUN E03]
|
||
│ │ ├── Step 04 · scheduler starts [RUN E04]
|
||
│ │ ├── Step 05 · first peer runs [RUN E05]
|
||
│ │ ├── Step 06 · first tick hook observes timer interrupt [RUN E06]
|
||
│ │ └── Step 07 · trace contains A→B→A [RUN E07]
|
||
│ └── Phase · PREEMPT / FINISH
|
||
│ ├── Step 08 · peer A commits before_raise [RUN E08]
|
||
│ ├── Step 09 · high probe runs before caller returns [RUN E09]
|
||
│ ├── Step 10 · peer A commits after_raise and stop [RUN E10]
|
||
│ ├── Step 11 · equal-priority peers finish [RUN E11]
|
||
│ └── Step 12 · low-priority verifier publishes PASS [RUN E12]
|
||
├── Block · A6 STATE
|
||
│ ├── Phase · HIGH PROBE
|
||
│ │ ├── Step 01 · Ready at priority 0 [RUN E02]
|
||
│ │ ├── Step 02 · Ready priority changes 0 → 3 [RUN E08]
|
||
│ │ └── Step 03 · selected → Running → Deleted [RUN E09]
|
||
│ └── Phase · PEERS / VERIFIER
|
||
│ ├── Step 04 · peer A and B alternate Ready/Running [RUN E07]
|
||
│ ├── Step 05 · caller remains Ready during preemption [RUN E09]
|
||
│ └── Step 06 · verifier runs after priorities 2/3 end [RUN E12]
|
||
├── Block · A7 RUNTIME
|
||
│ ├── Phase · TIMER / CPU
|
||
│ │ ├── Step 01 · tick hook records machine-timer cause [RUN E06]
|
||
│ │ ├── Step 02 · ticks in trace are nondecreasing [RUN E07]
|
||
│ │ └── Step 03 · PC/SP identify the selected task [RUN E09]
|
||
│ └── Phase · SCHEDULER EVIDENCE
|
||
│ ├── Step 04 · priorities read through public API [RUN E03]
|
||
│ ├── Step 05 · marker projection is before/high/after [RUN E10]
|
||
│ └── Step 06 · source, ELF and final invariants match [RUN E12]
|
||
└── Exercise · Bounded no-time-slicing observation and explanation
|
||
```
|
||
|
||
## Checkpoint contract
|
||
|
||
| Event | Snapshot | Required observation |
|
||
|---|---|---|
|
||
| E01 | `task01.config` | one core; preemption, time slicing, tick hook, priority get/set and delete enabled |
|
||
| E02 | `task01.high-dormant` | high handle exists and priority is 0 |
|
||
| E03 | `task01.priorities` | high=0, peers=2/2, verifier=1 via public API |
|
||
| E04 | `task01.scheduler` | scheduler start requested with all handles valid |
|
||
| E05 | `task01.peer-entry` | peer A or B is Running on its own stack |
|
||
| E06 | `task01.first-tick` | tick hook count=1; timer cause and ISR stack recorded |
|
||
| E07 | `task01.timeslice` | committed trace contains A→B→A and nondecreasing ticks |
|
||
| E08 | `task01.before-raise` | caller marker set; high marker and after marker clear |
|
||
| E09 | `task01.high-preempts` | high marker set while caller after marker remains clear |
|
||
| E10 | `task01.after-raise` | marker projection is A.before→HIGH→A.after; stop requested |
|
||
| E11 | `task01.peers-finished` | both peer handles cleared after bounded work |
|
||
| E12 | `task01.pass` | verifier ran last and every scheduler invariant is true |
|
||
|
||
All task-context checkpoint writes complete before entering the stable
|
||
noinline sink. The tick hook uses a separate ISR-safe sink, emits E06 only
|
||
once and performs bounded writes only. E07 is emitted only by peer A after a
|
||
one-entry-per-observed-slice trace contains A→B→A. The exact
|
||
before→HIGH→after claim applies to the marker projection, not to every task
|
||
that may legally run before peer A is selected again.
|
||
|
||
## Debug strategies
|
||
|
||
- `code.tick-boundary`: open RISC-V port/config and trace the public boundary
|
||
without making application code depend on kernel internals.
|
||
- `code.scheduler-data`: inspect C contexts, priority constants and trace
|
||
layout; compile-time assertions keep IDs and buffer bounds stable.
|
||
- `run.tick`: stop in the first tick hook; capture `mcause`, `mepc`, ISR SP,
|
||
tick count and source/ELF identity.
|
||
- `run.timeslice`: show the trace buffer beside peer source and current
|
||
task/PC evidence; assert A→B→A.
|
||
- `run.preempt`: show `before_raise`, high marker and `after_raise` beside
|
||
the call site and selected task; assert the exact ordering.
|
||
- `run.pass`: show all handles, priorities, ticks and final invariants.
|
||
|
||
Application assertions use only public APIs and application-owned records.
|
||
Kernel internals such as `pxCurrentTCB` may appear only as a clearly labelled
|
||
debugger observation in A7.
|
||
|
||
## Page layout
|
||
|
||
1. goal, scope, book mapping and viewpoint index — portrait;
|
||
2. A1 vertical context — portrait;
|
||
3. A2 data/trace structure — landscape;
|
||
4. A4 experiment topology — landscape;
|
||
5. A5 part 1, E01–E07 — landscape;
|
||
6. A5 part 2, E08–E12 — landscape, joined with sheet 5 on screen;
|
||
7. A6 state lanes — landscape;
|
||
8. A7 tick/CPU/scheduler evidence — landscape.
|
||
|
||
Each diagram starts on a new sheet. The A5 split is one logical sequence with
|
||
identical participants and a centered join; no block is cut at the sheet
|
||
boundary.
|
||
|
||
## Acceptance gates
|
||
|
||
- RV32I/Hazard3 freestanding C11 build against the pinned FreeRTOS kernel;
|
||
- no C++ runtime or mangled application symbols;
|
||
- deterministic E01–E12 replay from clean RAM;
|
||
- A→B→A occurs with equal priority and at least two tick observations;
|
||
- high probe commits before peer A returns from `vTaskPrioritySet`;
|
||
- verifier priority is lower and it publishes PASS only after higher tasks
|
||
terminate;
|
||
- every CODE step resolves a stable source reference;
|
||
- every RUN step has a strategy, checkpoint and non-empty assertions;
|
||
- generated HTML and TeX validate; no PDF and no commit without an explicit
|
||
request.
|