commit 3937199dd5cfdc1395ed53dace72466c706620a2 Author: M. Pabiszczak <2+mpabi@noreply.zsl-gitea.mpabi.pl> Date: Mon Jul 20 08:25:17 2026 +0200 publish: FC12 runtime diagnostics v00.01 diff --git a/json/card_source.json b/json/card_source.json new file mode 100644 index 0000000..10e972f --- /dev/null +++ b/json/card_source.json @@ -0,0 +1,1342 @@ +{ + "$schema": "../../../tools/card-layouts/schemas/card-source.schema.json", + "schema": "esc-card-source.v1", + "card": { + "id": "mpabi-freertos-c-12-diagnostics", + "series": "freertos-c", + "series_title": "FreeRTOS C", + "number": "12", + "count": "15", + "slug": "diagnostics", + "title": "Assertions, hooks and runtime diagnostics", + "topic": "healthy evidence and four isolated expected-fail fixtures", + "project": "Freestanding C nad FreeRTOS", + "subject": "Informatyka", + "level": "Rok 2 · L12 · RV32I/Hazard3", + "revision_date": "2026-07-19T00:00:00+02:00", + "status": "Gotowa", + "version": "v00.01", + "uuid": "b059cd72-9dac-523e-8658-2be46dd4558d", + "author": "M. Pabiszczak", + "year": "2026" + }, + "generated": { + "tex": "doc/generated/main.tex", + "html": "web/index.html", + "html_css": "web/style.css", + "html_tree_inspector": false, + "react_app": true + }, + "render_dictionary": false, + "viewpoints": [ + { + "id": "A1", + "label": "CONTEXT", + "subtitle": "diagnostic boundaries", + "status": "enabled", + "target_label": "fig:a1-context" + }, + { + "id": "A2", + "label": "STRUCTURE", + "subtitle": "evidence and fault records", + "status": "enabled", + "target_label": "fig:a2-structure" + }, + { + "id": "A3", + "label": "DISPATCH", + "subtitle": "raw hook signatures", + "status": "unavailable", + "reason": "Raw C hook signatures are explicit and add no separate binding model." + }, + { + "id": "A4", + "label": "APPLICATION", + "subtitle": "single diagnostic topology", + "status": "unavailable", + "reason": "The application boundary and object topology are already distinct in A1 and A2." + }, + { + "id": "A5", + "label": "FLOW", + "subtitle": "healthy E01-E06", + "status": "enabled", + "target_label": "fig:a5-flow" + }, + { + "id": "A6", + "label": "STATE", + "subtitle": "one terminal per run", + "status": "enabled", + "target_label": "fig:a6-state" + }, + { + "id": "A7", + "label": "RUNTIME", + "subtitle": "stack, tasks and identity", + "status": "enabled", + "target_label": "fig:a7-runtime" + }, + { + "id": "A8", + "label": "PATTERNS", + "subtitle": "no new pattern", + "status": "unavailable", + "reason": "This card teaches diagnostic contracts rather than a reusable structural pattern." + } + ], + "debug_strategies": { + "code.contracts": { + "id": "code.contracts", + "kind": "code", + "action": "open", + "expected_observations": [ + "three kernel diagnostics enabled", + "bounded records and static stacks" + ], + "assertions": [ + "hooks do not allocate or block", + "fixture selector is set after startup" + ], + "evidence_fields": [ + "config macro", + "hook signature", + "record field", + "code_ref" + ], + "prerequisites": [ + "FC01-FC11 complete" + ], + "layout": [ + "FreeRTOSConfig", + "records", + "main fixture switch" + ], + "commands": [ + "rg -n 'configASSERT|MALLOC_FAILED|STACK_OVERFLOW|g_fc12_fixture' include src scripts" + ] + }, + "run.healthy": { + "id": "run.healthy", + "kind": "run", + "action": "replay", + "expected_observations": [ + "E01-E06 in order", + "heartbeat in deadline", + "healthy PASS" + ], + "assertions": [ + "watermark is bounded", + "task count is at least three", + "task SP values differ" + ], + "evidence_fields": [ + "event", + "tick", + "HWM", + "task count", + "SP", + "digest" + ], + "prerequisites": [ + "clean Hazard3 RAM", + "fixture 0" + ], + "layout": [ + "bounded trace", + "experiment", + "terminal" + ], + "commands": [ + "make sim", + "print g_fc12", + "print g_fc12_events" + ] + }, + "run.fixtures": { + "id": "run.fixtures", + "kind": "run", + "action": "replay", + "expected_observations": [ + "one expected terminal", + "committed fault record", + "no healthy PASS" + ], + "assertions": [ + "selector survives because it is set at main", + "fixture and hook numbers match" + ], + "evidence_fields": [ + "fixture", + "hook", + "line", + "task", + "SP", + "committed" + ], + "prerequisites": [ + "GDB stop at main", + "one selector from 1 to 4" + ], + "layout": [ + "fixture branch", + "hook", + "fault record" + ], + "commands": [ + "make sim-fixtures", + "break main", + "set variable g_fc12_fixture=1" + ] + }, + "code.identity": { + "id": "code.identity", + "kind": "code", + "action": "open", + "expected_observations": [ + "required C symbols in ELF", + "source and artifact hashes are pinned" + ], + "assertions": [ + "no C++ or unwind metadata", + "diagnostic boundaries remain visible" + ], + "evidence_fields": [ + "source blob", + "ELF SHA256", + "image SHA256", + "symbol" + ], + "prerequisites": [ + "built artifact" + ], + "layout": [ + "ABI", + "artifact", + "symbols" + ], + "commands": [ + "make check-abi", + "riscv64-unknown-elf-nm build/task01_diagnostics/prog.elf" + ] + }, + "run.identity": { + "id": "run.identity", + "kind": "run", + "action": "replay", + "expected_observations": [ + "required C symbols in ELF", + "three identical healthy logs" + ], + "assertions": [ + "no C++ or unwind metadata", + "source and artifact hashes are pinned" + ], + "evidence_fields": [ + "source blob", + "ELF SHA256", + "image SHA256", + "digest" + ], + "prerequisites": [ + "built artifact" + ], + "layout": [ + "ABI", + "artifact", + "three processes" + ], + "commands": [ + "make check-abi", + "make check-determinism" + ] + } + }, + "template": "templates/karta-klasyczna.json", + "title_block": { + "category": "KARTA PRACY · INFORMATYKA", + "prepared_by": "M. Pabiszczak", + "prepared_on": "2026-07-19T00:00:00+02:00", + "title": "Assertions, hooks and runtime diagnostics", + "url": "https://dce7fb9d-7b2f-5d49-96a2-3a30d3070b84.mpabi.pl/c3027314-85a4-5e4a-af13-0939c7467a62", + "repository_url": "https://zsl-gitea.mpabi.pl/edu-freertos-c/lab-rv32i-freertos-c-diagnostics", + "url_host_uuid": "dce7fb9d-7b2f-5d49-96a2-3a30d3070b84", + "url_domain": "mpabi.pl", + "doc_uuid": "c3027314-85a4-5e4a-af13-0939c7467a62", + "revision": "v00.01", + "issued_on": "2026-07-19T00:00:00+02:00", + "series": "FREERTOS-C-12", + "document_type": "karta pracy", + "tool": "card-layouts", + "show_qr": true, + "show_repository_qr": true, + "height_cm": 2.6, + "repeat_on_every_page": true, + "replace_front_matter": true + }, + "front_page_scope": { + "title": "Cel karty", + "content_tex": "Uczeń rozróżnia asercję, hook kernela i monitor aplikacyjny oraz zachowuje wystarczający dowód, aby wskazać zamierzony terminal bez fałszywego PASS.", + "scope_title": "Zakres karty", + "scope_content_tex": "Jeden zdrowy przebieg mierzy heartbeat, stack high-water mark, snapshot tasków i dwa stosy. Cztery izolowane fixture'y dowodzą ścieżek ASSERT, MALLOC, STACK i DEADLINE.", + "scope_table": { + "headers": [ + "Lekcja", + "Task", + "Najważniejsza idea", + "Priorytet", + "Status", + "Version" + ], + "rows": [ + { + "chapter": "FC12", + "task": "Task01", + "idea_tex": "healthy evidence and four isolated expected-fail fixtures", + "priority": "główny", + "status": "ready", + "version": "v00.01", + "key": true + } + ] + } + }, + "side_margin_tree_layout": { + "columns": [ + { + "id": "zawodowe", + "label": "TECH", + "side": "left", + "tree": "WE -> EK -> KW", + "description": "Dowody runtime." + }, + { + "id": "ogolne", + "label": "OG", + "side": "right", + "tree": "WE -> EN -> KW", + "description": "Model FreeRTOS C." + } + ] + }, + "learning_effects": { + "FC12.EN01": { + "bloom_level": "Analiza", + "label": "Diagnostic boundaries", + "text": "Uczeń rozróżnia asercję, hook kernela, historyczny watermark i monitor deadline.", + "assessment_criteria": [ + "FC12.KW01" + ] + }, + "FC12.EK01": { + "bloom_level": "Zastosowanie", + "label": "Healthy and fault replay", + "text": "Uczeń odtwarza E01-E10 i wiąże każdy terminal z zatwierdzonym rekordem.", + "assessment_criteria": [ + "FC12.KW01" + ] + } + }, + "assessment_criteria": { + "FC12.KW01": { + "text": "Healthy PASS; four intended fault terminals; bounded evidence; deterministic artifact identity.", + "learning_effects": [ + "FC12.EN01", + "FC12.EK01" + ] + } + }, + "educational_requirements": { + "FC12.WE01": { + "text": "Diagnozowanie stanu i kontrolowanych awarii aplikacji FreeRTOS C.", + "label": "healthy evidence and four isolated expected-fail fixtures", + "learning_effects": [ + "FC12.EN01", + "FC12.EK01" + ], + "learning_tree": { + "schema": "we-learning-tree.v1", + "policy": "Każda aktywna kotwica wskazuje kod lub checkpoint.", + "ogolne": [ + { + "effect_ref": "FC12.EN01", + "display": "EN LOCAL RTOS.12", + "source": "LOCAL", + "official": "RTOS", + "local": "12", + "kind": "EN", + "tree_id": "FC12.WE01.OG.LOCAL.RTOS.12", + "text": "Uczeń rozróżnia asercję, hook kernela, historyczny watermark i monitor deadline.", + "kw": [ + { + "criterion_ref": "FC12.KW01", + "display": "KW LOCAL RTOS.12", + "source": "LOCAL", + "kind": "KW", + "official": "RTOS", + "local": "12", + "text": "Łączy kod, diagram i zweryfikowany dowód." + } + ] + } + ], + "zawodowe": [ + { + "effect_ref": "FC12.EK01", + "display": "EK LOCAL RTOS.12", + "source": "LOCAL", + "official": "RTOS", + "local": "12", + "kind": "EK", + "tree_id": "FC12.WE01.TECH.LOCAL.RTOS.12", + "text": "Uczeń odtwarza E01-E10 i wiąże każdy terminal z zatwierdzonym rekordem.", + "kw": [ + { + "criterion_ref": "FC12.KW01", + "display": "KW LOCAL RTOS.12", + "source": "LOCAL", + "kind": "KW", + "official": "RTOS", + "local": "12", + "text": "Łączy kod, diagram i zweryfikowany dowód." + } + ] + } + ] + } + } + }, + "debug_checkpoints": { + "schema": "stem-debug-checkpoints.v1", + "semantics": "deterministic-replay", + "artifact": { + "source": "src/tasks/task01_diagnostics.c", + "source_git_blob": "6b8adec8d639109cf128b069c1e470a5b40688a0", + "elf": "build/task01_diagnostics/prog.elf", + "hazard3_elf_sha256": "167e558385843f8d45110de5a22496251828b44bcac37939689c42038b1b1427", + "hazard3_image": "build/task01_diagnostics/prog.bin", + "hazard3_image_sha256": "21b95ac5978140ca6e3b962c9b3715b0bfab76caa862fdd163f24c818a9f9e9e" + }, + "targets": { + "hazard3-sim": { + "adapter": "hazard3-reset-load-replay.v1", + "baseline": "restart-backend", + "clean_ram": true + } + }, + "items": { + "task01.configured": { + "event_id": "E01", + "stop": { + "symbol": "fc12_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 1" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc12_event_count", + "equals": 1 + }, + { + "expr": "g_fc12_events[0].value", + "equals": 2 + } + ] + } + }, + "task01.worker-ran": { + "event_id": "E02", + "stop": { + "symbol": "fc12_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 2" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc12_events[1].value", + "equals": 21 + } + ] + } + }, + "task01.heartbeat": { + "event_id": "E03", + "stop": { + "symbol": "fc12_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 3" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc12.heartbeat", + "equals": 1 + } + ] + } + }, + "task01.watermark": { + "event_id": "E04", + "stop": { + "symbol": "fc12_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 4" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc12.high_water > 0 && g_fc12.high_water < 256", + "equals": 1 + } + ] + } + }, + "task01.snapshot": { + "event_id": "E05", + "stop": { + "symbol": "fc12_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 5" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc12.task_count >= 3", + "equals": 1 + } + ] + } + }, + "task01.pass": { + "event_id": "E06", + "stop": { + "symbol": "fc12_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 6" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc12_pass", + "equals": 1 + }, + { + "expr": "g_fc12_event_count", + "equals": 6 + }, + { + "expr": "g_fc12.worker_sp != g_fc12.diagnostics_sp", + "equals": 1 + } + ] + } + }, + "task01.assert-hook": { + "event_id": "E07", + "stop": { + "symbol": "fc12_fault_committed", + "offset": 0, + "condition": "$a0 == 1" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc12_fault.fixture", + "equals": 1 + }, + { + "expr": "g_fc12_fault.hook", + "equals": 1 + }, + { + "expr": "g_fc12_fault.committed == 0xFC12FA17", + "equals": 1 + } + ] + } + }, + "task01.malloc-hook": { + "event_id": "E08", + "stop": { + "symbol": "fc12_fault_committed", + "offset": 0, + "condition": "$a0 == 2" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc12_fault.fixture", + "equals": 2 + }, + { + "expr": "g_fc12_fault.hook", + "equals": 2 + }, + { + "expr": "g_fc12_fault.committed == 0xFC12FA17", + "equals": 1 + } + ] + } + }, + "task01.stack-hook": { + "event_id": "E09", + "stop": { + "symbol": "fc12_fault_committed", + "offset": 0, + "condition": "$a0 == 3" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc12_fault.fixture", + "equals": 3 + }, + { + "expr": "g_fc12_fault.hook", + "equals": 3 + }, + { + "expr": "g_fc12_fault.sp != 0", + "equals": 1 + } + ] + } + }, + "task01.deadline-hook": { + "event_id": "E10", + "stop": { + "symbol": "fc12_fault_committed", + "offset": 0, + "condition": "$a0 == 4" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc12_fault.fixture", + "equals": 4 + }, + { + "expr": "g_fc12_fault.hook", + "equals": 4 + }, + { + "expr": "g_fc12_fault.sp != 0", + "equals": 1 + } + ] + } + } + } + }, + "sections": [ + { + "title": "A1 — Diagnostic boundaries", + "order": 10, + "content_kind": "prose", + "asset_page_mode": "one-per-page", + "page_orientation": "portrait", + "content_tex": "The application measures health; the kernel calls bounded hooks; the simulator preserves source, ELF and terminal evidence.", + "assets": [ + { + "path": "assets/a1-context.png", + "html_path": "assets/a1-context.svg", + "source_path": "assets/a1-context.puml", + "caption": "A1 CONTEXT — application, kernel hooks and evidence.", + "label": "fig:a1-context", + "alt": "A1 · diagnostic boundaries", + "kind": "diagram", + "width": 1.0, + "page_grid": { + "columns": 1, + "rows": 1, + "page_width": 660, + "page_height": 760, + "overview": true, + "step_tiles": { + "application": 1, + "kernel": 1, + "fixtures": 1, + "hazard3": 1, + "committed": 1 + } + }, + "interactive": { + "kind": "uml-class", + "storage_key": "fc12-a1-context", + "title": "A1 · diagnostic boundaries", + "task": { + "id": "task01", + "label": "Task01 · healthy run and fault fixtures" + }, + "block": { + "id": "a1", + "label": "A1 CONTEXT", + "description": "Application monitoring, kernel hooks and Hazard3 evidence have explicit responsibilities." + }, + "phases": [ + { + "id": "boundaries", + "label": "DIAGNOSTIC BOUNDARIES", + "steps": [ + { + "id": "application", + "number": 1, + "label": "application owns heartbeat policy", + "mode": "CODE", + "strategy_ref": "code.contracts", + "svg_label": "01", + "code_ref": "src/tasks/task01_diagnostics.c:162", + "description": "application owns heartbeat policy", + "evidence": "bounded deadline monitor" + }, + { + "id": "kernel", + "number": 2, + "label": "kernel owns assert and hook dispatch", + "mode": "CODE", + "strategy_ref": "code.contracts", + "svg_label": "02", + "code_ref": "include/FreeRTOSConfig.h:20", + "description": "kernel owns assert and hook dispatch", + "evidence": "three configured diagnostics" + }, + { + "id": "fixtures", + "number": 3, + "label": "fixtures are isolated at main", + "mode": "CODE", + "strategy_ref": "code.contracts", + "svg_label": "03", + "code_ref": "src/tasks/task01_diagnostics.c:227", + "description": "fixtures are isolated at main", + "evidence": "selector 0..4" + }, + { + "id": "hazard3", + "number": 4, + "label": "Hazard3 runs one clean image", + "mode": "CODE", + "strategy_ref": "code.contracts", + "svg_label": "04", + "code_ref": "scripts/run_fixtures.sh:14", + "description": "Hazard3 runs one clean image", + "evidence": "GDB selects after C startup" + }, + { + "id": "committed", + "number": 5, + "label": "evidence is committed before PASS", + "mode": "RUN", + "event_id": "E06", + "strategy_ref": "run.healthy", + "svg_label": "05", + "code_ref": "src/tasks/task01_diagnostics.c:192", + "snapshot_ref": "task01.pass", + "description": "evidence is committed before PASS", + "evidence": "six ordered events" + } + ] + } + ] + } + } + ] + }, + { + "title": "A2 — Evidence and hook contracts", + "order": 20, + "content_kind": "prose", + "asset_page_mode": "one-per-page", + "page_orientation": "portrait", + "content_tex": "The experiment owns task handles and health values; evidence records form a bounded trace; a fault record freezes fixture, hook, line/task and SP.", + "assets": [ + { + "path": "assets/a2-structure.png", + "html_path": "assets/a2-structure.svg", + "source_path": "assets/a2-structure.puml", + "caption": "A2 STRUCTURE — experiment, trace, fault and static storage.", + "label": "fig:a2-structure", + "alt": "A2 · evidence records", + "kind": "diagram", + "width": 1.0, + "page_grid": { + "columns": 1, + "rows": 1, + "page_width": 660, + "page_height": 760, + "overview": true, + "step_tiles": { + "experiment": 1, + "events": 1, + "fault": 1, + "storage": 1, + "fault-record": 1 + } + }, + "interactive": { + "kind": "uml-class", + "storage_key": "fc12-a2-structure", + "title": "A2 · evidence records", + "task": { + "id": "task01", + "label": "Task01 · healthy run and fault fixtures" + }, + "block": { + "id": "a2", + "label": "A2 STRUCTURE", + "description": "Healthy measurements and terminal faults use separate, commit-last records." + }, + "phases": [ + { + "id": "records", + "label": "RECORDS AND STORAGE", + "steps": [ + { + "id": "experiment", + "number": 1, + "label": "DiagnosticsExperiment owns health data", + "mode": "CODE", + "strategy_ref": "code.contracts", + "svg_label": "01", + "code_ref": "include/task01_diagnostics.h:33", + "description": "DiagnosticsExperiment owns health data", + "evidence": "handles, ticks, HWM and SP" + }, + { + "id": "events", + "number": 2, + "label": "DiagnosticsEvidence is commit-last", + "mode": "CODE", + "strategy_ref": "code.contracts", + "svg_label": "02", + "code_ref": "include/task01_diagnostics_model.h:6", + "description": "DiagnosticsEvidence is commit-last", + "evidence": "sequence/event/tick/value" + }, + { + "id": "fault", + "number": 3, + "label": "DiagnosticFault freezes terminal data", + "mode": "CODE", + "strategy_ref": "code.contracts", + "svg_label": "03", + "code_ref": "include/task01_diagnostics.h:23", + "description": "DiagnosticFault freezes terminal data", + "evidence": "fixture/hook/line/task/SP" + }, + { + "id": "storage", + "number": 4, + "label": "worker and monitor own static stacks", + "mode": "CODE", + "strategy_ref": "code.contracts", + "svg_label": "04", + "code_ref": "src/tasks/task01_diagnostics.c:25", + "description": "worker and monitor own static stacks", + "evidence": "distinct TCB and stack arrays" + }, + { + "id": "fault-record", + "number": 5, + "label": "fault publication exposes committed marker", + "mode": "RUN", + "event_id": "E07", + "strategy_ref": "run.fixtures", + "svg_label": "05", + "code_ref": "src/tasks/task01_diagnostics.c:91", + "snapshot_ref": "task01.assert-hook", + "description": "fault publication exposes committed marker", + "evidence": "0xFC12FA17" + } + ] + } + ] + } + } + ] + }, + { + "title": "A5 — Healthy replay", + "order": 50, + "content_kind": "prose", + "asset_page_mode": "one-per-page", + "page_orientation": "portrait", + "content_tex": "A worker publishes bounded work and a heartbeat. A lower-priority diagnostics task then records the historical stack watermark, task snapshot and final invariant result.", + "assets": [ + { + "path": "assets/a5-flow.png", + "html_path": "assets/a5-flow.svg", + "source_path": "assets/a5-flow.puml", + "caption": "A5 FLOW — E01 to E06 healthy evidence.", + "label": "fig:a5-flow", + "alt": "A5 · healthy replay", + "kind": "diagram", + "width": 1.0, + "page_grid": { + "columns": 1, + "rows": 1, + "page_width": 660, + "page_height": 760, + "overview": true, + "step_tiles": { + "configured": 1, + "worker-ran": 1, + "heartbeat": 1, + "watermark": 1, + "snapshot": 1, + "pass": 1 + } + }, + "interactive": { + "kind": "uml-sequence", + "storage_key": "fc12-a5-flow", + "title": "A5 · healthy replay", + "task": { + "id": "task01", + "label": "Task01 · healthy run and fault fixtures" + }, + "block": { + "id": "a5", + "label": "A5 FLOW", + "description": "The healthy path publishes six ordered events from configuration through verified PASS." + }, + "phases": [ + { + "id": "healthy", + "label": "HEALTHY E01–E06", + "steps": [ + { + "id": "configured", + "number": 1, + "label": "diagnostics enabled", + "mode": "RUN", + "event_id": "E01", + "strategy_ref": "run.healthy", + "svg_label": "01", + "code_ref": "src/tasks/task01_diagnostics.c:233", + "snapshot_ref": "task01.configured", + "description": "diagnostics enabled", + "evidence": "stack check level 2" + }, + { + "id": "worker-ran", + "number": 2, + "label": "worker performs bounded work", + "mode": "RUN", + "event_id": "E02", + "strategy_ref": "run.healthy", + "svg_label": "02", + "code_ref": "src/tasks/task01_diagnostics.c:152", + "snapshot_ref": "task01.worker-ran", + "description": "worker performs bounded work", + "evidence": "value 21" + }, + { + "id": "heartbeat", + "number": 3, + "label": "worker publishes heartbeat", + "mode": "RUN", + "event_id": "E03", + "strategy_ref": "run.healthy", + "svg_label": "03", + "code_ref": "src/tasks/task01_diagnostics.c:156", + "snapshot_ref": "task01.heartbeat", + "description": "worker publishes heartbeat", + "evidence": "heartbeat = 1" + }, + { + "id": "watermark", + "number": 4, + "label": "diagnostics measures watermark", + "mode": "RUN", + "event_id": "E04", + "strategy_ref": "run.healthy", + "svg_label": "04", + "code_ref": "src/tasks/task01_diagnostics.c:181", + "snapshot_ref": "task01.watermark", + "description": "diagnostics measures watermark", + "evidence": "0 < HWM < 256" + }, + { + "id": "snapshot", + "number": 5, + "label": "diagnostics snapshots task table", + "mode": "RUN", + "event_id": "E05", + "strategy_ref": "run.healthy", + "svg_label": "05", + "code_ref": "src/tasks/task01_diagnostics.c:182", + "snapshot_ref": "task01.snapshot", + "description": "diagnostics snapshots task table", + "evidence": "task count at least 3" + }, + { + "id": "pass", + "number": 6, + "label": "all healthy invariants pass", + "mode": "RUN", + "event_id": "E06", + "strategy_ref": "run.healthy", + "svg_label": "06", + "code_ref": "src/tasks/task01_diagnostics.c:192", + "snapshot_ref": "task01.pass", + "description": "all healthy invariants pass", + "evidence": "PASS plus deterministic digest" + } + ] + } + ] + } + } + ] + }, + { + "title": "A6 — Healthy and expected-fail terminals", + "order": 60, + "content_kind": "prose", + "asset_page_mode": "one-per-page", + "page_orientation": "portrait", + "content_tex": "Fixture selection occurs at main after startup. Each failing branch commits one typed record and must not reach the healthy PASS.", + "assets": [ + { + "path": "assets/a6-state.png", + "html_path": "assets/a6-state.svg", + "source_path": "assets/a6-state.puml", + "caption": "A6 STATE — healthy PASS versus four isolated terminals.", + "label": "fig:a6-state", + "alt": "A6 · terminal states", + "kind": "diagram", + "width": 1.0, + "page_grid": { + "columns": 1, + "rows": 1, + "page_width": 660, + "page_height": 760, + "overview": true, + "step_tiles": { + "select": 1, + "healthy-terminal": 1, + "assert-hook": 1, + "malloc-hook": 1, + "stack-hook": 1, + "deadline-hook": 1 + } + }, + "interactive": { + "kind": "uml-class", + "storage_key": "fc12-a6-state", + "title": "A6 · terminal states", + "task": { + "id": "task01", + "label": "Task01 · healthy run and fault fixtures" + }, + "block": { + "id": "a6", + "label": "A6 STATE", + "description": "A run has exactly one terminal: healthy PASS or one selected expected fault." + }, + "phases": [ + { + "id": "terminal", + "label": "ONE TERMINAL PER RUN", + "steps": [ + { + "id": "select", + "number": 1, + "label": "select fixture only after main", + "mode": "CODE", + "strategy_ref": "code.contracts", + "svg_label": "01", + "code_ref": "scripts/run_fixtures.sh:18", + "description": "select fixture only after main", + "evidence": "BSS cannot erase selector" + }, + { + "id": "healthy-terminal", + "number": 2, + "label": "fixture 0 reaches healthy PASS", + "mode": "RUN", + "event_id": "E06", + "strategy_ref": "run.healthy", + "svg_label": "02", + "code_ref": "src/tasks/task01_diagnostics.c:198", + "snapshot_ref": "task01.pass", + "description": "fixture 0 reaches healthy PASS", + "evidence": "normal terminal" + }, + { + "id": "assert-hook", + "number": 3, + "label": "assert fixture commits hook 1", + "mode": "RUN", + "event_id": "E07", + "strategy_ref": "run.fixtures", + "svg_label": "03", + "code_ref": "src/tasks/task01_diagnostics.c:100", + "snapshot_ref": "task01.assert-hook", + "description": "assert fixture commits hook 1", + "evidence": "fixture=1 hook=1" + }, + { + "id": "malloc-hook", + "number": 4, + "label": "malloc fixture commits hook 2", + "mode": "RUN", + "event_id": "E08", + "strategy_ref": "run.fixtures", + "svg_label": "04", + "code_ref": "src/tasks/task01_diagnostics.c:100", + "snapshot_ref": "task01.malloc-hook", + "description": "malloc fixture commits hook 2", + "evidence": "fixture=2 hook=2" + }, + { + "id": "stack-hook", + "number": 5, + "label": "stack fixture commits hook 3", + "mode": "RUN", + "event_id": "E09", + "strategy_ref": "run.fixtures", + "svg_label": "05", + "code_ref": "src/tasks/task01_diagnostics.c:100", + "snapshot_ref": "task01.stack-hook", + "description": "stack fixture commits hook 3", + "evidence": "fixture=3 hook=3" + }, + { + "id": "deadline-hook", + "number": 6, + "label": "deadline fixture commits hook 4", + "mode": "RUN", + "event_id": "E10", + "strategy_ref": "run.fixtures", + "svg_label": "06", + "code_ref": "src/tasks/task01_diagnostics.c:100", + "snapshot_ref": "task01.deadline-hook", + "description": "deadline fixture commits hook 4", + "evidence": "fixture=4 hook=4" + } + ] + } + ] + } + } + ] + }, + { + "title": "A7 — Runtime proof", + "order": 70, + "content_kind": "prose", + "asset_page_mode": "one-per-page", + "page_orientation": "portrait", + "content_tex": "The watermark is a historical minimum of unused stack, not current consumption. Three clean simulations must emit identical healthy evidence.", + "assets": [ + { + "path": "assets/a7-runtime.png", + "html_path": "assets/a7-runtime.svg", + "source_path": "assets/a7-runtime.puml", + "caption": "A7 RUNTIME — stack, task snapshot, terminal record and identity.", + "label": "fig:a7-runtime", + "alt": "A7 · runtime proof", + "kind": "diagram", + "width": 1.0, + "page_grid": { + "columns": 1, + "rows": 1, + "page_width": 660, + "page_height": 760, + "overview": true, + "step_tiles": { + "stacks": 1, + "hwm": 1, + "tasks": 1, + "fault-sp": 1, + "abi": 1, + "determinism": 1 + } + }, + "interactive": { + "kind": "uml-class", + "storage_key": "fc12-a7-runtime", + "title": "A7 · runtime proof", + "task": { + "id": "task01", + "label": "Task01 · healthy run and fault fixtures" + }, + "block": { + "id": "a7", + "label": "A7 RUNTIME", + "description": "Runtime evidence connects the two task stacks, historical watermark, bounded task snapshot, fault SP and exact artifact identity." + }, + "phases": [ + { + "id": "runtime", + "label": "RUNTIME EVIDENCE", + "steps": [ + { + "id": "stacks", + "number": 1, + "label": "worker and diagnostics SP differ", + "mode": "RUN", + "event_id": "E06", + "strategy_ref": "run.identity", + "svg_label": "01", + "code_ref": "src/tasks/task01_diagnostics.c:190", + "snapshot_ref": "task01.pass", + "description": "worker and diagnostics SP differ", + "evidence": "two task stacks" + }, + { + "id": "hwm", + "number": 2, + "label": "watermark remains inside declared bounds", + "mode": "RUN", + "event_id": "E04", + "strategy_ref": "run.identity", + "svg_label": "02", + "code_ref": "src/tasks/task01_diagnostics.c:178", + "snapshot_ref": "task01.watermark", + "description": "watermark remains inside declared bounds", + "evidence": "0 < HWM < 256" + }, + { + "id": "tasks", + "number": 3, + "label": "system snapshot contains all active tasks", + "mode": "RUN", + "event_id": "E05", + "strategy_ref": "run.identity", + "svg_label": "03", + "code_ref": "src/tasks/task01_diagnostics.c:179", + "snapshot_ref": "task01.snapshot", + "description": "system snapshot contains all active tasks", + "evidence": "task_count >= 3" + }, + { + "id": "fault-sp", + "number": 4, + "label": "fault record preserves stack pointer", + "mode": "RUN", + "event_id": "E09", + "strategy_ref": "run.fixtures", + "svg_label": "04", + "code_ref": "src/tasks/task01_diagnostics.c:97", + "snapshot_ref": "task01.stack-hook", + "description": "fault record preserves stack pointer", + "evidence": "SP != 0" + }, + { + "id": "abi", + "number": 5, + "label": "ELF exposes every diagnostic boundary", + "mode": "CODE", + "strategy_ref": "code.identity", + "svg_label": "05", + "code_ref": "scripts/check_abi.sh:17", + "description": "ELF exposes every diagnostic boundary", + "evidence": "hooks, checkpoints and task APIs" + }, + { + "id": "determinism", + "number": 6, + "label": "three clean processes agree", + "mode": "RUN", + "event_id": "E06", + "strategy_ref": "run.identity", + "svg_label": "06", + "code_ref": "scripts/check_determinism.sh:12", + "snapshot_ref": "task01.pass", + "description": "three clean processes agree", + "evidence": "identical digest" + } + ] + } + ] + } + } + ] + }, + { + "title": "Task01 — healthy run and fault fixtures", + "order": 90, + "content_kind": "tasks", + "task_refs": [ + "task01" + ] + } + ], + "tasks": { + "task01": { + "title": "Diagnose before changing the program", + "uuid": "c3027314-85a4-5e4a-af13-0939c7467a62", + "prompt_tex": "Odtwórz zdrowy ślad E01--E06, a potem cztery izolowane terminale E07--E10. Dla każdego zapisz, który kontrakt wykrył błąd i jakie pole rekordu to dowodzi.", + "criterion": "Healthy PASS; four intended fault terminals; bounded evidence; deterministic artifact identity.", + "conclusion_tex": "Diagnostyka jest wiarygodna wtedy, gdy zdrowy PASS i oczekiwane awarie mają rozłączne, mierzalne terminale oraz identyfikowalny artefakt.", + "flow": [ + { + "kind": "block", + "id": "predict", + "title": "A — przewidywanie", + "content_tex": "Przypisz każdy błąd do właściwego mechanizmu.", + "steps": [ + { + "id": "contracts", + "title": "Uzupełnij tabelę ASSERT/HOOK/MONITOR.", + "content_tex": "Podaj kontekst wywołania i dozwolone działania." + }, + { + "id": "healthy", + "title": "Zapisz zdrowe nierówności.", + "content_tex": "Nie myl high-water mark z bieżącym użyciem stosu." + } + ] + }, + { + "kind": "block", + "id": "replay", + "title": "B — replay", + "content_tex": "Uruchom zdrowy wariant i cztery fixture'y.", + "steps": [ + { + "id": "e01-e06", + "title": "Zweryfikuj E01--E06.", + "content_tex": "Heartbeat, HWM, task count, stosy i PASS." + }, + { + "id": "e07-e10", + "title": "Zweryfikuj E07--E10.", + "content_tex": "Każdy fixture ma dokładnie jeden oczekiwany terminal." + } + ] + }, + { + "kind": "exercise", + "id": "diagnose-trace", + "title": "Ćwiczenie — diagnoza rekordu", + "prompt_tex": "Dostajesz rekord fault bez opisu testu. Wskaż mechanizm, prawdopodobny kontekst i pierwszy bezpieczny krok diagnostyczny bez zmiany kodu.", + "evidence_tex": "fixture, hook, line/task, SP, committed marker oraz identyfikator ELF.", + "criterion": "Wniosek wynika z pól rekordu; uczeń nie traktuje samego komunikatu jako dowodu.", + "based_on": [ + "predict", + "replay" + ] + } + ], + "educational_requirement_refs": [ + "FC12.WE01" + ], + "learning_effect_refs": [ + "FC12.EN01", + "FC12.EK01" + ], + "assessment_criterion_ref": "FC12.KW01" + } + }, + "tasks_order": [ + "task01" + ] +} diff --git a/pdf/mpabi-inf-freertos-c-12-diagnostics-v00.01-b059cd72-9dac-523e-8658-2be46dd4558d.pdf b/pdf/mpabi-inf-freertos-c-12-diagnostics-v00.01-b059cd72-9dac-523e-8658-2be46dd4558d.pdf new file mode 100644 index 0000000..b0c68c6 Binary files /dev/null and b/pdf/mpabi-inf-freertos-c-12-diagnostics-v00.01-b059cd72-9dac-523e-8658-2be46dd4558d.pdf differ