text:
\section{Introduction}

 \emph{Linearizability} is a well-known and very useful property of shared object implementations~\cite{linearizability}.
Intuitively, with a linearizable (implementation of) object each operation must appear as if it takes effect instantaneously
	at some point during the time interval that it actually spans;
	for deterministic algorithms linearizable objects can be used as if they were atomic.\footnote{Throughout the paper we consider only implementations that are \emph{wait free}~\cite{herlihy91}.}
As pointed out by the seminal work of Golab \emph{et al.} \cite{sl11}, however,
	linearizable objects are not as strong as atomic objects in the following sense:
	a randomized algorithm that works with atomic objects may lose some of its properties
	if we replace the atomic objects that it uses with objects that are only linearizable.
In particular, they present a randomized algorithm
	that guarantees that
	some random variable has \emph{expected value} 1,
	but if we replace the algorithm's atomic registers with linearizable registers,
	a \mbox{\emph{strong adversary}} can manipulate schedules to
	ensure that this random variable
	has expected value $\frac{1}{2}$.

\subsection{Linearizability and termination}
A natural question is whether termination is one of the properties that can be lost
	with the use of linearizable objects.
More precisely:
	is there a randomized algorithm that
	(a) terminates with probability 1 against a strong adversary when the objects that it uses are atomic, but
	(b) when these objects are replaced with
	linearizable objects,
 	a strong adversary can
	ensure that
	the algorithm never terminates?
This question is particularly interesting because
	achieving termination is
	one of the main uses of randomized algorithms
	(e.g., to ``circumvent'' the famous FLP impossibility result~\cite{flp})~\cite{abrahamson1988,aspnes1993,aspnes1998,
	aspnes2003,aspnes1990,aspnes1992,attiya08,bracha1991,chandra1996},
	but it
	is not answered by the results in~\cite{sl11},
	and to the best of our knowledge,
	it is also not addressed in subsequent papers on this subject~\cite{sl19,sl15,sl12}.

In this paper, among other things, we show that termination can be lost.
Specifically, we give a randomized algorithm
	that uses registers such that:
	(1) if these registers are atomic then the algorithm terminates,
	i.e., all the processes
	halt, with probability~1, even against a strong adversary,
	and
	(2) if the registers are ``only'' linearizable,
	a strong adversary can prevent termination:
	it can always manipulate schedules so that processes never halt.

\subsection{Strong linearizability}
Golab \emph{et al.} also introduced a stronger version of linearizability called \emph{strong linearizability}~\cite{sl11}.
Intuitively, while in linearizability the order of all operations can be determined ``off-line'' given the entire execution,
	in strong linearizability the order of all operations has to be fixed irrevocably ``on-line'' without knowing the rest of the execution.
	Golab \emph{et al.} proved that strongly linearizable (implementations of) objects are ``as good'' as atomic objects, even for randomized algorithms:
	they can replace atomic objects while preserving the algorithm's correctness properties
	including termination with probability~1.
Unfortunately, there are important cases where strong linearizability is impossible to achieve.

For example, Helmi \emph{et al.} proved that
	a large class of so-called \emph{non-trivial} objects, including multi-writer multi-reader (MWMR) registers,
	do not
	have strongly linearizable implementations from single-writer multi-reader (SWMR) registers~\cite{sl12}.
This impossibility result may affect many existing randomized algorithms (e.g.,\cite{renaming2014,renaming2011,CRenaming2011,renaming2010,aspnes1993,appcount10}):
,	these algorithms use atomic MWMR registers,
	so if we want to run them in systems with SWMR registers
	we cannot hope to \emph{automatically} do so
	just by replacing their atomic MWMR registers
	with strongly linearizable implementations from SWMR registers.

Similarly, consider the well-known ABD algorithm that implements linearizable SWMR
	registers in message-passing systems~\cite{abd}.\footnote{This implementation works under the assumption that fewer than half of the processes may crash.}
One important use of this algorithm is to relate message-passing and shared-memory systems as follows:
	any algorithm that works with atomic shared registers can be automatically
	transformed into an algorithm for message-passing systems
	by replacing its atomic registers with the ABD register implementation.
It has been recently shown, however,
	that the ABD register implementation is \emph{not} strongly linearizable~\cite{abdnotsl}.
Thus one cannot use the ABD implementation to automatically transform any shared-memory randomized algorithm
	that terminates with probability~1
	into an algorithm that works in message-passing systems:
	using the ABD register implementation instead of atomic registers
	in a randomized algorithm may prevent termination.

\subsection{Write strong-linearizability}

Motivated by the impossibility of implementing strongly linearizable registers mentioned above,
	we propose a new type of register linearizability, called \emph{write strong-linearizability},
	that is strictly stronger than (plain) linearizability
	but strictly weaker than strong linearizability.
Intuitively, while in strong linearizability the order of \emph{all} operations has to be fixed irrevocably ``on-line''
	without knowing the rest of the execution,
	in write strong-linearizability only the write operations must be ordered ``on-line''.
This intermediate type of linearizability has some desirable properties,
	as described below:

\begin{itemize}

\item In some cases where linearizability is not sufficient to achieve termination,
	write strong-linearizability is.
	To show this, we describe a randomized algorithm such that
	if the registers of this algorithm are only \emph{linearizable},
    then a strong adversary can prevent its termination;
	but if they are \emph{$\textrm{write strongly-linearizable}$},
    then the algorithm terminates with probability 1 (Section~\ref{sectiontoyalgo}).

   We then generalize this result as follows:
	for every randomized algorithm $\mathcal{A}$ that solves a task $T$
	and terminates with probability~1 against a strong adversary,
	there is a corresponding randomized algorithm $\mathcal{A}'$ for task $T$ such that:
	(a)~if the registers that $\mathcal{A}'$ uses are only linearizable,
		$\mathcal{A}'$ does not terminate, but
	(b) if they are $\textrm{write strongly-linearizable}$, $\mathcal{A}'$ terminates.

\item In contrast to the impossibility result proved in~\cite{sl12},
	$\textrm{write strongly-linearizable}$ MWMR registers \emph{are} implementable from SWMR registers.
	To prove this we modify a known implementation of MWMR registers~\cite{swlamport},
	and we linearize the write operations ``on-line'' by using vector timestamps
	that may be \emph{only partially formed} (Section~\ref{sectionwslalgo}).

	Achieving write strong-linearizability, however, is harder than achieving just linearizability.
	We give a simpler implementation of  MWMR registers
	from SWMR registers
	that uses Lamport clocks to timestamp writes~\cite{lam86},
	and we prove that this implementation is linearizable but \emph{not} $\textrm{write strongly-linearizable}$ (Section~\ref{sectionlamport}).

\item	Although the ABD implementation of SWMR registers is not strongly linearizable,
	we show that it is actually $\textrm{write strongly-linearizable}$.
	In fact, we prove that \emph{any} linearizable implementation of SWMR registers is necessarily $\textrm{write strongly-linearizable}$;
	this holds for message-passing, shared-memory, and hybrid systems (Section~\ref{swsection}).
\end{itemize}

Finally, it is worth noting that even though we focus on registers here,
	our intermediate notion of linearizability
	can be extended to other types of objects
	and operations.
Intuitively, an implementation of an object is \emph{strongly linearizable with respect to a subset of operations $O$}
	if the order of all operations \emph{in $O$} must be fixed irrevocably ``on-line'' without knowing the rest of the execution.

All the results presented are proven in this paper, but due to the space limitation
	several proofs are relegated to optional appendices.

\section{Model sketch}
We consider a standard distributed system where asynchronous processes that may fail by crashing
communicate via registers and other shared objects.
In such systems, shared objects can be used to \emph{implement} other shared objects
such that the implemented objects are \emph{linearizable} and \emph{wait-free}~\cite{herlihy91,linearizability}.

\subsection{Atomic registers}
A register $R$ is \emph{atomic} if its read and write operations are \emph{instantaneous} (i.e., indivisible);
	each read
	must return the value of the last write
	that precedes it, or the initial value of $R$ if no such write exists.
A SWMR register $R$ is shared by a set $S$ of processes such that it can be written
	(sequentially) by exactly one process $w \in S$
	and can be read by all processes~in~$S$; we say that $w$ is the \emph{writer} of $R$~\cite{lam86}.
A MWMR register $R$ is shared by a set $S$ of processes such that it can be written
	and read by all processes~in~$S$.

\subsection{Linearizable implementations of registers}
In an object implementation,
	each operation spans an interval that starts
	with an \emph{invocation} and terminates with a \emph{response}.

\begin{definition}
Let $o$ and $o'$ be any two operations.
\begin{itemize}

