diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json index 5aede31..af46fd8 100644 --- a/.devcontainer/devcontainer.json +++ b/.devcontainer/devcontainer.json @@ -6,7 +6,7 @@ "containerEnv": { //Add your build arguments here "DEBIAN_FRONTEND": "noninteractive" }, - "runArgs": [], //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 diff --git a/README.md b/README.md index 8845d9b..3e968dc 100755 --- a/README.md +++ b/README.md @@ -1,7 +1,7 @@ # Consistence Faible Byzantine Pour le Cloud -Ce projet est hébergé ici: [https://amauryjoly.fr/gitea/amaury_joly/bwconsistency](https://amauryjoly.fr/gitea/amaury_joly/bwconsistency). -Un miror est disponible sur le gitlab du laboratoire du LIS: [https://gitlab.lis-lab.fr/amaury.joly/bwconsistency](https://gitlab.lis-lab.fr/amaury.joly/bwconsistency) +Ce projet est hébergé ici: . +Un miror est disponible sur le gitlab du laboratoire du LIS: ## Introduction diff --git a/Recherche/ALDLoverAB/main.pdf b/Recherche/ALDLoverAB/main.pdf index 40cc6ba..f3e8b5f 100644 Binary files a/Recherche/ALDLoverAB/main.pdf and b/Recherche/ALDLoverAB/main.pdf differ diff --git a/Recherche/ALDLoverAB/main.tex b/Recherche/ALDLoverAB/main.tex index 552cc04..2bc5759 100644 --- a/Recherche/ALDLoverAB/main.tex +++ b/Recherche/ALDLoverAB/main.tex @@ -1,63 +1,319 @@ -\documentclass{article} +\documentclass[11pt]{article} +\usepackage[margin=1in]{geometry} \usepackage[T1]{fontenc} \usepackage[utf8]{inputenc} +\usepackage{lmodern} +\usepackage{microtype} +\usepackage{amsmath,amssymb,amsthm,mathtools} +\usepackage{thmtools} +\usepackage{enumitem} \usepackage{csquotes} -\usepackage[french]{babel} -\usepackage[affil-it]{authblk} -\usepackage{fullpage} - -\usepackage{amsmath} -\usepackage{amssymb} - -\usepackage{biblatex} - -% \usepackage[linesnumbered,ruled,vlined]{algorithm2e} +\usepackage[hidelinks]{hyperref} +\usepackage[nameinlink,noabbrev]{cleveref} \usepackage{algorithm} -\usepackage{algorithmicx} -\usepackage[noend]{algpseudocode} -\algrenewcommand\alglinenumber[1]{\tiny #1} +\usepackage{algpseudocode} +% Line-number prefix configuration (A/B/C) +\renewcommand{\thealgorithm}{\Alph{algorithm}} % Float labels: Algorithm A, B, C +\newcommand{\algletter}{} +\algrenewcommand\alglinenumber[1]{\scriptsize\textbf{\algletter}#1} +\usepackage{tikz} +\usepackage{xspace} -\usepackage{etoolbox} +\usepackage[fr-FR]{datetime2} -% --- Partage du compteur de lignes entre plusieurs algorithmes -\makeatletter -\newcounter{algoLine} -\renewcommand{\alglinenumber}[1]{\arabic{algoLine}} -\newcommand{\nextalgline}{\stepcounter{algoLine}} -\newcommand{\resetalgline}{\setcounter{algoLine}{1}} -\makeatother +\usepackage{fancyhdr} +\pagestyle{fancy} +\fancyhf{} +\fancyfoot[L]{Compilé le \DTMnow} +\fancyfoot[C]{\thepage} +\renewcommand{\headrulewidth}{0pt} +\renewcommand{\footrulewidth}{0pt} -\newtheorem{property}{Property} +\theoremstyle{plain} \newtheorem{theorem}{Theorem} -\newtheorem{proof}{Proof} +\newtheorem{lemma}[theorem]{Lemma} +\newtheorem{corollary}[theorem]{Corollary} +\theoremstyle{definition} +\newtheorem{definition}{Definition} +\theoremstyle{remark} +\newtheorem{remark}{Remark} -\addbibresource{sources.bib} +\newcommand{\RB}{\textsf{RB}\xspace} +\newcommand{\ARB}{\textsf{ARB}\xspace} +\newcommand{\DL}{\textsf{DL}\xspace} +\newcommand{\APPEND}{\textsf{APPEND}} +\newcommand{\PROVE}{\textsf{PROVE}} +\newcommand{\READ}{\textsf{READ}} +\newcommand{\ABbroadcast}{\textsf{AB-broadcast}} +\newcommand{\ABdeliver}{\textsf{AB-deliver}} +\newcommand{\RBcast}{\textsf{RB-cast}} +\newcommand{\RBreceived}{\textsf{RB-received}} +\newcommand{\ordered}{\textsf{ordered}} +\newcommand{\Winners}{\mathsf{Winners}} +\newcommand{\ABlisten}{\textsf{AB-listen}} + +\newcommand{\delivered}{\mathsf{delivered}} +\newcommand{\received}{\mathsf{received}} +\newcommand{\prop}{\mathsf{prop}} + +\crefname{theorem}{Theorem}{Theorems} +\crefname{lemma}{Lemma}{Lemmas} +\crefname{definition}{Definition}{Definitions} +\crefname{algorithm}{Algorithm}{Algorithms} + +\title{Upgrading Reliable Broadcast to Atomic Reliable Broadcast with a DenyList Primitive} +\date{\vspace{-1ex}} \begin{document} +% \maketitle -\title{???} -\author{JOLY Amaury \\ \textbf{Encadrants :} GODARD Emmanuel, TRAVERS Corentin} -\affil{Aix-Marseille Université, Scille} -\date{\today} - -% \begin{titlepage} -% \maketitle -% \end{titlepage} +\begin{abstract} +We show how to upgrade a Reliable Broadcast (\RB) primitive to Atomic Reliable Broadcast (\ARB) by leveraging a synchronous DenyList (\DL) object. In a purely asynchronous message-passing model with crashes, \ARB is impossible without additional power. The \DL supplies this power by enabling round closing and agreement on a set of "+winners" for each round. We present the algorithm, its safety arguments, and discuss liveness and complexity under the assumed synchrony of \DL. +\end{abstract} +\paragraph{Keywords} Atomic broadcast, total order broadcast, reliable broadcast, consensus, synchrony, shared object, linearizability. \section{Introduction} +Atomic Reliable Broadcast (\ARB)---a.k.a. total order broadcast---ensures that all processes deliver the same sequence of messages. In asynchronous message-passing systems with crashes, implementing \ARB is impossible without additional assumptions, as it enables consensus. We assume a synchronous DenyList (\DL) object and demonstrate how to combine \DL with an asynchronous \RB to realize \ARB. -\subsection{Model} -\input{intro/index.tex} +\section{Model} +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. -\subsection{Algorithms} -\input{algo/index.tex} +\paragraph{Synchrony.} The network is asynchronous. Processes may crash; at most $f$ crashes occur. -\subsection{proof} -\input{proof/index.tex} +\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$()$. -\printbibliography +\paragraph{Notation.} Let $\Pi$ be the finite set of process identifiers and let $n \triangleq |\Pi|$. Two authorization subsets are $\Pi_M \subseteq \Pi$ (processes allowed to issue \APPEND) and $\Pi_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,\PROVE(r)) \prec \APPEND(r) \,\}$, i.e., the set of processes whose $\PROVE(r)$ appears before the first $\APPEND(r)$ in the \DL{} linearization. + +% ------------------------------------------------------------------------------ +\section{Primitives} +\subsection{Reliable Broadcast (RB)} + +\RB provides the following properties in the model. +\begin{itemize}[leftmargin=*] + \item \textbf{Integrity}: Every message received was previously sent. $\forall p_i:\ \RBreceived_i(m) \Rightarrow \exists p_j:\ \RBcast_j(m)$. + \item \textbf{No-duplicates}: No message is received more than once at any process. + \item \textbf{Validity}: If a correct process broadcasts $m$, every correct process eventually receives $m$. +\end{itemize} + +\subsection{DenyList (DL)} +The \DL is a \emph{shared, append-only} object that records attestations about opaque application-level tokens. It exposes the following operations: +\begin{itemize}[leftmargin=*] + \item \APPEND$(x)$ + \item \PROVE$(x)$: issue an attestation for token $x$; this operation is \emph{valid} (return true) only if no \APPEND$(x)$ occurs earlier in the \DL linearization. Otherwise, it is invalid (return false). + \item \READ$()$: return a (permutation of the) valid operations observed so far; subsequent reads are monotone (contain supersets of previously observed valid operations). +\end{itemize} + +\paragraph{Validity.} \APPEND$(x)$ is valid iff the issuer is authorized (in $\Pi_M$) and $x$ belongs to the application-defined domain $S$. \PROVE$(x)$ is valid iff the issuer is authorized (in $\Pi_V$) and there is no earlier \APPEND$(x)$ in the \DL linearization. + +\paragraph{Progress.} If a correct process invokes \APPEND$(x)$, then eventually all correct processes will be unable to issue a valid \PROVE$(x)$, and \READ{} at all correct processes will (eventually) reflect that \APPEND$(x)$ has been recorded. + +\paragraph{Termination.} Every operation invoked by a correct process eventually returns. + +\paragraph{Interface and Semantics.} The \DL provides a single global linearization of operations consistent with each process's program order. \READ{} is prefix-monotone; concurrent updates become visible to all correct processes within bounded time (by synchrony). Duplicate requests may be idempotently coalesced by the implementation. + +% ------------------------------------------------------------------------------ +\section{Target Abstraction: Atomic Reliable Broadcast (ARB)} +Processes export \ABbroadcast$(m)$ and \ABdeliver$(m)$. \ARB requires total order: +\begin{equation*} + \forall m_1,m_2,\ \forall p_i,p_j:\ \ \ABdeliver_i(m_1) < \ABdeliver_i(m_2) \Rightarrow \ABdeliver_j(m_1) < \ABdeliver_j(m_2), +\end{equation*} +plus Integrity/No-duplicates/Validity (inherited from \RB and the construction). + +% ------------------------------------------------------------------------------ + +\section{Algorithm} +Each process $p_i$ maintains: +\begin{itemize}[leftmargin=*] + \item $\received$ --- set of \RB-received messages not yet delivered; + \item $\delivered$ --- set of messages already delivered; + \item $\prop[r][j]$ --- proposal set announced by process $p_j$ for round $r$ (possibly $\bot$ locally); + \item Local view of \DL via \READ(). + \item $next$ --- lowest round index not yet delivered. +\end{itemize} + +\subsection{Handlers and Procedures} +\renewcommand{\algletter}{A} +\begin{algorithm}[H] + \caption{\RB handler (at process $p_i$)}\label{alg:rb-handler} + \begin{algorithmic}[1] + \State \textbf{on} $\RBreceived(m, S, r, j)$ \textbf{do} + \State $\received \leftarrow \received \cup \{m\}$ + \State $\prop[r][j] \leftarrow S$ \Comment{Record sender $j$'s proposal $S$ for round $r$} + \end{algorithmic} +\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. + +\renewcommand{\algletter}{B} +\begin{algorithm}[H] + \caption{\ABbroadcast$(m)$ (at process $p_i$)}\label{alg:ab-bcast} + \begin{algorithmic}[1] + \State \textbf{on} $\ABbroadcast(m, S, r, j)$ \textbf{do} + \State $P \leftarrow \READ()$ \Comment{Fetch latest \DL state to learn recent $\PROVE$ operations} + \State $r \leftarrow \max\{ r' : \exists j,\ (j,\PROVE(r')) \in P \}$ \Comment{Pick next open round: one past the most recent proved round} + \State $S \leftarrow (\received \setminus \delivered) \cup \{m\}$ \Comment{Propose all pending messages plus the new $m$} + \State $\RBcast\big(m, S, r, \textit{self}\big)$ \Comment{Asynchronously disseminate proposal via \RB} + \State $\PROVE(r)$ \Comment{Attest participation in round $r$ while it is still open} + \State $\APPEND(r)$ \Comment{Close round $r$; freezes $\Winners_r$ in the \DL linearization} + \While{$\big(\nexists j : \exists r, (j, \PROVE(r)) \in P \wedge \ m \in \prop[r][j])$} \Comment{Wait until $m$ is included in some closed round and all needed proposals are known} + \State $P \leftarrow \READ()$ \Comment{Refresh local view of \DL} + \State $\RBcast\big(m, S, r, \textit{self}\big)$ + \State $\PROVE(r)$ + \State $\APPEND(r)$ + \EndWhile + \end{algorithmic} +\end{algorithm} + +% \paragraph{} TODO +\renewcommand{\algletter}{C} +\begin{algorithm}[H] + \caption{\ABdeliver() at process $p_i$}\label{alg:delivery} + \begin{algorithmic}[1] + \State \textbf{on} \ABdeliver() \textbf{do} \Comment{Called when the process wants to receive the next message} + \State $P \leftarrow \READ()$ \Comment{Fetch latest \DL state to learn recent $\PROVE$ operations} + \If{$\nexists j : (j,\PROVE(next)) \in P$} \Comment{No process has proved round $\textit{next}$} + \State \Return $\bot$ \Comment{No closed round ready for delivery} + \EndIf + \State $\APPEND(next)$ \Comment{Close round $\textit{next}$ if not already closed} + \If{$\PROVE(next) == FALSE$} \Comment{Process closed rounds strictly in order} + \State $P \leftarrow \READ()$ \Comment{Refresh local view of \DL} + \State $\Winners_{\textit{next}} \leftarrow \{ j : (j,\PROVE(\textit{next})) \in P \}$ \Comment{Frozen winners of round $\textit{next}$} + \If{$\forall j \in \Winners_{\textit{next}}:\ \prop[\textit{next}][j] \neq \bot$} + \State $M_{\textit{next}} \leftarrow \bigcup_{j \in \Winners_{\textit{next}}} \prop[\textit{next}][j]$ \Comment{Round-$\textit{next}$ message set} + \ForAll{$m \in \ordered(M_{\textit{next}})$} \Comment{Deterministic per-round order} + \If{$m \notin \delivered$} + \State $\delivered \leftarrow \delivered \cup \{m\}$ + \State \Return $m$ \Comment{Deliver exactly one message per call} + \EndIf + \EndFor + \State $\textit{next} \leftarrow \textit{next} + 1$ \Comment{This round fully processed; advance} + \State \textbf{continue} \Comment{Try the next closed round (if any)} + \Else + \State \Return $\bot$ \Comment{Some winners' proposals not yet known via \RB} + \EndIf + \EndIf + \State \Return $\bot$ \Comment{No closed round ready for delivery} + \end{algorithmic} +\end{algorithm} +% ------------------------------------------------------------------------------ +\section{Correctness} + +\begin{definition}[Closed round]\label{def:closed-round} +Given a \DL{} linearization $H$, a round $r\in\mathcal{R}$ is \emph{closed} in $H$ iff $H$ contains an operation $\APPEND(r)$. +Equivalently, there exists a time after which every $\PROVE(r)$ is invalid in $H$. +\end{definition} + +\begin{lemma}[Stable round closure]\label{lem:closure-stable} +If a round $r$ is closed, then there exists a unique linearization point $t_0$ of $\APPEND(r)$ in the \DL, and from that point on, no $\PROVE(r)$ can be valid. +Once closed, a round never becomes open again. +\end{lemma} + +\begin{lemma}[Across rounds]\label{lem:across} +Rounds are delivered in strictly increasing $r$. Concatenating the per-round sequences yields a single global total order. +Equivalently, $\forall r_1,r_2$ such that $r_1, r_2$ are closed and $r_1 < r_2$, all round $r$ such that $r_1 < r < r_2$ are also closed. +\end{lemma} + +\begin{lemma}[Well-defined winners]\label{lem:winners} +In any execution, whenever some process computes $\Winners_r$, its current \DL-view contains $\APPEND(r)$; hence $\Winners_r$ is computed only for closed round. +\end{lemma} + +\begin{lemma}[View-Invariant Winners]\label{lem:view-invariant} +For any closed round $r$, there exists a unique set +\[ + \Winners_r = \{ j : (j,\PROVE(r)) \prec \APPEND^\star(r) \} +\] +with $\APPEND^\star(r)$ being the earliest \APPEND$(r)$ in the \DL linearization. +\end{lemma} + +\begin{proof}[Proof] + We admit that some $\APPEND(r)$ occurs; if $\APPEND(r)$ occurs then it exists an operation $\APPEND^\star(r)$ that is the earliest in the linearization. + + Due to the validity property of DL, a $\PROVE(r)$ is valid iff $\PROVE(r) \prec \APPEND^\star(r)$. Thus, + \[\Winners_r \triangleq \{ j : (j,\PROVE(r)) \prec \APPEND^\star(r) \}\] + + Let's consider two correct processes $p_i$ and $p_j$ and two \READ{} responses $P_i$ and $P_j$ such that + \[ + \APPEND^\star(r) \prec (i,\PROVE(r)) \prec P_i + \APPEND^\star(r) \prec (j,\PROVE(r)) \prec P_j + \] + By the \DL interface, \READ{} returns a permutation of the valid operations observed so far, and hence every $\PROVE(r)$ that precedes $\APPEND^\star(r)$ is valid while any $\PROVE(r)$ that follows $\APPEND^\star(r)$ is invalid. We ensures that + \[\{ j : (j,\PROVE(r)) \in P_i \} = \{ j : (j,\PROVE(r)) \in P_j \} = \Winners_r.\] +\end{proof} + +\begin{lemma}[No empty winners]\label{lem:nonempty} +For any round $r$ closed, $\Winners_r \neq \emptyset$. +\end{lemma} + +\begin{proof}[Proof] + Assume some correct process invokes \APPEND$(r)$. Hence an \APPEND$(r)$ occurs, and there exists an operation $\APPEND^\star(r)$ that is earliest in the \DL linearization. + + Let $p_k$ be the issuer of $\APPEND^\star(r)$. By the algorithm (\ABbroadcast), any process that issues \APPEND$(r)$ (B6) must have previously invoked \PROVE$(r)$ (B5) in its program order. Because the \DL is linearizable and preserves per-process program order in the linearization, we obtain + \[ + (k,\PROVE(r)) \prec \APPEND^\star(r). + \] + Consequently, $(k,\PROVE(r))$ is a \emph{valid} attestation for round $r$ (no prior \APPEND$(r)$ exists before $\APPEND^\star(r)$ by definition of $\APPEND^\star(r)$). By the definition of $\Winners_r$, + \[ + k \in \Winners_r. + \] + Therefore $\Winners_r \neq \emptyset$, i.e., $|\Winners_r|>0$. +\end{proof} + +\begin{lemma}[Proposal convergence]\label{lem:convergence} +For any closed round $r$, after all \RB messages from $\Winners_r$ are received, every correct process computes the same $M_r = \bigcup_{j\in \Winners_r} \prop[r][j]$. +\end{lemma} + +\begin{proof}[Proof] + Fix a round $r$ such that some $\APPEND(r)$ occurs; hence $r$ is \emph{closed}. By \Cref{lem:winners}, all correct processes that observe $\READ()$ after $\APPEND^\star(r)$ compute the same winner set $\Winners_r$. + + For any $j \in \Winners_r$, in process $p_j$'s program order we have, for round $r$: + \[ + \RBcast(\_, S_j, r, j) \ \text{(B4)} \quad\text{before}\quad \PROVE(r) \ \text{(B5)} \quad\text{before}\quad \APPEND(r) \ \text{(B6)}. + \] + Since $\Winners_r = \{\, j : (j,\PROVE(r)) \prec \APPEND^\star(r) \,\}$, each winner $j$ executed (B4) before $\APPEND^\star(r)$, thereby broadcasting a \RB message for $(r,j)$ with some (uniquely determined) payload $S_j$. + + The round chosen at (B2) is the next open round. After (B6) closes $r$, any later invocation of \ABbroadcast\ by $p_j$ picks a strictly larger round. Thus $p_j$ executes at most one $\RBcast(\_,\cdot,r,j)$, so the set $S_j$ attached to $(r,j)$ is unique. + + Now consider any two correct processes $p_a$ and $p_b$ that have (via \RB) received all winners' messages for round $r$. By the \RB \emph{Integrity} and \emph{No-duplicates} properties, every delivery of $p_j$'s \RB message for $(r,j)$ carries the same $S_j$, and the handler sets + \[ + \prop[r][j] \leftarrow S_j \text{ (A3)} + \] + at both $p_a$ and $p_b$. Therefore, + \[ + M_r^{(a)} \triangleq \bigcup_{j\in\Winners_r} \prop^{(a)}[r][j] + \;=\; \bigcup_{j\in\Winners_r} S_j + \;=\; \bigcup_{j\in\Winners_r} \prop^{(b)}[r][j] + \triangleq M_r^{(b)}. + \] + Hence, after all \RB messages from $\Winners_r$ have been received, every correct process computes the same $M_r$. +\end{proof} + +\begin{lemma}[Per-round determinism]\label{lem:per-round} +Given \Cref{lem:convergence}, all correct processes iterate $\ordered(M_r)$ in the same order; hence the delivery order inside round $r$ is identical at all correct processes. +\end{lemma} -\end{document} \ No newline at end of file +\begin{corollary}[No duplicates] +Each message is delivered at most once since membership in $\delivered$ is tested before delivery. +\end{corollary} + +\begin{lemma}[Inclusion]\label{lem:inclusion} +If some process invokes $\ABbroadcast(m)$, then there exist a (closed) round $r$ and a process +$j\in\Winners_r$ such that $j$ invokes +\[ +\RBcast(\_, S, r, j)\quad\text{with}\quad m\in S. +\] +Equivalently, every $\ABbroadcast(m)$ is included in the proposal of some winner of some closed round. +\end{lemma} + +\begin{theorem}[\ARB] +Under the assumed \DL synchrony and \RB reliability, the algorithm implements Atomic Reliable Broadcast. +\end{theorem} + +\bibliographystyle{plain} +\begin{thebibliography}{9} +% (left intentionally blank) +\end{thebibliography} + +\end{document}