Compare commits
3 Commits
55fa76a272
...
18448b481e
| Author | SHA1 | Date | |
|---|---|---|---|
|
|
18448b481e | ||
|
|
94b22408e5 | ||
|
|
8f51a7eed6 |
@@ -6,7 +6,7 @@
|
||||
"containerEnv": { //Add your build arguments here
|
||||
"DEBIAN_FRONTEND": "noninteractive"
|
||||
},
|
||||
"runArgs": ["--net=host"], //Add you docker run arguments here
|
||||
// "runArgs": ["--net=host"], //Add you docker run arguments here
|
||||
"updateContentCommand": ".devcontainer/install-tools.sh", //Path to the installation script run inside the DevContainer
|
||||
// "customizations": {
|
||||
// //Add your customizations here
|
||||
|
||||
@@ -8,66 +8,76 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
|
||||
Equivalently, there exists a time after which every $\PROVE(r)$ is invalid in $H$.
|
||||
\end{definition}
|
||||
|
||||
\subsubsection{Variables}
|
||||
Each process $p_i$ maintains:
|
||||
|
||||
\LinesNotNumbered
|
||||
\begin{algorithm}
|
||||
$\received \gets \emptyset$\; %\Comment{Messages received via \RB but not yet delivered}
|
||||
$\delivered \gets \emptyset$\; %\Comment{Messages already delivered}
|
||||
$\prop[r][j] \gets \bot,\ \forall r,j$\; %\Comment{Proposal from process $j$ for round $r$}
|
||||
$\current \gets 0$\;
|
||||
\end{algorithm}
|
||||
|
||||
% \paragraph{DenyList.} The \DL is initialized empty. We assume $\Pi_M = \Pi_V = \Pi$ (all processes can invoke \APPEND and \PROVE).
|
||||
|
||||
\subsubsection{Handlers and Procedures}
|
||||
|
||||
\LinesNumbered
|
||||
\begin{algorithm}[H]
|
||||
\caption{ARB at process $p_i$}\label{alg:arb-crash}
|
||||
% \SetAlgoLined
|
||||
|
||||
\SetKwBlock{LocalVars}{Local Variables:}{}
|
||||
\LocalVars{
|
||||
$\mathit{unordered} \gets \emptyset$,
|
||||
$\mathit{ordered} \gets \epsilon$,
|
||||
$\mathit{delivered} \gets \epsilon$\;
|
||||
$\mathit{prop}[r][j] \gets \bot,\ \forall r,j$\;
|
||||
\caption{\RB handler (at process $p_i$)}\label{alg:rb-handler}
|
||||
\Fn{RBreceived($S, r, j$)}{
|
||||
$\received \leftarrow \received \cup \{S\}$\;\nllabel{code:receivedConstruction}
|
||||
$\prop[r][j] \leftarrow S$\;\nllabel{code:prop-set} % \Comment{Record sender $j$'s proposal $S$ for round $r$}
|
||||
}
|
||||
|
||||
\vspace{0.3em}
|
||||
|
||||
\For{$r = 1, 2, \ldots$}{
|
||||
\textbf{wait until} $\mathit{unordered} \setminus \mathit{ordered} \neq \emptyset$\;
|
||||
$S \leftarrow (\mathit{unordered} \setminus \mathit{ordered})$\;\nllabel{code:Sconstruction}
|
||||
$\RBcast(S, r, i)$; $\PROVE(r)$; $\APPEND(r)$\;\nllabel{code:submit-proposition}
|
||||
|
||||
$\mathit{winners}_r \gets \{(j,r): (j,r) \in \READ()\}$\;
|
||||
\textbf{wait until} $\mathit{winners}_r \neq \emptyset$\;\nllabel{code:check-if-winners}
|
||||
|
||||
$\APPEND(r)$\;\nllabel{code:append-read}
|
||||
$W_r \gets \{ j : (j, r) \in \READ() \}$\;\nllabel{code:Wcompute}
|
||||
|
||||
\textbf{wait until} $\forall j \in W_r,\ \mathit{prop}[r][j] \neq \bot$\;\nllabel{code:check-winners-ack}
|
||||
|
||||
$M_r \gets \bigcup_{j \in W_r} \mathit{prop}[r][j]$\;\nllabel{code:Mcompute}
|
||||
$\mathit{ordered} \leftarrow \mathit{ordered} \cdot \ordered(M_r)$\;\nllabel{code:next-msg-extraction}
|
||||
}
|
||||
|
||||
\vspace{0.3em}
|
||||
|
||||
\Upon{$\ABbroadcast(m)$}{
|
||||
$\mathit{unordered} \gets \mathit{unordered} \cup \{m\}$\;
|
||||
}
|
||||
|
||||
\vspace{0.3em}
|
||||
|
||||
\Upon{$\textsf{rdeliver}(S, r, j)$ from process $p_j$}{
|
||||
$\mathit{unordered} \leftarrow \mathit{unordered} \cup \{S\}$\;\nllabel{code:receivedConstruction}
|
||||
$\mathit{prop}[r][j] \leftarrow S$\;\nllabel{code:prop-set}
|
||||
}
|
||||
|
||||
\vspace{0.3em}
|
||||
|
||||
\Upon{$\ABdeliver()$}{
|
||||
\If{$\mathit{ordered} \setminus \mathit{delivered} = \emptyset$}{
|
||||
\Return{$\bot$}
|
||||
}
|
||||
$m \gets (\mathit{ordered} \setminus \mathit{delivered})[0]$\;\nllabel{code:adeliver-extract}
|
||||
$\mathit{delivered} \gets \mathit{delivered} \cdot m$\;
|
||||
\Return{$m$}
|
||||
}
|
||||
|
||||
\end{algorithm}
|
||||
|
||||
% \paragraph{} An \ABbroadcast$(m)$ chooses the next open round from the \DL view, proposes all pending messages together with the new $m$, disseminates this proposal via \RB, then executes $\PROVE(r)$ followed by $\APPEND(r)$ to freeze the winners of the round. The loop polls \DL until (i) some winner’s proposal includes $m$ in a \emph{closed} round and (ii) all winners' proposals for closed rounds are known locally, ensuring eventual inclusion and delivery.
|
||||
|
||||
\begin{algorithm}[H]\label{alg:ABroadcast}
|
||||
\caption{\ABbroadcast$(m)$ (at process $p_i$)}\label{alg:ab-bcast}
|
||||
\Fn{ABbroadcast($m$)}{
|
||||
$P \leftarrow \READ()$\;\nllabel{code:set-up-read} %\Comment{Fetch latest \DL state to learn recent $\PROVE$ operations}
|
||||
$r_{max} \leftarrow \max(\{ r' : \exists j,\ (j,r') \in P \})$\;\nllabel{code:rmax-compute} %\Comment{Pick current open round}
|
||||
$S \leftarrow (\received \setminus \delivered) \cup \{m\}$\;\nllabel{code:Sconstruction}
|
||||
%\Comment{Propose all pending messages plus the new $m$}
|
||||
|
||||
\vspace{1em}
|
||||
|
||||
$r \gets r_{max} - 1$\;
|
||||
\While{$((i, r) \not\in P\ \wedge (\nexists j, r': (j, r') \in P \wedge m \in \prop[r'][j]))$}{\nllabel{code:sumbited-check-loop}
|
||||
$r \gets r + 1$\;\nllabel{code:round-increment}
|
||||
$\RBcast(S, r, i)$; $\PROVE(r)$; $\APPEND(r)$;\;\nllabel{code:submit-proposition}
|
||||
$P \leftarrow \READ()$\; % \Comment{Refresh local view of \DL}
|
||||
}
|
||||
}
|
||||
\end{algorithm}
|
||||
|
||||
\begin{algorithm}[H]\label{alg:ADeliver}
|
||||
\caption{\ABdeliver() at process $p_i$}\label{alg:delivery}
|
||||
\Fn{ABdeliver($\bot$)}{
|
||||
$r \gets \current$\;
|
||||
$P_r \gets \{(j,r): (j,r) \in \READ()\}$ \;
|
||||
\If{$P_r = \emptyset$}{\nllabel{code:check-if-winners}
|
||||
\Return{$\bot$}
|
||||
}
|
||||
$\APPEND(r)$; $P \gets \READ()$\; \nllabel{code:append-read}
|
||||
$W_r \gets \{ j : (j, \PROVEtrace(r)) \in P \}$\;\nllabel{code:Wcompute}
|
||||
\If{$\exists j \in W_r,\ \prop[r][j] = \bot$}{ \nllabel{code:check-winners-ack}
|
||||
\Return{$\bot$}
|
||||
}
|
||||
$M_r \gets \bigcup_{j \in W_r} \prop[r][j]$\;\nllabel{code:Mcompute}
|
||||
$m \gets \ordered(M_r \setminus \delivered)[0]$\;\nllabel{code:next-msg-extraction}
|
||||
%\Comment{Set $m$ as the smaller message not already delivered}
|
||||
$\delivered \leftarrow \delivered \cup \{m\}$\;
|
||||
\If{$M_r \setminus \delivered = \emptyset$}{ %\Comment{Check if all messages from round $r$ have been delivered}
|
||||
$\current \leftarrow \current + 1$
|
||||
}
|
||||
\Return{$m$}
|
||||
}
|
||||
\end{algorithm}
|
||||
|
||||
% ------------------------------------------------------------------------------
|
||||
\subsection{Correctness}
|
||||
|
||||
\begin{definition}[First APPEND]\label{def:first-append}
|
||||
@@ -103,7 +113,7 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
|
||||
There are two possibilities for where $\APPEND^{(\star)}(r+1)$ is invoked.
|
||||
|
||||
\begin{itemize}
|
||||
\item \textbf{Case Algorithm \ref{alg:arb-crash} :}
|
||||
\item \textbf{Case Algorithm \ref{alg:ABroadcast} :}
|
||||
Some process executes the loop at \ref{code:sumbited-check-loop} and invokes $\PROVE(r+1);\APPEND^{(\star)}(r+1)$ at line~\ref{code:submit-proposition}. Let $p_i$ be this process.
|
||||
Immediately before line~\ref{code:submit-proposition}, line~\ref{code:round-increment} sets $r\leftarrow r+1$, so the previous loop iteration targeted $r$. We consider two sub-cases.
|
||||
|
||||
@@ -119,10 +129,10 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
|
||||
If round $r$ wasn't closed when $p_j$ execute $\PROVE_j(r)$ at \ref{code:submit-proposition}, then the $(j, r)$ will be in $P$ and the condition at \ref{code:sumbited-check-loop} should be true which implies that $p_j$ sould leave the loop at round $r$, contradicting the assumption that $p_j$ is now executing $\PROVE_j(r+1)$. In this case $r$ is closed.
|
||||
\end{itemize}
|
||||
|
||||
\item \textbf{Case Algorithm \ref{alg:arb-crash} :}
|
||||
\item \textbf{Case Algorithm \ref{alg:ADeliver} :}
|
||||
Some process invokes $\APPEND(r+1)$ at \ref{code:append-read}. Let $p_i$ be this process.
|
||||
Line~\ref{code:append-read} is guarded by the condition at \ref{code:check-if-winners}, which ensures that $p_i$ observed some $(\_,r+1)$ in $P$. Let $p_j$ be the issuer of the first $\PROVE_j(r+1)$ in the linearization $H$.
|
||||
When $p_j$ executed $\PROVE_j(r+1)$ at \ref{code:submit-proposition}, he observed no tuple $(\_,r+1)$ in $P$ at \ref{code:check-if-winners} because he's the issuer of the first one. By the same reasoning as in the Case Algorithm \ref{alg:arb-crash} (ii), $p_j$ must have observed that the round $r$ was closed.
|
||||
When $p_j$ executed $\PROVE_j(r+1)$ at \ref{code:submit-proposition}, he observed no tuple $(\_,r+1)$ in $P$ at \ref{code:check-if-winners} because he's the issuer of the first one. By the same reasoning as in the Case Algorithm \ref{alg:ABroadcast} (ii), $p_j$ must have observed that the round $r$ was closed.
|
||||
% Line C7 is guarded by the presence of $\PROVE(r)$ in $P$ with $r=r+1$ (C5).
|
||||
% Moreover, the local pointer $\textit{next}$ grow by increment of 1 and only advances after finishing the current round (C17), so if a process can reach $\textit{next}=r+1$ it implies that he has completed round $r$, which includes closing $r$ at C8 when $\PROVE(r)$ is observed.
|
||||
% Hence $\APPEND^\star(r+1)$ implies a prior $\APPEND(r)$ in $H$, so $r$ is closed.
|
||||
@@ -279,7 +289,7 @@ If some process invokes $\APPEND(r)$, then at least a process must have previous
|
||||
|
||||
Consider that there exists no round $r_1$ such that $p_i$ invokes a valid $\PROVE(r_1)$. In this case $p_i$ invokes infinitely many $\RBcast(S, \_, i)$ at line~\ref{code:submit-proposition} with $m \in S$ (line~\ref{code:Sconstruction}).\\
|
||||
The assumption that no $\PROVE(r_1)$ invoked by $p$ is valid implies by \DL \emph{Validity} that for every round $r' \geq r_{max}$, there exists at least one $\APPEND(r')$ in the DL linearization, hence by \Cref{lem:nonempty} for every possible round $r'$ there at least a winner. Because there is an infinite number of rounds, and a finite number of processes, there exists at least one process $p_k$ that invokes infinitely many valid $\PROVE(r')$ and by extension infinitely many $\ABbroadcast(\_)$. By \RB \emph{Validity}, $p_k$ eventually receives $p_i$ 's \RB messages. Let call $t_0$ the time when $p_k$ receives $p_i$ 's \RB message. \\
|
||||
At $t_0$, $p_k$ executes Algorithm \ref{alg:arb-crash} and sets $\mathit{received} \leftarrow \mathit{received} \cup \{S\}$ with $m \in S$ (line~\ref{code:receivedConstruction}).
|
||||
At $t_0$, $p_k$ executes Algorithm \ref{alg:rb-handler} and sets $\received \leftarrow \received \cup \{S\}$ with $m \in S$ (line~\ref{code:receivedConstruction}).
|
||||
For the first invocation of $\ABbroadcast(\_)$ by $p_k$ after the execution of \texttt{RReceived()}, $p_k$ must include $m$ in his proposal $S$ at line~\ref{code:Sconstruction} (because $m$ is pending in $j$'s $\received \setminus \delivered$ set). There exists a minimum round $r_2$ such that $p_k \in \Winners_{r_2}$ after $t_0$. By \Cref{lem:winners-propose}, eventually $\prop^{(i)}[r_2][k] \neq \bot$. By \Cref{lem:unique-proposal}, $\prop^{(i)}[r_2][k]$ is uniquely defined as the set $S$ proposed by $p_k$ at B6, which by \Cref{lem:inclusion} includes $m$. Hence eventually $m \in \prop^{(i)}[r_2][k]$ and $k \in \Winners_{r_2}$.
|
||||
|
||||
So if $p_i$ is a winner he satisfies the condition $(i, r_1) \in P$. And we show that if the first condition is never satisfied, the second one will eventually be satisfied. Hence either the first or the second condition will eventually be satisfied, and $p_i$ eventually exits the loop and returns from $\ABbroadcast(m)$.
|
||||
@@ -427,25 +437,19 @@ Which are cover by our FIFO-\ARB specification.
|
||||
|
||||
\subsubsection{Example executions}
|
||||
|
||||
% \begin{figure}
|
||||
% \centering
|
||||
% \resizebox{0.4\textwidth}{!}{
|
||||
% \input{diagrams/nonBFT_behaviour.tex}
|
||||
% }
|
||||
% \caption{Example execution of the ARB algorithm in a non-BFT setting}
|
||||
% \end{figure}
|
||||
\begin{figure}
|
||||
\centering
|
||||
\resizebox{0.4\textwidth}{!}{
|
||||
\input{diagrams/nonBFT_behaviour.tex}
|
||||
}
|
||||
\caption{Example execution of the ARB algorithm in a non-BFT setting}
|
||||
\end{figure}
|
||||
|
||||
|
||||
% \begin{figure}
|
||||
% \centering
|
||||
% \resizebox{0.4\textwidth}{!}{
|
||||
% \input{diagrams/BFT_behaviour.tex}
|
||||
% }
|
||||
% \caption{Example execution of the ARB algorithm with a byzantine process}
|
||||
% \end{figure}
|
||||
|
||||
|
||||
% font en fonctin de lusage
|
||||
|
||||
% winner invariant
|
||||
% order invariant
|
||||
\begin{figure}
|
||||
\centering
|
||||
\resizebox{0.4\textwidth}{!}{
|
||||
\input{diagrams/BFT_behaviour.tex}
|
||||
}
|
||||
\caption{Example execution of the ARB algorithm with a byzantine process}
|
||||
\end{figure}
|
||||
|
||||
@@ -172,80 +172,112 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au
|
||||
|
||||
\subsection{Algorithm}
|
||||
|
||||
\subsubsection{Variables}
|
||||
Each process $p_i$ maintains the following local variables:
|
||||
\LinesNotNumbered
|
||||
\begin{algorithm}
|
||||
$\texttt{last\_commited} \gets 0$\;
|
||||
$\texttt{last\_delivered} \gets 0$\;
|
||||
$\received \gets \emptyset$\;
|
||||
$\delivered \gets \emptyset$\;
|
||||
$\prop[r][j] \gets \bot, \forall r, j$\;
|
||||
$W[r] \gets \bot, \forall r$; this is the set of the winners for the round $r$\\
|
||||
$B[r] \gets \bot, \forall r$; this is the set of processes who have bahaved maliciously for round $r$\\
|
||||
$\resolved[r] \gets \bot, \forall r$\;
|
||||
$Y$ a $\BFTDL$ such that the value space is $\mathcal{R} \times \Pi$\;
|
||||
$V$ a $\BFTDL$ such that the value space is $(\mathcal{R} \times \mathcal{M} \times \Pi)$\;
|
||||
\end{algorithm}
|
||||
|
||||
\LinesNumbered
|
||||
\begin{algorithm}[H]
|
||||
\caption{t-BFT ARB at process $p_i$}\label{alg:bft-arb}
|
||||
|
||||
\SetKwBlock{LocalVars}{Local Variables:}{}
|
||||
\LocalVars{
|
||||
$\mathit{unordered} \gets \emptyset$,
|
||||
$\mathit{ordered} \gets \epsilon$,
|
||||
$\mathit{delivered} \gets \epsilon$\;
|
||||
$\mathit{prop}[r][j] \gets \bot, \forall j, r \in \Pi \times \mathbb{N}$\;
|
||||
$\mathit{done}[r] \gets \emptyset, \forall r \in \mathbb{N}$\;
|
||||
\caption{$\ABbroadcast(m)$ at process $p_i$}\label{alg:broadcast-bft}
|
||||
\SetAlgoLined
|
||||
\Fn{ABroadcast($m$)}{
|
||||
$\received \gets \received \cup \{m\}$\;
|
||||
Propose()\;
|
||||
}
|
||||
\end{algorithm}
|
||||
|
||||
\vspace{0.3em}
|
||||
|
||||
\For{$r = 1, 2, \ldots$}{
|
||||
\textbf{wait until} $\mathit{unordered} \setminus \mathit{ordered} \neq \emptyset$\;
|
||||
$S \gets \mathit{unordered} \setminus \mathit{ordered}$;
|
||||
$\RBcast(i, \texttt{PROP}, S, r)$\;
|
||||
|
||||
\textbf{wait until} $|\textsf{validated}(r)| \geq n - t$\;
|
||||
|
||||
\ForEach{$j \in \Pi$}{
|
||||
$\BFTAPPEND(\langle j, r\rangle)$\;
|
||||
\begin{algorithm}[H]
|
||||
\caption{Propose($\bot$) at process $p_i$}\label{alg:propose-bft}
|
||||
\SetAlgoLined
|
||||
% \Statex \textbf{Proposer Job}
|
||||
\Fn{Propose($\bot$)}{
|
||||
$r \gets \texttt{last\_commited}$\;
|
||||
\While{$S \neq \emptyset$ with $S \gets \received \setminus (\delivered \cup (\bigcup_{r' < r} \bigcup_{\substack{(j,S')\in W[r']\\ j\notin B[r']\\ S' \in \prop[r'][j]}} S'))$}{
|
||||
% \Comment{PROP PHASE}\;
|
||||
\tcc*[f]{PROP PHASE}\\
|
||||
$V.\BFTPROVE((r, S, i))$\;
|
||||
$\RBcast(i, \texttt{PROP}, S, r)$\;
|
||||
\textbf{wait} until $|\{j: \exists S, |\{k: (k,(r, S, j)) \in V.\BFTREAD()\}| \geq t+1\}| \geq n - t$\;
|
||||
% \Comment{COMMIT PHASE}
|
||||
\tcc*[f]{COMMIT PHASE}\\
|
||||
\For{\textbf{each} $j \in \Pi$}{
|
||||
% $Y[j].\BFTAPPEND(r)$\;
|
||||
$V.\BFTAPPEND((r, S, j))$\;
|
||||
$Y.\BFTAPPEND((r, j))$\;
|
||||
}
|
||||
$\RBcast(i, \texttt{COMMIT}, r)$\;
|
||||
\textbf{wait} until $|\resolved[r]| \geq n - t$\;
|
||||
% \Comment*{X PHASE}
|
||||
% \tcc*[f]{X PHASE}\\
|
||||
\BlankLine
|
||||
$W[r] \gets \{(j, S): |\{k: (k, (r, S, j)) \in V.\BFTREAD()\}| \geq t+1\}$\;
|
||||
$B[r] \gets \{j: |\{k: (k, (r, j)) \in Y.\BFTREAD()\}| \geq t+1\}$\;
|
||||
$r \gets r + 1$\;
|
||||
}
|
||||
|
||||
\ForEach{$j \in \Pi$}{
|
||||
$\textsf{send}(j, \texttt{DONE}, r)$\;
|
||||
}
|
||||
\textbf{wait until} $|\mathit{done}[r]| \geq n - t$\;
|
||||
|
||||
$\mathit{winners}[r] \gets \textsf{validated}(r)$\;
|
||||
|
||||
\textbf{wait until} $\forall j \in \mathit{winners}[r],\ \mathit{prop}[r][j] \neq \bot$\;
|
||||
$M \gets \bigcup_{j \in \mathit{winners}[r]} \mathit{prop}[r][j]$\;\nllabel{code:Mcompute}
|
||||
$\mathit{ordered} \gets \mathit{ordered} \cdot \ordered(M)$\;
|
||||
$\texttt{last\_commited} \gets r$\;
|
||||
}
|
||||
\end{algorithm}
|
||||
|
||||
\vspace{0.3em}
|
||||
|
||||
\Fn{\textsf{validated}($r$)}{
|
||||
\Return{$\{j: |\{k: (k, r) \in \BFTREAD()\}| \geq t+1\}$}\;
|
||||
}
|
||||
|
||||
\vspace{0.3em}
|
||||
|
||||
\Upon{$\ABbroadcast(m)$}{
|
||||
$\mathit{unordered} \gets \mathit{unordered} \cup \{m\}$\;
|
||||
}
|
||||
|
||||
\vspace{0.3em}
|
||||
|
||||
\Upon{$\textsf{rdeliver}(\texttt{PROP}, S, \langle j, r \rangle)$ from process $p_j$}{
|
||||
$\mathit{unordered} \gets \mathit{unordered} \cup S$;
|
||||
$\mathit{prop}[r][j] \gets S$\;
|
||||
$\BFTPROVE(\langle j, r\rangle)$\;
|
||||
}
|
||||
|
||||
\vspace{0.3em}
|
||||
|
||||
\Upon{$\textsf{receive}(\texttt{DONE}, r)$ from process $p_j$}{
|
||||
$\mathit{done}[r] \gets \mathit{done}[r] \cup \{j\}$\;
|
||||
}
|
||||
|
||||
\vspace{0.3em}
|
||||
|
||||
\Upon{$\ABdeliver()$}{
|
||||
\If{$\mathit{ordered} \setminus \mathit{delivered} = \emptyset$}{
|
||||
\begin{algorithm}[H]
|
||||
\caption{$\ABdeliver()$ at process $p_i$}\label{alg:deliver-bft}
|
||||
\SetAlgoLined
|
||||
\Fn{ADeliver($\bot$)}{
|
||||
$r \gets \texttt{last\_delivered}$\;
|
||||
\If{$|\resolved[r]| < n - t$}{
|
||||
\Return{$\bot$}
|
||||
}
|
||||
let $m$ be the first message in $\mathit{ordered} \setminus \mathit{delivered}$\;
|
||||
$\mathit{delivered} \gets \mathit{delivered} \cdot \{m\}$\;
|
||||
$W \gets \{(j, S): |\{k: (k, (r, S, j)) \in V.\BFTREAD()\}| \geq t+1\}$\;
|
||||
$B \gets \{j: |\{k: (k, (r, j)) \in Y.\BFTREAD()\}| \geq t+1\}$\;
|
||||
|
||||
\If{$\exists (j, S) \in W, j \notin B, S \notin \prop[r][j]$}{
|
||||
\Return{$\bot$}
|
||||
}
|
||||
\BlankLine
|
||||
$M \gets \bigcup_{\substack{(j,S)\in W\\ j\notin B\\ S \in prop[r][j]}} S$\;\nllabel{code:Mcompute}
|
||||
$m \gets \ordered(M \setminus \delivered)[0]$\;
|
||||
% \Comment*{Set $m$ as the smaller message not already delivered}
|
||||
$\delivered \leftarrow \delivered \cup \{m\}$\;
|
||||
\If{$M \setminus \delivered = \emptyset$}{
|
||||
$\texttt{last\_delivered} \gets \texttt{last\_delivered} + 1$\;
|
||||
}
|
||||
% \Comment*{Check if all messages from round $r$ have been delivered}
|
||||
\Return{$m$}
|
||||
}
|
||||
|
||||
\end{algorithm}
|
||||
|
||||
\begin{algorithm}[H]
|
||||
\caption{RB handler at process $p_i$}\label{alg:rb-handler-bft}
|
||||
\SetAlgoLined
|
||||
\Upon{$Rdeliver(j, \texttt{PROP}, S, r)$}{
|
||||
$\received \gets \received \cup \{S\}$\;
|
||||
\uIf{$\prop[r][j] = \bot \vee (\{S' : (j, (r, S', j)) \in V.\BFTREAD()\} = \{S\})$}{
|
||||
$V.\BFTPROVE((r, S, j))$\;
|
||||
}
|
||||
\Else{
|
||||
$Y.\BFTPROVE((r, j))$\;
|
||||
}
|
||||
$\prop[r][j] \gets \prop[r][j] \cup S$\;
|
||||
Propose()\;
|
||||
}
|
||||
|
||||
\vspace{1em}
|
||||
|
||||
\Upon{$Rdeliver(j, \texttt{COMMIT}, r)$}{
|
||||
$\resolved[r] \gets \resolved[r] \cup \{j\}$\;
|
||||
}
|
||||
\end{algorithm}
|
||||
|
||||
\textbf{Everything below has to be updated}
|
||||
|
||||
Binary file not shown.
@@ -61,7 +61,7 @@
|
||||
\newcommand{\ABdeliver}{\textsf{ADeliver}}
|
||||
\newcommand{\RBcast}{\textsf{RBroadcast}}
|
||||
\newcommand{\RBreceived}{\textsf{RReceived}}
|
||||
\newcommand{\ordered}{\textsf{order}}
|
||||
\newcommand{\ordered}{\textsf{ordered}}
|
||||
\newcommand{\Winners}{\mathsf{Winners}}
|
||||
\newcommand{\Messages}{\mathsf{Messages}}
|
||||
\newcommand{\ABlisten}{\textsf{AB-listen}}
|
||||
|
||||
BIN
misc/InstalParty2026/imgs/canonical.png
Normal file
BIN
misc/InstalParty2026/imgs/canonical.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 327 KiB |
BIN
misc/InstalParty2026/imgs/i3.png
Normal file
BIN
misc/InstalParty2026/imgs/i3.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 7.5 KiB |
BIN
misc/InstalParty2026/imgs/logo-6011e.png
Normal file
BIN
misc/InstalParty2026/imgs/logo-6011e.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 47 KiB |
BIN
misc/InstalParty2026/imgs/plasma.png
Normal file
BIN
misc/InstalParty2026/imgs/plasma.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 748 KiB |
BIN
misc/InstalParty2026/imgs/xfce.jpg
Normal file
BIN
misc/InstalParty2026/imgs/xfce.jpg
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 306 KiB |
BIN
misc/InstalParty2026/main.pdf
Normal file
BIN
misc/InstalParty2026/main.pdf
Normal file
Binary file not shown.
291
misc/InstalParty2026/main.tex
Normal file
291
misc/InstalParty2026/main.tex
Normal file
@@ -0,0 +1,291 @@
|
||||
\documentclass[aspectratio=43,10pt]{beamer}
|
||||
|
||||
\usetheme{Madrid}
|
||||
\usecolortheme{default}
|
||||
\usefonttheme{professionalfonts}
|
||||
\setbeamertemplate{navigation symbols}{}
|
||||
|
||||
\usepackage[T1]{fontenc}
|
||||
\usepackage[utf8]{inputenc}
|
||||
\usepackage[french]{babel}
|
||||
\usepackage{lmodern}
|
||||
\usepackage{microtype}
|
||||
|
||||
\usepackage{tikz}
|
||||
\usetikzlibrary{positioning,fit,calc,arrows.meta}
|
||||
|
||||
\title{}
|
||||
\subtitle{}
|
||||
\author{}
|
||||
\institute{}
|
||||
\date{}
|
||||
|
||||
\begin{document}
|
||||
|
||||
\begin{frame}{Install Party Linux}
|
||||
\framesubtitle{Luminy - 18 fevrier 2026}
|
||||
\centering
|
||||
\includegraphics[width=\linewidth,height=0.34\textheight,keepaspectratio]{imgs/logo-6011e.png}
|
||||
\end{frame}
|
||||
|
||||
\begin{frame}{Architecture d'un système d'exploitation}
|
||||
|
||||
Un OS c'est :
|
||||
\begin{itemize}
|
||||
\item Un Noyau (Kernel) : Ordonnancement, gestion de la mémoire, intéraction entre les composants physiques.
|
||||
\item Des Bibliothèques (Drivers) : UN driver est UNE interface avec un composant physique. (Carte Graphique, carte réseau, imprimante, \dots)
|
||||
\item Une Interface Graphique : Comment sont agenceés et gérées les fenetres
|
||||
\item Des Application : Les logiciels à utiliser
|
||||
\end{itemize}
|
||||
|
||||
\end{frame}
|
||||
|
||||
\begin{frame}{Architecture d'un système d'exploitation}
|
||||
|
||||
Un OS c'est :
|
||||
|
||||
\vspace{1em}
|
||||
|
||||
\centering
|
||||
\begin{tikzpicture}[
|
||||
box/.style={draw, rounded corners, align=center, minimum width=6cm, minimum height=0.9cm},
|
||||
arrow/.style={-{Latex[length=3mm,width=2mm]}, thick}
|
||||
]
|
||||
\pause
|
||||
\node[box] at (0, 5) (Noyau) {Noyau \\ (XNU, Windows NT, Linux, BSD, \dots)};
|
||||
\pause
|
||||
\node[box] at (0, 4) (Drivers) {Drivers \\ (Carte Graphique, disques durs, carte réseau, \dots)};
|
||||
\node[box, red] at (0, 3) (Drivers) {Materiel};
|
||||
\pause
|
||||
\node[box] at (0, 6) (GUI) {GUI \\ (DWM, Quartz Compositor + WindowServer, X11 + Gnome, Wayland + Swayne)};
|
||||
\pause
|
||||
\node[box] at (0, 7) (Apps) {Applications};
|
||||
\end{tikzpicture}
|
||||
|
||||
\end{frame}
|
||||
|
||||
\begin{frame}{Architecture d'un système d'exploitation}
|
||||
|
||||
Dans le cas de Windows, une version de windows = un package Noyau/GUI/Drivers définit et immuable + quelques applications par defaut
|
||||
|
||||
\vspace{1em}
|
||||
|
||||
\centering
|
||||
\begin{tikzpicture}[
|
||||
box/.style={draw, rounded corners, align=center, minimum width=6cm, minimum height=0.9cm},
|
||||
arrow/.style={-{Latex[length=3mm,width=2mm]}, thick}
|
||||
]
|
||||
\node[box] at (0, 5) (Noyau) {Noyau \\ Windows NT};
|
||||
\node[box] at (0, 4) (Drivers) {Drivers};
|
||||
\node[box] at (0, 3) (Drivers) {Materiel};
|
||||
\node[box] at (0, 6) (GUI) {GUI \\ DWM};
|
||||
\node[box] at (0, 7) (Apps) {Applications \\ Microsoft Edge, Outlook, Skype, \dots};
|
||||
\end{tikzpicture}
|
||||
|
||||
\pause
|
||||
|
||||
\textcolor{red}{Une distribution Linux c'est pareil !} \\
|
||||
\pause
|
||||
Une distribution = un package Noyau/GUI/Drivers définit + quelques applications par defaut
|
||||
|
||||
\end{frame}
|
||||
|
||||
\begin{frame}{Allons un peu plus en détail - L'interface graphique}
|
||||
|
||||
D'un point de vue de "à quoi ca ressemble", une distribution linux peut jouer sur 3 facteurs :
|
||||
\begin{itemize}
|
||||
\item Le serveur d'affichage (Xorg ou Weston principalement)
|
||||
\item Le gestionnaire de fenetres (flottant ou tiling)
|
||||
\item L'interface graphique (Gnome, KDE)
|
||||
\end{itemize}
|
||||
|
||||
\begin{center}
|
||||
\resizebox{0.8\width}{!}{
|
||||
\begin{tikzpicture}[
|
||||
box/.style={draw, rounded corners, align=center, minimum width=6cm, minimum height=0.9cm},
|
||||
arrow/.style={-{Latex[length=3mm,width=2mm]}, thick}
|
||||
]
|
||||
\node[box] at (0, 5) (Noyau) {Noyau \\ Linux};
|
||||
\node[box] at (0, 4) (Drivers) {Drivers};
|
||||
\node[box] at (0, 3) (Drivers) {Materiel};
|
||||
\node[box] at (0, 6) (GUI) {Serveur d'affichage \\ Xorg, Weston};
|
||||
\node[box] at (6, 6) (GUI) {Windows Manager \\ Compiz, KWin, Awesome, I3};
|
||||
\node[box] at (0, 7) (GUI) {Interface Graphique \\ Gnome, KDE};
|
||||
\node[box] at (0, 8) (Apps) {Applications};
|
||||
\end{tikzpicture}
|
||||
}
|
||||
\end{center}
|
||||
|
||||
\end{frame}
|
||||
|
||||
\begin{frame}{Allons un peu plus en détail - L'interface graphique}
|
||||
|
||||
|
||||
|
||||
\begin{center}
|
||||
\begin{minipage}{0.49\textwidth}
|
||||
\centering
|
||||
\includegraphics[width=\linewidth,height=0.34\textheight,keepaspectratio]{imgs/canonical.png}
|
||||
\par\smallskip
|
||||
\small GNOME
|
||||
\end{minipage}
|
||||
\hfill
|
||||
\begin{minipage}{0.49\textwidth}
|
||||
\centering
|
||||
\includegraphics[width=\linewidth,height=0.34\textheight,keepaspectratio]{imgs/xfce.jpg}
|
||||
\par\smallskip
|
||||
\small Xfce
|
||||
\end{minipage}
|
||||
|
||||
\vspace{4mm}
|
||||
|
||||
\begin{minipage}{0.49\textwidth}
|
||||
\centering
|
||||
\includegraphics[width=\linewidth,height=0.34\textheight,keepaspectratio]{imgs/plasma.png}
|
||||
\par\smallskip
|
||||
\small KDE Plasma
|
||||
\end{minipage}
|
||||
\hfill
|
||||
\begin{minipage}{0.49\textwidth}
|
||||
\centering
|
||||
\includegraphics[width=\linewidth,height=0.34\textheight,keepaspectratio]{imgs/i3.png}
|
||||
\par\smallskip
|
||||
\small i3 (tiling)
|
||||
\end{minipage}
|
||||
\end{center}
|
||||
|
||||
\end{frame}
|
||||
|
||||
\begin{frame}{Allons un peu plus en détail - La gestion des paquets}
|
||||
Pour installer une applications sous windows :
|
||||
\pause
|
||||
\begin{itemize}
|
||||
\item On execute un installeur (.msi ou .exe)
|
||||
\item On execute une version "portable" (.exe)
|
||||
\end{itemize}
|
||||
\pause
|
||||
\vspace{1em}
|
||||
Sous linux c'est pareil :
|
||||
\begin{itemize}
|
||||
\item On execute un installeur (.dnf ou .deb)
|
||||
\item On execute une version portable (Snap, Appimage, Flatpak, \dots)
|
||||
\end{itemize}
|
||||
|
||||
\pause
|
||||
\vspace{1em}
|
||||
Le support des format d'installer dependent des distribution. \\
|
||||
Les version portable (ou conteneurisé) sont a priori universel.
|
||||
\end{frame}
|
||||
|
||||
\begin{frame}{Allons un peu plus en détail - La gestion des paquets}
|
||||
On distingue donc deux grandes familles (en vrai y'en a plus que ca) \\
|
||||
RPM Package Manager et dpkg.
|
||||
|
||||
\pause
|
||||
|
||||
\begin{center}
|
||||
\begin{tikzpicture}[
|
||||
font=\small,
|
||||
n/.style={draw, rounded corners, align=center, minimum height=8mm, inner sep=3pt},
|
||||
a/.style={-{Latex[length=3mm,width=2mm]}, thick},
|
||||
node distance=10mm and 14mm
|
||||
]
|
||||
|
||||
\node[n] (rpm) {RPM\\DNF};
|
||||
\node[n, below=5mm of rpm] (dpkg) {DPKG\\APT};
|
||||
|
||||
\node[n, right=10mm of rpm] (redhat) {Red Hat};
|
||||
\node[n, right=10mm of redhat] (fedora) {Fedora};
|
||||
\node[n, right=10mm of fedora] (nobara) {Nobara};
|
||||
|
||||
\node[n, right=10mm of dpkg] (debian) {Debian};
|
||||
\node[n, right=10mm of debian] (ubuntu) {Ubuntu};
|
||||
\node[n, right=10mm of ubuntu] (mint) {Linux Mint};
|
||||
|
||||
\draw[a] (rpm) -- (redhat);
|
||||
\draw[a] (redhat) -- (fedora);
|
||||
\draw[a] (fedora) -- (nobara);
|
||||
|
||||
\draw[a] (dpkg) -- (debian);
|
||||
\draw[a] (debian) -- (ubuntu);
|
||||
\draw[a] (ubuntu) -- (mint);
|
||||
|
||||
\pause
|
||||
\node[n, below=5mm of dpkg] (tar) {tar.xx \\ PacMan};
|
||||
|
||||
\node[n, right=10mm of tar] (arch) {Arch Linux};
|
||||
\node[n, right=10mm of arch] (manjaro) {Manjaro};
|
||||
|
||||
\draw[a] (tar) -- (arch);
|
||||
\draw[a] (arch) -- (manjaro);
|
||||
|
||||
\end{tikzpicture}
|
||||
\end{center}
|
||||
|
||||
\end{frame}
|
||||
|
||||
\begin{frame}{Allons un peu plus en détail - La gestion des paquets}
|
||||
Les grosses différences de chaque gestionnaire sont plutot philosophique :
|
||||
\begin{itemize}
|
||||
\pause
|
||||
\item APT : Image de stabilité et de grand publique.
|
||||
\begin{itemize}
|
||||
\item + : Très stable, grosse communauté donc beaucoup de ressources dont en francais.
|
||||
\item - : Souvent plus en retard sur des versions très recentes de certains logiciels.
|
||||
\end{itemize}
|
||||
\pause
|
||||
|
||||
\item DNF : Image de robustesse avec une image plus d'usage professionel
|
||||
\begin{itemize}
|
||||
\item + : Très robuste, moins de chance de casser le système même pour des configurations exotiques
|
||||
\item - : Le processus de mise à jour peut être plus lent, et plus compliqué à prendre en main que APT.
|
||||
\end{itemize}
|
||||
\pause
|
||||
|
||||
\item PacMan : Minimaliste et ultra à jour.
|
||||
\begin{itemize}
|
||||
\item + : Systeme de "Rolling Release" qui permet d'avoir les mise à jour en continu.
|
||||
\item - : Necessite un plus grand travail de veille sur les mise à jour.
|
||||
\end{itemize}
|
||||
\end{itemize}
|
||||
|
||||
\end{frame}
|
||||
|
||||
\begin{frame}{Quelques autres trucs à savoir}
|
||||
\begin{itemize}
|
||||
\item /bin (binaries): Exécutables essentiels au système, utilisables par tous les utilisateurs
|
||||
\pause
|
||||
\item /boot: fichiers permettant à Linux de démarrer
|
||||
\pause
|
||||
\item /dev (device): Fichiers spéciaux représentant les point d'entrées de tous les périphériques (fichiers spéciaux des disques durs, écrans, partitions, consoles TTY, webcam, clavier, ...)
|
||||
\pause
|
||||
\item /etc (editing text config): Contient les fichiers de configuration du système et des setvices (*.conf, passwd, inittab, fstab)
|
||||
\pause
|
||||
\item /home: Répertoire personnel des utilisateurs
|
||||
\pause
|
||||
\item /mnt (mount) /media: Là où les ressources peuvent être montées de manière permanente (/media) ou temporaire (/mnt)
|
||||
\pause
|
||||
\item /root: Répertoire personnel du super utilisateur
|
||||
\pause
|
||||
\item /sbin (super binaries): Contient les programmes système essentiels utilisables par l'admin uniquement.
|
||||
\pause
|
||||
\item /tmp (temporary): Répertoire fichier temporaires
|
||||
\pause
|
||||
\item /usr (Unix System Resources): Contient des programmes, des librairies et des données utilisés par tous les utilisateurs du système
|
||||
\pause
|
||||
\item /var (variable): contient les données variables qui varient en fonction de l'utilisation du système. (logs, bdd, mails)
|
||||
\end{itemize}
|
||||
\end{frame}
|
||||
|
||||
\begin{frame}{Comment ca s'installe}
|
||||
\begin{itemize}
|
||||
\item Faire un backup
|
||||
\item Avoir une clé usb bootable
|
||||
\item Rentrer dans la selection du disque de boot en trouvant le bon FX
|
||||
\item Tester en execution "live" que tout fonctionne bien
|
||||
\item Choisir si on veut du mono ou dual-boot
|
||||
\item Allouer ses partitions en fonction des ses usages
|
||||
\end{itemize}
|
||||
\end{frame}
|
||||
|
||||
\end{document}
|
||||
Reference in New Issue
Block a user