\item $o$ \emph{precedes} $o'$ if the response of $o$ occurs
	before \mbox{the invocation of $o'$.}\XMP{make terms consistent}

\item $o$ \emph{is concurrent with} $o'$ if neither precedes the other.

\end{itemize}
\end{definition}

Roughly speaking,
	an object implementation is \emph{linearizable}~\cite{linearizability}
	if, although operations can be concurrent,
	operations behave as if they occur in a \emph{sequential} order (called ``linearization order'')
	that is consistent with the order in which operations actually occur:
	if an operation $o$ precedes an operation $o'$, then $o$ is before $o'$ in the linearization order
	(the precise definition is given in~\cite{linearizability}).

Let $\mathcal{H}$ be the set of histories of a register implementation.
An operation $o$ is \emph{complete} in a history $H\in\mathcal{H}$ if $H$ contains both the invocation and response of $o$,
	otherwise $o$ is \emph{pending}.
\XMP{define set of history H, we have it before?}

\begin{definition}\label{defl}
A function $f$ is \emph{a linearization function for $\mathcal{H}$} (with respect to the type register)
	if it maps each history $H \in \mathcal{H}$ to a sequential history $f(H)$ such that:\MP{sequential history def?}
\begin{enumerate}
	\item \label{p1} $f(H)$ contains all completed operations of $H$ and possibly some non-completed ones (with matching responses added).

	\item \label{p2} If operation $o$ precedes $o'$ in $H$,
		then $o$ occurs before $o'$ in $f(H)$.

	\item \label{p3} For any read operation $r$ in $f(H)$,
		if no write operation occurs before $r$ in $f(H)$, then $r$ reads the initial value of the register;
		otherwise, $r$ reads the value written by the last write operation that occurs before $r$ in $f(H)$.
\end{enumerate}
\end{definition}

\begin{definition}\cite{sl11}
A function $f$ is \emph{a strong linearization function for $\mathcal{H}$} if:

(L) $f$ is a linearization function for $\mathcal{H}$, and

(P) for any histories $G,H \in \mathcal{H}$, if $G$ is a prefix of $H$,
	then $f(G)$ is a prefix of $f(H)$.
\end{definition}

By restricting the strong linearization requirement, i.e., property (P)
	 to write operations only,
	 we define the following:

\begin{definition}\label{defwsl}
A function $f$ is \emph{a $\str$ function for $\mathcal{H}$} if:

(L) $f$ is a linearization function for $\mathcal{H}$, and

(P) for any histories $G,H \in \mathcal{H}$, if $G$ is a prefix of $H$,
	then the sequence of write operations in $f(G)$ is a prefix of the sequence of write operations in $f(H)$.
\end{definition}

\begin{definition}\label{L-I}
An algorithm $\mathcal{A}$ that implements a \emph{register}
	is linearizable,
	$\textrm{write strongly-linearizable}$, or strong linearizable,
	if there is a linearization, $\str$, or strong linearization function (with respect to the type register)
	for the set of histories $\mathcal{H}$ of $\mathcal{A}$.
\end{definition}

\section{Termination under linearizability and write strong-linearizability}\label{sectiontoyalgo}
In this section,
	we show that in some cases linearizability is not sufficient for termination but
	write strong-linearizability~is.
To do so,
	we present a randomized algorithm, namely Algorithm~\ref{toyalgo}, and prove that
	(a) it fails to terminate if its registers are only linearizable
	but (b) it terminates if they are $\textrm{write strongly-linearizable}$.
We then use Algorithm~\ref{toyalgo} to show that
	every randomized algorithm $\mathcal{A}$ that solves a task
	and terminates with probability~1 against a strong adversary,
	has a corresponding randomized algorithm $\mathcal{A}'$ for the same task such that:
	(a) if the registers that $\mathcal{A}'$ uses are linearizable,
		$\mathcal{A}'$ does not terminate, but
	(b) if they are $\textrm{write strongly-linearizable}$, $\mathcal{A}'$ terminates.

\begin{algorithm}[!ht]
\caption{A game for $n\ge3$ processes}
\begin{flushleft}
\textsc{Shared MWMR registers} $R_1, R_2, C$
\vspace*{-2mm}
\end{flushleft}
\begin{multicols}{2}
\label{toyalgo}
\begin{algorithmic}[1]

\STATEx \textsc{Code of process $p_i$, $i\in \{0, 1\}$}:
\vspace{1mm}
\FOR  {rounds $j=1,2,...$}\label{enter1}
\vspace{.7mm}
\STATE \{* \textbf{Phase 1} *\}
\STATE $R_1 \gets [i,j]$ \label{pwrite1}
\IF{$i=0$}\label{cointosser1}
\STATE \{* $p_0$ flips a coin and writes it into $C$ *\}
\STATE $c \gets$ coin flip \label{pcoin1-1}
\STATE $C \gets c$  \label{pcoin1-2}
\ENDIF
\vspace{.7mm}
\STATE \{* \textbf{Phase 2} *\}
\STATE $R_2 \gets \textsc{0}$ \label{cleanr2}
\STATE $v\gets R_2$ \label{v1}
\IF{$v < n-2$}\label{guard2}
     \STATE \textbf{exit for loop} \label{exit2}
\ENDIF
\vspace{.7mm}
\ENDFOR
\STATE \textbf{return}\label{halt0}

\columnbreak

\STATEx \textsc{Code of process $p_i$, \mbox{$i\in \{2, 3, \ldots, n-1\}$}:}
\vspace{1mm}

\FOR  {rounds $j=1,2,...$}\label{enter2}
\vspace{.7mm}
\STATE \{* \textbf{Phase 1} *\}
\STATE $R_1 \gets \bot$\label{cleanr1}
\STATE $C \gets \bot$\label{cleanc}
\STATE $u_1 \gets R_1$ \label{u1}
\STATE $u_2 \gets R_1$ \label{u2}
\STATE $c \gets C$ \label{rcoin1}
\IF{($u_1 = \bot$ \textbf{or} $u_2 = \bot$ \textbf{or} $c = \bot$)}\label{guard0}
     \STATE \textbf{exit for loop} \label{exit0}
\ENDIF
\IF{($u_1 \neq [c,j]$ \textbf{or} $u_2 \neq [1-c,j]$)}\label{guard1}
     \STATE \textbf{exit for loop} \label{exit1}
\ENDIF\label{endexit}
\vspace{.7mm}
\STATE \{* \textbf{Phase 2} *\}
\STATE $R_2 \gets \textsc{0}$ \label{cleanr2-2}
\STATE $v \gets R_2$ \label{pread2}
\STATE $v \gets v+1$ \label{inc2}
\STATE $R_2 \gets v$ \label{pwrite2}
\vspace{.7mm}
\ENDFOR
\STATE \textbf{return}\label{halt1}
\end{algorithmic}
\end{multicols}
\vspace*{-3mm}
\end{algorithm}

Algorithm~\ref{toyalgo} uses three MWMR registers $R_1$, $R_2$, and $C$.
It can be viewed as a game executed by $n \ge 3$ processes, which are partitioned into
	two groups: the ``hosts'' $p_0$ and $p_1$ and the ``players'' $p_2,...,p_n$.
The game proceeds in asynchronous rounds, each round consisting of two phases.
In Phase 1 of a round $j$, process $p_1$ writes $[1,j]$ into $R_1$;
	while $p_0$ first writes $[0,j]$ in $R_1$,
	 and then it writes the result
	of a 0-1 coin flip into $C$ (lines~\ref{pwrite1}-\ref{pcoin1-2}).
After doing so, each of $p_0$ and $p_1$ proceeds to Phase 2.

In Phase 1, each player $p_i$ ($2 \le i \le n-1)$ reads $R_1$ twice (lines~\ref{u1}--\ref{u2}),
	and then it reads $C$ (line~\ref{rcoin1}).
If $p_i$ reads $c \in \{0,1\}$ from $C$ and the sequence of two values that it read from $R_1$ is
	$[c,j]$ and then $[1-c,j]$, $p_i$ proceeds to Phase~2,
	otherwise it exits the game (lines~\ref{guard0}-\ref{endexit}).
Every player $p_i$ that stays in the game
	resets $R_2$ to $0$ (line~\ref{cleanr2-2})
	and tries to increment it by 1 (lines~\ref{pread2}-\ref{pwrite2});
	thus $R_2$ holds a lower bound on the number of players that enter Phase 2.
After doing so $p_i$ proceeds to the next round.

In Phase 2, each host $p_0$ and $p_1$ first resets $R_2$ to $0$ (line~\ref{cleanr2})
	and then reads $R_2$ (line~\ref{v1}).
If a host sees that $R_2 \ge n-2$
	then it is certain that \emph{all} the players remained in the game,
	and so it also remains in the game by proceeding to the next round;
	otherwise it exits the game.

We will show that if the registers are only linearizable,
 	then a strong adversary $\mathcal{S}$ can manipulate schedules such
	that the game represented by Algorithm~\ref{toyalgo} continues forever;
	more precisely, regardless of the coin flip results, $\mathcal{S}$ can construct a run of Algorithm~\ref{toyalgo}
	in which all the processes loop forever (Theorem~\ref{LinearizableIsWeak} in Section~\ref{ltoysection}).
We then show that if the registers are $\textrm{write strongly-linearizable}$, then all the correct processes\footnote{A process is correct
	if it takes infinitely many steps. We assume that processes continue to take steps (forever)
	even after returning from the algorithm in lines~\ref{halt0} or line~\ref{halt1}.}
	 return from the algorithm with probability~$1$ (Theorem~\ref{WSLinearizableIsStrong} in Section~\ref{wsltoysection})

At high-level, the main idea of the proof is as follows.
Assume the register $R_1$ is not atomic,
	so each of its operations spans an interval of time, and operations on $R_1$ can be concurrent.
Consider the time $t$ after $p_0$ flipped the coin (line~\ref{pcoin1-1}).
Suppose at that time $t$, the write of $[1,j]$ into $R_1$ by $p_1$ is still pending and concurrent
	with the completed write of $[0,j]$ into $R_1$ by $p_0$.

If $R_1$ is linearizable,
	then adversary has the power to linearize the two writes in either order:
	$[0,j]$ before $[1,j]$, or $[1,j]$ before $[0,j]$.
So based on the outcome $c$ of the coin flip,
	the adversary can ensure that all the players
	read $[c,j]$ and then $[1-c,j]$ from $R_1$
	which forces them to stay in the game.

If, on the other hand, $R_1$ is write strongly-linearizable,
	the adversary does not have this power:
	at the time $p_0$ completes its write of $[0,j]$ into $R_1$
	(and therefore before the adversary can see the result of the coin flip)
	the adversary must decide whether the concurrent write of $[1,j]$ by $p_1$
	is linearized before $[0,j]$ or not.
With probability at least 1/2,
	the result of the coin flip will not ``match'' this decision.
So in each round, with probability at least 1/2, the players
	will \emph{not} read $[c,j]$ and then $[1-c,j]$ from $R_1$
	and so they will exit the game.
(Note that if $R_1$ is atomic, operations are instantaneous, and so of course the adversary has no power to continue the game forever.)

In Algorithm~\ref{toyalgo} only register $R_1$ is unbounded, but we can easily make
	$R_1$ bounded (see Appendix~\ref{btoysection}).

\subsection{Linearizability does not ensure termination}\label{ltoysection}

\begin{theorem}\label{LinearizableIsWeak}
If registers $R_1$, $R_2$, and $C$ are only linearizable,
	a~strong adversary $\mathcal{S}$ can construct a run of Algorithm~\ref{toyalgo} where all the processes execute
	infinitely many rounds.
\end{theorem}

\begin{proof}
Assume the registers of Algorithm~\ref{toyalgo} are only linearizable but \emph{not} $\textrm{write strongly-linearizable}$.
A strong adversary $\mathcal{S}$ can construct an infinite run of Algorithm~\ref{toyalgo} as follows (Figure~\ref{toy}):

\begin{figure}[!htb]
   		 \centering
    		\includegraphics[width=0.8\textwidth]{sg/toy-algo.pdf}
   		 \caption{Phase 1 in round $j=1$ of an infinite execution}
   		 \label{toy}
	\end{figure}

\medskip
\noindent
\textbf{Phase 1} (of round $j=1$):
\begin{enumerate}

\item Processes $p_2, p_3, \ldots, p_{n-1}$ write $\bot$ into $R_1$ and $C$ in lines~\ref{cleanr1} and~\ref{cleanc}.

\item At some time $t_0$ after all the above write operations complete,
	process $p_0$ starts writing~$[0,1]$ into $R_1$ in line~\ref{pwrite1},
	process $p_1$ starts writing~$[1,1]$ into $R_1$ in line~\ref{pwrite1},
	and $\textrm{processes } p_2, p_3, \ldots, p_{n-1}$ start reading $R_1$ in line~\ref{u1}.

\item At time $t_1 > t_0$, process $p_0$ completes its writing of $[0,1]$ into $R_1$ in line~\ref{pwrite1}.

\item After time $t_1$,
	process $p_0$ flips a coin in line~\ref{pcoin1-1} and writes the result into the shared register $C$ in line~\ref{pcoin1-2}.
	Let $t_c > t_1$ be the time when $p_0$ completes this write of $C$.

Depending on the result of $p_0$'s coin flip (and therefore the content of $C$),
	the adversary $\mathcal{S}$ continues the run it is constructing in one of the following two ways:

\textbf{Case 1}: $C=0$ at time $t_c$.

The continuation of the run in this case is shown at the top right of Figure~\ref{toy}.

\begin{enumerate}

\item At time $t_2 > t_c$,
		$p_1$ completes its writing of [1,1] into $R_1$ in line~\ref{pwrite1}.

		Note that \emph{both} $p_0$ and $p_1$ have now completed Phase 1 of round $j=1$.

\item The adversary $\mathcal{S}$ linearizes the write of $[1,1]$ into $R_1$ by $p_1$
	\emph{after} the write of $[0,1]$ into $R_1$ by~$p_0$.

\item Note that $p_2, p_3, \ldots, p_{n-1}$ are still reading $R_1$ in line~\ref{u1}.
Now the adversary linearizes these read operations \emph{between} the above write of $[0,1]$ by $p_0$ and the write of $[1,1]$ by~$p_1$.

\item At time $t_3 > t_2$,
		$\textrm{processes } p_2, p_3, \ldots, p_{n-1}$ complete their read of $R_1$ in line~\ref{u1}.
By the above linearization, they read $[0,1]$, and so they set (their local variable) $u_1 = [0,1]$ in line~\ref{u1}.

\item Then $\textrm{processes } p_2, p_3, \ldots, p_{n-1}$ start and complete their read of $R_1$ in line~\ref{u2}.
Since (1)~these reads start \emph{after} the time $t_2$ when $p_1$ completed its write of $[1,1]$ into $R_1$,
	and (2)~this write is linearized \emph{after} the write of $[0,1]$ by $p_0$ into $R_1$,
	$\textrm{processes } p_2, p_3, \ldots, p_{n-1}$ read~$[1,1]$.
So they all set (their local variable) $u_2 = [1,1]$ in line~\ref{u2}.
Let $t_4 > t_3$ be the time when every process in $\{p_2, p_3, \ldots, p_{n-1}\}$ has set $u_2 = [1,1]$ in line~\ref{u2}.

\item After time $t_4$, $\textrm{processes } p_2, p_3, \ldots, p_{n-1}$ start reading $C$ in line~\ref{rcoin1}.
		Since $C =0$ at time~$t_c$ and it is not modified thereafter,
		$p_2, p_3, \ldots, p_{n-1}$ read $0$ and set (their local variable) $c = 0$ in line~\ref{rcoin1}.

	So at this point, $\textrm{processes } p_2, p_3, \ldots, p_{n-1}$ have $u_1 = [0,1]$, $u_2 = [1,1]$ and $c = 0$.

\item Then $p_2, p_3, \ldots, p_{n-1}$ execute line~\ref{guard0}, and find that
	the condition ($u_1 = \bot$ \textbf{or} $u_2 = \bot$ \textbf{or} $c = \bot$)
	of this line does not hold,
	and so they proceed to execute line~~\ref{guard1}.

\item When $p_2, p_3, \ldots, p_{n-1}$ execute line~\ref{guard1}, they find that the condition ($u_1 \neq [c,j]$ \textbf{or}  $u_2 \neq [1-c,j]$)
	of this line does \emph{not} hold, because they have $u_1 = [c,1] = [0,1]$ and $u_2 = [1- c,1] = [1,1]$.

	   So $p_2, p_3, \ldots, p_{n-1}$ complete Phase 1 of round $j=1$
	   without exiting in line~\ref{exit1}.
	Recall that both $p_0$ and $p_1$ also completed Phase 1 of round $j=1$ without exiting.

\end{enumerate}

\textbf{Case 2}: $C=1$ at time $t_c$.

The continuation of the run in this case is shown at the bottom right of Figure~\ref{toy}.
This continuation is symmetric to the one for Case 1:
	the key difference is that the adversary $\mathcal{S}$ now linearizes
	$p_1$'s write of $[1,1]$ into $R_1$ \emph{before} $p_0$'s write of $[0,1]$ into $R_1$,
	and so processes $p_2, p_3, \ldots, p_{n-1}$ have $u_1 = [c,1]=[1,1]$ and $u_2 = [1-c,1]=[0,1]$ and so they will also complete Phase 1 without existing in line~\ref{exit1}.

\rmv{
as we describe below.

\begin{enumerate}

\item At time $t_2 > t_c$,
		$p_1$ completes its writing of [1,1] into $R_1$ in line~\ref{pwrite1}.

		Note that \emph{both} $p_0$ and $p_1$ have now completed Phase 1 of round $j=1$.

\item The adversary $\mathcal{S}$ linearizes the write of $[1,1]$ into $R_1$ by $p_1$
	\emph{before} the write of $[0,1]$ into $R_1$ by~$p_0$.

\item Note that $p_2, p_3, \ldots, p_{n-1}$ are still reading $R_1$ in line~\ref{u1}.
Now the adversary linearizes these read operations \emph{between}
	the above write of $[1,1]$ by~$p_1$
	and the write of $[0,1]$ by~$p_0$.

\item At time $t_3 > t_2$,
		$\textrm{processes } p_2, p_3, \ldots, p_{n-1}$ complete their read of $R_1$ in line~\ref{u1}.
By the above linearization, they read $[1,1]$, and so they set (their local variable) $u_1 = [1,1]$ in line~\ref{u1}.

\item Then $\textrm{processes } p_2, p_3, \ldots, p_{n-1}$ start and complete their read of $R_1$ in line~\ref{u2}.
Since (1)~these reads start \emph{after} the time $t_1$ when $p_0$ completed its write of $[0,1]$ into $R_1$,
	and (2)~this write is linearized \emph{after} the write of $[1,1]$ by $p_1$ into $R_1$,
	$\textrm{processes } p_2, p_3, \ldots, p_{n-1}$ read~$[0,1]$.
So they all set (their local variable) $u_2 = [0,1]$ in line~\ref{u2}.
Let $t_4 > t_3$ be the time when every process in $\{p_2, p_3, \ldots, p_{n-1}\}$ has set $u_2 = [0,1]$ in line~\ref{u2}.

\item After time $t_4$, $\textrm{processes } p_2, p_3, \ldots, p_{n-1}$ start reading $C$ in line~\ref{rcoin1}.
		Since $C =1$ at time~$t_c$ and it is not modified thereafter,
		$p_2, p_3, \ldots, p_{n-1}$ read $1$ and set (their local variable) $c = 1$ in line~\ref{rcoin1}.

	So at this point, $\textrm{processes } p_2, p_3, \ldots, p_{n-1}$ have $u_1 = [1,1]$, $u_2 = [0,1]$ and $c = 1$.

\item Then $p_2, p_3, \ldots, p_{n-1}$ execute line~\ref{guard0}, and find that
	the condition ($u_1 = \bot$ \textbf{or} $u_2 = \bot$ \textbf{or} $c = \bot$)
	of this line does not hold,
	and so they proceed to execute line~~\ref{guard1}.

\item When $p_2, p_3, \ldots, p_{n-1}$ execute line~\ref{guard1}, they find that the condition ($u_1 \neq [c,j]$ \textbf{or}  $u_2 \neq [1-c,j]$)
	of this line does \emph{not} hold, because they have $u_1 = [c,1] = [1,1]$ and $u_2 = [1- c,1] = [0,1]$.

	   So $p_2, p_3, \ldots, p_{n-1}$ complete Phase 1 of round $j=1$
	   without exiting in line~\ref{exit1}.
	Recall that both $p_0$ and $p_1$ also completed Phase 1 of round $j=1$ without exiting.

\end{enumerate}
}

Thus in both Case 1 and Case 2, all the $n$ processes complete Phase 1 of round $j=1$ without exiting,
	and are now poised to execute Phase 2 of this round.
The adversary $\mathcal{S}$ extends the run that it built so far as follows (Figure~\ref{toy2}).

\end{enumerate}

\begin{figure}[!htb]
   		 \centering
    		\includegraphics[width=0.5\textwidth]{sg/toy-algo2.pdf}
   		 \caption{Phase 2 in round $j=1$ of an infinite execution}
   		 \label{toy2}
\end{figure}

\noindent
\textbf{Phase 2} (of round $j=1$):

\begin{enumerate}

\item Processes $p_0$ and $p_1$ write $0$ into $R_2$ in line~\ref{cleanr2},
	and processes $p_2, p_3, \ldots, p_{n-1}$ write $0$ into $R_2$ in line~\ref{cleanr2-2}.

\item After all the above write operations complete,
	$\textrm{processes } p_2, p_3, \ldots, p_{n-1}$ successively read and increment $R_2$
	by executing lines~\ref{pread2}--\ref{pwrite2}

	in the following order:
	$p_2$ executes lines~\ref{pread2}--\ref{pwrite2},
	and then, for  each  \mbox{$i\in \{3, \ldots, n-2\}$},
	process $p_{i+1}$ starts reading $R_2$ in line~\ref{pread2} \emph{after}
	$p_i$ completes its write of $R_2$ in line~\ref{pwrite2}.

Let $t'_0$ be the time when the above $n-2$ write operations by $p_2, p_3, \ldots, p_{n-1}$ have completed.

	Note that at time $t'_0$: (i) register $R_2$ contains $n-2$, and
	(ii) all $\textrm{processes } p_2, p_3, \ldots, p_{n-1}$ have completed~Phase~2 of round $j=1$.

\item After time $t'_0$, $p_0$ and $p_1$ read $R_2$ into $v$ in line~\ref{v1},
	and so they set $v =  n-2$ in that line.

\item Then $p_0$ and $p_1$ execute line~\ref{guard2}
	and find that the condition ``$v <  n-2$'' of this line does \emph{not} hold.
         So $p_0$ and $p_1$ complete Phase 2 of round $j=1$
	 without exiting in line~\ref{exit2}.

Thus all the $n$ processes $p_0, p_1, \ldots, p_{n-1}$,
	have completed Phase 2 of round $1$ without exiting;
	they are now poised to execute round $j=2$.

\end{enumerate}

\noindent
The adversary $\mathcal{S}$ continues to build the run
	by repeating the above scheduling of $p_0, p_1, \ldots, p_{n-1}$ for rounds $j=2,3 \ldots$.
This gives a non-terminating run of Algorithm~\ref{toyalgo} with \mbox{probability~1:}
	in this run,
	all processes are correct, i.e., they take an infinite number of steps, but they loop forever
	and never reach the return statement in lines~\ref{halt0} or line~\ref{halt1}.
\end{proof}

\subsection{Write strong-linearizability ensures termination}\label{wsltoysection}

\rmv
\noindent
We now show that if registers $R_1$, $R_2$, and $C$ are $\textrm{write strongly-linearizable}$,
	Algorithm~\ref{toyalgo} terminates with \mbox{probability~1} even against a strong adversary.
To prove this, we first show four lemmas (Lemmas~\ref{prev-reads}--\ref{C-non-bot}) about some safety properties of Algorithm~\ref{toyalgo}.
Specifically, Lemma~\ref{bigarestuck} and~\ref{smallarestuck}
	state that processes $p_0$ and $p_1$ on one side,
	and processes $p_2, p_3, \ldots, p_{n-1}$ on the other side,
	remain within one round of each other.
Lemma~\ref{prev-reads} and~\ref{C-non-bot}
	state that the non-$\bot$ values that $p_2, p_3, \ldots, p_{n-1}$ read from registers $R_1$ and $C$ in any round $j$
	were also written in~round~$j$.
The proofs of Lemmas~\ref{prev-reads}--\ref{C-non-bot} require only linearizability and they are shown in in Appendix~\ref{a1}.

In the following lemmas, we say that a process ``enters round $r \ge 1$'' if it executes line~\ref{enter1} or \ref{enter2} with $j =r$.

\begin{restatable}{lemma}{safetyone}\label{prev-reads}
For all $j\ge1$,
	if $p_i \in \{ p_2, p_3, \ldots, p_{n-1} \}$ $\textrm{reaches}$ line~\ref{cleanr2-2} in round $j$,
	then
	$p_i$ previously read both $[b,j]$ and $[1-b,j]$ for some
	$b \in \{0, 1\}$ from register $R_1$ in lines~\ref{u1} and~\ref{u2} in round $j$.
\end{restatable}

\begin{restatable}{lemma}{safetytwo}\label{bigarestuck}
For all $j\ge1$,
	if $p_i \in \{ p_2, p_3, \ldots, p_{n-1} \}$ $\textrm{reaches}$ line~\ref{cleanr2-2} in round $j$, then $p_0$ and $p_1$ previously entered round $j$.
\end{restatable}

\begin{restatable}{lemma}{safetythree}\label{smallarestuck}
For all $j\ge1$,
	if $p_0$ or $p_1$ enters round $j+1$, then every $p_i \in \{ p_2, p_3, \ldots, p_{n-1} \}$ previously reached line 37 in round $j$.
\end{restatable}

\begin{restatable}{lemma}{safetyfour}\label{C-non-bot}
For all $j\ge1$,
	if $p_i \in \{ p_2, p_3, \ldots, p_{n-1} \}$ $\textrm{reaches}$ line~\ref{guard1} in round $j$,
	then in that line $p_i$ has $c=b$ such that $b \in \{0,1\}$ and
	$p_0$ wrote $b$ into register $C$ in line~\ref{pcoin1-2} in round $j$.
\end{restatable}

We now prove that if registers $R_1$, $R_2$, and $C$ are $\textrm{write strongly-linearizable}$,
	then Algorithm~\ref{toyalgo} terminates with \mbox{probability~1}
	even against a strong adversary (Theorem~\ref{WSLinearizableIsStrong}).
Intuitively,
	this is because if $R_1$, $R_2$, and $C$ are $\textrm{write strongly-linearizable}$,
	then the order in which $[0,j]$ and $[1,j]$ are written into $R_1$ in line~\ref{pwrite1} in round $j$ is already \emph{fixed}
	before the adversary $\mathcal{S}$ can see the result of the coin flip in line~\ref{pcoin1-1} in round $j$.
So for every round $j\ge 1$,
	the adversary can\emph{not} ``retroactively'' decide on this linearization order of write operations\MP{write-linearization?}
	according to the coin flip result
	(like it did when $R_1$ was merely linearizable)
	to ensure that
	processes $p_1, p_2,...,p_{n-1}$ do not exit by the condition of line~\ref{guard1}.
Thus, with probability 1/2, all these processes will exit in line~\ref{exit1}.
And if they all exit there, then no process will increment register $R_2$ in lines~\ref{pread2}-\ref{pwrite2},
	and so $p_0$ and $p_1$ will also exit.

The proof of Theorem~\ref{WSLinearizableIsStrong} is based on the following:

\begin{lemma}\label{exitchance}
For all rounds $j \ge1$,
	with probability at least $1/2$,
	no process enters round $j+1$.
\end{lemma}

\begin{proof}
Consider any round $j\ge1$.
There are two cases:

\begin{enumerate}[(I)]
\item\label{noRwrite} \textbf{Process $p_0$ does not complete its write of $[0,j]$ into register $R_1$ in line~\ref{pwrite1} in round $j$.}

Thus, $p_0$ does not invoke the write of any value into $C$ in line~\ref{pcoin1-2} in round $j$ (*).

\begin{claim}\label{allarestuck-det}
No process enters round $j+1$.
\end{claim}

\begin{proof}
We first show that no process in $\{ p_2, p_3, \ldots, p_{n-1} \}$ $\textrm{reaches}$ line~\ref{pwrite2} in round $j$.
To see why, suppose, for contradiction,
	some process $p_i$ with $i\in\{2,3,...,n-1\}$
	$\textrm{reaches}$ line~\ref{pwrite2} in round $j$.
By Lemma~\ref{C-non-bot},
	in that line $p_i$ has $c=b \in \{0,1\}$ such that
	$p_0$ invoked the write of $b$ into $C$ in line~\ref{pcoin1-2} in round $j$ --- a contradiction to (*).

Thus no process in $\{ p_2, p_3, \ldots, p_{n-1} \}$ $\textrm{reaches}$ line~\ref{pwrite2} in round $j$.
By Lemma~\ref{smallarestuck}, neither $p_0$ nor $p_1$ enters round~$j+1$.
\end{proof}

\item\label{Rwrite} \textbf{Process $p_0$ completes its write of $[0,j]$ into register $R_1$ in line~\ref{pwrite1} in round $j$.}

\begin{claim}\label{allarestuck-rndm}
With probability at least 1/2, no process enters round $j+1$.
\end{claim}

\begin{proof}
Consider the set of histories $\mathcal{H}$ of Algorithm~\ref{toyalgo}; this is a set of histories over
	the registers $R_1$, $R_2$, $C$.
Since these registers are $\textrm{write strongly-linearizable}$,
	by Lemma 4.8 of~\cite{sl11}, $\mathcal{H}$~is~$\textrm{write strongly-linearizable}$, i.e., it has
	at least one $\str$ function
	that satisfies properties (L) and (P) of Definition~\ref{defwsl}.
Let $f$ be the $\str$ function that
	the~adversary~$\mathcal{S}$~uses.

Let $g$ be an arbitrary history of the algorithm up to
	and including the completion of the write of $[0,j]$ into $R_1$
	by $p_0$ in line~\ref{pwrite1} in round $j$.
Since $p_0$ completes its write of $[0,j]$ into $R_1$ in $g$,
	this write operation appears in the $\str$ $f(g)$.
Now there are two cases:

\begin{itemize}
\item\label{Casino1} \textbf{Case A}:
In $f(g)$, the write of $[1,j]$ into $R_1$ by $p_1$ in line~\ref{pwrite1} in round $j$
	occurs \emph{before}
	the write of $[0,j]$ into $R_1$ by $p_0$ in line~\ref{pwrite1} in round $j$.

Since $f$ is a $\str$ function,
	for every extension $h$ of the history $g$
	(i.e., for every history $h$ such that $g$ is a prefix of $h$),
	the write of $[1,j]$ into $R_1$
	occurs before
	the write of $[0,j]$ into $R_1$
	in the linearization $f(h)$
	(note that for all $j\ge1$, each of $[1,j]$ and $[0,j]$ is written \emph{at most once} in $R_1$, so it appears at most once in $h$ and $f(h)$).
Thus, in $g$ and every extension $h$ of $g$,
	no process can first read $[0,j]$ from $R_1$ and then read $[1,j]$ from $R_1$ ($\star$).

Let $\mathcal{P}$ be the subset of processes in $\{p_2 , p_3, \ldots , p_{n-1} \}$
	that

	evaluate the condition
	($u_1 \neq [c,j]$ \textbf{or}  $u_2 \neq [1-c,j]$)
	in line~\ref{guard1} in round $j$.
Note that for each process $p_i$ in $\mathcal{P}$,
	$u_1$ and $u_2$ are the values that $p_i$ read from $R_1$
	consecutively in lines~\ref{u1} and \ref{u2} in round $j$.
By~($\star$), $p_i$ cannot first read $u_1=[0,j]$ and then read $u_2=[1,j]$ from $R_1$.
Thus, no process $p_i$ in $\mathcal{P}$ can have both $u_1=[0,j]$ and $u_2=[1,j]$ in line~\ref{guard1} in round $j$ ($\star \star$).

Let $\mathcal{P' \subseteq P}$ be the subset of processes in $\mathcal{P}$
	that have $c = 0$
	in line~\ref{guard1} in round $j$.

\begin{cclaim}\label{Mannaggia1}
~
\begin{enumerate}[(a)]
\item\label{SC1} No process in $\mathcal{P'}$ $\textrm{reaches}$ line~\ref{pwrite2} in round $j$.
\item\label{SC2} If $\mathcal{P'} = \mathcal{P}$ then neither $p_0$ nor $p_1$ enters round $j+1$.
\end{enumerate}
\end{cclaim}

\begin{proof}
To see why Part~\ref{SC1} holds, note that no process $p_i$ in $\mathcal{P'}$
	can find the condition~($u_1 \neq [c,j]$ \textbf{or}  $u_2 \neq [1-c,j]$) in line~\ref{guard1} in round $j$
	to be false: otherwise $p_i$ would have both $u_1 = [c,j] = [0,j]$ \textbf{and} $u_2 = [1-c,j] = [1,j]$ in that line,
	but this is not possible by ($\star \star$).
Thus, no process in $\mathcal{P'}$ $\textrm{reaches}$ line~\ref{pwrite2} in round $j$
	(it would exit in line~\ref{exit1} before reaching that line).

To see why Part~\ref{SC2} holds, suppose $\mathcal{P'} = \mathcal{P}$
	and consider any process $p_i$ in $\{ p_2, p_3, \ldots, p_{n-1} \}$.
If $p_i \not \in \mathcal{P}$
	then $p_i$ never evaluates the condition
	in line~\ref{guard1} in round $j$;
	and if $p_i \in \mathcal{P}$, then $p_i \in \mathcal{P'}$, and so from Part~\ref{SC1},
	$p_i$ does not $\textrm{reach}$ line~\ref{pwrite2} in round $j$.
So \emph{in both cases},
	$p_i$ does not $\textrm{reach}$ line~\ref{pwrite2} in round $j$.
Thus, by Lemma~\ref{smallarestuck}, neither $p_0$ nor $p_1$ enters round $j+1$.
\end{proof}

Now recall that $g$ is the history of the algorithm up to
	and including the completion of the write of $[0,j]$ into $R_1$
	by $p_0$ in line~\ref{pwrite1} in round $j$.
After the completion of this write, i.e., in any extension $h$ of $g$,
	$p_0$ is supposed to flip a coin and write the result into $C$ in line~\ref{pcoin1-2} in round~$j$.
Thus, with probability \emph{at least}~$1/2$,
	$p_0$~will \emph{not} invoke
	the operation to write $1$ into $C$ in line~\ref{pcoin1-2} in round~$j$.\MP{The adversary may decide to kill $p_0$
	before he flips a coin or before the write of $C$ in round $j$, or even after $p_0$ invokes the write  of $C$ in round $j$
	but before completing the write.}
So, from Lemma~\ref{C-non-bot},
	with probability \emph{at least}~$1/2$,
	every process in $\mathcal{P}$ has $c = 0$
	in line~\ref{guard1} in round $j$;
	this means that
        with probability at least~$1/2$,
	$\mathcal{P' = P}$.
Therefore, from Claim~\ref{Mannaggia1}, with probability at least~$1/2$:
\begin{enumerate}[(a)]
\item No process in $\mathcal{P}$ $\textrm{reaches}$ line~\ref{pwrite2} in round $j$.
\item Neither $p_0$ nor $p_1$ enters round $j+1$.
\end{enumerate}
This implies that in Case~A, with probability at least~$1/2$,
	no process enters round $j+1$.

\item\label{Casino2} \textbf{Case B}:
In $f(g)$, the write of $[1,j]$ into $R_1$ by $p_1$ in line~\ref{pwrite1} in round $j$
	does \emph{not} occur before
	the write of $[0,j]$ into $R_1$ by $p_0$ in line~\ref{pwrite1} in round $j$.
This case is essentially symmetric to the one for Case A, we include it below for completeness.

Since $f$ is a $\str$ function,
	for every extension $h$ of the history $g$,
	the write of $[1,j]$ into $R_1$
	does not occur before
	the write of $[0,j]$ into $R_1$
	in the linearization $f(h)$.
Thus, in $g$ and every extension $h$ of $g$,
	no process can first read $[1,j]$ from $R_1$ and then read $[0,j]$ from $R_1$ ($\dagger$).

Let $\mathcal{P}$ be the subset of processes in $\{p_2 , p_3, \ldots , p_{n-1} \}$
	that

	evaluate the condition
	($u_1 \neq [c,j]$ \textbf{or}  $u_2 \neq [1-c,j]$)
	in line~\ref{guard1} in round $j$.
Note that for each process $p_i$ in $\mathcal{P}$,
	$u_1$ and $u_2$ are the values that $p_i$ read from $R_1$
	consecutively in lines~\ref{u1} and \ref{u2} in round $j$.
By~($\dagger$), $p_i$ cannot first read $u_1=[1,j]$ and then read $u_2=[0,j]$ from $R_1$.
Thus, no process $p_i$ in $\mathcal{P}$ can have both $u_1=[1,j]$ and $u_2=[0,j]$ in line~\ref{guard1} in round $j$ ($\dagger \dagger$).

Let $\mathcal{P' \subseteq P}$ be the subset of processes in $\mathcal{P}$
	that have $c = 1$
	in line~\ref{guard1} in round $j$.

\begin{cclaim}\label{Mannaggia2}
~
\begin{enumerate}[(a)]
\item\label{SC21} No process in $\mathcal{P'}$ $\textrm{reaches}$ line~\ref{pwrite2} in round $j$.
\item\label{SC22} If $\mathcal{P'} = \mathcal{P}$ then neither $p_0$ nor $p_1$ enters round $j+1$.
\end{enumerate}
\end{cclaim}

\begin{proof}
To see why \ref{SC21} holds, note that no process $p_i$ in $\mathcal{P'}$
	can find the condition ($u_1 \neq [c,j]$ \textbf{or}  $u_2 \neq [1-c,j]$) in line~\ref{guard1} in round $j$
	to be false: otherwise $p_i$ would have both $u_1 = [c,j] = [1,j]$ \textbf{and} $u_2 = [1-c,j] = [0,j]$ in that line,
	but this is not possible by ($\dagger \dagger$).
Thus, no process in $\mathcal{P'}$ $\textrm{reaches}$ line~\ref{pwrite2} in round $j$
	(it would exit in line~\ref{exit1} before reaching that line).

To see why \ref{SC2} holds, suppose $\mathcal{P'} = \mathcal{P}$
	and consider any process $p_i$ in $\{ p_2, p_3, \ldots, p_{n-1} \}$.
If $p_i \not \in \mathcal{P}$
	then $p_i$ never evaluates the condition
	in line~\ref{guard1} in round $j$;
	and if $p_i \in \mathcal{P}$, then $p_i \in \mathcal{P'}$, and so from \ref{SC21},
	$p_i$ does not $\textrm{reach}$ line~\ref{pwrite2} in round $j$.
So \emph{in both cases},
	$p_i$ does not $\textrm{reach}$ line~\ref{pwrite2} in round $j$.
Thus, by Lemma~\ref{smallarestuck}, neither $p_0$ nor $p_1$ enters round $j+1$.
\end{proof}

Now recall that $g$ is the history of the algorithm up to
	and including the completion of the write of $[0,j]$ into $R_1$
	by $p_0$ in line~\ref{pwrite1} in round $j$.
After the completion of this write, i.e., in any extension $h$ of $g$,
	$p_0$ is supposed to flip a coin and write the result into $C$ in line~\ref{pcoin1-2} in round~$j$.
Thus, with probability \emph{at least}~$1/2$,
	$p_0$~will \emph{not} invoke
	the operation to write $0$ into $C$ in line~\ref{pcoin1-2} in round~$j$.
So, from Lemma~\ref{C-non-bot},
	with probability \emph{at least}~$1/2$,
	every process in $\mathcal{P}$ has $c = 1$
	in line~\ref{guard1} in round $j$;
	this means that
        with probability at least~$1/2$,
	$\mathcal{P' = P}$.
Therefore, from Claim~\ref{Mannaggia2}, with probability at least~$1/2$:
\begin{enumerate}[(a)]
\item No process in $\mathcal{P}$ $\textrm{reaches}$ line~\ref{pwrite2} in round $j$.
\item Neither $p_0$ nor $p_1$ enters round $j+1$.
\end{enumerate}
This implies that in Case~B, with probability at least~$1/2$,
	no process enters round $j+1$.
\end{itemize}

So in both Cases A and B, with probability at least 1/2, no process enters round $j+1$.
\end{proof}
\end{enumerate}

\noindent
Therefore, from Claims~\ref{allarestuck-det} and~\ref{allarestuck-rndm} of Cases~\ref{noRwrite} and~\ref{Rwrite},
	with probability at least $1/2$,
	no process enters round $j+1$.
\end{proof}

\noindent
We can now complete the proof of Theorem~\ref{WSLinearizableIsStrong},
	namely, that with $\textrm{write strongly-linearizable}$ registers,
	Algorithm~\ref{toyalgo} terminates with probability 1 in expected $2$ rounds, even against a strong adversary.

In Appendix~\ref{toyterminatewithwsl}, we prove:

\begin{restatable}{theorem}{toyterminate}\label{WSLinearizableIsStrong}
If registers $R_1$, $R_2$, and $C$ are $\textrm{write strongly-linearizable}$,
	 then Algorithm~\ref{toyalgo} terminates with probability 1 against a strong adversary.

	 \MP{Expected 2 rounds?}
\end{restatable}

Combining Theorems~\ref{LinearizableIsWeak} and ~\ref{WSLinearizableIsStrong},
	we have:
\begin{corollary}\label{smallbob}
If $R_1$, $R_2$, and $C$ are
\begin{enumerate}
\item  only linearizable,
    then a strong adversary can prevent the termination~of~Algorithm~\ref{toyalgo};

\item $\textrm{write strongly-linearizable}$,
    then Algorithm~\ref{toyalgo} terminates with probability 1 against a strong adversary.

\end{enumerate}
\end{corollary}

\rmv{
\begin{proof}
Consider any round $j \ge 1$.
By Lemma~\ref{exitchance},
	with probability at least $1/2$,
	no process enters round $j+1$.
Since this holds for every round $j \ge 1$,
	then, with probability 1,
	all the correct processes
	return in lines~\ref{halt0} or line~\ref{halt1}
	within a finite number of rounds $r$,
	and the expected value of $r$ is 2.
\end{proof}

}

Consider any randomized algorithm $\mathcal{A}$ that solves some task $T$,
	such as consensus,
	for $n \ge 3$ processes $p_0, p_1, p_2, \ldots, p_{n-1}$,
	and terminates with probability 1 against a strong adversary.
Using $\mathcal{A}$, we can construct a corresponding randomized algorithm $\mathcal{A}'$ as follows:
	every process $p_i$ with $i\in\{0,1,2,...,n-1\}$
	first executes Algorithm~\ref{toyalgo};
	if~$p_i$ returns then it executes algorithm~$\mathcal{A}$.
From Corollary~\ref{smallbob} we have:

\begin{corollary}\label{bigbob}
Let $\mathcal{A}$ be any randomized algorithm that solves a task $T$
	for $n \ge 3$ processes and terminates with probability~1 against a strong adversary.
There is a corresponding randomized algorithm $\mathcal{A}'$
	that solves $T$ for $n \ge 3$ processes such that:

\begin{enumerate}

\item $\mathcal{A}'$ uses a set $\mathcal{R}$ of three shared registers
	in addition to the set of base objects of $\mathcal{A}$.

\item If the registers in $\mathcal{R}$ are only linearizable,
    then a strong adversary can prevent the termination~of~$\mathcal{A}'$.

\item If the registers in $\mathcal{R}$ are $\textrm{write strongly-linearizable}$,
    then $\mathcal{A}'$ terminates with probability 1 against a strong adversary.\footnote{$\mathcal{A}'$ also terminates if the registers in $\mathcal{R}$ are atomic, because atomic registers are $\textrm{write strongly-linearizable}$.}

\end{enumerate}
\end{corollary}

\rmv{
\begin{proof}
Consider any randomized algorithm $\mathcal{A}$ that solves some task $T$
	for $n \ge 3$ processes $p_0, p_1, p_2, \ldots, p_{n-1}$,
	and terminates with probability 1 even against a strong adversary.
Using $\mathcal{A}$, we construct the following randomized algorithm $\mathcal{A}'$ (see Figure~\ref{toy3}):
	every process $p_i$ with $i\in\{0,1,2,...,n-1\}$
	first executes Algorithm~\ref{toyalgo};
	if $p_i$ returns then it executes algorithm $\mathcal{A}$.
Note that:

\begin{enumerate}

\item In addition to the set of base objects that $\mathcal{A}$ uses,
	the algorithm $\mathcal{A}'$ uses the set of shared registers ${\mathcal{R}} = \{R_1, R_2, C \}$.

\item Suppose registers in $\mathcal{R}$ are $\textrm{write strongly-linearizable}$.
	Then, by Theorem~\ref{WSLinearizableIsStrong},
	Algorithm~\ref{toyalgo} (that processes execute before executing $\mathcal{A}$)
	terminates with probability 1

	against a strong adversary.
	Since $\mathcal{A}$ also terminates with probability 1 against a strong adversary,
	the algorithm $\mathcal{A}'$ terminates with probability 1 against a strong adversary,
	and the expected running time of $\mathcal{A}'$ is only a constant
        more than the expected running time of the given algorithm $\mathcal{A}$.

	Since $\mathcal{A}$ solves task $T$, it is clear that $\mathcal{A}'$ also solves $T$.

\item Suppose registers in $\mathcal{R}$ are linearizable but not $\textrm{write strongly-linearizable}$.
	Then, by Theorem~\ref{LinearizableIsWeak},
	a~strong adversary can construct a run of Algorithm~\ref{toyalgo} where, with probability~$1$,
	all the processes execute
	infinitely many rounds and never return.
	Thus, since $\mathcal{A}'$ starts by executing Algorithm~\ref{toyalgo},
	it is clear that a strong adversary can prevent the termination of $\mathcal{A}'$ \emph{with probability 1}.
\end{enumerate}
\end{proof}

}

\section{Implementing write strongly-linearizable MWMR registers from SWMR registers}\label{sectionwslalgo}

To implement a write strongly-linearizable MWMR register $\textbf{R}$,
	we must be able to linearize all the write operations ``on-line''
	without looking at what may happen in the future.
The challenge is that at the moment $t$ a write operation $w$ completes,
	for each write $w'$ that is concurrent with $w$ and is still pending at time $t$,
	we must have enough information to \emph{irrevocably} decide
	whether $w'$ should be linearized before or after $w$;
	of course this linearization order must be consistent with the values that
	processes previously read and will read in the future from $\textbf{R}$.
Using simple ``Lamport clocks'' to timestamp and linearize write operations does not seem to work:
	in the next section, we give an implementation showing that Lamport clocks
	are sufficient to implement a linerizable MWMR register,
	but this implementation is \emph{not} $\textrm{write strongly-linearizable}$.

In this section we give an implementation of a MWMR register
	from SWMR registers ($\textrm{Algorithm}~\ref{wsl}$), and prove that it is write strongly-linearizable.
This is a modification of an implementation given in~\cite{swlamport}
	and it uses vector clocks to timestamp write operations.
The question is how to use vector timestamps to linearize write operations \emph{on-line}.
Specifically, at the moment $t$ a write operation $w$ completes,

	for each operation $w'$ that is concurrent with $w$ and still pending at time $t$,
	how do we decide the order of $w'$ with respect to $w$?
Note that at time $t$, while the vector timestamp of $w$ is known,
	the vector timestamp of such $w'$ may not be known:
	it is still being computed (it may be incomplete with just a few entries set).
The proof of linearization given in~\cite{swlamport} does not work here:
	that proof can linearize all the write operations after seeing their \emph{complete} vector timestamps;
	and it can do so because linearization is done ``off-line''.

$\textrm{Algorithm}~\ref{wsl}$ uses SWMR registers $Val[i]$ for $i=1,2,...,n$.
Each write operation $w$ is timestamped with a vector timestamp;
	roughly speaking, this represents the number of write operations that every
	process performed ``causally before'' $w$.
Each $Val[k]$ contains the latest value that $p_k$ wrote to $\textbf{R}$
	with its corresponding vector timestamp.
To write a value $v$ into $\textbf{R}$,
	a process $p_k$ first constructs a new timestamp $\textit{new\_ts}$, incrementally one component at a time,
	by successively reading $Val[1], \ldots, Val[n]$ (lines~\ref{timestampb}--\ref{timestampe});
	then $p_k$ writes the tuple $(v,\textit{new\_ts})$ into $Val[k]$ (line~\ref{write});
	finally $p_k$ resets its $\textit{new\_ts}$ to $[ \infty, \ldots, \infty]$ (as we will see,
	this is important for the $\str$).
To read $\textbf{R}$,
	a process $p$ first reads all $Val[-]$ (lines~\ref{collecttsb}--\ref{collecttse});
	then $r$ returns the value $v$ with the greatest vector timestamp in \emph{lexicographic order $\le$}
	(lines~\ref{max}--\ref{readreturn}).
Note that this is a total order.

We now prove that this MWMR implementation is indeed $\textrm{write strongly-linearizable}$.
Before we do so, we first illustrate the problem that we mentioned earlier,
	namely, how to linearize write operations on-line based on incomplete vector timestamps,
	and then we give some intuition on how this problem is solved.

\begin{algorithm}[!h]
\caption{Implementing a $\textrm{write strongly-linearizable}$ MWMR register $\textbf{R}$ from SWMR registers}
\begin{flushleft}
\textsc{Shared Object:}

For $i=1,2,...,n$:

$Val[i]$: SWMR register that contains a tuple $(v,ts)$ where $v$ is a value and $ts$ is a vector timestamp;

\hspace*{0.95cm}initialized to $( 0,[0\ldots0] )$ where $0$ is the initial value of $\textbf{R}$ and  $[0\ldots0]$ is an array of length $n$.

\vspace{0.2cm}

\textsc{Local Object:}

$new\_ts$: For each process, a local array of length $n$;
	initialized to $[\infty, \ldots, \infty]$.
\end{flushleft}
\vspace{0.05cm}
\begin{algorithmic}[1]
\STATEx
When writer $p_k$ writes $v$ to $\textbf{R}$:  \hfill // $1\le k \le n$

\FOR{$i = 1$ to $n$} \label{timestampb}

	\IF{$i\ne k$}

	\STATE \label{ts1} $\textit{new\_ts}[i] \gets (Val[i].ts)[i]$ \hfill // $Val[i].ts$ is the vector timestamp of the tuple in $Val[i]$
		\ELSE

	\STATE \label{ts2} $\textit{new\_ts}[i] \gets (Val[i].ts)[i]+1$
	\ENDIF

\ENDFOR\label{timestampe}

\STATE $Val[k] \gets (v,\textit{new\_ts})$ \hfill // write to shared register \label{write}
\STATE $ \textit{new\_ts} \gets [ \infty, \ldots, \infty]$
\STATE \label{wreturn}\textbf{return} done
\newline

\STATEx When a process reads from $\textbf{R}$:

\FOR{$i = 1$ to $n$}\label{collecttsb}

	\STATE $(v_i,ts_i)\gets Val[i]$\label{readall}
\ENDFOR\label{collecttse}

\STATE let $j$ be such that $ts_j = \max \{ts_1,...,ts_n\}$ \label{max}  \hfill // lexicographic max

\STATE \textbf{return} $(v_j,ts_j)$\label{readreturn}
\end{algorithmic}\label{wsl}
\end{algorithm}

Consider a write operation $w_2$ that finishes at time $t$,
	as illustrated in Figure~\ref{diff1}.
For each write operation that is active at time $t$
	we must decide whether it should be linearized
	before or after $w_2$.
We cannot treat all such operations in the same way:
	we cannot simply linearize all of them before
	or all of them after $w_2$.
This is because the linearization order of these write operations
	depends on their timestamps
	(so as to respect the order of the read operations
	that read their values),
	which may not yet be fully formed at time $t$.
Indeed, the timestamp of a write operation active at $t$
	may end up being greater than, or smaller than,
	the timestamp of $w_2$.
For example, in Figure~\ref{diff1}
	the timestamps eventually computed
	by the write operations $w_1$ and $w_3$,
	which are active at time $t$,
	end up being, respectively,
	greater than and smaller than the timestamp of $w_2$.
As we will see, by looking carefully at the progress
	that each of $w_1$ and $w_3$ has made by time $t$
	towards computing its vector timestamp,
	we can determine, \emph{at time $t$},
	the correct linearization order of
	$w_1$ and $w_3$ relative to $w_2$.
We do so by
	(a) initializing the timestamp of each write to $[ \infty, \ldots, \infty]$
	(so it gets smaller and smaller while it is being formed); and
	(b) ordering the writes by comparing their (possibly incomplete) timestamps
	in lexicographical order.
This makes it possible to linearize the write operations on-line.

\begin{figure}[!h]
\centering
\includegraphics[width=0.7\textwidth]{sg/diff1}
  \caption{Three concurrent writes under $\textrm{Algorithm}~\ref{wsl}$}
  \label{diff1}
\end{figure}

\begin{algorithm}[!htb]
\caption{A $\str$ function $f$ for the set of histories $\mathcal{H}$ of $\textrm{Algorithm}~\ref{wsl}$}
\begin{flushleft}
\textbf{Input:} a history $H \in \mathcal{H}$

\textbf{Output:} $\seq{}$, a sequential history of the operations in $H$
\end{flushleft}
\vspace{0.1cm}
\begin{algorithmic}[1]
\STATEx linearization of write operations in $H$
\STATE \label{seq0}$\wseq{0} \leftarrow()$
\STATE $m \gets$ the number of operations that write to $Val[-]$ in $H$    \hfill//{ $m$ can be $\infty$}
\FOR{$i = 1, 2, \ldots,m$}\label{findleader1}

\STATE \label{findleader2} $t_i \gets$ the time of the $i$th write to a register $Val[-]$ in $H$ (line~\ref{write} of $\textrm{Algorithm}~\ref{wsl}$)

\STATE \label{findleader3} $w_i \gets$ the operation that writes to $Val[-]$ at time $t_i$

\IF{$w_i \notin \wseq{i-1}$}\label{line13} \label{findleader4}

\STATE\label{C} $\sC{i} \leftarrow \{ w~|~w \text{ is a write operation such that } w \notin \wseq{i-1}  \text{ and } w \text{ is active at time } t_i \text{ in } H\}$

\STATE \label{newts} $\forall w\in \sC{i}$,
	$\pts{w}{i}\gets \text{the value of $\textit{new\_ts}$,
	 at time $t_i$}$,
	 of the process executing $w$

\STATE \label{Bt} $\B{i} \leftarrow \{w~|~w\in \sC{i} \text{ and } \pts{w}{i} \le \pts{w_i}{i}\}$
\STATE \label{seqi1} $\wseq{i} \gets \wseq{i-1}\circ (\text{the sequence of operations $w \in \B{i}$ in increasing order of $\pts{w}{i}$)}$

\ELSE
\STATE $\sC{i} \leftarrow \emptyset$; $\B{i} \leftarrow \emptyset$
\STATE \label{seqi2}$\wseq{i} \gets \wseq{i-1}$
\ENDIF
\ENDFOR

\IF{$m = \infty$}
\STATE \label{wseq1}$\wseq{} \gets \lim_{i\rightarrow \infty} \wseq{i}$
\ELSE
\STATE \label{wseq2}$\wseq{} \gets \wseq{m}$
\ENDIF

\smallskip

\STATEx linearization of read operations in $H$
\STATE $\seq{}' \gets \wseq{}$
\FOR{every value $(v,ts)$ that processes read in $H$}\label{fmapread}
\STATE \label{R} $\mathcal{R} \leftarrow \{ r~|~r \text{ is a read operation that returns $(v,ts)$ in $H$} \}$
\STATE \label{S} $S_\mathcal{R} \leftarrow$ the sequence of operations in
$\mathcal{R}$ in increasing order of their start time
\IF{$ts=[0,\ldots,0]$} \label{readinit1}
\STATE \label{readinit2} prepend $S_\mathcal{R}$ to $\seq{}'$
\ELSE
\STATE \label{followwrite1} $w \leftarrow$ the operation in $\seq{}'$ that writes $(v,ts)$
\STATE \label{followwrite2} insert $S_\mathcal{R}$ after $w$ and before any subsequent write operation in $\seq{}'$
\ENDIF

\ENDFOR\label{endfmapread}
\STATE $\seq{} \gets \seq{}'$
\end{algorithmic}\label{f}
\end{algorithm}

To prove that the MWMR implementation given by $\textrm{Algorithm}~\ref{wsl}$ is $\textrm{write strongly-linearizable}$,
	we give a $\str$ function $f$ for the set of histories $\mathcal{H}$ of this algorithm.
We describe $f$ as an algorithm ($\textrm{Algorithm}~\ref{f}$)
	that takes as input any finite or infinite history $H \in \mathcal{H}$
	and outputs a sequential history $\seq{}$ that satisfies properties (L) and (P) of Definition~\ref{defwsl}.
Intuitively, $\textrm{Algorithm}~\ref{f}$ linearizes all the write operations \emph{on-line}, as follows.
 It scans the input history $H$ by increasing time;
	 while doing so it maintains a sequence $\wseq{}$ of write operations that it has linearized so far.
When it sees that, at some time $t_i$, a write operation $w_i$ writes to $Val[-]$,
	it first checks whether $w_i$ was already linearized i.e., whether $w_i$ is in $\wseq{}$ (lines~\ref{findleader1}--\ref{findleader4}).
If $w_i$ is not in $\wseq{}$,
	it forms the set $\sC{i}$ of all the write operations that are ``active'' at time $t_i$
	and are not yet in $\wseq{}$ (line~\ref{C}).\footnote{
An operation that starts at time $s$ and completes at time $f$ is \emph{active} at time $t$ if $s \le t \le f$.
}
It then determines the (possibly incomplete) timestamp of each operation in $\sC{i}$ at time $t_i$ (line~\ref{newts});
	note that $w_i$ is in $\sC{i}$ and $w_i$'s timestamp, denoted $\pts{w_i}{i}$, is complete.
Finally, it selects the operations in $\sC{i}$ whose (possibly incomplete) timestamps are smaller than or equal to $\pts{w_i}{i}$ (line~\ref{Bt}),
	and then it appends them to the linearization sequence $\wseq{}$ in increasing timestamp order (line~\ref{seqi1}).
To linearize the read operations, it collects all the read operations that return some value $(v,ts)$,
 	and linearizes them after the write operation that writes $(v,ts)$, in increasing start time order (lines~\ref{fmapread}--\ref{endfmapread}).

Intuitively,
	$\textrm{Algorithm}~\ref{f}$ gives a $\textrm{write strongly-linearizable}$ function $f$ because:
	 (1) by scanning $H$ in increasing time, it linearizes each write operation by the time the operation completes without ``peeking into the future'',
	and (2) it only \emph{appends} write operations to $\wseq{}$, and so it satisfies the ``prefix property'' (P) of Definition~\ref{defwsl}.
In Appendix~\ref{proofwsl},
	we prove that $\textrm{Algorithm}~\ref{f}$ defines a $\str$ function for $\mathcal{H}$ and
	thus show:

\rmv{

In the following,
	we consider an arbitrary history $H \in \mathcal{H}$ of $\textrm{Algorithm}~\ref{wsl}$ and the history $\seq{}=f(H)$ constructed by $\textrm{Algorithm}~\ref{f}$ on input $H$.
We first show $f$ is a linearization function of $\mathcal{H}$,
	i.e., $\seq{}$ satisfies properties~\ref{p1}--\ref{p3} of Definition~\ref{defl}.

\begin{definition}
Let $o$ be an operation that starts at time $s_o$ and completes at time $f_o$ and let $t$ be a time.
We say that $o$ is active at time $t$ if and only if $s_o \le t \le f_o$.
\end{definition}

\begin{definition}\label{tscompare}
Let $a$ and $b$ be two timestamps
then:
\begin{itemize}

\item $a < b$ if and only if $a$ precedes $b$ in lexicographic order.

\item $a \leq b$ if and only if $a = b$ or $a < b$.
\end{itemize}
\end{definition}

\begin{observation}
Relation $\le$ is a total order on the set of timestamps.
\end{observation}

\begin{notation}
Let $w$ be an operation that writes into $Val[-]$.
We denote by $\ts{w}$ the timestamp that $w$ writes into $Val[-]$.
That is, if $w$ writes $(-,ts)$,
	$\ts{w}=ts$.
\end{notation}

\begin{observation}\label{onlyone}
The tuples $(v,ts)$ and $(v',ts')$ written to $Val[-]$ by two distinct write operations have distinct timestamps, i.e.,
	$ts \ne ts'$.
\end{observation}

\begin{observation}\label{a1ob2}
Consider the execution of a write operation (lines~\ref{timestampb}--\ref{wreturn}) by a process $p_k$.
During that execution,
	the values of the variable $\textit{new\_ts}$ of $p_k$ are non-increasing with time.
\end{observation}

\begin{observation}\label{obsreadtime}
		If a read operation returns $(v,ts) \neq (0,[0, \ldots, 0])$\XMP{If a read operation reads $(v,ts)$ such that $ts \neq [0, \ldots, 0]$ ?},
		then there is an operation $w$
		that writes $(v,ts)$ to $Val[-]$.
\end{observation}

\begin{lemma}\label{last}
If a read operations $r$ starts after an operation $w$ writes to $Val[-]$ and $r$ returns $(-,ts)$,
	then $ts \ge \ts{w}$.
\end{lemma}
\begin{proof}
 Assume a read operations $r$ starts after an operation $w$ writes to some $Val[k]$ and $r$ returns $(-,ts)$.
Then $r$ reads $Val[i]$ (line~\ref{readall} of $\textrm{Algorithm}~\ref{wsl}$) for every $1 \le i \le n$ after $w$ writes $(-,\ts{w})$ to $Val[k]$.
Since the timestamps in each $Val[-]$ are monotonically increasing,
	$r$ reads $(-,ts'')$ from $Val[k]$ for some $ts' \ge \ts{w}$.
Since $ts$ is the largest timestamp that $r$ reads among all $Val[-]$ (lines~\ref{max}--\ref{readreturn} of $\textrm{Algorithm}~\ref{wsl}$),
	$ts \ge ts' \ge \ts{w}$.
\end{proof}

\begin{observation}\label{w}
If an operation $w$ writes to $Val[-]$,
		there is an $i\ge 1$ such that
		$w = w_i$.
\end{observation}

\begin{observation}\label{fmapwritex0}
If an operation $w$ writes to $Val[-]$,
		there is a unique $j\ge 1$ such that
		$w \in \B{j}$.
\end{observation}

\begin{observation}\label{leaderofbatch0}
For every write operation $w$,
	$w \in \seq{}$ if and only if
	there is an $i$ such that $w\in \mathcal{B}_i$.
\end{observation}

By Observations~\ref{fmapwritex0} and~\ref{leaderofbatch0}, we have:

\begin{corollary}\label{wwi}
If an operation $w$ writes to $Val[-]$,
	then $w \in \seq{}$.
\end{corollary}

\begin{observation}\label{leaderofbatch1}
For any two write operations $w$ and $w'$,
	if $w\in \mathcal{B}_i$,
	$w' \in \mathcal{B}_j$,
	and $i < j$,
	then $w$ is before $w'$ in $\seq{}$.
\end{observation}

Recall that
	$\pts{w}{i}$ is the value of $\textit{new\_ts}$,
	 at time $t_i$,
	 of the process executing the write operation $w$ (see line~\ref{newts} of $f$).

\begin{observation}\label{leaderofbatch2}
For all $i \ge 1$,
	if $w_i \in \B{i}$
	then $\pts{w_i}{i} = \ts{w_i}$.
\end{observation}

\begin{observation}\label{leaderofbatch3}
For all $i \ge 1$,
	 for all operations $w \in \B{i}$,
	 if $w \ne w_i $
	 then $\pts{w}{i} < \ts{w_i}$.
\end{observation}

By Observation~\ref{a1ob2}, we have:
\begin{observation}\label{leaderofbatch5}
For all $i \ge 1$,
	for all operations $w \in \B{i}$ that write to $Val[-]$,
	 $\ts{w} \le \pts{w}{i}$.
\end{observation}

By Observations~\ref{leaderofbatch3} and \ref{leaderofbatch5}, we have:
\begin{observation}\label{leaderofbatch4}
For all $i \ge 1$,
	for all operations $w \in \B{i}$ that write to $Val[-]$,
	 $\ts{w}  \le  \ts{w_i}$.
\end{observation}

\begin{lemma}\label{later}
For all $i \ge 1$,
	 for all operations $w$ that write to $Val[-]$,
	 if $w \in \sC{i}$ and $w \notin \B{i}$,
	 then $\ts{w} > \ts{w_i}$.\XMP{New lemma says that if $f$ decides not to linearize $w$ by time $t_i$, then $\ts{w} > \ts{w_i}$}
\end{lemma}
\begin{proof}
Let $i \ge 1$ and assume that an operation $w$ writes to $Val[-]$
	such that $w \in \sC{i}$ and $w \notin \B{i}$.
By line~\ref{Bt} of $\textrm{Algorithm}~\ref{f}$,
	$\pts{w}{i} > \pts{w_i}{i}$.
Since by Observation~\ref{leaderofbatch2} $\pts{w_i}{i} = \ts{w_i}$,
	$\pts{w}{i} > \ts{w_i}$ (*).
There are two cases:

\textbf{Case 1:} $\pts{w}{i}$ contains no $\infty$.
This implies $\ts{w} = \pts{w}{i}$.
Thus, by (*),
	$\ts{w} = \pts{w}{i} > \ts{w_i}$.

\textbf{Case 2:} $\pts{w}{i}$ contains $\infty$.
Then there is a $k$ such that for every $k \le l \le n$,
	$w$ reads $(Val[l].ts)[l]$ (lines~\ref{ts1} and~\ref{ts2} of $\textrm{Algorithm}~\ref{wsl}$) after time $t_i$.
Note that $w_i$ reads $(Val[l].ts)[l]$ before time $t_i$ for every $k \le l \le n$,
	and $w_i$ writes $(-,\ts{w_i})$ to some $Val[-]$ at time $t_i$.
Thus,
	for every $k \le l \le n$,
	since $(Val[l].ts)[l]$ is non-decreasing,
	$\ts{w}[l] \ge \ts{w_i}[l]$ ($\dagger$).

For every $1 \le l \le k-1$,
	since $w$ reads $(Val[l].ts)[l]$ before time $t_i$,
	$\ts{w}[l] = \pts{w}{i}[l]$.
By (*),
	 $\pts{w}{i}[1,\ldots, k-1] \ge \ts{w_i}[1,\ldots, k-1]$.
So $\ts{w}[1,\ldots, k-1] \ge \ts{w_i}[1,\ldots, k-1]$ ($\dagger \dagger$).

By ($\dagger$) and ($\dagger \dagger$),
	$\ts{w} \ge \ts{w_i}$.
Since $w \notin \B{i}$,
	$w \ne w_i$.
By Observation~\ref{onlyone},
	$\ts{w} \ne \ts{w_i}$.
Thus, $\ts{w} > \ts{w_i}$.
\end{proof}

\begin{lemma}\label{tsorder}\XMP{intuition of why we can decide the order of writes by seeing the partial new\_ts}
For all $j > i \ge 1$,
	if $w \in \B{i}$,
	$w' \in \B{j}$,
	and $w$ and $w'$ both write to $Val[-]$,
	then $\ts{w'} > \ts{w}$.
\end{lemma}

\begin{proof}
Assume $j > i \ge 1$,
	$w \in \B{i}$,
	$w' \in \B{j}$,
	and $w$ and $w'$ both write to $Val[-]$.

\begin{claim}\label{tsorderc1}
$\ts{w'} > \ts{w_i}$.
\end{claim}

\begin{proof}
Since $w' \in \B{j}$ and $j > i$,
	$w' \notin \B{i}$\XMP{unique $\B{i}$ of Observation~\ref{fmapwritex0}} and $w' \notin \wseq{i}$.
There are two cases:

\textbf{Case 1}:
	$w' \in \sC{i}$.

Since $w' \in \sC{i}$ and $w' \notin \B{i}$,
	by Lemma~\ref{later},
	$\ts{w'} > \ts{w_i}$.
\smallskip

\textbf{Case 2}:
	$w' \notin \sC{i}$.
By lines~\ref{seqi1} and~\ref{seqi2} of $\textrm{Algorithm}~\ref{f}$,
	$\wseq{i-1}$ is a prefix of $\wseq{i}$.
Since $w' \notin \wseq{i}$,
	$w' \notin \wseq{i-1}$.
Since $w' \notin \sC{i}$,
	by line~\ref{C} of $\textrm{Algorithm}~\ref{f}$,
	$w'$ is not active at time $t_i$.
Since $w' \in \B{j} \subseteq \sC{j}$,
 	by line~\ref{C} of $\textrm{Algorithm}~\ref{f}$,
 	$w'$ is active at time $t_j$.
Since $i < j$,
	$t_i < t_j$.
So $w'$ starts after $t_i$
	and $w'$ reads all $(Val[-].ts)[-]$ (lines~\ref{timestampb}--\ref{timestampe} of $\textrm{Algorithm}~\ref{f}$) after $t_i$.
Note that $w_i$ reads $(Val[l].ts)[l]$ before time $t_i$ for every $1 \le l \le n$,
	and $w_i$ writes $(-,\ts{w_i})$ to some $Val[-]$ at time $t_i$.
Thus,
	for every $1 \le l \le n$,
	since $(Val[l].ts)[l]$ is non-decreasing,
	$\ts{w'}[l] \ge \ts{w_i}[l]$.
So $\ts{w'} \ge \ts{w_i}$.
Since $w' \notin \B{i}$,
	$w' \ne w_i$.
By Observation~\ref{onlyone},
	$\ts{w'} \ne \ts{w_i}$
	and so $\ts{w'} > \ts{w_i}$.

Therefore in both cases,
	$ts_{w'} > \ts{w_i}$.
\end{proof}

Since $w \in \B{i}$,
	by Observation~\ref{leaderofbatch4},
	$\ts{w} \le \ts{w_i}$.
By Claim~\ref{tsorderc1},
	$\ts{w'} > \ts{w_i} \ge \ts{w'}$.
\end{proof}

We now show that for every two operations $o_1$ and $o_2$,
	if $o_1$ completes before $o_2$ starts in $H$\XMP{in $H$} and $o_1,o_2 \in \seq{}$,
	then $o_1$ is before $o_2$ in $\seq{}$.

\begin{lemma}\label{linearization1}
If a write operation $w$ completes before a write operation $w'$ starts and $w,w' \in \seq{}$,
	then $w$ is before $w'$ in $\seq{}$.
\end{lemma}

\begin{proof}
Assume a write operation $w$ completes before a write operation $w'$ starts and $w,w' \in \seq{}$.
By Observation~\ref{leaderofbatch0},
	there are $i$ and $j$ such that $w \in \B{i}$ and $w' \in \B{j}$.
By line~\ref{C} of $\textrm{Algorithm}~\ref{f}$,
	$w$ and $w'$ are active at time $t_i$ and $t_j$ respectively.
Since $w'$ starts after $w$ completes,
	$t_i < t_j$ and so $i < j$.
Thus, by Observation~\ref{leaderofbatch1},
	$w$ is before $w'$ in $\seq{}$.
\end{proof}

\begin{lemma}\label{last3}
If an operation $w$ writes to $Val[-]$ at time $t$ and $w \in \B{i}$ for some $i \ge 1$,
	then $t_i \le t$.
\end{lemma}
\begin{proof}
Assume,
	for contradiction,
	an operation $w$ writes to $Val[-]$ at time $t$,
	$w \in \B{i}$ for some $i \ge 1$,
	and $t_i > t$.
By Observation~\ref{w},
	there is a $k\ge 1$ such that $w = w_k$
	and $t = t_k$.
By lines~\ref{line13}--\ref{seqi1} of $\textrm{Algorithm}~\ref{f}$
	(the $k$th iteration of the for loop),
	$w_k \in \wseq{k}$.
Since $t_i > t = t_k$,
	$k \le i-1$.
By lines~\ref{seqi1} and~\ref{seqi2} of $\textrm{Algorithm}~\ref{f}$,
	$\wseq{k}$ is a prefix of $\wseq{i-1}$.
Since $w_k \in \wseq{k}$,
	 $w_k \in \wseq{i-1}$.
Thus,
	by line~\ref{C} of $\textrm{Algorithm}~\ref{f}$,
	$w_k \notin \sC{i}$
	and so $w_k \notin \B{i}$.
Since $w_k = w$,
	this contradicts that $w \in \B{i}$.
\end{proof}

\begin{lemma}\label{linearization2}
If a read operation $r$ completes before a write operation $w$ starts and $r, w \in \seq{}$,
	then $r$ is before $w$ in $\seq{}$.
\end{lemma}

\begin{proof}
Assume a read operation $r$ completes before a write operation $w$ starts and $r, w \in \seq{}$.
Let $(-,ts)$ denote the value that $r$ returns.

\textbf{Case 1}: $ts = [0, \ldots, 0]$.
By lines~\ref{readinit1}--\ref{readinit2} of $\textrm{Algorithm}~\ref{f}$,
	$r$ is before all the write operations in $\seq{}$.
Thus,
	$r$ is before $w$ in $\seq{}$.

\textbf{Case 2}: $ts \ne [0, \ldots, 0]$.
By Observation~\ref{obsreadtime},
	an operation $w'$ writes $(-,ts)$ to $Val[-]$ and by Corollary~\ref{wwi},
	$w' \in \seq{}$.
By lines~\ref{followwrite1}--\ref{followwrite2} of $\textrm{Algorithm}~\ref{f}$,
	$r$ is after $w'$ and before any subsequent write in $\seq{}$.
So to show $r$ is before $w$ in $\seq{}$,
	it is sufficient to show that $w'$ is before $w$ in $\seq{}$.
\begin{claim}
 $w'$ is before $w$ in $\seq{}$.
\end{claim}
\begin{proof}
Since $w', w \in \seq{}$,
	by Observation~\ref{leaderofbatch0},
	there are $i$ and $j$ such that
	$w' \in \B{i}$ and	$w \in \B{j}$.
Let $t'$ be the time when $w'$ writes $(-,ts)$ to $Val[-]$.
Since $w' \in \B{i}$,
	by Lemma~\ref{last3},
	$t_i \le t'$.
Since $r$ returns $(-,ts)$,
	 $r$ reads $(-,ts)$ from $Val[-]$ and so $r$ completes after $t'\ge t_i$.
Since $w$ starts after $r$ completes,
	$w$ starts after time $t_i$.
Since $w \in \B{j} \subseteq \sC{j}$,
	by line~\ref{C} of $\textrm{Algorithm}~\ref{f}$,
	$w$ is active at time $t_j$.
Thus, $t_i < t_j$
	and so $i < j$.
By Observation~\ref{leaderofbatch1},
	$w'$ is before $w$ in $\seq{}$.
\end{proof}
Therefore,
	in both cases 1 and 2,
	$r$ is before $w$ in $\seq{}$.
\end{proof}

\begin{lemma}\label{last1}
If a write operation $w$ writes to $Val[-]$ before a read operation $r$ starts and $w, r \in \seq{}$,
	then $w$ is before $r$ in $\seq{}$.
\end{lemma}

\begin{proof}
Assume a write operation $w$ writes to $Val[-]$ before a read operation $r$ starts and $w, r \in \seq{}$.
Let $(-,ts)$
	denote the value that $r$ returns.
By Lemma~\ref{last},
	$ts \ge \ts{w}$
	and so $ts \ne [0 \ldots 0]$.
By Observation~\ref{obsreadtime},
	an operation $w'$ writes $(-,ts)$\XMP{this notation is a bit weird since w' writes ts instead of ts'} to $Val[-]$
	and by Corollary~\ref{wwi},
	 $w' \in \seq{}$.
By lines~\ref{followwrite1}--\ref{followwrite2} of $\textrm{Algorithm}~\ref{f}$,
	$r$ is after $w'$ in $\seq{}$.
Since $ts \ge \ts{w}$,
	there are two cases:

\textbf{Case 1:} $ts = \ts{w}$.
By Observation~\ref{onlyone},
	$w = w'$.
So $r$ is after $w = w'$ in $\seq{}$.

\textbf{Case 2:} $ts > \ts{w}$.
Since $r$ is after $w'$ in $\seq{}$,
	to show $w$ is before $r$ in $\seq{}$,
	it is sufficient to show that $w$ is before $w'$ in $\seq{}$.

\begin{claim}
$w$ is before $w'$ in $\seq{}$.
\end{claim}

\begin{proof}
Since $w,w' \in \seq{}$,
	by Observation~\ref{leaderofbatch0},
 	there are $i$ and $j$
 	such that $w \in \B{i}$ and $w' \in \B{j}$.

\textbf{Case (a)}: $i \ne j$.
Since $w \in \B{i}$,
	 $w' \in \B{j}$,
	 $i \ne j$,
	 and $ts > \ts{w}$,
	 by Lemma~\ref{tsorder},
	 $j > i$ (otherwise $ts < \ts{w}$).
Thus,
	by Observation~\ref{leaderofbatch1},
	$w$ is before $w'$ in $\seq{}$.

\smallskip

\textbf{Case (b)}: $i = j$.
Then $w, w'\in\B{i}$.
\begin{cclaim}\label{wrcc1}
$w' = w_i$.
\end{cclaim}
\begin{proof}
Since $ w \in \B{i}\subseteq \sC{i}$,
	by line~\ref{C} of $\textrm{Algorithm}~\ref{f}$,
	$w$ is active at time $t_i$.
Since $r$ starts after $w$ completes,
	$r$ starts after $t_i$.
Then by Lemma~\ref{last}
	$ts \ge \ts{w_i}$.
Since $w' \in \B{i}$,
	by Observation~\ref{leaderofbatch4},
	$ts \le \ts{w_i}$.
Thus, $ts = \ts{w_i}$ and by Observation~\ref{onlyone},
	$w' = w_i$.
\end{proof}
Since $ts \ne \ts{w}$,
	$w' \ne w$.
Thus, $w \ne w_i$.
Since $w \in \B{i}$,
	by line~\ref{seqi1} of $\textrm{Algorithm}~\ref{f}$,
	$w$ is before $w_i=w'$ in $\seq{}$.

Thus,
	 in both cases (a) and (b),
	  $w$ is before $w'$ in $\seq{}$.
\end{proof}
Therefore, in both cases 1 and 2,
	$w$ is before $r$ in $\seq{}$.
\end{proof}

Note that a completed write operation $w$ writes to $Val[-]$ before it completes.
Thus,
	Lemma~\ref{last1} immediately implies the following:
\begin{corollary}\label{linearization3}
If a write operation $w$ completes before a read operation $r$ starts and $w, r \in \seq{}$,
	then $w$ is before $r$ in $\seq{}$.
\end{corollary}

\begin{lemma}\label{linearization4}
If a read operation $r$ completes before a read operation $r'$ starts and $r,r' \in \seq{}$,
	then $r$ is before $r'$ in $\seq{}$.
\end{lemma}

\begin{proof}
Assume a read operation $r$ completes before a read operation $r'$ starts and $r,r' \in \seq{}$.
Let $(-,ts)$ denote the value that $r$ returns
and $(-,ts')$ denote the value that $r'$ returns.

\textbf{Case A:} $ts' = ts$.
By lines~\ref{R}--\ref{S} of $\textrm{Algorithm}~\ref{f}$,
	$r$ and $r'$ are in the same sequence $S_\mathcal{R}$ that is ordered by their start time.
Since $r'$ starts after $r$ completes,
	$r$ is before $r'$ in $S_\mathcal{R}$.
By lines~\ref{readinit2} and \ref{followwrite2},
	$r$ is before $r'$ in $\seq{}$.

\textbf{Case B:} $ts' \ne ts$.

\textbf{Subcase B.1}: $ts = [0, \ldots, 0]$.
By lines~\ref{readinit1}--\ref{readinit2} of $\textrm{Algorithm}~\ref{f}$,
	$r$ is before all the write operations in $\seq{}$.
Since $ts' \ne ts$,
	$ts' \ne [0, \ldots, 0]$.
By Observation~\ref{obsreadtime},
	 an operation $w'$ writes $(-,ts')$ to $Val[-]$
	 and by Corollary~\ref{wwi},
	$w' \in \seq{}$.
By lines~\ref{followwrite1}--\ref{followwrite2} of $\textrm{Algorithm}~\ref{f}$,
	$r'$ is after $w'$ in $\seq{}$.
Since $r$ is before $w'$ in $\seq{}$,
	$r$ is before $r'$ in $\seq{}$.

\textbf{Subcase B.2}:
	$ts > [0, \ldots, 0]$.
By Observation~\ref{obsreadtime},
	 an operation $w$ writes $(-,ts)$ to $Val[-]$
	and by Corollary~\ref{wwi},
	$w \in \seq{}$.
Since $r$ reads $(-,ts)$ from $Val[-]$
	and $r'$ starts after $r$ completes,
	$r'$ starts after $w$ writes $(-,ts)$ to $Val[-]$.
By Lemma~\ref{last},
	$ts' \ge ts$.
So $ts' \ge ts > [0, \ldots, 0]$.
By Observation~\ref{obsreadtime},
		an operation $w'$ writes $(-,ts')$ to $Val[-]$ and by Corollary~\ref{wwi},
	$w' \in \seq{}$.
Since $ts' \ne ts$, $w' \ne w$.
By lines~\ref{followwrite1}--\ref{followwrite2} of $\textrm{Algorithm}~\ref{f}$,
	 $r'$ is after $w'$ before any subsequent write in $\seq{}$
	 and $r$ is after $w$ before any subsequent write in $\seq{}$.
Since $r'$ starts after $w$ writes to $Val[-]$,
	by Lemma~\ref{last1},
	$w$ is before $r'$ in $\seq{}$.
Thus,
	$w$ is before $w'$ in $\seq{}$
	and so $r$ is before $w'$ in $\seq{}$.
Since $r'$ is after $w'$ in $\seq{}$,
	$r$ is before $r'$ in $\seq{}$.

Therefore,
	in both cases A and B,
	$r$ is before $r'$ in $\seq{}$.
\end{proof}

From Lemma~\ref{linearization1},
	Lemma~\ref{linearization2},
	Corollary~\ref{linearization3},
	and Lemma~\ref{linearization4},
	we have the following:
\begin{corollary}\label{linearizationf}
For every two operations $o_1$ and $o_2$,
	if $o_1$ completes before $o_2$ starts and $o_1,o_2 \in \seq{}$,
	then $o_1$ is before $o_2$ in $\seq{}$.
\end{corollary}

\begin{lemma}\label{l1}
$\seq{}$ contains all completed operations of $H$ and possibly some non-completed ones.
\end{lemma}
\begin{proof}
By Corollary~\ref{wwi},
	$\seq{}$ contains all the completed write operations in $H$ and possibly some non-completed ones.
Let $r$ be any completed read operation in $H$.
Since $r$ is completed,
	 $r$ returns some value $(-,ts)$.
If $ts = [0,...0]$,
	by line~\ref{readinit2} of $\textrm{Algorithm}~\ref{f}$,
	$r$ is in $\seq{}$.
If $ts \ne [0,...0]$,
	by Observation~\ref{obsreadtime} and Corollary~\ref{wwi},
	there is a write operation $w$ in $\seq{}$ that writes $(v,ts)$.
So by lines~\ref{followwrite1} and \ref{followwrite2} of $\textrm{Algorithm}~\ref{f}$,
	$r$ is in $\seq{}$.
In both cases, $\seq{}$ contains the completed read operation $r$.
Thus, $\seq{}$ contains all completed operations of $H$ and possibly some non-completed ones.
\end{proof}

\begin{observation}\label{reg}
For any read operation $r$ in $\seq{}$,
		if no write precedes $r$ in $\seq{}$, then $r$ returns the initial value of the register;
		Otherwise, $r$ returns the value written by the last write that occurs before $r$ in $\seq{}$
\end{observation}

\begin{lemma}\label{fsatl2}\XMP{linearization -> linearization function}
$f$ is a linearization function of $\mathcal{H}$.
\end{lemma}

\begin{proof}
Recall that:
	(1)~$\seq{}$ is the output of $\textrm{Algorithm}~\ref{f}$ ``executed'' on an arbitrary history
	$H \in \mathcal{H}$ of $\textrm{Algorithm}~\ref{wsl}$ (the implementation on MRMW registers), and
	(2)~$\textrm{Algorithm}~\ref{f}$ defines the linearization function $f$; in other words, $f(H) = \seq{}$.
Furthermore,
	$\seq{}$ satisfies properties~\ref{p1}, \ref{p2}, and \ref{p3} of Definition~\ref{defl},
	by Observation~\ref{l1},
	 Corollary~\ref{linearizationf},
	and Observation~\ref{reg},
	respectively.
Thus, $f$ is a linearization function of $\mathcal{H}$.
\end{proof}

To prove that $f$ is a $\str$ function for the set of histories $\mathcal{H}$ of $\textrm{Algorithm}~\ref{wsl}$,
	it now suffices to show that $f$ also satisfies property~(P) of Definition~\ref{defwsl}, namely:

\begin{restatable}{lemma}{propp}\label{fsatp}
For any $G, H \in \mathcal{H}$,
	if $G$ is a prefix of $H$,
	then the sequence of write operations in $f(G)$\XMP{f(G) here is SEQ}
	is a prefix of the sequence of write operations in $f(H)$.
\end{restatable}

Intuitively, the above lemma holds, because $\textrm{Algorithm}~\ref{f}$ scans the input history $H$ (of Algorithm 1) \emph{by increasing time},
	and it linearizes the write operations as follows:
	when some write to $Val[-]$ occurs, say at time $t_i$,
	\emph{without looking ``ahead'' at what occurs in $H$ after time $t_i$},
	$\textrm{Algorithm}~\ref{f}$ linearizes a (possibly empty) batch of write operations
	that started before time $t_i$,
	by \emph{appending} them to the sequence of write operations that it previously linearized.
The proof of Lemma~\ref{fsatp} is straightforward and relegated to Appendix~\ref{app1}.

By Corollary~\ref{fsatl2} and Lemma~\ref{fsatp},
	the function $f$ defined by $\textrm{Algorithm}~\ref{f}$ is a $\str$ function for the set of histories $\mathcal{H}$
	of $\textrm{Algorithm}~\ref{wsl}$.
Therefore:

\begin{restatable}{theorem}{algowsl}\label{aiswsl}
$\textrm{Algorithm}~\ref{wsl}$ is a $\textrm{write strongly-linearizable}$ implementation of a MWMR register from SWMR registers.
\end{restatable}

Helmi \emph{et. al} show that there is no strongly linearizable implementation of MWMR registers from SWMR registers
	(Corollary 3.7 in \cite{sl12}).
Thus:
\begin{corollary}
$\textrm{Algorithm}~\ref{wsl}$ is not a strongly linearizable implementation of a MWMR register.
\end{corollary}

This implies that strong linearizability is strictly stronger than write strong-linearizability.

\section{Achieving write strong-linearizability is harder than achieving linearizability}\label{sectionlamport}

As we will see, every linearizable implementation of an SWMR register
	is necessarily write strongly-linearizable.
In contrast, here we prove that there is
	a linearizable implementation of an MWMR register from SWMR registers (namely, Algorithm~\ref{Al})
	that is \emph{not} write strongly-linearizable.

\begin{algorithm}[!b]
\caption{Implementing a linearizable MWMR register $\textbf{R}$ from SWMR registers}
\begin{flushleft}
\textsc{Shared Object:}

For $i=1,2,...,n$:

$Val[i]$: SWMR register that contains a tuple $(v,ts)$
	where $v$ is a value and $ts$ is a tuple of the form~$\langle sq, pid\rangle$;

\hspace*{1.2cm}initialized to $(0,\langle 0,i \rangle)$.

\vspace{0.2cm}

\textsc{Local Object:}

$\textit{new\_sq}$: a register initialized to $0$.

$\textit{new\_ts}$: a register initialized to $\langle 0,k \rangle$ for process $p_k$.
\end{flushleft}
\vspace{0.05cm}

\begin{algorithmic}[1]

\STATEx When writer $p_k$ writes $v$ to $\textbf{R}$ \hfill//$1 \le k \le n$
\FOR{$i = 1$ to $n$} \label{wcollectts1}
	\STATE $(v_i,ts_i) \gets Val[i]$ \label{wcollectts2}
\ENDFOR\label{wcollectts3}
\STATE $\textit{new\_sq} \gets \max \{ts_1.sq,...,ts_n.sq\} +1$ \label{nsq}
\STATE $\textit{new\_ts} \gets \langle new\_sq, k \rangle$ \label{nts}
\STATE $Val[k] \gets (v,new\_ts)$\label{writeAl}
\STATE \textbf{return} done
\newline

\STATEx When a process reads from $\textbf{R}$
\FOR{$i = 1$ to $n$}\label{collectts1}
	\STATE $(v_i,ts_i) \gets Val[i]$\label{collectts2}
\ENDFOR\label{collectts3}
\STATE let $j$ be such that $ts_j = \max \{ts_1,...,ts_n\}$ \label{tsmax} \hfill// lexicographic max
\STATE \textbf{return} $(v_j,ts_j)$ \label{returnmax}
\end{algorithmic}\label{Al}
\end{algorithm}

Algorithm~\ref{Al} implements a MWMR register $\textbf{R}$ from SWMR registers $Val[i]$ for $i=1,2,...,n$.
Each value written to $\textbf{R}$ is timestamped with tuple $\langle sq,pid\rangle$
	where $sq$ is a sequence number and $pid$ is the id of the process that writes the value;
	intuitively, these are Lamport clocks that respect the causal order of write events.
Each register $Val[k]$ contains the latest value that $p_k$ wrote to $\textbf{R}$
	with its corresponding timestamp.
To write a value $v$ into $\textbf{R}$,
	$p_k$ first reads every register $Val[-]$ (lines~\ref{wcollectts1}--\ref{wcollectts3});
	then $p_k$ forms a new sequence number $\textit{new\_sq}$ by
	incrementing the maximum sequence number
	that it read from $Val[-]$ (line~\ref{nsq});
	finally, $p_k$ writes the tuple $(v,\textit{new\_ts})$, where  $\textit{new\_ts} = \langle \textit{new\_sq}, k\rangle$, into $Val[k]$ (lines~\ref{nts}--\ref{writeAl}).
To read $\textbf{R}$,
	a process $p$ first reads all registers $Val[-]$ (lines~\ref{collectts1}--\ref{collectts3});
	then $r$ returns the value $v$ with the greatest timestamp in lexicographic order
	(lines~\ref{tsmax}--\ref{returnmax}).

Intuitively, Algorithm~\ref{Al} implements a linearizable MWMR register:
	the write operations can be linearized by their timestamps (which form a total order);
	the read operations are linearized according to the value that they read.
The proof of the following theorem is given in Appendix~\ref{lamport1}.

\begin{restatable}{theorem}{lampol}\label{lamportisl}
$\textrm{Algorithm}~\ref{Al}$ is a linearizable implementation of a MWMR register from SWMR registers.
\end{restatable}

The implemented register, however, is not $\textrm{write strongly-linearizable}$: roughly speaking the information provided by Lamport clocks
	is not sufficient to linearize the write operations on-line.

\begin{theorem}
$\textrm{Algorithm}~\ref{Al}$ is not a $\textrm{write strongly-linearizable}$ implementation of a MWMR register.
\end{theorem}

\begin{proof}
Consider the set of histories $\mathcal{H}$ of $\textrm{Algorithm}~\ref{Al}$ executed by $n=3$ processes,
	 $p_1$, $p_2$ and $p_3$.
To prove that $\textrm{Algorithm}~\ref{Al}$ is not a $\textrm{write strongly-linearizable}$ implementation,
		we show that $\mathcal{H}$ is not \linebreak $\textrm{write strongly-linearizable}$.
More precisely,
	we prove that for any function $f$ that maps histories in $\mathcal{H}$ to sequential histories,
	there exist histories $G,H\in \mathcal{H}$ such that $G$ is a prefix of $H$ but $f(G)$ is not a prefix of~$f(H)$.

\begin{figure}[!b]
\centering
\includegraphics[width=1\textwidth]{sg/newgh}
  \caption{Histories $G$ and $H$ for Cases 1 and 2}
  \label{Hg}
\end{figure}

Let $f$ be a function that maps histories in $\mathcal{H}$ to sequential histories.
Consider the following history $G \in \mathcal{H}$ (shown at the left of Figure~\ref{Hg}): \XMP{caption of fig??}
\begin{itemize}
\item Initially, $\textbf{R}$ contains $0$, and each register $Val[i]$ contains $(0,\langle 0,i\rangle)$.
\item At time $t_0$,
	process $p_1$ starts an operation $\W{1}$ to write a value $v \ne 0$ to $\textbf{R}$.
By lines \ref{wcollectts1}--\ref{wcollectts2},
	$p_1$ first reads $(0,\langle 0,1\rangle)$ from $Val[1]$ into $(-,ts_1)$,
	say at time $t_1$,
	and then reads $(0,\langle 0,2\rangle)$ from $Val[2]$ into $(-,ts_2)$,
	say at time $t_2$.
Thus,
	$p_1$ now has $ts_1 = \langle 0,1\rangle$
	and $ts_2 = \langle 0,2\rangle$,
	i.e., $ts_1.sq = ts_2.sq = 0$.

\item At time $t_3 > t_2$,
	process $p_2$ starts an operation $\W{2}$ to write a value $v'$ to $\textbf{R}$ such that $v' \ne v$ and $v' \ne 0$.
By lines \ref{wcollectts1}--\ref{wcollectts2},
		$p_2$ reads $(0, \langle 0,1\rangle)$ from $Val[1]$ into $(-,ts_1)$,
		 $(0, \langle 0,2\rangle)$ from $Val[2]$ into $(-,ts_2)$,
		 and $(0, \langle 0,3\rangle)$ from $Val[3]$ into $(-,ts_3)$.
Thus,
	$p_2$ now has $ts_1 = \langle 0,1\rangle$,
	$ts_2 = \langle 0,2\rangle$,
	and $ts_2 = \langle 0,3\rangle$,
	i.e., $ts_1.sq = ts_2.sq = ts_3.sq = 0$.
By lines~\ref{nts}--\ref{writeAl},
	 $p_2$ then writes $(v',\langle 1,2\rangle)$ to $Val[2]$
	 and completes $\W{2}$ at time $t_4$.
Then at time $t_4$,
	$Val[1]$ contains $(0,\langle 0,1\rangle)$,
	 $Val[2]$ contains $(v',\langle 1,2\rangle)$, and
	$Val[3]$ contains $(0,\langle 0,3\rangle)$.
\end{itemize}

Since the write operation $\W{2}$ completes in $G \in \mathcal{H}$ and $f$ is a linearization function for $\mathcal{H}$,
	by property~\ref{p1} of Definition~\ref{defl},
	$\W{2}$ is in $f(G)$.
Since the write operation $\W{1}$ is concurrent with $\W{2}$,
there are two cases: (1)~$\W{1}$ is not before $\W{2}$ in $f(G)$,
	 or (2) $\W{1}$ is before $\W{2}$ in $f(G)$.

\textbf{Case 1}: $\W{1}$ is not before $\W{2}$ in $f(G)$.
Consider the following history $H \in \mathcal{H}$ (shown at the top right of Figure~\ref{Hg}):
\begin{itemize}
\item $H$ is an extension of $G$, i.e., $G$ is a prefix of $H$.
\item At time $t_5> t_4$,
	$p_1$ continues the operation $\W{1}$ and reads $(0, \langle 0,3\rangle)$ from $Val[3]$ into $(-,ts_3)$ so it has
	 $ts_3.sq = 0$.
By lines~\ref{nts}--\ref{writeAl},
	$p_1$ writes $(v,\langle 1,1\rangle)$ to $Val[1]$.
After that,
	$p_1$ completes $\W{1}$, say at time $t_6$.
At time $t_6$,
	$Val[1]$ contains $(v,\langle 1,1\rangle)$,
	$Val[2]$ contains $(v',\langle 1,2\rangle)$,
	and $Val[3]$ contains $(0,\langle 0,3\rangle)$.
\item At time $t_7> t_6$,
	$p_3$ starts a read operation $\RD{}$ to read $\textbf{R}$.
In lines~\ref{collectts1}--\ref{collectts2},
	 $p_3$ reads $ts_1 = \langle 1,1\rangle$,
	$ts_2 = \langle 1,2\rangle$,
	and $ts_3 = \langle 0,3\rangle$.
Since $ts_2 =\langle 1,2\rangle > ts_1 =\langle 1,1\rangle > ts_3 =\langle 0,3\rangle$,
	by line~\ref{tsmax},
	$\RD{}$ returns $(v',\langle 1,2\rangle)$ -- the value written by $\W{2}$.
\end{itemize}
Since the read operation $\RD{}$ returns the value written by $\W{2}$ in $H\in \mathcal{H}$,
	and $f$ is a linearization function for~$\mathcal{H}$,
		by property~\ref{p3} of Definition~\ref{defl},
	 	$\RD{}$ is after $\W{2}$ and before any subsequent write operation in $f(H)$.
Since $\RD{}$ starts after $\W{1}$ completes,
		by property~\ref{p2} of Definition~\ref{defl},
	$\RD{}$ is after $\W{1}$ in $f(H)$.
Thus,
	$\W{1}$ is before $\W{2}$ in $f(H)$.
Since, by assumption,
	 $\W{2}$ is in $f(G)$ and $\W{1}$ is not before $\W{2}$ in $f(G)$,
	$f(G)$ is not a prefix of $f(H)$.

\textbf{Case 2}: $\W{1}$ is before $\W{2}$ in $f(G)$.
Consider the following history $H \in \mathcal{H}$ (shown at the bottom right of Figure~\ref{Hg}):
\begin{itemize}
\item $H$ is an extension of $G$.
\item At time $t_5> t_4$,
	process $p_3$ starts an operation $\W{3}$ to write $v''$ to $\textbf{R}$ such $v'' \ne v$.
In lines~\ref{wcollectts1}--\ref{wcollectts2},
	$p_3$ reads $(0, \langle 0,1\rangle)$ from $Val[1]$ into $(-,ts_1)$,
	$(v', \langle 1,2\rangle)$ from $Val[2]$ into $(-,ts_2)$,
	and $(0, \langle 0,3\rangle)$ from $Val[3]$ into $(-,ts_3)$
Thus,
	$p_3$ now has $ts_1 = \langle 0,1\rangle$,
	$ts_2 = \langle 1,2\rangle$,
	and $ts_2 = \langle 0,3\rangle$,
	i.e., $ts_1.sq = 0$, $ts_2.sq =1$, and $ts_3.sq = 0$.
By lines~\ref{nts}--\ref{writeAl},
	$p_3$ then writes $(v'',\langle 2,3\rangle)$ to $Val[3]$.
	and completes $\W{3}$ at time $t_6$.
\item At time $t_7> t_6$,
	$p_1$ continues the operation $\W{1}$ and reads $(v'', \langle 2,3\rangle)$ from $Val[3]$ into $(-,ts_3)$ so it has
	 $ts_3.sq = 2$.
By lines~\ref{nts}--\ref{writeAl},
	$p_1$ writes $(v,\langle 3,1\rangle)$ to $Val[1]$.
After that,
	$p_1$ completes $\W{1}$, say at time $t_8$.
At time $t_8$,
	$Val[1]$ contains $(v,\langle 3,1 \rangle)$,
	$Val[2]$ contains $(v',\langle 1,2 \rangle)$,
	and $Val[3]$ contains $(v'',\langle 2,3 \rangle)$.
\item At time $t_9 > t_8$,
	$p_3$ starts a read operation $\RD{}$ to read $\textbf{R}$.
In lines~\ref{collectts1}--\ref{collectts2},
	$p_3$ reads $(v, \langle 3,1\rangle)$ from $Val[1]$ into $(-,ts_1)$,
	$(v', \langle 1,2\rangle)$ from $Val[2]$ into $(-,ts_2)$,
	and $(v'', \langle 2,3\rangle)$ from $Val[3]$ into $(-,ts_3)$.
Since $ts_1 = \langle 3,1\rangle > ts_3 =\langle  2,3\rangle > ts_2 = \langle 1,2\rangle$,
	by line~\ref{tsmax},
	$\RD{}$ returns $(v,\langle 3,1 \rangle)$ -- the value written by $\W{1}$.
\end{itemize}

Since the read operation $\RD{}$ returns the value written by $\W{1}$ in $H \in \mathcal{H}$,
	and $f$ is a linearization function for $\mathcal{H}$,
	by property~\ref{p3} of Definition~\ref{defl},
	 	$\RD{}$ is after $\W{1}$ and before any subsequent write operation in $f(H)$.
Since $\RD{}$ starts after $\W{2}$ completes,
		by property~\ref{p2} of Definition~\ref{defl},
	$\RD{}$ is after $\W{2}$ in $f(H)$.
Thus,
	$\W{2}$ is before $\W{1}$ in $f(H)$.
Since, by assumption,
	 $\W{1}$ is before $\W{2}$ in $f(G)$,
	$f(G)$ is not a prefix of $f(H)$.

Then, in both case 1 and case 2,
	there is a history $H \in \mathcal{H}$
	such that $G$ is a prefix of $H$ but $f(G)$ is not a prefix of $f(H)$.
Therefore
	the theorem holds.
\end{proof}

\section{Linearizable SWMR registers are necessarily write strongly-linearizable}\label{swsection}

In Appendix~\ref{proofsw}, we show that \emph{any} linearizable implementation of SWMR registers is $\textrm{write strongly-linearizable}$
	(this holds for message-passing, shared-memory, and hybrid systems).
Thus, the well-known ABD implementation of SWMR registers in message-passing systems
	is not only linearizable; it is actually write strongly-linearizable.

\rmv{

We now prove that \emph{any} linearizable implementation of SWMR registers is $\textrm{write strongly-linearizable}$
	(this holds for message-passing, shared-memory, and hybrid systems).
Thus, the well-known ABD implementation of SWMR registers in message-passing systems
	is not only linearizable but actually write strongly-linearizable.
(This implementation however is \emph{not} strongly linearizable~\cite{abdnotsl}.)

Consider an arbitrary implementation $\mathcal{A}$ of a SWMR register.
Let $\mathcal{H}$ be the set of histories of $\mathcal{A}$.
Since $\mathcal{A}$ implements a single-writer register,
	the following holds:
\begin{observation}\label{swob}
In any history $H\in \mathcal{H}$,
\begin{enumerate}
	\item \label{swob11}there are no concurrent write operations, and
	\item \label{swob12}there is at most one incomplete write operation.
\end{enumerate}
\end{observation}

By part~\ref{swob11} of Observation~\ref{swob} and property~\ref{p2} of Definition~\ref{defl},
	we have the following:
\begin{observation}\label{swob2}
For any history $H\in \mathcal{H}$ and any linearization function $f$ of $\mathcal{H}$,
	the write operations in $f(H)$ are totally ordered by their start time in $H$.
\end{observation}

\begin{lemma}
If $\mathcal{A}$ is linearizable,
	then $\mathcal{A}$ is $\textrm{write strongly-linearizable}$.
\end{lemma}

\begin{proof}
Assume $\mathcal{A}$ is linearizable.
By Definition~\ref{L-I},
	 there is a linearization function $f$ for $\mathcal{H}$.
Consider a function $f^*$ that is modified from $f$ as follows:
for any history $H$ and its linearization $f(H)$,
	if the last operation $o$ in $f(H)$ is a write operation that is incomplete in $H$,
	then we obtain $f^*(H)$ by removing $o$ from $f(H)$;
	otherwise, $f^*(H)$ equals $f(H)$.

\begin{claim}\label{ifwinthencor}
If a write operation $w$ is in $f^*(H)$,
	then $w$ is completed or read by some read operation in $H$.
\end{claim}

\begin{proof}
Assume, for contradiction,
	a write operation $w \in f^*(H)$ is incomplete and not read by any read operation in $H$.
Since $w \in f^*(H)$,
	$w$ is in $f(H)$ such that $w$ is not the last operation in $f(H)$ ($\star$).
Since $w$ is incomplete,
	by Observation~\ref{swob},
	$w$ is the last write operation in $H$.
By Observation~\ref{swob2},
	$w$ is the last write operation in $f(H)$.
Furthermore,
	since $w$ is not read by any read operation in $H$,
	no read operation is after $w$ in $f(H)$.
Thus, $w$ is the last operation in $f(H)$,
	which contradicts ($\star$).
\end{proof}

\begin{claim}\label{ifcorthenwin}
If a write operation $w$ is completed or read by some read operation in $H$,
	then $w$ is in $f^*(H)$,
\end{claim}

\begin{proof}
Assume a write operation $w$ is completed or read by some read operation in $H$.

\textbf{Case 1:} $w$ is completed in $H$.
Since $f$ is a linearization function for $\mathcal{H}$,
	by property~\ref{p1} of Definition~\ref{defl},
	$w$ is in $f(H)$.
Since $f^*(H)$ removes only the incomplete operation from $f(H)$,
	$w$ is in $f^*(H)$.

\textbf{Case 2:} $w$ is read by some read operation $r$ in $H$.
Since $f$ is a linearization function for $\mathcal{H}$,
	by property~\ref{p3} of Definition~\ref{defl},
	$w$ is before $r$ in $f(H)$ and so $w$ is not the last operation in $f(H)$.
Since $f^*(H)$ removes only the last operation from $f(H)$,
	$w$ is in $f^*(H)$.

Thus, in both cases 1 and 2,
	 $w$ is in $f^*(H)$.
\end{proof}

\begin{claim}
$f^*$ is a linearization function of $\mathcal{H}$.
\end{claim}
\begin{proof}
Consider any history $H\in \mathcal{H}$.
Since $f^*(H)$ removes from $f(H)$ only the operation that is incomplete in $H$,
	$f^*(H)$ still satisfies properties~\ref{p1} and \ref{p2} of Definition~\ref{defl}.
Since $f^*(H)$ removes only the last operation from $f(H)$,
	$f^*(H)$ still satisfies property~\ref{p3} of Definition~\ref{defl}.
Therefore,
	$f^*$ is a linearization function of $\mathcal{H}$.
\end{proof}

\begin{claim}
$f^*$ satisfies property (P) of Definition~\ref{defwsl}.
\end{claim}
\begin{proof}
Consider histories $G, H\in \mathcal{H}$ such that $G$ is a prefix of $H$.
Let $W_G$ and $W_H$ denote the write sequences in $f^*(G)$ and $f^*(H)$ respectively.
By Claim~\ref{ifwinthencor},
	 all the operations in $W_G$ are completed in $G$ or read by some read operations in $G$.
Since $G$ is a prefix of $H$,
	all operations in $W_G$ are also completed in $H$ or read by some read operations in $H$.
So By Claim~\ref{ifcorthenwin},
	$W_H$ contains all the operations in $W_G$.
By Observation~\ref{swob2},
	the write operations in $W_G$ and $W_H$ are totally ordered by their start time in $G$ and $H$, respectively.
Then since $G$ is a prefix of $H$ and $W_H$ contains all the operations in $W_G$ ,
	$W_G$ is a prefix of $W_H$.
So $f$ satisfies property (P) of Definition~\ref{defwsl}.
\end{proof}
Thus,
	 $f$ is a $\str$ function for $\mathcal{H}$ and $\mathcal{A}$ is $\textrm{write strongly-linearizable}$.
\end{proof}

\begin{restatable}{theorem}{swe}\label{swequal}
Any linearizable implementation of a SWMR register is necessarily $\textrm{write strongly-linearizable}$.
\end{restatable}

\section{Concluding remarks}
As we mentioned earlier,
	many randomized algorithms in the literature use atomic MWMR registers.
An interesting open problem is to determine which ones
	can also (be made to) work in systems with atomic SWMR registers.
If we replace a randomized algorithm's atomic MWMR registers with
	\emph{linearizable}\linebreak
	implementations of MWMR registers from atomic SWMR registers,
	we may break it:
	it may lose some of its properties~\cite{sl11} including,
	as we showed in this paper,
	termination.
On the other hand, we cannot replace
	an algorithm's atomic MWMR registers with
	\emph{strongly linearizable}
	implementations of MWMR registers from atomic SWMR registers
	--- which would automatically preserve the correctness of this algorithm ---
	simply because no such implementation exists~\cite{sl12}.
But perhaps many (maybe even most) of the known randomized algorithms that use atomic MWMR registers
	do not actually need the full strength of strongly linearizable registers:
	in particular, they may not need the ``strong linearizability property'' to hold for
	\emph{both} read and write operations.\footnote{In fact, a recent paper
	shows that a well-known randomized algorithm by Aspness and Herlihy that assumes atomic registers
	does not actually need any linearizability property:
	it works correctly with registers that are only \emph{regular}~\cite{vassos20}.}
Randomized algorithms that need the strong linearizability properties only for \emph{write operations},
	also work in systems with atomic SWMR registers:
	just replace their MWMR registers with the register implementation given by $\textrm{Algorithm}~\ref{wsl}$.

\section*{Acknowledgments}
We thank Wojciech Golab and Philipp Woelfel for their helpful comments.

\bibliographystyle{abbrv}

redpajama_set_name: RedPajamaArXiv