feat: add lab-rv32i-freertos-allocator-resource card

2026-07-21 19:13:55 +02:00
commit 5432095596
65 changed files with 34038 additions and 0 deletions
@@ -0,0 +1,106 @@
+# K06 — MemoryResource and FreeRtosAllocator<T>
+
+## Position
+
+- Series: FreeRTOS C++
+- Lesson: L05, card K06
+- Duration: 30 minutes
+- Runtime: FreeRTOS `heap_4.c` plus a 256-byte `.bss` arena on Hazard3
+- C++ mode: freestanding C++17, no exceptions, RTTI, vtables or hosted allocator
+
+K05 selected and measured one kernel heap. K06 adds an explicit runtime
+resource boundary so identical typed code can use either that heap or caller
+owned static storage.
+
+## Outcome
+
+After 30 minutes the student can draw the three-word resource object, explain
+why it is not virtual inheritance, implement overflow-safe `count*sizeof(T)`,
+classify addresses by storage domain, and state the different release policies
+of a general heap and monotonic arena.
+
+## Lesson plan — 30 minutes
+
+| Time | Mode | Evidence |
+| --- | --- | --- |
+| 0–5 | contract | draw context + allocate/deallocate functions |
+| 5–10 | typed count | complete and justify the overflow guard |
+| 10–16 | two resources | allocate 16 `uint32_t` values from heap and arena |
+| 16–21 | address proof | classify `ucHeap` versus `.bss`; check alignment |
+| 21–26 | failure | overflow and capacity failures change no storage state |
+| 26–30 | release | compare heap free, arena no-op deallocate and reset |
+
+## Runtime dispatch without vtable
+
+```cpp
+struct MemoryResource {
+    void* context;
+    void* (*allocate)(void*, size_t, size_t) noexcept;
+    void  (*deallocate)(void*, void*, size_t, size_t) noexcept;
+};
+```
+
+The provider owns state; the view stores a non-owning context. `HeapResource`
+counts attempts and delegates to FreeRTOS. `StaticArenaResource` stores base,
+capacity and current offset. The ELF must have no vtable/typeinfo.
+
+## Typed overflow contract
+
+For `T` and `count`:
+
+```text
+count == 0                         -> nullptr
+count > SIZE_MAX / sizeof(T)       -> nullptr, resource not called
+otherwise bytes=count*sizeof(T)    -> resource.allocate(bytes, alignof(T))
+```
+
+The failure must not wrap to a small allocation. Both resource counters and
+storage state are captured before and after the overflow request.
+
+## Canonical experiment
+
+```text
+HeapResource --MemoryResource--> FreeRtosAllocator<uint32_t> -> 16 values
+    address inside ucHeap; deallocate -> baseline immediately
+
+StaticArenaResource --MemoryResource--> same typed allocator -> 16 values
+    address inside g_static_arena_storage (.bss)
+    deallocate -> used remains 64
+    reset      -> used becomes 0
+```
+
+Both addresses satisfy `address % alignof(uint32_t) == 0` and both buffers
+produce the predicted sums.
+
+## Stable evidence
+
+| Evidence | Required relation |
+| --- | --- |
+| resource representation | context and function pointers are non-null; allocate functions differ |
+| heap address | lies inside `ucHeap`, aligned for `uint32_t` |
+| arena address | lies in global arena range, outside `ucHeap`, aligned |
+| overflow | both return null before provider failure counters increase |
+| capacity failure | heap available and arena used remain unchanged |
+| heap policy | successful=1, failed=1, deallocations=1; final free=baseline |
+| arena policy | successful=1, failed=1; used 64 after deallocate, 0 after reset |
+
+## Main traps
+
+1. Multiply only after the division guard; detecting overflow after wrapping is
+   too late.
+2. A resource view does not own its context; provider lifetime must dominate.
+3. Arena `deallocate` is not heap free. Reset invalidates all arena allocations
+   at once and therefore needs an external lifetime boundary.
+4. An alignment greater than the provider guarantee must fail explicitly.
+5. This fallible allocator is not ordinary `new` and is not advertised as a
+   complete hosted/STL allocator.
+
+## Acceptance
+
+- host ASan/UBSan test validates alignment, overflow and no-op/reset behavior;
+- `MemoryResource` occupies three pointers and all resource classes are
+  non-polymorphic;
+- ABI has no vtable, RTTI, unwind, dynamic initializer or global new/delete;
+- Hazard3 proves two storage domains and identical 16-element operations;
+- all failure and release relations pass at checkpoint 7.
+