commit 7fc596bb57d014621614e21fd473e8fcbb642ff7 Author: M. Pabiszczak <2+mpabi@noreply.zsl-gitea.mpabi.pl> Date: Mon Jul 20 08:47:38 2026 +0200 publish: FC15 integration v00.01 diff --git a/json/card_source.json b/json/card_source.json new file mode 100644 index 0000000..07c1232 --- /dev/null +++ b/json/card_source.json @@ -0,0 +1,2012 @@ +{ + "$schema": "../../../tools/card-layouts/schemas/card-source.schema.json", + "schema": "esc-card-source.v1", + "card": { + "id": "mpabi-freertos-c-15-integration", + "series": "freertos-c", + "series_title": "FreeRTOS C", + "number": "15", + "count": "15", + "slug": "integration", + "title": "Integrated deterministic FreeRTOS C application", + "topic": "real IRQ, typed pipeline, heartbeat rendezvous and bounded diagnostics", + "project": "Freestanding C nad FreeRTOS", + "subject": "Informatyka", + "level": "Rok 2 · L15 · RV32I/Hazard3", + "revision_date": "2026-07-19T00:00:00+02:00", + "status": "Gotowa", + "version": "v00.01", + "uuid": "0092481f-af7c-517a-87f7-e0d7af7e5a0e", + "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": "end-to-end boundaries", + "status": "enabled", + "target_label": "fig:a1-context" + }, + { + "id": "A2", + "label": "STRUCTURE", + "subtitle": "typed objects and static storage", + "status": "enabled", + "target_label": "fig:a2-structure" + }, + { + "id": "A3", + "label": "DISPATCH", + "subtitle": "IRQ and timer bindings", + "status": "enabled", + "target_label": "fig:a3-dispatch" + }, + { + "id": "A4", + "label": "APPLICATION", + "subtitle": "task and primitive topology", + "status": "enabled", + "target_label": "fig:a4-application" + }, + { + "id": "A5", + "label": "FLOW", + "subtitle": "E01-E14 replay", + "status": "enabled", + "target_label": "fig:a5-flow" + }, + { + "id": "A6", + "label": "STATE", + "subtitle": "payload and readiness lifetime", + "status": "enabled", + "target_label": "fig:a6-state" + }, + { + "id": "A7", + "label": "RUNTIME", + "subtitle": "deadline, heap, stacks and ELF", + "status": "enabled", + "target_label": "fig:a7-runtime" + }, + { + "id": "A8", + "label": "PATTERNS", + "subtitle": "smallest justified mechanism", + "status": "enabled", + "target_label": "fig:a8-patterns" + } + ], + "debug_strategies": { + "code.architecture": { + "id": "code.architecture", + "kind": "code", + "action": "open", + "expected_observations": [ + "each primitive has one role", + "application objects are static" + ], + "assertions": [ + "notification carries no payload", + "shared state is accessed under mutex" + ], + "evidence_fields": [ + "type", + "owner", + "priority", + "storage", + "code_ref" + ], + "prerequisites": [ + "FC01-FC14 complete" + ], + "layout": [ + "typed payloads", + "object owners", + "callbacks", + "static storage" + ], + "commands": [ + "rg -n 'CreateStatic|FromISR|Queue|EventGroup|Semaphore|Timer' include src" + ] + }, + "run.startup": { + "id": "run.startup", + "kind": "run", + "action": "replay", + "expected_observations": [ + "E01-E05 block in strict priority order", + "E06 publishes one input" + ], + "assertions": [ + "heap delta is zero", + "every handle and stack pointer is nonzero" + ], + "evidence_fields": [ + "handle", + "SP", + "heap", + "priority", + "event" + ], + "prerequisites": [ + "clean Hazard3 RAM", + "static object creation complete" + ], + "layout": [ + "five task stacks", + "two queues", + "event group", + "mutex", + "timer" + ], + "commands": [ + "break fc15_checkpoint_committed if $a0 <= 6", + "print g_fc15" + ] + }, + "run.pipeline": { + "id": "run.pipeline", + "kind": "run", + "action": "replay", + "expected_observations": [ + "E07-E10 form one uninterrupted priority chain", + "sum_squares=140" + ], + "assertions": [ + "source clears before notify", + "E10 precedes stimulus E11" + ], + "evidence_fields": [ + "mcause", + "wake", + "payload", + "checksum", + "tick", + "SP" + ], + "prerequisites": [ + "E02-E05 waiting", + "input status ready" + ], + "layout": [ + "external IRQ", + "notification", + "Sample queue", + "Result queue", + "publication" + ], + "commands": [ + "make sim", + "print g_fc15_events", + "print g_fc15.result_seen" + ] + }, + "run.rendezvous": { + "id": "run.rendezvous", + "kind": "run", + "action": "replay", + "expected_observations": [ + "heartbeat at start+5", + "supervisor receives mask 0x3" + ], + "assertions": [ + "mutex entered three times", + "completion is within eight ticks" + ], + "evidence_fields": [ + "timer tick", + "event mask", + "revision", + "heartbeat", + "heap", + "HWM" + ], + "prerequisites": [ + "result bit set", + "one-shot timer active" + ], + "layout": [ + "timer daemon", + "mutex snapshot", + "event bits", + "diagnostics" + ], + "commands": [ + "break fc15_checkpoint_committed if $a0 >= 12", + "print g_fc15" + ] + }, + "code.identity": { + "id": "code.identity", + "kind": "code", + "action": "open", + "expected_observations": [ + "every selected primitive is linked", + "no C++ or unwind metadata" + ], + "assertions": [ + "external trap and daemon task are present", + "static memory hooks are present" + ], + "evidence_fields": [ + "symbol", + "source blob", + "ELF SHA256", + "image SHA256" + ], + "prerequisites": [ + "built ELF" + ], + "layout": [ + "C callbacks", + "kernel primitives", + "static hooks", + "artifact hashes" + ], + "commands": [ + "make check-abi", + "riscv64-unknown-elf-nm build/task01_integration/prog.elf" + ] + }, + "run.identity": { + "id": "run.identity", + "kind": "run", + "action": "replay", + "expected_observations": [ + "one PASS per run", + "digest 8f767299 three times" + ], + "assertions": [ + "event order is exact", + "all terminal invariants are true" + ], + "evidence_fields": [ + "digest", + "event count", + "PASS", + "artifact identity" + ], + "prerequisites": [ + "built image" + ], + "layout": [ + "fourteen events", + "three clean processes", + "terminal" + ], + "commands": [ + "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": "Integrated deterministic FreeRTOS C application", + "url": "https://dce7fb9d-7b2f-5d49-96a2-3a30d3070b84.mpabi.pl/fe92efeb-3c38-5975-86d8-ed630e1ad3bb", + "repository_url": "https://zsl-gitea.mpabi.pl/edu-freertos-c/lab-rv32i-freertos-c-integration", + "url_host_uuid": "dce7fb9d-7b2f-5d49-96a2-3a30d3070b84", + "url_domain": "mpabi.pl", + "doc_uuid": "fe92efeb-3c38-5975-86d8-ed630e1ad3bb", + "revision": "v00.01", + "issued_on": "2026-07-19T00:00:00+02:00", + "series": "FREERTOS-C-15", + "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ń składa kompletną aplikację FreeRTOS C i uzasadnia każdy użyty mechanizm przez payload, własność, fan-in albo czas, a następnie dowodzi całego kontraktu jednym deterministycznym śladem.", + "scope_title": "Zakres karty", + "scope_content_tex": "Prawdziwy external IRQ budzi acquisition. Dwie kolejki prowadzą Sample przez obliczenie sumy kwadratów do publikacji. Timer daemon dodaje heartbeat; event group i mutex tworzą spójny snapshot. Wszystkie obiekty aplikacji mają pamięć statyczną.", + "scope_table": { + "headers": [ + "Lekcja", + "Task", + "Najważniejsza idea", + "Priorytet", + "Status", + "Version" + ], + "rows": [ + { + "chapter": "FC15", + "task": "Task01", + "idea_tex": "real IRQ, typed pipeline, heartbeat rendezvous and bounded diagnostics", + "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": { + "FC15.EN01": { + "bloom_level": "Analiza", + "label": "Justified RTOS architecture", + "text": "Uczeń dobiera notification, queue, mutex, event group and timer by ownership and synchronization need.", + "assessment_criteria": [ + "FC15.KW01" + ] + }, + "FC15.EK01": { + "bloom_level": "Zastosowanie", + "label": "Deterministic end-to-end proof", + "text": "Uczeń odtwarza E01–E14 from hardware input through result, heartbeat, diagnostics and PASS.", + "assessment_criteria": [ + "FC15.KW01" + ] + } + }, + "assessment_criteria": { + "FC15.KW01": { + "text": "PASS; real MEI; pipeline before stimulus resume; sum 140; result and heartbeat ALL-mask; completion by tick 8; zero application heap delta; positive stack HWM; deterministic digest.", + "learning_effects": [ + "FC15.EN01", + "FC15.EK01" + ] + } + }, + "educational_requirements": { + "FC15.WE01": { + "text": "Samodzielne zaprojektowanie, implementacja i diagnostyka deterministycznej aplikacji FreeRTOS C.", + "label": "real IRQ, typed pipeline, heartbeat rendezvous and bounded diagnostics", + "learning_effects": [ + "FC15.EN01", + "FC15.EK01" + ], + "learning_tree": { + "schema": "we-learning-tree.v1", + "policy": "Każda aktywna kotwica wskazuje kod lub checkpoint.", + "ogolne": [ + { + "effect_ref": "FC15.EN01", + "display": "EN LOCAL RTOS.15", + "source": "LOCAL", + "official": "RTOS", + "local": "15", + "kind": "EN", + "tree_id": "FC15.WE01.OG.LOCAL.RTOS.15", + "text": "Uczeń dobiera notification, queue, mutex, event group and timer by ownership and synchronization need.", + "kw": [ + { + "criterion_ref": "FC15.KW01", + "display": "KW LOCAL RTOS.15", + "source": "LOCAL", + "kind": "KW", + "official": "RTOS", + "local": "15", + "text": "Łączy kod, diagram i zweryfikowany dowód." + } + ] + } + ], + "zawodowe": [ + { + "effect_ref": "FC15.EK01", + "display": "EK LOCAL RTOS.15", + "source": "LOCAL", + "official": "RTOS", + "local": "15", + "kind": "EK", + "tree_id": "FC15.WE01.TECH.LOCAL.RTOS.15", + "text": "Uczeń odtwarza E01–E14 from hardware input through result, heartbeat, diagnostics and PASS.", + "kw": [ + { + "criterion_ref": "FC15.KW01", + "display": "KW LOCAL RTOS.15", + "source": "LOCAL", + "kind": "KW", + "official": "RTOS", + "local": "15", + "text": "Łączy kod, diagram i zweryfikowany dowód." + } + ] + } + ] + } + } + }, + "debug_checkpoints": { + "schema": "stem-debug-checkpoints.v1", + "semantics": "deterministic-replay", + "artifact": { + "source": "src/tasks/task01_integration.c", + "source_git_blob": "b53b089d45e31108123aff657619dfc1603fe0b3", + "elf": "build/task01_integration/prog.elf", + "hazard3_elf_sha256": "9ebc2e032d20cf55c43b862e60936b26df0de0899cab6fca65ba032b4de77695", + "hazard3_image": "build/task01_integration/prog.bin", + "hazard3_image_sha256": "fd46dd3a71a4c0b5d9c5fe9c1c62a5201eed4c229331d207d97fec658f6e7570" + }, + "targets": { + "hazard3-sim": { + "adapter": "hazard3-reset-load-replay.v1", + "baseline": "restart-backend", + "clean_ram": true + } + }, + "items": { + "task01.configured": { + "event_id": "E01", + "stop": { + "symbol": "fc15_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 1" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc15_event_count", + "equals": 1 + }, + { + "expr": "g_fc15.heap_before == g_fc15.heap_after", + "equals": 1 + }, + { + "expr": "g_fc15.sample_queue != 0 && g_fc15.result_queue != 0", + "equals": 1 + } + ] + } + }, + "task01.acquisition-ready": { + "event_id": "E02", + "stop": { + "symbol": "fc15_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 2" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc15.acquisition_sp != 0", + "equals": 1 + }, + { + "expr": "g_fc15.acquired", + "equals": 0 + } + ] + } + }, + "task01.processor-ready": { + "event_id": "E03", + "stop": { + "symbol": "fc15_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 3" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc15.processor_sp != 0", + "equals": 1 + }, + { + "expr": "g_fc15.processed", + "equals": 0 + } + ] + } + }, + "task01.publisher-ready": { + "event_id": "E04", + "stop": { + "symbol": "fc15_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 4" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc15.publisher_sp != 0", + "equals": 1 + }, + { + "expr": "g_fc15.published", + "equals": 0 + } + ] + } + }, + "task01.supervisor-ready": { + "event_id": "E05", + "stop": { + "symbol": "fc15_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 5" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc15.supervisor_sp != 0", + "equals": 1 + }, + { + "expr": "g_fc15.returned_bits", + "equals": 0 + } + ] + } + }, + "task01.input-ready": { + "event_id": "E06", + "stop": { + "symbol": "fc15_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 6" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc15.input.status", + "equals": 1 + }, + { + "expr": "g_fc15.input.sequence", + "equals": 42 + }, + { + "expr": "g_fc15.input.value", + "equals": 7 + } + ] + } + }, + "task01.irq": { + "event_id": "E07", + "stop": { + "symbol": "fc15_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 7" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc15.mcause", + "equals": 2147483659 + }, + { + "expr": "g_fc15.irq_after_clear", + "equals": 0 + }, + { + "expr": "g_fc15.higher_priority_task_woken", + "equals": 1 + } + ] + } + }, + "task01.acquired": { + "event_id": "E08", + "stop": { + "symbol": "fc15_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 8" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc15.acquired", + "equals": 1 + }, + { + "expr": "g_fc15.sample_seen.value", + "equals": 7 + }, + { + "expr": "g_fc15.acquisition_saw_stimulus_after", + "equals": 0 + } + ] + } + }, + "task01.processed": { + "event_id": "E09", + "stop": { + "symbol": "fc15_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 9" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc15.processed", + "equals": 1 + }, + { + "expr": "g_fc15.result_seen.sum_squares", + "equals": 140 + } + ] + } + }, + "task01.published": { + "event_id": "E10", + "stop": { + "symbol": "fc15_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 10" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc15.published", + "equals": 1 + }, + { + "expr": "g_fc15.shared.revision", + "equals": 1 + }, + { + "expr": "g_fc15.result_ready", + "equals": 1 + } + ] + } + }, + "task01.stimulus-resumed": { + "event_id": "E11", + "stop": { + "symbol": "fc15_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 11" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc15.pipeline_done_at_stimulus_resume", + "equals": 1 + }, + { + "expr": "g_fc15.stimulus_after_irq", + "equals": 1 + } + ] + } + }, + "task01.heartbeat": { + "event_id": "E12", + "stop": { + "symbol": "fc15_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 12" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc15.heartbeat_calls", + "equals": 1 + }, + { + "expr": "g_fc15.shared.heartbeat", + "equals": 1 + }, + { + "expr": "g_fc15.heartbeat_tick == g_fc15.start_tick + 5", + "equals": 1 + } + ] + } + }, + "task01.diagnostics": { + "event_id": "E13", + "stop": { + "symbol": "fc15_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 13" + }, + "verify": { + "expressions": [ + { + "expr": "(g_fc15.returned_bits & 3) == 3", + "equals": 1 + }, + { + "expr": "g_fc15.mutex_entries", + "equals": 3 + }, + { + "expr": "g_fc15.heap_before == g_fc15.heap_terminal", + "equals": 1 + } + ] + } + }, + "task01.pass": { + "event_id": "E14", + "stop": { + "symbol": "fc15_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 14" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc15_pass", + "equals": 1 + }, + { + "expr": "g_fc15_event_count", + "equals": 14 + }, + { + "expr": "g_fc15.snapshot.result.sum_squares", + "equals": 140 + } + ] + } + } + } + }, + "sections": [ + { + "title": "A1 — End-to-end responsibility boundary", + "order": 10, + "content_kind": "prose", + "asset_page_mode": "one-per-page", + "page_orientation": "portrait", + "content_tex": "Each boundary has one transport and one owner. The ISR carries no payload; the queues carry values; the event group carries readiness; the mutex protects a consistent shared snapshot.", + "assets": [ + { + "path": "assets/a1-context.png", + "html_path": "assets/a1-context.svg", + "source_path": "assets/a1-context.puml", + "caption": "A1 CONTEXT — device, ISR, pipeline, heartbeat and supervision.", + "label": "fig:a1-context", + "alt": "A1 · integrated responsibility boundary", + "kind": "diagram", + "width": 1.0, + "page_grid": { + "columns": 1, + "rows": 1, + "page_width": 660, + "page_height": 760, + "overview": true, + "step_tiles": { + "device": 1, + "isr": 1, + "pipeline": 1, + "daemon": 1, + "supervisor": 1, + "terminal": 1 + } + }, + "interactive": { + "kind": "uml-class", + "storage_key": "fc15-a1-context", + "title": "A1 · integrated responsibility boundary", + "task": { + "id": "task01", + "label": "Task01 · integrated deterministic application" + }, + "block": { + "id": "a1", + "label": "A1 CONTEXT", + "description": "The external device, ISR, data pipeline, timer daemon, shared publication and supervisor are independent responsibility zones." + }, + "phases": [ + { + "id": "boundary", + "label": "END-TO-END BOUNDARIES", + "steps": [ + { + "id": "device", + "number": 1, + "label": "input register bank owns raw sample", + "mode": "CODE", + "strategy_ref": "code.architecture", + "svg_label": "01", + "code_ref": "include/task01_integration.h:28", + "description": "input register bank owns raw sample", + "evidence": "status, sequence, value" + }, + { + "id": "isr", + "number": 2, + "label": "external ISR only clears and notifies", + "mode": "CODE", + "strategy_ref": "code.architecture", + "svg_label": "02", + "code_ref": "src/tasks/task01_integration.c:154", + "description": "external ISR only clears and notifies", + "evidence": "no payload copy" + }, + { + "id": "pipeline", + "number": 3, + "label": "three tasks transform typed values", + "mode": "CODE", + "strategy_ref": "code.architecture", + "svg_label": "03", + "code_ref": "src/tasks/task01_integration.c:170", + "description": "three tasks transform typed values", + "evidence": "Sample to Result to publication" + }, + { + "id": "daemon", + "number": 4, + "label": "software timer owns independent heartbeat", + "mode": "CODE", + "strategy_ref": "code.architecture", + "svg_label": "04", + "code_ref": "src/tasks/task01_integration.c:288", + "description": "software timer owns independent heartbeat", + "evidence": "timer daemon context" + }, + { + "id": "supervisor", + "number": 5, + "label": "supervisor joins and diagnoses", + "mode": "CODE", + "strategy_ref": "code.architecture", + "svg_label": "05", + "code_ref": "src/tasks/task01_integration.c:319", + "description": "supervisor joins and diagnoses", + "evidence": "result plus heartbeat" + }, + { + "id": "terminal", + "number": 6, + "label": "one trace proves the whole boundary", + "mode": "RUN", + "event_id": "E14", + "strategy_ref": "run.identity", + "svg_label": "06", + "code_ref": "src/tasks/task01_integration.c:404", + "snapshot_ref": "task01.pass", + "description": "one trace proves the whole boundary", + "evidence": "PASS and deterministic digest" + } + ] + } + ] + } + } + ] + }, + { + "title": "A2 — Typed objects and static ownership", + "order": 20, + "content_kind": "prose", + "asset_page_mode": "one-per-page", + "page_orientation": "portrait", + "content_tex": "A Sample has two words, a Result has four, and PublishedState adds revision and heartbeat. Queue storage copies the typed payload; notification and event bits never impersonate it.", + "assets": [ + { + "path": "assets/a2-structure.png", + "html_path": "assets/a2-structure.svg", + "source_path": "assets/a2-structure.puml", + "caption": "A2 STRUCTURE — typed messages, kernel objects and static storage.", + "label": "fig:a2-structure", + "alt": "A2 · static object graph", + "kind": "diagram", + "width": 1.0, + "page_grid": { + "columns": 1, + "rows": 1, + "page_width": 660, + "page_height": 760, + "overview": true, + "step_tiles": { + "types": 1, + "state": 1, + "handles": 1, + "storage": 1, + "heap": 1 + } + }, + "interactive": { + "kind": "uml-class", + "storage_key": "fc15-a2-structure", + "title": "A2 · static object graph", + "task": { + "id": "task01", + "label": "Task01 · integrated deterministic application" + }, + "block": { + "id": "a2", + "label": "A2 STRUCTURE", + "description": "All application tasks and kernel objects use named static storage; payload and synchronization records remain distinct." + }, + "phases": [ + { + "id": "objects", + "label": "TYPES / OBJECTS / STORAGE", + "steps": [ + { + "id": "types", + "number": 1, + "label": "Sample and Result have explicit value layouts", + "mode": "CODE", + "strategy_ref": "code.architecture", + "svg_label": "01", + "code_ref": "include/task01_integration_model.h:12", + "description": "Sample and Result have explicit value layouts", + "evidence": "2-word and 4-word payloads" + }, + { + "id": "state", + "number": 2, + "label": "PublishedState is one mutex snapshot", + "mode": "CODE", + "strategy_ref": "code.architecture", + "svg_label": "02", + "code_ref": "include/task01_integration_model.h:26", + "description": "PublishedState is one mutex snapshot", + "evidence": "result, revision, heartbeat" + }, + { + "id": "handles", + "number": 3, + "label": "experiment names every task and object handle", + "mode": "CODE", + "strategy_ref": "code.architecture", + "svg_label": "03", + "code_ref": "include/task01_integration.h:35", + "description": "experiment names every task and object handle", + "evidence": "five tasks, two queues, event, mutex, timer" + }, + { + "id": "storage", + "number": 4, + "label": "TCBs, stacks and control blocks are static", + "mode": "CODE", + "strategy_ref": "code.architecture", + "svg_label": "04", + "code_ref": "src/tasks/task01_integration.c:36", + "description": "TCBs, stacks and control blocks are static", + "evidence": "bounded application storage" + }, + { + "id": "heap", + "number": 5, + "label": "object creation leaves current heap unchanged", + "mode": "RUN", + "event_id": "E01", + "strategy_ref": "run.startup", + "svg_label": "05", + "code_ref": "src/tasks/task01_integration.c:477", + "snapshot_ref": "task01.configured", + "description": "object creation leaves current heap unchanged", + "evidence": "before equals after" + } + ] + } + ] + } + } + ] + }, + { + "title": "A3 — Two asynchronous bindings", + "order": 30, + "content_kind": "prose", + "asset_page_mode": "one-per-page", + "page_orientation": "portrait", + "content_tex": "FromISR notification selects acquisition immediately. The timer service later calls the heartbeat callback in task context; neither path calls the other's API family.", + "assets": [ + { + "path": "assets/a3-dispatch.png", + "html_path": "assets/a3-dispatch.svg", + "source_path": "assets/a3-dispatch.puml", + "caption": "A3 DISPATCH — external IRQ to acquisition and timer expiry to daemon.", + "label": "fig:a3-dispatch", + "alt": "A3 · IRQ and timer dispatch", + "kind": "diagram", + "width": 1.0, + "page_grid": { + "columns": 1, + "rows": 1, + "page_width": 660, + "page_height": 760, + "overview": true, + "step_tiles": { + "external-vector": 1, + "notify": 1, + "immediate": 1, + "timer-binding": 1, + "heartbeat": 1 + } + }, + "interactive": { + "kind": "uml-class", + "storage_key": "fc15-a3-dispatch", + "title": "A3 · IRQ and timer dispatch", + "task": { + "id": "task01", + "label": "Task01 · integrated deterministic application" + }, + "block": { + "id": "a3", + "label": "A3 DISPATCH", + "description": "The application has two unrelated asynchronous entries: a real external ISR and a software timer callback on the daemon task." + }, + "phases": [ + { + "id": "dispatch", + "label": "TWO ASYNCHRONOUS ENTRIES", + "steps": [ + { + "id": "external-vector", + "number": 1, + "label": "external trap enters application ISR", + "mode": "CODE", + "strategy_ref": "code.architecture", + "svg_label": "01", + "code_ref": "src/common/hazard3_freertos_traps.S:24", + "description": "external trap enters application ISR", + "evidence": "full context save" + }, + { + "id": "notify", + "number": 2, + "label": "ISR clears and wakes acquisition", + "mode": "RUN", + "event_id": "E07", + "strategy_ref": "run.pipeline", + "svg_label": "02", + "code_ref": "src/tasks/task01_integration.c:158", + "snapshot_ref": "task01.irq", + "description": "ISR clears and wakes acquisition", + "evidence": "MEI, source zero, wake true" + }, + { + "id": "immediate", + "number": 3, + "label": "acquisition runs before stimulus resumes", + "mode": "RUN", + "event_id": "E08", + "strategy_ref": "run.pipeline", + "svg_label": "03", + "code_ref": "src/tasks/task01_integration.c:186", + "snapshot_ref": "task01.acquired", + "description": "acquisition runs before stimulus resumes", + "evidence": "stimulus_after=0" + }, + { + "id": "timer-binding", + "number": 4, + "label": "timer object binds one callback and context", + "mode": "CODE", + "strategy_ref": "code.architecture", + "svg_label": "04", + "code_ref": "src/tasks/task01_integration.c:491", + "description": "timer object binds one callback and context", + "evidence": "one-shot period five" + }, + { + "id": "heartbeat", + "number": 5, + "label": "timer daemon publishes independent readiness", + "mode": "RUN", + "event_id": "E12", + "strategy_ref": "run.rendezvous", + "svg_label": "05", + "code_ref": "src/tasks/task01_integration.c:297", + "snapshot_ref": "task01.heartbeat", + "description": "timer daemon publishes independent readiness", + "evidence": "heartbeat=1 at tick+5" + } + ] + } + ] + } + } + ] + }, + { + "title": "A4 — Task and primitive topology", + "order": 40, + "content_kind": "prose", + "asset_page_mode": "one-per-page", + "page_orientation": "portrait", + "content_tex": "Priorities 6, 5 and 4 let the data pipeline finish before returning to stimulus priority 1. Supervisor priority 2 remains blocked until both result and heartbeat exist.", + "assets": [ + { + "path": "assets/a4-application.png", + "html_path": "assets/a4-application.svg", + "source_path": "assets/a4-application.puml", + "caption": "A4 APPLICATION — priorities, transports and one rendezvous.", + "label": "fig:a4-application", + "alt": "A4 · application topology", + "kind": "diagram", + "width": 1.0, + "page_grid": { + "columns": 1, + "rows": 1, + "page_width": 660, + "page_height": 760, + "overview": true, + "step_tiles": { + "acq-ready": 1, + "proc-ready": 1, + "pub-ready": 1, + "supervisor-ready": 1, + "heartbeat-role": 1, + "stimulus-role": 1 + } + }, + "interactive": { + "kind": "uml-class", + "storage_key": "fc15-a4-application", + "title": "A4 · application topology", + "task": { + "id": "task01", + "label": "Task01 · integrated deterministic application" + }, + "block": { + "id": "a4", + "label": "A4 APPLICATION", + "description": "Five application tasks and the timer daemon form one acyclic data path plus one independent control path." + }, + "phases": [ + { + "id": "topology", + "label": "TASK / OBJECT TOPOLOGY", + "steps": [ + { + "id": "acq-ready", + "number": 1, + "label": "acquisition priority 6 waits on notification", + "mode": "RUN", + "event_id": "E02", + "strategy_ref": "run.startup", + "svg_label": "01", + "code_ref": "src/tasks/task01_integration.c:179", + "snapshot_ref": "task01.acquisition-ready", + "description": "acquisition priority 6 waits on notification", + "evidence": "one-to-one wake" + }, + { + "id": "proc-ready", + "number": 2, + "label": "processor priority 5 waits on Sample queue", + "mode": "RUN", + "event_id": "E03", + "strategy_ref": "run.startup", + "svg_label": "02", + "code_ref": "src/tasks/task01_integration.c:217", + "snapshot_ref": "task01.processor-ready", + "description": "processor priority 5 waits on Sample queue", + "evidence": "typed copy" + }, + { + "id": "pub-ready", + "number": 3, + "label": "publisher priority 4 waits on Result queue", + "mode": "RUN", + "event_id": "E04", + "strategy_ref": "run.startup", + "svg_label": "03", + "code_ref": "src/tasks/task01_integration.c:256", + "snapshot_ref": "task01.publisher-ready", + "description": "publisher priority 4 waits on Result queue", + "evidence": "typed copy" + }, + { + "id": "supervisor-ready", + "number": 4, + "label": "supervisor waits for both event bits", + "mode": "RUN", + "event_id": "E05", + "strategy_ref": "run.startup", + "svg_label": "04", + "code_ref": "src/tasks/task01_integration.c:327", + "snapshot_ref": "task01.supervisor-ready", + "description": "supervisor waits for both event bits", + "evidence": "ALL mask" + }, + { + "id": "heartbeat-role", + "number": 5, + "label": "daemon priority 3 provides heartbeat", + "mode": "CODE", + "strategy_ref": "code.architecture", + "svg_label": "05", + "code_ref": "include/FreeRTOSConfig.h:26", + "description": "daemon priority 3 provides heartbeat", + "evidence": "independent control path" + }, + { + "id": "stimulus-role", + "number": 6, + "label": "stimulus priority 1 injects one input", + "mode": "RUN", + "event_id": "E06", + "strategy_ref": "run.pipeline", + "svg_label": "06", + "code_ref": "src/tasks/task01_integration.c:430", + "snapshot_ref": "task01.input-ready", + "description": "stimulus priority 1 injects one input", + "evidence": "sequence 42, value 7" + } + ] + } + ] + } + } + ] + }, + { + "title": "A5 — Fourteen-event replay", + "order": 50, + "content_kind": "prose", + "asset_page_mode": "one-per-page", + "page_orientation": "portrait", + "content_tex": "E07–E11 prove that notification plus strict priorities complete acquisition, calculation and publication before the interrupted stimulus resumes. E12–E14 prove the independent rendezvous and deadline.", + "assets": [ + { + "path": "assets/a5-flow.png", + "html_path": "assets/a5-flow.svg", + "source_path": "assets/a5-flow.puml", + "caption": "A5 FLOW — E01–E14 from static configuration to PASS.", + "label": "fig:a5-flow", + "alt": "A5 · integrated deterministic replay", + "kind": "diagram", + "width": 1.0, + "page_grid": { + "columns": 1, + "rows": 1, + "page_width": 660, + "page_height": 760, + "overview": true, + "step_tiles": { + "e01": 1, + "e02": 1, + "e03": 1, + "e04": 1, + "e05": 1, + "e06": 1, + "e07": 1, + "e08": 1, + "e09": 1, + "e10": 1, + "e11": 1, + "e12": 1, + "e13": 1, + "e14": 1 + } + }, + "interactive": { + "kind": "uml-sequence", + "storage_key": "fc15-a5-flow", + "title": "A5 · integrated deterministic replay", + "task": { + "id": "task01", + "label": "Task01 · integrated deterministic application" + }, + "block": { + "id": "a5", + "label": "A5 FLOW", + "description": "The trace separates startup, the immediate IRQ-driven data chain, delayed heartbeat and final diagnostic terminal." + }, + "phases": [ + { + "id": "startup", + "label": "STARTUP E01–E06", + "steps": [ + { + "id": "e01", + "number": 1, + "label": "static objects and timer configured", + "mode": "RUN", + "event_id": "E01", + "strategy_ref": "run.startup", + "svg_label": "01", + "code_ref": "src/tasks/task01_integration.c:475", + "snapshot_ref": "task01.configured", + "description": "static objects and timer configured", + "evidence": "heap delta zero" + }, + { + "id": "e02", + "number": 2, + "label": "acquisition blocks", + "mode": "RUN", + "event_id": "E02", + "strategy_ref": "run.startup", + "svg_label": "02", + "code_ref": "src/tasks/task01_integration.c:180", + "snapshot_ref": "task01.acquisition-ready", + "description": "acquisition blocks", + "evidence": "priority 6" + }, + { + "id": "e03", + "number": 3, + "label": "processor blocks", + "mode": "RUN", + "event_id": "E03", + "strategy_ref": "run.startup", + "svg_label": "03", + "code_ref": "src/tasks/task01_integration.c:218", + "snapshot_ref": "task01.processor-ready", + "description": "processor blocks", + "evidence": "priority 5" + }, + { + "id": "e04", + "number": 4, + "label": "publisher blocks", + "mode": "RUN", + "event_id": "E04", + "strategy_ref": "run.startup", + "svg_label": "04", + "code_ref": "src/tasks/task01_integration.c:257", + "snapshot_ref": "task01.publisher-ready", + "description": "publisher blocks", + "evidence": "priority 4" + }, + { + "id": "e05", + "number": 5, + "label": "supervisor waits ALL", + "mode": "RUN", + "event_id": "E05", + "strategy_ref": "run.startup", + "svg_label": "05", + "code_ref": "src/tasks/task01_integration.c:328", + "snapshot_ref": "task01.supervisor-ready", + "description": "supervisor waits ALL", + "evidence": "mask 0x3" + }, + { + "id": "e06", + "number": 6, + "label": "stimulus publishes input", + "mode": "RUN", + "event_id": "E06", + "strategy_ref": "run.pipeline", + "svg_label": "06", + "code_ref": "src/tasks/task01_integration.c:432", + "snapshot_ref": "task01.input-ready", + "description": "stimulus publishes input", + "evidence": "42 and 7" + } + ] + }, + { + "id": "runtime", + "label": "PIPELINE E07–E14", + "steps": [ + { + "id": "e07", + "number": 7, + "label": "ISR notifies acquisition", + "mode": "RUN", + "event_id": "E07", + "strategy_ref": "run.pipeline", + "svg_label": "07", + "code_ref": "src/tasks/task01_integration.c:162", + "snapshot_ref": "task01.irq", + "description": "ISR notifies acquisition", + "evidence": "wake true" + }, + { + "id": "e08", + "number": 8, + "label": "acquisition queues Sample", + "mode": "RUN", + "event_id": "E08", + "strategy_ref": "run.pipeline", + "svg_label": "08", + "code_ref": "src/tasks/task01_integration.c:192", + "snapshot_ref": "task01.acquired", + "description": "acquisition queues Sample", + "evidence": "value 7" + }, + { + "id": "e09", + "number": 9, + "label": "processor queues Result", + "mode": "RUN", + "event_id": "E09", + "strategy_ref": "run.pipeline", + "svg_label": "09", + "code_ref": "src/tasks/task01_integration.c:225", + "snapshot_ref": "task01.processed", + "description": "processor queues Result", + "evidence": "sum 140" + }, + { + "id": "e10", + "number": 10, + "label": "publisher commits result bit", + "mode": "RUN", + "event_id": "E10", + "strategy_ref": "run.pipeline", + "svg_label": "10", + "code_ref": "src/tasks/task01_integration.c:266", + "snapshot_ref": "task01.published", + "description": "publisher commits result bit", + "evidence": "revision 1" + }, + { + "id": "e11", + "number": 11, + "label": "stimulus resumes after pipeline", + "mode": "RUN", + "event_id": "E11", + "strategy_ref": "run.pipeline", + "svg_label": "11", + "code_ref": "src/tasks/task01_integration.c:442", + "snapshot_ref": "task01.stimulus-resumed", + "description": "stimulus resumes after pipeline", + "evidence": "result already ready" + }, + { + "id": "e12", + "number": 12, + "label": "daemon commits heartbeat bit", + "mode": "RUN", + "event_id": "E12", + "strategy_ref": "run.rendezvous", + "svg_label": "12", + "code_ref": "src/tasks/task01_integration.c:299", + "snapshot_ref": "task01.heartbeat", + "description": "daemon commits heartbeat bit", + "evidence": "tick +5" + }, + { + "id": "e13", + "number": 13, + "label": "supervisor joins and measures", + "mode": "RUN", + "event_id": "E13", + "strategy_ref": "run.rendezvous", + "svg_label": "13", + "code_ref": "src/tasks/task01_integration.c:332", + "snapshot_ref": "task01.diagnostics", + "description": "supervisor joins and measures", + "evidence": "bits, heap, HWM" + }, + { + "id": "e14", + "number": 14, + "label": "all contracts reach PASS", + "mode": "RUN", + "event_id": "E14", + "strategy_ref": "run.identity", + "svg_label": "14", + "code_ref": "src/tasks/task01_integration.c:404", + "snapshot_ref": "task01.pass", + "description": "all contracts reach PASS", + "evidence": "digest 8f767299" + } + ] + } + ] + } + } + ] + }, + { + "title": "A6 — Data, readiness and lifetime states", + "order": 60, + "content_kind": "prose", + "asset_page_mode": "one-per-page", + "page_orientation": "portrait", + "content_tex": "Queues become empty after each transfer; the shared state becomes valid at revision one; the event group releases only after both independent bits are present and then clears them on exit.", + "assets": [ + { + "path": "assets/a6-state.png", + "html_path": "assets/a6-state.svg", + "source_path": "assets/a6-state.puml", + "caption": "A6 STATE — device, queues, shared state and ALL-bit rendezvous.", + "label": "fig:a6-state", + "alt": "A6 · integrated state machine", + "kind": "diagram", + "width": 1.0, + "page_grid": { + "columns": 1, + "rows": 1, + "page_width": 660, + "page_height": 760, + "overview": true, + "step_tiles": { + "device-ready": 1, + "sample-copy": 1, + "result-copy": 1, + "result-bit": 1, + "both-bits": 1, + "snapshot": 1 + } + }, + "interactive": { + "kind": "uml-class", + "storage_key": "fc15-a6-state", + "title": "A6 · integrated state machine", + "task": { + "id": "task01", + "label": "Task01 · integrated deterministic application" + }, + "block": { + "id": "a6", + "label": "A6 STATE", + "description": "Payload lifetime, task blocking and readiness bits evolve on separate state axes." + }, + "phases": [ + { + "id": "state", + "label": "STATE AXES", + "steps": [ + { + "id": "device-ready", + "number": 1, + "label": "device changes empty to ready", + "mode": "RUN", + "event_id": "E06", + "strategy_ref": "run.pipeline", + "svg_label": "01", + "code_ref": "src/tasks/task01_integration.c:435", + "snapshot_ref": "task01.input-ready", + "description": "device changes empty to ready", + "evidence": "status=1" + }, + { + "id": "sample-copy", + "number": 2, + "label": "Sample queue transfers and returns empty", + "mode": "RUN", + "event_id": "E08", + "strategy_ref": "run.pipeline", + "svg_label": "02", + "code_ref": "src/tasks/task01_integration.c:192", + "snapshot_ref": "task01.acquired", + "description": "Sample queue transfers and returns empty", + "evidence": "acquired=1" + }, + { + "id": "result-copy", + "number": 3, + "label": "Result queue transfers and returns empty", + "mode": "RUN", + "event_id": "E10", + "strategy_ref": "run.pipeline", + "svg_label": "03", + "code_ref": "src/tasks/task01_integration.c:258", + "snapshot_ref": "task01.published", + "description": "Result queue transfers and returns empty", + "evidence": "published=1" + }, + { + "id": "result-bit", + "number": 4, + "label": "result bit waits for heartbeat bit", + "mode": "RUN", + "event_id": "E10", + "strategy_ref": "run.pipeline", + "svg_label": "04", + "code_ref": "src/tasks/task01_integration.c:276", + "snapshot_ref": "task01.published", + "description": "result bit waits for heartbeat bit", + "evidence": "mask incomplete" + }, + { + "id": "both-bits", + "number": 5, + "label": "heartbeat completes ALL mask", + "mode": "RUN", + "event_id": "E12", + "strategy_ref": "run.rendezvous", + "svg_label": "05", + "code_ref": "src/tasks/task01_integration.c:311", + "snapshot_ref": "task01.heartbeat", + "description": "heartbeat completes ALL mask", + "evidence": "mask 0x3" + }, + { + "id": "snapshot", + "number": 6, + "label": "supervisor locks one complete snapshot", + "mode": "RUN", + "event_id": "E13", + "strategy_ref": "run.rendezvous", + "svg_label": "06", + "code_ref": "src/tasks/task01_integration.c:338", + "snapshot_ref": "task01.diagnostics", + "description": "supervisor locks one complete snapshot", + "evidence": "three mutex entries" + } + ] + } + ] + } + } + ] + }, + { + "title": "A7 — Deadline, memory and context proof", + "order": 70, + "content_kind": "prose", + "asset_page_mode": "one-per-page", + "page_orientation": "portrait", + "content_tex": "All application objects are static, so current heap is equal before creation, after creation and at the terminal. Historical minimum remains a separate diagnostic value.", + "assets": [ + { + "path": "assets/a7-runtime.png", + "html_path": "assets/a7-runtime.svg", + "source_path": "assets/a7-runtime.puml", + "caption": "A7 RUNTIME — cause, timing, heap, stacks and artifact identity.", + "label": "fig:a7-runtime", + "alt": "A7 · final runtime proof", + "kind": "diagram", + "width": 1.0, + "page_grid": { + "columns": 1, + "rows": 1, + "page_width": 660, + "page_height": 760, + "overview": true, + "step_tiles": { + "cause": 1, + "ordering": 1, + "deadline": 1, + "heap": 1, + "watermarks": 1, + "abi": 1, + "digest": 1 + } + }, + "interactive": { + "kind": "uml-class", + "storage_key": "fc15-a7-runtime", + "title": "A7 · final runtime proof", + "task": { + "id": "task01", + "label": "Task01 · integrated deterministic application" + }, + "block": { + "id": "a7", + "label": "A7 RUNTIME", + "description": "The terminal connects hardware cause, scheduling order, queue state, stack watermarks, heap invariance and exact artifact identity." + }, + "phases": [ + { + "id": "runtime", + "label": "RUNTIME ACCEPTANCE", + "steps": [ + { + "id": "cause", + "number": 1, + "label": "real MEI uses separate ISR stack", + "mode": "RUN", + "event_id": "E07", + "strategy_ref": "run.pipeline", + "svg_label": "01", + "code_ref": "src/tasks/task01_integration.c:158", + "snapshot_ref": "task01.irq", + "description": "real MEI uses separate ISR stack", + "evidence": "0x8000000b" + }, + { + "id": "ordering", + "number": 2, + "label": "pipeline finishes before ISR return target resumes", + "mode": "RUN", + "event_id": "E11", + "strategy_ref": "run.pipeline", + "svg_label": "02", + "code_ref": "src/tasks/task01_integration.c:443", + "snapshot_ref": "task01.stimulus-resumed", + "description": "pipeline finishes before ISR return target resumes", + "evidence": "done=1" + }, + { + "id": "deadline", + "number": 3, + "label": "heartbeat and completion stay within eight ticks", + "mode": "RUN", + "event_id": "E13", + "strategy_ref": "run.rendezvous", + "svg_label": "03", + "code_ref": "src/tasks/task01_integration.c:349", + "snapshot_ref": "task01.diagnostics", + "description": "heartbeat and completion stay within eight ticks", + "evidence": "completion tick <= start+8" + }, + { + "id": "heap", + "number": 4, + "label": "static app objects preserve current heap", + "mode": "RUN", + "event_id": "E13", + "strategy_ref": "run.rendezvous", + "svg_label": "04", + "code_ref": "src/tasks/task01_integration.c:351", + "snapshot_ref": "task01.diagnostics", + "description": "static app objects preserve current heap", + "evidence": "three equal heap readings" + }, + { + "id": "watermarks", + "number": 5, + "label": "six task contexts retain positive HWM", + "mode": "RUN", + "event_id": "E14", + "strategy_ref": "run.identity", + "svg_label": "05", + "code_ref": "src/tasks/task01_integration.c:392", + "snapshot_ref": "task01.pass", + "description": "six task contexts retain positive HWM", + "evidence": "acq/proc/pub/sup/stim/daemon" + }, + { + "id": "abi", + "number": 6, + "label": "ELF requires every selected primitive", + "mode": "CODE", + "strategy_ref": "code.identity", + "svg_label": "06", + "code_ref": "scripts/check_abi.sh:18", + "description": "ELF requires every selected primitive", + "evidence": "C only; exact symbols" + }, + { + "id": "digest", + "number": 7, + "label": "three clean images agree", + "mode": "RUN", + "event_id": "E14", + "strategy_ref": "run.identity", + "svg_label": "07", + "code_ref": "scripts/check_determinism.sh:14", + "snapshot_ref": "task01.pass", + "description": "three clean images agree", + "evidence": "8f767299" + } + ] + } + ] + } + } + ] + }, + { + "title": "A8 — Smallest justified mechanism", + "order": 80, + "content_kind": "prose", + "asset_page_mode": "one-per-page", + "page_orientation": "portrait", + "content_tex": "Notification carries a one-to-one wake, queues carry typed values, mutex protects a multi-writer snapshot, event bits join independent conditions, and the software timer supplies time-based control work.", + "assets": [ + { + "path": "assets/a8-patterns.png", + "html_path": "assets/a8-patterns.svg", + "source_path": "assets/a8-patterns.puml", + "caption": "A8 PATTERNS — choose by payload, fan-in, ownership and time.", + "label": "fig:a8-patterns", + "alt": "A8 · mechanism selection map", + "kind": "diagram", + "width": 1.0, + "page_grid": { + "columns": 1, + "rows": 1, + "page_width": 660, + "page_height": 760, + "overview": true, + "step_tiles": { + "notification": 1, + "queue": 1, + "mutex": 1, + "event-group": 1, + "timer": 1, + "proof": 1 + } + }, + "interactive": { + "kind": "uml-class", + "storage_key": "fc15-a8-patterns", + "title": "A8 · mechanism selection map", + "task": { + "id": "task01", + "label": "Task01 · integrated deterministic application" + }, + "block": { + "id": "a8", + "label": "A8 PATTERNS", + "description": "The architecture uses several primitives because each solves a different ownership problem, not because every learned API must appear." + }, + "phases": [ + { + "id": "choices", + "label": "PROBLEM → SMALLEST MECHANISM", + "steps": [ + { + "id": "notification", + "number": 1, + "label": "one ISR wakes one acquisition task", + "mode": "CODE", + "strategy_ref": "code.architecture", + "svg_label": "01", + "code_ref": "src/tasks/task01_integration.c:162", + "description": "one ISR wakes one acquisition task", + "evidence": "notification; no payload" + }, + { + "id": "queue", + "number": 2, + "label": "typed ownership crosses task boundaries", + "mode": "CODE", + "strategy_ref": "code.architecture", + "svg_label": "02", + "code_ref": "src/tasks/task01_integration.c:192", + "description": "typed ownership crosses task boundaries", + "evidence": "two value queues" + }, + { + "id": "mutex", + "number": 3, + "label": "two writers build one consistent snapshot", + "mode": "CODE", + "strategy_ref": "code.architecture", + "svg_label": "03", + "code_ref": "src/tasks/task01_integration.c:261", + "description": "two writers build one consistent snapshot", + "evidence": "publisher and daemon" + }, + { + "id": "event-group", + "number": 4, + "label": "supervisor joins independent conditions", + "mode": "CODE", + "strategy_ref": "code.architecture", + "svg_label": "04", + "code_ref": "src/tasks/task01_integration.c:332", + "description": "supervisor joins independent conditions", + "evidence": "wait ALL" + }, + { + "id": "timer", + "number": 5, + "label": "control work is scheduled by time", + "mode": "CODE", + "strategy_ref": "code.architecture", + "svg_label": "05", + "code_ref": "src/tasks/task01_integration.c:491", + "description": "control work is scheduled by time", + "evidence": "one-shot heartbeat" + }, + { + "id": "proof", + "number": 6, + "label": "one terminal validates all choices together", + "mode": "RUN", + "event_id": "E14", + "strategy_ref": "run.identity", + "svg_label": "06", + "code_ref": "src/tasks/task01_integration.c:358", + "snapshot_ref": "task01.pass", + "description": "one terminal validates all choices together", + "evidence": "no redundant transport" + } + ] + } + ] + } + } + ] + }, + { + "title": "Task01 — integrated deterministic application", + "order": 90, + "content_kind": "tasks", + "task_refs": [ + "task01" + ] + } + ], + "tasks": { + "task01": { + "title": "Prove one complete FreeRTOS C architecture", + "uuid": "fe92efeb-3c38-5975-86d8-ed630e1ad3bb", + "prompt_tex": "Odtwórz E01--E14 i dla każdego mechanizmu zapisz jedną odpowiedzialność. Następnie udowodnij ciąg input 7, suma kwadratów 140, publikacja, heartbeat w ticku 5 i terminal przed tickiem 8.", + "criterion": "PASS; real MEI; pipeline before stimulus resume; sum 140; result and heartbeat ALL-mask; completion by tick 8; zero application heap delta; positive stack HWM; deterministic digest.", + "conclusion_tex": "Poprawna architektura RTOS nie maksymalizuje liczby prymitywów. Każdy obiekt ma rozwiązywać inną granicę własności lub synchronizacji, a cały wybór musi być widoczny w jednym mierzalnym śladzie.", + "flow": [ + { + "kind": "block", + "id": "architecture", + "title": "A — architektura", + "content_tex": "Przypisz każdemu prymitywowi dokładnie jedną rolę.", + "steps": [ + { + "id": "owners", + "title": "Zapisz tabelę własności.", + "content_tex": "Payload, wake, shared snapshot, fan-in i time trigger nie są tym samym." + }, + { + "id": "predict", + "title": "Przewidź E07--E12.", + "content_tex": "Użyj priorytetów 6, 5, 4, 3, 2 i 1 do wyznaczenia kolejności." + } + ] + }, + { + "kind": "block", + "id": "replay", + "title": "B — replay", + "content_tex": "Zbierz jeden spójny dowód od sprzętu do diagnostyki.", + "steps": [ + { + "id": "startup", + "title": "Sprawdź E01--E06.", + "content_tex": "Statyczna pamięć, taski zablokowane i input gotowy." + }, + { + "id": "pipeline", + "title": "Sprawdź E07--E11.", + "content_tex": "IRQ, notification, dwie kolejki, wynik i natychmiastowy chain." + }, + { + "id": "health", + "title": "Sprawdź E12--E14.", + "content_tex": "Timer daemon, mutex, ALL-mask, deadline, HWM, heap i digest." + } + ] + }, + { + "kind": "exercise", + "id": "policy", + "title": "Ćwiczenie — zmiana polityki", + "prompt_tex": "Zmień wejście z 7 na 9 bez zmiany topologii. Wyznacz nową sumę kwadratów i checksum, zachowaj heartbeat oraz wszystkie kontrakty pamięci i kolejności.", + "evidence_tex": "Nowy typed payload, przewidywany Result, E06/E09/E10/E14 oraz niezmienione heap, HWM i deadline gates.", + "criterion": "Zmienia się wyłącznie polityka danych; architektura, własność, liczba zdarzeń i bramki bezpieczeństwa pozostają spójne.", + "based_on": [ + "architecture", + "replay" + ] + } + ], + "educational_requirement_refs": [ + "FC15.WE01" + ], + "learning_effect_refs": [ + "FC15.EN01", + "FC15.EK01" + ], + "assessment_criterion_ref": "FC15.KW01" + } + }, + "tasks_order": [ + "task01" + ] +} diff --git a/pdf/mpabi-inf-freertos-c-15-integration-v00.01-0092481f-af7c-517a-87f7-e0d7af7e5a0e.pdf b/pdf/mpabi-inf-freertos-c-15-integration-v00.01-0092481f-af7c-517a-87f7-e0d7af7e5a0e.pdf new file mode 100644 index 0000000..1bbf3c7 Binary files /dev/null and b/pdf/mpabi-inf-freertos-c-15-integration-v00.01-0092481f-af7c-517a-87f7-e0d7af7e5a0e.pdf differ