feat: add lab-rv32i-freertos-static-task card

2026-07-21 19:14:20 +02:00
commit 62efc0c91f
65 changed files with 33788 additions and 0 deletions
@@ -0,0 +1,76 @@
+# K08 — DynamicTask, StaticTask, deletion and lifetime
+
+## Position
+
+- Series: FreeRTOS C++
+- Lesson: L07, card K08
+- Duration: 30 minutes
+- Real dynamic `heap_4` plus caller TCB/stack in `.bss`
+- Idle task itself and the verifier use static storage to isolate measurement
+
+## Outcome
+
+After 30 minutes the student can calculate stack words and bytes, prove dynamic
+heap cost versus zero-delta static creation, classify TCB/stack addresses, and
+explain why self-deletion and actual dynamic memory reclamation are separated by
+idle-task cleanup.
+
+## Lesson plan
+
+| Time | Mode | Evidence |
+| --- | --- | --- |
+| 0–5 | units/storage | predict 256 words, bytes and locations |
+| 5–10 | dynamic create | measure heap delta and classify TCB/stack |
+| 10–15 | static create | caller TCB/stack addresses; heap delta zero |
+| 15–20 | run/complete | identical result 500500; wrappers completed/null |
+| 20–25 | delete timing | heap still reduced immediately after self-delete |
+| 25–30 | idle cleanup | block verifier; recover exact dynamic delta/baseline |
+
+## Canonical timeline
+
+```text
+baseline
+ -> xTaskCreate(dynamic): heap - dynamic_cost
+ -> xTaskCreateStatic(static): no heap change
+ -> both run and complete
+ -> both call vTaskDelete(nullptr)
+ -> verifier runs before idle: dynamic storage still pending cleanup
+ -> verifier blocks
+ -> idle calls termination cleanup:
+      dynamic TCB/stack -> vPortFree
+      static TCB/stack  -> not freed (caller owned)
+ -> verifier wakes: heap == baseline
+```
+
+## Stable evidence
+
+| Evidence | Required relation |
+| --- | --- |
+| dynamic cost | baseline - after_dynamic > 0 |
+| static delta | after_static == after_dynamic |
+| verifier delta | static verifier creation also leaves heap unchanged |
+| dynamic addresses | TCB and stack base lie in `ucHeap` |
+| static addresses | observed TCB/stack equal caller storage and lie outside heap |
+| before idle | free equals post-create value, despite completed wrappers |
+| after idle | free=baseline; recovered bytes=dynamic cost |
+| units | 256 `StackType_t` words = 1024 B on RV32I |
+
+## Main traps
+
+1. `stack_depth` counts words, not bytes.
+2. `vTaskDelete(nullptr)` removes the current task from scheduling but dynamic
+   memory reclamation is deferred to idle.
+3. Static task deletion does not free caller storage; premature reuse is a
+   lifetime bug.
+4. A wrapper handle becoming null is not proof that idle cleanup already ran.
+5. Forced deletion does not run arbitrary C++ destructors on the victim stack.
+
+## Acceptance
+
+- host test proves both create APIs receive the same stable context and static
+  native handle equals caller TCB;
+- ABI proves static worker storage is `.bss` and no vtable/init runtime exists;
+- static create and verifier create have exactly zero heap delta;
+- dynamic cost is recovered only after the verifier lets idle run;
+- both results are 500500, states completed, handles null and final PASS is 1.
+