feat: publish FreeRTOS C FC04 card
This commit is contained in:
File diff suppressed because it is too large
Load Diff
@@ -0,0 +1,271 @@
|
||||
{
|
||||
"card": {
|
||||
"number": "04",
|
||||
"slug": "delay-state",
|
||||
"title": "Delay, blokowanie, stany taska i usuwanie",
|
||||
"topic": "vTaskDelayUntil, Blocked, Suspended i vTaskDelete",
|
||||
"status": "Gotowa",
|
||||
"version": "v00.01"
|
||||
},
|
||||
"front": {
|
||||
"goal": "Uczeń odróżnia Ready, Running, Blocked, Suspended i Deleted oraz wiąże każdy stan z konkretną przyczyną i publiczną obserwacją FreeRTOS.",
|
||||
"scope": "Task okresowy budzi się co dwa ticki przez vTaskDelayUntil. Drugi task zawiesza się bez warunku czasowego i jest jawnie wznawiany. Observer sprawdza publiczne eTaskState, dokładną oś 2/4/6, osobny stos i bezpieczny zapis przed self-delete."
|
||||
},
|
||||
"viewpoints": [
|
||||
{"id": "A1", "label": "CONTEXT", "status": "unavailable", "subtitle": "Granice systemu", "reason": "Granica aplikacja–kernel–Hazard3 nie zmienia się względem FC03."},
|
||||
{"id": "A2", "label": "STRUCTURE", "status": "enabled", "subtitle": "Konteksty i oś wybudzeń"},
|
||||
{"id": "A3", "label": "DISPATCH", "status": "unavailable", "subtitle": "Callback ABI", "reason": "TaskFunction_t i void* zostały udowodnione w FC02."},
|
||||
{"id": "A4", "label": "APPLICATION", "status": "unavailable", "subtitle": "Topologia", "reason": "Topologia trzech tasków jest już kompletna w A2 i A5."},
|
||||
{"id": "A5", "label": "FLOW", "status": "enabled", "subtitle": "E01–E10 od startu do PASS"},
|
||||
{"id": "A6", "label": "STATE", "status": "enabled", "subtitle": "Ready, Running, Blocked, Suspended, Deleted"},
|
||||
{"id": "A7", "label": "RUNTIME", "status": "enabled", "subtitle": "eTaskState, TCB, stack i tick"},
|
||||
{"id": "A8", "label": "PATTERNS", "status": "unavailable", "subtitle": "Wzorce", "reason": "Karta bada semantykę stanu kernela, nie wzorzec aplikacyjny."}
|
||||
],
|
||||
"artifact": {
|
||||
"source": "src/tasks/task01_delay_state.c",
|
||||
"elf": "build/task01_delay_state/prog.elf",
|
||||
"image": "build/task01_delay_state/prog.bin"
|
||||
},
|
||||
"strategies": [
|
||||
{
|
||||
"id": "code.state-model",
|
||||
"kind": "code",
|
||||
"prerequisites": ["źródło FC04"],
|
||||
"layout": ["nagłówek kontekstów", "kod tasków", "diagram stanu"],
|
||||
"commands": ["rg -n 'PeriodicContext|SuspendContext|eTaskState|Fc04Phase' include src"],
|
||||
"expected_observations": ["stan aplikacyjny i eTaskState są osobnymi pojęciami", "context pozostaje po self-delete"],
|
||||
"assertions": ["Blocked ma warunek wybudzenia", "Suspended nie ma automatycznego wake tick"],
|
||||
"evidence_fields": ["code_ref", "typ pola", "kotwica UML"]
|
||||
},
|
||||
{
|
||||
"id": "run.state",
|
||||
"kind": "run",
|
||||
"prerequisites": ["Hazard3 online", "czysta RAM"],
|
||||
"layout": ["source", "eTaskState", "handle/TCB", "PC/SP"],
|
||||
"commands": ["print g_periodic", "print g_suspend_target", "print g_observer"],
|
||||
"expected_observations": ["observer widzi eBlocked i eSuspended", "resume wybiera wyższy task"],
|
||||
"assertions": ["publiczne handle są ważne podczas obserwacji", "każdy task czyści własny handle"],
|
||||
"evidence_fields": ["event_id", "state", "handle", "PC", "SP", "timestamp"]
|
||||
},
|
||||
{
|
||||
"id": "run.timeline",
|
||||
"kind": "run",
|
||||
"prerequisites": ["scheduler uruchomiony", "period=2"],
|
||||
"layout": ["vTaskDelayUntil call", "wake ticks", "task stack"],
|
||||
"commands": ["print g_periodic.initial_tick", "print g_periodic.release_tick", "print g_periodic.release_count"],
|
||||
"expected_observations": ["kolejne delty wynoszą dokładnie 2", "task jest Blocked między wybudzeniami"],
|
||||
"assertions": ["release count=3", "SP mieści się w stack range"],
|
||||
"evidence_fields": ["initial tick", "release ticks", "SP", "stack range"]
|
||||
},
|
||||
{
|
||||
"id": "run.pass",
|
||||
"kind": "run",
|
||||
"prerequisites": ["oba taski robocze zakończone"],
|
||||
"layout": ["contexts", "timeline", "final assertions"],
|
||||
"commands": ["print g_fc04_pass", "print g_periodic", "print g_suspend_target"],
|
||||
"expected_observations": ["timeline 2/4/6", "resumed=1", "PASS=1"],
|
||||
"assertions": ["observer uruchamia się po wyższych taskach", "forensic context nie jest dereferencją usuniętego TCB"],
|
||||
"evidence_fields": ["PASS", "timeline", "source blob", "image hash", "timestamp"]
|
||||
}
|
||||
],
|
||||
"checkpoints": {
|
||||
"task01.config": {
|
||||
"event_id": "E01",
|
||||
"stop": {"symbol": "fc04_checkpoint_committed", "offset": 0, "condition": "$a0 == 1"},
|
||||
"verify": {"expressions": [{"expr": "g_fc04_last_checkpoint", "equals": 1}, {"expr": "g_periodic.handle == 0", "equals": 1}]}
|
||||
},
|
||||
"task01.scheduler": {
|
||||
"event_id": "E02",
|
||||
"stop": {"symbol": "fc04_checkpoint_committed", "offset": 0, "condition": "$a0 == 2"},
|
||||
"verify": {"expressions": [{"expr": "g_periodic.handle != 0", "equals": 1}, {"expr": "g_suspend_target.handle != 0", "equals": 1}, {"expr": "g_observer.handle != 0", "equals": 1}]}
|
||||
},
|
||||
"task01.periodic-entry": {
|
||||
"event_id": "E03",
|
||||
"stop": {"symbol": "fc04_checkpoint_committed", "offset": 0, "condition": "$a0 == 3 && $a1 == &g_periodic"},
|
||||
"verify": {"expressions": [{"expr": "g_periodic.phase", "equals": 4}, {"expr": "g_periodic.release_count", "equals": 0}]}
|
||||
},
|
||||
"task01.states": {
|
||||
"event_id": "E04",
|
||||
"stop": {"symbol": "fc04_checkpoint_committed", "offset": 0, "condition": "$a0 == 4 && $a1 == &g_observer"},
|
||||
"verify": {"expressions": [{"expr": "g_observer.periodic_state", "equals": 2}, {"expr": "g_observer.suspend_state", "equals": 3}]}
|
||||
},
|
||||
"task01.resumed": {
|
||||
"event_id": "E05",
|
||||
"stop": {"symbol": "fc04_checkpoint_committed", "offset": 0, "condition": "$a0 == 5 && $a1 == &g_suspend_target"},
|
||||
"verify": {"expressions": [{"expr": "g_suspend_target.resumed", "equals": 1}, {"expr": "g_suspend_target.phase", "equals": 4}]}
|
||||
},
|
||||
"task01.release-1": {
|
||||
"event_id": "E06",
|
||||
"stop": {"symbol": "fc04_checkpoint_committed", "offset": 0, "condition": "$a0 == 6 && $a1 == &g_periodic"},
|
||||
"verify": {"expressions": [{"expr": "g_periodic.release_count", "equals": 1}, {"expr": "g_periodic.release_tick[0] - g_periodic.initial_tick", "equals": 2}]}
|
||||
},
|
||||
"task01.release-2": {
|
||||
"event_id": "E07",
|
||||
"stop": {"symbol": "fc04_checkpoint_committed", "offset": 0, "condition": "$a0 == 7 && $a1 == &g_periodic"},
|
||||
"verify": {"expressions": [{"expr": "g_periodic.release_count", "equals": 2}, {"expr": "g_periodic.release_tick[1] - g_periodic.release_tick[0]", "equals": 2}]}
|
||||
},
|
||||
"task01.release-3": {
|
||||
"event_id": "E08",
|
||||
"stop": {"symbol": "fc04_checkpoint_committed", "offset": 0, "condition": "$a0 == 8 && $a1 == &g_periodic"},
|
||||
"verify": {"expressions": [{"expr": "g_periodic.release_count", "equals": 3}, {"expr": "g_periodic.release_tick[2] - g_periodic.release_tick[1]", "equals": 2}]}
|
||||
},
|
||||
"task01.periodic-finished": {
|
||||
"event_id": "E09",
|
||||
"stop": {"symbol": "fc04_checkpoint_committed", "offset": 0, "condition": "$a0 == 9 && $a1 == &g_periodic"},
|
||||
"verify": {"expressions": [{"expr": "g_periodic.phase", "equals": 5}, {"expr": "g_periodic.handle == 0", "equals": 1}]}
|
||||
},
|
||||
"task01.pass": {
|
||||
"event_id": "E10",
|
||||
"stop": {"symbol": "fc04_checkpoint_committed", "offset": 0, "condition": "$a0 == 10 && $a1 == &g_observer"},
|
||||
"verify": {"expressions": [{"expr": "g_fc04_pass", "equals": 1}, {"expr": "g_suspend_target.resumed", "equals": 1}, {"expr": "g_periodic.release_count", "equals": 3}]}
|
||||
}
|
||||
},
|
||||
"sections": [
|
||||
{
|
||||
"id": "A2",
|
||||
"label": "STRUCTURE",
|
||||
"title": "Structure",
|
||||
"order": 20,
|
||||
"orientation": "landscape",
|
||||
"description": "Konteksty C i ograniczona oś czasu.",
|
||||
"content_tex": "Konteksty aplikacyjne przechowują uchwyty, stan diagnostyczny i bounded evidence; nie kopiują prywatnych list kernela.",
|
||||
"assets": [{
|
||||
"stem": "a2-structure",
|
||||
"title": "A2 · konteksty i timeline",
|
||||
"caption": "A2 STRUCTURE — trzy konteksty i absolutna oś wybudzeń.",
|
||||
"label": "fig:a2-structure",
|
||||
"alt": "PeriodicContext, SuspendContext, ObserverContext i timeline.",
|
||||
"phases": [{"id": "contexts", "label": "CONTEXTS / TIMELINE", "steps": [
|
||||
{"id": "periodic", "number": 1, "label": "periodic context owns wake evidence", "mode": "CODE", "strategy_ref": "code.state-model", "svg_label": "01", "svg_target": "Periodic", "code_ref": "include/task01_delay_state.h:23", "description": "Context zachowuje t0 i trzy release ticks.", "evidence": "Static storage przeżywa self-delete."},
|
||||
{"id": "suspend", "number": 2, "label": "suspend context records explicit resume", "mode": "CODE", "strategy_ref": "code.state-model", "svg_label": "02", "svg_target": "Suspend", "code_ref": "include/task01_delay_state.h:37", "description": "Suspended nie ma time-based wake.", "evidence": "resumed zmienia się wyłącznie po vTaskResume."},
|
||||
{"id": "observer", "number": 3, "label": "observer stores public eTaskState", "mode": "RUN", "event_id": "E04", "strategy_ref": "run.state", "svg_label": "03", "svg_target": "Observer", "code_ref": "src/tasks/task01_delay_state.c:150", "snapshot_ref": "task01.states", "description": "Publiczne API odróżnia Blocked i Suspended.", "evidence": "eBlocked oraz eSuspended."},
|
||||
{"id": "timeline", "number": 4, "label": "absolute timeline has exact deltas", "mode": "RUN", "event_id": "E10", "strategy_ref": "run.timeline", "svg_label": "04", "svg_target": "Timeline", "code_ref": "src/tasks/task01_delay_state.c:168", "snapshot_ref": "task01.pass", "description": "Deltas nie zależą od momentu powrotu z pracy.", "evidence": "t0, t0+2, t0+4, t0+6."}
|
||||
]}]
|
||||
}]
|
||||
},
|
||||
{
|
||||
"id": "A5",
|
||||
"label": "FLOW",
|
||||
"title": "Flow",
|
||||
"order": 40,
|
||||
"orientation": "landscape",
|
||||
"description": "Jeden deterministyczny przebieg E01–E10.",
|
||||
"content_tex": "Sekwencja pokazuje przyczynę każdego przejścia i jawny moment zapisu dowodu.",
|
||||
"assets": [{
|
||||
"stem": "a5-flow",
|
||||
"diagram_kind": "sequence",
|
||||
"title": "A5 · delay i resume",
|
||||
"caption": "A5 FLOW — od konfiguracji do okresowych wybudzeń i PASS.",
|
||||
"label": "fig:a5-flow",
|
||||
"alt": "Sekwencja periodic, suspend target, observer i scheduler.",
|
||||
"phases": [{"id": "replay", "label": "DELAY / STATE / DELETE", "steps": [
|
||||
{"id": "config", "number": 1, "label": "configuration committed", "mode": "RUN", "event_id": "E01", "strategy_ref": "run.state", "svg_label": "01", "code_ref": "src/tasks/task01_delay_state.c:227", "snapshot_ref": "task01.config", "description": "Czysta RAM i konfiguracja FC04.", "evidence": "Brak uchwytów przed create."},
|
||||
{"id": "scheduler", "number": 2, "label": "three tasks created", "mode": "RUN", "event_id": "E02", "strategy_ref": "run.state", "svg_label": "02", "code_ref": "src/tasks/task01_delay_state.c:256", "snapshot_ref": "task01.scheduler", "description": "Wszystkie publiczne handle są ważne.", "evidence": "Priorytety 3,2,1."},
|
||||
{"id": "periodic-entry", "number": 3, "label": "periodic starts and blocks", "mode": "RUN", "event_id": "E03", "strategy_ref": "run.timeline", "svg_label": "03", "code_ref": "src/tasks/task01_delay_state.c:87", "snapshot_ref": "task01.periodic-entry", "description": "t0 jest punktem odniesienia vTaskDelayUntil.", "evidence": "release_count=0."},
|
||||
{"id": "states", "number": 4, "label": "observer sees Blocked and Suspended", "mode": "RUN", "event_id": "E04", "strategy_ref": "run.state", "svg_label": "04", "code_ref": "src/tasks/task01_delay_state.c:150", "snapshot_ref": "task01.states", "description": "Oba stany mają różną przyczynę.", "evidence": "eBlocked i eSuspended."},
|
||||
{"id": "resumed", "number": 5, "label": "target resumes and self-deletes", "mode": "RUN", "event_id": "E05", "strategy_ref": "run.state", "svg_label": "05", "code_ref": "src/tasks/task01_delay_state.c:122", "snapshot_ref": "task01.resumed", "description": "Wyższy priorytet preemptuje observera.", "evidence": "resumed=1."},
|
||||
{"id": "release-1", "number": 6, "label": "release at t0 plus 2", "mode": "RUN", "event_id": "E06", "strategy_ref": "run.timeline", "svg_label": "06", "code_ref": "src/tasks/task01_delay_state.c:96", "snapshot_ref": "task01.release-1", "description": "Pierwszy absolute wake.", "evidence": "delta=2."},
|
||||
{"id": "release-2", "number": 7, "label": "release at t0 plus 4", "mode": "RUN", "event_id": "E07", "strategy_ref": "run.timeline", "svg_label": "07", "code_ref": "src/tasks/task01_delay_state.c:96", "snapshot_ref": "task01.release-2", "description": "Drugi absolute wake.", "evidence": "delta=2."},
|
||||
{"id": "release-3", "number": 8, "label": "release at t0 plus 6", "mode": "RUN", "event_id": "E08", "strategy_ref": "run.timeline", "svg_label": "08", "code_ref": "src/tasks/task01_delay_state.c:96", "snapshot_ref": "task01.release-3", "description": "Trzeci absolute wake.", "evidence": "delta=2."},
|
||||
{"id": "periodic-finished", "number": 9, "label": "periodic clears handle before delete", "mode": "RUN", "event_id": "E09", "strategy_ref": "run.state", "svg_label": "09", "code_ref": "src/tasks/task01_delay_state.c:99", "snapshot_ref": "task01.periodic-finished", "description": "Context zachowuje forensic values.", "evidence": "phase=COMPLETED, handle=NULL."},
|
||||
{"id": "pass", "number": 10, "label": "observer verifies PASS", "mode": "RUN", "event_id": "E10", "strategy_ref": "run.pass", "svg_label": "10", "code_ref": "src/tasks/task01_delay_state.c:192", "snapshot_ref": "task01.pass", "description": "Observer sprawdza stany, timeline i stack.", "evidence": "PASS=1."}
|
||||
]}]
|
||||
}]
|
||||
},
|
||||
{
|
||||
"id": "A6",
|
||||
"label": "STATE",
|
||||
"title": "State",
|
||||
"order": 50,
|
||||
"orientation": "landscape",
|
||||
"description": "Przyczyny przejść między stanami taska.",
|
||||
"content_tex": "Blocked ma warunek czasu lub zdarzenia; Suspended wymaga jawnego resume. Deleted nie oznacza natychmiastowego wymazania wszystkich śladów.",
|
||||
"assets": [{
|
||||
"stem": "a6-state",
|
||||
"title": "A6 · stany taska",
|
||||
"caption": "A6 STATE — Ready, Running, Blocked, Suspended i Deleted.",
|
||||
"label": "fig:a6-state",
|
||||
"alt": "Maszyna stanów taska FreeRTOS.",
|
||||
"phases": [{"id": "states", "label": "TASK STATE", "steps": [
|
||||
{"id": "ready", "number": 1, "label": "Ready waits for selection", "mode": "RUN", "event_id": "E02", "strategy_ref": "run.state", "svg_label": "01", "code_ref": "src/tasks/task01_delay_state.c:229", "snapshot_ref": "task01.scheduler", "description": "Created nie znaczy Running.", "evidence": "handle ważny przed startem."},
|
||||
{"id": "running", "number": 2, "label": "highest Ready task runs", "mode": "RUN", "event_id": "E03", "strategy_ref": "run.state", "svg_label": "02", "code_ref": "src/tasks/task01_delay_state.c:72", "snapshot_ref": "task01.periodic-entry", "description": "Periodic ma priorytet 3.", "evidence": "PC/SP w periodic."},
|
||||
{"id": "blocked", "number": 3, "label": "delay moves task to Blocked", "mode": "RUN", "event_id": "E04", "strategy_ref": "run.state", "svg_label": "03", "code_ref": "src/tasks/task01_delay_state.c:92", "snapshot_ref": "task01.states", "description": "Wake tick istnieje.", "evidence": "eBlocked."},
|
||||
{"id": "suspended", "number": 4, "label": "self-suspend has no wake tick", "mode": "RUN", "event_id": "E04", "strategy_ref": "run.state", "svg_label": "04", "code_ref": "src/tasks/task01_delay_state.c:118", "snapshot_ref": "task01.states", "description": "Tylko jawne resume przywraca Ready.", "evidence": "eSuspended."},
|
||||
{"id": "resumed-ready", "number": 5, "label": "resume makes target Ready", "mode": "RUN", "event_id": "E05", "strategy_ref": "run.state", "svg_label": "05", "code_ref": "src/tasks/task01_delay_state.c:160", "snapshot_ref": "task01.resumed", "description": "Priorytet 2 wyprzedza observera 1.", "evidence": "target Running po resume."},
|
||||
{"id": "completed", "number": 6, "label": "application records completion", "mode": "RUN", "event_id": "E09", "strategy_ref": "run.state", "svg_label": "06", "code_ref": "src/tasks/task01_delay_state.c:99", "snapshot_ref": "task01.periodic-finished", "description": "COMPLETED jest stanem diagnostycznym aplikacji.", "evidence": "Zapis przed delete."},
|
||||
{"id": "deleted", "number": 7, "label": "self-delete delegates cleanup", "mode": "RUN", "event_id": "E10", "strategy_ref": "run.pass", "svg_label": "07", "code_ref": "src/tasks/task01_delay_state.c:102", "snapshot_ref": "task01.pass", "description": "Idle może później odzyskać TCB/stack.", "evidence": "Context static pozostaje."}
|
||||
]}]
|
||||
}]
|
||||
},
|
||||
{
|
||||
"id": "A7",
|
||||
"label": "RUNTIME",
|
||||
"title": "Runtime",
|
||||
"order": 60,
|
||||
"orientation": "landscape",
|
||||
"description": "Publiczny stan, TCB/stack i oś ticków.",
|
||||
"content_tex": "A7 wiąże publiczne eTaskState z pamięcią taska i bounded evidence, bez uzależniania programu od pxCurrentTCB.",
|
||||
"assets": [{
|
||||
"stem": "a7-runtime",
|
||||
"title": "A7 · runtime evidence",
|
||||
"caption": "A7 RUNTIME — stany publiczne, task memory, wake ticks i PASS.",
|
||||
"label": "fig:a7-runtime",
|
||||
"alt": "Runtime evidence dla delay i suspend.",
|
||||
"phases": [{"id": "runtime", "label": "STATE / MEMORY / TIME", "steps": [
|
||||
{"id": "public", "number": 1, "label": "public API exposes two states", "mode": "RUN", "event_id": "E04", "strategy_ref": "run.state", "svg_label": "01", "svg_target": "Public", "code_ref": "src/tasks/task01_delay_state.c:150", "snapshot_ref": "task01.states", "description": "Program nie czyta prywatnych list.", "evidence": "eBlocked, eSuspended."},
|
||||
{"id": "periodic-runtime", "number": 2, "label": "periodic has separate TCB and stack", "mode": "RUN", "event_id": "E03", "strategy_ref": "run.timeline", "svg_label": "02", "svg_target": "Periodic", "code_ref": "src/tasks/task01_delay_state.c:59", "snapshot_ref": "task01.periodic-entry", "description": "SP należy do task stack.", "evidence": "created_handle i stack range."},
|
||||
{"id": "wake", "number": 3, "label": "absolute wake timeline is exact", "mode": "RUN", "event_id": "E08", "strategy_ref": "run.timeline", "svg_label": "03", "svg_target": "Wake", "code_ref": "src/tasks/task01_delay_state.c:96", "snapshot_ref": "task01.release-3", "description": "Trzy wybudzenia zachowują okres.", "evidence": "2/4/6."},
|
||||
{"id": "suspend-runtime", "number": 4, "label": "suspended task resumes explicitly", "mode": "RUN", "event_id": "E05", "strategy_ref": "run.state", "svg_label": "04", "svg_target": "Suspend", "code_ref": "src/tasks/task01_delay_state.c:107", "snapshot_ref": "task01.resumed", "description": "Brak time-based wake.", "evidence": "resumed=1."},
|
||||
{"id": "evidence", "number": 5, "label": "forensic evidence remains bounded", "mode": "RUN", "event_id": "E10", "strategy_ref": "run.pass", "svg_label": "05", "svg_target": "Evidence", "code_ref": "src/tasks/task01_delay_state.c:192", "snapshot_ref": "task01.pass", "description": "Snapshot wiąże wynik ze źródłem i ELF.", "evidence": "PASS, source blob, image hash, timestamp."}
|
||||
]}]
|
||||
}]
|
||||
}
|
||||
],
|
||||
"learning": {
|
||||
"model_label": "Model stanów taska",
|
||||
"model": "Uczeń rozróżnia Ready, Running, Blocked, Suspended i Deleted oraz przyczynę każdego przejścia.",
|
||||
"replay_label": "Replay delay i resume",
|
||||
"replay": "Uczeń odtwarza E01–E10 i wiąże publiczny stan, tick, PC/SP, TCB oraz stos.",
|
||||
"criterion": "Program kończy się PASS; observer widzi eBlocked i eSuspended; timeline ma dokładne delty 2; resume działa raz; context, TCB i stack pozostają rozdzielone.",
|
||||
"requirement": "Zaprojektowanie i zbadanie deterministycznego eksperymentu delay, suspend, resume i self-delete."
|
||||
},
|
||||
"task": {
|
||||
"short_label": "delay i stany",
|
||||
"title": "Delay, blokowanie, zawieszenie i self-delete",
|
||||
"prompt_tex": "Przejdź po A2, A5, A6 i A7. Odtwórz E01–E10, rozróżnij Blocked od Suspended i udowodnij dokładny okres vTaskDelayUntil.",
|
||||
"conclusion_tex": "Blocked task ma warunek wybudzenia, Suspended wymaga jawnego resume, a vTaskDelayUntil utrzymuje absolutną fazę okresu. Self-delete kończy task, lecz aplikacyjny context może zachować bounded forensic evidence.",
|
||||
"flow": [
|
||||
{
|
||||
"kind": "block",
|
||||
"id": "state-model",
|
||||
"title": "A — model stanów",
|
||||
"content_tex": "Najpierw przewidź przyczynę i wyjście z każdego stanu.",
|
||||
"steps": [
|
||||
{"id": "classify", "title": "Sklasyfikuj Blocked i Suspended.", "content_tex": "Wskaż warunek automatycznego wybudzenia albo jego brak."},
|
||||
{"id": "predict", "title": "Przewidź oś czasu.", "content_tex": "Zapisz oczekiwane t0+2, t0+4 i t0+6."}
|
||||
]
|
||||
},
|
||||
{
|
||||
"kind": "block",
|
||||
"id": "runtime-replay",
|
||||
"title": "B — replay Hazard3",
|
||||
"content_tex": "Każdy RUN zaczyna się od czystej RAM.",
|
||||
"steps": [
|
||||
{"id": "observe", "title": "Zbadaj E04.", "content_tex": "Zapisz publiczne stany obu tasków i ich przyczyny."},
|
||||
{"id": "resume", "title": "Zbadaj E05.", "content_tex": "Wyjaśnij, dlaczego target preemptuje observera."},
|
||||
{"id": "timeline", "title": "Zbadaj E06–E08.", "content_tex": "Policz delty release ticks i sprawdź stack taska."},
|
||||
{"id": "finish", "title": "Zbadaj E09–E10.", "content_tex": "Oddziel application completion od cleanup kernela."}
|
||||
]
|
||||
},
|
||||
{
|
||||
"kind": "exercise",
|
||||
"id": "relative-delay-drift",
|
||||
"title": "Ćwiczenie — względny delay i dryf",
|
||||
"prompt_tex": "Zastąp vTaskDelayUntil przez vTaskDelay i dodaj bounded workload trwający jeden tick po każdym wybudzeniu. Zmierz trzy release ticks i porównaj fazę z wersją bazową.",
|
||||
"evidence_tex": "Timestampowane snapshoty release ticks oraz krótka tabela różnic względem 2/4/6.",
|
||||
"criterion": "Uczeń poprawnie wyjaśnia, dlaczego relative delay kumuluje czas pracy i przesuwa fazę.",
|
||||
"based_on": ["state-model", "runtime-replay"]
|
||||
}
|
||||
]
|
||||
}
|
||||
}
|
||||
Reference in New Issue
Block a user