amaury_joly/bwconsistency
1
0
Fork 0
Code Issues 5 Pull Requests Packages Projects 3 Releases Wiki Activity

nouvel algo

Browse Source
This commit is contained in:
Amaury JOLY
2025-09-29 16:06:43 +02:00
parent 35a9d91779
commit 3ea8de6388
4 changed files with 300 additions and 44 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
.devcontainer/devcontainer.json
View File

@@ -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

4
README.md
View File

@@ -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: <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>
## Introduction

BIN
Recherche/ALDLoverAB/main.pdf
View File

Binary file not shown.

338
Recherche/ALDLoverAB/main.tex
View File

@@ -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}
\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}