# 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.