feat: add organization-per-series EDU catalog
This commit is contained in:
@@ -0,0 +1,186 @@
|
||||
# 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.
|
||||
Reference in New Issue
Block a user