commit a90c26737adcdb713f9a2ef0adfdc1de97705c15 Author: M. Pabiszczak <2+mpabi@noreply.zsl-gitea.mpabi.pl> Date: Mon Jul 20 08:47:34 2026 +0200 publish: FC14 gpio-timer-deferred v00.01 diff --git a/json/card_source.json b/json/card_source.json new file mode 100644 index 0000000..06a8400 --- /dev/null +++ b/json/card_source.json @@ -0,0 +1,1438 @@ +{ + "$schema": "../../../tools/card-layouts/schemas/card-source.schema.json", + "schema": "esc-card-source.v1", + "card": { + "id": "mpabi-freertos-c-14-gpio-timer-deferred", + "series": "freertos-c", + "series_title": "FreeRTOS C", + "number": "14", + "count": "15", + "slug": "gpio-timer-deferred", + "title": "GPIO, hardware timer and deferred work", + "topic": "mtime tick ISR, pended daemon callback and one bounded GPIO transition", + "project": "Freestanding C nad FreeRTOS", + "subject": "Informatyka", + "level": "Rok 2 · L14 · RV32I/Hazard3", + "revision_date": "2026-07-19T00:00:00+02:00", + "status": "Gotowa", + "version": "v00.01", + "uuid": "7de92b94-df89-5c00-be47-d85523ad02ac", + "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": "hardware/ISR/daemon boundary", + "status": "enabled", + "target_label": "fig:a1-context" + }, + { + "id": "A2", + "label": "STRUCTURE", + "subtitle": "event and register records", + "status": "enabled", + "target_label": "fig:a2-structure" + }, + { + "id": "A3", + "label": "DISPATCH", + "subtitle": "pended callback binding", + "status": "enabled", + "target_label": "fig:a3-dispatch" + }, + { + "id": "A4", + "label": "APPLICATION", + "subtitle": "single event topology", + "status": "unavailable", + "reason": "A1 already identifies every application participant and A5 provides the complete concrete topology in time." + }, + { + "id": "A5", + "label": "FLOW", + "subtitle": "E01-E06 hardware replay", + "status": "enabled", + "target_label": "fig:a5-flow" + }, + { + "id": "A6", + "label": "STATE", + "subtitle": "pending and applied states", + "status": "enabled", + "target_label": "fig:a6-state" + }, + { + "id": "A7", + "label": "RUNTIME", + "subtitle": "mtime, stacks and ELF", + "status": "enabled", + "target_label": "fig:a7-runtime" + }, + { + "id": "A8", + "label": "PATTERNS", + "subtitle": "deferred interrupt processing", + "status": "unavailable", + "reason": "Deferred interrupt processing is the mechanism proved in A3 and A6; a separate page would repeat the same decision." + } + ], + "debug_strategies": { + "code.contract": { + "id": "code.contract", + "kind": "code", + "action": "open", + "expected_observations": [ + "ISR and callback are separate functions", + "one GPIO owner" + ], + "assertions": [ + "hook never blocks", + "callback arguments outlive the ISR" + ], + "evidence_fields": [ + "code_ref", + "priority", + "register", + "API" + ], + "prerequisites": [ + "FC06 and FC07 complete" + ], + "layout": [ + "mtime port", + "tick hook", + "timer queue", + "daemon callback", + "GPIO" + ], + "commands": [ + "rg -n 'TickHook|PendFunction|MTIME|gpio' include src Makefile" + ] + }, + "run.timer": { + "id": "run.timer", + "kind": "run", + "action": "replay", + "expected_observations": [ + "E03 at target tick", + "pend returns pdPASS and wake true" + ], + "assertions": [ + "mcause is MTI", + "compare was reloaded", + "one command accepted" + ], + "evidence_fields": [ + "tick", + "mtime", + "mtimecmp", + "mcause", + "pend result", + "ISR SP" + ], + "prerequisites": [ + "clean Hazard3 RAM", + "target tick armed" + ], + "layout": [ + "mtime", + "mtimecmp", + "mcause", + "timer command queue" + ], + "commands": [ + "make sim", + "print g_fc14", + "print g_fc14_events" + ] + }, + "run.daemon": { + "id": "run.daemon", + "kind": "run", + "action": "replay", + "expected_observations": [ + "callback at same tick", + "GPIO low-to-high once" + ], + "assertions": [ + "daemon handle matches", + "E04 precedes E05", + "callback stack differs from ISR" + ], + "evidence_fields": [ + "TaskHandle_t", + "SP", + "tick", + "GPIO before/after", + "transition count" + ], + "prerequisites": [ + "E03 command queued", + "daemon priority 3" + ], + "layout": [ + "daemon handle", + "callback arguments", + "GPIO bank", + "event order" + ], + "commands": [ + "break fc14_checkpoint_committed if $a0 == 4", + "print g_fc14" + ] + }, + "code.identity": { + "id": "code.identity", + "kind": "code", + "action": "open", + "expected_observations": [ + "all C boundaries are linked", + "no C++ metadata" + ], + "assertions": [ + "timer task implementation is present", + "pended function API is present" + ], + "evidence_fields": [ + "symbol", + "source blob", + "ELF SHA256", + "image SHA256" + ], + "prerequisites": [ + "built ELF" + ], + "layout": [ + "trap", + "tick", + "timer daemon", + "application symbols" + ], + "commands": [ + "make check-abi", + "riscv64-unknown-elf-nm build/task01_gpio_timer/prog.elf" + ] + }, + "run.identity": { + "id": "run.identity", + "kind": "run", + "action": "replay", + "expected_observations": [ + "one PASS", + "digest bf66bc48 three times" + ], + "assertions": [ + "six ordered events", + "exactly one GPIO transition" + ], + "evidence_fields": [ + "digest", + "event count", + "SP values", + "artifact identity" + ], + "prerequisites": [ + "built image" + ], + "layout": [ + "six-event trace", + "three clean processes" + ], + "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": "GPIO, hardware timer and deferred work", + "url": "https://dce7fb9d-7b2f-5d49-96a2-3a30d3070b84.mpabi.pl/0cc561df-bf81-5bba-9df1-c872d5b42eb8", + "repository_url": "https://zsl-gitea.mpabi.pl/edu-freertos-c/lab-rv32i-freertos-c-gpio-timer", + "url_host_uuid": "dce7fb9d-7b2f-5d49-96a2-3a30d3070b84", + "url_domain": "mpabi.pl", + "doc_uuid": "0cc561df-bf81-5bba-9df1-c872d5b42eb8", + "revision": "v00.01", + "issued_on": "2026-07-19T00:00:00+02:00", + "series": "FREERTOS-C-14", + "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ń odróżnia hardware timer interrupt od callbacku software timera: ISR tylko zatwierdza zdarzenie i odkłada pracę, a timer daemon wykonuje ograniczoną zmianę GPIO.", + "scope_title": "Zakres karty", + "scope_content_tex": "Stimulus uzbraja tick +3. Machine timer ISR zapisuje mtime, mtimecmp, mcause i stos, po czym wywołuje xTimerPendFunctionCallFromISR. Daemon priority 3 przełącza GPIO przed powrotem do przerwanego taska priority 2.", + "scope_table": { + "headers": [ + "Lekcja", + "Task", + "Najważniejsza idea", + "Priorytet", + "Status", + "Version" + ], + "rows": [ + { + "chapter": "FC14", + "task": "Task01", + "idea_tex": "mtime tick ISR, pended daemon callback and one bounded GPIO transition", + "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": { + "FC14.EN01": { + "bloom_level": "Analiza", + "label": "Hardware timer versus deferred callback", + "text": "Uczeń rozdziela machine timer ISR, tick hook, timer command queue, daemon task and GPIO owner.", + "assessment_criteria": [ + "FC14.KW01" + ] + }, + "FC14.EK01": { + "bloom_level": "Zastosowanie", + "label": "One-event deferred-work replay", + "text": "Uczeń odtwarza E01–E06 i dowodzi kolejności ISR → daemon → interrupted task.", + "assessment_criteria": [ + "FC14.KW01" + ] + } + }, + "assessment_criteria": { + "FC14.KW01": { + "text": "PASS; mcause=MTI; mtimecmp>mtime; one successful pend; daemon callback in target tick; one GPIO transition; three distinct stacks; deterministic digest.", + "learning_effects": [ + "FC14.EN01", + "FC14.EK01" + ] + } + }, + "educational_requirements": { + "FC14.WE01": { + "text": "Projektowanie i badanie deferred interrupt processing dla timera sprzętowego i GPIO w FreeRTOS C.", + "label": "mtime tick ISR, pended daemon callback and one bounded GPIO transition", + "learning_effects": [ + "FC14.EN01", + "FC14.EK01" + ], + "learning_tree": { + "schema": "we-learning-tree.v1", + "policy": "Każda aktywna kotwica wskazuje kod lub checkpoint.", + "ogolne": [ + { + "effect_ref": "FC14.EN01", + "display": "EN LOCAL RTOS.14", + "source": "LOCAL", + "official": "RTOS", + "local": "14", + "kind": "EN", + "tree_id": "FC14.WE01.OG.LOCAL.RTOS.14", + "text": "Uczeń rozdziela machine timer ISR, tick hook, timer command queue, daemon task and GPIO owner.", + "kw": [ + { + "criterion_ref": "FC14.KW01", + "display": "KW LOCAL RTOS.14", + "source": "LOCAL", + "kind": "KW", + "official": "RTOS", + "local": "14", + "text": "Łączy kod, diagram i zweryfikowany dowód." + } + ] + } + ], + "zawodowe": [ + { + "effect_ref": "FC14.EK01", + "display": "EK LOCAL RTOS.14", + "source": "LOCAL", + "official": "RTOS", + "local": "14", + "kind": "EK", + "tree_id": "FC14.WE01.TECH.LOCAL.RTOS.14", + "text": "Uczeń odtwarza E01–E06 i dowodzi kolejności ISR → daemon → interrupted task.", + "kw": [ + { + "criterion_ref": "FC14.KW01", + "display": "KW LOCAL RTOS.14", + "source": "LOCAL", + "kind": "KW", + "official": "RTOS", + "local": "14", + "text": "Łączy kod, diagram i zweryfikowany dowód." + } + ] + } + ] + } + } + }, + "debug_checkpoints": { + "schema": "stem-debug-checkpoints.v1", + "semantics": "deterministic-replay", + "artifact": { + "source": "src/tasks/task01_gpio_timer.c", + "source_git_blob": "ec2e552d61694b31bbe65af1ec361442980de23b", + "elf": "build/task01_gpio_timer/prog.elf", + "hazard3_elf_sha256": "dde14e1ccc2ad816883b45a7cd9a1b431f157c1509abe02b9f6559e53365d619", + "hazard3_image": "build/task01_gpio_timer/prog.bin", + "hazard3_image_sha256": "3ffeec5e5e362efdd714ef9d354b1e3592a183bda582c6fb21be63736fb7a92d" + }, + "targets": { + "hazard3-sim": { + "adapter": "hazard3-reset-load-replay.v1", + "baseline": "restart-backend", + "clean_ram": true + } + }, + "items": { + "task01.configured": { + "event_id": "E01", + "stop": { + "symbol": "fc14_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 1" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc14_event_count", + "equals": 1 + }, + { + "expr": "g_fc14.gpio.direction", + "equals": 1 + }, + { + "expr": "g_fc14_events[0].value", + "equals": 3 + } + ] + } + }, + "task01.armed": { + "event_id": "E02", + "stop": { + "symbol": "fc14_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 2" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc14.armed", + "equals": 1 + }, + { + "expr": "g_fc14.pended", + "equals": 0 + }, + { + "expr": "g_fc14.target_tick == g_fc14_events[1].value", + "equals": 1 + } + ] + } + }, + "task01.tick-isr": { + "event_id": "E03", + "stop": { + "symbol": "fc14_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 3" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc14.mcause", + "equals": 2147483655 + }, + { + "expr": "g_fc14.pend_result", + "equals": 1 + }, + { + "expr": "g_fc14.higher_priority_task_woken", + "equals": 1 + }, + { + "expr": "g_fc14.mtimecmp_after_reload > g_fc14.mtime_at_isr", + "equals": 1 + } + ] + } + }, + "task01.callback": { + "event_id": "E04", + "stop": { + "symbol": "fc14_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 4" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc14.callback_calls", + "equals": 1 + }, + { + "expr": "g_fc14.gpio.data", + "equals": 1 + }, + { + "expr": "g_fc14.gpio.transitions", + "equals": 1 + }, + { + "expr": "g_fc14.callback_saw_stimulus_after", + "equals": 0 + } + ] + } + }, + "task01.stimulus-resumed": { + "event_id": "E05", + "stop": { + "symbol": "fc14_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 5" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc14.applied_at_stimulus_resume", + "equals": 1 + }, + { + "expr": "g_fc14.stimulus_after", + "equals": 1 + } + ] + } + }, + "task01.pass": { + "event_id": "E06", + "stop": { + "symbol": "fc14_checkpoint_committed", + "offset": 0, + "condition": "$a0 == 6" + }, + "verify": { + "expressions": [ + { + "expr": "g_fc14_pass", + "equals": 1 + }, + { + "expr": "g_fc14_event_count", + "equals": 6 + }, + { + "expr": "g_fc14.pend_calls", + "equals": 1 + }, + { + "expr": "g_fc14.callback_calls", + "equals": 1 + } + ] + } + } + } + }, + "sections": [ + { + "title": "A1 — Hardware, ISR and daemon boundary", + "order": 10, + "content_kind": "prose", + "asset_page_mode": "one-per-page", + "page_orientation": "portrait", + "content_tex": "The hardware interrupt only records and defers. GPIO changes later in task context; this is not a software-timer expiry callback.", + "assets": [ + { + "path": "assets/a1-context.png", + "html_path": "assets/a1-context.svg", + "source_path": "assets/a1-context.puml", + "caption": "A1 CONTEXT — mtime, tick ISR, pend queue, daemon and GPIO.", + "label": "fig:a1-context", + "alt": "A1 · hardware-to-deferred-work boundary", + "kind": "diagram", + "width": 1.0, + "page_grid": { + "columns": 1, + "rows": 1, + "page_width": 660, + "page_height": 760, + "overview": true, + "step_tiles": { + "mtime": 1, + "port": 1, + "hook": 1, + "daemon": 1, + "gpio": 1, + "pass": 1 + } + }, + "interactive": { + "kind": "uml-class", + "storage_key": "fc14-a1-context", + "title": "A1 · hardware-to-deferred-work boundary", + "task": { + "id": "task01", + "label": "Task01 · hardware timer to deferred GPIO" + }, + "block": { + "id": "a1", + "label": "A1 CONTEXT", + "description": "The machine timer, kernel tick path, application hook, timer queue, daemon task and GPIO register bank have separate roles." + }, + "phases": [ + { + "id": "boundary", + "label": "HARDWARE / ISR / DAEMON", + "steps": [ + { + "id": "mtime", + "number": 1, + "label": "mtime and mtimecmp generate the kernel tick", + "mode": "CODE", + "strategy_ref": "code.contract", + "svg_label": "01", + "code_ref": "include/FreeRTOSConfig.h:4", + "description": "mtime and mtimecmp generate the kernel tick", + "evidence": "10 MHz clock, 1 kHz tick" + }, + { + "id": "port", + "number": 2, + "label": "port reloads compare and increments tick", + "mode": "CODE", + "strategy_ref": "code.contract", + "svg_label": "02", + "code_ref": "vendor/FreeRTOS-Kernel/portable/GCC/RISC-V/portASM.S:368", + "description": "port reloads compare and increments tick", + "evidence": "machine timer trap" + }, + { + "id": "hook", + "number": 3, + "label": "tick hook accepts exactly one target event", + "mode": "CODE", + "strategy_ref": "code.contract", + "svg_label": "03", + "code_ref": "src/tasks/task01_gpio_timer.c:97", + "description": "tick hook accepts exactly one target event", + "evidence": "minimal ISR path" + }, + { + "id": "daemon", + "number": 4, + "label": "pended function runs on timer daemon", + "mode": "CODE", + "strategy_ref": "code.contract", + "svg_label": "04", + "code_ref": "src/tasks/task01_gpio_timer.c:127", + "description": "pended function runs on timer daemon", + "evidence": "task context" + }, + { + "id": "gpio", + "number": 5, + "label": "daemon owns the GPIO transition", + "mode": "CODE", + "strategy_ref": "code.contract", + "svg_label": "05", + "code_ref": "include/task01_gpio_timer_model.h:32", + "description": "daemon owns the GPIO transition", + "evidence": "exactly one toggle" + }, + { + "id": "pass", + "number": 6, + "label": "runtime proves every boundary", + "mode": "RUN", + "event_id": "E06", + "strategy_ref": "run.identity", + "svg_label": "06", + "code_ref": "src/tasks/task01_gpio_timer.c:202", + "snapshot_ref": "task01.pass", + "description": "runtime proves every boundary", + "evidence": "PASS and deterministic digest" + } + ] + } + ] + } + } + ] + }, + { + "title": "A2 — Event and register records", + "order": 20, + "content_kind": "prose", + "asset_page_mode": "one-per-page", + "page_orientation": "portrait", + "content_tex": "The callback receives a pointer and a 32-bit event value through the timer command queue. It does not capture ISR stack storage.", + "assets": [ + { + "path": "assets/a2-structure.png", + "html_path": "assets/a2-structure.svg", + "source_path": "assets/a2-structure.puml", + "caption": "A2 STRUCTURE — experiment, command, GPIO and evidence records.", + "label": "fig:a2-structure", + "alt": "A2 · deferred event storage", + "kind": "diagram", + "width": 1.0, + "page_grid": { + "columns": 1, + "rows": 1, + "page_width": 660, + "page_height": 760, + "overview": true, + "step_tiles": { + "experiment": 1, + "gpio-record": 1, + "event-record": 1, + "command": 1, + "identity": 1 + } + }, + "interactive": { + "kind": "uml-class", + "storage_key": "fc14-a2-structure", + "title": "A2 · deferred event storage", + "task": { + "id": "task01", + "label": "Task01 · hardware timer to deferred GPIO" + }, + "block": { + "id": "a2", + "label": "A2 STRUCTURE", + "description": "One bounded experiment record connects hardware time, trap state, daemon identity, GPIO values and six commit-last events." + }, + "phases": [ + { + "id": "storage", + "label": "RECORDS AND OWNERSHIP", + "steps": [ + { + "id": "experiment", + "number": 1, + "label": "experiment stores timing and context proof", + "mode": "CODE", + "strategy_ref": "code.contract", + "svg_label": "01", + "code_ref": "include/task01_gpio_timer.h:20", + "description": "experiment stores timing and context proof", + "evidence": "ticks, mtime, SP and result" + }, + { + "id": "gpio-record", + "number": 2, + "label": "volatile GPIO bank stores direction and data", + "mode": "CODE", + "strategy_ref": "code.contract", + "svg_label": "02", + "code_ref": "include/task01_gpio_timer_model.h:10", + "description": "volatile GPIO bank stores direction and data", + "evidence": "transition counter" + }, + { + "id": "event-record", + "number": 3, + "label": "six evidence records commit last", + "mode": "CODE", + "strategy_ref": "code.contract", + "svg_label": "03", + "code_ref": "include/task01_gpio_timer_model.h:17", + "description": "six evidence records commit last", + "evidence": "sequence, actor and tick" + }, + { + "id": "command", + "number": 4, + "label": "timer queue copies callback and arguments", + "mode": "CODE", + "strategy_ref": "code.contract", + "svg_label": "04", + "code_ref": "vendor/FreeRTOS-Kernel/timers.c:1233", + "description": "timer queue copies callback and arguments", + "evidence": "daemon command message" + }, + { + "id": "identity", + "number": 5, + "label": "callback handle equals timer daemon handle", + "mode": "RUN", + "event_id": "E04", + "strategy_ref": "run.daemon", + "svg_label": "05", + "code_ref": "src/tasks/task01_gpio_timer.c:135", + "snapshot_ref": "task01.callback", + "description": "callback handle equals timer daemon handle", + "evidence": "same TaskHandle_t" + } + ] + } + ] + } + } + ] + }, + { + "title": "A3 — Pended-function dispatch", + "order": 30, + "content_kind": "prose", + "asset_page_mode": "one-per-page", + "page_orientation": "portrait", + "content_tex": "The port restores the daemon task before the interrupted stimulus continues. The callback and ISR therefore have different stacks and API permissions.", + "assets": [ + { + "path": "assets/a3-dispatch.png", + "html_path": "assets/a3-dispatch.svg", + "source_path": "assets/a3-dispatch.puml", + "caption": "A3 DISPATCH — MTI, tick hook, timer queue and daemon restore.", + "label": "fig:a3-dispatch", + "alt": "A3 · timer-to-daemon dispatch", + "kind": "diagram", + "width": 1.0, + "page_grid": { + "columns": 1, + "rows": 1, + "page_width": 660, + "page_height": 760, + "overview": true, + "step_tiles": { + "trap": 1, + "reload": 1, + "pend": 1, + "yield": 1, + "callback": 1, + "resume": 1 + } + }, + "interactive": { + "kind": "uml-class", + "storage_key": "fc14-a3-dispatch", + "title": "A3 · timer-to-daemon dispatch", + "task": { + "id": "task01", + "label": "Task01 · hardware timer to deferred GPIO" + }, + "block": { + "id": "a3", + "label": "A3 DISPATCH", + "description": "A real machine timer trap reaches the tick hook, which queues one function and requests a switch to the higher-priority timer daemon." + }, + "phases": [ + { + "id": "dispatch", + "label": "MTI / PEND / RESTORE", + "steps": [ + { + "id": "trap", + "number": 1, + "label": "machine timer enters full trap path", + "mode": "CODE", + "strategy_ref": "code.contract", + "svg_label": "01", + "code_ref": "vendor/FreeRTOS-Kernel/portable/GCC/RISC-V/portASM.S:368", + "description": "machine timer enters full trap path", + "evidence": "mcause timer interrupt" + }, + { + "id": "reload", + "number": 2, + "label": "port reloads mtimecmp before hook", + "mode": "CODE", + "strategy_ref": "code.contract", + "svg_label": "02", + "code_ref": "vendor/FreeRTOS-Kernel/portable/GCC/RISC-V/portASM.S:377", + "description": "port reloads mtimecmp before hook", + "evidence": "next compare is in the future" + }, + { + "id": "pend", + "number": 3, + "label": "hook records and pends one callback", + "mode": "RUN", + "event_id": "E03", + "strategy_ref": "run.timer", + "svg_label": "03", + "code_ref": "src/tasks/task01_gpio_timer.c:109", + "snapshot_ref": "task01.tick-isr", + "description": "hook records and pends one callback", + "evidence": "pdPASS and wake=true" + }, + { + "id": "yield", + "number": 4, + "label": "FromISR result requests daemon restore", + "mode": "CODE", + "strategy_ref": "code.contract", + "svg_label": "04", + "code_ref": "src/tasks/task01_gpio_timer.c:117", + "description": "FromISR result requests daemon restore", + "evidence": "one port yield" + }, + { + "id": "callback", + "number": 5, + "label": "daemon applies GPIO in the same tick", + "mode": "RUN", + "event_id": "E04", + "strategy_ref": "run.daemon", + "svg_label": "05", + "code_ref": "src/tasks/task01_gpio_timer.c:135", + "snapshot_ref": "task01.callback", + "description": "daemon applies GPIO in the same tick", + "evidence": "daemon stack and GPIO=1" + }, + { + "id": "resume", + "number": 6, + "label": "stimulus resumes only after callback", + "mode": "RUN", + "event_id": "E05", + "strategy_ref": "run.daemon", + "svg_label": "06", + "code_ref": "src/tasks/task01_gpio_timer.c:183", + "snapshot_ref": "task01.stimulus-resumed", + "description": "stimulus resumes only after callback", + "evidence": "applied_at_resume=1" + } + ] + } + ] + } + } + ] + }, + { + "title": "A5 — One hardware event replay", + "order": 50, + "content_kind": "prose", + "asset_page_mode": "one-per-page", + "page_orientation": "portrait", + "content_tex": "The decisive order is E03 ISR, E04 daemon, E05 interrupted stimulus. Exactly one accepted event produces exactly one GPIO transition.", + "assets": [ + { + "path": "assets/a5-flow.png", + "html_path": "assets/a5-flow.svg", + "source_path": "assets/a5-flow.puml", + "caption": "A5 FLOW — E01–E06 from configuration to PASS.", + "label": "fig:a5-flow", + "alt": "A5 · deferred GPIO replay", + "kind": "diagram", + "width": 1.0, + "page_grid": { + "columns": 1, + "rows": 1, + "page_width": 660, + "page_height": 760, + "overview": true, + "step_tiles": { + "config": 1, + "arm": 1, + "isr": 1, + "apply": 1, + "stimulus": 1, + "verified": 1 + } + }, + "interactive": { + "kind": "uml-sequence", + "storage_key": "fc14-a5-flow", + "title": "A5 · deferred GPIO replay", + "task": { + "id": "task01", + "label": "Task01 · hardware timer to deferred GPIO" + }, + "block": { + "id": "a5", + "label": "A5 FLOW", + "description": "Six events show configuration, arming, timer ISR, daemon callback, interrupted-task resume and final verification." + }, + "phases": [ + { + "id": "flow", + "label": "ARM / INTERRUPT / DEFER / APPLY", + "steps": [ + { + "id": "config", + "number": 1, + "label": "configure daemon priority and GPIO output", + "mode": "RUN", + "event_id": "E01", + "strategy_ref": "run.timer", + "svg_label": "01", + "code_ref": "src/tasks/task01_gpio_timer.c:260", + "snapshot_ref": "task01.configured", + "description": "configure daemon priority and GPIO output", + "evidence": "daemon priority 3" + }, + { + "id": "arm", + "number": 2, + "label": "stimulus arms target tick plus three", + "mode": "RUN", + "event_id": "E02", + "strategy_ref": "run.timer", + "svg_label": "02", + "code_ref": "src/tasks/task01_gpio_timer.c:163", + "snapshot_ref": "task01.armed", + "description": "stimulus arms target tick plus three", + "evidence": "armed=1" + }, + { + "id": "isr", + "number": 3, + "label": "mtime compare fires at target", + "mode": "RUN", + "event_id": "E03", + "strategy_ref": "run.timer", + "svg_label": "03", + "code_ref": "src/tasks/task01_gpio_timer.c:112", + "snapshot_ref": "task01.tick-isr", + "description": "mtime compare fires at target", + "evidence": "mcause=MTI; pended once" + }, + { + "id": "apply", + "number": 4, + "label": "daemon toggles GPIO low to high", + "mode": "RUN", + "event_id": "E04", + "strategy_ref": "run.daemon", + "svg_label": "04", + "code_ref": "src/tasks/task01_gpio_timer.c:141", + "snapshot_ref": "task01.callback", + "description": "daemon toggles GPIO low to high", + "evidence": "transition count 1" + }, + { + "id": "stimulus", + "number": 5, + "label": "interrupted task resumes after apply", + "mode": "RUN", + "event_id": "E05", + "strategy_ref": "run.daemon", + "svg_label": "05", + "code_ref": "src/tasks/task01_gpio_timer.c:183", + "snapshot_ref": "task01.stimulus-resumed", + "description": "interrupted task resumes after apply", + "evidence": "applied already true" + }, + { + "id": "verified", + "number": 6, + "label": "verifier commits complete proof", + "mode": "RUN", + "event_id": "E06", + "strategy_ref": "run.identity", + "svg_label": "06", + "code_ref": "src/tasks/task01_gpio_timer.c:225", + "snapshot_ref": "task01.pass", + "description": "verifier commits complete proof", + "evidence": "digest bf66bc48" + } + ] + } + ] + } + } + ] + }, + { + "title": "A6 — Pending and applied states", + "order": 60, + "content_kind": "prose", + "asset_page_mode": "one-per-page", + "page_orientation": "portrait", + "content_tex": "Queue acceptance does not mean GPIO has changed. The callback commit is the first point where applied and the output register may be one.", + "assets": [ + { + "path": "assets/a6-state.png", + "html_path": "assets/a6-state.svg", + "source_path": "assets/a6-state.puml", + "caption": "A6 STATE — armed, pended, daemon-running, applied and verified.", + "label": "fig:a6-state", + "alt": "A6 · deferred-work state machine", + "kind": "diagram", + "width": 1.0, + "page_grid": { + "columns": 1, + "rows": 1, + "page_width": 660, + "page_height": 760, + "overview": true, + "step_tiles": { + "armed": 1, + "queued": 1, + "running": 1, + "applied": 1, + "retired": 1, + "terminal": 1 + } + }, + "interactive": { + "kind": "uml-class", + "storage_key": "fc14-a6-state", + "title": "A6 · deferred-work state machine", + "task": { + "id": "task01", + "label": "Task01 · hardware timer to deferred GPIO" + }, + "block": { + "id": "a6", + "label": "A6 STATE", + "description": "The event moves through armed, accepted, queued, executing and applied states; hardware and software ownership change at explicit boundaries." + }, + "phases": [ + { + "id": "state", + "label": "EVENT LIFETIME", + "steps": [ + { + "id": "armed", + "number": 1, + "label": "armed until target tick", + "mode": "RUN", + "event_id": "E02", + "strategy_ref": "run.timer", + "svg_label": "01", + "code_ref": "src/tasks/task01_gpio_timer.c:169", + "snapshot_ref": "task01.armed", + "description": "armed until target tick", + "evidence": "pended=0" + }, + { + "id": "queued", + "number": 2, + "label": "ISR queues one daemon command", + "mode": "RUN", + "event_id": "E03", + "strategy_ref": "run.timer", + "svg_label": "02", + "code_ref": "src/tasks/task01_gpio_timer.c:117", + "snapshot_ref": "task01.tick-isr", + "description": "ISR queues one daemon command", + "evidence": "pended=1" + }, + { + "id": "running", + "number": 3, + "label": "daemon consumes callback and arguments", + "mode": "RUN", + "event_id": "E04", + "strategy_ref": "run.daemon", + "svg_label": "03", + "code_ref": "src/tasks/task01_gpio_timer.c:128", + "snapshot_ref": "task01.callback", + "description": "daemon consumes callback and arguments", + "evidence": "callback_calls=1" + }, + { + "id": "applied", + "number": 4, + "label": "GPIO records one transition", + "mode": "RUN", + "event_id": "E04", + "strategy_ref": "run.daemon", + "svg_label": "04", + "code_ref": "src/tasks/task01_gpio_timer.c:142", + "snapshot_ref": "task01.callback", + "description": "GPIO records one transition", + "evidence": "data=1" + }, + { + "id": "retired", + "number": 5, + "label": "stimulus observes completed work", + "mode": "RUN", + "event_id": "E05", + "strategy_ref": "run.daemon", + "svg_label": "05", + "code_ref": "src/tasks/task01_gpio_timer.c:184", + "snapshot_ref": "task01.stimulus-resumed", + "description": "stimulus observes completed work", + "evidence": "applied=1" + }, + { + "id": "terminal", + "number": 6, + "label": "all counts remain exactly one", + "mode": "RUN", + "event_id": "E06", + "strategy_ref": "run.identity", + "svg_label": "06", + "code_ref": "src/tasks/task01_gpio_timer.c:203", + "snapshot_ref": "task01.pass", + "description": "all counts remain exactly one", + "evidence": "PASS" + } + ] + } + ] + } + } + ] + }, + { + "title": "A7 — Timer, stacks and artifact proof", + "order": 70, + "content_kind": "prose", + "asset_page_mode": "one-per-page", + "page_orientation": "portrait", + "content_tex": "The final gate also requires C-only ABI symbols, the exact source and ELF hashes, and three identical simulator processes.", + "assets": [ + { + "path": "assets/a7-runtime.png", + "html_path": "assets/a7-runtime.svg", + "source_path": "assets/a7-runtime.puml", + "caption": "A7 RUNTIME — mtime, mtimecmp, cause, three stacks and identity.", + "label": "fig:a7-runtime", + "alt": "A7 · hardware and context proof", + "kind": "diagram", + "width": 1.0, + "page_grid": { + "columns": 1, + "rows": 1, + "page_width": 660, + "page_height": 760, + "overview": true, + "step_tiles": { + "registers": 1, + "cause": 1, + "same-tick": 1, + "stacks": 1, + "abi": 1, + "determinism": 1 + } + }, + "interactive": { + "kind": "uml-class", + "storage_key": "fc14-a7-runtime", + "title": "A7 · hardware and context proof", + "task": { + "id": "task01", + "label": "Task01 · hardware timer to deferred GPIO" + }, + "block": { + "id": "a7", + "label": "A7 RUNTIME", + "description": "Runtime evidence distinguishes hardware time, RTOS tick, ISR stack, daemon stack and interrupted-task stack." + }, + "phases": [ + { + "id": "runtime", + "label": "RUNTIME PROOF", + "steps": [ + { + "id": "registers", + "number": 1, + "label": "mtimecmp is reloaded beyond current mtime", + "mode": "RUN", + "event_id": "E03", + "strategy_ref": "run.timer", + "svg_label": "01", + "code_ref": "src/tasks/task01_gpio_timer.c:115", + "snapshot_ref": "task01.tick-isr", + "description": "mtimecmp is reloaded beyond current mtime", + "evidence": "compare > counter" + }, + { + "id": "cause", + "number": 2, + "label": "mcause identifies machine timer interrupt", + "mode": "RUN", + "event_id": "E03", + "strategy_ref": "run.timer", + "svg_label": "02", + "code_ref": "src/tasks/task01_gpio_timer.c:113", + "snapshot_ref": "task01.tick-isr", + "description": "mcause identifies machine timer interrupt", + "evidence": "0x80000007" + }, + { + "id": "same-tick", + "number": 3, + "label": "ISR and callback share target tick", + "mode": "RUN", + "event_id": "E04", + "strategy_ref": "run.daemon", + "svg_label": "03", + "code_ref": "src/tasks/task01_gpio_timer.c:137", + "snapshot_ref": "task01.callback", + "description": "ISR and callback share target tick", + "evidence": "isr_tick=callback_tick" + }, + { + "id": "stacks", + "number": 4, + "label": "ISR, daemon and stimulus SP differ", + "mode": "RUN", + "event_id": "E06", + "strategy_ref": "run.identity", + "svg_label": "04", + "code_ref": "src/tasks/task01_gpio_timer.c:222", + "snapshot_ref": "task01.pass", + "description": "ISR, daemon and stimulus SP differ", + "evidence": "three contexts" + }, + { + "id": "abi", + "number": 5, + "label": "ELF exposes tick, pend and daemon symbols", + "mode": "CODE", + "strategy_ref": "code.identity", + "svg_label": "05", + "code_ref": "scripts/check_abi.sh:18", + "description": "ELF exposes tick, pend and daemon symbols", + "evidence": "no C++ runtime" + }, + { + "id": "determinism", + "number": 6, + "label": "three processes agree on digest", + "mode": "RUN", + "event_id": "E06", + "strategy_ref": "run.identity", + "svg_label": "06", + "code_ref": "scripts/check_determinism.sh:14", + "snapshot_ref": "task01.pass", + "description": "three processes agree on digest", + "evidence": "bf66bc48" + } + ] + } + ] + } + } + ] + }, + { + "title": "Task01 — hardware timer to deferred GPIO", + "order": 90, + "content_kind": "tasks", + "task_refs": [ + "task01" + ] + } + ], + "tasks": { + "task01": { + "title": "Prove one machine-timer event from ISR to daemon GPIO work", + "uuid": "0cc561df-bf81-5bba-9df1-c872d5b42eb8", + "prompt_tex": "Odtwórz E01--E06. Udowodnij, że źródłem jest machine timer interrupt, ISR jedynie odkłada pracę, a GPIO zmienia dopiero callback timer daemon taska.", + "criterion": "PASS; mcause=MTI; mtimecmp>mtime; one successful pend; daemon callback in target tick; one GPIO transition; three distinct stacks; deterministic digest.", + "conclusion_tex": "Hardware timer określa moment przerwania; kolejka timer service określa moment wykonania odroczonej funkcji. Są to dwa konteksty, dwa stosy i dwa różne kontrakty API.", + "flow": [ + { + "kind": "block", + "id": "contract", + "title": "A — kontrakt", + "content_tex": "Rozdziel hardware, ISR, daemon i rejestr GPIO.", + "steps": [ + { + "id": "contexts", + "title": "Przypisz konteksty i API.", + "content_tex": "Wskaż, co wolno zrobić w tick hooku, a co dopiero w callbacku." + }, + { + "id": "predict", + "title": "Przewidź kolejność.", + "content_tex": "Zapisz oczekiwane E03, E04 i E05 dla daemon priority 3." + } + ] + }, + { + "kind": "block", + "id": "replay", + "title": "B — replay", + "content_tex": "Zbierz dowód hardware i task context.", + "steps": [ + { + "id": "timer", + "title": "Sprawdź E02--E03.", + "content_tex": "Target tick, mtime, mtimecmp, mcause i pend result." + }, + { + "id": "daemon", + "title": "Sprawdź E04--E05.", + "content_tex": "Daemon handle, callback SP, GPIO i kolejność restore." + }, + { + "id": "pass", + "title": "Sprawdź E06.", + "content_tex": "Counts, trzy stosy, ABI i digest." + } + ] + }, + { + "kind": "exercise", + "id": "select-mechanism", + "title": "Ćwiczenie — wybór mechanizmu", + "prompt_tex": "Dla trzech prac wybierz notification, semaphore albo daemon deferral: inkrementacja licznika, zapis bloku flash i obudzenie konkretnego taska. Uzasadnij właściciela, latency i budżet.", + "evidence_tex": "Tabela workload → mechanizm → odbiorca → dozwolone operacje → ryzyko blokowania.", + "criterion": "Wybór wynika z wymaganej własności i kosztu; uczeń nie przeciąża timer daemon taska nieograniczoną pracą.", + "based_on": [ + "contract", + "replay" + ] + } + ], + "educational_requirement_refs": [ + "FC14.WE01" + ], + "learning_effect_refs": [ + "FC14.EN01", + "FC14.EK01" + ], + "assessment_criterion_ref": "FC14.KW01" + } + }, + "tasks_order": [ + "task01" + ] +} diff --git a/pdf/mpabi-inf-freertos-c-14-gpio-timer-deferred-v00.01-7de92b94-df89-5c00-be47-d85523ad02ac.pdf b/pdf/mpabi-inf-freertos-c-14-gpio-timer-deferred-v00.01-7de92b94-df89-5c00-be47-d85523ad02ac.pdf new file mode 100644 index 0000000..cfe6248 Binary files /dev/null and b/pdf/mpabi-inf-freertos-c-14-gpio-timer-deferred-v00.01-7de92b94-df89-5c00-be47-d85523ad02ac.pdf differ