typos

Recherche/BFT-ARBover/6_BFT_ARB/index.tex

@@ -2,29 +2,18 @@
 \subsection{Model extension}
 We consider a static set of $n$ processes with known identities, communicating by reliable point-to-point channels, in a complete graph. Messages are uniquely identifiable.
 
-\paragraph{Synchrony.} The network is asynchronous. Processes may crash or be byzantine; at most $f = \frac{n}{2} - 1$ processes can be faulty.
+\paragraph{Synchrony.} The network is asynchronous. Processes may crash or be byzantine.
 
-\paragraph{Communication.} Processes can exchange through a Reliable Broadcast (\RB) primitive (defined below) which's invoked with the functions \RBcast$(m)$ and \RBreceived$(m)$. There exists a shared object called DenyList (\DL) (defined below) that is interfaced with the functions \APPEND$(x)$, \PROVE$(x)$ and \READ$()$.
+\paragraph{Communication.} Processes can exchange through a Reliable Broadcast (\RB) object (defined below) which is invoked with the functions \RBcast$(m)$ and \RBreceived$()$. There exists $n$ shared object called DenyList (\DL) (defined below) that is interfaced with the functions \APPEND$(x)$, \PROVE$(x)$ and \READ$()$.
 
 \paragraph{Byzantine behaviour}
-A process exhibits Byzantine behavior if it deviates arbitrarily from the specified algorithm. This includes, but is not limited to, the following actions:
+A process is said to exhibit Byzantine behaviour if it deviates arbitrarily from the prescribed algorithm. Such deviations may, for instance, consist in invoking primitives (\RBcast, \APPEND, \PROVE, etc.) with invalid inputs or inputs crafted maliciously, colluding with other Byzantine processes in an attempt to manipulate the system state or violate its guarantees, deliberately delaying or accelerating the delivery of messages to selected nodes so as to disrupt the expected timing of operations, or withholding messages and responses in order to induce inconsistencies in the system state.
 
-\begin{itemize}
+Byzantine processes are constrained by the following. They cannot forge valid cryptographic signatures or threshold shares without access to the corresponding private keys. They cannot violate the termination, validity, or anti-flickering properties of the \DL{} object. They also cannot break the integrity, no-duplicates, or validity properties of the \RB{} primitive.
-  \item Invoking primitives (\RBcast, \APPEND, \PROVE, etc.) with invalid or maliciously crafted inputs.
-  \item Colluding with other Byzantine processes to manipulate the system's state or violate its guarantees.
-  \item Delaying or accelerating message delivery to specific nodes to disrupt the expected timing of operations.
-  \item Withholding messages or responses to create inconsistencies in the system's state.
-\end{itemize}
 
-Byzantine processes are constrained by the following:
-\begin{itemize}
-  \item They cannot forge valid cryptographic signatures or threshold shares without the corresponding private keys.
-  \item They cannot violate the termination, validity, or anti-flickering properties of the \DL{} object.
-  \item They cannot break the integrity, no-duplicates, or validity properties of the \RB{} primitive.
-\end{itemize}
 
