edu-inf/lab-rv32i-c-machine-timer
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

feat: add lab-rv32i-c-machine-timer card

Browse Source
This commit is contained in:
user
2026-07-21 19:14:20 +02:00
commit a0e116f24e
23 changed files with 4720 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
json/card_source.json
+667
View File
@@ -0,0 +1,667 @@
{
"$schema": "../../../tools/card-layouts/schemas/card-source.schema.json",
"schema": "esc-card-source.v1",
"card": {
"id": "mpabi-inf-c-11-machine-timer",
"series": "c",
"series_title": "C · Freestanding RV32I and K&R",
"number": "11",
"count": "13",
"slug": "machine-timer",
"title": "Machine timer: od mtime do okresowego deadline'u",
"topic": "RV32I/Hazard3: spójny odczyt mtime, mtimecmp i przerwania machine timer",
"project": "Freestanding C na RV32I",
"subject": "Informatyka",
"level": "Rok 1 · C11 · RV32I/Hazard3",
"revision_date": "2026-07-20T00:00:00+02:00",
"status": "Gotowa",
"version": "v00.01",
"uuid": "45f57fde-fc7b-5f41-a3af-f153202dff0f",
"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,
"template": "templates/karta-klasyczna.json",
"title_block": {
"category": "KARTA PRACY · INFORMATYKA",
"prepared_by": "M. Pabiszczak",
"prepared_on": "2026-07-20T00:00:00+02:00",
"title": "Machine timer: od mtime do okresowego deadline'u",
"url": "https://dce7fb9d-7b2f-5d49-96a2-3a30d3070b84.mpabi.pl/f37170be-e988-5f5d-b3cf-6ea179a9cd54",
"repository_url": "https://zsl-gitea.mpabi.pl/edu-inf/lab-rv32i-c-machine-timer",
"url_host_uuid": "dce7fb9d-7b2f-5d49-96a2-3a30d3070b84",
"url_domain": "mpabi.pl",
"doc_uuid": "f37170be-e988-5f5d-b3cf-6ea179a9cd54",
"revision": "v00.01",
"issued_on": "2026-07-20T00:00:00+02:00",
"series": "C-11",
"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_break": true,
"front_page_scope": {
"title": "Cel karty",
"content_tex": "Uczeń rozdziela źródło czasu, warunek pending, dwa poziomy enable, wybór handlera i jego efekt. Potrafi spójnie odczytać 64-bitowy licznik na RV32, uruchomić jednorazowe przerwanie oraz utrzymać fazę okresowego zegara przez deadline += period.",
"scope_title": "Zakres i zachowane przykłady",
"scope_content_tex": "Trzy przykłady wykonują się na rzeczywistym modelu RTL Hazard3. Task01 wymusza rollover dolnego słowa mtime. Task02 dowodzi wejścia przez slot 7 wektora, skasowania poziomowego źródła przez przesunięcie mtimecmp i wznowienia po mret. Task03 zapisuje cztery planowane i obserwowane czasy oraz spóźnienia. Host nie jest używany jako substytut urządzenia MMIO i przerwań.\\par\\textbf{Układ każdego przykładu:} pełny profil A1--A8; widok N/D ma jawny powód, a diagram nie jest wymagany, gdy tekst daje lepszy dowód.",
"scope_table": {
"headers": [
"Typ",
"Task",
"Idea",
"Waga"
],
"rows": [
{
"chapter": "MMIO",
"task": "Task01",
"idea_tex": "RV32 split-register MMIO i high--low--high",
"priority": "kluczowe",
"key": true
},
{
"chapter": "IRQ",
"task": "Task02",
"idea_tex": "mtimecmp, pending, MTIE/MIE, mtvec, mret i rearm",
"priority": "kluczowe",
"key": true
},
{
"chapter": "TICK",
"task": "Task03",
"idea_tex": "deadline += period, tick sequence i lateness",
"priority": "kluczowe",
"key": true
}
]
}
},
"side_margin_tree_layout": {
"columns": [
{
"id": "zawodowe",
"label": "TECH",
"side": "left",
"tree": "WE -> EK -> KW",
"description": "Kod C, ABI i obserwacja RV32I."
},
{
"id": "ogolne",
"label": "OG",
"side": "right",
"tree": "WE -> EN -> KW",
"description": "Przewidywanie, pomiar i wniosek."
}
]
},
"learning_effects": {
"C11.EN01": {
"bloom_level": "Analiza",
"label": "Od źródła do efektu ISR",
"text": "Uczeń dla każdego zachowania wskazuje osobno source, pending, enabled, decyzję dispatchera i efekt handlera, zamiast nazywać cały łańcuch jednym słowem timer.",
"assessment_criteria": [
"C11.KW01"
]
},
"C11.EK01": {
"bloom_level": "Zastosowanie",
"label": "Dowód na RTL Hazard3",
"text": "Uczeń buduje obrazy RV32I, uruchamia je z limitem cykli i sprawdza raport MMIO, mcause, liczbę ISR, powrót z pułapki oraz arytmetykę deadline'ów.",
"assessment_criteria": [
"C11.KW01"
]
}
},
"assessment_criteria": {
"C11.KW01": {
"text": "Wszystkie trzy programy kończą się kodem 0 bez nieobsłużonej pułapki i timeoutu. Task01 wykazuje co najmniej dwie próby przez rollover, high=1 i monotoniczny drugi odczyt. Task02 ma dokładnie jeden ISR, mcause=0x80000007, pending=0 przed uzbrojeniem i po obsłudze oraz resume=1. Task03 ma cztery ISR, planowane czasy różniące się dokładnie o 1600, observed >= scheduled, lateness=observed-scheduled i fazowe przesunięcie modelu now+period równe bieżącemu spóźnieniu.",
"learning_effects": [
"C11.EN01",
"C11.EK01"
]
}
},
"educational_requirements": {
"C11.WE01": {
"text": "Obsługa split-register MMIO i machine timer interrupt na RV32I z jawnym kontraktem poziomowego źródła, maskowania i bezwzględnego deadline'u.",
"label": "RV32I/Hazard3: spójny odczyt mtime, mtimecmp i przerwania machine timer",
"learning_effects": [
"C11.EN01",
"C11.EK01"
],
"learning_tree": {
"schema": "we-learning-tree.v1",
"policy": "Najpierw przewidywanie, następnie wykonanie i odczyt dowodu.",
"ogolne": [
{
"effect_ref": "C11.EN01",
"display": "EN C11 01",
"source": "LOCAL",
"official": "C",
"local": "01",
"kind": "EN",
"tree_id": "C11.WE01.OG.LOCAL.C.01",
"text": "Uczeń dla każdego zachowania wskazuje osobno source, pending, enabled, decyzję dispatchera i efekt handlera, zamiast nazywać cały łańcuch jednym słowem timer.",
"kw": [
{
"criterion_ref": "C11.KW01",
"display": "KW C11 01",
"source": "LOCAL",
"kind": "KW",
"official": "C",
"local": "01",
"text": "Kod, przewidywanie i pomiar tworzą jeden dowód."
}
]
}
],
"zawodowe": [
{
"effect_ref": "C11.EK01",
"display": "EK C11 01",
"source": "LOCAL",
"official": "C",
"local": "01",
"kind": "EK",
"tree_id": "C11.WE01.TECH.LOCAL.C.01",
"text": "Uczeń buduje obrazy RV32I, uruchamia je z limitem cykli i sprawdza raport MMIO, mcause, liczbę ISR, powrót z pułapki oraz arytmetykę deadline'ów.",
"kw": [
{
"criterion_ref": "C11.KW01",
"display": "KW C11 01",
"source": "LOCAL",
"kind": "KW",
"official": "C",
"local": "01",
"text": "Kod, przewidywanie i pomiar tworzą jeden dowód."
}
]
}
]
}
}
},
"sections": [
{
"title": "1 — Jeden timer, pięć różnych ról",
"order": 10,
"content_kind": "prose",
"page_orientation": "portrait",
"content_tex": "\\texttt{mtime} jest źródłem rosnącego czasu, a relacja \\texttt{mtime >= mtimecmp} wytwarza poziomowy stan pending. \\texttt{mie.MTIE} dopuszcza tę klasę przerwań lokalnie, \\texttt{mstatus.MIE} dopuszcza przerwania globalnie, a \\texttt{mtvec} wybiera kod według przyczyny. Dopiero handler zmienia stan programu i przesuwa komparator. Żaden z bitów enable nie kasuje źródła.\n\nW testbenchu Hazard3 \\texttt{mtime} rośnie raz na krok, a linia timera jest aktywna tak długo, jak licznik nie jest mniejszy od komparatora. Dlatego powrót bez zapisu przyszłego \\texttt{mtimecmp} wywołałby następną pułapkę niemal natychmiast.",
"educational_requirement_refs": [
"C11.WE01"
],
"learning_effect_refs": [
"C11.EN01",
"C11.EK01"
],
"assessment_criterion_refs": [
"C11.KW01"
]
},
{
"title": "2 — 64 bity urządzenia na 32-bitowym rdzeniu",
"order": 20,
"content_kind": "prose",
"page_orientation": "portrait",
"content_tex": "Dwa odczyty 32-bitowe nie tworzą automatycznie spójnego odczytu 64-bitowego MMIO. Sekwencja high--low--high akceptuje parę dopiero wtedy, gdy oba odczyty high są równe; zmiana high oznacza rollover między transakcjami i wymusza powtórzenie. Przy zapisie komparatora kolejność high=UINT32\\_MAX, low, docelowe high usuwa niebezpieczne okno z przejściowo zbyt małym \\texttt{mtimecmp}.\n\nTask01 zapisuje \\texttt{mtime} tylko po to, aby fixture testbencha deterministycznie doprowadził do rolloveru. Nie jest to obietnica, że licznik czasu będzie zapisywalny w innym SoC.",
"educational_requirement_refs": [
"C11.WE01"
],
"learning_effect_refs": [
"C11.EN01",
"C11.EK01"
],
"assessment_criterion_refs": [
"C11.KW01"
]
},
{
"title": "3 — Okres to oś czasu, nie odstęp od spóźnionego now",
"order": 30,
"content_kind": "prose",
"page_orientation": "portrait",
"content_tex": "Dla periodycznego zegara handler wykonuje \\texttt{deadline += period}. Wtedy planowana sekwencja zachowuje fazę nawet wtedy, gdy wejście do ISR następuje później niż deadline. Reguła \\texttt{now + period} użyta jako jedyny model przenosi aktualne spóźnienie do następnego terminu i tworzy dryf.\n\nKarta mierzy \\texttt{lateness = observed - scheduled}; nie obiecuje stałej wartości opóźnienia. Bieżący RTL i build dają 40 taktów, lecz wynik zależy od magistrali, prologu ISR i punktu próbkowania. Przykład nie definiuje jeszcze polityki nadrabiania wielu całkowicie pominiętych okresów.",
"educational_requirement_refs": [
"C11.WE01"
],
"learning_effect_refs": [
"C11.EN01",
"C11.EK01"
],
"assessment_criterion_refs": [
"C11.KW01"
]
},
{
"title": "Zadania — zachowane przykłady w profilu A1–A8",
"order": 40,
"content_kind": "tasks",
"page_orientation": "portrait",
"task_refs": [
"task01",
"task02",
"task03"
],
"educational_requirement_refs": [
"C11.WE01"
],
"learning_effect_refs": [
"C11.EN01",
"C11.EK01"
],
"assessment_criterion_refs": [
"C11.KW01"
]
}
],
"tasks": {
"task01": {
"title": "Spójny odczyt mtime przez rollover",
"uuid": "c33548e4-07c8-599c-9457-8ba457701659",
"prompt_tex": "Wyjaśnij, jaki błędny 64-bitowy wynik może utworzyć pojedyncze low--high podczas rolloveru. Następnie wskaż w raporcie próbę odrzuconą przez high--low--high i rozdziel kod produkcyjnego odczytu od zapisywalnego fixture'u testbencha.",
"criterion": "Oracle Hazard3: retry=1, attempts > 1, value_high=1, monotonic=1, pass=1 i kod wyjścia 0. W bieżącym buildzie okno znaleziono dla offsetu 0x13 i po dwóch próbach; sam offset nie jest kontraktem architektury.",
"conclusion_tex": "",
"render_task_acceptance": false,
"viewpoints": [
{
"id": "A1",
"status": "enabled",
"title": "CONTEXT — atomowość C nie jest atomowością MMIO",
"content_tex": "Urządzenie ma 64-bitowy licznik, lecz RV32 wykonuje trzy jawne odczyty 32-bitowych rejestrów. Typ \\texttt{uint64\\_t} służy do złożenia zaakceptowanych połówek; nie zamienia dwóch transakcji magistrali w jeden atomowy odczyt."
},
{
"id": "A2",
"status": "enabled",
"title": "STRUCTURE — dwa słowa jednego licznika",
"content_tex": "\\texttt{timer\\_hw\\_t} mapuje kolejno \\texttt{mtime}, \\texttt{mtimeh}, \\texttt{mtimecmp} i \\texttt{mtimecmph} od adresu 0xc0000100. \\texttt{volatile} wymusza obserwowalne dostępy C, ale regułę spójności dostarcza dopiero algorytm."
},
{
"id": "A3",
"status": "unavailable",
"title": "DISPATCH",
"reason": "Task01 ma wyłączone przerwania i wykonuje bezpośredni odczyt MMIO; nie ma ISR, callbacku, tablicy funkcji ani wyboru odbiorcy."
},
{
"id": "A4",
"status": "enabled",
"title": "APPLICATION — kontrolowane przejście przez 0xffffffff",
"content_tex": "Fixture ustawia high=0 i low blisko \\texttt{UINT32\\_MAX}, a następnie wyszukuje małe okno, w którym high zmieni się między pierwszym i drugim odczytem. Zaakceptowany wynik musi pochodzić już z epoki high=1; kolejny odczyt nie może być mniejszy."
},
{
"id": "A5",
"status": "enabled",
"title": "FLOW — read, validate, retry",
"content_tex": "Jedna próba czyta \\texttt{high\\_before}, \\texttt{low}, \\texttt{high\\_after}. Równość high kończy pętlę i pozwala złożyć wynik. Nierówność odrzuca low należące do niejednoznacznej granicy epok i powtarza wszystkie trzy transakcje."
},
{
"id": "A6",
"status": "enabled",
"title": "STATE — epoka 0, rollover, epoka 1",
"content_tex": "Stan urządzenia przechodzi z high=0 i low blisko maksimum przez rollover do high=1 i małego low. Pierwsza para high opisuje zmianę stanu, więc nie wolno do niej przypisać jednego snapshotu; druga próba stabilizuje się w epoce 1."
},
{
"id": "A7",
"status": "enabled",
"title": "RUNTIME — dwa dostępy high są widocznym dowodem",
"content_tex": "Oracle raportuje offset, liczbę prób, retry, high wyniku i monotoniczność. Bieżący RTL daje offset 0x13 i attempts=2. Listing ma pokazać dwa osobne \\texttt{lw} z rejestru high, rozdzielone odczytem low, oraz gałąź powrotną przy nierówności."
},
{
"id": "A8",
"status": "enabled",
"title": "PATTERNS — stabilny snapshot z licznika split-register",
"content_tex": "Wzorzec high--low--high stosuj, gdy dokumentacja urządzenia gwarantuje monotoniczny licznik i zgodne zachowanie połówek. Fixture zapisujący czas pozostaje poza produkcyjnym API odczytu."
}
],
"flow": [
{
"kind": "block",
"id": "task01.a1",
"title": "A1 CONTEXT · AKTYWNE — atomowość C nie jest atomowością MMIO",
"content_tex": "\\textbf{Zachowany przykład:} \\nolinkurl{src/tasks/task01_mtime_consistent_read.c}.\\par Urządzenie ma 64-bitowy licznik, lecz RV32 wykonuje trzy jawne odczyty 32-bitowych rejestrów. Typ \\texttt{uint64\\_t} służy do złożenia zaakceptowanych połówek; nie zamienia dwóch transakcji magistrali w jeden atomowy odczyt."
},
{
"kind": "block",
"id": "task01.a2",
"title": "A2 STRUCTURE · AKTYWNE — dwa słowa jednego licznika",
"content_tex": "\\texttt{timer\\_hw\\_t} mapuje kolejno \\texttt{mtime}, \\texttt{mtimeh}, \\texttt{mtimecmp} i \\texttt{mtimecmph} od adresu 0xc0000100. \\texttt{volatile} wymusza obserwowalne dostępy C, ale regułę spójności dostarcza dopiero algorytm."
},
{
"kind": "block",
"id": "task01.a3",
"title": "A3 DISPATCH · N/D",
"content_tex": "\\textbf{N/D.} Task01 ma wyłączone przerwania i wykonuje bezpośredni odczyt MMIO; nie ma ISR, callbacku, tablicy funkcji ani wyboru odbiorcy."
},
{
"kind": "block",
"id": "task01.a4",
"title": "A4 APPLICATION · AKTYWNE — kontrolowane przejście przez 0xffffffff",
"content_tex": "Fixture ustawia high=0 i low blisko \\texttt{UINT32\\_MAX}, a następnie wyszukuje małe okno, w którym high zmieni się między pierwszym i drugim odczytem. Zaakceptowany wynik musi pochodzić już z epoki high=1; kolejny odczyt nie może być mniejszy."
},
{
"kind": "block",
"id": "task01.a5",
"title": "A5 FLOW · AKTYWNE — read, validate, retry",
"content_tex": "Jedna próba czyta \\texttt{high\\_before}, \\texttt{low}, \\texttt{high\\_after}. Równość high kończy pętlę i pozwala złożyć wynik. Nierówność odrzuca low należące do niejednoznacznej granicy epok i powtarza wszystkie trzy transakcje."
},
{
"kind": "block",
"id": "task01.a6",
"title": "A6 STATE · AKTYWNE — epoka 0, rollover, epoka 1",
"content_tex": "Stan urządzenia przechodzi z high=0 i low blisko maksimum przez rollover do high=1 i małego low. Pierwsza para high opisuje zmianę stanu, więc nie wolno do niej przypisać jednego snapshotu; druga próba stabilizuje się w epoce 1."
},
{
"kind": "block",
"id": "task01.a7",
"title": "A7 RUNTIME · AKTYWNE — dwa dostępy high są widocznym dowodem",
"content_tex": "Oracle raportuje offset, liczbę prób, retry, high wyniku i monotoniczność. Bieżący RTL daje offset 0x13 i attempts=2. Listing ma pokazać dwa osobne \\texttt{lw} z rejestru high, rozdzielone odczytem low, oraz gałąź powrotną przy nierówności."
},
{
"kind": "block",
"id": "task01.a8",
"title": "A8 PATTERNS · AKTYWNE — stabilny snapshot z licznika split-register",
"content_tex": "Wzorzec high--low--high stosuj, gdy dokumentacja urządzenia gwarantuje monotoniczny licznik i zgodne zachowanie połówek. Fixture zapisujący czas pozostaje poza produkcyjnym API odczytu."
},
{
"kind": "exercise",
"id": "task01.proof",
"title": "Przewidywanie → wykonanie → wniosek",
"prompt_tex": "Wyjaśnij, jaki błędny 64-bitowy wynik może utworzyć pojedyncze low--high podczas rolloveru. Następnie wskaż w raporcie próbę odrzuconą przez high--low--high i rozdziel kod produkcyjnego odczytu od zapisywalnego fixture'u testbencha.",
"evidence_tex": "Przewidywany błąd na granicy rolloveru, log z RTL Hazard3 z kodem wyjścia i limitem cykli, fragment listingu z dwoma odczytami high oraz wniosek o spójności zaakceptowanego snapshotu.",
"criterion": "Oracle Hazard3: retry=1, attempts > 1, value_high=1, monotonic=1, pass=1 i kod wyjścia 0. W bieżącym buildzie okno znaleziono dla offsetu 0x13 i po dwóch próbach; sam offset nie jest kontraktem architektury."
},
{
"kind": "block",
"id": "task01.worksheet",
"title": "TASK01 · Zapis dowodu ucznia",
"content_tex": "\\textbf{1. Przewidywanie przed uruchomieniem}\\par\\noindent\\dotfill\\par\\noindent\\dotfill\\par\\textbf{2. Log wykonania RTL Hazard3 i kod wyjścia}\\par\\noindent\\dotfill\\par\\noindent\\dotfill\\par\\textbf{3. Dowód w listingu: high--low--high i retry}\\par\\noindent\\dotfill\\par\\noindent\\dotfill\\par\\textbf{4. Wniosek: reguła języka lub kontrakt targetu potwierdzony przez pomiar}\\par\\noindent\\dotfill\\par\\noindent\\dotfill"
}
],
"educational_requirement_refs": [
"C11.WE01"
],
"learning_effect_refs": [
"C11.EN01",
"C11.EK01"
],
"assessment_criterion_ref": "C11.KW01"
},
"task02": {
"title": "Jednorazowe przerwanie machine timer",
"uuid": "dc7f8696-19db-55b6-8fd9-cb676b399ec7",
"prompt_tex": "Ułóż w poprawnej kolejności: wyłącz maski, ustaw przyszły mtimecmp, sprawdź pending, włącz MTIE i MIE, czekaj w wfi, przesuń komparator w ISR, wróć przez mret. Dla każdego kroku nazwij source, pending, enable, decyzję dispatchera albo efekt.",
"criterion": "Oracle Hazard3: count=1, mcause=0x80000007, pending_before=0, pending_after=0, resumed=1, deadline_reached=1, pass=1 i kod wyjścia 0. Listing ISR kończy się mret.",
"conclusion_tex": "",
"render_task_acceptance": false,
"viewpoints": [
{
"id": "A1",
"status": "enabled",
"title": "CONTEXT — enable nie jest źródłem",
"content_tex": "Źródłem jest relacja \\texttt{mtime >= mtimecmp}; \\texttt{mip.MTIP} reprezentuje pending. \\texttt{mie.MTIE} i \\texttt{mstatus.MIE} są dwiema bramkami. Program najpierw ustawia przyszły komparator, a dopiero potem otwiera obie bramki."
},
{
"id": "A2",
"status": "enabled",
"title": "STRUCTURE — wspólny driver i stan dowodowy",
"content_tex": "Wspólny nagłówek zawiera dostęp MMIO, bezpieczny zapis komparatora i operacje CSR. Task przechowuje osobno deadline, czas zaobserwowany, mcause, liczbę ISR, pending przed i po oraz znacznik wznowienia."
},
{
"id": "A3",
"status": "enabled",
"title": "DISPATCH — przyczyna 7 wybiera handler timera",
"content_tex": "Startup zapisuje do \\texttt{mtvec} adres tablicy z bitem trybu vectored. Machine timer ma cause=7, więc rdzeń wybiera slot 7, którego skok wiąże się z silnym symbolem \\texttt{isr\\_machine\\_timer} zamiast słabego handlera domyślnego. Atrybut GCC kończy funkcję instrukcją \\texttt{mret}."
},
{
"id": "A4",
"status": "enabled",
"title": "APPLICATION — one-shot z jawnym kryterium zakończenia",
"content_tex": "Main planuje deadline 1200 taktów po spójnym odczycie. Sukces wymaga dokładnie jednego wejścia, poprawnego mcause, obserwacji nie wcześniejszej niż deadline, skasowanego pending po rearmie i wykonania instrukcji po \\texttt{wfi}."
},
{
"id": "A5",
"status": "enabled",
"title": "FLOW — source → pending → enable → handler → effect",
"content_tex": "Rosnące mtime osiąga comparator i ustawia pending. Otwarty MTIE oraz MIE pozwalają wejść do wektora. Handler zapisuje obserwację i mcause, przesuwa comparator na \\texttt{UINT64\\_MAX}, publikuje count, a \\texttt{mret} przywraca przerwany przepływ. Main ustawia resumed i zamyka maski."
},
{
"id": "A6",
"status": "enabled",
"title": "STATE — DISARMED, ARMED, PENDING, HANDLED, RESUMED",
"content_tex": "Komparator maksimum reprezentuje DISARMED. Przyszły deadline tworzy ARMED. Po osiągnięciu terminu urządzenie jest PENDING, handler ponownie zapisuje maksimum i publikuje HANDLED, a kod po pętli \\texttt{wfi} potwierdza RESUMED."
},
{
"id": "A7",
"status": "enabled",
"title": "RUNTIME — mcause, mip i mret",
"content_tex": "Raport z RTL ma: count=1, mcause=0x80000007, pending 0/0, resumed=1 i deadline\\_reached=1. Objdump ma pokazać zapis trzech połówek mtimecmp w handlerze oraz końcowe \\texttt{mret}; zwykłe \\texttt{ret} nie byłoby poprawnym powrotem z pułapki."
},
{
"id": "A8",
"status": "enabled",
"title": "PATTERNS — arm before unmask, clear source before publish",
"content_tex": "Najpierw ustaw bezpieczny stan urządzenia, potem włącz źródło w \\texttt{mie}, na końcu globalne MIE. W ISR usuń poziomowe źródło przed opublikowaniem zakończenia; inaczej powrót może natychmiast wejść ponownie."
}
],
"flow": [
{
"kind": "block",
"id": "task02.a1",
"title": "A1 CONTEXT · AKTYWNE — enable nie jest źródłem",
"content_tex": "\\textbf{Zachowany przykład:} \\nolinkurl{src/tasks/task02_oneshot_timer_irq.c}.\\par Źródłem jest relacja \\texttt{mtime >= mtimecmp}; \\texttt{mip.MTIP} reprezentuje pending. \\texttt{mie.MTIE} i \\texttt{mstatus.MIE} są dwiema bramkami. Program najpierw ustawia przyszły komparator, a dopiero potem otwiera obie bramki."
},
{
"kind": "block",
"id": "task02.a2",
"title": "A2 STRUCTURE · AKTYWNE — wspólny driver i stan dowodowy",
"content_tex": "Wspólny nagłówek zawiera dostęp MMIO, bezpieczny zapis komparatora i operacje CSR. Task przechowuje osobno deadline, czas zaobserwowany, mcause, liczbę ISR, pending przed i po oraz znacznik wznowienia."
},
{
"kind": "block",
"id": "task02.a3",
"title": "A3 DISPATCH · AKTYWNE — przyczyna 7 wybiera handler timera",
"content_tex": "Startup zapisuje do \\texttt{mtvec} adres tablicy z bitem trybu vectored. Machine timer ma cause=7, więc rdzeń wybiera slot 7, którego skok wiąże się z silnym symbolem \\texttt{isr\\_machine\\_timer} zamiast słabego handlera domyślnego. Atrybut GCC kończy funkcję instrukcją \\texttt{mret}."
},
{
"kind": "block",
"id": "task02.a4",
"title": "A4 APPLICATION · AKTYWNE — one-shot z jawnym kryterium zakończenia",
"content_tex": "Main planuje deadline 1200 taktów po spójnym odczycie. Sukces wymaga dokładnie jednego wejścia, poprawnego mcause, obserwacji nie wcześniejszej niż deadline, skasowanego pending po rearmie i wykonania instrukcji po \\texttt{wfi}."
},
{
"kind": "block",
"id": "task02.a5",
"title": "A5 FLOW · AKTYWNE — source → pending → enable → handler → effect",
"content_tex": "Rosnące mtime osiąga comparator i ustawia pending. Otwarty MTIE oraz MIE pozwalają wejść do wektora. Handler zapisuje obserwację i mcause, przesuwa comparator na \\texttt{UINT64\\_MAX}, publikuje count, a \\texttt{mret} przywraca przerwany przepływ. Main ustawia resumed i zamyka maski."
},
{
"kind": "block",
"id": "task02.a6",
"title": "A6 STATE · AKTYWNE — DISARMED, ARMED, PENDING, HANDLED, RESUMED",
"content_tex": "Komparator maksimum reprezentuje DISARMED. Przyszły deadline tworzy ARMED. Po osiągnięciu terminu urządzenie jest PENDING, handler ponownie zapisuje maksimum i publikuje HANDLED, a kod po pętli \\texttt{wfi} potwierdza RESUMED."
},
{
"kind": "block",
"id": "task02.a7",
"title": "A7 RUNTIME · AKTYWNE — mcause, mip i mret",
"content_tex": "Raport z RTL ma: count=1, mcause=0x80000007, pending 0/0, resumed=1 i deadline\\_reached=1. Objdump ma pokazać zapis trzech połówek mtimecmp w handlerze oraz końcowe \\texttt{mret}; zwykłe \\texttt{ret} nie byłoby poprawnym powrotem z pułapki."
},
{
"kind": "block",
"id": "task02.a8",
"title": "A8 PATTERNS · AKTYWNE — arm before unmask, clear source before publish",
"content_tex": "Najpierw ustaw bezpieczny stan urządzenia, potem włącz źródło w \\texttt{mie}, na końcu globalne MIE. W ISR usuń poziomowe źródło przed opublikowaniem zakończenia; inaczej powrót może natychmiast wejść ponownie."
},
{
"kind": "exercise",
"id": "task02.proof",
"title": "Przewidywanie → wykonanie → wniosek",
"prompt_tex": "Ułóż w poprawnej kolejności: wyłącz maski, ustaw przyszły mtimecmp, sprawdź pending, włącz MTIE i MIE, czekaj w wfi, przesuń komparator w ISR, wróć przez mret. Dla każdego kroku nazwij source, pending, enable, decyzję dispatchera albo efekt.",
"evidence_tex": "Przewidywana sekwencja source--pending--enable--dispatch--effect, log RTL Hazard3 z mcause i kodem wyjścia, fragment listingu z wektorem oraz mret i wniosek o skasowaniu poziomowego źródła.",
"criterion": "Oracle Hazard3: count=1, mcause=0x80000007, pending_before=0, pending_after=0, resumed=1, deadline_reached=1, pass=1 i kod wyjścia 0. Listing ISR kończy się mret."
},
{
"kind": "block",
"id": "task02.worksheet",
"title": "TASK02 · Zapis dowodu ucznia",
"content_tex": "\\textbf{1. Przewidywanie przed uruchomieniem}\\par\\noindent\\dotfill\\par\\noindent\\dotfill\\par\\textbf{2. Log wykonania RTL: mcause, pending i resume}\\par\\noindent\\dotfill\\par\\noindent\\dotfill\\par\\textbf{3. Dowód w CSR i listingu: slot 7 oraz mret}\\par\\noindent\\dotfill\\par\\noindent\\dotfill\\par\\textbf{4. Wniosek: reguła języka lub kontrakt targetu potwierdzony przez pomiar}\\par\\noindent\\dotfill\\par\\noindent\\dotfill"
}
],
"educational_requirement_refs": [
"C11.WE01"
],
"learning_effect_refs": [
"C11.EN01",
"C11.EK01"
],
"assessment_criterion_ref": "C11.KW01"
},
"task03": {
"title": "Okresowe deadline'y bez dryfu fazy",
"uuid": "6c330959-1a78-5068-8c59-6b18f712122c",
"prompt_tex": "Dla czterech ticków porównaj scheduled, observed i lateness. Udowodnij stały krok 1600 oraz wyprowadź, o ile przesunąłby następną fazę model now+period. Wyjaśnij granicę: przykład nie nadrabia dowolnej liczby całkowicie pominiętych okresów.",
"criterion": "Oracle Hazard3: count=causes=4, period=1600, step_ok=ordered=late_math=naive_shift_ok=pass=1. Bieżący pomiar daje cztery lateness po 40 taktów, ale test nie uznaje liczby 40 za kontrakt sprzętowy.",
"conclusion_tex": "",
"render_task_acceptance": false,
"viewpoints": [
{
"id": "A1",
"status": "enabled",
"title": "CONTEXT — harmonogram i wykonanie to dwie osie",
"content_tex": "Scheduled opisuje idealną oś czasu usługi, observed chwilę rzeczywistego wejścia do pomiaru w ISR, a lateness ich różnicę. Okres ma aktualizować harmonogram, nie kopiować opóźnienia wykonania do przyszłej fazy."
},
{
"id": "A2",
"status": "enabled",
"title": "STRUCTURE — cztery rekordy ticków",
"content_tex": "Trzy tablice po cztery elementy zapisują deadline, obserwację i lateness. \\texttt{g\\_task03\\_next\\_deadline} jest stanem planisty, a count publikuje liczbę kompletnych rekordów. Stała period wynosi 1600 taktów modelu."
},
{
"id": "A3",
"status": "enabled",
"title": "DISPATCH — każdy MTIP trafia przez slot 7",
"content_tex": "Dla każdego z czterech terminów rdzeń koduje interrupt bit i cause=7 w mcause, a tryb vectored wybiera ten sam \\texttt{isr\\_machine\\_timer}. Handler sprawdza mcause przy każdym wejściu; licznik causes=4 dowodzi czterech decyzji dispatchera."
},
{
"id": "A4",
"status": "enabled",
"title": "APPLICATION — stała faza i zmierzone spóźnienie",
"content_tex": "Dla i>0 musi zachodzić \\texttt{scheduled[i]-scheduled[i-1]=1600}. Dla każdego rekordu observed nie może być wcześniejsze od scheduled, a lateness musi być dokładnie ich różnicą. Po czwartym ticku comparator wraca do maksimum."
},
{
"id": "A5",
"status": "enabled",
"title": "FLOW — sample, record, advance, rearm, publish",
"content_tex": "ISR najpierw pobiera indeks i aktualny deadline, potem czyta czas oraz zapisuje rekord. Następnie oblicza deadline+period, uzbraja ten bezwzględny termin albo rozbraja po ostatnim ticku, a count publikuje dopiero na końcu. Main czeka w \\texttt{wfi} do czterech rekordów."
},
{
"id": "A6",
"status": "enabled",
"title": "STATE — TICK0 → TICK4 i niezmienna faza",
"content_tex": "Stan count przechodzi 0,1,2,3,4; razem z każdym przejściem next\\_deadline rośnie dokładnie o period. Po count=4 urządzenie jest DISARMED. Tablice pozostają historią czterech zakończonych przejść i są analizowane dopiero po zamknięciu masek."
},
{
"id": "A7",
"status": "enabled",
"title": "RUNTIME — cztery terminy i 40 taktów bieżącego RTL",
"content_tex": "Bieżący raport podaje deadline low 0x96b, 0xfab, 0x15eb, 0x1c2b; obserwacje są o 0x28 późniejsze. Ważne są relacje step\\_ok, ordered i late\\_math, ponieważ absolutne wartości oraz 40 taktów mogą się zmienić po zmianie RTL, optymalizacji lub prologu ISR."
},
{
"id": "A8",
"status": "enabled",
"title": "PATTERNS — absolute periodic deadline",
"content_tex": "\\texttt{deadline += period} zachowuje fazę. Gdyby następny termin powstał wyłącznie jako \\texttt{observed + period}, jego przesunięcie względem osi absolutnej byłoby równe bieżącemu lateness; powtarzanie tej reguły kumuluje dryf. Osobna polityka musi zdecydować, czy po dużym opóźnieniu nadrabiać, pomijać, czy zgłaszać błąd."
}
],
"flow": [
{
"kind": "block",
"id": "task03.a1",
"title": "A1 CONTEXT · AKTYWNE — harmonogram i wykonanie to dwie osie",
"content_tex": "\\textbf{Zachowany przykład:} \\nolinkurl{src/tasks/task03_periodic_absolute_deadline.c}.\\par Scheduled opisuje idealną oś czasu usługi, observed chwilę rzeczywistego wejścia do pomiaru w ISR, a lateness ich różnicę. Okres ma aktualizować harmonogram, nie kopiować opóźnienia wykonania do przyszłej fazy."
},
{
"kind": "block",
"id": "task03.a2",
"title": "A2 STRUCTURE · AKTYWNE — cztery rekordy ticków",
"content_tex": "Trzy tablice po cztery elementy zapisują deadline, obserwację i lateness. \\texttt{g\\_task03\\_next\\_deadline} jest stanem planisty, a count publikuje liczbę kompletnych rekordów. Stała period wynosi 1600 taktów modelu."
},
{
"kind": "block",
"id": "task03.a3",
"title": "A3 DISPATCH · AKTYWNE — każdy MTIP trafia przez slot 7",
"content_tex": "Dla każdego z czterech terminów rdzeń koduje interrupt bit i cause=7 w mcause, a tryb vectored wybiera ten sam \\texttt{isr\\_machine\\_timer}. Handler sprawdza mcause przy każdym wejściu; licznik causes=4 dowodzi czterech decyzji dispatchera."
},
{
"kind": "block",
"id": "task03.a4",
"title": "A4 APPLICATION · AKTYWNE — stała faza i zmierzone spóźnienie",
"content_tex": "Dla i>0 musi zachodzić \\texttt{scheduled[i]-scheduled[i-1]=1600}. Dla każdego rekordu observed nie może być wcześniejsze od scheduled, a lateness musi być dokładnie ich różnicą. Po czwartym ticku comparator wraca do maksimum."
},
{
"kind": "block",
"id": "task03.a5",
"title": "A5 FLOW · AKTYWNE — sample, record, advance, rearm, publish",
"content_tex": "ISR najpierw pobiera indeks i aktualny deadline, potem czyta czas oraz zapisuje rekord. Następnie oblicza deadline+period, uzbraja ten bezwzględny termin albo rozbraja po ostatnim ticku, a count publikuje dopiero na końcu. Main czeka w \\texttt{wfi} do czterech rekordów."
},
{
"kind": "block",
"id": "task03.a6",
"title": "A6 STATE · AKTYWNE — TICK0 → TICK4 i niezmienna faza",
"content_tex": "Stan count przechodzi 0,1,2,3,4; razem z każdym przejściem next\\_deadline rośnie dokładnie o period. Po count=4 urządzenie jest DISARMED. Tablice pozostają historią czterech zakończonych przejść i są analizowane dopiero po zamknięciu masek."
},
{
"kind": "block",
"id": "task03.a7",
"title": "A7 RUNTIME · AKTYWNE — cztery terminy i 40 taktów bieżącego RTL",
"content_tex": "Bieżący raport podaje deadline low 0x96b, 0xfab, 0x15eb, 0x1c2b; obserwacje są o 0x28 późniejsze. Ważne są relacje step\\_ok, ordered i late\\_math, ponieważ absolutne wartości oraz 40 taktów mogą się zmienić po zmianie RTL, optymalizacji lub prologu ISR."
},
{
"kind": "block",
"id": "task03.a8",
"title": "A8 PATTERNS · AKTYWNE — absolute periodic deadline",
"content_tex": "\\texttt{deadline += period} zachowuje fazę. Gdyby następny termin powstał wyłącznie jako \\texttt{observed + period}, jego przesunięcie względem osi absolutnej byłoby równe bieżącemu lateness; powtarzanie tej reguły kumuluje dryf. Osobna polityka musi zdecydować, czy po dużym opóźnieniu nadrabiać, pomijać, czy zgłaszać błąd."
},
{
"kind": "exercise",
"id": "task03.proof",
"title": "Przewidywanie → wykonanie → wniosek",
"prompt_tex": "Dla czterech ticków porównaj scheduled, observed i lateness. Udowodnij stały krok 1600 oraz wyprowadź, o ile przesunąłby następną fazę model now+period. Wyjaśnij granicę: przykład nie nadrabia dowolnej liczby całkowicie pominiętych okresów.",
"evidence_tex": "Przewidywana sekwencja czterech deadline'ów, log RTL Hazard3 z planowanymi i obserwowanymi czasami, kontrola różnic i kodu wyjścia oraz wniosek porównujący deadline+period z now+period.",
"criterion": "Oracle Hazard3: count=causes=4, period=1600, step_ok=ordered=late_math=naive_shift_ok=pass=1. Bieżący pomiar daje cztery lateness po 40 taktów, ale test nie uznaje liczby 40 za kontrakt sprzętowy."
},
{
"kind": "block",
"id": "task03.worksheet",
"title": "TASK03 · Zapis dowodu ucznia",
"content_tex": "\\textbf{1. Przewidywanie przed uruchomieniem}\\par\\noindent\\dotfill\\par\\noindent\\dotfill\\par\\textbf{2. Log RTL: deadline, observed i lateness}\\par\\noindent\\dotfill\\par\\noindent\\dotfill\\par\\textbf{3. Dowód stałego kroku i braku dryfu fazy}\\par\\noindent\\dotfill\\par\\noindent\\dotfill\\par\\textbf{4. Wniosek: reguła języka lub kontrakt targetu potwierdzony przez pomiar}\\par\\noindent\\dotfill\\par\\noindent\\dotfill"
}
],
"educational_requirement_refs": [
"C11.WE01"
],
"learning_effect_refs": [
"C11.EN01",
"C11.EK01"
],
"assessment_criterion_ref": "C11.KW01"
}
},
"tasks_order": [
"task01",
"task02",
"task03"
]
}
json/card_spec.json
+233
View File
@@ -0,0 +1,233 @@
{
"card": {
"number": "11",
"slug": "machine-timer",
"title": "Machine timer: od mtime do okresowego deadline'u",
"topic": "RV32I/Hazard3: spójny odczyt mtime, mtimecmp i przerwania machine timer",
"status": "Gotowa",
"version": "v00.01",
"revision_date": "2026-07-20T00:00:00+02:00",
"level": "Rok 1 · C11 · RV32I/Hazard3"
},
"front": {
"goal": "Uczeń rozdziela źródło czasu, warunek pending, dwa poziomy enable, wybór handlera i jego efekt. Potrafi spójnie odczytać 64-bitowy licznik na RV32, uruchomić jednorazowe przerwanie oraz utrzymać fazę okresowego zegara przez deadline += period.",
"scope": "Trzy przykłady wykonują się na rzeczywistym modelu RTL Hazard3. Task01 wymusza rollover dolnego słowa mtime. Task02 dowodzi wejścia przez slot 7 wektora, skasowania poziomowego źródła przez przesunięcie mtimecmp i wznowienia po mret. Task03 zapisuje cztery planowane i obserwowane czasy oraz spóźnienia. Host nie jest używany jako substytut urządzenia MMIO i przerwań."
},
"scope_headers": ["Typ", "Task", "Idea", "Waga"],
"learning": {
"reasoning_label": "Od źródła do efektu ISR",
"reasoning": "Uczeń dla każdego zachowania wskazuje osobno source, pending, enabled, decyzję dispatchera i efekt handlera, zamiast nazywać cały łańcuch jednym słowem timer.",
"practice_label": "Dowód na RTL Hazard3",
"practice": "Uczeń buduje obrazy RV32I, uruchamia je z limitem cykli i sprawdza raport MMIO, mcause, liczbę ISR, powrót z pułapki oraz arytmetykę deadline'ów.",
"criterion": "Wszystkie trzy programy kończą się kodem 0 bez nieobsłużonej pułapki i timeoutu. Task01 wykazuje co najmniej dwie próby przez rollover, high=1 i monotoniczny drugi odczyt. Task02 ma dokładnie jeden ISR, mcause=0x80000007, pending=0 przed uzbrojeniem i po obsłudze oraz resume=1. Task03 ma cztery ISR, planowane czasy różniące się dokładnie o 1600, observed >= scheduled, lateness=observed-scheduled i fazowe przesunięcie modelu now+period równe bieżącemu spóźnieniu.",
"requirement": "Obsługa split-register MMIO i machine timer interrupt na RV32I z jawnym kontraktem poziomowego źródła, maskowania i bezwzględnego deadline'u."
},
"sections": [
{
"title": "1 — Jeden timer, pięć różnych ról",
"content_tex": "\u005ctexttt{mtime} jest źródłem rosnącego czasu, a relacja \u005ctexttt{mtime >= mtimecmp} wytwarza poziomowy stan pending. \u005ctexttt{mie.MTIE} dopuszcza tę klasę przerwań lokalnie, \u005ctexttt{mstatus.MIE} dopuszcza przerwania globalnie, a \u005ctexttt{mtvec} wybiera kod według przyczyny. Dopiero handler zmienia stan programu i przesuwa komparator. Żaden z bitów enable nie kasuje źródła.\n\nW testbenchu Hazard3 \u005ctexttt{mtime} rośnie raz na krok, a linia timera jest aktywna tak długo, jak licznik nie jest mniejszy od komparatora. Dlatego powrót bez zapisu przyszłego \u005ctexttt{mtimecmp} wywołałby następną pułapkę niemal natychmiast."
},
{
"title": "2 — 64 bity urządzenia na 32-bitowym rdzeniu",
"content_tex": "Dwa odczyty 32-bitowe nie tworzą automatycznie spójnego odczytu 64-bitowego MMIO. Sekwencja high--low--high akceptuje parę dopiero wtedy, gdy oba odczyty high są równe; zmiana high oznacza rollover między transakcjami i wymusza powtórzenie. Przy zapisie komparatora kolejność high=UINT32\\_MAX, low, docelowe high usuwa niebezpieczne okno z przejściowo zbyt małym \u005ctexttt{mtimecmp}.\n\nTask01 zapisuje \u005ctexttt{mtime} tylko po to, aby fixture testbencha deterministycznie doprowadził do rolloveru. Nie jest to obietnica, że licznik czasu będzie zapisywalny w innym SoC."
},
{
"title": "3 — Okres to oś czasu, nie odstęp od spóźnionego now",
"content_tex": "Dla periodycznego zegara handler wykonuje \u005ctexttt{deadline += period}. Wtedy planowana sekwencja zachowuje fazę nawet wtedy, gdy wejście do ISR następuje później niż deadline. Reguła \u005ctexttt{now + period} użyta jako jedyny model przenosi aktualne spóźnienie do następnego terminu i tworzy dryf.\n\nKarta mierzy \u005ctexttt{lateness = observed - scheduled}; nie obiecuje stałej wartości opóźnienia. Bieżący RTL i build dają 40 taktów, lecz wynik zależy od magistrali, prologu ISR i punktu próbkowania. Przykład nie definiuje jeszcze polityki nadrabiania wielu całkowicie pominiętych okresów."
}
],
"tasks": [
{
"id": "task01",
"source": "src/tasks/task01_mtime_consistent_read.c",
"chapter": "MMIO",
"title": "Spójny odczyt mtime przez rollover",
"idea_tex": "RV32 split-register MMIO i high--low--high",
"priority": "kluczowe",
"key": true,
"prompt_tex": "Wyjaśnij, jaki błędny 64-bitowy wynik może utworzyć pojedyncze low--high podczas rolloveru. Następnie wskaż w raporcie próbę odrzuconą przez high--low--high i rozdziel kod produkcyjnego odczytu od zapisywalnego fixture'u testbencha.",
"evidence_tex": "Przewidywany błąd na granicy rolloveru, log z RTL Hazard3 z kodem wyjścia i limitem cykli, fragment listingu z dwoma odczytami high oraz wniosek o spójności zaakceptowanego snapshotu.",
"worksheet_step2": "Log wykonania RTL Hazard3 i kod wyjścia",
"worksheet_step3": "Dowód w listingu: high--low--high i retry",
"criterion": "Oracle Hazard3: retry=1, attempts > 1, value_high=1, monotonic=1, pass=1 i kod wyjścia 0. W bieżącym buildzie okno znaleziono dla offsetu 0x13 i po dwóch próbach; sam offset nie jest kontraktem architektury.",
"viewpoints": [
{
"id": "A1",
"status": "enabled",
"title": "CONTEXT — atomowość C nie jest atomowością MMIO",
"content_tex": "Urządzenie ma 64-bitowy licznik, lecz RV32 wykonuje trzy jawne odczyty 32-bitowych rejestrów. Typ \u005ctexttt{uint64\\_t} służy do złożenia zaakceptowanych połówek; nie zamienia dwóch transakcji magistrali w jeden atomowy odczyt."
},
{
"id": "A2",
"status": "enabled",
"title": "STRUCTURE — dwa słowa jednego licznika",
"content_tex": "\u005ctexttt{timer\\_hw\\_t} mapuje kolejno \u005ctexttt{mtime}, \u005ctexttt{mtimeh}, \u005ctexttt{mtimecmp} i \u005ctexttt{mtimecmph} od adresu 0xc0000100. \u005ctexttt{volatile} wymusza obserwowalne dostępy C, ale regułę spójności dostarcza dopiero algorytm."
},
{
"id": "A3",
"status": "unavailable",
"title": "DISPATCH",
"reason": "Task01 ma wyłączone przerwania i wykonuje bezpośredni odczyt MMIO; nie ma ISR, callbacku, tablicy funkcji ani wyboru odbiorcy."
},
{
"id": "A4",
"status": "enabled",
"title": "APPLICATION — kontrolowane przejście przez 0xffffffff",
"content_tex": "Fixture ustawia high=0 i low blisko \u005ctexttt{UINT32\\_MAX}, a następnie wyszukuje małe okno, w którym high zmieni się między pierwszym i drugim odczytem. Zaakceptowany wynik musi pochodzić już z epoki high=1; kolejny odczyt nie może być mniejszy."
},
{
"id": "A5",
"status": "enabled",
"title": "FLOW — read, validate, retry",
"content_tex": "Jedna próba czyta \u005ctexttt{high\\_before}, \u005ctexttt{low}, \u005ctexttt{high\\_after}. Równość high kończy pętlę i pozwala złożyć wynik. Nierówność odrzuca low należące do niejednoznacznej granicy epok i powtarza wszystkie trzy transakcje."
},
{
"id": "A6",
"status": "enabled",
"title": "STATE — epoka 0, rollover, epoka 1",
"content_tex": "Stan urządzenia przechodzi z high=0 i low blisko maksimum przez rollover do high=1 i małego low. Pierwsza para high opisuje zmianę stanu, więc nie wolno do niej przypisać jednego snapshotu; druga próba stabilizuje się w epoce 1."
},
{
"id": "A7",
"status": "enabled",
"title": "RUNTIME — dwa dostępy high są widocznym dowodem",
"content_tex": "Oracle raportuje offset, liczbę prób, retry, high wyniku i monotoniczność. Bieżący RTL daje offset 0x13 i attempts=2. Listing ma pokazać dwa osobne \u005ctexttt{lw} z rejestru high, rozdzielone odczytem low, oraz gałąź powrotną przy nierówności."
},
{
"id": "A8",
"status": "enabled",
"title": "PATTERNS — stabilny snapshot z licznika split-register",
"content_tex": "Wzorzec high--low--high stosuj, gdy dokumentacja urządzenia gwarantuje monotoniczny licznik i zgodne zachowanie połówek. Fixture zapisujący czas pozostaje poza produkcyjnym API odczytu."
}
]
},
{
"id": "task02",
"source": "src/tasks/task02_oneshot_timer_irq.c",
"chapter": "IRQ",
"title": "Jednorazowe przerwanie machine timer",
"idea_tex": "mtimecmp, pending, MTIE/MIE, mtvec, mret i rearm",
"priority": "kluczowe",
"key": true,
"prompt_tex": "Ułóż w poprawnej kolejności: wyłącz maski, ustaw przyszły mtimecmp, sprawdź pending, włącz MTIE i MIE, czekaj w wfi, przesuń komparator w ISR, wróć przez mret. Dla każdego kroku nazwij source, pending, enable, decyzję dispatchera albo efekt.",
"evidence_tex": "Przewidywana sekwencja source--pending--enable--dispatch--effect, log RTL Hazard3 z mcause i kodem wyjścia, fragment listingu z wektorem oraz mret i wniosek o skasowaniu poziomowego źródła.",
"worksheet_step2": "Log wykonania RTL: mcause, pending i resume",
"worksheet_step3": "Dowód w CSR i listingu: slot 7 oraz mret",
"criterion": "Oracle Hazard3: count=1, mcause=0x80000007, pending_before=0, pending_after=0, resumed=1, deadline_reached=1, pass=1 i kod wyjścia 0. Listing ISR kończy się mret.",
"viewpoints": [
{
"id": "A1",
"status": "enabled",
"title": "CONTEXT — enable nie jest źródłem",
"content_tex": "Źródłem jest relacja \u005ctexttt{mtime >= mtimecmp}; \u005ctexttt{mip.MTIP} reprezentuje pending. \u005ctexttt{mie.MTIE} i \u005ctexttt{mstatus.MIE} są dwiema bramkami. Program najpierw ustawia przyszły komparator, a dopiero potem otwiera obie bramki."
},
{
"id": "A2",
"status": "enabled",
"title": "STRUCTURE — wspólny driver i stan dowodowy",
"content_tex": "Wspólny nagłówek zawiera dostęp MMIO, bezpieczny zapis komparatora i operacje CSR. Task przechowuje osobno deadline, czas zaobserwowany, mcause, liczbę ISR, pending przed i po oraz znacznik wznowienia."
},
{
"id": "A3",
"status": "enabled",
"title": "DISPATCH — przyczyna 7 wybiera handler timera",
"content_tex": "Startup zapisuje do \u005ctexttt{mtvec} adres tablicy z bitem trybu vectored. Machine timer ma cause=7, więc rdzeń wybiera slot 7, którego skok wiąże się z silnym symbolem \u005ctexttt{isr\\_machine\\_timer} zamiast słabego handlera domyślnego. Atrybut GCC kończy funkcję instrukcją \u005ctexttt{mret}."
},
{
"id": "A4",
"status": "enabled",
"title": "APPLICATION — one-shot z jawnym kryterium zakończenia",
"content_tex": "Main planuje deadline 1200 taktów po spójnym odczycie. Sukces wymaga dokładnie jednego wejścia, poprawnego mcause, obserwacji nie wcześniejszej niż deadline, skasowanego pending po rearmie i wykonania instrukcji po \u005ctexttt{wfi}."
},
{
"id": "A5",
"status": "enabled",
"title": "FLOW — source → pending → enable → handler → effect",
"content_tex": "Rosnące mtime osiąga comparator i ustawia pending. Otwarty MTIE oraz MIE pozwalają wejść do wektora. Handler zapisuje obserwację i mcause, przesuwa comparator na \u005ctexttt{UINT64\\_MAX}, publikuje count, a \u005ctexttt{mret} przywraca przerwany przepływ. Main ustawia resumed i zamyka maski."
},
{
"id": "A6",
"status": "enabled",
"title": "STATE — DISARMED, ARMED, PENDING, HANDLED, RESUMED",
"content_tex": "Komparator maksimum reprezentuje DISARMED. Przyszły deadline tworzy ARMED. Po osiągnięciu terminu urządzenie jest PENDING, handler ponownie zapisuje maksimum i publikuje HANDLED, a kod po pętli \u005ctexttt{wfi} potwierdza RESUMED."
},
{
"id": "A7",
"status": "enabled",
"title": "RUNTIME — mcause, mip i mret",
"content_tex": "Raport z RTL ma: count=1, mcause=0x80000007, pending 0/0, resumed=1 i deadline\\_reached=1. Objdump ma pokazać zapis trzech połówek mtimecmp w handlerze oraz końcowe \u005ctexttt{mret}; zwykłe \u005ctexttt{ret} nie byłoby poprawnym powrotem z pułapki."
},
{
"id": "A8",
"status": "enabled",
"title": "PATTERNS — arm before unmask, clear source before publish",
"content_tex": "Najpierw ustaw bezpieczny stan urządzenia, potem włącz źródło w \u005ctexttt{mie}, na końcu globalne MIE. W ISR usuń poziomowe źródło przed opublikowaniem zakończenia; inaczej powrót może natychmiast wejść ponownie."
}
]
},
{
"id": "task03",
"source": "src/tasks/task03_periodic_absolute_deadline.c",
"chapter": "TICK",
"title": "Okresowe deadline'y bez dryfu fazy",
"idea_tex": "deadline += period, tick sequence i lateness",
"priority": "kluczowe",
"key": true,
"prompt_tex": "Dla czterech ticków porównaj scheduled, observed i lateness. Udowodnij stały krok 1600 oraz wyprowadź, o ile przesunąłby następną fazę model now+period. Wyjaśnij granicę: przykład nie nadrabia dowolnej liczby całkowicie pominiętych okresów.",
"evidence_tex": "Przewidywana sekwencja czterech deadline'ów, log RTL Hazard3 z planowanymi i obserwowanymi czasami, kontrola różnic i kodu wyjścia oraz wniosek porównujący deadline+period z now+period.",
"worksheet_step2": "Log RTL: deadline, observed i lateness",
"worksheet_step3": "Dowód stałego kroku i braku dryfu fazy",
"criterion": "Oracle Hazard3: count=causes=4, period=1600, step_ok=ordered=late_math=naive_shift_ok=pass=1. Bieżący pomiar daje cztery lateness po 40 taktów, ale test nie uznaje liczby 40 za kontrakt sprzętowy.",
"viewpoints": [
{
"id": "A1",
"status": "enabled",
"title": "CONTEXT — harmonogram i wykonanie to dwie osie",
"content_tex": "Scheduled opisuje idealną oś czasu usługi, observed chwilę rzeczywistego wejścia do pomiaru w ISR, a lateness ich różnicę. Okres ma aktualizować harmonogram, nie kopiować opóźnienia wykonania do przyszłej fazy."
},
{
"id": "A2",
"status": "enabled",
"title": "STRUCTURE — cztery rekordy ticków",
"content_tex": "Trzy tablice po cztery elementy zapisują deadline, obserwację i lateness. \u005ctexttt{g\\_task03\\_next\\_deadline} jest stanem planisty, a count publikuje liczbę kompletnych rekordów. Stała period wynosi 1600 taktów modelu."
},
{
"id": "A3",
"status": "enabled",
"title": "DISPATCH — każdy MTIP trafia przez slot 7",
"content_tex": "Dla każdego z czterech terminów rdzeń koduje interrupt bit i cause=7 w mcause, a tryb vectored wybiera ten sam \u005ctexttt{isr\\_machine\\_timer}. Handler sprawdza mcause przy każdym wejściu; licznik causes=4 dowodzi czterech decyzji dispatchera."
},
{
"id": "A4",
"status": "enabled",
"title": "APPLICATION — stała faza i zmierzone spóźnienie",
"content_tex": "Dla i>0 musi zachodzić \u005ctexttt{scheduled[i]-scheduled[i-1]=1600}. Dla każdego rekordu observed nie może być wcześniejsze od scheduled, a lateness musi być dokładnie ich różnicą. Po czwartym ticku comparator wraca do maksimum."
},
{
"id": "A5",
"status": "enabled",
"title": "FLOW — sample, record, advance, rearm, publish",
"content_tex": "ISR najpierw pobiera indeks i aktualny deadline, potem czyta czas oraz zapisuje rekord. Następnie oblicza deadline+period, uzbraja ten bezwzględny termin albo rozbraja po ostatnim ticku, a count publikuje dopiero na końcu. Main czeka w \u005ctexttt{wfi} do czterech rekordów."
},
{
"id": "A6",
"status": "enabled",
"title": "STATE — TICK0 → TICK4 i niezmienna faza",
"content_tex": "Stan count przechodzi 0,1,2,3,4; razem z każdym przejściem next\\_deadline rośnie dokładnie o period. Po count=4 urządzenie jest DISARMED. Tablice pozostają historią czterech zakończonych przejść i są analizowane dopiero po zamknięciu masek."
},
{
"id": "A7",
"status": "enabled",
"title": "RUNTIME — cztery terminy i 40 taktów bieżącego RTL",
"content_tex": "Bieżący raport podaje deadline low 0x96b, 0xfab, 0x15eb, 0x1c2b; obserwacje są o 0x28 późniejsze. Ważne są relacje step\\_ok, ordered i late\\_math, ponieważ absolutne wartości oraz 40 taktów mogą się zmienić po zmianie RTL, optymalizacji lub prologu ISR."
},
{
"id": "A8",
"status": "enabled",
"title": "PATTERNS — absolute periodic deadline",
"content_tex": "\u005ctexttt{deadline += period} zachowuje fazę. Gdyby następny termin powstał wyłącznie jako \u005ctexttt{observed + period}, jego przesunięcie względem osi absolutnej byłoby równe bieżącemu lateness; powtarzanie tej reguły kumuluje dryf. Osobna polityka musi zdecydować, czy po dużym opóźnieniu nadrabiać, pomijać, czy zgłaszać błąd."
}
]
}
]
}