ajout biblio

Recherche/BFT-ARBover/2_Primitives/index.tex

@@ -1,6 +1,6 @@
 \subsection{DenyList Object}
 
- We assume a linearizable DenyList (\DL) object as in~\cite{frey:disc23} with the following properties.
+ We assume a linearizable DenyList (\DL) object, following the specification in~\cite{frey:disc23}, with the following properties.
   
     The DenyList object type supports three operations: $\APPEND$, $\PROVE$, and $\READ$. These operations appear as if executed in a sequence $\Seq$ such that:
     \begin{itemize}

Recherche/BFT-ARBover/3_ARB_Def/index.tex

@@ -1,5 +1,5 @@
 
-Processes export \ABbroadcast$(m)$ and $m = \ABdeliver()$. \ARB requires the following properties:
+Processes export \ABbroadcast$(m)$ and $m = \ABdeliver()$. We adopt the standard Atomic Broadcast specification of~\cite{Defago2004}. \ARB requires the following properties:
 \begin{itemize}[leftmargin=*]
   \item \textbf{Total Order}: 
   \begin{equation*}

Recherche/BFT-ARBover/4_ARB_with_RB_DL/index.tex

@@ -318,8 +318,7 @@ history of operations) are uniquely determined.
 
 \paragraph{State machine replication over \ARB.}
 Assume a system that exports a FIFO-\ARB primitive with the guarantees that if a correct process invokes $\ABbroadcast(m)$, then every correct process eventually $\ABdeliver(m)$ and the invocation eventually returns.
-Following the classical \emph{state machine replication} approach
-such as described in Schneider~\cite{Schneider90}, we can implement a fault-tolerant service by ensuring the following properties:
+Following the classical \emph{state machine replication} approach described by Schneider~\cite{Schneider90}, we can implement a fault-tolerant service by ensuring the following properties:
 \begin{quote}
   \textbf{Agreement.} Every nonfaulty state machine replica receives every request. \\
   \textbf{Order.} Every nonfaulty state machine replica processes the requests it receives in
@@ -332,7 +331,7 @@ Which are cover by our FIFO-\ARB specification.
 
 
 \begin{theorem}[From \ARB to synchronous \DL]\label{thm:arb-to-dl}
-  In an asynchronous message-passing system with crash failures, assume a FIFO Atomic Reliable Broadcast primitive with Integrity, No-duplicates,Validity, and the liveness of $\ABbroadcast$. Then there exists an implementation of a DenyList object that satisfies Termination, Validity, and Anti-flickering properties.
+  In an asynchronous message-passing system with crash failures, assume a FIFO Atomic Reliable Broadcast primitive (in the standard Total Order / Atomic Broadcast sense of~\cite{Defago2004}) with Integrity, No-duplicates, Validity, and the liveness of $\ABbroadcast$. Then there exists an implementation of a DenyList object that satisfies Termination, Validity, and Anti-flickering properties.
 \end{theorem}
 
 \begin{proof}

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

@@ -2,9 +2,9 @@
 \subsection{Model extension}
 We extend the crash model of Section 1 (same process universe, asynchronous setting, uniquely identifiable messages, and reliable point-to-point channels) with Byzantine faults and Byzantine-resilient dissemination primitives.
 
-\paragraph{Failure threshold.} At most $t$ processes may be Byzantine, and we assume $n > 3t$.
+\paragraph{Failure threshold.} At most $t$ processes may be Byzantine, and we assume $n > 3t$, following standard asynchronous Byzantine assumptions~\cite{Bracha87}.
 
-\paragraph{Additional communication primitive.} In addition to reliable point-to-point channels, processes use Reliable Broadcast ($\RB$) with operations $\RBcast(m)$ and $m=\rdeliver()$. We use Bracha's Byzantine RB specification (1987): for a fixed sender and broadcast instance, all correct processes that deliver, deliver the same payload, and Byzantine equivocation on that instance is prevented.
+\paragraph{Additional communication primitive.} In addition to reliable point-to-point channels, processes use Reliable Broadcast ($\RB$) with operations $\RBcast(m)$ and $m=\rdeliver()$. We use Bracha's Byzantine RB specification~\cite{Bracha87}: for a fixed sender and broadcast instance, all correct processes that deliver, deliver the same payload, and Byzantine equivocation on that instance is prevented.
 
 \paragraph{Byzantine behaviour}
 A Byzantine process may deviate arbitrarily from the algorithm (malformed inputs, selective omission, collusion, inconsistent timing, etc.).
@@ -20,7 +20,7 @@ For any operation $F \in O$,$F_i(...)$ denotes that the operation $F$ is invoked
 
 \subsection{Reliable Broadcast (RB)}
 
-\RB provides the following properties in the model.
+\RB provides the following properties in this model (cf.~\cite{Bracha87}).
 \begin{itemize}[leftmargin=*]
   \item \textbf{Integrity}: Every message received was previously sent. $\forall p_i:\ m = \rbreceived_i() \Rightarrow \exists p_j:\ \RBcast_j(m)$.
   \item \textbf{No-duplicates}: No message is received more than once at any process.

Recherche/BFT-ARBover/main.tex

@@ -113,7 +113,7 @@
 \begin{document}
 
 \section{Model 1: Crash}
-We consider a static set $\Pi$ of $n$ processes with known identities, communicating by reliable point-to-point channels, in a complete graph. Messages are uniquely identifiable. At most $f$ processes can crash, with $n \geq f$.
+We consider a static set $\Pi$ of $n$ processes with known identities, communicating by reliable point-to-point channels, in a complete graph. Messages are uniquely identifiable. At most $f$ processes can crash, with $n \geq f$, in the standard asynchronous crash-failure message-passing model~\cite{ChandraToueg96}.
 
 \paragraph{Synchrony.} The network is asynchronous.
 
@@ -298,6 +298,27 @@ For any operation $F \in O$,$F_i(...)$ denotes that the operation $F$ is invoked
 \bibliographystyle{plain}
 \begin{thebibliography}{9}
 % (left intentionally blank)
+\bibitem{frey:disc23}
+Davide Frey, Mathieu Gestin, and Michel Raynal.
+\newblock The synchronization power (consensus number) of access-control objects: The case of allowlist and denylist.
+\newblock {\em LIPIcs, DISC 2023}, 281:21:1--21:23, 2023.
+\newblock doi:10.4230/LIPIcs.DISC.2023.21.
+
+\bibitem{Bracha87}
+Gabriel Bracha.
+\newblock Asynchronous byzantine agreement protocols.
+\newblock {\em Information and Computation}, 75(2):130--143, 1987.
+
+\bibitem{Defago2004}
+Xavier Defago, Andre Schiper, and Peter Urban.
+\newblock Total order broadcast and multicast algorithms: Taxonomy and survey.
+\newblock {\em ACM Computing Surveys}, 36(4):372--421, 2004.
+
+\bibitem{ChandraToueg96}
+Tushar Deepak Chandra and Sam Toueg.
+\newblock Unreliable failure detectors for reliable distributed systems.
+\newblock {\em Journal of the ACM}, 43(2):225--267, 1996.
+
 \bibitem{Schneider90}
 Fred B.~Schneider.
 \newblock Implementing fault-tolerant services using the state machine