feat: add lab-rv32i-freertos-vector-raii card
This commit is contained in:
@@ -0,0 +1,105 @@
|
||||
# K03 — Vector V1: destructor, move, ownership and RAII
|
||||
|
||||
## Position in the series
|
||||
|
||||
- Series: FreeRTOS C++
|
||||
- Lesson: L02, card K03
|
||||
- Executables: exactly one
|
||||
- Kernel: unchanged FreeRTOS V11.3.0 in C
|
||||
- C++ mode: freestanding C++17, no exceptions, RTTI or hosted `libstdc++`
|
||||
- Starting artifact: the deliberately incomplete `Vector V0` shown on the card
|
||||
|
||||
The current K02 card concentrates on `Task<Derived>` and does not require a
|
||||
separate Vector exercise. K03 therefore carries its short V0 starting snippet
|
||||
on page 1. This removes a hidden prerequisite without spending a second card
|
||||
on the broken implementation.
|
||||
|
||||
## Outcome
|
||||
|
||||
After 45 minutes the student can state and prove the one-owner invariant,
|
||||
explain why copy operations are deleted, implement the release-before-transfer
|
||||
order of move assignment, and show in Hazard3 that normal scope exit returns
|
||||
the FreeRTOS heap to its baseline.
|
||||
|
||||
## Canonical experiment
|
||||
|
||||
```text
|
||||
heap baseline
|
||||
-> source(4) owns A
|
||||
-> destination(2) owns B
|
||||
-> destination = move(source)
|
||||
free B
|
||||
destination takes A
|
||||
source becomes {nullptr, 0}
|
||||
-> final_owner(move(destination)) owns A
|
||||
-> final_owner destructor frees A
|
||||
-> two empty moved-from objects destruct without another free
|
||||
-> heap baseline restored
|
||||
```
|
||||
|
||||
## Lesson plan — 45 minutes
|
||||
|
||||
| Time | Mode | Student evidence |
|
||||
| --- | --- | --- |
|
||||
| 0–5 | diagnose V0 | identify leak, shallow-copy double-free risk and missing ownership rule |
|
||||
| 5–11 | destructor | connect object scope to `delete[]` and then to `vPortFree()` |
|
||||
| 11–17 | copy vs move | justify deleted copy and the empty moved-from state |
|
||||
| 17–25 | move assignment | order `release -> take -> clear source`; handle occupied destination and self-move |
|
||||
| 25–38 | Hazard3/GDB | replay checkpoints 1–7 and follow buffer A, buffer B, counts and heap bytes |
|
||||
| 38–43 | exercise | complete the three state-changing parts of move assignment and test the invariant |
|
||||
| 43–45 | exit | explain one-owner, baseline recovery and the limit of RAII under forced task deletion |
|
||||
|
||||
## Stable evidence contract
|
||||
|
||||
| Point | Required observation |
|
||||
| --- | --- |
|
||||
| 1 | `g_initial_free` is the reference after heap initialization |
|
||||
| 2 | `source.data() == A`, allocation count 1 |
|
||||
| 3 | `destination.data() == B`, `A != B`, allocation count 2 |
|
||||
| 4 | first freed address is B; destination has A; source is empty |
|
||||
| 5 | final owner has the same A; destination is empty |
|
||||
| 6 | A is the second freed address; current free equals baseline |
|
||||
| 7 | allocations=2, deallocations=2, live=0, `pass=1` |
|
||||
|
||||
Numeric heap values are recorded but the assessment relies on relations:
|
||||
|
||||
```text
|
||||
after_two_owners < initial
|
||||
minimum_ever <= after_two_owners
|
||||
after_scope == initial
|
||||
```
|
||||
|
||||
## Student exercise
|
||||
|
||||
The destination already owns B. The learner must put these operations in the
|
||||
only safe order and explain each invariant boundary:
|
||||
|
||||
```cpp
|
||||
if (this != &other) {
|
||||
release();
|
||||
elements_ = other.elements_;
|
||||
size_ = other.size_;
|
||||
other.elements_ = nullptr;
|
||||
other.size_ = 0;
|
||||
}
|
||||
```
|
||||
|
||||
Required reasoning:
|
||||
|
||||
1. Taking A before releasing B loses the only pointer to B and leaks it.
|
||||
2. Releasing after taking A would free A, the buffer just transferred.
|
||||
3. Not clearing the source creates two owners and a later double free.
|
||||
4. Omitting the self-move guard releases the only buffer before reading it.
|
||||
|
||||
## Acceptance
|
||||
|
||||
- host test passes under ASan and UBSan;
|
||||
- a copy attempt fails to compile because the operation is deleted;
|
||||
- ELF contains no vtable, RTTI, exceptions, dynamic initializer or hosted C++
|
||||
dependency;
|
||||
- all six required scalar/array, sized/unsized allocation functions exist;
|
||||
- Hazard3 reaches checkpoint 7 with `pass=1`;
|
||||
- student connects `delete[] -> operator delete[] -> vPortFree()`;
|
||||
- student states that RAII requires normal C++ lifetime completion and does not
|
||||
promise cleanup after arbitrary task termination.
|
||||
|
||||
Reference in New Issue
Block a user