feat: add lab-rv32i-freertos-kernel-facade card
This commit is contained in:
user
@@ -0,0 +1,62 @@
|
||||
# K09 — Scheduler facade and scoped kernel guards
|
||||
|
||||
## Position
|
||||
|
||||
- Series: FreeRTOS C++
|
||||
- Lesson: L08, card K09
|
||||
- Duration: 30 minutes
|
||||
- Platform: Hazard3 / RV32I, FreeRTOS V11.3.0
|
||||
- Evidence: kernel state, `xCriticalNesting`, `mstatus.MIE`, ELF assembly
|
||||
|
||||
## Outcome
|
||||
|
||||
After 30 minutes the student can distinguish scheduler suspension from a
|
||||
critical section, choose a static facade versus an RAII guard, and prove that
|
||||
three early-return paths restore the paired kernel state.
|
||||
|
||||
## Lesson plan
|
||||
|
||||
| Time | Mode | Evidence |
|
||||
| --- | --- | --- |
|
||||
| 0–5 | raw API | classify service calls and paired calls |
|
||||
| 5–10 | critical nesting | record 0→1→2→1→0 and MIE transitions |
|
||||
| 10–15 | critical guard | run three early returns; prove depth 0/MIE 1 |
|
||||
| 15–20 | scheduler guard | prove suspended state with interrupts enabled |
|
||||
| 20–25 | nesting/`this_task` | nested guards, current handle, tick and yield |
|
||||
| 25–30 | ABI and repair | no wrapper symbols; repair three-exit function |
|
||||
|
||||
## Canonical comparison
|
||||
|
||||
| Operation | Context switch | Interrupt MIE | Pair |
|
||||
| --- | --- | --- | --- |
|
||||
| `vTaskSuspendAll` | deferred | remains enabled | `xTaskResumeAll` |
|
||||
| `taskENTER_CRITICAL` | prevented | disabled | `taskEXIT_CRITICAL` |
|
||||
|
||||
Scheduler suspension can nest. The inner guard's destructor decreases the
|
||||
nesting level but the state remains suspended until the outer guard exits.
|
||||
Critical sections also nest; MIE is enabled only when depth returns to zero.
|
||||
|
||||
## Student repair
|
||||
|
||||
Start with a function containing a manual enter/suspend call and three returns.
|
||||
Replace only the pairing mechanism with the appropriate guard. Verify every
|
||||
path at the checkpoint rather than accepting source-level appearance as proof.
|
||||
|
||||
## Acceptance
|
||||
|
||||
- static facade is non-constructible;
|
||||
- both guards are non-copyable/non-movable and restore all three paths;
|
||||
- raw critical values are exactly 0/1/2/1/0 and MIE 1/0/0/0/1;
|
||||
- scheduler suspension leaves MIE enabled;
|
||||
- nested scheduler guard remains suspended after inner destruction;
|
||||
- `this_task::current()` equals the worker handle;
|
||||
- facade and guard calls are inline with no vtable, RTTI or hosted runtime;
|
||||
- target exits with PASS.
|
||||
|
||||
## Main traps
|
||||
|
||||
1. `Scheduler` is a facade, not a scoped owner.
|
||||
2. Scheduler suspension is not interrupt masking.
|
||||
3. Never block while the scheduler is suspended.
|
||||
4. A task-context critical guard is not an ISR-safe mutex.
|
||||
5. RAII balances control flow; it does not make an invalid operation valid.
|
||||
@@ -0,0 +1,344 @@
|
||||
% Generated from json/card_source.json by tools/render_card.py.
|
||||
% Do not edit manually; update the JSON and regenerate.
|
||||
|
||||
\documentclass[12pt,a4paper]{article}
|
||||
|
||||
\usepackage[T1]{fontenc}
|
||||
\usepackage{lmodern}
|
||||
\usepackage[utf8]{inputenc}
|
||||
\usepackage[polish]{babel}
|
||||
\usepackage{csquotes}
|
||||
\usepackage{amsmath}
|
||||
\usepackage{amssymb}
|
||||
\usepackage{xcolor}
|
||||
\usepackage[a4paper,left=2.15cm,right=2.15cm,top=0.5cm,bottom=0.5cm,headheight=24mm,headsep=3mm,includehead]{geometry}
|
||||
\usepackage{eso-pic}
|
||||
\usepackage{marginnote}
|
||||
\usepackage{array}
|
||||
\usepackage{tabularx}
|
||||
\usepackage{graphicx}
|
||||
\usepackage{pdflscape}
|
||||
\usepackage{float}
|
||||
\usepackage{silence}
|
||||
\WarningFilter{soulutf8}{This package is obsolete}
|
||||
\usepackage{pdfcomment}
|
||||
\usepackage{enumitem}
|
||||
\usepackage{needspace}
|
||||
\usepackage{fancyhdr}
|
||||
\usepackage{lastpage}
|
||||
\usepackage{microtype}
|
||||
\usepackage[most]{tcolorbox}
|
||||
\usepackage{qrcode}
|
||||
\IfFileExists{references.bib}{%
|
||||
\usepackage[backend=biber,style=numeric,sorting=none]{biblatex}%
|
||||
\addbibresource{references.bib}%
|
||||
}{}
|
||||
|
||||
\hypersetup{hidelinks}
|
||||
|
||||
\IfFileExists{build-meta.tex}{%
|
||||
\input{build-meta.tex}%
|
||||
}{%
|
||||
\newcommand{\BuildCommit}{lokalna}%
|
||||
}
|
||||
|
||||
\newcommand{\DocumentAuthor}{M. Pabiszczak}
|
||||
\newcommand{\DocumentYear}{2026}
|
||||
\newcommand{\CardSeries}{freertos-cpp}
|
||||
\newcommand{\CardNumber}{09}
|
||||
\newcommand{\CardCount}{16}
|
||||
\newcommand{\CardSlug}{kernel-facade}
|
||||
\newcommand{\CardVersion}{v00.01}
|
||||
\newcommand{\DocumentUUID}{6a2ab068-17e7-4bfa-b726-2df37787ed69}
|
||||
|
||||
\newcommand{\EmptyCheck}{\(\square\)}
|
||||
\newcommand{\EscAnswerLines}[1][3]{\par\noindent\dotfill\par\noindent\dotfill\par\noindent\dotfill}
|
||||
\newcommand{\EscWriteRow}[1][2.8em]{\rule{0pt}{#1}}
|
||||
\setlength{\parindent}{0pt}
|
||||
\setlength{\parskip}{0.45em}
|
||||
\setlength{\headheight}{24mm}
|
||||
\setlength{\headsep}{3mm}
|
||||
\setlength{\footskip}{8mm}
|
||||
\setlength{\marginparwidth}{1.5cm}
|
||||
\setlength{\marginparsep}{0.25cm}
|
||||
\renewcommand{\arraystretch}{1.22}
|
||||
% Margin separator lines disabled for layout trial.
|
||||
|
||||
\newcommand{\ESCPageResourceHeader}{%
|
||||
\begingroup%
|
||||
\setlength{\parskip}{0pt}%
|
||||
\setlength{\fboxsep}{0pt}%
|
||||
\setlength{\fboxrule}{0.35pt}%
|
||||
\setlength{\arrayrulewidth}{0.35pt}%
|
||||
\noindent\fbox{%
|
||||
\begin{minipage}[c][23.5mm][c]{\dimexpr\textwidth-2\fboxrule\relax}%
|
||||
\begin{minipage}[c][23mm][c]{\dimexpr\linewidth-24mm-0.35pt\relax}%
|
||||
\setlength{\tabcolsep}{0pt}%
|
||||
\renewcommand{\arraystretch}{0}%
|
||||
\begin{tabularx}{\linewidth}{@{}p{\dimexpr0.50000000\linewidth-\arrayrulewidth\relax}|p{\dimexpr0.15126050\linewidth-\arrayrulewidth\relax}|X@{}}%
|
||||
\parbox[c][5.19414mm][c]{\linewidth}{\hspace{0.45mm}{\fontsize{3.2}{3.4}\selectfont\ttfamily\bfseries TITLE}\par\nointerlineskip\vspace{0.12mm}\noindent\makebox[\linewidth][r]{{\fontsize{7.7}{7.9}\selectfont\ttfamily\bfseries Scheduler Facade and Scoped Kernel Guards}\hspace{0.45mm}}\par} & \parbox[c][5.19414mm][c]{\linewidth}{\hspace{0.45mm}{\fontsize{3.2}{3.4}\selectfont\ttfamily\bfseries VER.}\par\nointerlineskip\vspace{0.12mm}\noindent\makebox[\linewidth][r]{{\fontsize{6.6}{6.8}\selectfont\ttfamily\bfseries v00.01}\hspace{0.45mm}}\par} & \parbox[c][5.19414mm][c]{\linewidth}{\hspace{0.45mm}{\fontsize{3.2}{3.4}\selectfont\ttfamily\bfseries DATETIME}\par\nointerlineskip\vspace{0.12mm}\noindent\makebox[\linewidth][r]{{\fontsize{6.4}{6.6}\selectfont\ttfamily\bfseries 2026-07-19T00:00:00+02:00}\hspace{0.45mm}}\par} \\%
|
||||
\end{tabularx}%
|
||||
\par\nointerlineskip%
|
||||
\hrule height0.35pt%
|
||||
\nointerlineskip%
|
||||
\begin{tabularx}{\linewidth}{@{}p{\dimexpr0.50000000\linewidth-\arrayrulewidth\relax}|p{\dimexpr0.25210084\linewidth-\arrayrulewidth\relax}|p{\dimexpr0.14285714\linewidth-\arrayrulewidth\relax}|X@{}}%
|
||||
\parbox[c][5.19414mm][c]{\linewidth}{\hspace{0.45mm}{\fontsize{3.2}{3.4}\selectfont\ttfamily\bfseries PROJECT}\par\nointerlineskip\vspace{0.12mm}\noindent\makebox[\linewidth][r]{{\fontsize{7.7}{7.9}\selectfont\ttfamily\bfseries Freestanding C++ nad FreeRTOS}\hspace{0.45mm}}\par} & \parbox[c][5.19414mm][c]{\linewidth}{\hspace{0.45mm}{\fontsize{3.2}{3.4}\selectfont\ttfamily\bfseries SERIES}\par\nointerlineskip\vspace{0.12mm}\noindent\makebox[\linewidth][r]{{\fontsize{6.4}{6.6}\selectfont\ttfamily\bfseries FreeRTOS C++}\hspace{0.45mm}}\par} & \parbox[c][5.19414mm][c]{\linewidth}{\hspace{0.45mm}{\fontsize{3.2}{3.4}\selectfont\ttfamily\bfseries CARD}\par\nointerlineskip\vspace{0.12mm}\noindent\makebox[\linewidth][r]{{\fontsize{6.4}{6.6}\selectfont\ttfamily\bfseries 09/16}\hspace{0.45mm}}\par} & \parbox[c][5.19414mm][c]{\linewidth}{\hspace{0.45mm}{\fontsize{3.2}{3.4}\selectfont\ttfamily\bfseries SHEET}\par\nointerlineskip\vspace{0.12mm}\noindent\makebox[\linewidth][r]{{\fontsize{6.4}{6.6}\selectfont\ttfamily\bfseries \thepage/\pageref{LastPage}}\hspace{0.45mm}}\par} \\%
|
||||
\end{tabularx}%
|
||||
\par\nointerlineskip%
|
||||
\hrule height0.35pt%
|
||||
\nointerlineskip%
|
||||
\begin{tabularx}{\linewidth}{@{}p{\dimexpr0.05882353\linewidth-\arrayrulewidth\relax}|p{\dimexpr0.05042017\linewidth-\arrayrulewidth\relax}|p{\dimexpr0.14705882\linewidth-\arrayrulewidth\relax}|p{\dimexpr0.09243697\linewidth-\arrayrulewidth\relax}|p{\dimexpr0.07563025\linewidth-\arrayrulewidth\relax}|p{\dimexpr0.07563025\linewidth-\arrayrulewidth\relax}|X@{}}%
|
||||
\parbox[c][5.19414mm][c]{\linewidth}{\hspace{0.15mm}{\fontsize{2.85}{3}\selectfont\ttfamily\bfseries SUBJ.}\par\nointerlineskip\vspace{0.12mm}\noindent\makebox[\linewidth][r]{{\fontsize{4.45}{4.65}\selectfont\ttfamily\bfseries Inf.}\hspace{0.15mm}}\par} & \parbox[c][5.19414mm][c]{\linewidth}{\hspace{0.15mm}{\fontsize{2.85}{3}\selectfont\ttfamily\bfseries PROG.}\par\nointerlineskip\vspace{0.12mm}\noindent\makebox[\linewidth][r]{{\fontsize{4.45}{4.65}\selectfont\ttfamily\bfseries —}\hspace{0.15mm}}\par} & \parbox[c][5.19414mm][c]{\linewidth}{\hspace{0.15mm}{\fontsize{2.85}{3}\selectfont\ttfamily\bfseries CORE}\par\nointerlineskip\vspace{0.12mm}\noindent\makebox[\linewidth][r]{{\fontsize{4.45}{4.65}\selectfont\ttfamily\bfseries —}\hspace{0.15mm}}\par} & \parbox[c][5.19414mm][c]{\linewidth}{\hspace{0.15mm}{\fontsize{2.85}{3}\selectfont\ttfamily\bfseries SCOPE}\par\nointerlineskip\vspace{0.12mm}\noindent\makebox[\linewidth][r]{{\fontsize{4.45}{4.65}\selectfont\ttfamily\bfseries —}\hspace{0.15mm}}\par} & \parbox[c][5.19414mm][c]{\linewidth}{\hspace{0.15mm}{\fontsize{2.85}{3}\selectfont\ttfamily\bfseries LEVEL}\par\nointerlineskip\vspace{0.12mm}\noindent\makebox[\linewidth][r]{{\fontsize{4.45}{4.65}\selectfont\ttfamily\bfseries —}\hspace{0.15mm}}\par} & \parbox[c][5.19414mm][c]{\linewidth}{\hspace{0.15mm}{\fontsize{2.85}{3}\selectfont\ttfamily\bfseries POS.}\par\nointerlineskip\vspace{0.12mm}\noindent\makebox[\linewidth][r]{{\fontsize{4.45}{4.65}\selectfont\ttfamily\bfseries —}\hspace{0.15mm}}\par} & \parbox[c][5.19414mm][c]{\linewidth}{\hbox to\linewidth{\hspace{0.35mm}{\fontsize{3.4}{3.75}\selectfont\ttfamily\bfseries GITEA UUID}\hfill{\fontsize{3.4}{3.75}\selectfont\ttfamily 6a2ab068-17e7-4bfa-b726-2df37787ed69}\hspace{0.35mm}}\par\nointerlineskip\hbox to\linewidth{\hspace{0.35mm}{\fontsize{3.4}{3.75}\selectfont\ttfamily\bfseries CARD UUID} {\fontsize{3.4}{3.75}\selectfont\ttfamily 6a2ab068-17e7-4bfa-b726-2df37787ed69}\hfill{\fontsize{3.4}{3.75}\selectfont\ttfamily\bfseries AUTHOR M. Pabiszczak}\hspace{0.35mm}}} \\%
|
||||
\end{tabularx}%
|
||||
\par\nointerlineskip%
|
||||
\hrule height0.35pt%
|
||||
\nointerlineskip%
|
||||
\begin{tabularx}{\linewidth}{@{}X@{}}%
|
||||
\parbox[c][3.46276mm][c]{\linewidth}{\hspace{0.45mm}{\fontsize{4.5}{4.85}\selectfont\ttfamily\bfseries GITEA} {\fontsize{4.5}{4.85}\selectfont\ttfamily\href{https://zsl-gitea.mpabi.pl/edu-freertos-cpp/lab-rv32i-freertos-kernel-facade}{\nolinkurl{https://zsl-gitea.mpabi.pl/edu-freertos-cpp/lab-rv32i-freertos-kernel-facade}}}} \\%
|
||||
\end{tabularx}%
|
||||
\par\nointerlineskip%
|
||||
\hrule height0.35pt%
|
||||
\nointerlineskip%
|
||||
\begin{tabularx}{\linewidth}{@{}X@{}}%
|
||||
\parbox[c][3.46276mm][c]{\linewidth}{\hspace{0.45mm}{\fontsize{4.5}{4.85}\selectfont\ttfamily\bfseries HTML} {\fontsize{4.5}{4.85}\selectfont\ttfamily\href{}{\nolinkurl{}}}} \\%
|
||||
\end{tabularx}%
|
||||
\end{minipage}%
|
||||
\vrule width0.35pt%
|
||||
\begin{minipage}[c][23mm][c]{24mm}\centering%
|
||||
{\tiny QR wyłączony}%
|
||||
\end{minipage}%
|
||||
\end{minipage}%
|
||||
}%
|
||||
\endgroup%
|
||||
}
|
||||
|
||||
\pagestyle{fancy}
|
||||
\fancyhf{}
|
||||
\fancyhead[C]{\ESCPageResourceHeader}
|
||||
\renewcommand{\headrulewidth}{0pt}
|
||||
\renewcommand{\footrulewidth}{0pt}
|
||||
|
||||
\newcommand{\ESCMarginTag}[4]{%
|
||||
\hspace*{#1}\textcolor{#2}{#3~#4}%
|
||||
}
|
||||
\newcommand{\ESCSectionBlockStart}{%
|
||||
\Needspace{8\baselineskip}%
|
||||
\par\vspace{0.35em}%
|
||||
\noindent\textcolor{black!28}{\rule{\textwidth}{0.35pt}}%
|
||||
\par\vspace{0.15em}%
|
||||
}
|
||||
\newcommand{\ESCSectionBlockEnd}{%
|
||||
\par\vspace{0.25em}%
|
||||
\noindent\textcolor{black!18}{\rule{\textwidth}{0.25pt}}%
|
||||
\par\vspace{0.45em}%
|
||||
}
|
||||
\newcommand{\ESCTinyStepSeparator}{%
|
||||
\par\vspace{0.10em}%
|
||||
\noindent{\color{black!18}\leaders\hbox{\rule{0.60em}{0.22pt}\hspace{0.38em}}\hfill\kern0pt}%
|
||||
\par\vspace{0.10em}%
|
||||
}
|
||||
\newtcolorbox{ESCTaskFrame}[1]{enhanced,breakable,arc=0pt,boxrule=0.35pt,colback=white,colframe=black,boxsep=0pt,left=1.4mm,right=1.4mm,top=0.8mm,bottom=0.8mm,colbacktitle=black!7,coltitle=black,title={\ttfamily\bfseries TASK\quad #1}}
|
||||
\newtcolorbox{ESCBlockFrame}[1]{enhanced,breakable,arc=0pt,boxrule=0.35pt,colback=white,colframe=black!55,boxsep=0pt,left=1.0mm,right=1.0mm,top=0.6mm,bottom=0.6mm,colbacktitle=black!4,coltitle=black,title={\ttfamily\bfseries BLOCK\quad #1}}
|
||||
\newtcolorbox{ESCStepFrame}[1]{enhanced,breakable,arc=0pt,boxrule=0.35pt,colback=white,colframe=black!28,boxsep=0pt,left=0.8mm,right=0.8mm,top=0.45mm,bottom=0.45mm,colbacktitle=black!2,coltitle=black,title={\ttfamily STEP\quad #1}}
|
||||
\newtcolorbox{ESCConclusionFrame}{enhanced,breakable,arc=0pt,boxrule=0.45pt,colback=blue!2,colframe=blue!45!black,boxsep=0pt,left=1.2mm,right=1.2mm,top=0.7mm,bottom=0.7mm,colbacktitle=blue!7,coltitle=black,title={\ttfamily\bfseries WNIOSEK}}
|
||||
|
||||
\newcommand{\ESCLearningTreeWidget}{%
|
||||
\reversemarginpar
|
||||
\marginnote[%
|
||||
\begin{minipage}{\marginparwidth}%
|
||||
\raggedright
|
||||
{\fontsize{3.55}{3.95}\selectfont\ttfamily
|
||||
\begin{minipage}[t]{\marginparwidth}%
|
||||
\raggedright
|
||||
{\bfseries\textcolor{black!65}{TECH}\par}%
|
||||
\vspace{0.08em}%
|
||||
\hspace*{0.00em}\textcolor{red}{WE~01}\textcolor{black!48}{}\par%
|
||||
\hspace*{0.28em}\textcolor{orange!85!black}{EK~LOCAL~RTOS.KERNEL}\textcolor{black!48}{\pdftooltip[width=\textwidth]{.01}{Śledzi critical nesting, MIE, scheduler state i wynik inliningu.}}\par%
|
||||
\hspace*{0.54em}\textcolor{blue!70!black}{KW~LOCAL~RTOS.KERNEL}\textcolor{black!48}{\pdftooltip[width=\textwidth]{.01}{Pokazuje dokładne sekwencje, zachowanie IRQ podczas suspension oraz brak symboli wrappera.}}\par%
|
||||
\end{minipage}%
|
||||
}%
|
||||
\end{minipage}%
|
||||
]{}
|
||||
\normalmarginpar
|
||||
|
||||
\marginnote{%
|
||||
\begin{minipage}{\marginparwidth}%
|
||||
\raggedright
|
||||
{\fontsize{3.55}{3.95}\selectfont\ttfamily
|
||||
\hspace*{0.06cm}%
|
||||
\begin{minipage}[t]{\dimexpr\marginparwidth-0.06cm\relax}%
|
||||
\raggedright
|
||||
{\bfseries\textcolor{black!65}{OG}\par}%
|
||||
\vspace{0.08em}%
|
||||
\hspace*{0.00em}\textcolor{red}{WE~01}\textcolor{black!48}{}\par%
|
||||
\hspace*{0.28em}\textcolor{green!50!black}{EN~LOCAL~EN~OOP.RAII}\textcolor{black!48}{\pdftooltip[width=\textwidth]{.03}{Analizuje lifetime usługi, scope guarda i early-return control flow.}}\par%
|
||||
\hspace*{0.54em}\textcolor{blue!70!black}{KW~LOCAL~KW~OOP.RAII}\textcolor{black!48}{\pdftooltip[width=\textwidth]{.03}{Uzasadnia statyczny Scheduler i dokładnie jedno restore na każdej ścieżce.}}\par%
|
||||
\end{minipage}%
|
||||
}%
|
||||
\end{minipage}%
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
\begin{document}
|
||||
\sloppy
|
||||
|
||||
\vspace{1.0em}
|
||||
\noindent{\Large\bfseries Cel karty}\par
|
||||
\vspace{0.35em}
|
||||
Uczeń rozdziela bezstanową usługę Scheduler od parowanych operacji, mierzy critical nesting i mstatus.MIE oraz dowodzi odtworzenia stanu na trzech wczesnych wyjściach.
|
||||
|
||||
\vspace{0.8em}
|
||||
\noindent\textcolor{black!25}{\rule{\textwidth}{0.35pt}}
|
||||
\vspace{0.7em}
|
||||
\noindent{\Large\bfseries Zakres karty}\par
|
||||
\vspace{0.35em}
|
||||
Scheduler suspension nie maskuje przerwań i nie dopuszcza blokujących API. CriticalSection działa w task context, nie jest mutexem ani guardem ISR.
|
||||
|
||||
\vspace{0.8em}
|
||||
\noindent\textcolor{black!25}{\rule{\textwidth}{0.35pt}}
|
||||
|
||||
\clearpage
|
||||
|
||||
\ESCSectionBlockStart
|
||||
\section{Usługa kontra para}
|
||||
\reversemarginpar
|
||||
\marginnote[%
|
||||
\begin{minipage}{\marginparwidth}%
|
||||
\raggedright
|
||||
{\fontsize{3.55}{3.95}\selectfont\ttfamily
|
||||
\begin{minipage}[t]{\marginparwidth}%
|
||||
\raggedright
|
||||
{\bfseries\textcolor{black!65}{TECH}\par}%
|
||||
\vspace{0.08em}%
|
||||
\hspace*{0.00em}\textcolor{red}{WE~01}\textcolor{black!48}{}\par%
|
||||
\end{minipage}%
|
||||
}%
|
||||
\end{minipage}%
|
||||
]{}[-3.1em]
|
||||
\normalmarginpar
|
||||
|
||||
\marginnote{%
|
||||
\begin{minipage}{\marginparwidth}%
|
||||
\raggedright
|
||||
{\fontsize{3.55}{3.95}\selectfont\ttfamily
|
||||
\hspace*{0.06cm}%
|
||||
\begin{minipage}[t]{\dimexpr\marginparwidth-0.06cm\relax}%
|
||||
\raggedright
|
||||
{\bfseries\textcolor{black!65}{OG}\par}%
|
||||
\vspace{0.08em}%
|
||||
\hspace*{0.00em}\textcolor{red}{WE~01}\textcolor{black!48}{}\par%
|
||||
\end{minipage}%
|
||||
}%
|
||||
\end{minipage}%
|
||||
}[-3.1em]
|
||||
|
||||
|
||||
\begingroup
|
||||
\scriptsize\ttfamily\color{black!60}\sloppy
|
||||
\noindent drzewka: \pdftooltip[width=\textwidth]{D1}{K09.WE01.OG.LOCAL.OOP.RAII.03 | WE 01: Kernel facade i guards. Zaprojektowanie cienkiej\textCR fasady kernela i scope-bound par z dowodem odtworzenia stanu. | EN LOCAL OOP.RAII.03:\textCR Analizuje lifetime usługi, scope guarda i early-return control flow. | KW LOCAL OOP.RAII.03:\textCR Uzasadnia statyczny Scheduler i dokładnie jedno restore na każdej ścieżce.}\par
|
||||
\vspace{0.10em}%
|
||||
\noindent K1: Uzasadnij brak konstruktora i destruktora Scheduler.\quad D1\par
|
||||
\ESCTinyStepSeparator
|
||||
\noindent K2: Napraw trzy early returns jednym guardem.\quad D1\par
|
||||
\par\vspace{0.18em}%
|
||||
\endgroup
|
||||
|
||||
Sklasyfikuj Scheduler start/state jako statyczną fasadę, a enter/exit i suspend/resume jako zakresowe pary.
|
||||
\ESCSectionBlockEnd
|
||||
|
||||
\ESCSectionBlockStart
|
||||
\section{Critical nesting i mstatus.MIE}
|
||||
\reversemarginpar
|
||||
\marginnote[%
|
||||
\begin{minipage}{\marginparwidth}%
|
||||
\raggedright
|
||||
{\fontsize{3.55}{3.95}\selectfont\ttfamily
|
||||
\begin{minipage}[t]{\marginparwidth}%
|
||||
\raggedright
|
||||
{\bfseries\textcolor{black!65}{TECH}\par}%
|
||||
\vspace{0.08em}%
|
||||
\hspace*{0.00em}\textcolor{red}{WE~01}\textcolor{black!48}{}\par%
|
||||
\end{minipage}%
|
||||
}%
|
||||
\end{minipage}%
|
||||
]{}[-3.1em]
|
||||
\normalmarginpar
|
||||
|
||||
\marginnote{%
|
||||
\begin{minipage}{\marginparwidth}%
|
||||
\raggedright
|
||||
{\fontsize{3.55}{3.95}\selectfont\ttfamily
|
||||
\hspace*{0.06cm}%
|
||||
\begin{minipage}[t]{\dimexpr\marginparwidth-0.06cm\relax}%
|
||||
\raggedright
|
||||
{\bfseries\textcolor{black!65}{OG}\par}%
|
||||
\vspace{0.08em}%
|
||||
\hspace*{0.00em}\textcolor{red}{WE~01}\textcolor{black!48}{}\par%
|
||||
\end{minipage}%
|
||||
}%
|
||||
\end{minipage}%
|
||||
}[-3.1em]
|
||||
|
||||
|
||||
\begingroup
|
||||
\scriptsize\ttfamily\color{black!60}\sloppy
|
||||
\noindent drzewka: \pdftooltip[width=\textwidth]{D1}{K09.WE01.TECH.LOCAL.RTOS.KERNEL.01 | WE 01: Kernel facade i guards. Zaprojektowanie cienkiej\textCR fasady kernela i scope-bound par z dowodem odtworzenia stanu. | EK LOCAL RTOS.KERNEL.01:\textCR Śledzi critical nesting, MIE, scheduler state i wynik inliningu. | KW LOCAL RTOS.KERNEL.01:\textCR Pokazuje dokładne sekwencje, zachowanie IRQ podczas suspension oraz brak symboli wrappera.}\par
|
||||
\vspace{0.10em}%
|
||||
\noindent K1: Odtwórz 0-1-2-1-0 oraz 1-0-0-0-1.\quad D1\par
|
||||
\ESCTinyStepSeparator
|
||||
\noindent K2: Potwierdź depth 0 i MIE 1 po każdej ścieżce.\quad D1\par
|
||||
\par\vspace{0.18em}%
|
||||
\endgroup
|
||||
|
||||
Wykonaj raw enter/enter/exit/exit, a potem ten sam kontrakt przez CriticalSection. Zapisz depth i MIE na każdym checkpoint.
|
||||
\ESCSectionBlockEnd
|
||||
|
||||
\ESCSectionBlockStart
|
||||
\section{Scheduler suspension i this\_task}
|
||||
\reversemarginpar
|
||||
\marginnote[%
|
||||
\begin{minipage}{\marginparwidth}%
|
||||
\raggedright
|
||||
{\fontsize{3.55}{3.95}\selectfont\ttfamily
|
||||
\begin{minipage}[t]{\marginparwidth}%
|
||||
\raggedright
|
||||
{\bfseries\textcolor{black!65}{TECH}\par}%
|
||||
\vspace{0.08em}%
|
||||
\hspace*{0.00em}\textcolor{red}{WE~01}\textcolor{black!48}{}\par%
|
||||
\end{minipage}%
|
||||
}%
|
||||
\end{minipage}%
|
||||
]{}[-3.1em]
|
||||
\normalmarginpar
|
||||
|
||||
\marginnote{%
|
||||
\begin{minipage}{\marginparwidth}%
|
||||
\raggedright
|
||||
{\fontsize{3.55}{3.95}\selectfont\ttfamily
|
||||
\hspace*{0.06cm}%
|
||||
\begin{minipage}[t]{\dimexpr\marginparwidth-0.06cm\relax}%
|
||||
\raggedright
|
||||
{\bfseries\textcolor{black!65}{OG}\par}%
|
||||
\vspace{0.08em}%
|
||||
\hspace*{0.00em}\textcolor{red}{WE~01}\textcolor{black!48}{}\par%
|
||||
\end{minipage}%
|
||||
}%
|
||||
\end{minipage}%
|
||||
}[-3.1em]
|
||||
|
||||
|
||||
\begingroup
|
||||
\scriptsize\ttfamily\color{black!60}\sloppy
|
||||
\noindent drzewka: \pdftooltip[width=\textwidth]{D1}{K09.WE01.TECH.LOCAL.RTOS.KERNEL.01 | WE 01: Kernel facade i guards. Zaprojektowanie cienkiej\textCR fasady kernela i scope-bound par z dowodem odtworzenia stanu. | EK LOCAL RTOS.KERNEL.01:\textCR Śledzi critical nesting, MIE, scheduler state i wynik inliningu. | KW LOCAL RTOS.KERNEL.01:\textCR Pokazuje dokładne sekwencje, zachowanie IRQ podczas suspension oraz brak symboli wrappera.}\par
|
||||
\vspace{0.10em}%
|
||||
\noindent K1: Pokaż MIE=1 podczas suspension i outer/inner nesting.\quad D1\par
|
||||
\ESCTinyStepSeparator
|
||||
\noindent K2: Porównaj this\_task handle i sprawdź inline w ELF.\quad D1\par
|
||||
\par\vspace{0.18em}%
|
||||
\endgroup
|
||||
|
||||
Zmierz running-suspended-running przy stale włączonym MIE, przetestuj nesting i zidentyfikuj bieżący handle, tick oraz yield.
|
||||
\ESCSectionBlockEnd
|
||||
|
||||
\end{document}
|
||||
+237
@@ -0,0 +1,237 @@
|
||||
\documentclass[10pt]{article}
|
||||
\usepackage[T1]{fontenc}\usepackage[utf8]{inputenc}\usepackage[polish]{babel}
|
||||
\usepackage[a4paper,margin=1.55cm]{geometry}
|
||||
\usepackage{array,tabularx,booktabs,amsmath,amssymb,xcolor,listings,hyperref,fancyhdr,lastpage,enumitem}
|
||||
\definecolor{accent}{HTML}{16324A}\definecolor{accentlight}{HTML}{EEF3F7}\definecolor{rulegray}{HTML}{D7DEE5}
|
||||
\hypersetup{colorlinks=true,linkcolor=accent,urlcolor=blue}
|
||||
\IfFileExists{build-meta.tex}{\input{build-meta.tex}}{\newcommand{\BuildCommit}{local}}
|
||||
\newcommand{\PublisherDomain}{mpabi}
|
||||
\newcommand{\CardArea}{inf}
|
||||
\newcommand{\CardSeries}{freertos-cpp}
|
||||
\newcommand{\CardNumber}{09}
|
||||
\newcommand{\CardCount}{16}
|
||||
\newcommand{\CardSlug}{kernel-facade}
|
||||
\newcommand{\CardVersion}{v00.01}
|
||||
\newcommand{\DocumentUUID}{6a2ab068-17e7-4bfa-b726-2df37787ed69}
|
||||
\newcommand{\blank}[1]{\rule{#1}{.2pt}}
|
||||
\lstset{language=C++,basicstyle=\ttfamily\scriptsize,columns=fullflexible,keepspaces=true,frame=single,breaklines=true,showstringspaces=false,numbers=none,backgroundcolor=\color{accentlight},rulecolor=\color{rulegray}}
|
||||
\pagestyle{fancy}\fancyhf{}
|
||||
\lhead{\textbf{K09 · FreeRTOS C++ · kernel facade}}\rhead{\small L08 · paired kernel state}
|
||||
\lfoot{\scriptsize commit \BuildCommit}\cfoot{\scriptsize \thepage/\pageref{LastPage}}\rfoot{\scriptsize V11.3.0 / \CardVersion}
|
||||
\setlength{\headheight}{14pt}\setlength{\footskip}{19pt}
|
||||
\setlist[itemize]{nosep,leftmargin=1.45em}\setlist[enumerate]{nosep,leftmargin=1.65em}
|
||||
\begin{document}\sloppy
|
||||
\begin{center}
|
||||
{\LARGE\bfseries Scheduler facade i scoped guards}\par
|
||||
\vspace{.25em}{\large statyczna usługa; RAII tylko dla prawdziwych par}\par
|
||||
\end{center}
|
||||
\noindent\begin{tabularx}{\textwidth}{@{}p{1.65cm}Xp{1.55cm}X@{}}
|
||||
\toprule
|
||||
Karta & K09 / \CardCount & Czas & 30 minut \\
|
||||
Platforma & Hazard3 / RV32I & Język & freestanding C++17 \\
|
||||
Dowód & nesting + \texttt{mstatus.MIE} & API & task context \\
|
||||
Wersja & \CardVersion & UUID karty & \texttt{6a2ab068-...} \\
|
||||
\bottomrule
|
||||
\end{tabularx}
|
||||
|
||||
\section*{Najpierw klasyfikacja lifetime}
|
||||
\begin{center}
|
||||
\texttt{Scheduler::start/state} $\rightarrow$ usługa procesu, brak scoped lifetime\\[.35em]
|
||||
\texttt{enter/exit}, \texttt{suspend/resume} $\rightarrow$ pary, więc guard RAII
|
||||
\end{center}
|
||||
|
||||
\noindent\fcolorbox{accent}{accentlight}{\begin{minipage}{.94\textwidth}
|
||||
\textbf{Kontrakt K09.} Destruktor guarda ma odtworzyć stan również przy każdym
|
||||
\texttt{return}. Nie wolno jednak blokować przy zawieszonym schedulerze, a
|
||||
\texttt{CriticalSection} nie jest mutexem ani API dla ISR.
|
||||
\end{minipage}}
|
||||
|
||||
\section*{Plan 30 minut}
|
||||
\noindent\begin{tabularx}{\textwidth}{@{}p{1.35cm}p{3.15cm}X@{}}
|
||||
\toprule
|
||||
Czas & Tryb & Dowód \\
|
||||
\midrule
|
||||
0--5 & raw API & rozdziel usługi od par \\
|
||||
5--10 & critical & nesting oraz MIE przed/wewnątrz/po \\
|
||||
10--15 & guard & trzy wczesne wyjścia wracają do stanu bazowego \\
|
||||
15--20 & suspend & scheduler suspended, lecz MIE pozostaje 1 \\
|
||||
20--25 & nesting & inner exit nie wznawia jeszcze outer suspension \\
|
||||
25--30 & ABI & inline do raw API; brak vtable/runtime \\
|
||||
\bottomrule
|
||||
\end{tabularx}
|
||||
|
||||
\section*{Dwie różne blokady}
|
||||
\noindent\begin{tabularx}{\textwidth}{@{}p{4.1cm}p{3.3cm}p{3.2cm}X@{}}
|
||||
\toprule
|
||||
Operacja & Context switch & Przerwania & Para \\
|
||||
\midrule
|
||||
\texttt{vTaskSuspendAll} & odroczony & działają & \texttt{xTaskResumeAll} \\
|
||||
\texttt{taskENTER\_CRITICAL} & niemożliwy & MIE=0 & \texttt{taskEXIT\_CRITICAL} \\
|
||||
\bottomrule
|
||||
\end{tabularx}
|
||||
|
||||
Predykcja MIE podczas suspension: \blank{2cm}. Predykcja critical depth po
|
||||
dwóch enter i jednym exit: \blank{2cm}.
|
||||
|
||||
\newpage
|
||||
\section{Raw critical: zmierz dokładną sekwencję}
|
||||
|
||||
\begin{lstlisting}
|
||||
taskENTER_CRITICAL(); // depth + 1, MIE=0
|
||||
taskENTER_CRITICAL(); // depth + 1, MIE=0
|
||||
taskEXIT_CRITICAL(); // depth - 1, nadal MIE=0
|
||||
taskEXIT_CRITICAL(); // depth == 0, MIE=1
|
||||
\end{lstlisting}
|
||||
|
||||
\noindent\begin{tabularx}{\textwidth}{@{}p{2.0cm}p{3.0cm}p{2.5cm}X@{}}
|
||||
\toprule
|
||||
Checkpoint & Operacja & Predykcja depth/MIE & Odczyt depth/MIE \\
|
||||
\midrule
|
||||
C0 & przed & 0 / 1 & \blank{2.5cm} \\
|
||||
C1 & enter & 1 / 0 & \blank{2.5cm} \\
|
||||
C2 & drugi enter & 2 / 0 & \blank{2.5cm} \\
|
||||
C3 & pierwszy exit & 1 / 0 & \blank{2.5cm} \\
|
||||
C4 & drugi exit & 0 / 1 & \blank{2.5cm} \\
|
||||
\bottomrule
|
||||
\end{tabularx}
|
||||
|
||||
\section{RAII zamienia trzy krawędzie w jedną parę}
|
||||
\begin{lstlisting}
|
||||
uint32_t repair(uint32_t path) {
|
||||
freertos::CriticalSection guard;
|
||||
if (path == 0) return 0x10;
|
||||
if (path == 1) return 0x20;
|
||||
return 0x30;
|
||||
} // destructor runs on every return
|
||||
\end{lstlisting}
|
||||
|
||||
\noindent\begin{tabularx}{\textwidth}{@{}p{1.5cm}p{2.6cm}p{2.7cm}p{2.5cm}X@{}}
|
||||
\toprule
|
||||
Path & Wynik & inside depth/MIE & after depth/MIE & PASS \\
|
||||
\midrule
|
||||
0 & \texttt{0x10} & \blank{2cm} & \blank{2cm} & $\square$ \\
|
||||
1 & \texttt{0x20} & \blank{2cm} & \blank{2cm} & $\square$ \\
|
||||
2 & \texttt{0x30} & \blank{2cm} & \blank{2cm} & $\square$ \\
|
||||
\bottomrule
|
||||
\end{tabularx}
|
||||
|
||||
\section*{Co dokładnie gwarantuje guard?}
|
||||
\begin{itemize}
|
||||
\item paruje wywołania w normalnym przepływie i przy wcześniejszym return;
|
||||
\item nie jest kopiowalny ani przenoszalny, więc nie powiela exit;
|
||||
\item zachowuje zagnieżdżenie: inner exit nie kończy outer critical section.
|
||||
\end{itemize}
|
||||
|
||||
Czy RAII pozwala wywołać blokujące API wewnątrz critical section?
|
||||
\blank{2cm}. Uzasadnienie:\\[.5em]\blank{16cm}
|
||||
|
||||
\newpage
|
||||
\section{SchedulerSuspendGuard: context switch bez maskowania IRQ}
|
||||
|
||||
\begin{lstlisting}
|
||||
{
|
||||
freertos::SchedulerSuspendGuard guard;
|
||||
// scheduler state == suspended; mstatus.MIE == 1
|
||||
// no delay, queue wait, semaphore wait or other blocking API
|
||||
} // xTaskResumeAll exactly once
|
||||
\end{lstlisting}
|
||||
|
||||
\noindent\begin{tabularx}{\textwidth}{@{}p{2cm}p{3.3cm}p{3.1cm}X@{}}
|
||||
\toprule
|
||||
Path & Inside state/MIE & After state/MIE & Wynik \\
|
||||
\midrule
|
||||
0 & suspended / \blank{1cm} & running / \blank{1cm} & \texttt{0x40} \\
|
||||
1 & suspended / \blank{1cm} & running / \blank{1cm} & \texttt{0x50} \\
|
||||
2 & suspended / \blank{1cm} & running / \blank{1cm} & \texttt{0x60} \\
|
||||
\bottomrule
|
||||
\end{tabularx}
|
||||
|
||||
\section*{Zagnieżdżenie}
|
||||
\begin{center}
|
||||
\texttt{running}\\
|
||||
$\downarrow$ outer ctor: \texttt{suspended}\\
|
||||
$\downarrow$ inner ctor: \texttt{suspended}\\
|
||||
$\downarrow$ inner dtor: \texttt{suspended}\\
|
||||
$\downarrow$ outer dtor: \texttt{running}
|
||||
\end{center}
|
||||
|
||||
Dlaczego inner destructor nie może jeszcze zwrócić stanu running?\\[.5em]
|
||||
\blank{16cm}
|
||||
|
||||
\section{Statyczna fasada i bieżący task}
|
||||
\begin{lstlisting}
|
||||
freertos::Scheduler::start();
|
||||
auto state = freertos::Scheduler::state();
|
||||
auto handle = freertos::this_task::current();
|
||||
auto tick = freertos::this_task::tick_count();
|
||||
freertos::this_task::yield();
|
||||
\end{lstlisting}
|
||||
|
||||
\noindent\begin{tabularx}{\textwidth}{@{}p{5cm}p{4cm}X@{}}
|
||||
\toprule
|
||||
Relacja & Predykcja & Odczyt \\
|
||||
\midrule
|
||||
state przed start & not started & \blank{2.5cm} \\
|
||||
state w workerze & running & \blank{2.5cm} \\
|
||||
this task handle & worker handle & \blank{2.5cm} \\
|
||||
tick after yield & $\geq$ tick before & \blank{2.5cm} \\
|
||||
\bottomrule
|
||||
\end{tabularx}
|
||||
|
||||
\section*{Granice}
|
||||
Suspension nie wyłącza ISR; tylko odracza przełączenie taska. Critical section
|
||||
maskuje przerwania i musi być krótka. Żaden z guardów nie jest zamiennikiem
|
||||
mutexa chroniącego zasób przez długą operację.
|
||||
|
||||
\newpage
|
||||
\section{Hazard3/GDB i ABI}
|
||||
\begin{lstlisting}[language=bash]
|
||||
make check
|
||||
riscv64-unknown-elf-gdb build/task01_kernel_facade/prog.elf
|
||||
b kernel_facade_debug_checkpoint
|
||||
\end{lstlisting}
|
||||
\begin{lstlisting}
|
||||
p g_raw_critical_depth
|
||||
p g_raw_critical_mie
|
||||
p g_guard_critical_after_depth
|
||||
p g_guard_critical_after_mie
|
||||
p g_raw_scheduler_state
|
||||
p g_guard_scheduler_after_state
|
||||
p g_nested_scheduler_state
|
||||
p g_this_task_handle
|
||||
p g_worker_handle
|
||||
p g_kernel_facade_pass
|
||||
\end{lstlisting}
|
||||
|
||||
\section*{Co ma zostać w assembly?}
|
||||
\noindent\begin{tabularx}{\textwidth}{@{}p{5.3cm}p{3.3cm}X@{}}
|
||||
\toprule
|
||||
Dowód & Oczekiwane & Odczyt \\
|
||||
\midrule
|
||||
disable IRQ & \texttt{csrci mstatus,8} & \blank{2.5cm} \\
|
||||
enable IRQ & \texttt{csrsi mstatus,8} & \blank{2.5cm} \\
|
||||
symbole wrappera & brak & \blank{2.5cm} \\
|
||||
vtable/RTTI/exception runtime & brak & \blank{2.5cm} \\
|
||||
\bottomrule
|
||||
\end{tabularx}
|
||||
|
||||
\section*{Zaliczenie}
|
||||
\begin{itemize}
|
||||
\item $\square$ rozdzielam statyczną fasadę od scoped ownera;
|
||||
\item $\square$ odtwarzam critical depth 0--1--2--1--0 i MIE 1--0--0--0--1;
|
||||
\item $\square$ pokazuję restore po trzech wczesnych return;
|
||||
\item $\square$ pokazuję, że suspension zachowuje MIE=1;
|
||||
\item $\square$ wyjaśniam nesting outer/inner i zakaz blokowania;
|
||||
\item $\square$ dowodzę inline facade/guards oraz końcowy PASS.
|
||||
\end{itemize}
|
||||
|
||||
\section*{Wyjście}
|
||||
Kiedy wybrać \texttt{CriticalSection}, a kiedy \texttt{SchedulerSuspendGuard}?\\[.5em]
|
||||
\blank{16cm}\\[1em]
|
||||
Dlaczego \texttt{Scheduler} nie jest obiektem RAII?\\[.5em]
|
||||
\blank{16cm}
|
||||
|
||||
\vfill
|
||||
\noindent\textbf{Następna karta K10:} typed \texttt{Queue<T>} i
|
||||
\texttt{StaticQueue<T,N>} z jawnym kontraktem copyable message type.
|
||||
\end{document}
|
||||
BIN
Binary file not shown.
Reference in New Issue
Block a user