-\paragraph{Notation.} Let $\Pi$ be the finite set of process identifiers and let $n \triangleq |\Pi|$. Two authorization subsets are $M \subseteq \Pi$ (processes allowed to issue \APPEND) and $V \subseteq \Pi$ (processes allowed to issue \PROVE). Indices $i,j \in \Pi$ refer to processes, and $p_i$ denotes the process with identifier $i$. Let $\mathcal{M}$ denote the universe of uniquely identifiable messages, with $m \in \mathcal{M}$. Let $\mathcal{R} \subseteq \mathbb{N}$ be the set of round identifiers; we write $r \in \mathcal{R}$ for a round. We use the precedence relation $\prec$ for the \DL{} linearization: $x \prec y$ means that operation $x$ appears strictly before $y$ in the linearized history of \DL. For any finite set $A \subseteq \mathcal{M}$, \ordered$(A)$ returns a deterministic total order over $A$ (e.g., lexicographic order on $(\textit{senderId},\textit{messageId})$ or on message hashes). For any round $r \in \mathcal{R}$, define $\Winners_r \triangleq \{\, j \in \Pi \mid (j,\PROVEtrace(r)) \prec \APPEND(r) \,\}$, i.e., the set of processes whose $\PROVE(r)$ appears before the first $\APPEND(r)$ in the \DL{} linearization.
+\paragraph{Notation.} Let $\Pi$ be the finite set of process identifiers. Two authorization subsets are $M \subseteq \Pi$ (processes allowed to issue \APPEND) and $V \subseteq \Pi$ (processes allowed to issue \PROVE). Indice $i \in \Pi$ refer to processes, and $p_i$ denotes the process with identifier $i$. Let $\mathcal{M}$ denote the universe of uniquely identifiable messages, with $m \in \mathcal{M}$. Let $\mathcal{R} \subseteq \mathbb{N}$ be the set of round identifiers; we write $r \in \mathcal{R}$ for a round. We use the precedence relation $\prec_k$ for the $\DL_k$ linearization: $x \prec_k y$ means that operation $x$ appears strictly before $y$ in the linearized history of $\DL_k$. For any finite set $A \subseteq \mathcal{M}$, \ordered$(A)$ returns a deterministic total order over $A$ (e.g., lexicographic order on $(\textit{senderId},\textit{messageId})$ or on message hashes). For any round $r \in \mathcal{R}$, define $\Winners_r^i \triangleq \{\, j \in \Pi \mid (j,\PROVEtrace(r)) \prec_k \APPEND(r) \,\}$, i.e., the set of processes whose $\PROVE(r)$ appears before the first $\APPEND(r)$ in the $\DL_k$ linearization. By extension for the set $X$ which contains every $\DL$ we define $\Winners_r \triangleq \bigcup_{k \in X} \Winners_r^k$.
-We denoted by $\PROVE^{(j)}(r)$ or $\APPEND^{(j)}(r)$ the operation $\PROVE(r)$ or $\APPEND(r)$ invoked by process $j$.
+We denoted by $\PROVE^{(j)}(r)$ or $\APPEND^{(j)}(r)$ the operation $\PROVE(r)$ or $\APPEND(r)$ invoked by process $j$, and by $\PROVE^{(j)}_{(k)}(r)$ or $\APPEND^{(j)}_{(k)}(r)$ the same operation invoked on the $\DL_k$ object.
 
 % ------------------------------------------------------------------------------
 \subsection{Primitives}
@@ -202,7 +191,7 @@ Each process $p_i$ maintains the following local variables:
   \State $Y[j]$ \Comment{Set of $n$ \BFTDL{}}
 \end{algorithmic}
 
-\renewcommand{\algletter}{A}
+\renewcommand{\algletter}{D}
 \begin{algorithm}[H]
     \caption{ABroadcast$(m)$}
     \begin{algorithmic}[1]
@@ -210,13 +199,16 @@ Each process $p_i$ maintains the following local variables:
             % \State $r \gets \current$
             \State $S \gets (\received \cup \{m\})$
             \For{\textbf{each}\ $r \in \{\current, \current +1, \dots\}$}
-                \State $\RBcast(i, PROP, S, r)$
+                \Statex \Comment{PROPOSAL PHASE}
-                \State \textbf{wait} until $|W_r| \geq n - f$ where $W_r = \bigcup_{j \in \Pi} Y[j].\BFTREAD()$
+                \State $\RBcast(i, \texttt{PROP}, S, r)$
-                \State $\forall j \in W_r, Y[j].\BFTAPPEND(r)$
+                \State \textbf{wait} until $|W_r| \geq n - f$ where $W_r \gets \{j: (j, \PROVEtrace(x)) \in \bigcup_{k \in \Pi} Y[k].\BFTREAD()\}$
-                \State $\RBcast(i, COMMIT, r)$
+                \Statex \Comment{COMMIT PHASE}
+                \State \textbf{for each} $j \in W_r$ \textbf{do} $Y[j].\BFTAPPEND(r)$
+                \State $\RBcast(i, \texttt{COMMIT}, r)$
                 \State \textbf{wait} until $|\resolved[r]| \geq n - f$
