Compare commits
1 Commits
| Author | SHA1 | Date | |
|---|---|---|---|
| 521e9259fd |
@@ -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-isr-semaphore}%
|
\href{https://zsl-gitea.mpabi.pl/edu-freertos-c/lab-rv32i-freertos-c-isr-semaphore}{\qrcode[level=L,height=22mm]{https://zsl-gitea.mpabi.pl/edu-freertos-c/lab-rv32i-freertos-c-isr-semaphore}}%
|
||||||
\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/a6da1075-8d1f-5615-b0e6-0fc33e59e1e3}%
|
\href{https://dce7fb9d-7b2f-5d49-96a2-3a30d3070b84.mpabi.pl/a6da1075-8d1f-5615-b0e6-0fc33e59e1e3}{\qrcode[level=L,height=22mm]{https://dce7fb9d-7b2f-5d49-96a2-3a30d3070b84.mpabi.pl/a6da1075-8d1f-5615-b0e6-0fc33e59e1e3}}%
|
||||||
\end{minipage}%
|
\end{minipage}%
|
||||||
\end{minipage}%
|
\end{minipage}%
|
||||||
}%
|
}%
|
||||||
@@ -197,7 +197,7 @@ Uczeń rozdziela task context od ISR context, używa API FromISR i dowodzi natyc
|
|||||||
\vspace{0.7em}
|
\vspace{0.7em}
|
||||||
\noindent{\Large\bfseries Zakres karty}\par
|
\noindent{\Large\bfseries Zakres karty}\par
|
||||||
\vspace{0.35em}
|
\vspace{0.35em}
|
||||||
Prawdziwe wejście IRQ5 testbencha wywołuje machine external interrupt. Port zapisuje pełny kontekst i przechodzi na xISRStack. ISR czyści źródło, daje binary semaphore i wywołuje portYIELD_FROM_ISR. Waiter priority 3 działa przed powrotem do stimulus priority 2.
|
Prawdziwe wejście IRQ5 testbencha wywołuje machine external interrupt. Port zapisuje pełny kontekst i przechodzi na \texttt{xISRStack}. ISR czyści źródło, daje binary semaphore i wywołuje \texttt{portYIELD\_FROM\_ISR}. Waiter priority 3 działa przed powrotem do stimulus priority 2.
|
||||||
\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
|
||||||
@@ -295,7 +295,7 @@ Wskaż, czy pierwszy wykona się waiter czy stimulus.
|
|||||||
\begin{ESCBlockFrame}{B — replay Hazard3}
|
\begin{ESCBlockFrame}{B — replay Hazard3}
|
||||||
Każdy RUN zaczyna się od czystej RAM i wyłączonego źródła.
|
Każdy RUN zaczyna się od czystej RAM i wyłączonego źródła.
|
||||||
\begin{ESCStepFrame}{trap · Zbadaj E03–E05.}
|
\begin{ESCStepFrame}{trap · Zbadaj E03–E05.}
|
||||||
Zapisz mcause, mepc, isr_sp i source state.
|
Zapisz \texttt{mcause}, \texttt{mepc}, \texttt{isr\_sp} i source state.
|
||||||
\end{ESCStepFrame}
|
\end{ESCStepFrame}
|
||||||
\begin{ESCStepFrame}{handoff · Zbadaj E06–E08.}
|
\begin{ESCStepFrame}{handoff · Zbadaj E06–E08.}
|
||||||
Porównaj xHPW i kolejność tasków.
|
Porównaj xHPW i kolejność tasków.
|
||||||
@@ -305,14 +305,14 @@ Sprawdź trzy stosy, markers i digest.
|
|||||||
\end{ESCStepFrame}
|
\end{ESCStepFrame}
|
||||||
\end{ESCBlockFrame}
|
\end{ESCBlockFrame}
|
||||||
\begin{ESCBlockFrame}{Ćwiczenie · Ćwiczenie — brak yield request}
|
\begin{ESCBlockFrame}{Ćwiczenie · Ćwiczenie — brak yield request}
|
||||||
W kontrolowanym wariancie pomiń portYIELD_FROM_ISR, zachowując GiveFromISR. Zmierz, kiedy waiter zacznie działać i wskaż następny legalny scheduling point.
|
W kontrolowanym wariancie pomiń \texttt{portYIELD\_FROM\_ISR}, zachowując GiveFromISR. Zmierz, kiedy waiter zacznie działać i wskaż następny legalny scheduling point.
|
||||||
\par\textbf{Evidence:} Dwa timestampowane ślady E07/E08 z yield i bez yield oraz opis różnicy.
|
\par\textbf{Evidence:} Dwa timestampowane ślady E07/E08 z yield i bez yield oraz opis różnicy.
|
||||||
\par\textbf{Acceptance:} Uczeń nie myli odblokowania taska z natychmiastowym wykonaniem i przywraca poprawny yield w wersji finalnej.
|
\par\textbf{Acceptance:} Uczeń nie myli odblokowania taska z natychmiastowym wykonaniem i przywraca poprawny yield w wersji finalnej.
|
||||||
\end{ESCBlockFrame}
|
\end{ESCBlockFrame}
|
||||||
\tcblower\textbf{Task acceptance:} PASS; mcause=MEI; source=0 przed give; xHPW=1; waiter E07 przed stimulus E08; trzy różne stosy; deterministyczny digest.
|
\tcblower\textbf{Task acceptance:} PASS; mcause=MEI; source=0 przed give; xHPW=1; waiter E07 przed stimulus E08; trzy różne stosy; deterministyczny digest.
|
||||||
\end{ESCTaskFrame}
|
\end{ESCTaskFrame}
|
||||||
\begin{ESCConclusionFrame}
|
\begin{ESCConclusionFrame}
|
||||||
ISR działa na osobnym stacku i używa FromISR API. xHigherPriorityTaskWoken jest informacją dla portu; dopiero portYIELD_FROM_ISR powoduje restore kontekstu wyższego taska przed powrotem do przerwanego kodu.
|
ISR działa na osobnym stacku i używa FromISR API. \texttt{xHigherPriorityTaskWoken} jest informacją dla portu; dopiero \texttt{portYIELD\_FROM\_ISR} powoduje restore kontekstu wyższego taska przed powrotem do przerwanego kodu.
|
||||||
\end{ESCConclusionFrame}
|
\end{ESCConclusionFrame}
|
||||||
\ESCSectionBlockEnd
|
\ESCSectionBlockEnd
|
||||||
|
|
||||||
|
|||||||
@@ -245,7 +245,7 @@
|
|||||||
"title": "Cel karty",
|
"title": "Cel karty",
|
||||||
"content_tex": "Uczeń rozdziela task context od ISR context, używa API FromISR i dowodzi natychmiastowego przełączenia do wyższego taska.",
|
"content_tex": "Uczeń rozdziela task context od ISR context, używa API FromISR i dowodzi natychmiastowego przełączenia do wyższego taska.",
|
||||||
"scope_title": "Zakres karty",
|
"scope_title": "Zakres karty",
|
||||||
"scope_content_tex": "Prawdziwe wejście IRQ5 testbencha wywołuje machine external interrupt. Port zapisuje pełny kontekst i przechodzi na xISRStack. ISR czyści źródło, daje binary semaphore i wywołuje portYIELD_FROM_ISR. Waiter priority 3 działa przed powrotem do stimulus priority 2.",
|
"scope_content_tex": "Prawdziwe wejście IRQ5 testbencha wywołuje machine external interrupt. Port zapisuje pełny kontekst i przechodzi na \\texttt{xISRStack}. ISR czyści źródło, daje binary semaphore i wywołuje \\texttt{portYIELD\\_FROM\\_ISR}. Waiter priority 3 działa przed powrotem do stimulus priority 2.",
|
||||||
"scope_table": {
|
"scope_table": {
|
||||||
"headers": [
|
"headers": [
|
||||||
"Lekcja",
|
"Lekcja",
|
||||||
@@ -1293,7 +1293,7 @@
|
|||||||
"uuid": "a6da1075-8d1f-5615-b0e6-0fc33e59e1e3",
|
"uuid": "a6da1075-8d1f-5615-b0e6-0fc33e59e1e3",
|
||||||
"prompt_tex": "Przejdź po A1, A3, A5, A6 i A7. Odtwórz E01–E09 i udowodnij source-clear-before-give oraz waiter-before-stimulus.",
|
"prompt_tex": "Przejdź po A1, A3, A5, A6 i A7. Odtwórz E01–E09 i udowodnij source-clear-before-give oraz waiter-before-stimulus.",
|
||||||
"criterion": "PASS; mcause=MEI; source=0 przed give; xHPW=1; waiter E07 przed stimulus E08; trzy różne stosy; deterministyczny digest.",
|
"criterion": "PASS; mcause=MEI; source=0 przed give; xHPW=1; waiter E07 przed stimulus E08; trzy różne stosy; deterministyczny digest.",
|
||||||
"conclusion_tex": "ISR działa na osobnym stacku i używa FromISR API. xHigherPriorityTaskWoken jest informacją dla portu; dopiero portYIELD_FROM_ISR powoduje restore kontekstu wyższego taska przed powrotem do przerwanego kodu.",
|
"conclusion_tex": "ISR działa na osobnym stacku i używa FromISR API. \\texttt{xHigherPriorityTaskWoken} jest informacją dla portu; dopiero \\texttt{portYIELD\\_FROM\\_ISR} powoduje restore kontekstu wyższego taska przed powrotem do przerwanego kodu.",
|
||||||
"flow": [
|
"flow": [
|
||||||
{
|
{
|
||||||
"kind": "block",
|
"kind": "block",
|
||||||
@@ -1322,7 +1322,7 @@
|
|||||||
{
|
{
|
||||||
"id": "trap",
|
"id": "trap",
|
||||||
"title": "Zbadaj E03–E05.",
|
"title": "Zbadaj E03–E05.",
|
||||||
"content_tex": "Zapisz mcause, mepc, isr_sp i source state."
|
"content_tex": "Zapisz \\texttt{mcause}, \\texttt{mepc}, \\texttt{isr\\_sp} i source state."
|
||||||
},
|
},
|
||||||
{
|
{
|
||||||
"id": "handoff",
|
"id": "handoff",
|
||||||
@@ -1340,7 +1340,7 @@
|
|||||||
"kind": "exercise",
|
"kind": "exercise",
|
||||||
"id": "no-yield",
|
"id": "no-yield",
|
||||||
"title": "Ćwiczenie — brak yield request",
|
"title": "Ćwiczenie — brak yield request",
|
||||||
"prompt_tex": "W kontrolowanym wariancie pomiń portYIELD_FROM_ISR, zachowując GiveFromISR. Zmierz, kiedy waiter zacznie działać i wskaż następny legalny scheduling point.",
|
"prompt_tex": "W kontrolowanym wariancie pomiń \\texttt{portYIELD\\_FROM\\_ISR}, zachowując GiveFromISR. Zmierz, kiedy waiter zacznie działać i wskaż następny legalny scheduling point.",
|
||||||
"evidence_tex": "Dwa timestampowane ślady E07/E08 z yield i bez yield oraz opis różnicy.",
|
"evidence_tex": "Dwa timestampowane ślady E07/E08 z yield i bez yield oraz opis różnicy.",
|
||||||
"criterion": "Uczeń nie myli odblokowania taska z natychmiastowym wykonaniem i przywraca poprawny yield w wersji finalnej.",
|
"criterion": "Uczeń nie myli odblokowania taska z natychmiastowym wykonaniem i przywraca poprawny yield w wersji finalnej.",
|
||||||
"based_on": [
|
"based_on": [
|
||||||
|
|||||||
+4
-4
@@ -1,6 +1,6 @@
|
|||||||
{
|
{
|
||||||
"card":{"number":"07","slug":"isr-semaphore","title":"Przerwanie zewnętrzne i semaphore FromISR","topic":"Hazard3 MEI, xISRStack, xSemaphoreGiveFromISR i yield","status":"Gotowa","version":"v00.01"},
|
"card":{"number":"07","slug":"isr-semaphore","title":"Przerwanie zewnętrzne i semaphore FromISR","topic":"Hazard3 MEI, xISRStack, xSemaphoreGiveFromISR i yield","status":"Gotowa","version":"v00.01"},
|
||||||
"front":{"goal":"Uczeń rozdziela task context od ISR context, używa API FromISR i dowodzi natychmiastowego przełączenia do wyższego taska.","scope":"Prawdziwe wejście IRQ5 testbencha wywołuje machine external interrupt. Port zapisuje pełny kontekst i przechodzi na xISRStack. ISR czyści źródło, daje binary semaphore i wywołuje portYIELD_FROM_ISR. Waiter priority 3 działa przed powrotem do stimulus priority 2."},
|
"front":{"goal":"Uczeń rozdziela task context od ISR context, używa API FromISR i dowodzi natychmiastowego przełączenia do wyższego taska.","scope":"Prawdziwe wejście IRQ5 testbencha wywołuje machine external interrupt. Port zapisuje pełny kontekst i przechodzi na \\texttt{xISRStack}. ISR czyści źródło, daje binary semaphore i wywołuje \\texttt{portYIELD\\_FROM\\_ISR}. Waiter priority 3 działa przed powrotem do stimulus priority 2."},
|
||||||
"viewpoints":[
|
"viewpoints":[
|
||||||
{"id":"A1","label":"CONTEXT","status":"enabled","subtitle":"Testbench → Hazard3 → port → task"},
|
{"id":"A1","label":"CONTEXT","status":"enabled","subtitle":"Testbench → Hazard3 → port → task"},
|
||||||
{"id":"A2","label":"STRUCTURE","status":"unavailable","subtitle":"Struktura","reason":"Obiekty runtime i ich relacje są pełniej pokazane w A7."},
|
{"id":"A2","label":"STRUCTURE","status":"unavailable","subtitle":"Struktura","reason":"Obiekty runtime i ich relacje są pełniej pokazane w A7."},
|
||||||
@@ -74,9 +74,9 @@
|
|||||||
]}]}]}
|
]}]}]}
|
||||||
],
|
],
|
||||||
"learning":{"model_label":"Model ISR handoff","model":"Uczeń rozdziela hardware source, trap port, xISRStack, FromISR API i task scheduling.","replay_label":"Replay realnego MEI","replay":"Uczeń odtwarza E01–E09 i wiąże mcause, source clear, xHPW, trzy SP oraz kolejność context restore.","criterion":"PASS; mcause=MEI; source=0 przed give; xHPW=1; waiter E07 przed stimulus E08; trzy różne stosy; deterministyczny digest.","requirement":"Zaprojektowanie i zbadanie bezpiecznego handoff z prawdziwego przerwania do taska FreeRTOS."},
|
"learning":{"model_label":"Model ISR handoff","model":"Uczeń rozdziela hardware source, trap port, xISRStack, FromISR API i task scheduling.","replay_label":"Replay realnego MEI","replay":"Uczeń odtwarza E01–E09 i wiąże mcause, source clear, xHPW, trzy SP oraz kolejność context restore.","criterion":"PASS; mcause=MEI; source=0 przed give; xHPW=1; waiter E07 przed stimulus E08; trzy różne stosy; deterministyczny digest.","requirement":"Zaprojektowanie i zbadanie bezpiecznego handoff z prawdziwego przerwania do taska FreeRTOS."},
|
||||||
"task":{"short_label":"ISR semaphore","title":"External IRQ → FromISR semaphore → high-priority task","prompt_tex":"Przejdź po A1, A3, A5, A6 i A7. Odtwórz E01–E09 i udowodnij source-clear-before-give oraz waiter-before-stimulus.","conclusion_tex":"ISR działa na osobnym stacku i używa FromISR API. xHigherPriorityTaskWoken jest informacją dla portu; dopiero portYIELD_FROM_ISR powoduje restore kontekstu wyższego taska przed powrotem do przerwanego kodu.","flow":[
|
"task":{"short_label":"ISR semaphore","title":"External IRQ → FromISR semaphore → high-priority task","prompt_tex":"Przejdź po A1, A3, A5, A6 i A7. Odtwórz E01–E09 i udowodnij source-clear-before-give oraz waiter-before-stimulus.","conclusion_tex":"ISR działa na osobnym stacku i używa FromISR API. \\texttt{xHigherPriorityTaskWoken} jest informacją dla portu; dopiero \\texttt{portYIELD\\_FROM\\_ISR} powoduje restore kontekstu wyższego taska przed powrotem do przerwanego kodu.","flow":[
|
||||||
{"kind":"block","id":"contract","title":"A — kontrakt przerwania","content_tex":"Rozdziel source, vector, port, ISR i task.","steps":[{"id":"order","title":"Ustal kolejność ISR.","content_tex":"Najpierw clear, potem give, na końcu yield."},{"id":"predict","title":"Przewidź context restore.","content_tex":"Wskaż, czy pierwszy wykona się waiter czy stimulus."}]},
|
{"kind":"block","id":"contract","title":"A — kontrakt przerwania","content_tex":"Rozdziel source, vector, port, ISR i task.","steps":[{"id":"order","title":"Ustal kolejność ISR.","content_tex":"Najpierw clear, potem give, na końcu yield."},{"id":"predict","title":"Przewidź context restore.","content_tex":"Wskaż, czy pierwszy wykona się waiter czy stimulus."}]},
|
||||||
{"kind":"block","id":"replay","title":"B — replay Hazard3","content_tex":"Każdy RUN zaczyna się od czystej RAM i wyłączonego źródła.","steps":[{"id":"trap","title":"Zbadaj E03–E05.","content_tex":"Zapisz mcause, mepc, isr_sp i source state."},{"id":"handoff","title":"Zbadaj E06–E08.","content_tex":"Porównaj xHPW i kolejność tasków."},{"id":"pass","title":"Zbadaj E09.","content_tex":"Sprawdź trzy stosy, markers i digest."}]},
|
{"kind":"block","id":"replay","title":"B — replay Hazard3","content_tex":"Każdy RUN zaczyna się od czystej RAM i wyłączonego źródła.","steps":[{"id":"trap","title":"Zbadaj E03–E05.","content_tex":"Zapisz \\texttt{mcause}, \\texttt{mepc}, \\texttt{isr\\_sp} i source state."},{"id":"handoff","title":"Zbadaj E06–E08.","content_tex":"Porównaj xHPW i kolejność tasków."},{"id":"pass","title":"Zbadaj E09.","content_tex":"Sprawdź trzy stosy, markers i digest."}]},
|
||||||
{"kind":"exercise","id":"no-yield","title":"Ćwiczenie — brak yield request","prompt_tex":"W kontrolowanym wariancie pomiń portYIELD_FROM_ISR, zachowując GiveFromISR. Zmierz, kiedy waiter zacznie działać i wskaż następny legalny scheduling point.","evidence_tex":"Dwa timestampowane ślady E07/E08 z yield i bez yield oraz opis różnicy.","criterion":"Uczeń nie myli odblokowania taska z natychmiastowym wykonaniem i przywraca poprawny yield w wersji finalnej.","based_on":["contract","replay"]}
|
{"kind":"exercise","id":"no-yield","title":"Ćwiczenie — brak yield request","prompt_tex":"W kontrolowanym wariancie pomiń \\texttt{portYIELD\\_FROM\\_ISR}, zachowując GiveFromISR. Zmierz, kiedy waiter zacznie działać i wskaż następny legalny scheduling point.","evidence_tex":"Dwa timestampowane ślady E07/E08 z yield i bez yield oraz opis różnicy.","criterion":"Uczeń nie myli odblokowania taska z natychmiastowym wykonaniem i przywraca poprawny yield w wersji finalnej.","based_on":["contract","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
+128
-58
File diff suppressed because one or more lines are too long
Reference in New Issue
Block a user