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:

the highest-priority Ready task is selected;
equal-priority Ready tasks may time-slice when the option is enabled;
the tick provides a scheduling opportunity, not per-task fairness;
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

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:

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

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

goal, scope, book mapping and viewpoint index — portrait;
A1 vertical context — portrait;
A2 data/trace structure — landscape;
A4 experiment topology — landscape;
A5 part 1, E01–E07 — landscape;
A5 part 2, E08–E12 — landscape, joined with sheet 5 on screen;
A6 state lanes — landscape;
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.

10 KiB Raw Permalink Blame History Unescape Escape