chore: preserve current FreeRTOS and C card updates
This commit is contained in:
@@ -73,7 +73,7 @@
|
|||||||
\noindent\fbox{%
|
\noindent\fbox{%
|
||||||
\begin{minipage}[c][23.5mm][c]{\dimexpr\textwidth-2\fboxrule\relax}%
|
\begin{minipage}[c][23.5mm][c]{\dimexpr\textwidth-2\fboxrule\relax}%
|
||||||
\begin{minipage}[c][23mm][c]{24mm}\centering%
|
\begin{minipage}[c][23mm][c]{24mm}\centering%
|
||||||
\qrcode[level=L,height=22mm]{https://zsl-gitea.mpabi.pl/edu-freertos-c/lab-rv32i-freertos-c-event-groups}%
|
\href{https://zsl-gitea.mpabi.pl/edu-freertos-c/lab-rv32i-freertos-c-event-groups}{\qrcode[level=L,height=22mm]{https://zsl-gitea.mpabi.pl/edu-freertos-c/lab-rv32i-freertos-c-event-groups}}%
|
||||||
\end{minipage}%
|
\end{minipage}%
|
||||||
\vrule width0.35pt%
|
\vrule width0.35pt%
|
||||||
\begin{minipage}[c][23mm][c]{\dimexpr\linewidth-48mm-0.7pt\relax}%
|
\begin{minipage}[c][23mm][c]{\dimexpr\linewidth-48mm-0.7pt\relax}%
|
||||||
@@ -109,7 +109,7 @@
|
|||||||
\end{minipage}%
|
\end{minipage}%
|
||||||
\vrule width0.35pt%
|
\vrule width0.35pt%
|
||||||
\begin{minipage}[c][23mm][c]{24mm}\centering%
|
\begin{minipage}[c][23mm][c]{24mm}\centering%
|
||||||
\qrcode[level=L,height=22mm]{https://dce7fb9d-7b2f-5d49-96a2-3a30d3070b84.mpabi.pl/3f4c1b8b-d54b-58d5-b92d-87a7233cbd9f}%
|
\href{https://dce7fb9d-7b2f-5d49-96a2-3a30d3070b84.mpabi.pl/3f4c1b8b-d54b-58d5-b92d-87a7233cbd9f}{\qrcode[level=L,height=22mm]{https://dce7fb9d-7b2f-5d49-96a2-3a30d3070b84.mpabi.pl/3f4c1b8b-d54b-58d5-b92d-87a7233cbd9f}}%
|
||||||
\end{minipage}%
|
\end{minipage}%
|
||||||
\end{minipage}%
|
\end{minipage}%
|
||||||
}%
|
}%
|
||||||
@@ -197,7 +197,7 @@ Uczeń projektuje rozłączne maski EventGroup i dowodzi różnicy między oczek
|
|||||||
\vspace{0.7em}
|
\vspace{0.7em}
|
||||||
\noindent{\Large\bfseries Zakres karty}\par
|
\noindent{\Large\bfseries Zakres karty}\par
|
||||||
\vspace{0.35em}
|
\vspace{0.35em}
|
||||||
Koordynator p3 blokuje się na READY_ALL. Worker A ustawia READY_A i blokuje się w xEventGroupSync. Worker B potwierdza maskę częściową, ustawia READY_B, po czym koordynator wnosi SYNC_C. Ostatni SYNC_B zwalnia wszystkich; każdy wynik zawiera 0x70, a automatycznie wyczyszczona grupa kończy z 0.
|
Koordynator p3 blokuje się na \texttt{READY\_ALL}. Worker A ustawia \texttt{READY\_A} i blokuje się w \texttt{xEventGroupSync}. Worker B potwierdza maskę częściową, ustawia \texttt{READY\_B}, po czym koordynator wnosi \texttt{SYNC\_C}. Ostatni \texttt{SYNC\_B} zwalnia wszystkich; każdy wynik zawiera 0x70, a automatycznie wyczyszczona grupa kończy z 0.
|
||||||
\vspace{0.55em}
|
\vspace{0.55em}
|
||||||
\small\begin{tabularx}{\textwidth}{@{}>{\ttfamily\raggedright\arraybackslash}p{0.85cm}>{\ttfamily\raggedright\arraybackslash}p{1.45cm}X>{\raggedright\arraybackslash}p{2.45cm}>{\raggedright\arraybackslash}p{1.75cm}>{\ttfamily\raggedright\arraybackslash}p{1.50cm}@{}}
|
\small\begin{tabularx}{\textwidth}{@{}>{\ttfamily\raggedright\arraybackslash}p{0.85cm}>{\ttfamily\raggedright\arraybackslash}p{1.45cm}X>{\raggedright\arraybackslash}p{2.45cm}>{\raggedright\arraybackslash}p{1.75cm}>{\ttfamily\raggedright\arraybackslash}p{1.50cm}@{}}
|
||||||
\textbf{Lekcja} & \textbf{Task} & \textbf{Najważniejsza idea} & \textbf{Priorytet} & \textbf{Status} & \textbf{Version} \\ \hline
|
\textbf{Lekcja} & \textbf{Task} & \textbf{Najważniejsza idea} & \textbf{Priorytet} & \textbf{Status} & \textbf{Version} \\ \hline
|
||||||
@@ -319,7 +319,7 @@ Zapisz final bits, SP, PASS i digest.
|
|||||||
\end{ESCStepFrame}
|
\end{ESCStepFrame}
|
||||||
\end{ESCBlockFrame}
|
\end{ESCBlockFrame}
|
||||||
\begin{ESCBlockFrame}{Ćwiczenie · Ćwiczenie — ANY kontra ALL}
|
\begin{ESCBlockFrame}{Ćwiczenie · Ćwiczenie — ANY kontra ALL}
|
||||||
Uruchom kontrolowany wariant wait ANY na tej samej sekwencji READY_A/READY_B. Zachowaj osobne maski i porównaj moment release oraz wartość zwrotną.
|
Uruchom kontrolowany wariant wait ANY na tej samej sekwencji \texttt{READY\_A/READY\_B}. Zachowaj osobne maski i porównaj moment release oraz wartość zwrotną.
|
||||||
\par\textbf{Evidence:} Dwa timestampowane ślady i tabela semantyki clear-on-exit.
|
\par\textbf{Evidence:} Dwa timestampowane ślady i tabela semantyki clear-on-exit.
|
||||||
\par\textbf{Acceptance:} Uczeń nie przypisuje API gwarancji kolejności równorzędnych waiterów.
|
\par\textbf{Acceptance:} Uczeń nie przypisuje API gwarancji kolejności równorzędnych waiterów.
|
||||||
\end{ESCBlockFrame}
|
\end{ESCBlockFrame}
|
||||||
|
|||||||
@@ -237,7 +237,7 @@
|
|||||||
"title": "Cel karty",
|
"title": "Cel karty",
|
||||||
"content_tex": "Uczeń projektuje rozłączne maski EventGroup i dowodzi różnicy między oczekiwaniem ALL a trzyosobową barierą.",
|
"content_tex": "Uczeń projektuje rozłączne maski EventGroup i dowodzi różnicy między oczekiwaniem ALL a trzyosobową barierą.",
|
||||||
"scope_title": "Zakres karty",
|
"scope_title": "Zakres karty",
|
||||||
"scope_content_tex": "Koordynator p3 blokuje się na READY_ALL. Worker A ustawia READY_A i blokuje się w xEventGroupSync. Worker B potwierdza maskę częściową, ustawia READY_B, po czym koordynator wnosi SYNC_C. Ostatni SYNC_B zwalnia wszystkich; każdy wynik zawiera 0x70, a automatycznie wyczyszczona grupa kończy z 0.",
|
"scope_content_tex": "Koordynator p3 blokuje się na \\texttt{READY\\_ALL}. Worker A ustawia \\texttt{READY\\_A} i blokuje się w \\texttt{xEventGroupSync}. Worker B potwierdza maskę częściową, ustawia \\texttt{READY\\_B}, po czym koordynator wnosi \\texttt{SYNC\\_C}. Ostatni \\texttt{SYNC\\_B} zwalnia wszystkich; każdy wynik zawiera 0x70, a automatycznie wyczyszczona grupa kończy z 0.",
|
||||||
"scope_table": {
|
"scope_table": {
|
||||||
"headers": [
|
"headers": [
|
||||||
"Lekcja",
|
"Lekcja",
|
||||||
@@ -585,7 +585,7 @@
|
|||||||
"content_kind": "prose",
|
"content_kind": "prose",
|
||||||
"asset_page_mode": "one-per-page",
|
"asset_page_mode": "one-per-page",
|
||||||
"page_orientation": "landscape",
|
"page_orientation": "landscape",
|
||||||
"content_tex": "EventBits_t jest wspólną wartością bitową. Znaczenie każdego bitu wynika wyłącznie z jawnego kontraktu aplikacji.",
|
"content_tex": "\\texttt{EventBits\\_t} jest wspólną wartością bitową. Znaczenie każdego bitu wynika wyłącznie z jawnego kontraktu aplikacji.",
|
||||||
"assets": [
|
"assets": [
|
||||||
{
|
{
|
||||||
"path": "assets/a2-structure.png",
|
"path": "assets/a2-structure.png",
|
||||||
@@ -1457,7 +1457,7 @@
|
|||||||
"kind": "exercise",
|
"kind": "exercise",
|
||||||
"id": "any-all",
|
"id": "any-all",
|
||||||
"title": "Ćwiczenie — ANY kontra ALL",
|
"title": "Ćwiczenie — ANY kontra ALL",
|
||||||
"prompt_tex": "Uruchom kontrolowany wariant wait ANY na tej samej sekwencji READY_A/READY_B. Zachowaj osobne maski i porównaj moment release oraz wartość zwrotną.",
|
"prompt_tex": "Uruchom kontrolowany wariant wait ANY na tej samej sekwencji \\texttt{READY\\_A/READY\\_B}. Zachowaj osobne maski i porównaj moment release oraz wartość zwrotną.",
|
||||||
"evidence_tex": "Dwa timestampowane ślady i tabela semantyki clear-on-exit.",
|
"evidence_tex": "Dwa timestampowane ślady i tabela semantyki clear-on-exit.",
|
||||||
"criterion": "Uczeń nie przypisuje API gwarancji kolejności równorzędnych waiterów.",
|
"criterion": "Uczeń nie przypisuje API gwarancji kolejności równorzędnych waiterów.",
|
||||||
"based_on": [
|
"based_on": [
|
||||||
|
|||||||
+3
-3
@@ -1,6 +1,6 @@
|
|||||||
{
|
{
|
||||||
"card":{"number":"09","slug":"event-groups","title":"Event Groups: ALL-ready i bariera","topic":"bit masks, wait semantics, automatic clear i xEventGroupSync","status":"Gotowa","version":"v00.01"},
|
"card":{"number":"09","slug":"event-groups","title":"Event Groups: ALL-ready i bariera","topic":"bit masks, wait semantics, automatic clear i xEventGroupSync","status":"Gotowa","version":"v00.01"},
|
||||||
"front":{"goal":"Uczeń projektuje rozłączne maski EventGroup i dowodzi różnicy między oczekiwaniem ALL a trzyosobową barierą.","scope":"Koordynator p3 blokuje się na READY_ALL. Worker A ustawia READY_A i blokuje się w xEventGroupSync. Worker B potwierdza maskę częściową, ustawia READY_B, po czym koordynator wnosi SYNC_C. Ostatni SYNC_B zwalnia wszystkich; każdy wynik zawiera 0x70, a automatycznie wyczyszczona grupa kończy z 0."},
|
"front":{"goal":"Uczeń projektuje rozłączne maski EventGroup i dowodzi różnicy między oczekiwaniem ALL a trzyosobową barierą.","scope":"Koordynator p3 blokuje się na \\texttt{READY\\_ALL}. Worker A ustawia \\texttt{READY\\_A} i blokuje się w \\texttt{xEventGroupSync}. Worker B potwierdza maskę częściową, ustawia \\texttt{READY\\_B}, po czym koordynator wnosi \\texttt{SYNC\\_C}. Ostatni \\texttt{SYNC\\_B} zwalnia wszystkich; każdy wynik zawiera 0x70, a automatycznie wyczyszczona grupa kończy z 0."},
|
||||||
"viewpoints":[
|
"viewpoints":[
|
||||||
{"id":"A1","label":"CONTEXT","status":"unavailable","subtitle":"Granice","reason":"Bez nowej granicy sprzętowej lub callbacku."},
|
{"id":"A1","label":"CONTEXT","status":"unavailable","subtitle":"Granice","reason":"Bez nowej granicy sprzętowej lub callbacku."},
|
||||||
{"id":"A2","label":"STRUCTURE","status":"enabled","subtitle":"EventGroup, masks i participants"},
|
{"id":"A2","label":"STRUCTURE","status":"enabled","subtitle":"EventGroup, masks i participants"},
|
||||||
@@ -32,7 +32,7 @@
|
|||||||
"task01.pass":{"event_id":"E11","stop":{"symbol":"fc09_checkpoint_committed","offset":0,"condition":"$a0 == 11"},"verify":{"expressions":[{"expr":"g_fc09_pass","equals":1},{"expr":"g_fc09.final_bits","equals":0},{"expr":"g_fc09_event_count","equals":11}]}}
|
"task01.pass":{"event_id":"E11","stop":{"symbol":"fc09_checkpoint_committed","offset":0,"condition":"$a0 == 11"},"verify":{"expressions":[{"expr":"g_fc09_pass","equals":1},{"expr":"g_fc09.final_bits","equals":0},{"expr":"g_fc09_event_count","equals":11}]}}
|
||||||
},
|
},
|
||||||
"sections":[
|
"sections":[
|
||||||
{"id":"A2","label":"STRUCTURE","title":"Structure","order":20,"orientation":"landscape","description":"One group, two disjoint protocols and three participants.","content_tex":"EventBits_t jest wspólną wartością bitową. Znaczenie każdego bitu wynika wyłącznie z jawnego kontraktu aplikacji.","assets":[{"stem":"a2-structure","title":"A2 · masks and participants","caption":"A2 STRUCTURE — READY and SYNC masks.","label":"fig:a2-structure","alt":"Struktura EventGroup.","phases":[{"id":"structure","label":"GROUP / MASKS / PARTICIPANTS","steps":[
|
{"id":"A2","label":"STRUCTURE","title":"Structure","order":20,"orientation":"landscape","description":"One group, two disjoint protocols and three participants.","content_tex":"\\texttt{EventBits\\_t} jest wspólną wartością bitową. Znaczenie każdego bitu wynika wyłącznie z jawnego kontraktu aplikacji.","assets":[{"stem":"a2-structure","title":"A2 · masks and participants","caption":"A2 STRUCTURE — READY and SYNC masks.","label":"fig:a2-structure","alt":"Struktura EventGroup.","phases":[{"id":"structure","label":"GROUP / MASKS / PARTICIPANTS","steps":[
|
||||||
{"id":"group","number":1,"label":"one real EventGroup","mode":"CODE","strategy_ref":"code.protocol","svg_label":"01","code_ref":"src/tasks/task01_event_groups.c:261","description":"Kernel object holds bits and wait lists.","evidence":"xEventGroupCreate symbol."},
|
{"id":"group","number":1,"label":"one real EventGroup","mode":"CODE","strategy_ref":"code.protocol","svg_label":"01","code_ref":"src/tasks/task01_event_groups.c:261","description":"Kernel object holds bits and wait lists.","evidence":"xEventGroupCreate symbol."},
|
||||||
{"id":"ready","number":2,"label":"READY bits are disjoint","mode":"CODE","strategy_ref":"code.protocol","svg_label":"02","code_ref":"include/task01_event_groups.h:11","description":"A and B own one bit each.","evidence":"ALL=0x03."},
|
{"id":"ready","number":2,"label":"READY bits are disjoint","mode":"CODE","strategy_ref":"code.protocol","svg_label":"02","code_ref":"include/task01_event_groups.h:11","description":"A and B own one bit each.","evidence":"ALL=0x03."},
|
||||||
{"id":"sync","number":3,"label":"SYNC is a separate mask","mode":"CODE","strategy_ref":"code.protocol","svg_label":"03","code_ref":"include/task01_event_groups.h:14","description":"Barrier cannot consume readiness meaning.","evidence":"ALL=0x70."},
|
{"id":"sync","number":3,"label":"SYNC is a separate mask","mode":"CODE","strategy_ref":"code.protocol","svg_label":"03","code_ref":"include/task01_event_groups.h:14","description":"Barrier cannot consume readiness meaning.","evidence":"ALL=0x70."},
|
||||||
@@ -86,6 +86,6 @@
|
|||||||
"task":{"short_label":"EventGroup","title":"ALL-ready i trzyosobowa bariera","prompt_tex":"Przejdź po A2, A4, A5, A6, A7 i A8. Odtwórz E01–E11 i udowodnij, że maska częściowa nie zwalnia tasków, a bariera zwalnia wszystkich dokładnie raz.","conclusion_tex":"EventGroup przechowuje bity stanu protokołu, nie historię zdarzeń. Rozłączne maski i jawne reguły clear są warunkiem poprawnej synchronizacji.","flow":[
|
"task":{"short_label":"EventGroup","title":"ALL-ready i trzyosobowa bariera","prompt_tex":"Przejdź po A2, A4, A5, A6, A7 i A8. Odtwórz E01–E11 i udowodnij, że maska częściowa nie zwalnia tasków, a bariera zwalnia wszystkich dokładnie raz.","conclusion_tex":"EventGroup przechowuje bity stanu protokołu, nie historię zdarzeń. Rozłączne maski i jawne reguły clear są warunkiem poprawnej synchronizacji.","flow":[
|
||||||
{"kind":"block","id":"predict","title":"A — mask table","content_tex":"Przypisz READY i SYNC do właścicieli.","steps":[{"id":"partial","title":"Przewidź 0x11.","content_tex":"Wskaż, które taski muszą być Blocked."},{"id":"clear","title":"Przewidź final zero.","content_tex":"Rozdziel clear-on-exit od barrier auto-clear."}]},
|
{"kind":"block","id":"predict","title":"A — mask table","content_tex":"Przypisz READY i SYNC do właścicieli.","steps":[{"id":"partial","title":"Przewidź 0x11.","content_tex":"Wskaż, które taski muszą być Blocked."},{"id":"clear","title":"Przewidź final zero.","content_tex":"Rozdziel clear-on-exit od barrier auto-clear."}]},
|
||||||
{"kind":"block","id":"replay","title":"B — replay Hazard3","content_tex":"RUN zaczyna się od czystej RAM.","steps":[{"id":"ready","title":"Zbadaj E02–E06.","content_tex":"Porównaj maski i task states."},{"id":"barrier","title":"Zbadaj E07–E10.","content_tex":"Porównaj trzy wartości zwrotne."},{"id":"pass","title":"Zbadaj E11.","content_tex":"Zapisz final bits, SP, PASS i digest."}]},
|
{"kind":"block","id":"replay","title":"B — replay Hazard3","content_tex":"RUN zaczyna się od czystej RAM.","steps":[{"id":"ready","title":"Zbadaj E02–E06.","content_tex":"Porównaj maski i task states."},{"id":"barrier","title":"Zbadaj E07–E10.","content_tex":"Porównaj trzy wartości zwrotne."},{"id":"pass","title":"Zbadaj E11.","content_tex":"Zapisz final bits, SP, PASS i digest."}]},
|
||||||
{"kind":"exercise","id":"any-all","title":"Ćwiczenie — ANY kontra ALL","prompt_tex":"Uruchom kontrolowany wariant wait ANY na tej samej sekwencji READY_A/READY_B. Zachowaj osobne maski i porównaj moment release oraz wartość zwrotną.","evidence_tex":"Dwa timestampowane ślady i tabela semantyki clear-on-exit.","criterion":"Uczeń nie przypisuje API gwarancji kolejności równorzędnych waiterów.","based_on":["predict","replay"]}
|
{"kind":"exercise","id":"any-all","title":"Ćwiczenie — ANY kontra ALL","prompt_tex":"Uruchom kontrolowany wariant wait ANY na tej samej sekwencji \\texttt{READY\\_A/READY\\_B}. Zachowaj osobne maski i porównaj moment release oraz wartość zwrotną.","evidence_tex":"Dwa timestampowane ślady i tabela semantyki clear-on-exit.","criterion":"Uczeń nie przypisuje API gwarancji kolejności równorzędnych waiterów.","based_on":["predict","replay"]}
|
||||||
]}
|
]}
|
||||||
}
|
}
|
||||||
|
|||||||
+1
-1
File diff suppressed because one or more lines are too long
+9
-9
File diff suppressed because one or more lines are too long
+127
-57
File diff suppressed because one or more lines are too long
Reference in New Issue
Block a user