user
103 lines
4.6 KiB
Markdown
103 lines
4.6 KiB
Markdown
# FC01 — plan iteracji diagramów w Hazard3
|
||
|
||
## Zasada
|
||
|
||
Kursor porusza się po diagramie, nie po przypadkowych liniach programu.
|
||
Każda kotwica ma jeden z dwóch kontraktów:
|
||
|
||
- `CODE` — otwiera właściwe źródło lub dowód ELF; nie uruchamia programu;
|
||
- `RUN` — odtwarza program od czystego resetu do wskazanego checkpointu,
|
||
ustawia Neovima i udostępnia zestaw wyrażeń GDB.
|
||
|
||
Ten sam snapshot może wystąpić w kilku perspektywach. Nie powtarza to
|
||
eksperymentu: A2 pyta o strukturę, A6 o stan, a A7 o jakość dowodu.
|
||
|
||
## A1 CONTEXT — granice odpowiedzialności
|
||
|
||
| Step | Tryb | Otwórz | Pytanie kontrolne |
|
||
|---|---|---|---|
|
||
| 01 Application | CODE | `main()` | Czy aplikacja dotyka metadanych allocatora? |
|
||
| 02 FreeRTOS API | CODE | wywołania `pvPortMalloc`, `vPortFree`, stats | Gdzie kończy się publiczny kontrakt? |
|
||
| 03 heap_4 | CODE | upstream `heap_4.c` | Które funkcje wybierają, dzielą i scalają blok? |
|
||
| 04 ucHeap | CODE | definicja `ucHeap[4096]` | Gdzie fizycznie leżą nagłówki i payload? |
|
||
| 05 Hazard3 | CODE | test symboli ELF | Czy debugujemy dokładnie artefakt z karty? |
|
||
|
||
A1 nie ma checkpointu: opisuje architekturę, a nie zdarzenie runtime.
|
||
|
||
## A2 STRUCTURE — nagłówek, split i scalenie
|
||
|
||
| Step | Tryb / replay | Obserwuj | Warunek zaliczenia |
|
||
|---|---|---|---|
|
||
| 01 Header | CODE | `BlockLink_t`, `portBYTE_ALIGNMENT` | raw header=8 B, alignment=16 B, `xHeapStructSize`=16 B |
|
||
| 02 Alignment | RUN E02 | `g_a`, `g_a_consumed` | A jest wyrównane, cały blok zużywa 48 B |
|
||
| 03 Split | RUN E02 | `g_after_a_stats` | pozostaje 1 wolny blok i 4032 B |
|
||
| 04 Address order | RUN E06 | `g_a`, `g_b`, `g_c`, stats | adresy rosną, a B rozdziela 2 wolne obszary |
|
||
| 05 Merge previous | RUN E06 + step | `pxIterator`, `pxBlockToInsert` | poprzedni/lewy blok jest testowany i scalany pierwszy |
|
||
| 06 Merge next | RUN E06 + step | powiększony blok i `pxNextFreeBlock` | następny/prawy blok jest scalany drugi |
|
||
|
||
Dla kroków 05–06 po replay E06:
|
||
|
||
```gdb
|
||
tbreak prvInsertBlockIntoFreeList
|
||
continue # wykonaj vPortFree(g_b)
|
||
p pxIterator
|
||
p pxBlockToInsert
|
||
next # test poprzedniego/lewego sąsiada
|
||
next # test następnego/prawego sąsiada
|
||
```
|
||
|
||
## A5 FLOW — pełny przebieg
|
||
|
||
| Event | Operacja | Wartości RV32/Hazard3 | Dowód |
|
||
|---|---|---|---|
|
||
| E01 | reset/init | free=4080 | 1 blok, largest=4080 |
|
||
| E02 | alloc A(24) | consumed=48, free=4032 | A != NULL, aligned=1 |
|
||
| E03 | alloc B(40) | consumed=64, free=3968 | B != NULL, aligned=1 |
|
||
| E04 | alloc C(16) | consumed=32, free=3936 | C != NULL, aligned=1 |
|
||
| E05 | free A | free=3984 | 2 wolne bloki |
|
||
| E06 | free C | free=4016 | 2 bloki, free > largest |
|
||
| E07 | free B | free=largest=4080 | 1 wolny blok, minimum-ever=3936 |
|
||
| E08 | oversized alloc | NULL | hook=1, asserts=0, layout=1, PASS=1 |
|
||
|
||
Każdy Enter na A5 wykonuje czysty replay do dokładnie jednego eventu. Nie
|
||
kontynuujemy stanu pozostałego po poprzednim kroku.
|
||
|
||
## A6 STATE — znaczenie liczników
|
||
|
||
| Step | Replay | Hipoteza |
|
||
|---|---|---|
|
||
| 01 Free | E01 | current free i largest są równe |
|
||
| 02 Allocated | E04 | przydziały zmniejszają current free do 3936 |
|
||
| 03 Fragmented | E06 | total free może być większe od largest |
|
||
| 04 Coalesced | E07 | current, largest i initial znów są równe |
|
||
| 05 Minimum-ever | E08 | minimum-ever pozostaje 3936 mimo odzyskania areny |
|
||
|
||
## A7 RUNTIME — jakość dowodu
|
||
|
||
| Step | Tryb / replay | Co musi znaleźć się w dowodzie |
|
||
|---|---|---|
|
||
| 01 Source | CODE | blob źródła eksperymentu |
|
||
| 02 ELF | CODE | SHA artefaktu i symbole upstream/checkpointów |
|
||
| 03 Fragmented | RUN E06 | PC, 2 bloki, free=4016, largest<free |
|
||
| 04 Memory | RUN E06 | adres `ucHeap`, adresy A/B/C i bajty nagłówków |
|
||
| 05 Verdict | RUN E08 | final=initial, OOM NULL, hook=1, asserts=0, PASS=1 |
|
||
|
||
Snapshot do raportu jest kompletny dopiero wtedy, gdy łączy nazwę eventu,
|
||
tożsamość ELF, pozycję programu i wartości rozstrzygające hipotezę.
|
||
|
||
## Świadomie pominięte perspektywy
|
||
|
||
- A3 DISPATCH — allocator nie ma callbacku ani mechanizmu dispatch;
|
||
- A4 APPLICATION — konkretny eksperyment A/B/C jest pełnym A5;
|
||
- A8 PATTERNS — first-fit i intrusive address-ordered list są już mierzalne w
|
||
A2 i A5; osobny diagram powielałby materiał.
|
||
|
||
## Definition of done
|
||
|
||
1. Hostowe modele i adapter przechodzą `tests/test_host.sh`.
|
||
2. ELF RV32 zawiera upstream `heap_4` oraz osiem symboli checkpointów.
|
||
3. Hazard3 RTL kończy Task03 kodem `0`.
|
||
4. E01–E08 spełniają wyrażenia z `debug_checkpoints`.
|
||
5. Wszystkie kroki RUN mają `snapshot_ref`; kroki CODE nie udają runtime.
|
||
6. SVG, HTML i TeX powstają z tego samego `json/card_source.json`.
|