feat: add interactive FC01 heap4 card
This commit is contained in:
user
File diff suppressed because it is too large
Load Diff
@@ -0,0 +1,811 @@
|
||||
{
|
||||
"card": {
|
||||
"number": "01",
|
||||
"slug": "heap4-mechanics",
|
||||
"title": "heap_4: From Linear Cursor to Reusable Blocks",
|
||||
"topic": "headers, address-ordered free list, first-fit, split, coalescing and heap statistics",
|
||||
"status": "Gotowa",
|
||||
"version": "v00.01",
|
||||
"revision_date": "2026-07-20T00:00:00+02:00"
|
||||
},
|
||||
"front": {
|
||||
"goal": "Uczeń przechodzi od liniowego kursora z K\\&R 5.4 do wielokrotnego użycia tej samej areny: rozpoznaje nagłówek bloku, first-fit, split oraz dwustronne scalanie wolnych bloków w heap\\_4.",
|
||||
"scope": "Dwa małe modele C przygotowują przewidywanie. Główny replay uruchamia prawdziwe FreeRTOS-Kernel V11.3.0 heap\\_4 na RV32I/Hazard3 i dowodzi fragmentacji, pełnego scalenia, minimum-ever oraz kontrolowanego OOM."
|
||||
},
|
||||
"viewpoints": [
|
||||
{
|
||||
"id": "A1",
|
||||
"label": "CONTEXT",
|
||||
"subtitle": "from cursor to reusable heap",
|
||||
"status": "enabled"
|
||||
},
|
||||
{
|
||||
"id": "A2",
|
||||
"label": "STRUCTURE",
|
||||
"subtitle": "headers and address order",
|
||||
"status": "enabled"
|
||||
},
|
||||
{
|
||||
"id": "A3",
|
||||
"label": "DISPATCH",
|
||||
"subtitle": "not used by the allocator",
|
||||
"status": "unavailable",
|
||||
"reason": "heap_4 is called directly through pvPortMalloc and vPortFree; there is no callback or dispatch mechanism to explain."
|
||||
},
|
||||
{
|
||||
"id": "A4",
|
||||
"label": "APPLICATION",
|
||||
"subtitle": "experiment is already explicit",
|
||||
"status": "unavailable",
|
||||
"reason": "The concrete A/B/C allocation experiment is completely represented by A5 and its two runtime checkpoints."
|
||||
},
|
||||
{
|
||||
"id": "A5",
|
||||
"label": "FLOW",
|
||||
"subtitle": "allocate, fragment, coalesce",
|
||||
"status": "enabled"
|
||||
},
|
||||
{
|
||||
"id": "A6",
|
||||
"label": "STATE",
|
||||
"subtitle": "block list and statistics",
|
||||
"status": "enabled"
|
||||
},
|
||||
{
|
||||
"id": "A7",
|
||||
"label": "RUNTIME",
|
||||
"subtitle": "Hazard3 evidence",
|
||||
"status": "enabled"
|
||||
},
|
||||
{
|
||||
"id": "A8",
|
||||
"label": "PATTERNS",
|
||||
"subtitle": "mechanism, not a separate page",
|
||||
"status": "unavailable",
|
||||
"reason": "First-fit and the intrusive address-ordered free list are already proved in A2 and A5; a separate pattern page would duplicate them."
|
||||
}
|
||||
],
|
||||
"artifact": {
|
||||
"source": "src/tasks/task03_freertos_heap4.c",
|
||||
"elf": "build/task03_freertos_heap4/prog.elf",
|
||||
"image": "build/task03_freertos_heap4/prog.bin"
|
||||
},
|
||||
"strategies": [
|
||||
{
|
||||
"id": "code.model",
|
||||
"kind": "code",
|
||||
"prerequisites": [
|
||||
"K&R 5.4 linear allocator complete"
|
||||
],
|
||||
"layout": [
|
||||
"header",
|
||||
"payload",
|
||||
"remainder",
|
||||
"address-ordered list"
|
||||
],
|
||||
"commands": [
|
||||
"rg -n 'ModelBlock|align_up|insert_and_coalesce' src/tasks"
|
||||
],
|
||||
"expected_observations": [
|
||||
"requested size includes header and alignment",
|
||||
"free list is ordered by block address"
|
||||
],
|
||||
"assertions": [
|
||||
"payload begins after the header",
|
||||
"split preserves the total arena size"
|
||||
],
|
||||
"evidence_fields": [
|
||||
"code_ref",
|
||||
"header bytes",
|
||||
"wanted bytes",
|
||||
"block address"
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "code.heap4",
|
||||
"kind": "code",
|
||||
"prerequisites": [
|
||||
"FreeRTOS-Kernel V11.3.0 available"
|
||||
],
|
||||
"layout": [
|
||||
"ucHeap",
|
||||
"BlockLink_t",
|
||||
"xStart",
|
||||
"pxEnd"
|
||||
],
|
||||
"commands": [
|
||||
"rg -n 'BlockLink_t|prvInsertBlockIntoFreeList|pvPortMalloc|vPortFree' vendor/FreeRTOS-Kernel/portable/MemMang/heap_4.c"
|
||||
],
|
||||
"expected_observations": [
|
||||
"heap_4 keeps metadata inside the arena",
|
||||
"free blocks form one address-ordered intrusive list"
|
||||
],
|
||||
"assertions": [
|
||||
"allocated bit is stored in the size field",
|
||||
"xStart and pxEnd are sentinels"
|
||||
],
|
||||
"evidence_fields": [
|
||||
"symbol",
|
||||
"list link",
|
||||
"block size",
|
||||
"arena address"
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "run.fragmented",
|
||||
"kind": "run",
|
||||
"prerequisites": [
|
||||
"clean Hazard3 RAM",
|
||||
"task03 image loaded"
|
||||
],
|
||||
"layout": [
|
||||
"source",
|
||||
"free-list stats",
|
||||
"ucHeap memory",
|
||||
"registers"
|
||||
],
|
||||
"commands": [
|
||||
"break heap4_fragmented_checkpoint",
|
||||
"print g_fragmented_stats",
|
||||
"x/64bx ucHeap"
|
||||
],
|
||||
"expected_observations": [
|
||||
"A and C are free while B remains allocated",
|
||||
"the free list contains two blocks"
|
||||
],
|
||||
"assertions": [
|
||||
"xNumberOfFreeBlocks equals 2",
|
||||
"current free bytes exceed the largest free block"
|
||||
],
|
||||
"evidence_fields": [
|
||||
"free blocks",
|
||||
"largest block",
|
||||
"free bytes",
|
||||
"heap bytes"
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "run.coalesced",
|
||||
"kind": "run",
|
||||
"prerequisites": [
|
||||
"fragmented checkpoint reached"
|
||||
],
|
||||
"layout": [
|
||||
"final stats",
|
||||
"minimum-ever",
|
||||
"OOM hook",
|
||||
"PASS"
|
||||
],
|
||||
"commands": [
|
||||
"break task03_debug_checkpoint",
|
||||
"print g_final_stats",
|
||||
"print g_task03_pass"
|
||||
],
|
||||
"expected_observations": [
|
||||
"freeing B joins both neighbours",
|
||||
"the arena returns to one reusable block"
|
||||
],
|
||||
"assertions": [
|
||||
"final free equals initial free",
|
||||
"minimum-ever does not rise after free",
|
||||
"oversized allocation returns NULL and calls the hook once"
|
||||
],
|
||||
"evidence_fields": [
|
||||
"final free",
|
||||
"largest block",
|
||||
"minimum-ever",
|
||||
"OOM hook",
|
||||
"PASS"
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "code.identity",
|
||||
"kind": "code",
|
||||
"prerequisites": [
|
||||
"built ELF"
|
||||
],
|
||||
"layout": [
|
||||
"symbols",
|
||||
"sections",
|
||||
"artifact hashes"
|
||||
],
|
||||
"commands": [
|
||||
"tests/check_task03_elf.sh build/task03_freertos_heap4/prog.elf"
|
||||
],
|
||||
"expected_observations": [
|
||||
"upstream heap_4 symbols are linked",
|
||||
"checkpoint and ucHeap symbols remain observable"
|
||||
],
|
||||
"assertions": [
|
||||
"pvPortMalloc and vPortFree are present",
|
||||
"prvInsertBlockIntoFreeList is present"
|
||||
],
|
||||
"evidence_fields": [
|
||||
"source blob",
|
||||
"ELF SHA256",
|
||||
"image SHA256",
|
||||
"symbol"
|
||||
]
|
||||
}
|
||||
],
|
||||
"checkpoints": {
|
||||
"task01.fragmented": {
|
||||
"event_id": "E01",
|
||||
"stop": {
|
||||
"symbol": "heap4_fragmented_checkpoint",
|
||||
"offset": 0
|
||||
},
|
||||
"verify": {
|
||||
"expressions": [
|
||||
{
|
||||
"expr": "g_fragmented_stats.xNumberOfFreeBlocks",
|
||||
"equals": 2
|
||||
},
|
||||
{
|
||||
"expr": "g_initial_free > g_after_allocations",
|
||||
"equals": 1
|
||||
},
|
||||
{
|
||||
"expr": "g_allocations_aligned",
|
||||
"equals": 1
|
||||
}
|
||||
]
|
||||
}
|
||||
},
|
||||
"task01.coalesced": {
|
||||
"event_id": "E02",
|
||||
"stop": {
|
||||
"symbol": "task03_debug_checkpoint",
|
||||
"offset": 0
|
||||
},
|
||||
"verify": {
|
||||
"expressions": [
|
||||
{
|
||||
"expr": "g_final_stats.xNumberOfFreeBlocks",
|
||||
"equals": 1
|
||||
},
|
||||
{
|
||||
"expr": "g_final_free == g_initial_free",
|
||||
"equals": 1
|
||||
},
|
||||
{
|
||||
"expr": "g_oom_is_null",
|
||||
"equals": 1
|
||||
},
|
||||
{
|
||||
"expr": "g_task03_pass",
|
||||
"equals": 1
|
||||
}
|
||||
]
|
||||
}
|
||||
}
|
||||
},
|
||||
"sections": [
|
||||
{
|
||||
"id": "A1",
|
||||
"label": "CONTEXT",
|
||||
"title": "Od liniowego kursora do odzyskiwalnej areny",
|
||||
"order": 10,
|
||||
"orientation": "portrait",
|
||||
"description": "Aplikacja korzysta z publicznego API, heap_4 zarządza jedną areną, a Hazard3 pokazuje jej rzeczywisty stan.",
|
||||
"content_tex": "Kursor liniowy potrafi tylko rosnąć. heap_4 dodaje metadane i listę wolnych bloków, dzięki czemu zwolniona pamięć wraca do ponownego użycia.",
|
||||
"assets": [
|
||||
{
|
||||
"stem": "a1-context",
|
||||
"title": "A1 · granice odpowiedzialności heap_4",
|
||||
"caption": "A1 CONTEXT — od żądania aplikacji do rzeczywistych bajtów ucHeap.",
|
||||
"label": "fig:a1-context",
|
||||
"alt": "A1 · granice odpowiedzialności heap_4",
|
||||
"phases": [
|
||||
{
|
||||
"id": "boundary",
|
||||
"label": "APPLICATION / API / ALLOCATOR / TARGET",
|
||||
"steps": [
|
||||
{
|
||||
"id": "application",
|
||||
"number": 1,
|
||||
"label": "aplikacja żąda i zwalnia bajty",
|
||||
"mode": "CODE",
|
||||
"strategy_ref": "code.heap4",
|
||||
"svg_label": "01",
|
||||
"code_ref": "src/tasks/task03_freertos_heap4.c:78",
|
||||
"description": "Aplikacja zna wyłącznie publiczne API i wskaźniki payloadu.",
|
||||
"evidence": "trzy żądania 24, 40 i 16 bajtów"
|
||||
},
|
||||
{
|
||||
"id": "api",
|
||||
"number": 2,
|
||||
"label": "FreeRTOS wystawia malloc, free i statystyki",
|
||||
"mode": "CODE",
|
||||
"strategy_ref": "code.heap4",
|
||||
"svg_label": "02",
|
||||
"code_ref": "src/tasks/task03_freertos_heap4.c:90",
|
||||
"description": "API oddziela eksperyment od prywatnej listy bloków.",
|
||||
"evidence": "pvPortMalloc, vPortFree, vPortGetHeapStats"
|
||||
},
|
||||
{
|
||||
"id": "allocator",
|
||||
"number": 3,
|
||||
"label": "heap_4 zarządza blokami i kolejnością adresów",
|
||||
"mode": "CODE",
|
||||
"strategy_ref": "code.heap4",
|
||||
"svg_label": "03",
|
||||
"code_ref": "src/tasks/task03_freertos_heap4.c:70",
|
||||
"description": "Prywatny mechanizm wybiera, dzieli i scala wolne bloki.",
|
||||
"evidence": "reset i inicjalizacja listy"
|
||||
},
|
||||
{
|
||||
"id": "arena",
|
||||
"number": 4,
|
||||
"label": "ucHeap jest jedną ograniczoną areną",
|
||||
"mode": "CODE",
|
||||
"strategy_ref": "code.heap4",
|
||||
"svg_label": "04",
|
||||
"code_ref": "src/tasks/task03_freertos_heap4.c:11",
|
||||
"description": "Metadane i payload znajdują się w tej samej statycznej tablicy.",
|
||||
"evidence": "4096 bajtów, wyrównanie portu"
|
||||
},
|
||||
{
|
||||
"id": "target",
|
||||
"number": 5,
|
||||
"label": "Hazard3 ujawnia adresy i bajty",
|
||||
"mode": "CODE",
|
||||
"strategy_ref": "code.identity",
|
||||
"svg_label": "05",
|
||||
"code_ref": "tests/check_task03_elf.sh:8",
|
||||
"description": "ELF łączy kod, symbole i pamięć obserwowaną przez GDB.",
|
||||
"evidence": "ucHeap i checkpointy w symbolach ELF"
|
||||
}
|
||||
]
|
||||
}
|
||||
]
|
||||
}
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "A2",
|
||||
"label": "STRUCTURE",
|
||||
"title": "Nagłówek, payload i lista wolnych bloków",
|
||||
"order": 20,
|
||||
"orientation": "portrait",
|
||||
"description": "Każdy blok ma nagłówek, a tylko wolne bloki wykorzystują wskaźnik next do budowy listy uporządkowanej adresami.",
|
||||
"content_tex": "Rozmiar żądania rośnie o nagłówek i wyrównanie. Duży wolny blok może zostać rozdzielony na blok przydzielony i użyteczną resztę.",
|
||||
"assets": [
|
||||
{
|
||||
"stem": "a2-structure",
|
||||
"title": "A2 · struktura bloku i listy",
|
||||
"caption": "A2 STRUCTURE — metadane wewnątrz areny i adresowo uporządkowana lista.",
|
||||
"label": "fig:a2-structure",
|
||||
"alt": "A2 · struktura bloku i listy",
|
||||
"phases": [
|
||||
{
|
||||
"id": "blocks",
|
||||
"label": "HEADER / PAYLOAD / FREE LIST",
|
||||
"steps": [
|
||||
{
|
||||
"id": "header",
|
||||
"number": 1,
|
||||
"label": "nagłówek przechowuje next i size",
|
||||
"mode": "CODE",
|
||||
"strategy_ref": "code.model",
|
||||
"svg_label": "01",
|
||||
"code_ref": "src/tasks/heap4_model.h:11",
|
||||
"description": "ModelBlock pokazuje minimalny kontrakt metadanych heap_4.",
|
||||
"evidence": "dwa słowa metadanych"
|
||||
},
|
||||
{
|
||||
"id": "alignment",
|
||||
"number": 2,
|
||||
"label": "żądanie obejmuje nagłówek i wyrównanie",
|
||||
"mode": "CODE",
|
||||
"strategy_ref": "code.model",
|
||||
"svg_label": "02",
|
||||
"code_ref": "src/tasks/task01_first_fit_split.c:3",
|
||||
"description": "13 bajtów payloadu zajmuje 32 bajty całego bloku.",
|
||||
"evidence": "header=16, wanted=32"
|
||||
},
|
||||
{
|
||||
"id": "split",
|
||||
"number": 3,
|
||||
"label": "split pozostawia osobny wolny blok",
|
||||
"mode": "CODE",
|
||||
"strategy_ref": "code.model",
|
||||
"svg_label": "03",
|
||||
"code_ref": "src/tasks/task01_first_fit_split.c:43",
|
||||
"description": "Reszta zachowuje własny nagłówek i trafia na listę wolnych.",
|
||||
"evidence": "32 + 224 = 256"
|
||||
},
|
||||
{
|
||||
"id": "address-order",
|
||||
"number": 4,
|
||||
"label": "lista jest uporządkowana rosnącymi adresami",
|
||||
"mode": "CODE",
|
||||
"strategy_ref": "code.model",
|
||||
"svg_label": "04",
|
||||
"code_ref": "src/tasks/task02_address_order_coalesce.c:29",
|
||||
"description": "Pozycja w liście ujawnia bezpośredniego poprzednika i następnika.",
|
||||
"evidence": "previous < block < current"
|
||||
},
|
||||
{
|
||||
"id": "right-join",
|
||||
"number": 5,
|
||||
"label": "blok scala się z prawym sąsiadem",
|
||||
"mode": "CODE",
|
||||
"strategy_ref": "code.model",
|
||||
"svg_label": "05",
|
||||
"code_ref": "src/tasks/task02_address_order_coalesce.c:40",
|
||||
"description": "Koniec zwalnianego bloku równy adresowi current oznacza ciągłość.",
|
||||
"evidence": "block + size == current"
|
||||
},
|
||||
{
|
||||
"id": "left-join",
|
||||
"number": 6,
|
||||
"label": "wynik scala się z lewym sąsiadem",
|
||||
"mode": "CODE",
|
||||
"strategy_ref": "code.model",
|
||||
"svg_label": "06",
|
||||
"code_ref": "src/tasks/task02_address_order_coalesce.c:48",
|
||||
"description": "Drugi test domyka dwustronne scalanie w jeden blok.",
|
||||
"evidence": "previous + size == block"
|
||||
}
|
||||
]
|
||||
}
|
||||
]
|
||||
}
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "A5",
|
||||
"label": "FLOW",
|
||||
"title": "First-fit, fragmentacja i pełne scalenie",
|
||||
"order": 50,
|
||||
"orientation": "landscape",
|
||||
"description": "Jeden przebieg A/B/C przechodzi od pustej areny przez trzy przydziały i dwa wolne obszary do ponownie scalonego bloku.",
|
||||
"content_tex": "Uczeń najpierw przewiduje liczbę wolnych bloków. RUN odtwarza dwa stabilne stany: po zwolnieniu A i C oraz po zwolnieniu B.",
|
||||
"assets": [
|
||||
{
|
||||
"stem": "a5-flow",
|
||||
"title": "A5 · pełny przebieg heap_4",
|
||||
"caption": "A5 FLOW — inicjalizacja, A/B/C, fragmentacja, dwustronne scalenie i OOM.",
|
||||
"label": "fig:a5-flow",
|
||||
"alt": "A5 · pełny przebieg heap_4",
|
||||
"diagram_kind": "sequence",
|
||||
"phases": [
|
||||
{
|
||||
"id": "replay",
|
||||
"label": "ALLOCATE / FRAGMENT / COALESCE",
|
||||
"steps": [
|
||||
{
|
||||
"id": "reset",
|
||||
"number": 1,
|
||||
"label": "reset i inicjalizacja areny",
|
||||
"mode": "CODE",
|
||||
"strategy_ref": "code.heap4",
|
||||
"svg_label": "01",
|
||||
"code_ref": "src/tasks/task03_freertos_heap4.c:70",
|
||||
"description": "Pierwsze małe żądanie inicjalizuje sentinele i listę.",
|
||||
"evidence": "initial free = 4080"
|
||||
},
|
||||
{
|
||||
"id": "alloc-a",
|
||||
"number": 2,
|
||||
"label": "first-fit przydziela A",
|
||||
"mode": "CODE",
|
||||
"strategy_ref": "code.heap4",
|
||||
"svg_label": "02",
|
||||
"code_ref": "src/tasks/task03_freertos_heap4.c:78",
|
||||
"description": "Pierwszy wystarczający blok zostaje rozdzielony.",
|
||||
"evidence": "A payload = 24"
|
||||
},
|
||||
{
|
||||
"id": "alloc-bc",
|
||||
"number": 3,
|
||||
"label": "kolejne split tworzą B i C",
|
||||
"mode": "CODE",
|
||||
"strategy_ref": "code.heap4",
|
||||
"svg_label": "03",
|
||||
"code_ref": "src/tasks/task03_freertos_heap4.c:79",
|
||||
"description": "B i C zajmują kolejne fragmenty tego samego wolnego bloku.",
|
||||
"evidence": "after allocations = 3952"
|
||||
},
|
||||
{
|
||||
"id": "free-ac",
|
||||
"number": 4,
|
||||
"label": "zwolnij A i C, pozostaw B",
|
||||
"mode": "CODE",
|
||||
"strategy_ref": "code.heap4",
|
||||
"svg_label": "04",
|
||||
"code_ref": "src/tasks/task03_freertos_heap4.c:88",
|
||||
"description": "C scala się z prawą resztą, ale B oddziela ją od A.",
|
||||
"evidence": "dwa wolne bloki"
|
||||
},
|
||||
{
|
||||
"id": "fragmented",
|
||||
"number": 5,
|
||||
"label": "checkpoint fragmentacji",
|
||||
"mode": "RUN",
|
||||
"event_id": "E01",
|
||||
"strategy_ref": "run.fragmented",
|
||||
"svg_label": "05",
|
||||
"code_ref": "src/tasks/task03_freertos_heap4.c:91",
|
||||
"snapshot_ref": "task01.fragmented",
|
||||
"description": "GDB zatrzymuje program przy dwóch wolnych blokach.",
|
||||
"evidence": "xNumberOfFreeBlocks = 2"
|
||||
},
|
||||
{
|
||||
"id": "free-b",
|
||||
"number": 6,
|
||||
"label": "zwolnij B między dwoma sąsiadami",
|
||||
"mode": "CODE",
|
||||
"strategy_ref": "code.heap4",
|
||||
"svg_label": "06",
|
||||
"code_ref": "src/tasks/task03_freertos_heap4.c:93",
|
||||
"description": "Wstawienie adresowe umożliwia dwa testy ciągłości.",
|
||||
"evidence": "A + B + C + reszta są ciągłe"
|
||||
},
|
||||
{
|
||||
"id": "coalesced",
|
||||
"number": 7,
|
||||
"label": "arena wraca do jednego bloku",
|
||||
"mode": "RUN",
|
||||
"event_id": "E02",
|
||||
"strategy_ref": "run.coalesced",
|
||||
"svg_label": "07",
|
||||
"code_ref": "src/tasks/task03_freertos_heap4.c:96",
|
||||
"snapshot_ref": "task01.coalesced",
|
||||
"description": "Finalne statystyki dowodzą pełnego odzyskania areny.",
|
||||
"evidence": "final free = initial free; blocks = 1"
|
||||
},
|
||||
{
|
||||
"id": "oom",
|
||||
"number": 8,
|
||||
"label": "zbyt duże żądanie kończy się NULL",
|
||||
"mode": "CODE",
|
||||
"strategy_ref": "code.heap4",
|
||||
"svg_label": "08",
|
||||
"code_ref": "src/tasks/task03_freertos_heap4.c:98",
|
||||
"description": "Kontrolowany OOM nie narusza listy i wywołuje hook dokładnie raz.",
|
||||
"evidence": "NULL, hooks=1, asserts=0"
|
||||
}
|
||||
]
|
||||
}
|
||||
]
|
||||
}
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "A6",
|
||||
"label": "STATE",
|
||||
"title": "Stan bloku a stan statystyk",
|
||||
"order": 60,
|
||||
"orientation": "portrait",
|
||||
"description": "Bieżąca liczba wolnych bajtów może rosnąć po free, ale minimum-ever pozostaje historycznym minimum.",
|
||||
"content_tex": "Fragmentacja to nie tylko suma wolnych bajtów. O możliwości przydziału decyduje także największy pojedynczy blok.",
|
||||
"assets": [
|
||||
{
|
||||
"stem": "a6-state",
|
||||
"title": "A6 · stany bloków i liczników",
|
||||
"caption": "A6 STATE — wolny, przydzielony, rozdzielony, scalony oraz minimum-ever.",
|
||||
"label": "fig:a6-state",
|
||||
"alt": "A6 · stany bloków i liczników",
|
||||
"phases": [
|
||||
{
|
||||
"id": "state",
|
||||
"label": "BLOCK STATE / HEAP STATS",
|
||||
"steps": [
|
||||
{
|
||||
"id": "free",
|
||||
"number": 1,
|
||||
"label": "wolny blok należy do listy",
|
||||
"mode": "CODE",
|
||||
"strategy_ref": "code.heap4",
|
||||
"svg_label": "01",
|
||||
"code_ref": "src/tasks/task03_freertos_heap4.c:70",
|
||||
"description": "Stan początkowy zawiera jeden największy wolny blok.",
|
||||
"evidence": "initial free = largest free"
|
||||
},
|
||||
{
|
||||
"id": "allocated",
|
||||
"number": 2,
|
||||
"label": "przydzielony blok znika z listy wolnych",
|
||||
"mode": "CODE",
|
||||
"strategy_ref": "code.heap4",
|
||||
"svg_label": "02",
|
||||
"code_ref": "src/tasks/task03_freertos_heap4.c:78",
|
||||
"description": "Payload jest wyrównany, a bieżąca wolna pamięć maleje.",
|
||||
"evidence": "all payload pointers aligned"
|
||||
},
|
||||
{
|
||||
"id": "fragmented-state",
|
||||
"number": 3,
|
||||
"label": "dwa wolne bloki nie są jednym dużym blokiem",
|
||||
"mode": "RUN",
|
||||
"event_id": "E01",
|
||||
"strategy_ref": "run.fragmented",
|
||||
"svg_label": "03",
|
||||
"code_ref": "src/tasks/task03_freertos_heap4.c:90",
|
||||
"snapshot_ref": "task01.fragmented",
|
||||
"description": "Suma wolnego miejsca nie gwarantuje jednego dużego przydziału.",
|
||||
"evidence": "free blocks = 2"
|
||||
},
|
||||
{
|
||||
"id": "coalesced-state",
|
||||
"number": 4,
|
||||
"label": "scalenie przywraca jeden największy blok",
|
||||
"mode": "RUN",
|
||||
"event_id": "E02",
|
||||
"strategy_ref": "run.coalesced",
|
||||
"svg_label": "04",
|
||||
"code_ref": "src/tasks/task03_freertos_heap4.c:94",
|
||||
"snapshot_ref": "task01.coalesced",
|
||||
"description": "Current free i largest wracają do wartości początkowej.",
|
||||
"evidence": "free blocks = 1"
|
||||
},
|
||||
{
|
||||
"id": "minimum-ever",
|
||||
"number": 5,
|
||||
"label": "minimum-ever zachowuje najniższy poziom",
|
||||
"mode": "CODE",
|
||||
"strategy_ref": "code.heap4",
|
||||
"svg_label": "05",
|
||||
"code_ref": "src/tasks/task03_freertos_heap4.c:95",
|
||||
"description": "Historyczne minimum nie zwiększa się po odzyskaniu pamięci.",
|
||||
"evidence": "minimum-ever <= after allocations"
|
||||
}
|
||||
]
|
||||
}
|
||||
]
|
||||
}
|
||||
]
|
||||
},
|
||||
{
|
||||
"id": "A7",
|
||||
"label": "RUNTIME",
|
||||
"title": "Dowód w Hazard3 i ELF",
|
||||
"order": 70,
|
||||
"orientation": "landscape",
|
||||
"description": "Ten sam artefakt łączy źródło, symbole ELF, dwa checkpointy, pamięć ucHeap i końcowe asercje.",
|
||||
"content_tex": "Snapshot jest dowodem tylko wtedy, gdy zawiera tożsamość artefaktu, pozycję programu i wartości, które rozstrzygają hipotezę.",
|
||||
"assets": [
|
||||
{
|
||||
"stem": "a7-runtime",
|
||||
"title": "A7 · dowód runtime heap_4",
|
||||
"caption": "A7 RUNTIME — kod, ELF, checkpoint, pamięć i statystyki jednego przebiegu.",
|
||||
"label": "fig:a7-runtime",
|
||||
"alt": "A7 · dowód runtime heap_4",
|
||||
"phases": [
|
||||
{
|
||||
"id": "evidence",
|
||||
"label": "ARTIFACT / CHECKPOINT / MEMORY / ASSERTION",
|
||||
"steps": [
|
||||
{
|
||||
"id": "source",
|
||||
"number": 1,
|
||||
"label": "źródło wskazuje eksperyment A/B/C",
|
||||
"mode": "CODE",
|
||||
"strategy_ref": "code.identity",
|
||||
"svg_label": "01",
|
||||
"code_ref": "src/tasks/task03_freertos_heap4.c:62",
|
||||
"description": "Blob źródła jest częścią tożsamości karty.",
|
||||
"evidence": "source git blob"
|
||||
},
|
||||
{
|
||||
"id": "elf",
|
||||
"number": 2,
|
||||
"label": "ELF zawiera prawdziwe symbole heap_4",
|
||||
"mode": "CODE",
|
||||
"strategy_ref": "code.identity",
|
||||
"svg_label": "02",
|
||||
"code_ref": "tests/check_task03_elf.sh:8",
|
||||
"description": "Test ABI odrzuca atrapę bez pvPortMalloc, vPortFree i ucHeap.",
|
||||
"evidence": "upstream symbols present"
|
||||
},
|
||||
{
|
||||
"id": "fragmented-runtime",
|
||||
"number": 3,
|
||||
"label": "checkpoint pokazuje dwa wolne bloki",
|
||||
"mode": "RUN",
|
||||
"event_id": "E01",
|
||||
"strategy_ref": "run.fragmented",
|
||||
"svg_label": "03",
|
||||
"code_ref": "src/tasks/task03_freertos_heap4.c:91",
|
||||
"snapshot_ref": "task01.fragmented",
|
||||
"description": "Neovim, GDB i pamięć zatrzymują się na tym samym stanie.",
|
||||
"evidence": "blocks=2 and aligned=1"
|
||||
},
|
||||
{
|
||||
"id": "memory",
|
||||
"number": 4,
|
||||
"label": "ucHeap ujawnia nagłówki i payload",
|
||||
"mode": "CODE",
|
||||
"strategy_ref": "code.heap4",
|
||||
"svg_label": "04",
|
||||
"code_ref": "src/tasks/task03_freertos_heap4.c:11",
|
||||
"description": "Widok bajtów łączy diagram z realnym układem areny.",
|
||||
"evidence": "aligned arena and in-band metadata"
|
||||
},
|
||||
{
|
||||
"id": "final-runtime",
|
||||
"number": 5,
|
||||
"label": "checkpoint końcowy dowodzi odzyskania",
|
||||
"mode": "RUN",
|
||||
"event_id": "E02",
|
||||
"strategy_ref": "run.coalesced",
|
||||
"svg_label": "05",
|
||||
"code_ref": "src/tasks/task03_freertos_heap4.c:111",
|
||||
"snapshot_ref": "task01.coalesced",
|
||||
"description": "Jedna ramka łączy stats, OOM, hook i PASS.",
|
||||
"evidence": "final=initial, blocks=1, pass=1"
|
||||
}
|
||||
]
|
||||
}
|
||||
]
|
||||
}
|
||||
]
|
||||
}
|
||||
],
|
||||
"learning": {
|
||||
"model_label": "Model bloków heap_4",
|
||||
"model": "Uczeń wyjaśnia nagłówek, wyrównanie, first-fit, split, adresową listę wolnych bloków i dwustronne coalescing.",
|
||||
"replay_label": "Fragmentacja i odzyskanie areny",
|
||||
"replay": "Uczeń odtwarza dwa checkpointy Hazard3 i odróżnia current free, largest free block oraz minimum-ever.",
|
||||
"criterion": "Model 13 -> 32 bajty; poprawna predykcja dwóch wolnych bloków po free(A,C) i jednego po free(B); final free = initial free; minimum-ever nie rośnie; OOM zwraca NULL; PASS=1.",
|
||||
"requirement": "Analiza i weryfikacja mechaniki dynamicznej alokacji heap_4 w FreeRTOS C na RV32I/Hazard3."
|
||||
},
|
||||
"task": {
|
||||
"short_label": "mechanika heap_4",
|
||||
"title": "Predict and prove reusable heap_4 blocks",
|
||||
"prompt_tex": "Przewidź układ bloków po alloc A/B/C, następnie po free(A,C) i free(B). Odtwórz oba checkpointy i udowodnij, że arena została scalona bez utraty minimum-ever.",
|
||||
"conclusion_tex": "heap\\_4 odzyskuje pamięć dzięki metadanym w arenie, adresowo uporządkowanej liście i scalaniu sąsiadów. Suma wolnych bajtów nie zastępuje informacji o największym bloku, a minimum-ever jest historią, nie bieżącym stanem.",
|
||||
"flow": [
|
||||
{
|
||||
"kind": "block",
|
||||
"id": "predict",
|
||||
"title": "A — przewidywanie",
|
||||
"content_tex": "Przejdź przez model nagłówka, split i porządek adresowy przed uruchomieniem prawdziwego heap\\_4.",
|
||||
"steps": [
|
||||
{
|
||||
"id": "size",
|
||||
"title": "Policz rozmiar bloku.",
|
||||
"content_tex": "Dodaj nagłówek do 13 bajtów i wyrównaj wynik do ośmiu."
|
||||
},
|
||||
{
|
||||
"id": "list",
|
||||
"title": "Narysuj listę po free(A,C).",
|
||||
"content_tex": "Zaznacz, dlaczego przydzielony B rozdziela dwa wolne obszary."
|
||||
}
|
||||
]
|
||||
},
|
||||
{
|
||||
"kind": "block",
|
||||
"id": "replay",
|
||||
"title": "B — replay Hazard3",
|
||||
"content_tex": "Powiąż diagram z dwoma deterministycznymi checkpointami.",
|
||||
"steps": [
|
||||
{
|
||||
"id": "fragmented",
|
||||
"title": "Sprawdź E01.",
|
||||
"content_tex": "Porównaj liczbę wolnych bloków, największy blok i bieżące wolne bajty."
|
||||
},
|
||||
{
|
||||
"id": "coalesced",
|
||||
"title": "Sprawdź E02.",
|
||||
"content_tex": "Udowodnij pełne scalenie, zachowanie minimum-ever i kontrolowany OOM."
|
||||
}
|
||||
]
|
||||
},
|
||||
{
|
||||
"kind": "exercise",
|
||||
"id": "fragmentation",
|
||||
"title": "Ćwiczenie — ta sama suma, inna użyteczność",
|
||||
"prompt_tex": "Zaproponuj dwa układy wolnych bloków o tej samej sumie bajtów, ale tylko jeden zdolny obsłużyć wskazane duże żądanie. Uzasadnij odpowiedź przez largest-free-block.",
|
||||
"evidence_tex": "Dwa diagramy listy, suma wolnych bajtów, rozmiar największego bloku i wynik pvPortMalloc.",
|
||||
"criterion": "Uczeń nie utożsamia sumy wolnej pamięci z możliwością pojedynczego dużego przydziału.",
|
||||
"based_on": [
|
||||
"predict",
|
||||
"replay"
|
||||
]
|
||||
}
|
||||
]
|
||||
}
|
||||
}
|
||||
Reference in New Issue
Block a user