-                \State $W_r \gets \bigcup_{j \in \Pi} Y[j].\BFTREAD()$
+                \Statex \Comment{X PHASE}
-                \If{$i \in W_r \vee (\exists j, r': j \in W_{r'} \wedge \prop[r'][j] \ni m)$}
+                \State $W_r \gets \{j: (j, \PROVEtrace(x)) \in \bigcup_{k \in \Pi} Y[k].\BFTREAD()\}$
+                \If{$\exists r' \in \mathcal{R}, j \in W_{r'} : m \in \prop[r'][j]$} \Comment{any process $j$ submited $m$ in any round $r'$}
                     \State \textbf{break}
                 \EndIf
             \EndFor
@@ -224,7 +216,7 @@ Each process $p_i$ maintains the following local variables:
     \end{algorithmic}
 \end{algorithm}
 
-\renewcommand{\algletter}{B}
+\renewcommand{\algletter}{C}
 \begin{algorithm}[H]
     \caption{ADeliver$(m)$}
     \begin{algorithmic}[1]
@@ -233,7 +225,7 @@ Each process $p_i$ maintains the following local variables:
             \If{$|\resolved[r]| < n - f$}
                 \State \Return $\bot$
             \EndIf
-            \State $W_r \gets \bigcup_{j \in \Pi} Y[j].\BFTREAD()$
+            \State $W_r \gets \{j: (j, \PROVEtrace(x)) \in \bigcup_{k \in \Pi} Y[k].\BFTREAD()\}$
             \If{$\exists j \in W_r,\ \prop[r][j] = \bot$} 
                 \State \Return $\bot$
             \EndIf
@@ -248,21 +240,21 @@ Each process $p_i$ maintains the following local variables:
     \end{algorithmic}
 \end{algorithm}
 
-\renewcommand{\algletter}{C}
+\renewcommand{\algletter}{E}
 \begin{algorithm}[H]
     \caption{RB handlers}
     \begin{algorithmic}[1]
-        \Function{Rreceived}{j, PROP, S, r}
+        \Upon{$Rdeliver(j, \texttt{PROP}, S, r)$}
             \State $\received \gets \received \cup \{S\}$
             \State $\prop[r][j] \gets S$
             \State $Y[j].\BFTPROVE(r)$
-        \EndFunction
+        \EndUpon
 
         \vspace{1em}
         
-        \Function{Rreceived}{j, COMMIT, r}
+        \Upon{$Rdeliver(j, \texttt{COMMIT}, r)}$
-            \State $\resolved[r] \cup \{j\}$
+            \State $\resolved[r] \gets \resolved[r] \cup \{j\}$
-        \EndFunction
+        \EndUpon
     \end{algorithmic}
 \end{algorithm}
 

Recherche/BFT-ARBover/main.tex

@@ -18,6 +18,13 @@
 \renewcommand{\thealgorithm}{\Alph{algorithm}} % Float labels: Algorithm A, B, C
 \newcommand{\algletter}{}
 \algrenewcommand\alglinenumber[1]{\scriptsize\textbf{\algletter}#1}
+
+\algnewcommand\algorithmicupon{\textbf{upon}}
+% \algnewcommand\algorithmicdo{\textbf{do}}
+\algdef{SE}[UPON]{Upon}{EndUpon}[1]{%
+  \algorithmicupon\ #1\ \algorithmicdo%
+}{\textbf{end upon}}
+
 \usepackage{tikz}
 \graphicspath{{diagrams/out}}
 \usepackage{xspace}
@@ -45,7 +52,7 @@
 \newcommand{\RB}{\textsf{RB}\xspace}
 \newcommand{\res}{\mathsf{res}}
 \newcommand{\ARB}{\textsf{ARB}\xspace}
-\newcommand{\DL}{\textsf{DL}\xspace}
+\newcommand{\DL}{\textsf{DL}}
 \newcommand{\APPEND}{\textsf{APPEND}}
 \newcommand{\PROVE}{\textsf{PROVE}}
 \newcommand{\PROVEtrace}{\textsf{prove}}