\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[hidelinks]{hyperref}
\usepackage[nameinlink,noabbrev]{cleveref}
\usepackage{algorithm}
\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[fr-FR]{datetime2}

\usepackage{fancyhdr}
\pagestyle{fancy}
\fancyhf{}
\fancyfoot[L]{Compilé le \DTMnow}
\fancyfoot[C]{\thepage}
\renewcommand{\headrulewidth}{0pt}
\renewcommand{\footrulewidth}{0pt}

\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}{Definition}
\theoremstyle{remark}
\newtheorem{remark}{Remark}

\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

\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.

\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. 

\paragraph{Synchrony.} The network is asynchronous. Processes may crash; at most $f$ crashes occur.

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


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