commit a185916c8237c1f90818a1378e6a3ab984c7d0cd Author: M. Pabiszczak <2+mpabi@noreply.zsl-gitea.mpabi.pl> Date: Mon Jul 20 08:47:31 2026 +0200 publish: FC13 uart-pipeline v00.01 diff --git a/json/card_source.json b/json/card_source.json new file mode 100644 index 0000000..ed1ed53 --- /dev/null +++ b/json/card_source.json @@ -0,0 +1,1548 @@ +{ + "$schema": "../../../tools/card-layouts/schemas/card-source.schema.json", + "schema": "esc-card-source.v1", + "card": { + "id": "mpabi-freertos-c-13-uart-pipeline", + "series": "freertos-c", + "series_title": "FreeRTOS C", + "number": "13", + "count": "15", + "slug": "uart-pipeline", + "title": "UART interrupt-to-task pipeline", + "topic": "bounded RX ISR, SPSC ring, task notification and frame ownership", + "project": "Freestanding C nad FreeRTOS", + "subject": "Informatyka", + "level": "Rok 2 · L13 · RV32I/Hazard3", + "revision_date": "2026-07-19T00:00:00+02:00", + "status": "Gotowa", + "version": "v00.01", + "uuid": "90a3638b-63f8-5a9c-8b5e-5de4b72ac534", + "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": "peripheral/ISR/task boundary", + "status": "enabled", + "target_label": "fig:a1-context" + }, + { + "id": "A2", + "label": "STRUCTURE", + "subtitle": "registers, ring and frame", + "status": "enabled", + "target_label": "fig:a2-structure" + }, + { + "id": "A3", + "label": "DISPATCH", + "subtitle": "FromISR notification", + "status": "enabled", + "target_label": "fig:a3-dispatch" + }, + { + "id": "A4", + "label": "APPLICATION", + "subtitle": "single pipeline", + "status": "unavailable", + "reason": "The concrete topology is already explicit in A1 and its ordered behavior is complete in A5." + }, + { + "id": "A5", + "label": "FLOW", + "subtitle": "valid and overflow replays", + "status": "enabled", + "target_label": "fig:a5-flow" + }, + { + "id": "A6", + "label": "STATE", + "subtitle": "ring and receiver states", + "status": "enabled", + "target_label": "fig:a6-state" + }, + { + "id": "A7", + "label": "RUNTIME", + "subtitle": "MMIO, indices, stacks and ELF", + "status": "enabled", + "target_label": "fig:a7-runtime" + }, + { + "id": "A8", + "label": "PATTERNS", + "subtitle": "SPSC is part of the mechanism", + "status": "unavailable", + "reason": "The SPSC decision is fully proved by A2 and A6; a separate pattern page would duplicate that contract." + } + ], + "debug_strategies": { + "code.contract": { + "id": "code.contract", + "kind": "code", + "action": "open", + "expected_observations": [ + "one producer and one consumer", + "parsing absent from ISR" + ], + "assertions": [ + "byte is visible before head", + "TX has one task owner" + ], + "evidence_fields": [ + "code_ref", + "owner", + "capacity", + "budget" + ], + "prerequisites": [ + "FC07 and FC10 complete" + ], + "layout": [ + "register bank", + "SPSC ring", + "ISR", + "receiver" + ], + "commands": [ + "rg -n 'FromISR|ring_|UART|tx_task_only' include src" + ] + }, + "run.pipeline": { + "id": "run.pipeline", + "kind": "run", + "action": "replay", + "expected_observations": [ + "OK newline produces ACK", + "receiver runs before stimulus resumes" + ], + "assertions": [ + "ISR processes three bytes", + "wake request is true", + "TX count is four" + ], + "evidence_fields": [ + "mcause", + "processed", + "head", + "tail", + "task state" + ], + "prerequisites": [ + "clean Hazard3 RAM", + "IRQ5 enabled" + ], + "layout": [ + "UART registers", + "ring", + "notification", + "events" + ], + "commands": [ + "make sim", + "print g_fc13", + "print g_fc13_events" + ] + }, + "run.overflow": { + "id": "run.overflow", + "kind": "run", + "action": "replay", + "expected_observations": [ + "seven bytes queued", + "three newest bytes dropped" + ], + "assertions": [ + "indices stay in range", + "task discards partial frame" + ], + "evidence_fields": [ + "processed", + "queued", + "dropped", + "frame_length" + ], + "prerequisites": [ + "first frame completed", + "empty ring" + ], + "layout": [ + "ten RX bytes", + "seven usable slots", + "drop counter" + ], + "commands": [ + "break fc13_checkpoint_committed if $a0 == 8", + "print g_fc13.ring" + ] + }, + "code.identity": { + "id": "code.identity", + "kind": "code", + "action": "open", + "expected_observations": [ + "C ISR and task symbols are present", + "no C++ runtime" + ], + "assertions": [ + "notification implementation is linked", + "external trap is linked" + ], + "evidence_fields": [ + "symbol", + "source blob", + "ELF SHA256", + "image SHA256" + ], + "prerequisites": [ + "built ELF" + ], + "layout": [ + "symbols", + "sections", + "artifact hashes" + ], + "commands": [ + "make check-abi", + "riscv64-unknown-elf-nm build/task01_uart/prog.elf" + ] + }, + "run.identity": { + "id": "run.identity", + "kind": "run", + "action": "replay", + "expected_observations": [ + "three identical logs", + "digest 6089cfff" + ], + "assertions": [ + "PASS occurs once", + "eleven events are ordered" + ], + "evidence_fields": [ + "digest", + "event count", + "SP", + "artifact identity" + ], + "prerequisites": [ + "built image" + ], + "layout": [ + "three clean processes", + "terminal digest" + ], + "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": "UART interrupt-to-task pipeline", + "url": "https://dce7fb9d-7b2f-5d49-96a2-3a30d3070b84.mpabi.pl/6a838fd1-ab1b-52b6-baaf-659120a4d60a", + "repository_url": "https://zsl-gitea.mpabi.pl/edu-freertos-c/lab-rv32i-freertos-c-uart", + "url_host_uuid": "dce7fb9d-7b2f-5d49-96a2-3a30d3070b84", + "url_domain": "mpabi.pl", + "doc_uuid": "6a838fd1-ab1b-52b6-baaf-659120a4d60a", + "revision": "v00.01", + "issued_on": "2026-07-19T00:00:00+02:00", + "series": "FREERTOS-C-13", + "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ń buduje ograniczoną ścieżkę UART RX: ISR przenosi bajty do ringa i budzi zadanie, a zadanie składa ramki i jako jedyne posiada TX.", + "scope_title": "Zakres karty", + "scope_content_tex": "Dwa prawdziwe external IRQ pokazują poprawną ramkę OK oraz przepełnienie: ring o ośmiu slotach udostępnia siedem, ISR odrzuca trzy najnowsze bajty, a zadanie kasuje niepełną ramkę.", + "scope_table": { + "headers": [ + "Lekcja", + "Task", + "Najważniejsza idea", + "Priorytet", + "Status", + "Version" + ], + "rows": [ + { + "chapter": "FC13", + "task": "Task01", + "idea_tex": "bounded RX ISR, SPSC ring, task notification and frame ownership", + "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": { + "FC13.EN01": { + "bloom_level": "Analiza", + "label": "UART handoff ownership", + "text": "Uczeń rozdziela bounded ISR, SPSC data transport, notification, task parsing and TX ownership.", + "assessment_criteria": [ + "FC13.KW01" + ] + }, + "FC13.EK01": { + "bloom_level": "Zastosowanie", + "label": "Valid frame and overflow replay", + "text": "Uczeń odtwarza E01–E11 and proves publication order, immediate wake and drop-newest recovery.", + "assessment_criteria": [ + "FC13.KW01" + ] + } + }, + "assessment_criteria": { + "FC13.KW01": { + "text": "PASS; two real IRQs; ISR budget <= 10; valid ACK; seven accepted and three dropped on overflow; no index or TX ownership violation; deterministic digest.", + "learning_effects": [ + "FC13.EN01", + "FC13.EK01" + ] + } + }, + "educational_requirements": { + "FC13.WE01": { + "text": "Projektowanie i badanie ograniczonej ścieżki UART od przerwania do zadania FreeRTOS C.", + "label": "bounded RX ISR, SPSC ring, task notification and frame ownership", + "learning_effects": [ + "FC13.EN01", + "FC13.EK01" + ], + "learning_tree": { + "schema": "we-learning-tree.v1", + "policy": "Każda aktywna kotwica wskazuje kod lub checkpoint.", + "ogolne": [ + { + "effect_ref": "FC13.EN01", + "display": "EN LOCAL RTOS.13", + "source": "LOCAL", + "official": "RTOS", + "local": "13", + "kind": "EN", + "tree_id": "FC13.WE01.OG.LOCAL.RTOS.13", + "text": "Uczeń rozdziela bounded ISR, SPSC data transport, notification, task parsing and TX ownership.", + "kw": [ + { + "criterion_ref": "FC13.KW01", + "display": "KW LOCAL RTOS.13", + "source": "LOCAL", + "kind": "KW", + "official": "RTOS", + "local": "13", + "text": "Łączy kod, diagram i zweryfikowany dowód." + } + ] + } + ], + "zawodowe": [ + { + "effect_ref": "FC13.EK01", + "display": "EK LOCAL RTOS.13", + "source": "LOCAL", + "official": "RTOS", + "local": "13", + "kind": "EK", + "tree_id": "FC13.WE01.TECH.LOCAL.RTOS.13", + "text": "Uczeń odtwarza E01–E11 and proves publication order, immediate wake and drop-newest recovery.", + "kw": [ + { + "criterion_ref": "FC13.KW01", + "display": "KW LOCAL RTOS.13", + "source": "LOCAL", + "kind": "KW", + "official": "RTOS", + "local": "13", + "text": "Łączy kod, diagram i zweryfikowany dowód." + } + ] + } + ] + } + } + }, + "debug_checkpoints": { + "schema": "stem-debug-checkpoints.v1", + "semantics": "deterministic-replay", + "artifact": { + "source": "src/tasks/task01_uart.c", + "source_git_blob": "7b446e7bd4b77a01171791c15d6f534476465c46", + "elf": "build/task01_uart/prog.elf", + "hazard3_elf_sha256": "8a74313a087efb2b0626d5134af0c1289d21761733aba3ad4c31a837c2ab4768", + "hazard3_image": "build/task01_uart/prog.bin", + "hazard3_image_sha256": "2d3d44fbf0485bd4169d52ad203d50607eebfa70784f9899e20df5ad8dfb08de" + }, + "targets": { + "hazard3-sim": { + "adapter": "hazard3-reset-load-replay.v1", + "baseline": "restart-backend", + "clean_ram": true + } + }, + "items": { + "task01.configured": { + "event_id": "E01", + "stop": { + "symbol": "fc13_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 1" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc13_event_count", + "equals": 1 + }, + { + "expr": "g_fc13_events[0].value", + "equals": 8 + } + ] + } + }, + "task01.receiver-ready": { + "event_id": "E02", + "stop": { + "symbol": "fc13_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 2" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc13.receiver_sp != 0", + "equals": 1 + }, + { + "expr": "g_fc13.good_frames", + "equals": 0 + } + ] + } + }, + "task01.good-injected": { + "event_id": "E03", + "stop": { + "symbol": "fc13_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 3" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc13.uart.rx_count", + "equals": 3 + }, + { + "expr": "g_fc13.first_done", + "equals": 0 + } + ] + } + }, + "task01.isr-entry": { + "event_id": "E04", + "stop": { + "symbol": "fc13_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 4" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc13.mcause", + "equals": 2147483659 + }, + { + "expr": "g_fc13.isr_sp != g_fc13.stimulus_sp", + "equals": 1 + } + ] + } + }, + "task01.good-isr": { + "event_id": "E05", + "stop": { + "symbol": "fc13_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 5" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc13.processed[0]", + "equals": 3 + }, + { + "expr": "g_fc13.wake_requested[0]", + "equals": 1 + }, + { + "expr": "g_fc13.ring.head", + "equals": 3 + } + ] + } + }, + "task01.frame": { + "event_id": "E06", + "stop": { + "symbol": "fc13_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 6" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc13.good_frames", + "equals": 1 + }, + { + "expr": "g_fc13.uart.tx_count", + "equals": 4 + }, + { + "expr": "g_fc13.stimulus_after_first", + "equals": 0 + } + ] + } + }, + "task01.overlong-injected": { + "event_id": "E07", + "stop": { + "symbol": "fc13_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 7" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc13.uart.rx_count", + "equals": 10 + }, + { + "expr": "g_fc13.first_done", + "equals": 1 + } + ] + } + }, + "task01.overflow-isr": { + "event_id": "E08", + "stop": { + "symbol": "fc13_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 8" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc13.processed[1]", + "equals": 10 + }, + { + "expr": "g_fc13.ring.dropped", + "equals": 3 + }, + { + "expr": "fc13_ring_used(&g_fc13.ring)", + "equals": 7 + } + ] + } + }, + "task01.overflow-task": { + "event_id": "E09", + "stop": { + "symbol": "fc13_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 9" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc13.overflow_frames", + "equals": 1 + }, + { + "expr": "g_fc13.frame_length", + "equals": 0 + }, + { + "expr": "g_fc13.ring.head == g_fc13.ring.tail", + "equals": 1 + } + ] + } + }, + "task01.stimulus-resumed": { + "event_id": "E10", + "stop": { + "symbol": "fc13_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 10" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc13.second_done_at_resume", + "equals": 1 + }, + { + "expr": "g_fc13.stimulus_after_second", + "equals": 1 + } + ] + } + }, + "task01.pass": { + "event_id": "E11", + "stop": { + "symbol": "fc13_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 11" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc13_pass", + "equals": 1 + }, + { + "expr": "g_fc13_event_count", + "equals": 11 + }, + { + "expr": "g_fc13.ring.dropped", + "equals": 3 + } + ] + } + } + } + }, + "sections": [ + { + "title": "A1 — Peripheral-to-task boundary", + "order": 10, + "content_kind": "prose", + "asset_page_mode": "one-per-page", + "page_orientation": "portrait", + "content_tex": "The ISR moves available bytes and wakes a task. Framing and TX remain outside interrupt context.", + "assets": [ + { + "path": "assets/a1-context.png", + "html_path": "assets/a1-context.svg", + "source_path": "assets/a1-context.puml", + "caption": "A1 CONTEXT — peripheral, ISR, ring, notification and receiver.", + "label": "fig:a1-context", + "alt": "A1 · UART responsibility boundary", + "kind": "diagram", + "width": 1.0, + "page_grid": { + "columns": 1, + "rows": 1, + "page_width": 660, + "page_height": 760, + "overview": true, + "step_tiles": { + "registers": 1, + "isr": 1, + "ring": 1, + "receiver": 1, + "pass": 1 + } + }, + "interactive": { + "kind": "uml-class", + "storage_key": "fc13-a1-context", + "title": "A1 · UART responsibility boundary", + "task": { + "id": "task01", + "label": "Task01 · UART ISR to frame task" + }, + "block": { + "id": "a1", + "label": "A1 CONTEXT", + "description": "UART registers, the interrupt path, a bounded handoff and task-only parsing have separate owners." + }, + "phases": [ + { + "id": "boundary", + "label": "PERIPHERAL / ISR / TASK", + "steps": [ + { + "id": "registers", + "number": 1, + "label": "UART register bank exposes RX state", + "mode": "CODE", + "strategy_ref": "code.contract", + "svg_label": "01", + "code_ref": "include/task01_uart.h:27", + "description": "UART register bank exposes RX state", + "evidence": "status, data and indices" + }, + { + "id": "isr", + "number": 2, + "label": "ISR owns bounded byte transfer", + "mode": "CODE", + "strategy_ref": "code.contract", + "svg_label": "02", + "code_ref": "src/tasks/task01_uart.c:159", + "description": "ISR owns bounded byte transfer", + "evidence": "at most ten bytes" + }, + { + "id": "ring", + "number": 3, + "label": "ring connects one producer and one consumer", + "mode": "CODE", + "strategy_ref": "code.contract", + "svg_label": "03", + "code_ref": "include/task01_uart_model.h:40", + "description": "ring connects one producer and one consumer", + "evidence": "publish byte before head" + }, + { + "id": "receiver", + "number": 4, + "label": "receiver owns parsing and TX", + "mode": "CODE", + "strategy_ref": "code.contract", + "svg_label": "04", + "code_ref": "src/tasks/task01_uart.c:207", + "description": "receiver owns parsing and TX", + "evidence": "no parser in ISR" + }, + { + "id": "pass", + "number": 5, + "label": "runtime validates the boundary", + "mode": "RUN", + "event_id": "E11", + "strategy_ref": "run.identity", + "svg_label": "05", + "code_ref": "src/tasks/task01_uart.c:346", + "snapshot_ref": "task01.pass", + "description": "runtime validates the boundary", + "evidence": "PASS and stable digest" + } + ] + } + ] + } + } + ] + }, + { + "title": "A2 — Register, ring and task state", + "order": 20, + "content_kind": "prose", + "asset_page_mode": "one-per-page", + "page_orientation": "portrait", + "content_tex": "An eight-slot ring keeps one slot empty. Head belongs to the ISR, tail to the receiver, and dropped counts rejected newest bytes.", + "assets": [ + { + "path": "assets/a2-structure.png", + "html_path": "assets/a2-structure.svg", + "source_path": "assets/a2-structure.puml", + "caption": "A2 STRUCTURE — register bank, seven usable ring slots and frame state.", + "label": "fig:a2-structure", + "alt": "A2 · bounded UART storage", + "kind": "diagram", + "width": 1.0, + "page_grid": { + "columns": 1, + "rows": 1, + "page_width": 660, + "page_height": 760, + "overview": true, + "step_tiles": { + "uart": 1, + "capacity": 1, + "push": 1, + "pop": 1, + "overflow": 1 + } + }, + "interactive": { + "kind": "uml-class", + "storage_key": "fc13-a2-structure", + "title": "A2 · bounded UART storage", + "task": { + "id": "task01", + "label": "Task01 · UART ISR to frame task" + }, + "block": { + "id": "a2", + "label": "A2 STRUCTURE", + "description": "The register bank, SPSC ring, frame scratch space and evidence trace have explicit storage and ownership." + }, + "phases": [ + { + "id": "storage", + "label": "BOUNDED STORAGE", + "steps": [ + { + "id": "uart", + "number": 1, + "label": "volatile UART fields model device state", + "mode": "CODE", + "strategy_ref": "code.contract", + "svg_label": "01", + "code_ref": "include/task01_uart.h:27", + "description": "volatile UART fields model device state", + "evidence": "RX capacity twelve" + }, + { + "id": "capacity", + "number": 2, + "label": "ring has eight slots and seven usable", + "mode": "CODE", + "strategy_ref": "code.contract", + "svg_label": "02", + "code_ref": "include/task01_uart_model.h:7", + "description": "ring has eight slots and seven usable", + "evidence": "empty slot disambiguates full" + }, + { + "id": "push", + "number": 3, + "label": "producer publishes data before head", + "mode": "CODE", + "strategy_ref": "code.contract", + "svg_label": "03", + "code_ref": "include/task01_uart_model.h:43", + "description": "producer publishes data before head", + "evidence": "single ISR producer" + }, + { + "id": "pop", + "number": 4, + "label": "consumer retires data before tail", + "mode": "CODE", + "strategy_ref": "code.contract", + "svg_label": "04", + "code_ref": "include/task01_uart_model.h:58", + "description": "consumer retires data before tail", + "evidence": "single task consumer" + }, + { + "id": "overflow", + "number": 5, + "label": "second IRQ fills seven and drops three", + "mode": "RUN", + "event_id": "E08", + "strategy_ref": "run.overflow", + "svg_label": "05", + "code_ref": "src/tasks/task01_uart.c:202", + "snapshot_ref": "task01.overflow-isr", + "description": "second IRQ fills seven and drops three", + "evidence": "used=7, dropped=3" + } + ] + } + ] + } + } + ] + }, + { + "title": "A3 — ISR-to-notification binding", + "order": 30, + "content_kind": "prose", + "asset_page_mode": "one-per-page", + "page_orientation": "portrait", + "content_tex": "Only the FromISR notification API appears in the handler; the receiver blocks with the matching task-context take.", + "assets": [ + { + "path": "assets/a3-dispatch.png", + "html_path": "assets/a3-dispatch.svg", + "source_path": "assets/a3-dispatch.puml", + "caption": "A3 DISPATCH — MEI, bounded drain, notify and immediate task restore.", + "label": "fig:a3-dispatch", + "alt": "A3 · interrupt dispatch", + "kind": "diagram", + "width": 1.0, + "page_grid": { + "columns": 1, + "rows": 1, + "page_width": 660, + "page_height": 760, + "overview": true, + "step_tiles": { + "vector": 1, + "entry": 1, + "budget": 1, + "notify": 1, + "yield": 1, + "receiver-first": 1 + } + }, + "interactive": { + "kind": "uml-class", + "storage_key": "fc13-a3-dispatch", + "title": "A3 · interrupt dispatch", + "task": { + "id": "task01", + "label": "Task01 · UART ISR to frame task" + }, + "block": { + "id": "a3", + "label": "A3 DISPATCH", + "description": "The real external interrupt enters the FreeRTOS trap path, clears its source, notifies once and yields once." + }, + "phases": [ + { + "id": "dispatch", + "label": "IRQ / FROMISR / RESTORE", + "steps": [ + { + "id": "vector", + "number": 1, + "label": "external vector enters the port trap", + "mode": "CODE", + "strategy_ref": "code.contract", + "svg_label": "01", + "code_ref": "src/common/hazard3_freertos_traps.S:24", + "description": "external vector enters the port trap", + "evidence": "full context save" + }, + { + "id": "entry", + "number": 2, + "label": "first IRQ records MEI and ISR stack", + "mode": "RUN", + "event_id": "E04", + "strategy_ref": "run.pipeline", + "svg_label": "02", + "code_ref": "src/tasks/task01_uart.c:166", + "snapshot_ref": "task01.isr-entry", + "description": "first IRQ records MEI and ISR stack", + "evidence": "mcause is machine external interrupt" + }, + { + "id": "budget", + "number": 3, + "label": "loop obeys a ten-byte budget", + "mode": "CODE", + "strategy_ref": "code.contract", + "svg_label": "03", + "code_ref": "src/tasks/task01_uart.c:174", + "description": "loop obeys a ten-byte budget", + "evidence": "bounded ISR work" + }, + { + "id": "notify", + "number": 4, + "label": "one FromISR give merges wake request", + "mode": "CODE", + "strategy_ref": "code.contract", + "svg_label": "04", + "code_ref": "src/tasks/task01_uart.c:189", + "description": "one FromISR give merges wake request", + "evidence": "higher-priority task ready" + }, + { + "id": "yield", + "number": 5, + "label": "port performs one requested yield", + "mode": "CODE", + "strategy_ref": "code.contract", + "svg_label": "05", + "code_ref": "src/tasks/task01_uart.c:202", + "description": "port performs one requested yield", + "evidence": "receiver restored first" + }, + { + "id": "receiver-first", + "number": 6, + "label": "receiver completes before stimulus resumes", + "mode": "RUN", + "event_id": "E06", + "strategy_ref": "run.pipeline", + "svg_label": "06", + "code_ref": "src/tasks/task01_uart.c:256", + "snapshot_ref": "task01.frame", + "description": "receiver completes before stimulus resumes", + "evidence": "stimulus_after_first=0" + } + ] + } + ] + } + } + ] + }, + { + "title": "A5 — Two-frame replay", + "order": 50, + "content_kind": "prose", + "asset_page_mode": "one-per-page", + "page_orientation": "portrait", + "content_tex": "The first interrupt delivers OK plus newline and produces ACK. The second presents ten bytes, accepts seven, drops three and discards the partial frame in task context.", + "assets": [ + { + "path": "assets/a5-flow.png", + "html_path": "assets/a5-flow.svg", + "source_path": "assets/a5-flow.puml", + "caption": "A5 FLOW — E01–E11 from configuration to verified PASS.", + "label": "fig:a5-flow", + "alt": "A5 · UART pipeline replay", + "kind": "diagram", + "width": 1.0, + "page_grid": { + "columns": 1, + "rows": 1, + "page_width": 660, + "page_height": 760, + "overview": true, + "step_tiles": { + "config": 1, + "wait": 1, + "inject": 1, + "isr-entry-flow": 1, + "isr-good": 1, + "frame": 1, + "overlong": 1, + "drop": 1, + "discard": 1, + "resume": 1, + "verified": 1 + } + }, + "interactive": { + "kind": "uml-sequence", + "storage_key": "fc13-a5-flow", + "title": "A5 · UART pipeline replay", + "task": { + "id": "task01", + "label": "Task01 · UART ISR to frame task" + }, + "block": { + "id": "a5", + "label": "A5 FLOW", + "description": "Eleven committed events cover one valid frame and one deterministic overflow fixture." + }, + "phases": [ + { + "id": "flow", + "label": "VALID FRAME / OVERFLOW / PASS", + "steps": [ + { + "id": "config", + "number": 1, + "label": "configure IRQ and eight-slot ring", + "mode": "RUN", + "event_id": "E01", + "strategy_ref": "run.pipeline", + "svg_label": "01", + "code_ref": "src/tasks/task01_uart.c:411", + "snapshot_ref": "task01.configured", + "description": "configure IRQ and eight-slot ring", + "evidence": "capacity=8" + }, + { + "id": "wait", + "number": 2, + "label": "receiver reaches notification wait", + "mode": "RUN", + "event_id": "E02", + "strategy_ref": "run.pipeline", + "svg_label": "02", + "code_ref": "src/tasks/task01_uart.c:219", + "snapshot_ref": "task01.receiver-ready", + "description": "receiver reaches notification wait", + "evidence": "receiver priority 3" + }, + { + "id": "inject", + "number": 3, + "label": "stimulus publishes OK newline", + "mode": "RUN", + "event_id": "E03", + "strategy_ref": "run.pipeline", + "svg_label": "03", + "code_ref": "src/tasks/task01_uart.c:294", + "snapshot_ref": "task01.good-injected", + "description": "stimulus publishes OK newline", + "evidence": "three RX bytes" + }, + { + "id": "isr-entry-flow", + "number": 4, + "label": "external IRQ enters handler", + "mode": "RUN", + "event_id": "E04", + "strategy_ref": "run.pipeline", + "svg_label": "04", + "code_ref": "src/tasks/task01_uart.c:166", + "snapshot_ref": "task01.isr-entry", + "description": "external IRQ enters handler", + "evidence": "MEI and ISR SP" + }, + { + "id": "isr-good", + "number": 5, + "label": "ISR queues three and requests wake", + "mode": "RUN", + "event_id": "E05", + "strategy_ref": "run.pipeline", + "svg_label": "05", + "code_ref": "src/tasks/task01_uart.c:197", + "snapshot_ref": "task01.good-isr", + "description": "ISR queues three and requests wake", + "evidence": "processed=3" + }, + { + "id": "frame", + "number": 6, + "label": "task validates frame and owns ACK", + "mode": "RUN", + "event_id": "E06", + "strategy_ref": "run.pipeline", + "svg_label": "06", + "code_ref": "src/tasks/task01_uart.c:238", + "snapshot_ref": "task01.frame", + "description": "task validates frame and owns ACK", + "evidence": "good_frames=1" + }, + { + "id": "overlong", + "number": 7, + "label": "stimulus publishes ten X bytes", + "mode": "RUN", + "event_id": "E07", + "strategy_ref": "run.pipeline", + "svg_label": "07", + "code_ref": "src/tasks/task01_uart.c:306", + "snapshot_ref": "task01.overlong-injected", + "description": "stimulus publishes ten X bytes", + "evidence": "receiver already done" + }, + { + "id": "drop", + "number": 8, + "label": "ISR accepts seven and drops three", + "mode": "RUN", + "event_id": "E08", + "strategy_ref": "run.pipeline", + "svg_label": "08", + "code_ref": "src/tasks/task01_uart.c:202", + "snapshot_ref": "task01.overflow-isr", + "description": "ISR accepts seven and drops three", + "evidence": "drop-newest" + }, + { + "id": "discard", + "number": 9, + "label": "task discards partial overflow frame", + "mode": "RUN", + "event_id": "E09", + "strategy_ref": "run.pipeline", + "svg_label": "09", + "code_ref": "src/tasks/task01_uart.c:249", + "snapshot_ref": "task01.overflow-task", + "description": "task discards partial overflow frame", + "evidence": "overflow_frames=1" + }, + { + "id": "resume", + "number": 10, + "label": "stimulus resumes after receiver", + "mode": "RUN", + "event_id": "E10", + "strategy_ref": "run.pipeline", + "svg_label": "10", + "code_ref": "src/tasks/task01_uart.c:315", + "snapshot_ref": "task01.stimulus-resumed", + "description": "stimulus resumes after receiver", + "evidence": "second_done=1" + }, + { + "id": "verified", + "number": 11, + "label": "verifier commits deterministic PASS", + "mode": "RUN", + "event_id": "E11", + "strategy_ref": "run.identity", + "svg_label": "11", + "code_ref": "src/tasks/task01_uart.c:376", + "snapshot_ref": "task01.pass", + "description": "verifier commits deterministic PASS", + "evidence": "digest 6089cfff" + } + ] + } + ] + } + } + ] + }, + { + "title": "A6 — Ring and receiver states", + "order": 60, + "content_kind": "prose", + "asset_page_mode": "one-per-page", + "page_orientation": "portrait", + "content_tex": "Notification is a wake signal, not the byte container. The ring carries data; the receiver drains all published bytes after each wake.", + "assets": [ + { + "path": "assets/a6-state.png", + "html_path": "assets/a6-state.svg", + "source_path": "assets/a6-state.puml", + "caption": "A6 STATE — empty, filling, notified, draining and overflow recovery.", + "label": "fig:a6-state", + "alt": "A6 · ring and task state", + "kind": "diagram", + "width": 1.0, + "page_grid": { + "columns": 1, + "rows": 1, + "page_width": 660, + "page_height": 760, + "overview": true, + "step_tiles": { + "empty": 1, + "filled": 1, + "drained": 1, + "full": 1, + "recovered": 1 + } + }, + "interactive": { + "kind": "uml-class", + "storage_key": "fc13-a6-state", + "title": "A6 · ring and task state", + "task": { + "id": "task01", + "label": "Task01 · UART ISR to frame task" + }, + "block": { + "id": "a6", + "label": "A6 STATE", + "description": "Ring occupancy and receiver state change independently but obey one publication contract." + }, + "phases": [ + { + "id": "state", + "label": "RING / NOTIFICATION / FRAME", + "steps": [ + { + "id": "empty", + "number": 1, + "label": "empty ring and blocked receiver", + "mode": "RUN", + "event_id": "E03", + "strategy_ref": "run.pipeline", + "svg_label": "01", + "code_ref": "src/tasks/task01_uart.c:297", + "snapshot_ref": "task01.good-injected", + "description": "empty ring and blocked receiver", + "evidence": "head=tail before IRQ" + }, + { + "id": "filled", + "number": 2, + "label": "three bytes published before notify", + "mode": "RUN", + "event_id": "E05", + "strategy_ref": "run.pipeline", + "svg_label": "02", + "code_ref": "src/tasks/task01_uart.c:174", + "snapshot_ref": "task01.good-isr", + "description": "three bytes published before notify", + "evidence": "used=3" + }, + { + "id": "drained", + "number": 3, + "label": "receiver drains and returns to wait", + "mode": "RUN", + "event_id": "E06", + "strategy_ref": "run.pipeline", + "svg_label": "03", + "code_ref": "src/tasks/task01_uart.c:229", + "snapshot_ref": "task01.frame", + "description": "receiver drains and returns to wait", + "evidence": "head=tail" + }, + { + "id": "full", + "number": 4, + "label": "second IRQ reaches seven usable slots", + "mode": "RUN", + "event_id": "E08", + "strategy_ref": "run.pipeline", + "svg_label": "04", + "code_ref": "include/task01_uart_model.h:47", + "snapshot_ref": "task01.overflow-isr", + "description": "second IRQ reaches seven usable slots", + "evidence": "dropped=3" + }, + { + "id": "recovered", + "number": 5, + "label": "receiver resets partial frame", + "mode": "RUN", + "event_id": "E09", + "strategy_ref": "run.pipeline", + "svg_label": "05", + "code_ref": "src/tasks/task01_uart.c:249", + "snapshot_ref": "task01.overflow-task", + "description": "receiver resets partial frame", + "evidence": "frame length zero" + } + ] + } + ] + } + } + ] + }, + { + "title": "A7 — Runtime and artifact proof", + "order": 70, + "content_kind": "prose", + "asset_page_mode": "one-per-page", + "page_orientation": "portrait", + "content_tex": "Three clean simulator processes must produce the same terminal digest. ABI checks reject C++ and require the trap, notification and task boundaries.", + "assets": [ + { + "path": "assets/a7-runtime.png", + "html_path": "assets/a7-runtime.svg", + "source_path": "assets/a7-runtime.puml", + "caption": "A7 RUNTIME — cause, stacks, indices, symbols and deterministic 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": { + "cause": 1, + "indices": 1, + "stacks": 1, + "abi": 1, + "determinism": 1 + } + }, + "interactive": { + "kind": "uml-class", + "storage_key": "fc13-a7-runtime", + "title": "A7 · runtime proof", + "task": { + "id": "task01", + "label": "Task01 · UART ISR to frame task" + }, + "block": { + "id": "a7", + "label": "A7 RUNTIME", + "description": "The proof combines register values, ring indices, three stack contexts, event order and exact C artifact identity." + }, + "phases": [ + { + "id": "runtime", + "label": "RUNTIME EVIDENCE", + "steps": [ + { + "id": "cause", + "number": 1, + "label": "mcause proves a real external IRQ", + "mode": "RUN", + "event_id": "E04", + "strategy_ref": "run.pipeline", + "svg_label": "01", + "code_ref": "src/tasks/task01_uart.c:167", + "snapshot_ref": "task01.isr-entry", + "description": "mcause proves a real external IRQ", + "evidence": "0x8000000b" + }, + { + "id": "indices", + "number": 2, + "label": "head and tail stay inside capacity", + "mode": "RUN", + "event_id": "E09", + "strategy_ref": "run.pipeline", + "svg_label": "02", + "code_ref": "src/tasks/task01_uart.c:266", + "snapshot_ref": "task01.overflow-task", + "description": "head and tail stay inside capacity", + "evidence": "ring empty after drain" + }, + { + "id": "stacks", + "number": 3, + "label": "ISR, receiver and stimulus stacks differ", + "mode": "RUN", + "event_id": "E11", + "strategy_ref": "run.identity", + "svg_label": "03", + "code_ref": "src/tasks/task01_uart.c:373", + "snapshot_ref": "task01.pass", + "description": "ISR, receiver and stimulus stacks differ", + "evidence": "three SP values" + }, + { + "id": "abi", + "number": 4, + "label": "ELF exposes C and FromISR boundaries", + "mode": "CODE", + "strategy_ref": "code.identity", + "svg_label": "04", + "code_ref": "scripts/check_abi.sh:18", + "description": "ELF exposes C and FromISR boundaries", + "evidence": "no C++ or unwind" + }, + { + "id": "determinism", + "number": 5, + "label": "three clean runs agree", + "mode": "RUN", + "event_id": "E11", + "strategy_ref": "run.identity", + "svg_label": "05", + "code_ref": "scripts/check_determinism.sh:14", + "snapshot_ref": "task01.pass", + "description": "three clean runs agree", + "evidence": "identical digest" + } + ] + } + ] + } + } + ] + }, + { + "title": "Task01 — UART ISR to frame task", + "order": 90, + "content_kind": "tasks", + "task_refs": [ + "task01" + ] + } + ], + "tasks": { + "task01": { + "title": "Build and prove a bounded UART RX pipeline", + "uuid": "6a838fd1-ab1b-52b6-baaf-659120a4d60a", + "prompt_tex": "Odtwórz E01--E11. Udowodnij, że ISR tylko przenosi bajty i budzi zadanie, a parser oraz TX działają wyłącznie w kontekście zadania.", + "criterion": "PASS; two real IRQs; ISR budget <= 10; valid ACK; seven accepted and three dropped on overflow; no index or TX ownership violation; deterministic digest.", + "conclusion_tex": "Notyfikacja przenosi informację o pracy, nie bajty. Dane mają osobny ograniczony ring; kolejność publikacji, budżet ISR i jawna polityka przepełnienia są częścią kontraktu.", + "flow": [ + { + "kind": "block", + "id": "contract", + "title": "A — kontrakt", + "content_tex": "Rozdziel właścicieli rejestrów, indeksów, parsera i TX.", + "steps": [ + { + "id": "owners", + "title": "Zapisz tabelę własności.", + "content_tex": "ISR zapisuje head; zadanie zapisuje tail i stan ramki." + }, + { + "id": "predict", + "title": "Przewidź dwa przebiegi.", + "content_tex": "Wyznacz zajętość ringa dla trzech i dziesięciu bajtów." + } + ] + }, + { + "kind": "block", + "id": "replay", + "title": "B — replay", + "content_tex": "Powiąż każdy RUN z jednym zatwierdzonym eventem.", + "steps": [ + { + "id": "valid", + "title": "Sprawdź E03--E06.", + "content_tex": "Trzy bajty, wake request, ACK i natychmiastowy receiver." + }, + { + "id": "overflow", + "title": "Sprawdź E07--E10.", + "content_tex": "Siedem zaakceptowanych, trzy odrzucone i reset ramki." + }, + { + "id": "identity", + "title": "Sprawdź E11.", + "content_tex": "ABI, trzy stosy, kolejność i digest." + } + ] + }, + { + "kind": "exercise", + "id": "policy", + "title": "Ćwiczenie — polityka przepełnienia", + "prompt_tex": "Zmień wyłącznie politykę z drop-newest na drop-oldest. Zapisz nowy kontrakt indeksów i przewidź, które siedem z dziesięciu bajtów odczyta zadanie.", + "evidence_tex": "Tabela bajtów wejściowych, head/tail przed i po IRQ, drop counter oraz ślad zadania.", + "criterion": "Uczeń zachowuje bounded ISR, nie publikuje indeksu przed bajtem i potrafi wskazać utracone dane.", + "based_on": [ + "contract", + "replay" + ] + } + ], + "educational_requirement_refs": [ + "FC13.WE01" + ], + "learning_effect_refs": [ + "FC13.EN01", + "FC13.EK01" + ], + "assessment_criterion_ref": "FC13.KW01" + } + }, + "tasks_order": [ + "task01" + ] +} diff --git a/pdf/mpabi-inf-freertos-c-13-uart-pipeline-v00.01-90a3638b-63f8-5a9c-8b5e-5de4b72ac534.pdf b/pdf/mpabi-inf-freertos-c-13-uart-pipeline-v00.01-90a3638b-63f8-5a9c-8b5e-5de4b72ac534.pdf new file mode 100644 index 0000000..b59f69e Binary files /dev/null and b/pdf/mpabi-inf-freertos-c-13-uart-pipeline-v00.01-90a3638b-63f8-5a9c-8b5e-5de4b72ac534.pdf differ