\section{Introduction}
Most highly accessed websites rely on large volumes of data in the back end. Scalability of these websites is dependent on the 
ability to serve thousands of web-requests per second. Although it is desirable to store all of this data at a single server,  due to limited resources available on a single machine it is impossible to do so. Therefore, such data is partitioned
 and stored across multiple machines connected through high-speed networks. Subsequently, serving one webpage 
 request may involve retrieving various data objects of the page from multiple servers. These individual data objects are 
 often referred to as \emph{shards}  or \emph{objects}, where each object is managed by a separate server. 
 For example, a dynamically generated
 webpage may contain various objects, such as  texts, images, and videos: the text elements may be stored in one server, the images and thumbnails in another, and, similarly, the video clips may be managed by a separate server. During the webpage synthesis and loading,  the proxy reader reads all of these separate objects via a {\sc read} transaction.  Some of these objects may be updated while {\sc read} transactions are carried out. 
  A \emph{transaction} consists of a set of read or write operations on the underlying objects which are to be executed atomically.
  
   In our work, we consider two types of transactions:  \emph{{\sc write} transactions} and \emph{{\sc read} transactions}. A {\sc read} transaction consists of a set of read operations, one per each  object, and  a {\sc write} transaction comprises of a set of individual write operations on a subset of the objects.
   Consistent data access during a transactional read requires  \emph{transactional isolation}, where   reads to different objects  must  retrieve either all updates  for a given update or none. Similar transactional isolation of {\sc write} transactions is also desirable, where the collection of all the write operations to different objects is carried out atomically. Handling transactional isolation with concurrent read and {\sc write} transactions is complex and expensive which may often  lead to poor performance and lower throughput, which in turn  leads to substantial revenue loss and poor user experience.
  In  practice,  it is observed that most of the  transactions are {\sc read} transactions, and therefore, one approach to boost performance is to improve the performance of the {\sc read} transactions~\cite{TAO2013}. 
  
  In ~\cite{SNOW2016},  the authors study the question whether {\sc read} transactions can be fast enough even in the presence of concurrent {\sc write} transactions. They introduce four desirable properties  of a system to achieve low-latency  {\sc read} transactions, which they refer to collectively as the  \emph{SNOW  property}:  {\bf S}trict serializability among transactions, {\bf N}on-blocking operations and {\bf O}ne-response from each shard for the {\sc read} transactions, and compatibility with conflicting {\bf W}rite transactions. The ``strict serializability'' property requires that the set of read or writer operations of  any read and {\sc write} transactions is executed atomically as if executed by  a single server.
 ``Non-blocking'' requires the read requests corresponding to different objects  to be served by the managing servers immediately, without blocking for any other external input or output messages.   The ``one-response'' property requires that for any read operation of an object,  the server managing the object responds with only one version, and the operation completes in one round of client to server communication.  The final property ``conflicting and concurrent {\sc write} transactions'' allows {\sc write} transactions to execute concurrently with {\sc read} transactions  on the same set of objects.
 
In distributed systems, the availability  of the systems is often stated in terms of liveness properties of the transactions or operations~\cite{H91, Herlihy:2003, Massalin:1992}. Such a  requirement on responsiveness of a system is also referred to as availability.  One of the strongest, and  the most desirable of these properties is  \emph{wait-freedom}, which requires that as long as the client is taking a sufficient number of steps, it completes the operations irrespective of the speed of other clients. 
In~\cite{SNOW2016},  the wait-free property of the read operations, corresponding to a {\sc read} transaction in a system that satisfies SNOW properties,  is inherent in the  N and O properties; this also implies the wait-freedom property  for {\sc read} transactions. However, in~\cite{SNOW2016}, no liveness property for {\sc write} transactions is stated explicitly. In their work,  the authors prove that with at least three clients,  in an asynchronous message-passing environment, even in the absence of any failures, it is impossible to have a protocol that satisfies all of the four properties of SNOW, which they refer to as  the \emph{SNOW  theorem}. In their proof,  they consider a system with two read clients, which issues only {\sc read} transactions, and a write client invoking {\sc write} transactions. From their proof, it is not clear whether they consider the possibility of exchanging messages between clients. Additionally, there is no explicitly stated  requirement on the liveness of the {\sc write} transactions. They pose the case for two clients as an unresolved case, i.e., it is not known whether all of SNOW properties can be implemented for any two client system. 

\paragraph{Our contribution} In this work, we revisit the results of the  SNOW theorem and present four new results. First, we  show that even with two clients, in the absence of client-to-client messaging,  it is impossible to design a transaction processing system which satisfies  the SNOW properties. 
 Second, we provide a thorough proof of the  SNOW theorem for systems with at least three clients,  i.e.,  we show that it is impossible to implement a transaction processing system, which can implement the SNOW property, consisting of  at least  three clients, even with client-to-client messaging. In our proof, we explicitly make assumptions regarding  the liveness of {\sc write} transactions and  client-to-client messaging.  Our proof technique involves assuming  an  execution  of an arbitrary transaction processing system, assumed to be specified as an  I/O automaton,  that  satisfies the SNOW property, and then, argue by constructing a sequence of executions of the automata, finally,  leading to an  execution which contradicts  the S property. The above two results  indicate that client-to-client messaging ability plays a key role in the  achievability of the SNOW property. 
This motivates  our third result, where we present an algorithm with  \emph{multiple  writers,  single reader} (MWSR) which satisfies the SNOW properties when  client-to-client messaging is allowed. Finally, we present an algorithm, for \emph{multiple-writer, multiple-reader} (MWMR) setting in the absence of  client-to-client messaging,  which satisfies the ``S'', ``N'', ``W'' properties and and a weaker version the O property, which we denote by   ``o'',  where ``o''  refers to   the one-version  property of a read operation, but can take multiple rounds of communication to complete the read operation. Collectively, we refer to the ``S'', ``N'', ``o'' and ``W'' properties as the ``SNoW'' property.  

\paragraph{Related work} This will be filled in depending what type of conference we send the paper  to and whether we add some experimental results of the two algorithms presented in the paper.

\paragraph{Document Structure} The remainder of the document is organized as follows. Section~\ref{model} presents the models and definitions. Section~\ref{two-client}, provides the proof for the impossibility result for the two-client setting when clients do  not communicate among each other. In section~\ref{two-client}, we present the impossibility result for the three-client setting. Next, in section~\ref{mwsr} we present the algorithm with multi-writer, single-reader (MWSR) which satisfies the SNOW properties, when client-to-client communication is allowed. In section~\ref{mwmr},  we present an algorithm for multi-writer, multi-reader scenario which satisfies the  SNoW  properties.  

\section{System model and architecture}\label{model}

\subsection{I/O Automata}
We consider a distributed system consisting of \emph{asynchronous} processes of three types: a set of \emph{readers} and  \emph{writers}, called clients, and a set of  \emph{servers}.  Each of these processes is associated with an unique identifier. 
Processes can communicate via asynchronous reliable communication links. This means that  any message sent on the link is guaranteed to eventually reach the destination process. The model assumes that client or server processes never fail. We do not make any assumption regarding the  order of message delivery in the same channel.

We assume that the formal specification of an  algorithm in our context is  specified using the I/O Automata. An algorithm  is specified from the composition $A$ of a set of \emph{automata} where each automaton  $A_i$ corresponds to a process $i$ in the system. An automaton $A_i$ consists of 
a set of states $\states{A_i}$ , including a special subset $\startstates{A_i} \subseteq \states{A}$
called the \emph{start states} ; a \emph{signature}, denoted $\sig{A_i}$;
and a set of \emph{transitions} $\trans{A_i}$. The set of states $\states{A_i}$ are essentially defined by a set of  state variables in $A_i$.
The signature $\sig{A_i}$ consists of three disjoint sets in $\inactions{A_i}$, $\outactions{A_i}$ and $\intactions{A_i}$, 
where $\inactions{A_i}$ referred to as the \emph{input actions}, $\outactions{A_i}$ the \emph{output actions} and $\intactions{A_i}$
are the \emph{internal actions}.  The set $\trans{A_i}$ consists of the set of \emph{transitions} or \emph{steps}, where each step consists
of a 3-tuple $(\sigma_i, a_i, \sigma_{i+1})$, where $\sigma_i, \sigma_{i+1} \in \states{A_i}$ and $a_i \in \trans{A_i}$. The set $\inactions{A_i} \cup \outactions{A_i}$, often denoted as $\extactions{A_i}$, are called the \emph{external signature} of automaton $A_i$. 
Note that $A$ is a composition of the set of automata $A_i$, $i \in \mathcal{I}$ and the following analogous components for $A$ are defined as
$\states{A} \triangleq \prod_{i\in \mathcal{I}}  \states{A_i}$; $\sig{A} \triangleq \prod_{i\in \mathcal{I}} \sig{A_i}$; 
$\startstates{A} \triangleq  \prod_{i \in \mathcal{I}} \startstates{A_i}$ and 
$\trans{A} \triangleq \{ (\sigma, a, \sigma'): $ $\mbox{if~} a \in \trans{A_i}$$ \mbox{~for some~}$$ i \in \mathcal{I} \mbox{~then~}$$ \sigma, \sigma' \in \states{A_i}, $$\mbox{~else}$$~\sigma =\sigma'\}$.

Informally, the execution of the algorithm  corresponds to the concept of the execution of $A$. First, an \emph{execution fragment} $\alpha$ of $A$ is a finite or infinite sequence $\sigma_0, a_1, \sigma_1, a_2, \sigma_2, \ldots $, where each $\sigma_i$ belong to $\states{A}$ and $a_i$ belongs to 
$\trans{A}$. An \emph{execution} of $A$ is an execution fragment such that $\sigma_0 \in \startstates{A}$.
	%
	We use the notation $trace(\alpha)$ to denote the sequence of external  actions in $\alpha$; and by $trace(\alpha) | A_i$  to denote the sequence of external actions in $trace(\alpha)$ that belongs to automaton $A_i$. 

	 If $\alpha$  is a finite execution and $\beta$ is an execution fragment, such that,  $\beta$ starts with the final state of $\alpha$ then we use the symbol $\alpha \circ \beta$ to denote execution fragment obtained as a result of concatenation of  execution fragments $\alpha$ and $\beta$. The  set of locally controller actions in an automaton can be partitioned into tasks. Moreover, in the case of an execution, if the execution is infinite and events from each class occurs infinitely often, and if the execution is finite and  if none of the  events from any of the classes is enabled then the execution is called \emph{fair}. If $\epsilon$ and $\epsilon'$  are two execution fragments such that at some automaton $A$ they  are the same, i.e., $\epsilon|A = \epsilon'|A$,  then we use  the notation 
   $\epsilon \stackrel{A}{\sim} \epsilon'$.  When the automaton is clear from the context, for the sake of brevity we drop the symbol for the automaton over the $\sim$.
Below we add some useful  theorems are useful related to  executions of a composed I/O Automata~\cite{Lynch1996}. 


\begin{theorem} \label{thm:paste}
Let $\{A_i\}_{i \in  I}$ be a compatible collection of automata and let $A = \Pi_{i \in I}A_i$. Suppose $\alpha_i$ is an execution of $A_i$ for every $i \in I$, and suppose $\beta$ is a sequence of actions in $ext(A)$ such that 
$\beta | A_i = trace(\alpha_i)$ for every $i \in I$. Then there is an execution $\alpha$ of $A$ such that $\beta = trace(\alpha)$ and $\alpha_i = \alpha | A$, for every $i \in I$.
\end{theorem}

\begin{theorem} \label{thm:extension}
Let $A$ be any I/O automaton.
\begin{enumerate}
\item [1.] If $\alpha$ is a finite execution of $A$, then there is a fair execution of $A$ that starts with $\alpha$.
\item [2.]  If $\beta$ is a finite trace of $A$, then there is a fair trace of $A$ that starts with $\beta$.  
\item [3.] If $\alpha$ is a finite execution of $A$  and $\beta$ is any finite or infinite sequence of input actions of $A$, then there is a fair execution  $\alpha \circ \alpha'$ of $A$ such that the sequence of input actions in $\alpha'$ is exactly $\beta$.
 \item [4.]  If $\beta$ is a finite trace of $A$ and $\beta'$ is any finite or infinite sequence of input actions of $A$, then there is a fair execution $\alpha \circ \alpha'$ of $A$ such that $trace(\alpha) = \beta$ and such that the sequence of input actions in $\alpha'$ is exactly $\beta'$.
\end{enumerate}
\end{theorem}

The following useful  claim is adopted from  Chapter 16 of \cite{Lynch1996}.
\begin{claim}\label{claim:reorder}
Suppose we have an automaton $A = \Pi_{i=1}^k A_i$ where $A$ is composed of the compatible collection of automata $A_i$, where $i \in \{1, \cdots, k\}$.
Let $\beta$ be a fair trace of $A$ then we define an irreflexive partial order $\rightarrow_{\beta}$ on the actions of $\beta$
as follows. If $\pi$ and $\phi$ are events in $\beta$, with $\pi$ preceding $\phi$, then we say $\phi$ depends on $\pi$, which we denote as $\pi \rightarrow_{\beta}\phi$, if one of the following holds:  
\begin{enumerate}
\item[1.] $\pi$ and $\phi$ are actions at the same automaton;
\item[2.] $\pi$ is some $send(\cdot)_{j, i}$ at some $A_j$ and $\phi$ is some $recv(\cdot)_{j,i}$ at $A_i$; and
\item[3.] $\pi$ and $\phi$ are related by a chain of the relations of items 1. and 2.
\end{enumerate}
Then if $\gamma$ is a sequence obtained by reordering the events in $\beta$ while preserving the $\rightarrow_{\beta}$, then $\gamma$ is also a fair trace of $A$.
\end{claim}

\begin{theorem} \label{thm:fairtrace}
Let $\{A_i\}_{i \in I}$ be a compatible collection of automata and let $A = \Pi_{i=1}^k A_i$. Suppose $\alpha_i$ is a fair
execution of $A_i$ for every $i \in I$, and suppose $\beta$ is a sequence of actions  in $ext(A)$ such that $\beta|A_i=trace(\alpha_i)$
 for every $i \in I$. Then there is a fair execution $\alpha$ of $A$ such that $\beta=trace(\alpha)$ and $\alpha_i = \alpha|A$ for 
 every $i\in I$.
\end{theorem}

\subsection{Data type} \label{datatype}
In this section, we formally describe the  data type, which we denote as \blue{$\mathcal{O}_T$},   for the transaction processing systems considered in this paper. 
We assume there is a set of $k$ objects,  where $k$ is some positive integer, and  $o_k$ denotes the $k^{th}$ object. 
Object $o_k$ stores a value from some non-empty domain $V_k$ and supports two types of operations: \emph{read} and \emph{write} operations.
 A read operation on object $o_k$, denoted by $\readop{o_k}$, on completion returns the value stored in $o_k$.
  A write operation on $o_k$ with some value $v_k$ from $V_k$, denoted as $\writeop{o_k}{v_k}$,  on completion,  updates the value of  $o_k$.


\sloppy A {\sc write} transaction  consists  of a subset of $p$ distinct write operations for  a  subset of $p$ distinct objects, where $1 \leq p \leq k$.   For example, a {\sc write} transaction with  the set of operations   $\{ \writeop{o_{i_1}}{v_{i_1}}$, $\writeop{o_{i_2}}{v_{i_2}} \cdots \writeop{o_{i_p}}{v_{i_p}} \}$, means  value $v_{i_1}$  is to be written to object $o_{i_1}$,   value $v_{i_2}$ to object $o_{i_2}$, and so on.
 We denote such a {\sc write} transaction as $WRITE( (o_{i_1}, v_{i_1}), (o_{i_2}, v_{i_2}), \cdots, $
 $(o_{i_p}, v_{i_p})  )$. 

 
 A {\sc read} transaction consisting of a set of read operations is denoted as 
  $READ(o_{i_1}, o_{i_2}, \cdots, o_{i_q})$,  where $o_{i_1}, o_{i_2}, \cdots, o_{i_q}$ is a set of distinct objects,  $q$ is any positive integer, $1 \leq q \leq k$, which upon completion  returns the  values 
 $(v_{i_1}, v_{i_2}, \cdots, v_{i_q})$, where  $v_{i_j} \in V_{i_j}$  is the value returned by $\readop{o_{i_j}}$, for any $i_j  \in  \{i_1, i_2, \cdots i_q\}$ and  $1 \leq {i_1} < {i_2}< \cdots <  {i_q} \leq k$. 

 
Formally, we define the value type used in this paper for a  $k$ object data-type  as follows: 
\begin{enumerate}
\item [$(i)$] a tuple $(v_1, v_2, \cdots, v_k) \in \Pi_{i=1}^{k} V_i$, where $V_i$ is a domain of values, for each $i \in \{1, \cdots, k\}$;
\item [$(ii)$] an initial value $v^0_i$, $v^0_i \in V_i$  for each object $o_i$; 
\item[$(iii)$] \emph{invocations}: $READ(
 o_{i_1},  o_{i_2}, \cdots, o_{i_p})$  and  $WRITE((o_{i_1}, v_{i_1}), $
 $(o_{i_2}, v_{i_2}), \cdots, $ $(o_{i_p}, v_{i_p}))$,
  such that $v_{i_j}  \in V_{i_j}$ for any  $i_j  \in  \{i_1, i_2, \cdots i_p\}$  where  $1 \leq {i_1} < {i_2}< \cdots <  {i_p} \leq k$ and $p$ is   some integer with $1 \leq p \leq k$; 
\item[$(iv)$] \emph{responses}:    a tuple $(v_1, v_2, \cdots, v_k) \in \Pi_{i=1}^{k} V_i$ and $ok$; and 
\item [$(v)$] for any subset of  $p$ objects we  define  $f: invocations \times V \rightarrow responses \times V$, such that:
\begin{enumerate} 
\item $f( READ(o_{i_1}, o_{i_2}, \cdots, o_{i_p}),$ $ (v_1, v_2, \cdots, v_k) ) = (  (v_{i_1}, v_{i_2}, \cdots, v_{i_p}), (v_1, v_2, \cdots, v_k) )$; and 
\item $f( WRITE((o_{i_1}, u_{i_1}), (o_{i_2}, u_{i_2}), \cdots, $ $(o_{i_p}, u_{i_p})),  $ $ (v_1, v_2,$ $ \cdots, v_k)   ) = (ack,  (w_1, w_2,  \cdots, w_k) )$, where  for any $i$,  $w_i =  u_i$ if  
$i \in \{ i_1, i_2,  \cdots, i_p \}$, and for all other values of $i$,  $w_i=v_i$.
\end{enumerate} 
\end{enumerate}



\begin{figure}[!ht]
      \centering
         \includegraphics[width=1.0\textwidth]{architecture1_1.png}  \vspace{-2.5em}
         \caption{The architecture of a typical web service with clients and servers inside a datacenter. 
        
        
         } 
         \label{fig:architecture1}
 \end{figure}
 \begin{figure}[!ht]
      \centering
         \includegraphics[width=1.0\textwidth]{architecture2_1.png}  \vspace{-2.5em}
         \caption{
         The architecture of a typical web service with clients, servers, and 
        
         the communication channels inside a datacenter is modeled as a collection of I/O automata.
         } 
         \label{fig:architecture2a}
 \end{figure}

\subsection{System Model}
In our system,   we assume there are $\ell$ writers, for some $\ell \geq 1$;   $m$ readers, for some $m \geq 1$,  and  $k$ servers for some $k \geq 1$.
We denote the set of writers as  $\mathcal{W}$, which essentially  consists of the writer identifiers $w_1, w_2 \cdots w_{\ell}$. The set of readers,  with ids  $r_1, r_2 \cdots r_{m}$, is denoted as 
  $\mathcal{R}$.  The set of servers  $\mathcal{S}$ consists of the server  identifiers   $s_1, s_2\cdots s_k$. The servers $s_1, s_2\cdots s_k$  manage the objects $o_1, o_2, \cdots, o_k$, respectively,  in particular,  server $s_i$ is responsible for storing object $o_i$, for any  $i$, $1 \leq i\leq  k$. 

Communications between processes during the executions are point-to-point and are assumed to be reliable and asynchronous.  The communications are  
modeled with $Channel$ I/O automata and  are carried out via $send$ and $recv$ actions at the source and 
destination processes. For example, in Figure~\ref{fig:architecture2a}, the reader $r_1$ automaton sends,  via the action $send(m)$,  
some  message $m$, from some alphabet $\mathcal{M}$,  to server $s_1$ through the channel automaton $Channel_{r_1, s_1}$, and $s_1$ receives it though the action 
$recv(m)$. Similarly, the message $m'$, $m' \in \mathcal{M}$,  is transmitted from $s_1$ to $r_1$, through the  channel automaton $Channel_{s_1, r_1}$, via 
the actions $send(m')$ at $s_1$,  and   finally received at $r_1$ via the action $recv(m')$.

The schematic flow of a typical, but simplified,  webpage request from a service hosted in a datacenter is shown in Figure~\ref{fig:architecture1}. 
An end user sends a webpage request to a front-end client $r_1$. Upon receiving it $r_1$ generates a {\sc read} transaction $R$, 
which consists of a set of read operations and is  invoked via a $\INV{R}$ action at the client, which is essentially input to the client from the end user. The goal of 
these operations  is to read  a subset of the 
data objects by contacting the respective managing servers. 
The operations in a  transaction are carried out between the invocation and response actions of the transaction without any 
particular order of execution among the operations. Any operation $op$  begins with an  invocation action, $\inv{op}$, at the 
relevant client,  and ends with a response action $\resp{op}$, also at the client. 
 Once the front-end client completes the read operations, then $r_1$  synthesizes the webpage with the data retrieved by the read operations, and responds to the end user 
 request through the response action $\RESP{R}$ at the  
 client $r_1$.\footnote{In a typical production system the depth of the transactions (due to nested transactions) is more than 
 one~\cite{Lloyd2015}, however, we assume only transactions of depth one as in~\cite{SNOW2016}.} Similarly, the  update request 
 from the end user can be thought of a {\sc write} transaction $W$, consisting of a set of write operations for individual objects,  to update the set of object values,  initiated via an  invocation action $\INV{W}$ at the client. Then the writes operations are carried out by the client, and once they complete, the   transaction completes with the response action $\RESP{W}$, at the client.


	A transaction $\pi$ is \emph{incomplete} in an execution $\alpha$  when the action $\INV{\pi}$  does not have the $\RESP{\pi}$  in $\alpha$; otherwise, we say that $\pi$ is \emph{complete} in $\alpha$.  
	In an execution, we say that a transaction (read or write) $\pi_1$ {\em precedes} another transaction $\pi_2$ (denote as $\pi_1 \rightarrow \pi_2$),  if the response action $\RESP{\pi_1}$  precedes the invocation action  $\INV{\pi_2}$.  Two transactions
	are {\em concurrent} if neither precedes the other. 

 If in any execution of the system every  client initiates a new transaction only after the previous transactions initiated at the same client have completed, then  we say the execution is  {\em well-formed}.


 \remove{
The {\sc write} transactions issued by a writer consists  of a subset of $p$,  $1 \leq p \leq k$,  distinct write operations for corresponding subset of the objects,   For example, a {\sc write} transaction may comprise of  the set of operations   $\{ \writeop{o_{i_1}}{v_{i_1}}$, $\writeop{o_{i_2}}{v_{i_2}} \cdots \writeop{o_{i_p}}{v_{i_p}} \}$, meaning  value $v_{i_1}$  is to be written to object $o_{i_1}$,   value $v_{i_2}$ to object $o_{i_2}$, and so on.
 We denote such a {\sc write} transaction as $WRITE( \writeop{o_{i_1}}{v_{i_1}}, $$\writeop{ o_{i_2}}{v_{i_2}}, \cdots, $
 $ \writeop{o_{i_p}}{ v_{i_p}}  )$. Similarly,  a {\sc read} transaction, denoted by $READ$, omitting the list of operations to avoid notational clutter, may consist of a set of read operations. For example, a {\sc read} transaction may comprise of the set of read operations as 
  $\{\readop{o_{i_1}}, $$\readop{v_{i_2}}, \cdots, $
 $ \readop{ o_{i_q}}  \}$, for some $1 \leq q \leq k$ which upon completion  returns the  values 
 $(v_{i_1}, v_{i_2}, \cdots, v_{i_q})$, where $v_{i} \in V_i$, for any $i  \in  \{i_1, i_2, \cdots i_q\}$, is the value returned by $\readop{o_i}$, from some domain $V_i$  of  the values for  object $o_i$. 
 }
 


 
 \remove{
\begin{figure}[!tbp]
  \centering
  \begin{minipage}[b]{0.50\textwidth}
    \includegraphics[width=\textwidth]{figures/architecture1_1.png}
  \end{minipage}
  \hfill
  \begin{minipage}[b]{0.49\textwidth}
    \includegraphics[width=\textwidth]{figures/architecture2_1.png}
 
  \end{minipage}
  \label{fig:architecture}
   \vspace{-1.8em}
   \caption{The architecture of a typical web service with clients and servers inside a datacenter. The clients, servers and the communication channels are modeled as automata}
     \vspace{-0.8em}
\end{figure}
}
 \remove{
\begin{figure}[!ht]
      \centering
         \includegraphics[width=1.0\textwidth]{figures/architecture1.jpg}  \vspace{-3.5em}
         \caption{The architecture of a typical web service with clients and servers inside a datacenter. The clients, servers and the communication channels are modeled as automata.
        
         } 
         \label{fig:architecture}
 \end{figure}
 \begin{figure}[!ht]
      \centering
         \includegraphics[width=1.0\textwidth]{figures/architecture2.jpg}  \vspace{-3.5em}
         \caption{The architecture of a typical web service with clients and servers inside a datacenter. The clients, servers and the communication channels are modeled as automata.
        
         } 
         \label{fig:architecture}
 \end{figure}
 \vspace{-0.8em}
}
\subsection{SNOW Properties}   The SNOW properties for a transaction processing system can be described by requiring that any fair execution of the system satisfies the following four properties: $(i)$ \emph{Strict Serializability} (S), which means there is a total ordering  of the transactions such that  the resulting execution  seems to occur at  a single machine atomically; $(ii)$ \emph{Non-Blocking Operations} (N) property, which  means that the servers respond immediately, without waiting for any input from other processes, to read requests for the read operations, which belong to the {\sc read} transactions; $(iii)$ \emph{One Response Per Read} (O) property  requires that any read operation  consists of one-round trip of communication with a server,  and also,  the server responds with a message that contains exactly  one version of the  object value; and $(iv)$ \emph{{\sc write} transactions that Conflict} (W) implies the  existence of concurrent {\sc write} transactions that update the data objects  while {\sc read} transactions are in progress.  Below we describe the individual properties of the SNOW properties in more detail.

\paragraph{Strict serializability} By \emph{strict serializability}~\cite{HW90}, we mean each {\sc write} or {\sc read} transaction is executed atomically, at some point in an execution  between the invocation and response events.
In other words,  for  each transaction, we can associate a 
serialization point between the invocation and response actions, such that all  the read operations return values that are consistent with the ordering of the serialization points.

\paragraph{Non-blocking reads}Consider a {\sc read} transaction initiated by a read client $r$ and a read operation in it to read 
the value of  an object $o_i$ managed by some server $s_i$. The read operation involves $r$ communicating a \emph{send value} message   to $s_i$ requesting
the stored value of $o_i$. The \emph{non-blocking} property means that the server responds to the read request without waiting for any external input event, such as the arrival of messages, any mutex operations, time, etc. This property ensures that {\sc read} transactions are delayed only due to delay of  messages between $r$ and $s_i$.
Below we define the non-blocking nature of any  server's response  to a read request from a reader as follows.
\begin{definition}
If $\alpha$ is a fair execution of some server automaton for a server $s$ and action  $recv(m^r)_{r,s}$ appears in $\alpha$, where $r$ is a reader automaton and 
$m^r$ is a read value request to server $s$, and no other input actions follow  $recv(m^r)_{r,s}$,  then eventually, the action $send(v_i)_{s, r}$ occurs  in $\alpha$.
\end{definition}

\paragraph{One-response read operations } The \emph{one-response} property requires that each read operation, during any
{\sc read} transaction, completes in one round of client to server communication and receives exactly one version of the object value from the corresponding server. A round consists of 
a read  request from the client initiating the read operation to the server, and subsequently, the server sending only one version of the object value  in its response. The \emph{one-round} property is imposed to reduce  the number of messages between the client and the server during a read operation, and hence reducing the latency of the {\sc read} transaction. The \emph{one-version} property is added to reduce the amount of data transmitted during the read operation and hence reduce  latency of read operations, which also means lowering latency for the  {\sc read} transaction.

\paragraph{Concurrent and conflicting writes} The \emph{conflicting}, or \emph{concurrent writes}
 property states that {\sc read} transactions complete even in the presence of concurrent {\sc write}
  transactions, where the write operations  might update some objects that are also being read by read operations in {\sc read}. 
  This shows that {\sc read} transactions can be invoked at any point, even in the presence of ongoing {\sc write}
   transactions.  Note that the liveness of any {\sc write} transaction is not implied by any of 
   the SNOW properties;  however, for useful practical systems   the  {\sc write}s  must eventually complete. 
  

  
  
    Therefore, we assume that every {\sc write} 
    transaction eventually completes via the $RESP$ event, and think of this constraint as a part of the W property.  
	
\paragraph{The SNOW Theorem\cite{SNOW2016}}  The theorem states that \emph{no read-only transaction algorithm provides all of the SNOW properties.}	
	
\subsection{ One-version property} 
Motivated by the impossibility result of the SNOW theorem,  we propose  in Section~\ref{mwmr},  
an algorithm for transaction processing systems under constraints weaker than the SNOW properties.
With this in mind, we introduce a weaker version of the O property, denote it as ``o'',  where during a read operation the  server returns exactly one object value but there exists a finite bound on the number of rounds of communication between the client and the  server. We use the acronym SNoW to denote the S, N, o and W properties.  Moreover,  it is easy to realize that if an algorithm satisfies the SNoW properties then {\sc read} transactions always complete, and hence, {\sc read}'s are always live. This is because the N and o properties imply that the server must immediately respond to a read request due to a read operation with exactly one object value without waiting in expectation of incoming messages, and 
there  a fixed upper bound on the number of such rounds for a {\sc read}.

\remove{
\subsection{ To be deleted : Liveness of Write and Read-Only Transactions}
By liveness, we mean that during any well-formed execution of the algorithm,  any  transaction  initiated at any non-faulty client eventually completes. It is easy to realize that if an algorithm satisfies the SNOW properties then {\sc read} transactions always complete, and hence, always live. On the other hand, the liveness of a {\sc write} transaction is not guaranteed by the SNOW properties, therefore, liveness of write  transactions needs to be imposed explicitly.
}

\section{Impossibility of SNOW properties with two clients with restricted communication }\label{two-client}

In this section, we  prove that for a two-client transaction processing system with at least two objects it is impossible to design an 
algorithm that satisfies  the SNOW properties.We prove our result by showing 
 a contradiction. 
 For the model consider  in this section,  we assume that between every pair of client and server, or every pair of servers there are two  communication channels, one  in each direction; however, there are no  communication channels between any pair of clients Fig~\ref{fig:architecture2a}.
 
 
 Consider a system consisting of two servers,  $s_1$ and $s_2$, and two clients, a reader  $r$, which initiates only 
 {\sc read} transactions,  and a writer $w$, which initiates only {\sc write} transactions.  Servers $s_1$ and $s_2$ store  values for 
 objects $o_1$ and $o_2$, respectively.  The values stored in $o_1$ and $o_2$ belong to the domains $V_1$ and $V_2$, respectively;
the  initial values of $o_1$ and $o_2$ are $v_1^0$ and $v_2^0$, respectively. 
We denote the automata for servers $s_1$ and $s_2$ by $s_1^A$ and $s_2^A$, respectively, and the automata for the clients  $r$ and $w$ by $r^A$ and $w^A$, respectively.   
 We denote by $S_1$  the subsystem consisting of $s_1$, $s_2$ and $w$,  and  by $S_1^A$  the  automata composed of  $s_1^A$, $s_2^A$ and $w^A$, i.e., $s_1^A \times s_2^A \times w^A$. 
 Also, we  denote by $\mathcal{A}$, which can also be interpreted as the algorithm, the automaton representing the entire system consisting of $S_1^A$ and $r^A$ (i.e., $s_1^A \times  s_2^A$ $ \times w^A$ $ \times r^A$).  
 We assume that between any client $c$, 
 $c \in \{r, w \}$ and any server $s$,  $s \in \{s_1, s_2\}$ there are  channel automata $Channel_{c, s}$ and $Channel_{s, c}$.
Here, we consider only fair  executions of ${\mathcal A}$.
For contradiction, we  also assume that  any fair execution of $\mathcal{A}$  respects  the SNOW properties. 
 Also, we assume that in an execution $\epsilon$ of $\mathcal{A}$  we can identify each transaction with an unique identifier.

\sloppy Consider an execution of ${\mathcal A}$ with  two transactions in it as:   a {\sc write} transaction  $W \equiv $ $WRITE($$ (o_1, v_1^1),  (o_2, v_2^1) )$ initiated by  $w$, where $v_1^1 \neq v_1^0$ and $v_2^1 \neq v_2^0$; and a {\sc read} transaction   $R \equiv READ$$(o_1, o_2)$, initiated by $r$.  Let us denote by 
$op_1^r$ and $op_2^r$  the read operations $\readop{o_1}$ and  $ \readop{o_2} $, respectively.
 We assume that the  patterns of  sequences of invocations of transaction,  the times of these invocations,  and delays in local computation and message deliveries,  are controlled by an omniscient entity. 
 which we refer to as the \emph{adversary}. The assumption of such an adversary is in accordance with  the asynchronous nature of the model. 
This is also important in real systems, because such executions are possible to occur and thus important for making  the system safe.
\paragraph{Notations and Definitions:}
We  introduce  the following notations and definitions in the context of an execution $\epsilon$, of $\mathcal{A}$, with transactions $R$ and $W$ in it,
 where  $ j \in \{1, 2\}$:
\begin{enumerate}

\item $\send{m_j^{r}}{r, s_j}$: an  output action at $r^A$,  which sends a message $m_j^{r}$ from reader $r$ to server $s_j$, requesting the value for $o_j$;
\item $\recv{m_j^{r}}{r, s_j}$: an input action at $s_j^A$, that receives the message $m_j^{r}$, sent from $r$;
\item $\send{v_j}{ s_j, r}$: an output action at $s_j^A$,  that  sends value $v_j$, for   $o_j$, to $r$.
\item $\recv{v_j}{ s_j, r}$: an input action at $r^A$,  to receive a message $v_j$ from $s_j$ at  $r^A$.
\item  \emph{Non-blocking fragments $\frag{i}{\epsilon}$, $i \in \{1, 2\}$.}
 Suppose there is a fragment of  execution  in $\epsilon$  where the first action is   $recv(m_i^r)_{r, s_i}$ and  the last action is 
 $send(v_i)_{s_i, r}$ , both of which  occur  at $s_i^A$. Moreover, suppose there is  
 no other input action at $s_i^A$ in this fragment. Then we call this execution fragment 
   a \emph{non-blocking response fragment} for $op_i^r$ at  $s_i^A$.  We use the notation  $\frag{i}{\epsilon}$ to denote this fragment of 
  execution of $\epsilon$.



 \item  We use the notations $R(\epsilon)$ and $W(\epsilon)$ to denote the transactions $R$ and $W$, in $\epsilon$. When the underlying execution is clear from the context we simply use $R$ and $W$.

 \item If the non-blocking fragment $\frag{1}{\epsilon}$ appears in $\epsilon$ such that $recv(m^r_2)_{r, s_2}$, at $s_2^A$,  does not occur before
 $\frag{1}{\epsilon}$ completes and $\epsilon$ is of the form 
 $\finiteprefix{\ell-1}{\ell} \circ \frag{1}{\epsilon} \circ \frage{S}{\epsilon}{}$, where $\frage{S}{\epsilon}{}$ is any continuation of the execution, then we denote $\finiteprefix{\ell-1}{\ell} $ by $\prefix{\epsilon}$.
 
\item \sloppy If $\epsilon$ is of the form  
 $\finiteprefix{\ell-1}{\ell}  \circ \frag{1}{\epsilon} \circ \kappa \circ \frag{2}{\epsilon} , a_p, \sigma_p, \ldots$  or 
 $\finiteprefix{\ell-1}{\ell}  \circ \frag{2}{\epsilon} \circ \kappa \circ \frag{1}{\epsilon} \circ \frage{S}{\epsilon}{}$, where  
 $\ell$ is a positive integer, 
 $\kappa$ is a segment of $\epsilon$,  possibly even of length zero and $\frage{S}{\epsilon}{}$ is any suffix part of the execution 
 then we denote $\finiteprefix{\ell-1}{\ell} $ by $\prefix{\epsilon}$. Clearly,  we can write $\epsilon$ as $\prefix{\epsilon} \circ \frag{1}{\epsilon}\circ \kappa \circ \frag{2}{\epsilon} \circ \suffix{\epsilon}$ or $\prefix{\epsilon} \circ \frag{2}{\epsilon}\circ \kappa \circ \frag{1}{\epsilon} \circ \suffix{\epsilon}$.

\end{enumerate}


Now we describe the set of actions corresponding to the  {\sc read} transactions in a fair execution $\epsilon$ of $\mathcal{A}$. 

   Clearly,  in $\epsilon$, the actions $\inv{op_i^r}$ and $\resp{op_i^r}$ appear between the actions $\INV{R}$ and $\RESP{R}$. The  action  $\inv{op_i^r}$ is followed by action $send(m_i^r)_{r, s_i}$, which is 
 for  sending  the read object value request to server $s_i$. This request $m_i^r$ is communicated to $s_i$, via the channel automaton $Channel_{r, s_i}$.  Automaton 
 $s_i^A$ eventually receives the request 
  via the action   
   $recv(m_i^r)_{r, s_i}$,  and subsequently, responds back to $r$, with object value $v_i$,  through the action $send(v_i)_{s_i, r}$.  Next, 
   value $v_i$, $v_i \in V_i$,  communicated by the automaton  $Channel_{s_i, r}$,  is 
received at $r$ via the action  $recv(v_i)_{s_i, r}$, and finally,  $op_i^r$ completes with  response action $\resp{op_i^r}$ and returns $v_i$ to $r^A$. 



Here, we give a high-level idea of our proof,  which is based  on the existence of a sequence of fair executions of $\mathcal{A}$, eventually leading to a  execution  of ${\mathcal A}$ that contradicts  the S property.

 First,  we show the existence of an execution $\alpha$ of $\mathcal{A}$ where 
$R$ is invoked after $W$ completes, where the  send actions $send(m_1^r)_{r, s_1}$ and $send(m_2^r)_{r, s_2}$  at the  $r^A$,  occur consecutively, 
in  $P(\alpha)$. 
 Then we show $\alpha$  can be written in the form  
$\prefix{\alpha} \circ \frag{1}{\alpha}$ (Figure~\ref{fig:execution1} $(a)$, Lemma~\ref{lem:exec_alpha}). 
 Based on $\alpha$, we show the existence of  another  execution $\beta$, of $\mathcal{A}$, which can be written in the form $\prefix{\beta} \circ \frag{1}{\beta} \circ \frag{2}{\beta}$,   by extending $\alpha$ with an execution fragment $\frag{2}{\beta}$ such that, $\frag{1}{\beta} \stackrel{s_1}{\sim} \frag{1}{\alpha}$
  (Figure~\ref{fig:execution1} $(b)$; Lemma~\ref{lem:exec_beta}).
Note that in  any arbitrary extension (as a fair execution) of $\beta$,   eventually  $R$ returns $(v_1^1, v_2^1)$.
  %
Next, from $\beta$,  we show the existence of an execution $\gamma$, of $\mathcal{A}$, of the form  $\prefix{\gamma} \circ \frag{1}{\gamma} \circ \frag{2}{\gamma}$,  
 where the send actions $send(m_1^r)_{r, s_1}$ and $send(m_2^r)_{r, s_2}$  at  $r^A$, occur before $W$ is invoked   (Figure~\ref{fig:execution1} $(c)$; Lemma~\ref{lem:exec_gamma}), but the fragments 
$\frag{1}{\gamma}$  and $\frag{2}{\gamma}$
occur after $\RESP{W}$, as in $\beta$.
From $\gamma$ we show the existence of a fair execution $\delta$, of $\mathcal{A}$, 
of the form  $\prefix{\eta} \circ \frag{1}{\eta} \circ \frag{2}{\eta}\circ \suffix{\eta}$, where 
  $R$ responds with $(v_1^1, v_2^1)$.


 
  
   %
    Finally, starting with  $\eta$ we create a sequence of fair  executions $\delta (\equiv \eta)$, $\delta^{(1)}$, $\cdots$ $\delta^{(f)}$, of $\mathcal{A}$, 
     where in each of them $R$ responds with $(v_1^1, v_2^1)$  (Figure~\ref{fig:execution2} $(e)$ and $(g)$; Lemma~\ref{thm:two-snow}). Additionally,  for any $\delta^{(i)}$, the fragments   $\frag{1}{\delta^{(i)}}$ and
    $\frag{2}{\delta^{(i)}}$  appear in the execution before $\delta^{(i-1)}$.
   
    From $\delta^{(f)}$ we show the existence of  a fair execution $\phi$ (see Figure~\ref{fig:execution2} $(h)$),  of $\mathcal{A}$, where $R$ completes by returning  
    $(v_1^1, v_2^1)$ even before $W$ begins, which is violation of the  property $S$.

  
  Now, we state and prove the the relevant lemmas. The following lemma states that there is a finite execution of ${\mathcal A}$ where $R$ begins after  
  $W$ completes where the two send actions $send(m_1^r)_{r, s_1}$ and $send(m_2^r)_{r, s_2}$  occur before either of the servers $s_1$ and  $s_2$ 
  receives the messages $m_1^r$ or $m_2^r$  from $r$;  also,  server $s_1$ responds to $r$ in a non-blocking manner (execution $\alpha$ in Figure~\ref{fig:execution1} $(a)$).  
\begin{lemma}\label{lem:exec_alpha} 
There exists a finite execution $\alpha$ of $\mathcal{A}$ that contains transactions $R(\alpha)$ 
   
and $W(\alpha)$ where $\INV{R}$ appears after $\RESP{W}$ and the following conditions hold:
\begin{enumerate}
\item[$(i)$] The actions $send(m_1^r)_{r, s_1}$ and  $send(m_2^r)_{r, s_2}$ appear consecutively in $trace(\alpha)|r^A$; and 
\item[$(ii)$]   $\alpha$ contains the execution fragment  $\frag{1}{\alpha}$.
\end{enumerate} 
\end{lemma}


\begin{proof}
Consider a finite  execution fragment  of $\mathcal{A}$ with a completed transaction $W$, where  after $W$ 
completes  the adversary invokes $R$, i.e., $\INV{R}$ occurs.
 Note that each of the  read operations $op_1^r$ and $op_2^r$,  in $R$,  can be invoked by the adversary at any point in the execution.  
 Following $\INV{R}$,  the adversary introduces the invocation action $\inv{op_1^r}$;  by the O property of the read operations of $\mathcal{A}$  
the action $send(m_1^r)_{r, s_1}$ eventually occurs. Next, the adversary introduces 
 $\inv{op_2^r}$ and also, delays the arrival of  $m_1^r$ until  action $send(m_2^r)_{r, s_2}$ eventually occurs, 
 which  must occur in accordance with  the property O  of read operations. Let us call this finite execution $\alpha^0$. 
 
 Next, suppose at the end of $\alpha^0$  the adversary delivers the message $m_1^r$, which has been delayed so far,  via the action  $recv(m_1^r)_{r, s_1}$, 
 at  $s_1^A$,   but  it delays any  other input actions at $s_1^A$. Note that by the $N$ property of read operations $s_1^A$ eventually responds with  $send(v_1)_{s_1, r}$, with one value $v_1$ by O property,  where $v_1 = v_1^1$ by the S property, since $R$ begins after $W$ completes. 
 Let us call this execution $\alpha$. Note that $\alpha$ satisfies conditions $(i)$ and $(ii)$ by the design of the execution.
\end{proof}

 %

   The following lemma states that there is an execution $\beta$ of ${\mathcal A}$ where $R$ begins after  $W$ completes where the two send events at $r^A$ occurs before  $\frag{1}{\beta}$, which in turn, occurs before $\frag{2}{\beta}$ (execution $\beta$ in Figure~\ref{fig:execution1} $(b)$).  
   
  
\begin{lemma}\label{lem:exec_beta} 
There exists an  execution $\beta$ of $\mathcal{A}$ that contains transactions $R$ and $W$ where $\INV{R}$ appears after $\RESP{W}$ and the following conditions hold:
\begin{enumerate}
\item[$(i)$] The actions $send(m_1^r)_{r, s_1}$ and  $send(m_2^r)_{r, s_2}$ appear consecutively in $trace(\beta)|r^A$; and
\item[$(ii)$]   $\beta$ contains the execution fragment  $\frag{1}{\beta} \circ \frag{2}{\beta}$.
\end{enumerate} 
\end{lemma}
\begin{proof}
Consider the  execution $\alpha$ of $\mathcal{A}$ as constructed in Lemma~\ref{lem:exec_alpha}.  
At the end of the execution fragment $\alpha$,  the adversary  delivers the previously delayed message
 $m_2^r$, which is sent via the action $send(m_2^r)_{r, s_2}$,  by  introducing the action $recv(m_2^r)_{r, s_2}$. The adversary then delays any other  input action in $\mathcal{A}$. By the N property,  
server $s_2^A$ must respond to $r^A$, with some value $v_2$,  and hence 
the output action $send(v_2)_{s_2, r}$ must eventually occur at $s_2^A$.  
Let us call this finite execution as $\beta$. Note that $\beta$ satisfies the  properties $(i)$ and $(ii)$ in the statement of the lemma.
\end{proof}


 The following result shows  that starting with $\beta$  there is an execution 
 $\gamma$  of ${\mathcal A}$ where  $R$ is initiated before $W$ is initiated , also, the send events 
  $send(m_1^r)_{r, s_1}$ and  $send(m_2^r)_{r, s_2}$  occur before $\INV{W}$ (execution  Figure~\ref{fig:execution1} $(c)$) and the 
   messages $m_1^r$ and $m_2^r$ from $r^A$ reach the  servers $s_1$ and $s_2$, respectively,  after the action  $\RESP{W}$.  

\begin{lemma}\label{lem:exec_gamma} 
There exists a fair execution $\gamma$ of $\mathcal{A}$ with transactions $R$ and $W$ where the action  $\INV{R}$ appears before $\INV{W}$ and $\RESP{R}$ appears after  $\RESP{W}$,  and the following conditions hold for $\gamma$:
\begin{enumerate}
\item[$(i)$] The actions $send(m_1^r)_{r, s_1}$ and  $send(m_2^r)_{r, s_2}$  appear before $\INV{W}$ and they appear consecutively in $trace(\gamma)|r^A$;
\item[$(ii)$]   $\gamma$ contains the execution fragment  $\frag{1}{\gamma} \circ \frag{2}{\gamma}$; and 
\item[$(iii)$] action $\RESP{W}$ occurs before $\frag{1}{\gamma}$.
\end{enumerate} 
\end{lemma}


\begin{proof}
Consider the execution $\beta$ of $\mathcal{A}$  as in Lemma~\ref{lem:exec_beta}. Note that $\beta$
is an execution of the composed automaton $\mathcal{A}$ ($\equiv S_1^A \times r^A$).  In $\beta$,  the actions 
 $send(m_1^r)_{r, s_1}$ and   $send(m_2^r)_{r, s_2}$ occur at $r^A$; and following that,  the actions 
 $recv(m_1^r)_{r, s_1}$, $recv(m_2^r)_{r, s_2}$, $send(v_1)_{s_1, r}$ and  $send(v_2)_{s_2, r}$ occur at $S_1^A$. 
 Consider the executions $\alpha_r \equiv \beta|r^A$ and  $\alpha_{S_1} \equiv \beta|S_1^A$. Let $s_{\beta}$ denote  $trace(\beta)$.
 
 In $s_{\beta}$, $send(m_1^r)_{r, s_1}$,  $send(m_2^r)_{r, s_2}$ appear after $\RESP{W}$, as in $trace(\beta)$. Let $s'_{\beta}$ be the sequence of
 external actions of $S_2^A$ which we construct from $s_{\beta}$ by moving $send(m_1^r)_{r, s_1}$,  $send(m_2^r)_{r, s_2}$ before $\INV{W}$, which  is also 
 an external action of $\mathcal{A}$, and leaving the rest of the actions in $s_{\beta}$ as it is.
 
 
 In $\beta$,  $\INV{R}$, $recv(v_1)_{ s_1, r}$ and  $recv(v_2)_{s_2, r}$ 
  are the only input actions at $r^A$, therefore,   $s'_{\beta} |r^A = trace(\alpha_r)$. 
  %
  On the other hand,  $recv(m_1^r)_{r, s_1}$, $recv(m_2^r)_{r, s_2}$ are the only input actions at $s_1^A$ ,
   therefore, $s'_{\beta} |S_1^A = trace(\alpha_{S_1})$.  Now, by Theorem ~\ref{thm:paste}, there exists an execution 
 $\gamma$ of $\mathcal{A}$ such that, $s'_{\beta} = trace(\gamma)$ 
 and $\alpha_r = \gamma|r^A$ and $\alpha_{S_1} = \gamma|S_1^A$. Therefore, 
 in $\gamma$, $send(m_1^r)_{r, s_1}$,  $send(m_2^r)_{r, s_2}$ appear before
  $\INV{W}$ (condition $(i)$) and since $s'_{\beta} = trace(\gamma)$ condition $(ii)$  holds. Conditions $(iii)$ holds trivially.
\end{proof}

In the following lemma we show  that in any fair  execution, of ${\mathcal A}$,  that is  an extension of either execution $\beta$ or execution  $\gamma$, as in  the preceding lemmas, $R$ eventually returns $(v_1^1, v_2^1)$.

\begin{lemma}\label{lem:exec_xi}
Let $\xi$  be a fair execution of $\mathcal{A}$ that is an   extension of the either  execution $\beta$ from Lemma~\ref{lem:exec_beta} or execution  $\gamma$ from Lemma~\ref{lem:exec_gamma},  then  $R(\xi)$  responds with $(v_1^1, v_2^1)$.
\end{lemma}

\begin{proof}
Note that in executions $\beta$ and $\gamma$,  the traces $trace(\beta)|s_1^A$  is a prefix of $trace(\gamma)|s_1^A$, since  $\beta$ ends with
$\frag{1}{\beta}$ and $\gamma$ ends with $\frag{2}{\gamma}$
Therefore, in both $\beta$ and $\gamma$, the  respective $send(v_1)_{s_1, r}$ actions have the same value for their  $v_1$'s. 
Now, in  any extended  fair execution $\eta$ of $A$, which starts 
with $\beta$ or $\gamma$, by the properties $N$ and $O$ the transaction $R$ completes;  and  by the property $S$,   $R$ returns  $(v_1^1, v_2^1)$.
Therefore,  $R(\xi)$  returns $(v_1^1, v_2^1)$.
\end{proof}

 In the following lemma, we show there exists an    execution $\eta$  of  
$\mathcal{A}$  of the form 
$\prefix{\eta}\circ \frag{1}{\eta} \circ \frag{2}{\eta} \circ \suffix{\eta}$
where  $\RESP{R}$ appears in  $\suffix{\eta}$  (Figure~\ref{fig:execution1} $(d)$) and 
$R(\eta)$ returns $(v_1^1, v_2^1)$. 

\begin{lemma}\label{lem:exec_delta} 
There exists a fair execution $\eta$ of $\mathcal{A}$ that contains transactions $R$ and $W$ where $\INV{R}$ appears before $\INV{W}$;  $\RESP{R}$ appears after  $\RESP{W}$ and the following conditions hold for $\eta$:
\begin{enumerate}
\item[ $(i)$] $\eta$ can be written in the form $\prefix{\eta}\circ \frag{1}{\eta} \circ \frag{2}{\eta} \circ \suffix{\eta}$, for some 
   $\prefix{\eta}$ and $\suffix{\eta}$;
\item[$(ii)$] The actions $send(m_1^r)_{r, s_1}$ and  $send(m_2^r)_{r, s_2}$  appear before  $\INV{W}$ and they appear consecutively in $trace(\eta)|r^A$;
\item[$(iii)$] action $\RESP{W}$ occurs before $\frag{1}{\eta}$; and 
 \item[$(iv)$] $R(\eta)$ returns $(v_1^1, v_2^1)$. 
\end{enumerate} 
\end{lemma}
\begin{proof}
Let $\gamma$ be a fair execution of $\mathcal{A}$, as described in Lemma~\ref{lem:exec_gamma}. 
 Let $\gamma^0$ be the execution fragment of $\gamma$
up to the action $send(v_2)_{s_2, r}$. Now, by Theorem~\ref{thm:extension} (1), there exists a fair execution $\gamma^0 \circ \mu$, of 
$\mathcal{A}$, where $\mu$ denotes the extended portion of the execution.

 Clearly, by the N and O properties, 
the actions  $\resp{op_1^r}$ and $\resp{op_2^r}$ must eventually occur in $\gamma^0 \circ \mu$.
 Now,  identify $\eta$ as $\gamma^0 \circ \mu$,  where $\prefix{\eta} \circ \frag{1}{\eta} \circ \frag{2}{\eta}$  is $\gamma^0$,   and $\mu$ is $\suffix{\eta}$, thereby, proving condition $(i)$.

Note the condition $(ii)$ is satisfied by $\eta$ because $\RESP{W}$ appears in $\prefix{\eta}$, therefore, the fair execution $\gamma$ is equivalent to the execution fragment of $\prefix{\eta}$ up to the event $\INV{W}$, and  also, 
$\gamma$ satisfies condition $(ii)$ as stated in Lemma~\ref{lem:exec_gamma}.

Condition $(iii)$ is true because $\frag{1}{\eta}$ begins with action $recv(m_1^r)_{r, s_1}$, which occurs after $\RESP{W}$.
Condition $(iv)$ is satisfied by $\eta$ because $\eta$ is an extension of $\gamma$ and due to  the result of Lemma~\ref{lem:exec_xi}.
\end{proof}



\remove{	
Based on $\alpha$ we will extend prefixes of $\alpha$, by adding a {\sc read} transaction $R =READ$$\{ \readop{o_1},$ $ \readop{o_2} \} $ initiated by $r$, which returns a pair of values $(v_1, v_2)$, where $v_1 \in V_1$ from object $o_1$ and $v_2 \in V_2$ for object $o_2$.  so that,  they are  possible execution fragments of $\mathcal{A}$,  
Below we consider the construction of a  three executions of $\mathcal{A}$, or equivalently of the system $S_2$, based on $\alpha$
}

 
 
  
  \begin{figure}[!ht]
      \centering
         \includegraphics[width=1.05\textwidth]{exec3_a_d.png} \vspace{-2.0em}
         \caption{
\small{Schematic representation of executions $\alpha$, $\beta$, $\gamma$ and $\eta$,
          of ${\mathcal A}$ with transactions $R$ and $W$. The executions evolve from left to right. 
          The vertical marks denote  external events at the reader and the server automata. 
          The marks  above the horizontal line denote  external actions at $s_1^A$, and the marks  below  the  line for external actions at $s_2^A$, and 
            for actions $r^A$ the mark cuts through the line. The dots stand for other  external actions at the individual 
           automata.}} \label{fig:execution1}
 \end{figure}

\begin{figure}[!ht]
      \centering
         \includegraphics[width=1.0\textwidth]{exec3_e_g.png} \vspace{-8.0em}
         \caption{\small{Figure shows, starting with execution $\eta$ of $\mathcal{A}$,  the construction of the progressive sequence of executions 
         $\delta, \delta', \ldots$,  of  $\mathcal{A}$, of the form $\prefix{\cdot } \circ \frag{1}{\cdot}\circ \frag{2}{\cdot} \circ \suffix{\cdot}$, where we finally 
         construct the execution $\phi$ of $\mathcal{A}$ to contradict the S property.}} \label{fig:execution2}
 \end{figure}

\remove{
\sloppy In the following lemma we show that if there is a fair  execution $\delta^{(k+1)}$, of $\mathcal{A}$, of the form
$\finiteprefix{k}{k +1}$ $ \circ \frag{1}{\delta^{(k+1)}} $ $\circ \frag{2}{\delta^{(k+1)}} $ $\circ $ $ \suffix{\delta^{(k+1)}}$
  then we can create another fair execution $\delta^{(k)}$ of $\mathcal{A}$  of the form 
  $\finiteprefix{k-1}{k} $ $\circ$$ \frag{1}{\delta^{(k)}}$$ \circ$ $ \frag{2}{\delta^{(k)}} \circ $ $ \suffix{\delta^{(k)}}$
  where $\prefix{\delta^{(k)}}$ is a \emph{proper} prefix
    of $\prefix{\delta^{(k+1)}}$, i.e.,  length of  $\prefix{\delta^{(k)}}$    
   is shorter than that of $\prefix{\delta^{(k+1)}}$. Note that by our convention on notation 
    $\prefix{\delta^{(k+1)}}$    
   $ \equiv \finiteprefix{k-1}{k }$ and $\prefix{\delta^{(k+1)}}$  $ \equiv \finiteprefix{k}{k +1}  \circ \frag{1}{\delta^{(k+1)}}$.
  
  
\begin{lemma} \label{two:induction}
If  $\delta^{(k+1)}$ is a fair  execution of $\mathcal{A}$, of the form 
$\finiteprefix{k}{k +1} \circ \frag{1}{\delta^{(k+1)}} \circ \frag{2}{\delta^{(k+1)}} \circ \suffix{\delta^{(k+1)}}$, where  $k$ is a positive integer and  the $a_i$'s and $\sigma_i$'s denote states and actions, respectively,    and  transaction $R(\delta^{(k+1)})$ responds with 
$(v_1^1, v_2^1)$ then there exists another fair execution  $\delta^{(k)}$, of $\mathcal{A}$,  of the form 
$\finiteprefix{k-1}{k} \circ \frag{1}{\delta^{(k)}} \circ \frag{2}{\delta^{(k)}} \circ \suffix{\delta^{(k)}}$  such that  $R(\delta^{(k)})$ returns 
$(v_1^1, v_2^1)$. 
\end{lemma}
}


  In the following theorem we prove the impossibility  result for  achieving the SNOW properties  for the two-client system by starting with a fair execution $\eta$ and  creating a sequence of fair executions of 
  $\mathcal{A}$, where each one is of the form $\prefix{\cdot} \circ \frag{1}{\cdot}\circ \frag{2}{\cdot}\circ \suffix{\cdot}$, with progressively shorter $\prefix{\cdot}$ until one of them contradicts the property $S$.

 \begin{theorem}\label{thm:two-snow}
 The SNOW properties cannot be implemented in a system with two clients and two servers, where  the clients do not communicate with other clients.
\end{theorem}

\begin{proof}
\sloppy Consider a fair execution $\delta^{(\ell)}$  of $\mathcal{A}$ as in Lemma~\ref{lem:exec_delta}, and let $\prefix{\delta^{(\ell)}}$  be the execution fragment
$\finiteprefix{\ell-1}{\ell}$, where $\ell$ is some positive integer, and  the $\sigma_i$'s and $a_i$'s denote 
states and actions, respectively. By  Lemma~\ref{lem:exec_delta}, $\RESP{R(\delta^{(\ell)})}$  returns
 $(v_1^1, v_2^1)$ and $\delta^{(\ell)}$ is also of the form    
$\finiteprefix{\ell-1}{\ell} \circ \frag{1}{\delta^{(\ell)}} \circ \frag{2}{\delta^{(\ell)}} \circ \suffix{\delta^{(\ell)}}$.     

Now,  inductively we prove the existence of a  finite sequence of fair executions of $\mathcal{A}$--by proving the existence of one from the previous one--as  $\delta^{(\ell)}, \delta^{(\ell-1)}, \cdots \delta^{(i)}, \delta^{(i-1)},  \cdots \delta^{(f)}$, 
for some positive integer $f$, with the following properties: $(a)$ Each of the execution in 
the sequence can be written in the form  $\finiteprefix{i-1}{i} \circ \frag{1}{\delta^{(i)}} \circ \frag{2}{\delta^{(i)}} \circ \suffix{\delta^{(i)}}$ (or $\prefix{\cdot}\circ \frag{1}{\cdot}\circ \frag{2}{\cdot}\circ\suffix{\cdot}$); $(b)$ for each $i$, $f \leq i  < \ell$ we have  $\prefix{\delta^{(i)}}$  is a prefix of $\prefix{\delta^{(i+1)}}$; and $(c)$ $R(\delta^{(f)})$   returns  $(v_1^0, v_2^0)$ and for any $i$,  $f <  i \leq \ell$  we have   $R(\delta^{(i)})$   returns  $(v_1^1, v_2^1)$.  Note that there is a final execution of the form $\delta^{(f)}$  because of the initial values of $v_1^0$ and $v_2^0$,  and the {\sc write}  $W$. 



\remove{
Note that in  $\delta^{(f)}$,  $R$ returns  $(v_1^1, v_2^1)$,  therefore,   
 the action $send(v_1)_{s_1, r}$ in $\delta^{(f)}$  must have $v_1 =  v_1^1$. Now we can create a new fair execution $\phi$, of $\mathcal{A}$,  where  the adversary  delivers the 
 messages $v_1$ and $v_2$  sent via $send(v_1)_{s_1, r}$ and $send(v_2)_{s_2, r}$, respectively, at $r$ and  $R$ completes before $\INV{W}$ (Figure~\ref{fig:execution2} (g)), which the
  adversary can accomplish by  introducing  $recv(v_1)_{s_1, r}$ and $recv(v_2)_{s_1, r}$ at $r$ and completing $R$. Note that because $v_1 = v_1^1$ and $v_2 = v_2^1$ in the $send(\cdot)$ actions, therefore, by 
 $S$ property of  $\phi$, $R$  must also return  $(v_1^1, v_2^1)$,  which contradicts the  $S$ property of $\mathcal{A}$, and this  completes the proof.
}
 

Clearly, there exists an integer $k$,  $ f \leq  k < \ell$ such that $\frage{R}{\delta^{(k)}}{}$ returns $(v_1^0, v_2^0)$ and $\frage{R}{\delta^{(k+1)}}{}$ returns $(v_1^1, v_2^1)$. Now we start with execution 
$\delta^{(k+1)}$ and construct an execution $\delta^{(k)}$ as described in the rest of the proof. The following argument will show that  $\frage{R}{\delta^{(k)}}{}$ must also return $(v_1^1, v_2^1)$ thereby contradicting the above.

Consider  the fair execution $\delta^{(k+1)}$ of $\mathcal{A}$ which is of the form 
$\finiteprefix{k}{k +1} \circ \frag{1}{\delta^{(k+1)}} \circ \frag{2}{\delta^{(k+1)}} \circ \suffix{\delta^{(k+1)}}$. 
 The action  $a_{k+1}$ can  occur at any of the automata $r^A$, $w^A$, $s_1^A$ or $s_2^A$, therefore, we prove our claim by considering the following four possible cases.
\paragraph{  \underline{\it Case (i) $a_{k+1}$ occurs at $w^A$:}} The execution fragments
 $\frag{1}{\delta^{(k+1)}}$ and $\frag{2}{\delta^{(k+1)}}$ do not contain any input action  at $s_1^A$ and $s_2^A$, respectively,  and also,  $a_{k+1}$ does not occur at $s_1^A$ or $s_2^A$. 

 Hence,
 the adversary can
  delay the occurrence of action  $a_{k+1}$, at  $w^A$, to create the 
   finite execution   
$\finiteprefix{k-1}{k } \circ \frag{1}{\delta^{(k+1)}} \circ \frag{2}{\delta^{(k+1)}}$,  
 of $\mathcal{A}$. Note by Theorem~\ref{thm:extension} (1), there exists a fair execution $\delta^{(k)}$, of $\mathcal{A}$, that 
 is an extension of the above finite execution  where,  by the liveness property of a {\sc read} transaction, $R$ completes in $\delta^{(k)}$.
  Clearly, $\delta^{(k)}$ can be written as  
 $\finiteprefix{k-1}{k } \circ \frag{1}{\delta^{(k)}} \circ \frag{2}{\delta^{(k)}} \circ \suffix{\delta^{(k)}}$, where $ \suffix{\delta^{(k)}}$ is the tail part of the execution resulting from the extension.  At  $s_1^A$,  
  $\frag{1}{\delta^{(k+1)}}$   is indistinguishable  from   
  $\frag{1}{\delta^{(k)}}$   i.e., 
      $\frag{1}{\delta^{(k+1)}} \stackrel{s_1}{\sim} \frag{1}{\delta^{(k)}}$.  \footnote{We drop the superscript $A$, such as $s_1^A$ to $s_1$,  from the symbol above $\sim$ for formatting reasons, when necessary.}
   Therefore, in both of the above fragments, the $send(v_1)_{s_1, r}$ action  has the same object value 
   $v_1$.
  
   But this means $R$ returns $v_1^1$  as the value for $o_1$ and hence,  by the property $S$,  $R(\delta^{(k)})$ must respond with $(v_1^1, v_2^1)$.
   
   \paragraph{  \underline{\it Case (ii) $a_{k+1}$ occurs at $r^A$:}}  Similar to Case $(i)$.
   
   
   \paragraph{  \underline{\it Case (iii) $a_{k+1}$ occurs at $s_1^A$:}}  Observe that the execution fragments  
   $a_{k+1} \sigma_{k+1} \circ \frag{1}{\delta^{(k+1)}}$ and $\frag{2}{\delta^{(k+1)}}$ occur at separate  automata, i.e., at $s_1^A$ and $s_2^A$, respectively. 
    Observe that the  execution fragments  $a_{k+1} \sigma_{k+1} \circ \frag{1}{\delta^{(k+1)}}$ and $\frag{2}{\delta^{(k+1)}}$, of $\mathcal{A}$,  do not contain any  input actions at $s_1^A$ and $s_2^A$, respectively. 
    Therefore, by   Claim~\ref{claim:reorder}, we can create a fair execution  $\epsilon$, of $\mathcal{A}$,  which  can be expressed as 
    $\finiteprefix{k-1}{k }  \circ \frag{2}{\epsilon}\circ a_{k+1}, \sigma_{k+1} \circ \frag{1}{\epsilon} \circ \suffix{\epsilon}$. Clearly,   
     $\frag{1}{\epsilon} \stackrel{s_1}{\sim} \frag{1}{\delta^{(k+1)}}$ and  
     $\frag{2}{\epsilon} \stackrel{s_2}{\sim} \frag{2}{\delta^{(k+1)}}$.  
     %
     %
    
   %


  Now, since action $send(v_1)_{s_1, r}$,  in both $\frag{1}{\epsilon}$ and 
     $\frag{1}{\delta^{(k+1)}}$,  sends the same object value $v_1^1$ to $r$. Therefore, $R$ returns $(v_1^1, v_2^1)$. 
   
   Now let us denote the execution fragment  $\finiteprefix{k-1}{k }  \circ \frag{2}{\epsilon}$ by $\epsilon'$, which  is simply a finite prefix of $\epsilon$.
     Now,  suppose the 
        adversary appends the $recv(m_1^r)_{r, s_1}$ to $\epsilon'$,  i.e., delivers the value request  message from  $r$ to $s_1$,  and  creates a finite execution $\epsilon''$, of $\mathcal{A}$,  as 
        $\finiteprefix{k-1}{k }\circ \frag{2}{\epsilon''}, recv(m_1^r)_{r, s_1}$, and delays any input action at $s_2^A$.    
        Now, by Theorem~\ref{thm:extension} (1), there exists 
        a fair execution $\epsilon'''$ of $\mathcal{A}$, which extends $\epsilon''$. Clearly, 
             $\frag{2}{\epsilon'''} \stackrel{s_2}{\sim} \frag{2}{\epsilon''}$ and hence the $send(v_2 )_{s_2, r}$ actions  in $\epsilon''$ and $\epsilon'''$, send the same value $v_2^1$ for $o_2$. 
             Then by the N property action $send(v_1)_{s_1, r}$ eventually occurs and by O  property $v_1$  is send to $r^A$, therefore,   $R$ completes in $\epsilon'''$, this would imply that 
             $R(\epsilon''')$ must respond with   $(v_1^1, v_2^1)$.
             
             Note that the execution fragment of $\epsilon'''$, between the actions $ recv(m_1^r)_{r, s_1}$ and $send(v_1)_{s_1, r}$, has no input actions of $s_1^A$, which can be identified as $\frag{1}{\epsilon'''}$. Therefore, $\epsilon'''$ can be written as      $\finiteprefix{k-1}{k }  \circ \frag{2}{\epsilon'''} \circ \frag{1}{\epsilon'''} \circ \suffix{\epsilon'''}$.
   
    Next, since $\frag{1}{\epsilon'''}$ and $\frag{2}{\epsilon'''}$ contains actions of  two separate automata, therefore, by  Claim~\ref{claim:reorder},  we can create an execution prefix  $\epsilon^{(iv)}$ as 
    $\finiteprefix{k-1}{k }  \circ \frag{1}{\epsilon^{(iv)}} \circ \frag{2}{\epsilon^{(iv)}}$, 
     where  
     $\frag{1}{\epsilon^{(iv)}}$ appears before $\frag{2}{\epsilon^{(iv)}}$. Next  by using Theorem~\ref{thm:extension} $(1)$ we create fair execution $\delta^{(k)}$ as an extension of 
       $\epsilon^{(iv)}$. Clearly, it can be written   as $\finiteprefix{k-1}{k } \circ \frag{1}{\delta^{(k)}} \circ \frag{2}{\delta^{(k)}}\circ \suffix{\delta^{(k)}}$. 
       Then by O and N  properties  $R$ completes in $\delta^{(k)}$.  
       Since      $\frag{1}{\epsilon^{(iv)}} \stackrel{s_1}{\sim} \frag{1}{\epsilon'''}$ this implies action $send(v_1)_{s_1, r}$ sends $v_1^1$ for object $o_1$ in $\epsilon^{(iv)}$ 
    and    since 
      $\frag{1}{\delta^{(k)}} \stackrel{s_1}{\sim} \frag{1}{\epsilon^{(iv)}}$, this 
      implies action $send(v_1)_{s_1, r}$ sends $v_1^1$  in $\delta^{(k)}$, this would imply that 
     $R(\delta^{(k)})$ returns $(v_1^1, v_2^1)$.
  %
        \paragraph{  \underline{\it Case (iv) $a_{k+1}$ occur at $s_2^A$:}}  Since $a_{k+1}$ occurs at $s_2^A$ and $\frag{1}{\delta^{(k+1)}}$ occurs at $s_1^A$, (i.e.,  separate   automata),  then by applying  Claim~\ref{claim:reorder}  as in the 
        previous cases we can create a new fair execution $\epsilon$ of $\mathcal{A}$  (Figure~\ref{fig:execution2} $(f)$)  as   
             $\finiteprefix{k-1}{k } \circ \frag{1}{\epsilon} \circ a_{k+1}, \sigma_{k+1} \circ 
        \frag{2}{\epsilon}\circ \suffix{\epsilon}$  such that, $\frag{1}{\epsilon} \stackrel{s_1}{\sim}\frag{1}{\delta^{(k+1)}}$ where  
         $a_{k+1}, \sigma_{k+1} $
       occurs after $\frag{1}{\delta^{(k+1)}}$ and 
         $R(\epsilon)$ returns $(v_1^1, v_2^1)$.
        
     Now, consider the finite execution   $\finiteprefix{k-1}{k }\circ \frag{1}{\epsilon}$ for $\mathcal{A}$ and suppose the 
        adversary appends the $recv(m_2^r)_{r, s_2}$ to create a finite execution of $\mathcal{A}$ as 
        $\finiteprefix{k-1}{k }\circ \frag{1}{\epsilon}, recv(m_2^r)_{r, s_2}$. Now, by Theorem~\ref{thm:extension} (1), there exists 
        a fair execution $\epsilon'$ of $\mathcal{A}$, where 
              the adversary delays the input actions at $s_2^A$. By $N$ and $O$ properties $send(v_2)_{s_2, r}$ occurs in $\epsilon'$. Clearly,   since   $\frag{1}{\epsilon'} \stackrel{s_1}{\sim} \frag{1}{\epsilon}$  the $send(v_1)_{s_1, r}$ actions, in $\epsilon$ and $\epsilon'$,  send the same value for $o_1$. Therefore,  $R$ responds with   $(v_1^1, v_2)$, where $v_2 \in V_2$.
              
              Now, in $\epsilon'$, we identify the fragment  which begins with $recv(m_2^r)_{r, s_2}$ and end with the action 
              $send(v_2)_{s_2, r}$  as $\frag{2}{\epsilon'}$ to write $\epsilon'$ as  
              $\finiteprefix{k-1}{k } \circ \frag{1}{\epsilon'}  \circ 
        \frag{2}{\epsilon'}$. Now using Theorem~\ref{thm:extension} (1), we know there exists 
        a fair execution $\delta^{(k)}$ of $\mathcal{A}$, which is an extension of $\epsilon'$. Clearly, $\delta^{(k)}$ can be written as 
     $\finiteprefix{k-1}{k }  \circ \frag{1}{\delta^{(k)}} \circ \frag{2}{\delta^{(k)}} \circ \suffix{\delta^{(k)}}$, where $\suffix{\delta^{(k)}}$ is the tail part of the extended fair execution.  Clearly,  $\frag{1}{\delta^{(k)}} \stackrel{s_1}{\sim} \frag{1}{\epsilon'}$;  therefore,  $R(\delta^{(k)})$ returns $v_1^1$ for object $o_1$,  in $\delta^{(k)}$ and  this  implies $R(\delta^{(k)})$ must return $(v_1^1, v_2^1)$.    
\end{proof}

 
\remove{
\begin{theorem}\label{thm:two-snw}
 The SNOW properties cannot be implemented in a system with two clients and two servers, and  the clients do not communicate with other clients.
\end{theorem}

\begin{proof}
\sloppy Consider a fair execution $\delta^{(\ell)}$  of $\mathcal{A}$ as in Lemma~\ref{lem:exec_delta}, and let $\prefix{\delta^{(\ell)}}$  be the execution fragment
$\finiteprefix{\ell-1}{\ell}$, where $\ell$ is some positive integer, and  the $a_i$'s and $\sigma_i$'s denote states and actions, respectively. By  Lemma~\ref{lem:exec_delta}, $\RESP{R(\delta^{(\ell)})}$  returns $(v_1^1, v_2^1)$ and $\delta^{(\ell)}$ is also of the form    $\finiteprefix{\ell-1}{\ell} \circ \frag{1}{\delta^{(\ell)}} \circ \frag{2}{\delta^{(\ell)}} \circ \suffix{\delta^{(\ell)}}$.      Observe that by applying Lemma~\ref{two:induction} from $\delta$ we can create another execution $\delta^{(\ell-1)}$ of the form $\finiteprefix{\ell-2}{\ell-1} \circ \frag{1}{\delta^{(\ell-1)}} \circ \frag{2}{\delta^{(\ell-1)}} \circ \suffix{\delta^{(\ell-1)}}$ where   $\RESP{R(\delta^{(\ell-1)})}$  returns $(v_1^1, v_2^1)$. Note that $\prefix{\delta^{(\ell-1)}}$ ($\equiv  \finiteprefix{\ell-2}{\ell-1} $) is a prefix of $\prefix{\delta^{(\ell)}}$.
Now, by repeatedly applying Lemma~\ref{two:induction} we create a finite sequence of fair executions of $\mathcal{A}$ as  $\delta^{(\ell)}, \delta^{(\ell-1)}, \cdots \delta^{(i)}, \delta^{(i-1)},  \cdots \delta^{(f)}$, 
for some positive integer $f$, with the following properties: $(a)$ Each of the execution in 
the sequence can be written in the form 
$\prefix{\cdot}\circ \frag{1}{\cdot}\circ \frag{2}{\cdot}\circ\suffix{\cdot}$ ; $(b)$ for each pair consecutive executions $\delta^{(i)}$ and  $\delta^{(i+1)}$,  
$\prefix{\delta^{(i)}}$  is a prefix of $\prefix{\delta^{(i+1)}}$; $(c)$ the  $\RESP{R}$ action in each of these sequences  returns  $(v_1^1, v_2^1)$; and $(d)$  the $\frag{1}{\delta^{(f)}}\circ \frag{2}{\delta^{(f)}}$ 
 occurs before $\INV{W}$ in $\delta^{(f)}$. 
The claims $(a)$, $(b)$ and $(c)$ is due to Lemma~\ref{two:induction}, and $(d)$ follows from the fact that $\prefix{\delta^{(\ell)}}$ is a finite prefix.


Note that in  $\delta^{(f)}$,  $R$ returns  $(v_1^1, v_2^1)$,  therefore,   
 the action $send(v_1)_{s_1, r}$ in $\delta^{(f)}$  must have $v_1 =  v_1^1$. Now we can create a new fair execution $\phi$, of $\mathcal{A}$,  where  the adversary  delivers the 
 messages $v_1$ and $v_2$  sent via $send(v_1)_{s_1, r}$ and $send(v_2)_{s_2, r}$, respectively, at $r$ and  $R$ completes before $\INV{W}$ (Figure~\ref{fig:execution2} (g)), which the
  adversary can accomplish by  introducing  $recv(v_1)_{s_1, r}$ and $recv(v_2)_{s_1, r}$ at $r$ and completing $R$. Note that because $v_1 = v_1^1$ and $v_2 = v_2^1$ in the $send(\cdot)$ actions, therefore, by 
 $S$ property of  $\phi$, $R$  must also return  $(v_1^1, v_2^1)$,  which contradicts the  $S$ property of $\mathcal{A}$, and this  completes the proof.
\end{proof}
 }

 \begin{figure}[!ht]
      \centering
         \includegraphics[width=1.00\textwidth]{architecture3_1.png}  \vspace{-2.5em}
         \caption{
\small{The architecture of a typical web service with clients, servers, and 
        
         the communication channels, between every pair of processes, inside a datacenter is modeled as a collection of I/O automata. Note that, unlike the architecture in Fig.~\ref{fig:architecture2a}, in this setup there are communication channels between every pair of clients.}} 
         \label{fig:architecture2c}
 \end{figure}

\section{Impossibility of SNOW properties with  three clients}\label{three-client}
In this section, we  prove that for a three-client transaction processing system, with at least two objects, it is impossible to design an  algorithm that satisfies  the SNOW properties.
From the proof of the  SNOW Theorem~\cite{SNOW2016}, it is not  clear whether a {\sc write} transaction is ever required to complete in the presence of ongoing  {\sc read} transactions (Fig.~\ref{fig:architecture2c}). Moreover, the authors in ~\cite{SNOW2016} do not state explicitly  whether the result of the  SNOW Theorem holds if clients communicate with each other. In our proof, we state these points explicitly: each {\sc write} must complete even if there are concurrent {\sc read} transactions, and 
 between every pair of processes, there are two  communication channels, one  in each direction (Fig~\ref{fig:architecture2c}). Furthermore, we assume that if a {\sc read} is invoked at a reader, then the reader can proceed to contact the servers without waiting for any incoming messages.

 We prove our result by 
showing a contradiction. We consider a system consisting of two servers,  $s_1$ and $s_2$, and three clients: two 
readers  $r_1$ and $r_2$, which initiate only {\sc read} transactions,  and a writer $w$, which initiates only {\sc write} 
transactions.  Servers $s_1$ and $s_2$ store  values for objects $o_1$ and $o_2$, respectively;  the values  in $o_1$ and 
$o_2$ belong to the domains $V_1$ and $V_2$, respectively;
the  initial values of $o_1$ and $o_2$ are $v_1^0$ and $v_2^0$, respectively. 
We denote the automata for servers $s_1$ and $s_2$ by $s_1^A$ and $s_2^A$, respectively, and the automata for the clients  $r_1$, $r_2$ and $w$ by $r_1^A$, $r_2^A$  and $w^A$, respectively.   
 We assume that between any pair of processes $p_1$ and $p_2$,   such that $p_1 \neq p_2$,   there are channel automata $Channel_{p_1, p_2}$ and $Channel_{p_2, p_1}$.
For the purpose of proving by contradiction, we  also assume that  any fair execution of $\mathcal{B}$  respects  the SNOW properties. 
 Also, we assume that in any execution  of $\mathcal{B}$  we can identify each transaction with a unique identifier.

\sloppy Consider an execution of ${\mathcal B}$ with  three transactions:   a {\sc write} transaction  $W \equiv $ $WRITE($$ (o_1, v_1^1),  (o_2, v_2^1) )$ initiated by  $w$, where $v_1^1 \neq v_1^0$ and $v_2^1 \neq v_2^0$; and  {\sc read} transactions $R_1 \equiv READ$$(o_1, o_2)$  and   $R_2 \equiv READ$$(o_1, o_2)$
 initiated by $r_1$ and $r_2$, respectively.  Let us denote by 
$op_1^r$ and $op_2^r$  the read operations of types $\readop{o_1}$ and  $ \readop{o_2} $, respectively.
As in Section~\ref{two-client},  we assume an omniscient  adversary that can control the  patterns of  sequences of invocations of transactions,  the times of these invocations,  and delays in local computation and message deliveries. 
In the rest of the section,  in order to reduce notational clutter, for any   execution of $\mathcal{B}$, 
$\finiteprefix{k-1}{k}\cdots$, where $\sigma$'s and $a$'s are states and actions,
we use the notation  $\finiteprefixt{k-1}{k}\cdots$ that shows only the actions while leaving out the states.
\paragraph{Notations and Definitions:}
We  introduce  the following notations and definitions in the context of a fair execution $\alpha$, of $\mathcal{B}$, with transactions $R$ and $W$ in it,
 where  $ j \in \{1, 2\}$:
\begin{enumerate}
\item $\send{m_j^{r}}{r, s_j}$: an  output action at $r^A$,  which sends a message $m_j^{r}$ from reader $r$ to server $s_j$, requesting the value for $o_j$;
\item $\recv{m_j^{r}}{r, s_j}$: an input action at $s_j^A$, that receives the message $m_j^{r}$, sent from $r$;
\item $\send{v_j}{ s_j, r}$: an output action at $s_j^A$,  that  sends value $v_j$, for   $o_j$, to $r$.
\item $\recv{v_j}{ s_j, r}$: an input action at $r^A$,  to receive a message $v_j$ from $s_j$ at  $r^A$.
\item  \emph{Non-blocking fragments $\frage{F_j}{\alpha}{v_j}$, $j \in \{1, 2\}$.}
 Suppose there is a fragment of  execution  in $\alpha$  where the first action is   $recv(m_i^r)_{r, s_i}$ and  the last action is 
 $send(v_i)_{s_i, r}$ , both of which  occur  at $s_i^A$. Moreover, suppose there is  
 no other input action at $s_i^A$ in this fragment. Then we call this execution fragment 
   a \emph{non-blocking response fragment} for $op_i^r$ at  $s_i^A$.  We use the notation  $\frage{F_i}{\alpha}{v_j}$ to denote this fragment of   execution of $\alpha$ (Fig.~\ref{fig:exe3_fragments}). In the context of a {\sc read} $R_i$, for $i\in \{1, 2\}$, we use the notation $\frage{F_{i,j}}{\alpha}{v_j}$ to denote $\frage{F_j}{\alpha}{v_j}$.

\remove{
\item $\send{m_j^{r_i}}{r_i, s_j}$: an  output action at $r_i^A$,  which sends a message $m_j^{r_i}$ from reader $r_i$ to server $s_j$, requesting the value for $o_j$;
\item $\recv{m_j^{r_i}}{r_i, s_j}$: an input action at $s_j^A$, that receives the message $m_j^{r_i}$, sent from $r_i$;
\item $\send{v_j}{ s_j, r_i}$: an output action at $s_j^A$,  that  sends value $v_j$, for   $o_j$, to $r_i$.
\item $\recv{v_j}{ s_j, r_i}$: an input action at $r_i^A$,  to receive a message $v_j$ from $s_j$ at  $r_i^A$.
}
\item Suppose {\sc read} $R$ completes in $\alpha$. Consider the execution fragment in $\alpha$  between the event 
$\INV{R}$  and  whichever of the events  $\send{m_2^{r}}{r, s_2}$ and  $\send{m_1^{r}}{r, s_1}$ that occurs later. If all the 
actions in this fragment correspond to  $r^A$, then we denote this fragment as $\frage{I}{\alpha}{}$ (Fig.~\ref{fig:exe3_fragments}).  In case of a {\sc read} $R_i$, for $i\in \{1, 2\}$, we use the notation $\frage{I_i}{\alpha}{}$ for 
$\frage{I}{\alpha}{}$.

\remove{
\item  \emph{Non-blocking fragments $\frage{F_{i,j}}{\epsilon}{v_i}$ for  $i,j \in \{1, 2\}$.}
 Suppose in $\epsilon$, there is a fragment of  execution such that all of its actions occur at $s_j^A$ and  that begins with  action  $recv(m_j^{r_i})_{r, s_j}$ and  ends with action  
 $send(v_j)_{s_j, r}$. Moreover, suppose there is  
 no other input action at $s_j^A$ in this fragment then we call this execution fragment 
  as a \emph{non-blocking response fragment} for $op_i^r$ at  $s_j^A$.  We use the notation  $\frage{F_{i,j}}{\epsilon}{v_j}$   for $i, j   \in \{1, 2\}$,  
 to denote these fragments of   execution corresponding to a  {\sc read} $R_i$  (Fig.~\ref{fig:exe3_fragments}).  
  }
  

\item Suppose {\sc read}s $R$  completes in $\alpha$. Consider the execution fragments in $\alpha$ that
occurs between the later of the events   $\recv{v_1}{ s_1, r}$ or  $\recv{v_2}{s_2, r}$, i.e., at the point in $\alpha$ when $r$ receives responses from both the servers,  and the event $\RESP{R}$. If all the 
actions in this fragment occur at $r^A$, then we denote this fragment by $\frage{E}{\alpha}{v_1, v_2}$, where $R$ returns the values $(v_1, v_2)$  (Fig.~\ref{fig:exe3_fragments}).     In case of a {\sc read} $R_i$, for $i\in \{1, 2\}$, we use the notation $\frage{E_i}{\alpha}{v_1, v_2}$ for $\frage{E}{\alpha}{v_1, v_2}$.

 \item  We use the notations $R(\alpha)$ and $W(\alpha)$ to denote the transactions $R$ and $W$, in the context of $\alpha$. When the underlying execution is clear from the context we simply use $R$ and $W$.
\item For any $v^i_j\in V_j$,  the superscript $i$ corresponds to the version identifier, which uniquely identifies a version from a totally ordered  set.


 
 \remove{
\item \sloppy If $\epsilon$ is of the form  
 $\finiteprefix{\ell-1}{\ell}  \circ \frag{1}{\epsilon} \circ \kappa \circ \frag{2}{\epsilon} , a_p, \sigma_p, \ldots$  or 
 $\finiteprefix{\ell-1}{\ell}  \circ \frag{2}{\epsilon} \circ \kappa \circ \frag{1}{\epsilon} , a_p, \sigma_p, \ldots$, where 
 $\kappa$ is a segment of $\epsilon$,  possibly even of length zero, 
 then we denote $\finiteprefix{\ell-1}{\ell} $ by $\prefix{\epsilon}$ and $a_p, \sigma_p, \ldots$ by $\suffix{\epsilon}$, where $\ell$ and $m$ are positive integers. Clearly,  we can write $\epsilon$ as $\prefix{\epsilon} \circ \frag{1}{\epsilon}\circ \kappa \circ \frag{2}{\epsilon} \circ \suffix{\epsilon}$.}
\end{enumerate}


 \begin{figure}[!ht]
      \centering
         \includegraphics[width=1.00\textwidth,  height=12cm]{executions_3_2.png}  \vspace{-10.5em}
         \caption{
\small{The figure depicts for a fair execution $\alpha$ of $\mathcal{B}$ the relevant actions in the execution fragments of   $I_i(\alpha)$, $F_{i,1}(\alpha)^{(v_1)}$,    $F_{i,2}(\alpha)^{(v_2)}$ and   $E_{i}(\alpha)^{(v_1,v_2)}$ for any {\sc read} $R_i$, $i \in \{1, 2\}$.}}
         \label{fig:exe3_fragments}
 \end{figure}
  
Any  {\sc read} $R$ initiated at a reader $r$, via the  
invocation action  $\INV{R}$ at $r$, after which the  actions $send(m_1^{r})_{r, s_1}$ and $send(m_2^{r})_{r, s_2}$, at $r$, send message $m_1^r$  to $s_1$ and $m_2^r$ to $s_2$, respectively. Once
$s_1$   receives $recv(m_1^{r})_{r, s_1}$  then  $s_1$ responds to $r$,  in a 
non-blocking manner,  with value $v_1$ via  action $send(v_1)_{s_1, r}$. Similarly,  after $s_2$  receives $m_2^{r}$ it  responds with $v_2$ to 
$r$ in a non-blocking manner via the action $send(v_2)_{s_2, r}$. After  $r$ receives $v_1$ and $v_2$ via actions $recv(v_1)_{s_1, r}$ and $recv(v_2)_{s_2, r}$, respectively,  $R$  completes
 with the response action $\RESP{R}$ and  returns $(v_1, v_2)$. 
 

  
    
From the above discussion we can state the following useful lemma, which states that in any  execution of $\mathcal{B}$,  if 
a server $s_i$  responds with a value $v_i$ during a   
{\sc read}  then the {\sc read} returns  
$v_i$ for  object $o_i$ and also, the pair of values $(v_1^t, v_2^t)$ are from some version $t$.
The result follows from the reliable channel model, where messages  reach at their destinations unaltered;  and by the S property  the object values, for objects $o_1$ and $o_2$,  returned by $R$  are of the same version.

\begin{lemma}\label{lem:exec3_consistent} 
Suppose $\alpha$ is any execution of $\mathcal{B}$ such that a {\sc read} $R$ is in $\alpha$. Suppose the  execution fragment $\frage{I}{\alpha}{} \circ \frage{F_{1}}{\alpha}{v_1^{t}} \circ \frage{F_{2}}{\alpha}{v_2^{s}} \circ \frage{E}{\alpha}{v_1^{t'}, v_2^{s'}}$ in $\alpha$,  corresponds to $R$,  where   $v_1^t, v_1^{t'} \in V_1$ and  $v_2^s, v_2^{s'} \in V_2$, and $s, s', t, t' $ are version identifiers  then $(i)$ $s = s'$  and $ t=t'$ and $(ii)$ $s'=t'$.  
\end{lemma}

\begin{proof}
Suppose $R$ is invoked at reader $r$.  Then, via the action $send(v_1^t)_{s_1, r}$, in 
execution fragment  $\frage{F_{1}}{\alpha}{v_1^{t}}$, server $s_1$ sends the value $v_1^t$ to $r$,   which is received at $r$ through the action 
$recv(v_1^{t'})_{s_1, r}$ in $\frage{E}{\alpha}{v_1^{t'}, v_2^{s'}}$.
 By the assumptions of the reliable channel automata in our model,  we have $v_1^{t}=v_1^{t'}$, i.e., $t=t'$. Similar argument for 
$\frage{F_{2}}{\alpha}{v_2^{s}}$  and $\frage{E}{\alpha}{v_1^{t'}, v_2^{s'}}$ leads us to conclude $s=s'$. Next, $R$ responds with $(v_1^{t'}, v_2^{s'})$, which implies  by the S property for executions of
 $\mathcal{B}$ that  $v_1^{t'}$ and $v_2^{s'}$ must correspond to the same version, i.e., $s'=t'$.
\end{proof}

Note that the above results hold even if there are any other  execution fragments, that do not contain any actions at $r$, $s_1$ or $s_2$,   in-between the $I$, $F_i$ and $E$ execution  fragments. 
\begin{corollary}\label{lem:exec3_consistent_corollary} 
Suppose $\alpha$ is any execution of $\mathcal{B}$ such that a {\sc read} $R$ is in $\alpha$. Suppose the  execution fragment $\frage{I}{\alpha}{} \circ  X_1 \circ \frage{F_{1}}{\alpha}{v_1^{t}} \circ X_2 \circ  \frage{F_{2}}{\alpha}{v_2^{s}} \circ X_3 \circ \frage{E}{\alpha}{v_1^{t'}, v_2^{s'}}$ in $\alpha$,  corresponds to $R$,  where   $v_1^t, v_1^{t'} \in V_1$ and  $v_2^s, v_2^{s'} \in V_2$, $X_1, X_2, X_3$ are some execution fragments that do not contain any action at $r$, $s_1$ or $s_2$, and $s, s', t, t' $ are version identifiers  then $(i)$ $s = s'$  and $ t=t'$ and $(ii)$ $s'=t'$.  
\end{corollary}

The following lemma states that new fair executions of $\mathcal{B}$ can be created by swapping execution fragments that have no input actions, and in which   each fragment contains 
actions that occur  only at one automaton and the automata for the two fragments are different.   
  \begin{lemma}[Commuting fragments] \label{lem:exec3_commute} 
  Let $\alpha$ be a fair execution of $\mathcal{B}$. Suppose $\frage{G_1}{\alpha}{}$ and $\frage{G_2}{\alpha}{}$ are any  execution fragments in $\alpha$ such that
  all actions in each fragment occur only at one automaton and also, none of them are input actions. Suppose $\frage{G_1}{\alpha}{}$ 
  and $\frage{G_2}{\alpha}{}$  occur at two distinct automata and the execution
  fragment $\frage{G_1}{\alpha}{}\circ \frage{G_2}{\alpha}{}$ occurs in $\alpha$.
  Then there exists a fair execution $\alpha'$ of $\mathcal{B}$, where  the execution fragment  $\frage{G_2}{\alpha}{}\circ \frage{G_1}{\alpha}{}$ appears in $\alpha'$, such that $(i)$ 
the prefix  in $\alpha$  before  $\frage{G_1}{\alpha}{} \circ \frage{G_2}{\alpha}{}$
 is identical to the prefix  in $\alpha'$ before  $\frage{G_1}{\alpha'}{} \circ \frage{G_2}{\alpha'}{}$; and $(ii)$ 
the suffix in $\alpha$  after   
 $\frage{G_1}{\alpha}{} \circ \frage{G_2}{\alpha}{}$
is identical to the suffix in $\alpha'$ after the execution fragment 
 $\frage{G_2}{\alpha'}{} \circ \frage{G_1}{\alpha'}{}$. 


  \end{lemma}
 
  \begin{proof}
  This is clear because the adversary can move the actions in $G_2$ to occur before $G_1$ at their respective automata, and these fragments  do not contain any input actions, and hence 
  the actions in one of these fragments cannot affect the actions in the other fragment.
  \end{proof}

The following lemma states that if there are two fair executions of $\mathcal{B}$ with a {\sc read}  $R$ in each of them, and suppose at any server the non-blocking execution fragments  of $R$  are identical (in terms of the sequence of states and actions)  then in both executions, $R$   returns the same object value.

\begin{lemma}[Indistinguishability]  \label{lem:exec3_equiv}
Let $\alpha$ and $\beta$ be executions of $\mathcal{B}$ and let $R$ be any {\sc read}. Then 
$(i)$  if $\frage{F_{1}}{\alpha}{} \stackrel{s_1}{\sim}\frage{F_{1}}{\beta}{}$ then both 
$R(\alpha)$ and $R(\beta)$ respond with the same value  $v_1$ for $o_1$; and 
$(ii)$ if  $\frage{F_{2}}{\alpha}{} \stackrel{s_2}{\sim}\frage{F_{2}}{\beta}{}$ then both 
$R(\alpha)$ and $R(\beta)$ respond with the same value  $v_2$ for $o_2$;
\end{lemma}

\begin{proof}
Suppose $R$ is invoked at some reader $r$. Let $j \in \{1, 2\}$ and  suppose the fragments  $\frage{F_{j}}{\alpha}{}$ and  $\frage{F_{j}}{\beta}{}$ 
appears in $\alpha$ and $\beta$ respectively, where in $\frage{F_{j}}{\alpha}{}$ server $s_j$
sends  $v_j \in V_j$ to $r$. Then $R(\alpha)$ must return $v_j$ for object $o_j$ by the O property  of $\mathcal{B}$. Then since $\frage{F_{j}}{\alpha}{} \stackrel{s_j}{\sim} \frage{F_{j}}{\beta}{}$ then
in  $\frage{F_{j}}{\beta}{}$  the server $s_j$ 
must also  send $v_j$ to $r$,  therefore,  both $R(\alpha)$ and $R(\beta)$ must return value $v_j$ for $o_j$.
\end{proof}

 \begin{figure}[!ht]
      \centering
         \includegraphics[width=1.00\textwidth]{executions_3_1.jpg}  \vspace{-2.5em}
         \caption{
        \small{The sequence of fair executions of $\mathcal{B}$ with three clients with the operation  $W$, $R_1$ and $R_2$ eventually leading to the execution $\alpha_10$ that contradicts the S property. The directed arcs depicts the transposition of execution fragments from the previous execution in the sequence.
        
         }} 
         \label{fig:executions3}
 \end{figure}

\remove{
In the remainder of the section, for the traces of  $\frage{I_i}{\alpha}{}$, $\frage{F_{i,1}}{\alpha}{v_1}$, 
$\frage{F_{i,2}}{\alpha}{v_2}$, $\frage{E_i}{\alpha}{v_1, v_2} $ and $ \frage{S}{\alpha}{}$, for $i \in \{1, 2\}$,  we  
denote them simply as   $\fragt{I_i}{\alpha}{}$, $\fragt{F_{i,1}}{\alpha}{v_1}$, 
$\fragt{F_{i,2}}{\alpha}{v_2}$, $\fragt{E_i}{\alpha}{v_1, v_2} $ and $ \fragt{S}{\alpha}{}$, respectively, suppressing the explicit execution arguments. Moreover, for any execution $\alpha_i$ of 
$\mathcal{B}$ we denote the trace $trace(\alpha_i)$ as $\beta_i$, and  for executions $\alpha$, $\alpha'$ and $\alpha''$ their corresponding traces  as $\beta$, $\beta'$ and $\beta''$, respectively. With regard to any 
{\sc read} $R_i$ we denote the execution fragment 
$\frage{I_i}{\alpha}{} \circ \frage{F_{i,1}}{\alpha}{v_1} \circ 
\frage{F_{i,2}}{\alpha}{v_2} \circ \frage{E_i}{\alpha}{v_1, v_2} $
as  $\frage{R_i}{}{v_1, v_2}$, and the trace fragment $\fragt{I_i}{\alpha}{} \circ \fragt{F_{i,1}}{\alpha}{v_1} \circ 
\fragt{F_{i,2}}{\alpha}{v_2} \circ \fragt{E_i}{\alpha}{v_1, v_2} $
as  $\fragt{R_i}{}{v_1, v_2}$.
}

Below we show that in any finite execution of $\mathcal{B}$ where the final action is an invocation of  {\sc read} $R$ at a reader $r$, the adversary can always induce a fair execution of $\mathcal{B}$ where the fragments $I$, $\frage{F_{1}}{}{}$, $\frage{F_{2}}{}{}$ and $E$ appear consecutively in that order.

\begin{lemma}\label{lem:read_format}

If any finite execution of  $\mathcal{B}$ ends with $\INV{R}$, for a {\sc read} $R$ then there exists an extension $\alpha$ which is a fair execution of $\mathcal{B}$ and  is  of the form  
   $\frage{P}{\alpha}{} \circ\frage{I}{\alpha}{} \circ \frage{F_{1}}{\alpha}{v_1} \circ \frage{F_{2}}{\alpha}{v_2} \circ \frage{E}{\alpha}{v_1, v_2} \circ \frage{S}{\alpha}{}$, where $\frage{P}{\alpha}{}$ is the prefix and $\frage{S}{\alpha}{}$ denotes the rest of the execution. 
 \end{lemma}
 
 \begin{proof}
 Consider a finite execution of $\mathcal{B}$  that end with  $INV(R)$, which  occurs at some reader  $r$, 
then the  adversary  induces the execution fragment $\frage{I}{\alpha}{}$  by delaying all actions, except the internal and output actions at $r^A$, between 
the actions $\INV{R}$ and the later of the actions $send(m_1^{r})_{r, s_1}$ and $send(m_2^{r})_{r, s_2}$. Next, the adversary  
delivers $m_1^{r}$ at $s_1$ (via the action $recv(m_1^{r})_{r, s_1}$) and delays all actions, other than internal and output actions at $s_1^A$, until $s_1$ responds with $v_1$, via  $send(v_1)_{s_1, r}$; 
we identify this  execution fragment
 as $\frage{F_{1}}{\alpha}{v_1}$. Subsequently, in a similar manner, 
the  adversary  delivers the message  $m_2^{r}$ and delays appropriate actions to induce the execution fragment 
$\frage{F_{2}}{\alpha}{v_2}$. Finally, the adversary  delivers the values $v_1$ and $v_2$ to $r$ (via the events $recv(v_1)_{s_1, r}$ and $recv(v_2)_{s_2, r}$), 
and delays all actions at other automata until $R$ completes  with action $\RESP{R}$ by returning $(v_1, v_2)$.  As a result, we  arrive at a fair execution of $\mathcal{B}$ of the form
 $\frage{I}{\alpha}{} \circ \frage{F_{1}}{\alpha}{v_1} \circ \frage{F_{2}}{\alpha}{v_2} \circ \frage{E}{\alpha}{v_1, v_2} \circ \frage{S}{\alpha}{}$.
\end{proof}

\sloppy The high-level view of our proof strategy is to create a fair execution $\alpha$ of $\mathcal{B}$ that contradicts the S property. 
We begin with a fair execution of $\mathcal{B}$ that contains {\sc read}s $R_1$ and $R_2$, and {\sc write} $W$,  where  $R_1$ begins after $W$ completes, and $R_2$ begins after $R_1$ completes. Clearly, by the S property both  $R_1$   and $R_2$ return $(v_1^1, v_2^1)$.
Then we successively create a sequence of fair 
executions of $\mathcal{B}$  (Fig.~\ref{fig:executions3}), where we interchange the fragments until we  finally reach
 an execution of  where $R_2$ completes before $R_1$ begins, but $R_2$ returns 
$(v_1^1, v_2^1)$ and $R_1$ returns $(v_1^0, v_2^0)$ which contradicts the  S property.

The following lemma show that in an execution of $\mathcal{B}$ with a {\sc write} $W$ and a {\sc read} $R_1$, there exists a point  in the execution
such that if $R_1$ is invoked before that point then $R_1$ returns $(v_1^0, v_2^0)$ and if  invoked after 
that point   then $R_1$ returns $(v_1^1, v_2^1$).

\begin{lemma}[Existence of $\alpha_0$ and $\alpha_1$] \label{lem:exec3_alpha1} 
There exist  fair executions $\alpha_0$ and $\alpha_1$ of $\mathcal{B}$ that contain transactions $W$ and  $R_1$ 
   with  the following properties:
\begin{enumerate}
\item[$(i)$] $\alpha_0$ can be written as 
$\finiteprefixt{k-1}{k} \circ 
\frage{R_1}{\alpha_0}{v_1^0, v_2^0}
 \circ \frage{S}{\alpha_0}{}$ ;

\item[$(ii)$]   $\alpha_1$ can be written as 
$\finiteprefixt{k}{k+1} \circ 
\frage{R_1}{\alpha_1}{v_1^1, v_2^1}  \circ \frage{S}{\alpha_1}{}$; and  
\item[$(iii)$] $a_{k+1}$ in $\alpha_1$  occurs at  $r_1^A$, 
\end{enumerate} 
where $k$ is some positive integer and $\finiteprefixt{k-1}{k}$ is a prefix of $\finiteprefixt{k}{k+1}$.
\end{lemma}

\begin{proof}
Now we describe the construction of a sequence  $\{\gamma_k\}_{k=0}^{\infty}$ of finite executions of $\mathcal{B}$ such that each $\gamma_k$ contains $W$ and $R_1$.
Let us consider a fair execution $\alpha$ of $\mathcal{B}$ that contains $W$. 
Suppose $k$ is
any positive integer and suppose $R_1$ is invoked at $r_1^A$ after the execution fragment 
$\finiteprefixt{k}{k+1}$,  a
prefix of $\alpha$. After the action $\INV{R}$, the adversary schedules only internal and external actions at $r_1^A$ until both the  events
 $\send{m_1^{r_1}}{ r_1, s_1}$ and $\send{m_2^{r_1}}{ r_1, s_2}$ occur, thereby creating an execution fragment of the form
$\finiteprefixt{k}{k+1}\circ I_1(\alpha)$. Let us  denote $\finiteprefixt{k}{k+1}$ by $\finiteprefixA{k}{k+1}$.

 Following this,  the adversary delivers the messages $m_1^{r_1}$ at $s_1$, and delays 
all actions at other automata and also any  input action at $s_1$, until $s_1$ sends $v_1$ to $r_1$, therefore,  inducing the execution fragment   
$\finiteprefixA{k}{k+1}\circ \frage{ I_{1,1}}{\alpha}{} \circ \frage{F_{1,1}}{\alpha}{}$  of  ${\mathcal B}$. 
Next, the adversary delivers $m_2^{r_1}$ at $s_2$ and delays all actions at other automata and input actions at $s_2$, until $s_2$ sends $v_2$ to $r_1$. 
Then the adversary delivers $v_1$ and $v_2$ at $r_1$ but it delays  actions at other automata and any other input action at $r_1$, until $\RESP{R_1}$ occurs.  Up to this point this is an  execution fragment of $\mathcal{B}$, which can be written as 
 $\finiteprefixA{k}{k+1}\circ \frage{I_1}{\alpha}{} \circ \frage{F_{1,1}}{\alpha}{v_1} \circ \frage{F_{1,2}}{\alpha}{v_2} \circ \frage{E_1}{\alpha}{v_1,v_2}$, where $R_1$ responds with $(v_1, v_2)$ such that $(v_1, v_2) \in \{ (v_1^0, v_2^0), (v_1^1, v_2^1) \}$.  We denote this finite execution prefix as $\gamma_k$. Therefore, there exists the sequence of such finite executions  
 $\{\gamma_k\}_{k=0}^{\infty}$.

In  $\gamma_0$,  $R_1$ precedes  $W$  and therefore, by the S property, in $\gamma_0$,   $R_1$ must respond with $(v_1^0, v_2^0)$.   On the other hand, if $k$ is large enough such that $a_{k}$ occurs in $\alpha$ after the completion of $W$ then by  the $S$ property, in 
$\gamma_{k+1}$,  $R_1$ must return  $(v_1^1, v_2^1)$.  Therefore, there exists a minimum $k$  where in $\gamma_k$
{\sc read} $R_1$ returns  $(v_1^0, v_2^0)$ and 
 in $\gamma_{k+1}$,
$R_1$ returns  $(v_1^1, v_2^1)$. We identify $\gamma_{k}$ as  $\alpha_0$ and $\gamma_{k+1}$ as $\alpha_1$ as in claims $(i)$ and $(ii)$, respectively. 
\remove{
$\finiteprefixA{k}{k+1} \circ 
\frage{R_1}{\alpha_1}{v_1^1, v_2^1}
\circ \frage{S}{\alpha_1}{}$
where $\alpha_1$ is the resulting fair execution of $\mathcal{B}$.  Clearly, by definition of $k$ we have 
$\finiteprefixA{k-1}{k} \circ \frage{I_1}{\alpha_0}{} \circ \frage{F_{1,1}}{\alpha_0}{v_1^0} \circ \frage{F_{1,2}}{\alpha_0}{v_2^0} 
\circ \frage{E_1}{\alpha_0}{v_1^0, v_2^0} \circ \frage{S}{\alpha_0}{}$, which we denote by $\alpha_0$.
}

Now, we show $(iii)$ by eliminating the possibility of  $a_{k+1}$ occurring at $s_1^A$, $s_2^A$, $w^A$ or $r_2^A$ by showing 
contradictions.
Our proof is based on the following argument. 
The S property implies that  $R_1$ must respond with values for  $o_1$ and $o_2$ corresponding to  the same version, which implies that  $s_1$ and  $s_2$ must send values of the same version.
Observe that $R_1$, in $\alpha_0$ and $\alpha_1$, returns values for versions
 $0$ (i.e., $(v_1^0, v_2^0)$)  and $1$ (i.e., $(v_1^1, v_2^1)$), respectively, but the prefixes $\fragt{P_k}{\alpha_0}{}$ and 
 $\fragt{P_{k+1}}{\alpha_1}{}$ differ from one another only by action $a_{k+1}$. But just one action at any of  $s_1$, $s_2$, $r_2$
or $w$ is not enough for $s_1$ and $s_2$ to coordinate to return values of the same version. Therefore, $a_{k+1}$ must occur in $r_1$, which can 
possibly synchronize by sending some information in $m_1$ and $m_2$ to $s_1$ and $s_2$, respectively.

\emph{ \underline{Case $a_{k+1}$ occurs at $s_1^A$}:} Consider the  prefix of execution $\alpha_0$ up to the action $a_k$.  Suppose the adversary invokes 
$R_1$ immediately after action $a_{k}$, i.e.,  via $\INV{R_1}$. By Lemma~\ref{lem:read_format} there exists  
fair execution $\alpha'$ of $\mathcal{B}$  that contains an  execution fragment of the form
$\fragt{P_k}{\alpha'}{}
  \circ\frage{I_1}{\alpha'}{} \circ  \frage{F_{1,1}}{\alpha'}{v_1} 
  \circ\frage{F_{1,2}}{\alpha'}{v_2}
  \circ \frage{E}{\alpha'}{v_1, v_2}$. Note that in  both $\alpha'$ and $\alpha_1$
 we can have 
$\frage{I_1}{\alpha_1}{} \stackrel{r_1}{\sim} \frage{I_1}{\alpha'}{}$ and 
$\frage{F_{1,2}}{\alpha_1}{} \stackrel{s_2}{\sim} \frage{F_{1,2}}{\alpha'}{}$, this is because in both  executions 
the actions of $\frage{I_1}{}{}$ occur entirely at $r_1$ and those of $\frage{F_{1,2}}{}{}$ entirely at $s_2$.
As a result,  $\frage{F_{1, 2}}{\alpha'}{}$ must send the same value $v_2^1$  for $o_2$ to $r_1$ as 
 in  $\frage{F_{1,2}}{\alpha_1}{}$.
Then in $\alpha'$, by Lemma~\ref{lem:exec3_equiv}, $R_1(\alpha')$ returns $v_2^1$ for object $o_2$, and by the 
$S$ property, $R_1(\alpha')$ returns  $(v_1^1, v_2^1)$. But this contradicts the 
definition of $k$,  as the minimum value of $k$ such that $R_1$ responds with $(v_1^0, v_2^0)$.

\emph{ \underline{Case $a_{k+1}$ occurs at $s_2^A$}:} A  contradiction can be shown by following a line of reasoning similar to the  preceding case.

\emph{\underline{Case $a_{k+1}$ occurs at $w^A$}:}
This can be argued in a similar manner as the previous case and a bit  easier because we have  $\frage{F_{1,1}}{\alpha_1}{} \stackrel{s_1}{\sim} \frage{F_{1,1}}{\alpha'}{}$, and also, 
$\frage{F_{1,2}}{\alpha_1}{} \stackrel{s_2}{\sim} \frage{F_{1,2}}{\alpha'}{}$.
\remove{
 Suppose the adversary invokes 
$R_1$ immediately after action $a_{k}$ in the prefix of $\alpha_0$ ending with $a_k$, and creates and 
execution fragment $\alpha''$  such that it contains the execution fragment 
$ \fragt{P_k}{\alpha''}{} \circ\frage{I_1}{\alpha''}{} \circ  \frage{F_{1,1}}{\alpha''}{} \circ\frage{F_{1,2}}{\alpha''}{}$, where 
$\frage{I_1}{\alpha_1}{} \stackrel{r_1}{\sim} \frage{I_1}{\alpha''}{}$, 
$\frage{F_{1,1}}{\alpha_1}{} \stackrel{s_1}{\sim} \frage{F_{1,1}}{\alpha''}{}$, and 
$\frage{F_{1,2}}{\alpha_1}{} \stackrel{s_2}{\sim} \frage{F_{1,2}}{\alpha''}{}$.
This is because  $\fragt{I_1}{\alpha''}{} \circ  \fragt{F_{1,1}}{\alpha''}{} \circ  \fragt{F_{1,2}}{\alpha''}{}$ does not contain any input action at $w^A$. Now,  by Lemma~\ref{lem:exec3_equiv}, we infer that $R_1(\alpha'')$ returns $(v_1^1, v_2^1)$ in $\alpha''$. This  contradicts the definition of $k$, as the smallest index,  such that $\frage{R_1}{\alpha_1}{}$ responds with $(v_1^0, v_2^0)$.
}

\emph{\underline{Case $a_{k+1}$ occurs at $r_2^A$}:} 
A contradiction can be derived using a line of  reasoning as in the previous case.

From the above, we conclude that  in $\alpha_1$, action $a_{k+1}$ must occur at $r_1^A$.
\end{proof}

\paragraph{Additional notation:} In the remainder of the section, for the execution fragments  $\frage{I_i}{\alpha}{}$, $\frage{F_{i,1}}{\alpha}{v_1}$, 
$\frage{F_{i,2}}{\alpha}{v_2}$, $\frage{E_i}{\alpha}{v_1, v_2} $ and $ \frage{S}{\alpha}{}$, for $i \in \{1, 2\}$ we  use the notations   $\fragt{I_i}{\alpha}{}$, $\fragt{F_{i,1}}{\alpha}{v_1}$, 
$\fragt{F_{i,2}}{\alpha}{v_2}$, $\fragt{E_i}{\alpha}{v_1, v_2} $ and $ \fragt{S}{\alpha}{}$, respectively, suppressing the explicit reference to the execution. 
With regard to any 
{\sc read} $R_i$ if it has an  execution fragment of the form 
$\frage{I_i}{\alpha}{} \circ \frage{F_{i,1}}{\alpha}{v_1} \circ 
\frage{F_{i,2}}{\alpha}{v_2} \circ \frage{E_i}{\alpha}{v_1, v_2} $
we denote it  as  $\frage{R_i}{}{v_1, v_2}$. Also, wherever the returned values in the fragments are not known, clear from the context or irrelevant we omit them.
In the rest of the section, we fix  $\alpha_0$ and $\alpha_1$, and the value of $k$;  we denote  the execution fragments  $\finiteprefixt{k}{k}$ and $\finiteprefixt{k}{k+1}$ as 
$\finiteprefixA{k}{k}$ and $\finiteprefixA{k}{k+1}$, respectively, which are the same irrespective of the execution they appear in.



The following lemma states the existence of an execution of $\mathcal{B}$ where, following a {\sc write},  there are two consecutive  {\sc read}s  and both 
return the object values updated by the {\sc write}.
\begin{lemma}[Existence of $\alpha_2$] \label{lem:exec3_alpha2} 
\sloppy There exists  fair execution $\alpha_2$  of $\mathcal{B}$ that contains transactions 
$W$, $R_1$ and $R_2$ and can be written in the form 
$\finiteprefixA{k}{k+1} \circ 
\frage{R_1}{}{v_1^1, v_2^1}
 \circ
 \frage{R_2}{}{v_1^1, v_2^1}

\circ \fragt{S}{\alpha_2}{}$, where both $R_1$ and $R_2$ return $(v_1^1, v_2^1)$.
\end{lemma}

\begin{proof}

We can construct a fair execution  $\alpha_2$ of $\mathcal{B}$ as follows. Consider the prefix 
$\finiteprefixt{k}{k+1} \circ 
\frage{R_1}{\alpha_1}{v_1^1, v_2^1}$
of the execution $\alpha_1$, from Lemma~\ref{lem:exec3_alpha1}. At the end of this prefix, the adversary invokes $R_2$. Now, by 
Lemma~\ref{lem:read_format}, due to $\INV{R_2}$
there is an extension of the prefix of the form 
$\finiteprefixt{k}{k+1} \circ  \frage{R_1}{\alpha_1}{v_1^1, v_2^1} \circ 
\frage{I}{\alpha}{} \circ \frage{F_{1}}{\alpha}{v_1} \circ \frage{F_{2}}{\alpha}{v_2} \circ \frage{E}{\alpha}{v_1, v_2}$. 
By the S property, we have $v_1 = v_1^1$ and $v_2= v_2^1$. Therefore, $\alpha_2$ (Fig.~\ref{fig:executions3}) can be written in the form
$\finiteprefixA{k}{k+1} \circ 
\frage{R_1}{}{v_1^1, v_2^1}
 \circ
 \frage{R_2}{}{v_1^1, v_2^1}

\circ \fragt{S}{\alpha_2}{}$, where $\fragt{S}{\alpha_2}{}$ is the rest of the execution.
\remove{
At a high-level, such a fair execution of $\mathcal{B}$ can created if the adversary invokes $R_2$ in $\alpha_1$ after 
$\RESP{R_1}$, and the returned values are a consequence of the S property. Note that the forms 
$\frage{R_1}{}{v_1^1, v_2^1}$ and $\frage{R_2}{}{v_1^1, v_2^1}$ is due to an application of Lemma~\ref{lem:read_format}.

In a finite  execution, in $\alpha'$ as in  Lemma~\ref{lem:exec3_alpha1} 
we invoke the {\sc read} $R_2$ after the execution fragment $E_1$
to create the 
execution $\alpha_2$ in the current lemma.  Since $R_2$ occurs after $R_1$ completes, by the $S$ property, $R_2$ must respond with 
$(v_1^1, v_2^1)$.}
\end{proof}


Based on the previous execution, the following lemma states that there is a fair execution of 
$\mathcal{B}$ where the $I_2$ occurs earlier than the action $a_{k+1}$ and  invocation of  $R_1$.
\begin{lemma}[Existence of $\alpha_3$] \label{lem:exec3_alpha3} 
\sloppy There exists  fair execution $\alpha_3$  of $\mathcal{B}$ that contains transactions $W$, $R_1$ and $R_2$, and can be written in the form  
$\finiteprefixA{k-1}{k} \circ  \fragt{I_2}{\alpha_3}{} \circ  a_{k+1} \circ 
\frage{R_1}{}{v_1^1, v_2^1}
\circ \fragn{F_{2,1}}{\alpha_3}{v_1^1} \circ \fragn{F_{2,2}}{\alpha_3}{v_2^1} \circ \fragn{E_2}{\alpha_3}{v_1^1, v_2^1}
\circ \fragt{S}{\alpha_3}{}$,  where both $R_1$ and $R_2$ return $(v_1^1, v_2^1)$.
\end{lemma}

\begin{proof}
Consider the execution $\alpha_2$ as in  Lemma~\ref{lem:exec3_alpha2}. 
In the execution fragment $ \fragt{I_1}{\alpha_2}{} \circ  \fragt{F_{1,1}}{\alpha_2}{v_1^1} \circ \fragt{F_{1,2}}{\alpha_2}{v_2^1} 
\circ \fragt{E_1}{\alpha_2}{v_1^1, v_2^1}$  in $\alpha_2$,  none of the actions occur at $r_2$ and  by Lemma~\ref{lem:exec3_alpha1}, $a_{k+1}$ occurs at $r_1^A$, 
also the actions in $\fragt{I_2}{}{}$ occur only at $r_2$.
Starting with $\alpha_2$, and by repeatedly using Lemma~\ref{lem:exec3_commute}, we create a sequence of four fair executions of $\mathcal{B}$ by repeatedly swapping 
 $\fragt{I_2}{\alpha_2}{}$ with the execution fragments 
$\fragt{E_1}{\alpha_2}{v_1^1, v_2^1}$, $\fragt{F_{1,2}}{\alpha_2}{v_2^1}$, $ \fragt{F_{1,1}}{\alpha_2}{v_1^1}$
and $\fragt{I_1}{\alpha_2}{}$, which appears in   $ \fragt{I_1}{\alpha_2}{} \circ  \fragt{F_{1,1}}{\alpha_2}{v_1^1} \circ \fragt{F_{1,2}}{\alpha_2}{v_2^1} 
\circ \fragt{E_1}{\alpha_2}{v_1^1, v_2^1}
\circ \fragt{I_2}{\alpha_2}{}$, 
where the following sequence of execution fragments
 $ \fragt{I_1}{\alpha_2}{} \circ  \fragt{F_{1,1}}{\alpha_2}{v_1^1} \circ \fragt{F_{1,2}}{\alpha_2}{v_2^1}  \circ \fragt{I_2}{\alpha_2}{} \circ \fragt{E_1}{\alpha_2}{v_1^1, v_2^1}$ (by commuting  $\fragt{I_2}{\alpha_2}{}$  and $\fragt{E_1}{\alpha_2}{v_1^1, v_2^1}$); ~
 $ \fragt{I_1}{\alpha_2}{} \circ  \fragt{F_{1,1}}{\alpha_2}{v_1^1} \circ \fragt{I_2}{\alpha_2}{}  \circ \fragt{F_{1,2}}{\alpha_2}{v_2^1} \circ \fragt{E_1}{\alpha_2}{v_1^1, v_2^1}$ (by commuting $\fragt{I_2}{\alpha_2}{}$  and $\fragt{F_{1,2}}{\alpha_2}{v_2^1}$); ~
 $ \fragt{I_1}{\alpha_2}{} \circ  \fragt{I_2}{\alpha_2}{}  \circ \fragt{F_{1,1}}{\alpha_2}{v_1^1} \circ \fragt{F_{1,2}}{\alpha_2}{v_2^1} \circ \fragt{E_1}{\alpha_2}{v_1^1, v_2^1}$ (by commuting   $\fragt{I_2}{\alpha_2}{}$  and $\fragt{F_{1,1}}{\alpha_2}{v_1^1}$)
appear. Finally, we have an  execution $\alpha'$ of the form 
$ \finiteprefixA{k}{k+1} \circ  \fragt{I_2}{\alpha''}{} \circ 
\frage{R_1}{}{v_1^1, v_2^1}
\circ \fragt{F_{2,1}}{\alpha'}{v_1^1} \circ \fragt{F_{2,2}}{\alpha'}{v_2^1} \circ \fragt{E_2}{\alpha_3'}{v_1^1, v_2^1}
\circ \fragt{S}{\alpha'}{}$ (by commuting $\fragt{I_2}{\alpha_2}{}$ and $\fragt{I_1}{\alpha_2}{}$)
Next, from $\alpha'$, by using Lemma~\ref{lem:exec3_commute}  and swapping $a_{k+1}$ with $\fragt{I_2}{\alpha_2}{}$ we show the existence  of  a fair execution 
 $\alpha_3$  as stated in the lemma.
\end{proof}

In the following lemma, we show that we can create a fair execution $\alpha_4$, of $\mathcal{B}$, where 
$\fragt{F_{2,2}}{\alpha_4}{}$ occurs immediately before  $ \fragt{E_1}{\alpha_4}{v_1^1, v_2^1}$, while $\fragt{R_1}{\alpha_4}{}$ and 
$\fragt{R_2}{\alpha_4}{}$ both return 
$(v_1^1, v_2^1)$.
\begin{lemma}[Existence of $\alpha_4$] \label{lem:exec3_alpha4} 
\sloppy There exists  fair execution $\alpha_4$  of $\mathcal{B}$ that contains transactions $W$, $R_1$ and $R_2$ and  can be written in the form
$ \finiteprefixA{k-1}{k} \circ \fragt{I_2}{\alpha_4}{}  \circ a_{k+1} $$ \circ \fragt{I_1}{\alpha_4}{}
\circ \fragn{F_{1,1}}{\alpha_4}{v_1^1} \circ   \fragn{F_{1,2}}{\alpha_4}{v_2^1} 
\circ \fragn{F_{2,2}}{\alpha_4}{v_2^1} 
\circ \fragn{E_1}{\alpha_4}{v_1^1, v_2^1}
$$\circ \fragn{F_{2,1}}{\alpha_4}{v_1^1} \circ  \fragn{E_2}{\alpha_4}{v_1^1, v_2^1}\circ \fragt{S}{\alpha_4}{}$, where both $R_1$ and $R_2$ return $(v_1^1, v_2^1)$.
\end{lemma}

\begin{proof}
We start with an execution  $\alpha_3$, as in  Lemma~\ref{lem:exec3_alpha3}, and apply Lemma~\ref{lem:exec3_commute} twice.  

First, by  Lemma~\ref{lem:exec3_commute}, we know there exists a fair execution $\alpha'$ of $\mathcal{B}$
where  $\fragt{F_{2,1}}{\alpha_3}{}$ (identify as $G_1$) and 
$\fragt{F_{2,2}}{\alpha_3}{}$ (identify as $G_2$)  are interchanged since actions of 
$\fragt{F_{2,1}}{\alpha_3}{}$ occurs solely at $s_1$ and those of $\fragt{F_{2,2}}{\alpha_3}{}$ at $s_2$, 
and  $\fragt{F_{2,1}}{\alpha_3}{}$ and $\fragt{F_{2,2}}{\alpha_3}{}$ return $v_1^1$ and $v_2^1$, respectively, to $r_2$.


Next, by Lemma~\ref{lem:exec3_commute} there is 
fair execution  of $\mathcal{B}$,  say $\alpha_4$ where
the fragments 
$\fragt{E_1}{\alpha_3}{}$ (identify as $G_1$)  and 
$\fragt{F_{2,2}}{\alpha_3}{}$ (identify as $G_2$) are interchanged, with respect to $\alpha'$, because  the actions in  $\fragt{E_1}{\alpha'}{}$ occur at $r_1$ and 
those of $\fragt{F_{2,2}}{\alpha_3}{}$ at $s_2$. Furthermore, $\alpha_4$
  can be written in the form
 $  \finiteprefixA{k-1}{k}  \circ  \fragt{I_2}{\alpha''}{} \circ  a_{k+1}  \circ $$
  \fragt{I_1}{\alpha''}{} \circ \fragt{F_{1,1}}{\alpha''}{v_1^1}
   \circ \fragt{F_{1,2}}{\alpha''}{v_2^1} 
  \circ \fragt{F_{2,2}}{\alpha''}{v_2^1} 
\circ \fragt{E_1}{\alpha''}{v_1^1, v_2^1}
\circ \fragt{F_{2,1}}{\alpha''}{v_1^1} \circ \fragt{E_2}{\alpha''}{v_1^1, v_2^1}
\circ \fragt{S}{\alpha''}{}$.
\end{proof}

 Next, we create a new fair execution  $\alpha_5$ of $\mathcal{B}$ where 
    $\fragt{F_{2,2}}{\alpha_5}{}$ occurs before  $ \fragt{F_{1,2}}{\alpha_5}{}$. However, because the actions in 
  both of these execution fragments   occur at the same automaton care has to be taken to swap these fragments 
    compared to $\alpha_4$.
\begin{lemma}[Existence of $\alpha_5$] \label{lem:exec3_alpha4b} 
\sloppy There exists  fair execution $\alpha_4$  of $\mathcal{B}$ that contains transactions $W$, $R_1$ and $R_2$ and  can be written in the form
$ \finiteprefixA{k-1}{k} \circ \fragt{I_2}{\alpha_5}{}  \circ a_{k+1} $$ \circ \fragt{I_1}{\alpha_5}{}
\circ \fragn{F_{1,1}}{\alpha_5}{v_1^1} \circ \fragn{F_{2,2}}{\alpha_5}{v_2^1} \circ  \fragn{F_{1,2}}{\alpha_5}{v_2^1} \circ \fragn{E_1}{\alpha_5}{v_1^1, v_2^1}
$$\circ \fragn{F_{2,1}}{\alpha_5}{v_1^1} \circ  \fragn{E_2}{\alpha_5}{v_1^1, v_2^1}\circ \fragt{S}{\alpha_5}{}$, 
where both $R_1$ and $R_2$ return $(v_1^1, v_2^1)$.
\end{lemma}

\begin{proof}
In $\alpha_4$, all actions  in $ \fragt{F_{1,2}}{\alpha_4}{} $ and 
  $\fragt{F_{2,2}}{\alpha_4}{}$ occur at $s_2$.  Consider the prefix of $\alpha_4$ that ends with $\fragn{F_{1,1}}{\alpha''}{v_1^1}$. We extend this prefix as follows.
In this prefix,  the actions $send(m_2^{r_2})_{r_2, s_2}$ and 
 $send(m_2^{r_1})_{r_1, s_2}$ do not have their corresponding $recv$ actions.  Suppose  the adversary 
delivers $m_2^{r_2}$ at $s_2$ (via the action $recv(m_2^{r_2})_{r_2, s_2}$) and delays all actions, other than internal and output actions at $s_2^A$, until $s_2$ responds with $v_2$, via  action $send(v_2)_{s_2, r_2}$. This extended execution fragment is of the form $\fragt{F_{2,2}}{\alpha_4}{}$. Similarly, the adversary further extends the execution by placing  the 
action $recv(m_2^{r_1})_{r_1, s_2}$ at $s_2$  and create the execution fragment of form $\fragt{F_{1,2}}{\alpha_4}{}$. Note that, so far, the actions due to the above extensions are entirely at $s_2$. Suppose the adversary makes  the execution 
fragments $\fragt{E_1}{\alpha''}{}$ next, by delivering values sent during $\fragt{F_{1,1}}{\alpha_4}{}$ and $\fragt{F_{1,2}}{\alpha_4}{}$ via the actions  $recv(v_1)_{s_1, r_1}$ and $recv(v_2)_{s_2, r_1}$, respectively, at $r_1$. Then $\fragt{F_{2,1}}{\alpha''}{}$ appear next, such that this fragment contains exactly the same sequence of actions as  in the corresponding execution fragment in  $\alpha_4$.
This is possible because they are not influenced by  any output action in $\fragt{F_{2,2}}{\alpha_4}{}$  or $\fragt{F_{1,2}}{\alpha_4}{}$. 
Suppose the adversary places the execution fragment  $\fragt{E_2}{\alpha''}{}$ next.
Let us denote the fair execution that is a extension of this finite execution so far as $\alpha_5$, which is of the form $ \finiteprefixA{k-1}{k} \circ \fragt{I_2}{\alpha_5}{}  \circ a_{k+1} $$ \circ \fragt{I_1}{\alpha_5}{}
\circ \fragt{F_{1,1}}{\alpha_5}{} \circ \fragt{F_{2,2}}{\alpha_5}{} \circ  \fragt{F_{1,2}}{\alpha_5}{} \circ \fragt{E_1}{\alpha_5}{}
$$\circ \fragt{F_{2,1}}{\alpha_5}{} \circ  \fragt{E_2}{\alpha_5}{}\circ \fragt{S}{\alpha_5}{}$.
 Now we need to argue about the values returned by the reads.

 

Note that  the execution fragment  $\frage{F_{1,1}}{\alpha_4}{}$ in both $\alpha_4$ and $\alpha_5$ is the same,  therefore,   $\frage{F_{1,1}}{\alpha_4}{} \stackrel{s_1}{\sim} \frage{F_{1,1}}{\alpha_5}{}$. Hence as in 
$\alpha_4$,  $s_1$  returns $v_1^1$  in the execution fragment  $\fragt{F_{1,1}}{\alpha_4}{}$  in   $\alpha_5$. Next  by Lemma~\ref{lem:exec3_equiv} for $R_1$,  $s_2$ returns $v_2^1$ in $\fragt{F_{1,2}}{\alpha_5}{}$  and  hence by the $S$ property, $R_1(\alpha_5)$ returns $(v_1^1, v_2^1)$, i.e.,   that $r_1$ returns the new version of object values. Therefore, $\frage{F_{1,1}}{\alpha_4}{}$,  $\fragt{F_{1,2}}{\alpha_5}{}$ and $\fragt{E_1}{\alpha_5}{}$ are of the form $ \fragt{F_{1,1}}{\alpha_5}{v_1^1}$, $\fragt{F_{1,2}}{\alpha_5}{v_2^1}$ and  $\fragt{E_1}{\alpha_5}{v_1^1, v_2^1}$, respectively.

Note that by construction of $\alpha_5$ above,  the execution fragment  $\fragt{F_{2,1}}{\alpha_4}{}$ in both $\alpha_4$ and $\alpha_5$ is the same, therefore,   $\frage{F_{2,1}}{\alpha_4}{} \stackrel{s_1}{\sim} \frage{F_{2,1}}{\alpha_5}{}$. Hence as in 
$\alpha_4$,  $s_1$  returns $v_1^1$  in the execution fragment  $\frage{F_{2, 1}}{\alpha_5}{}$  in   $\alpha_5$,  i.e.,  of the form $\frage{F_{2, 1}}{\alpha_5}{v_1^1}$.
Since $s_1$ returns $v_1^1$ in $\fragt{F_{2, 1}}{\alpha_5}{}$ in $\alpha_5$,  by   
Lemma~\ref{lem:exec3_equiv}  and   the $S$ property,
  $R_2$ returns $(v_1^1, v_2^1)$  and hence $\fragt{E_2}{\alpha_5}{}$ is of the form $\fragt{E_2}{\alpha_5}{v_1^1, v_2^1}$.

From the above argument we know that  $\alpha_5$ is of the form $ \finiteprefixA{k-1}{k} \circ \fragt{I_2}{\alpha_5}{}  \circ a_{k+1} $$ \circ \fragt{I_1}{\alpha_5}{}
\circ \fragt{F_{1,1}}{\alpha_5}{v_1^1} \circ \fragt{F_{2,2}}{\alpha_5}{v_2^1} \circ  \fragt{F_{1,2}}{\alpha_5}{v_2^1} \circ \fragt{E_1}{\alpha_5}{v_1^1, v_2^1}
$$\circ \fragt{F_{2,1}}{\alpha_5}{v_1^1} \circ  \fragt{E_2}{\alpha_5}{v_1^1, v_2^1}\circ \fragt{S}{\alpha_5}{}$.
\end{proof}

\remove{
\begin{proof}
We create a new fair execution $\alpha_4$  from execution  $\alpha_3$ of Lemma~\ref{lem:exec3_alpha3} by moving 
the execution fragment $\fragt{F_{2,2}}{}{}$ before $\fragt{F_{1,2}}{}{}$ to have it in the form 
$ \sigma_0, a_1, \cdots  a_k, \sigma_{k} \circ  \fragt{I_2}{\alpha_4}{} \circ  a_{k+1}, \sigma_{k+1} \circ $$
  \fragt{I_1}{\alpha_4}{} \circ \fragt{F_{1,1}}{\alpha_4}{} \circ \fragt{F_{1,2}}{\alpha_4}{} 
\circ \fragt{E_1}{\alpha_4}{}
\circ \fragt{F_{2,1}}{\alpha_4}{} \circ \fragt{F_{2,2}}{\alpha_4}{} \circ \fragt{E_2}{\alpha_4}{}
\circ \fragt{S}{\alpha_4}{}$.
 Now, since $\fragt{F_{1,1}}{\alpha_3}{} \stackrel{s_1}{\sim} \fragt{F_{1,1}}{\alpha_4}{}$ then by Lemma~\ref{lem:exec_commute}  $\alpha_4$ is a fair execution of  $\mathcal{B}$.

$send(v_1^1)_{s_1, r_1}$ occurs in $\alpha_4$ and since 
$\fragt{F_{1,1}}{\alpha_3}{} \circ \fragt{F_{2,1}}{\alpha_3}{}\stackrel{s_1}{\sim} \fragt{F_{1,1}}{\alpha_4}{}\circ\fragt{F_{2,1}}{\alpha_4}{}$ and hence
the action $send(v_2^1)_{s_2, r_1}$ occurs in $\fragt{F_{2,1}}{\alpha_4}{}$. Hence  $\alpha_4$ can be written as 
$ \sigma_0, a_1, \cdots  a_k, \sigma_{k} \circ  \fragt{I_2}{\alpha_4}{}  \circ a_{k+1}, \sigma_{k+1} $$ \circ \fragt{I_1}{\alpha_4}{}
\circ \fragt{F_{1,1}}{\alpha_4}{v_1^1} \circ \fragt{F_{2,2}}{\alpha_4}{v_2^1} \circ  \fragt{F_{1,2}}{\alpha_4}{v_2^1} \circ \fragt{E_1}{\alpha_4}{v_1^1, v_2^1}
$$\circ \fragt{F_{2,1}}{\alpha_4}{v_1^1} \circ  \fragt{E_2}{\alpha_4}{v_1^1, v_2^1}\circ \fragt{S}{\alpha_4}{}$.
\end{proof}
}

In the next lemma, we show the existence of a fair execution of $\mathcal{B}$ where $R_1$ returns $(v_1^0, v_2^0)$  and $I_2$ occurs immediately after $a_{k}$ and 
 $R_2$ responds with $(v_1^1, v_2^1)$. In fact, this is the most important of the sequence of fair executions of  
$\mathcal{B}$  (Fig.~\ref{fig:executions3})  because later with this  we prove in Theorem~\ref{thm:snow3} the existence of a
fair execution of $\mathcal{B}$ where a {\sc read} returns object-values of an earlier version compared to a previous {\sc read} that is not
concurrent with it.
\begin{lemma}[Existence of $\alpha_6$] \label{lem:exec3_alpha5} 
\sloppy There exists  fair execution $\alpha_6$  of $\mathcal{B}$ that contains transactions $W$, $R_1$ and $R_2$ and can be
written in the form 
$ \finiteprefixA{k-1}{k} \circ\fragt{I_2}{\alpha_6}{} \circ  \fragt{I_1}{\alpha_6}{} \circ\fragn{F_{1,1}}{\alpha_6}{v_1^0}
\circ\fragn{F_{2,2}}{\alpha_6}{v_2^1}\circ \fragn{F_{1,2}}{\alpha_6}{v_2^0} \circ\fragn{E_1}{\alpha_6}{v_1^0, v_2^0}
\circ\fragn{F_{2,1}}{\alpha_6}{v_1^1} \circ \fragn{E_2}{\alpha_6}{v_1^1, v_2^1}\circ \fragt{S}{\alpha_6}{}$, 
where  $R_1$ returns $(v_1^0, v_2^0)$  and $R_2$ returns $(v_1^1, v_2^1)$.
\end{lemma}

\begin{proof}
The crucial part of this proof is to carefully use the result of  Lemma~\ref{lem:exec3_alpha1} so that $R_1$ returns $(v_1^0, v_2^0)$, instead of $(v_1^1, v_2^1)$.
Note that by the construction of $\alpha_5$, as in Lemma~\ref{lem:exec3_alpha4b}, the same prefix $\finiteprefixA{k-1}{k}$  appears in the fair executions $\alpha_5$, and the executions $\alpha_0$ and  $\alpha_1$ as in Lemma~\ref{lem:exec3_alpha1}, where
 $k$ is defined as in Lemma~\ref{lem:exec3_alpha1}.

Note that by Lemma~\ref{lem:exec3_alpha1}, action $a_{k+1}$ occurs at $r_1^A$.
 In $\alpha_5$,  in the execution fragment 
 $a_{k+1} $$ \circ \fragt{I_1}{\alpha_5}{}
\circ \fragt{F_{1,1}}{\alpha_5}{v_1^1} \circ \fragt{F_{2,2}}{\alpha_5}{v_2^1}$, the actions in  execution fragment 
 $a_{k+1} $$ \circ \fragt{I_1}{\alpha_4}{}$ occur at $r_1^A$; actions in 
$\fragt{F_{1,1}}{\alpha_4}{v_1^1}$ occur at $s_1^A$; and  actions in $\fragt{F_{2,2}}{\alpha_4}{v_2^1}$ occur at $s_2^A$. 
Now consider the  prefix of execution $\alpha_4$ ending with $I_2$ and  suppose the adversary invokes $R_1$ immediately after $I_2$  (instead of 
after $a_{k+1}$) and  extends by the execution fragment  $ \fragt{I_1}{\epsilon}{} \circ \fragt{F_{1,1}}{\epsilon}{} \circ  \fragt{F_{2,2}}{\epsilon}{}$ to create a new finite execution $\epsilon$, which is of the form $\finiteprefixA{k-1}{k}  \circ \fragt{I_2}{\epsilon}{} \circ \fragt{I_1}{\epsilon}{} \circ \fragt{F_{1,1}}{\epsilon}{} \circ  \fragt{F_{2,2}}{\epsilon}{}$. Note that as a result, $a_{k+1}$ may not be in $\epsilon$ because we are introducing changes before $a_{k+1}$ can occur.

Note  that if  in the prefix
 $\finiteprefixA{k-1}{k}  \circ \frage{I_2}{\epsilon}{} \circ \frage{I_1}{\epsilon}{} \circ \frage{F_{1,1}}{\epsilon}{} \circ  \frage{F_{2,2}}{\epsilon}{}$  of $\epsilon$ 
we ignore the actions in $\frage{I_2}{\epsilon}{}$
 then the remaining execution is the same as the prefix  
 $\finiteprefixA{k-1}{k}  \circ  \frage{I_1}{\alpha_0}{} \circ \frage{F_{1,1}}{\alpha_0}{} \circ  \frage{F_{2,2}}{\alpha_0}{}$ of $\alpha_0$ in 
Lemma~\ref{lem:exec3_alpha1}. Here we explicitly use the notations $\epsilon$ and $\alpha_0$ to avoid confusion. Since the actions in 
$\frage{I_2}{\epsilon}{}$ have no influence in  the actions on 
 $\frage{I_1}{\epsilon}{} \circ \frage{F_{1,1}}{\epsilon}{} \circ  \frage{F_{2,2}}{\epsilon}{}$, therefore,
we have $\frage{F_{1,1}}{\epsilon}{} \stackrel{s_1}{\sim} \frage{F_{1,1}}{\alpha_0}{}$, and hence by Lemma~\ref{lem:exec3_consistent} 
  $\frage{F_{1,1}}{\epsilon}{}$ returns $v_1^0$ as in  $\frage{F_{1,1}}{\alpha}{}$, i.e.,  in $\fragn{F_{1,1}}{\epsilon}{v_1^0}$, $s_1$ returns $v_1^0$. 
Now by Lemma~\ref{lem:exec3_equiv} we  conclude that 
for  any  extension of $\epsilon$, say $\gamma$, {\sc read} 
 $R_1(\gamma)$ returns $v_1^0$ for object $o_1$ and by the S property  $R_1(\gamma)$ returns  $(v_1^0, v_2^0)$. Also, since 
$\frage{F_{2,2}}{\alpha_5}{} \stackrel{s_2}{\sim} \frage{F_{2,2}}{\epsilon}{} \stackrel{s_2}{\sim} \frage{F_{2,2}}{\gamma}{}$  by Lemma~\ref{lem:exec3_equiv} and the S property,  $R_2(\gamma)$ must return $(v_1^1, v_2^1)$.  Therefore, $\gamma$ has an extension to a  fair 
execution $\alpha_6$ (Fig.~\ref{fig:executions3}) which is of  the form $ \finiteprefixA{k-1}{k}  \circ\fragt{I_2}{\alpha_6}{} \circ  \fragt{I_1}{\alpha_6}{} \circ\fragt{F_{1,1}}{\alpha_6}{v_1^0}
\circ\fragt{F_{2,2}}{\alpha_6}{v_2^1}\circ \fragt{F_{1,2}}{\alpha_6}{v_2^0} \circ\fragt{E_1}{\alpha_6}{v_1^0, v_2^0}
\circ\fragt{F_{2,1}}{\alpha_6}{v_1^1} \circ \fragt{E_2}{\alpha_6}{v_1^1, v_2^1}\circ \fragt{S}{\alpha_6}{}$ as in the statement of the lemma.
\end{proof}

In the following lemma,  starting from $\alpha_6$ in Lemma~\ref{lem:exec3_alpha5} we create a fair execution $\alpha_7$ for $\mathcal{B}$ where $\fragt{F_{2,1}}{\alpha_7}{}$ 
appears  before $\fragn{F_{1,2}}{\alpha_7}{v_2^0} \circ\fragn{E_1}{\alpha_7}{v_1^0, v_2^0}$, where $R_1$ returns $(v_1^0, v_2^0)$ and $R_2$ returns $(v_1^1, v_2^1)$.
At high level, we will be working on moving the execution fragments  of $R_2$ forward, a little at a time, until finally we have $R_2$ finishing before $R_1$ starts.  This simply uses commutativity since the actions in the swapped execution fragments occurs at different automata.

\begin{lemma}[Existence of $\alpha_7$] \label{lem:exec3_alpha6} 
\sloppy There exists  fair execution $\alpha_7$  of $\mathcal{B}$ that contains transactions $W$, $R_1$ and $R_2$, and   can be written in the form
$\finiteprefixA{k-1}{k} \circ \fragt{I_2}{\alpha_7}{}  \circ \fragt{I_1}{\alpha_7}{} \circ \fragn{F_{1,1}}{\alpha_7}{v_1^0} 
\circ \fragn{F_{2,2}}{\alpha_7}{v_2^1}\circ \fragn{F_{2,1}}{\alpha_7}{v_1^1} 
 \circ \fragn{F_{1,2}}{\alpha_7}{v_2^0} \circ\fragn{E_1}{\alpha_7}{v_1^0, v_2^0}\circ
 \fragn{E_2}{\alpha_7}{v_1^1, v_2^1}\circ \fragt{S}{\alpha_7}{}$ where $R_1$ returns $(v_1^0, v_2^0)$ and $R_2$ returns $(v_1^1, v_2^1)$.
\end{lemma}

\begin{proof}
\sloppy This result is proved by applying the result of Lemma~\ref{lem:exec3_commute}  to the fair execution created in Lemma~\ref{lem:exec3_alpha5}. 
Suppose,  $\alpha_6$ (Fig.~\ref{fig:executions3}) is a fair  execution as  in Lemma~\ref{lem:exec3_alpha5}, 
where in  the   execution fragment 
$\fragt{E_1}{\alpha_6}{v_1^0, v_2^0}\circ\fragt{F_{2,1}}{\alpha_6}{}$  we identify 
 $\fragt{E_1}{\alpha_6}{v_1^0, v_2^0}$  as $G_1$ and 
$\fragt{F_{1,2}}{\alpha_6}{v_2^0}$  as $G_2$. The actions of $G_1$ and $G_2$ occur at two distinct automata, therefore,  we  can use the result of Lemma~\ref{lem:exec3_commute}, to argue that there exists a fair execution $\alpha'$ of $\mathcal{B}$  that  contains the  execution fragment 
$\fragt{F_{2,1}}{\alpha_7}{}  \circ\fragt{E_1}{\alpha_7}{v_1^0, v_2^0}$, and $\alpha_6$ and $\alpha'$ are identical in the prefixes and suffixes corresponding to $G_1$ and $G_2$.

 Now,  $\alpha'$ contains  $\fragt{F_{1,2}}{\alpha''}{} \circ \fragt{F_{2,1}}{\alpha'}{}$, where  
  the actions in  $\fragt{F_{1,2}}{\alpha''}{}$ (identified as $G_1$) and $\fragt{F_{2,1}}{\alpha''}{}$ (identify as $G_2$)  occur  at distinct automata. Hence, by  Lemma~\ref{lem:exec3_commute} there exists  an execution $\alpha_7$ of the form
$\finiteprefixA{k-1}{k}  \circ \fragt{I_2}{\alpha_7}{}  \circ \fragt{I_1}{\alpha_7}{} \circ \fragt{F_{1,1}}{\alpha_7}{v_1^0} 
\circ \fragt{F_{2,2}}{\alpha_7}{v_2^1}\circ \fragt{F_{2,1}}{\alpha_7}{v_1^1} 
 \circ \fragt{F_{1,2}}{\alpha_7}{v_2^0} \circ\fragt{E_1}{\alpha_7}{v_1^0, v_2^0}\circ
 \fragt{E_2}{\alpha_7}{v_1^1, v_2^1}\circ \fragt{S}{\alpha_7}{}$.
\end{proof}
In the following lemma by using simple commuting arguments of Lemma~\ref{lem:exec3_commute}, we show the existence of a fair execution $\alpha_7$ of $\mathcal{B}$ where $\fragt{F_{2,2}}{\alpha_8}{}$ appears before $\fragt{I_1}{\alpha_8}{} \circ \fragt{F_{1,1}}{\alpha_8}{}$, where $R_1$ returns $(v_1^0, v_2^0)$ and $R_2$ returns $(v_1^1, v_2^1)$.

\begin{lemma} [Existence of $\alpha_8$]  \label{lem:exec3_alpha7} 
\sloppy There exists  fair execution $\alpha_8$  of $\mathcal{B}$ that contains transactions $W$, $R_1$ and $R_2$
and   can be written in the form 
$\finiteprefixA{k-1}{k}  \circ  \fragt{I_2}{\alpha_8}{} \circ \fragn{F_{2,2}}{\alpha_8}{v_2^1} \circ 
$$\fragt{I_1}{\alpha_8}{} \circ \fragn{F_{1,1}}{\alpha_8}{v_1^0} 
\circ  \fragn{F_{2,1}}{\alpha_8}{v_1^1} 
$$ \circ \fragn{F_{1,2}}{\alpha_8}{v_2^0} \circ \fragn{E_1}{\alpha_8}{v_1^0, v_2^0}
\circ \fragn{E_2}{\alpha_8}{v_1^1, v_2^1}\circ \fragt{S}{\alpha_8}{}$, where $R_1$ returns $(v_1^0, v_2^0)$ and $R_2$ returns $(v_1^1, v_2^1)$.
\end{lemma}

\begin{proof}
 Consider the fair execution $\alpha_7$ of $\mathcal{B}$ as in Lemma~\ref{lem:exec3_alpha6}. In the context of 
  of  Lemma~\ref{lem:exec3_commute}, in $\alpha_7$ (Fig.~\ref{fig:executions3}) the actions in  
 $ \fragt{F_{1,1}}{\alpha_8}{}$ (identify as $G_1$)  occur at $s_1^A$  and  those in $\fragt{F_{2,2}}{\alpha_8}{}$ (identify as $G_2$) at  $s_2^A$. Then by  
 Lemma~\ref{lem:exec3_commute} there exists a fair execution $\alpha'$ of $\mathcal{B}$,  of the form 
 $ \finiteprefixA{k-1}{k}  \circ \fragt{I_2}{\alpha'}{}  \circ \fragt{I_1}{\alpha''}{} 
 \circ \fragn{F_{2,2}}{\alpha'}{v_2^1} 
\circ \fragn{F_{1,1}}{\alpha'}{v_1^0} 
\circ \fragn{F_{2,1}}{\alpha'}{v_1^1} 
 \circ \fragn{F_{1,2}}{\alpha'}{v_2^0} \circ\fragn{E_1}{\alpha'}{v_1^0, v_2^0}\circ
 \fragn{E_2}{\alpha''}{v_1^1, v_2^1}\circ \fragt{S}{\alpha'}{}$, where $ \fragt{F_{2,2}}{\alpha_8}{}$ and 
  $ \fragt{F_{1,1}}{\alpha_8}{}$  are interchanged.
 
 Since  actions in  $ \fragt{F_{2,2}}{\alpha_8}{}$ (identify as $G_1$)  occur at $s_1^A$ and those in 
  $ \fragt{I_{1}}{\alpha_8}{}$ (identify as $G_1$)  occur at $s_1^A$ then by Lemma~\ref{lem:exec3_commute}
  there is a  fair execution of $\mathcal{B}$, $\alpha_8$ where $\fragt{F_{2,2}}{\alpha_8}{}$ appear before $\fragt{I_1}{\alpha_8}{}$, i.e., of the form  $\finiteprefixA{k-1}{k}  \circ \fragt{I_2}{\alpha_8}{} \circ \fragt{F_{2,2}}{\alpha_8}{}  \circ
 \fragt{I_1}{\alpha_7}{} \circ \fragt{F_{1,1}}{\alpha_8}{} 
\circ \fragt{F_{2,1}}{\alpha_8}{} 
 \circ \fragt{F_{1,2}}{\alpha_8}{} \circ\fragt{E_1}{\alpha_8}{} \circ
 \fragt{E_2}{\alpha_8}{}\circ \fragt{S}{\alpha_8}{}$, where $ \fragt{F_{2,2}}{\alpha_8}{}$ and 
  $ \fragt{I_{1}}{\alpha_8}{}$  are interchanged.
 
 By $(ii)$ of Lemma~\ref{lem:exec3_commute} we have 
$\frage{F_{2,1}}{\alpha'}{} \stackrel{s_1}{\sim} \frage{F_{2,1}}{\alpha_8}{}$ hence $\fragt{F_{2,1}}{\alpha_8}{}$ sends $v_1^1$ and 
$\fragt{F_{1,1}}{\alpha_8}{}$ and $\fragt{F_{1,2}}{\alpha_8}{}$ sends $v_1^0$ and $v_2^0$, respectively. So considering these returned values we have $\alpha_8$ 
(Fig.~\ref{fig:executions3}) in the form as stated in the lemma.
\end{proof}

The following lemma shows the existence of a fair execution of $\mathcal{B}$, $\alpha_9$, where we move 
$\fragt{F_{2,1}}{}{}$  forward past $\fragt{F_{1,1}}{}{}$.
\begin{lemma} [Existence of $\alpha_9$]  \label{lem:exec3_alpha8} 
\sloppy There exists  fair execution $\alpha_9$  of $\mathcal{B}$ that contains transactions $W$, $R_1$ and $R_2$
and   can be written in the form 
$\finiteprefixA{k-1}{k}  \circ  \fragt{I_2}{\alpha_8}{} \circ \fragt{F_{2,2}}{\alpha_8}{v_2^1} \circ 
$$\fragt{I_1}{\alpha_8}{} \circ \fragt{F_{2,1}}{\alpha_8}{v_1^1} 
\circ  \fragt{F_{1,1}}{\alpha_8}{v_1^0} 
$$ \circ \fragt{F_{1,2}}{\alpha_8}{v_2^0} \circ \fragt{E_1}{\alpha_8}{v_1^0, v_2^0}
\circ \fragt{E_2}{\alpha_8}{v_1^1, v_2^1}\circ \fragt{S}{\alpha_8}{}$
where $R_1$ returns $(v_1^0, v_2^0)$ and $R_2$ returns $(v_1^1, v_2^1)$.
\end{lemma}

\begin{proof}
In $\alpha_8$ from Lemma~\ref{lem:exec3_alpha7}, all the actions in  
 $ \fragn{I_1}{\alpha_8}{}$  occur at $r_1$; those in   $ \fragn{F_{1,1}}{\alpha_8}{v_1^1}$  occur at $s_1$; and  the  
actions in $ \fragn{F_{2,1}}{\alpha_8}{v_2^1}$ occur only  at $s_1$. 
Note that actions of  both execution fragments $ \fragt{F_{2,1}}{\alpha_8}{}$  and   
$\fragt{F_{1,1}}{\alpha_8}{}$ occur at $r_1$.  
Consider the prefix of $\alpha_8$ that ends with $\fragt{I_1}{}{}$ then suppose the adversary  extends this prefix by adding an execution fragment of the form
$ \fragt{F_{2,1}}{\alpha_8}{} \circ  \fragt{F_{1,1}}{\alpha_8}{}$ as follows.  
First note that  the actions $send(m_1^{r_2})_{r_2, s_1}$ and 
 $send(m_1^{r_1})_{r_1, s_1}$ appears in the prefix but do not have corresponding $recv$ actions.

The  adversary places action $recv(m_1^{r_2})_{r_2, s_1}$, and allows an execution fragment of the form 
$ \fragt{F_{2,1}}{\alpha_8}{}$ to appear. Now, immediately after this the adversary further extends it with 
an execution fragment of the form  $\fragt{F_{1,1}}{\alpha_8}{}$  by placing action $recv(m_1^{r_1})_{r_1, s_1}$. 
 Next the fragment $\fragn{F_{1,2}}{\alpha_8}{v_2^0}$ is added  and is the same as $ \frage{F_{1,2}}{\alpha_8}{}$.
This last step can be argued by the fact that none of the actions in  $ \fragn{F_{1,2}}{\alpha_8}{v_2^0}$ can be affected by 
any of the output actions at $ \fragt{F_{2,1}}{\alpha_8}{}$ and  $\fragt{F_{1,1}}{\alpha_8}{}$.
 Note that the actions in  $\fragt{F_{1,2}}{}{}$ are taking place at  $s_2$, which is not affected by the above fragments, and therefore,  at the end of this fragment $s_2$  returns $v_1^0$, as in $\alpha_8$. But by $S$ property $\fragt{F_{1,1}}{}{}$ has to return $v_1^0$ as well.
 Note that a careful argument can be done by using Theorem~\ref{thm:fairtrace} to conclude the same. Following this the adversary allows the rest of the execution by adding an execution fragment of the form $\fragn{E_1}{\alpha_8}{v_1^0, v_2^0}
\circ \fragn{E_2}{\alpha_8}{v_1^1, v_2^1}\circ \fragn{S}{\alpha_8}{}$. The resulting fair execution is of the form 
$\finiteprefixA{k-1}{k}  \circ  \fragt{I_2}{\alpha_8}{} \circ \fragt{F_{2,2}}{\alpha_8}{v_2^1} \circ 
$$\fragt{I_1}{\alpha_8}{} \circ \fragn{F_{2,1}}{\alpha_8}{v_1^1} 
\circ  \fragn{F_{1,1}}{\alpha_8}{v_1^0} 
$$ \circ \fragt{F_{1,2}}{\alpha_8}{v_2^0} \circ \fragn{E_1}{\alpha_8}{v_1^0, v_2^0}
\circ \fragn{E_2}{\alpha_8}{v_1^1, v_2^1}\circ \fragt{S}{\alpha_8}{}$, where we retained the values wherever it is known, and we denote this fair execution by $\alpha_9$.

Now, we argue about the return values in $\alpha_9$. 
Applying Lemma~\ref{lem:exec3_equiv} to $R_2$ and $\fragn{F_{2,2}}{\alpha_8}{v_2^1}$ implies that $R_2$ 
returns $(v_1^1, v_2^1 )$. Similarly, 
applying Lemma~\ref{lem:exec3_equiv} to $R_1$ and $\fragn{F_{1,2}}{\alpha_8}{v_2^0}$ implies that $R_1$ 
must return $(v_1^0, v_2^0 )$ in $\alpha_9$.
\end{proof}

Now we show the existence of a fair execution of $\mathcal{B}$ where the execution fragments corresponding to $R_1$ appears before $R_2$, where  $R_1$ returns $(v_1^0, v_2^0)$ and $R_2$ completes by returning $(v_1^1, v_2^1)$.
\begin{lemma} [Existence of $\alpha_{10}$]  \label{lem:exec3_alpha11} 
\sloppy There exists  fair execution $\alpha_{10}$  of $\mathcal{B}$ that contains transactions $W$, $R_1$ and $R_2$
and   can be written in the form 
$\finiteprefixA{k-1}{k}   \circ
\frage{R_2}{}{v_1^1, v_2^1} \circ
 \frage{R_1}{}{v_1^0, v_2^0}
 \circ \fragt{S}{\alpha_{10}}{}$.
where $R_1$ returns $(v_1^0, v_2^0)$ and $R_2$ returns $(v_1^1, v_2^1)$.
\end{lemma}
\begin{proof}
Now, by using Lemma~\ref{lem:exec3_commute} to $\alpha_{9}$, we can  interchange 
 $\fragt{F_{2,1}}{}{}$  and $ \fragt{I_1}{}{}$ to create a fair execution $\alpha_{10}$  (Fig.~\ref{fig:executions3}) of $\mathcal{B}$, which is
of the form 
$ \finiteprefixA{k-1}{k}   \circ 
\fragt{I_2}{\alpha_9}{} \circ \fragt{F_{2,2}}{\alpha_9}{v_2^1} 
\circ   \fragt{F_{2,1}}{\alpha_9}{v_1^1}  \circ 
\frage{R_1}{}{v_1^0, v_2^0} \circ \fragt{E_2}{\alpha_8}{v_1^1, v_2^1}
 \circ \fragt{S}{\alpha_9}{}$, where the returned values are determined by  Lemma~\ref{lem:exec3_consistent}.

 
Note that in the execution fragment none of the actions in the execution fragment 
$\fragt{I_1}{\alpha_9}{} \circ \fragt{F_{1,1}}{\alpha_9}{v_1^0} 
 \circ \fragt{F_{1,2}}{\alpha_9}{v_2^0} \circ \fragt{E_1}{\alpha_9}{v_1^0, v_2^0}$
occur at $r_2^A$ and in $\fragt{E_2}{\alpha_9}{v_1^1, v_2^1} $ each of the action occur at $r_2^A$. Therefore, by 
applying Lemma~\ref{lem:exec3_commute}, we can consecutively swap  $\fragt{E_2}{}{}$ with 
$\fragt{E_1}{}{}$, $\fragt{F_{1,2}}{}{}$,  $\fragt{I_1}{}{}$  and $\fragt{F_{1,1}}{}{}$ we create a sequence of 
four fair executions of $\mathcal{B}$ to arrive at fair execution $\alpha_{10}$ (Fig.~\ref{fig:executions3}) of the form
$\finiteprefixA{k-1}{k}   \circ
\frage{R_2}{}{v_1^1, v_2^1}


 \circ
 \frage{R_1}{}{v_1^0, v_2^0}
 \circ \fragt{S}{\alpha_{10}}{}$.
\end{proof}

The following statement proves the statement of the SNOW Theorem  by showing the existence of  fair execution $\alpha_{10}$, of $\mathcal{B}$,  where $R_2$ completes before $R_1$ is invoked and  $R_2$ completes by returning $(v_1^1, v_2^1)$ whereas $R_1$ returns $(v_1^0, v_2^0)$, which  violates the $S$ property in $\alpha_{10}$. 
\begin{theorem}\label{thm:snow3}
 The SNOW properties cannot be implemented in a system with two readers and one writer, for two servers even in the presence of client-to-client communication.
\end{theorem}

\begin{proof}

\sloppy 
Note that  in  $\alpha_{10}$,  $R_2$ completes by returning 
$(v_1^1, v_2^1)$ and $R_1$, although invoked after $R_2$ returns  $(v_1^0, v_2^0)$,  is initiated and as a result $\alpha_{10}$ violates the $S$ property. 
\end{proof}

\remove{
\begin{theorem}
 The SNOW properties cannot be implemented in a system with two readers and one writer, for two servers even in the presence of client-to-client communication.
\end{theorem}

\begin{proof}
We prove the claim of the theorem by contradiction, by assuming there is an algorithm $X$ that satisfies the $SNOW$ properties. We do so by constructing  a  possible execution of $X$ where $S$ property is violated. 
The steps of constructing the execution  starts  with an initial execution fragment and construct a  sequence of execution fragments where each execution fragment is derived form the previous one in the sequence. We assume that the initial values of the objects $o_1$ and $o_2$ are $v_1^0$ and $v_2^0$, respectively.

Below we present the sequence of execution fragments and later we provide the proof for constructing it.

\emph{\underline{$\alpha_0$}:} First show the existence of an execution fragment $\alpha_0$, of algorithm $X$, such that a write operation $W$ as $\Writetr{ \writeop{o_1}{v_1^1}, \writeop{o_2, v_2^1}}$ is invoked in $\alpha_0$ and complete in $\alpha_0$. 


\emph{\underline{$\alpha_1$}:}  Next, based on execution fragment $\alpha_0$, we construct an execution fragment $\alpha_1$ for algorithm $X$, by 
extending a prefix, $\prefix{\alpha_0}{\sigma}$ of $\alpha_0$ by adding an execution fragment $\alpha^e_0$, which includes a read operation 
$R_1$, at $r_1$, where $\sigma$ is a state (Fig.~\ref{fig:execution_a_c} (a)), such that, 
\begin{enumerate}
\item [$(a)$] between the actions $\INV{R_1}$ and $\RESP{R_1}$  in execution fragment $\alpha^e_0$, the following sequences of action are present in the order : $\send{m_1^{R_1}}{r_1, s_1}$ and  $\send{m_1^{R_1}}{r_1, s_1}$ at $r_1$; $\recv{m_1^{R_1}}{r_1, s_1}$ and  $\recv{m_1^{R_1}}{r_1, s_1}$ at $s_1$ and $s_2$, respectively;  
 $\send{v^1_2}{s_1, r_1}$  and  $\send{v^1_2}{s_1, r_1}$ at $s_1$ and $s_2$, respectively;  
$\recv{v^1_2}{s_1, r_1}$  and  $\recv{v^1_2}{s_1, r_1}$  at $r_1$.  These are the only external invocations allowed in $\alpha^e_0$; and 
\item [$(b)$] $\sigma$ is the earliest of such state in $\alpha_0$ where $R_1$ returns $(v^1_1, v_2^1)$, i.e., valency $1$.
\end{enumerate}

\emph{\underline{$\alpha_2$}:} Next from execution fragment $\alpha_1$, we create another execution fragment of algorithm $X$, $\alpha_2$ by pasting a second {\sc read} transaction $R_2$, from reader $r_2$, after $\RESP{R_1}$.  Since $R_2$ is invoked after $R_1$ completes in $\alpha_2$, hence  by the S property of the algorithm  the transaction operation $R_2$ returns $(v_1^1, v_2^1)$ (Fig.~\ref{fig:execution_a_c} (b)).

\emph{\underline{$\alpha_3$}:} Next  based on execution fragment $\alpha_2$, we construct a new  execution fragment $\alpha_3$ of algorithm $X$, where $\INV{R_2}$ appears before $\INV{R_1}$ and both $R_1$ and $R_2$ returns $(v_1^1, v_2^1)$ (Fig.~\ref{fig:execution_a_c} (c)).

\emph{\underline{$\alpha_4$}:} Then we construct an execution fragment $\alpha_4$ with the following action in the order they are presented
$\INV{R_2}$, $\INV{R_1}$,   $\recv{m^{R_1}_1}{r_1, s_1}$,     $\recv{m^{R_1}_2}{r_1, s_2}$, $\RESP{R_1}$,
$\recv{m^{R_2}_1}{r_2, s_1}$,  $\recv{m^{R_2}_2}{r_2, s_2}$ and $\RESP{R_2}$, such that, $R_1$ and $R_2$ returns $(v_1^1, v_2^1)$
(Fig.~\ref{fig:execution_d_f} (d)). 

\emph{\underline{$\alpha_6$}:}  Now, from $\alpha_4$ we construct an execution fragment $\alpha_6$, for algorithm $X$ where $\INV{R_1}$
appears as a $1$-valent state, i.e., $R_1$ returns $(v_1^0, v_2^0)$. and $R_2$ returns $(v_1^1, v_2^1)$ 
(Fig.~\ref{fig:execution_d_f} (e)).

\emph{\underline{$\alpha_7$}:} Finally, from $\alpha_6$, we construct a new execution fragment $\alpha_7$ for algorithm $A$, where 
$\INV{R_1}$ and $\RESP{R_1}$ appears before $\INV{R_1}$ and $R_1$ returns $(v_1^0, v_2^0)$ and $R_2$ returns $(v_1^1, v_2^1)$  with the order of the actions in $\alpha_7$ as : 
$\INV{R_2}$, $\recv{m^{R_2}_1}{r_2, s_1}$,  $\recv{m^{R_2}_2}{r_2, s_2}$, $\RESP{R_2}$,  $\INV{R_1}$,   $\recv{m^{R_1}_1}{r_1, s_1}$,     $\recv{m^{R_1}_2}{r_1, s_2}$, $\RESP{R_1}$  (Fig.~\ref{fig:execution_d_f} (f)). 

Note that the external action $\RESP{R_2}$  corresponding to $R_2$ occurs before $\INV{R_1}$ and $R_1$ returns $(v_1^1, v_2^1)$ and $R_2$ returns $(v_1^0, v_2^0)$.  Therefore, the valid execution fragment for algorithm $X$,  $\alpha_7$ is  contradictory to the SNOW properties  assumption, because  a later {\sc read} transaction returns a earlier value that then a preceding read. 

\end{proof}
\begin{figure}[!ht]
      \centering
         \includegraphics[width=1.0\textwidth]{figures/exec_a_c.jpg}
         \caption{The order of the actions in the execution fragments $\alpha_1$, $\alpha_2$ and $\alpha_3$ shown in $(a)$, $(b)$ and $(c)$, respectively. } \label{fig:execution_a_c}
 \end{figure}
 \begin{figure}[!ht]
      \centering
         \includegraphics[width=1.0\textwidth]{figures/exec_d_f.jpg}
         \caption{The order of the actions in the execution fragments $\alpha_4$, $\alpha_6$ and $\alpha_7$ shown in $(d)$, $(e)$ and $(f)$, respectively.  } \label{fig:execution_d_f}
 \end{figure}


Now, we prove the existence of the individual execution fragments described above.


\begin{claim}\label{claim:0} {\bf [Construction of $\alpha_0$]}
Execution fragment $\alpha_0$ for algorithm $X$ exists.
\end{claim}
\begin{proof}
In the execution of algorithm $X$, the adversary invokes a {\sc write} transaction $W$ as 

$\Writetr{ \writeop{o_1}{ v_1^1}, \writeop{o_2}{ v_2^1}}$. By liveness assumption 
of {\sc write} transaction s there exists a response action $\RESP{W}$ at writer $w$. Let $\alpha_0$ be the execution fragment from the initial 
state $\sigma_0$ and the state immediately following the $\RESP{W}$ action. 

\end{proof}

\begin{claim} \label{claim:1}{\bf  [Construction of $\alpha_1$]}
Execution fragment $\alpha_1$ for algorithm $X$ exists.
\end{claim}
\begin{proof}
Note that the adversary can invoke a read at $r_1$ following which as per algorithm specification $X$, $r_1$ can have the 
output actions  $\send{m_1^{R_1}}{r_1, s_1}$ and  $\send{m_2^{R_1}}{r_1, s_2}$ followed by the  $\recv{v_1^1}{s_1, r_1}$ and 
 $\recv{v_2^1}{s_2, r_1}$. Since we assume algorithm $X$ which satisfies SNOW properties   a 
response action $\RESP{R_1}$ must appear after these above actions. In other words, the following sequence of actions at automation 
$r_i$ appears in a valid execution of $A$:  $\RESP{R_1}$, $\send{m_1^{R_1}}{r_1, s_1}$,  $\send{m_2^{R_1}}{r_1, s_2}$,
$\recv{v_1^1}{s_1, r_1}$,  $\recv{v_2^1}{s_1, r_1}$.

Next, consider the set of action in $\alpha_0$ occurring at automation $s_1$. Next we add the action  $\send{m_1^{R_1}}{r_1, s_1}$  at 
$s_1$ after the final state. Due to the N property  the execution at $s_1$ consists of $\send{v_1}{s_1, r_1}$ for some $v_1 \in V_1$.
Similarly execution is possible by  considering the actions at automation $s_2$ and  $\send{m_2^{R_1}}{r_1, s_2}$ and  
$\send{v_2}{s_2, r_1}$ for some $v_2 \in V_2$.

Now, by Theorem ` and the S property we have an execution starting with the final state of $\alpha_0$, there is an execution fragment 
$\alpha_0^e$ where there is a read operation $R_1$ from $r_1$ and responds with $(v_1^1, v_2^1)$. Note that we can deduce
that 
$v_1 = v_1^1$ and $v_2 = v_2^1$. So by Theorem 2 we construct and execution fragment $\alpha_1$, as $\alpha_0 \circ \alpha_0^e$. 

Now to realize $(a)$ in $\alpha_1$ we can assume by synchrony and N property there is no external action in $\alpha^e_0$ between the actions  send  send.

To realize $(b)$ note that by S property any read after $W$, assuming not other writer, must respond with $(v_1^1, v_2^1)$. Therefore, 
we pick a state $\sigma$ such that it is the earliest in $\alpha_0$ such that $\prefix{\alpha_0}{\sigma}\circ  \alpha_0^e$, such that 
$\alpha_0^e$ begins with state $\sigma$.
\end{proof}


\begin{claim}\label{claim:2} {\bf [Construction of $\alpha_2$] }
Execution fragment $\alpha_2$ for algorithm $X$ exists.
\end{claim}
\begin{proof}
The proof is similar to that of Claim~\ref{claim:1}.
\end{proof}

\begin{claim}\label{claim:3} {\bf  [Construction of $\alpha_3$]}
Execution fragment $\alpha_3$ for algorithm $X$ exists.
\end{claim}
\begin{proof}
Since $\INV{R_2}$ occurs at $r_2$ in execution $\alpha_2$ during $R_1$, there is no communication between $r_1$ and $r_2$ hence we 
can assume $\INV{R_2}$ before $\INV{R_1}$ to construct $\alpha_3$.
\end{proof}


\begin{claim}\label{claim:4} {\bf [Construction of $\alpha_4$]}
Execution fragment $\alpha_4$ for algorithm $X$ exists.
\end{claim}
\begin{proof}
Note that we have in $\alpha_3$ the following actions in the order as presented
$\INV{R_2}$, $\INV{R_1}$,   $\recv{m^{R_1}_1}{r_1, s_1}$,     $\recv{m^{R_1}_2}{r_1, s_2}$, $\RESP{R_1}$,
$\recv{m^{R_2}_1}{r_2, s_1}$,  $\recv{m^{R_2}_2}{r_2, s_2}$ and $\RESP{R_2}$, where both $R_1$ and $R_2$ responds with $(v_1^1, v_2^1)$. 
Note that from $\alpha_3$ we can create a new execution $\alpha_3'$ where $\RESP{R_1}$ and $\recv{m_1^{R_2}}{r_2, s_1}$ are 
swapped. Note that since $\RESP{R_1}$ occurs at $r_1$ and $\recv{m_1^{R_2}}{r_2, s_1}$ at $s_2$ hence by indistinguishability argument 
at $r_1$ and $r_2$ we claim that both $R_1$ and $R_2$ returns $(v_1^1, v_2^1)$ in $\alpha^3$.  Reasoning in a similar manner we can switch 
$\recv{m_1^{R_1}}{r_1, s_1}$ and $\recv{m_2^{R_2}}{r_2, s_2}$ in $\alpha_3''$ to construct an execution  $\alpha^4$ where both $R_1$ and $R_2$
returns $(v_1^1, v_2^1)$ such that the order of relevant actions appears as 
$\INV{R_2}$, $\INV{R_1}$,  $\recv{m^{R_2}_1}{r_2, s_1}$,  $\recv{m^{R_1}_1}{r_1, s_1}$,  $\recv{m^{R_1}_2}{r_1, s_2}$ , 
$\RESP{R_1}$ ,   $\recv{m^{R_2}_2}{r_2, s_2}$ and $\RESP{R_2}$,
\end{proof}

\begin{claim}\label{claim:5} {\bf [Construction of $\alpha_6$]}
Execution fragment $\alpha_6$ for algorithm $X$ exists.
\end{claim}
\begin{proof}
Next base don execution $\alpha_4$ we construction a execution fragment $\alpha_6$ of algorithm $X$ where $\INV{R_1}$ is added before state $\sigma$ in $\prefix{\alpha_0}{ \sigma}$. Note that in this case according to our assumption of $\alpha$ in $\alpha_1$ $R_1$ returns 
$(v_1^0, v_2^0)$. Also, by indistinguishability,  at $s_i$ it responds with $v_1^1$ to $r_2$ so by S property $R_2$ responds with $(v_1^1, v_2^1)$.
\end{proof}

\begin{claim}\label{claim:6} {\bf [Construction of $\alpha_7$]}
Execution fragment $\alpha_7$ for algorithm $X$ exists.
\end{claim}
\begin{proof}
Now starting with execution fragment $\alpha_6$ we inductively argue as in the case of construction of fragments $\alpha_4$ and $\alpha_6$ using  indistinguishability argument and S property create an execution fragment $\alpha_7$ where the actions 
$\INV{R_2}$, $\recv{m^{R_2}_2}{r_2, s_2}$ and $\RESP{R_2}$
  appears before $\INV{R_1}$ and yet $R_2$ returns  $(v_1^1, v_2^1)$ and $R_1$ responds with $(v_1^0, v_2^0)$.
\end{proof}
}
\setcounter{algorithm}{3}

\section{Condition for proving strict serializability}\label{sc_condition}
In this section, we derive a useful property for  executions of  algorithms that implement  objects of data type $\mathcal{O}_T$  that will later  help us  show the \emph{strict serializability} property (S property) of algorithms presented in later sections.  

Although the strict serializability property in transaction-processing systems is a well-studied topic,  
the specific setting considered  in this paper is much simpler. Therefore, this allows  us to derive
 simpler conditions to prove the safety of these algorithms.  A wide range of transaction types and 
 transaction processing systems are considered in the literature. For example, in ~\cite{Papadimitriou79}, Papadimitriou   
defined the strict serializability conditions as a part of developing a  theory for analyzing transaction 
processing systems. In this work, each transaction $T$ consists of a set of write operations $W$, at 
individual objects, and a set of read operations $R$  from individual objects, where  the operations in 
$W$  must complete before the operations in $R$ execute.  
Other types of transaction processing systems allow nested transactions~\cite{Liskov1988, Lynch1994, 
Gary1993}, where the transactions may contain sub-transactions~\cite{Bernstein:1987} which may 
further contain a mix of read or write operations, or even child-transactions. 
In most transaction processing systems considered in the literature,  transactions can be 
\emph{aborted} so as  to handle  failed  transactions. As a result, the serializability theories are 
developed  while  considering the presence of  aborts. 
However, in our system, we do not consider any abort, nor any  client or  server failures.  A transaction 
in our system is either a set of independent writes or a set of reads (see Section~\ref{datatype}) with 
all the reads or writes in a transaction operating on different  objects. Such simplifications allow us to 
formulate an equivalent condition for the execution of an algorithm  to prove the S  
property of such algorithms while  implementing an object of data type $\mathcal{O}_T$.

\sloppy We note that an execution of a variable of type $\mathcal{O}_T$ is a finite sequence 
$\mathbf{v}_0, INV_1, RESP_1,$ $\mathbf{v}_1, INV_2,$ $ RESP_2, \mathbf{v}_2, \cdots, \mathbf{v}_r$ or an infinite sequence 
$\mathbf{v}_0, INV_1, RESP_1, \mathbf{v}_1, INV_2, RESP_2, \mathbf{v}_2, \ldots$, where $INV$'s and 
$RESP$'s are invocations and 
responses, respectively. The $\mathbf{v}_i$s are tuples  of the the form $(v_{1}, v_{2}, \cdots, v_{k}) \in \Pi_{i=1}^{q} V_{i}$, that 
corresponds to the latest values stored across the objects $o_1, o_2\cdots o_k$, and the values in  $\mathbf{v}_0$ are  the initial 
values of the objects. Any adjacent quadruple such as  $\mathbf{v}_i, INV_{i+1}, RESP_{i+1},$ $\mathbf{v}_{i+1}$  is consistent with the $f$ 
function for an object of type $\mathcal{O}_T$ (see  Section~\ref{sc_condition}) . Now, the safety property of such an 
object is a trace that describes the 
correct response to a sequence of $INV$s when all the transactions are executed sequentially. The \emph{strict serializability} of 
$\mathcal{O}_T$ says that each trace produced by an execution of $\mathcal{O}_T$ with concurrent transactions appears as some trace of $\mathcal{O}_T$. We describe this below in more detail. 

\begin{definition}[Strict-serializability] Let us consider an execution $\beta$ of an object of type $\mathcal{O}_T$, such that the invocations of any transaction at any 
client respects the well-formedness property.  Let $\Pi$ denote the set of complete transactions in $\beta$ then we say $\beta$ satisfies the strict-serializability property for 
$\mathcal{O}_T$ if the following are possible:
\begin{enumerate}
\item[$(i)$] For every complete {\sc read} or {\sc write} transaction $\pi$ we insert a point (serialization point) $\pi_*$ between the actions   $\INV{\pi}$ and $\RESP{\pi}$.
\item[$(ii)$] We select a set $\Phi$ of incomplete transactions in $\beta$ such that for 
each $\pi \in \Phi$ we   select a response $\RESP{\pi}$.
\item[ $(iii)$] For each $\pi \in \Phi$ we insert $\pi_*$ somewhere after $\INV{\pi}$ in $\beta$, and remove the $INV$ for the rest of the incomplete transactions in $\beta$.
\item[$(iv)$] If we assume for each $\pi \in \Pi \cup \Phi$ both $\INV{\pi}$ and $\RESP{\pi}$ to occur consecutively at $\pi_*$, with the interval of the transaction shrunk to $\pi_*$,   then the sequence of transactions in this  new trace  is a trace of an object of data type  $\mathcal{O}_T$.
\end{enumerate}
\end{definition}
Now, we consider any automaton $\mathcal{B}$ that implements an object of  type $\mathcal{O}_T$, and prove a result that serves us an  equivalent condition for proving  the strict serializability property of $\mathcal{B}$. Any trace property $P$ of an automaton  is a \emph{safety property}  if the set of executions in $P$ is non-empty; \emph{prefix-closed}, meaning any prefix of an execution in $P$ is also in $P$; and \emph{limit-closed}, i.e., if $\beta_1$, $\beta_2, \cdots$ is any infinite sequence of executions in $P$ is such that $\beta_i$ is prefix of $\beta_{i+1}$ for any $i$, then the limit $\beta$ of the sequence of executions $\{\beta_i\}_{i=0}^{\infty}$  is also in $P$. From Theorem~13.1 in~\cite{Lynch1996}, we know that the trace property, which we denote by $P_{SC}$, of 
any well-formed execution of $\mathcal{B}$ that satisfies the strict-serializability property is a safety property. Moreover, from 
Lemma 13.10 in~\cite{Lynch1996} we can deduce that  if  every execution of $\mathcal{B}$ that is well-formed and failure-free, and also contains no incomplete transactions,  satisfies $P_{SC}$, then any well-formed  execution of $\mathcal{B}$ that can possibly have incomplete transactions is also in $P_{SC}$. 
Therefore, in the following lemma,  which gives us an equivalent condition for the strict serializability property of an execution $\beta$, we consider only executions without any incomplete transactions.
The lemma is proved in a manner similar to Lemma 13.16 in~\cite{Lynch1996}, for atomicity guarantee of a single multi-reader multi-writer object.


\begin{lemma}\label{lem:equivalence}
Let $\beta$ be an execution (finite or infinite) of  an  automaton $\mathcal{B}$ that implements an object of type $\mathcal{O}_T$, which consists of  a set of $k$ sub-objects.
 Suppose all clients in $\beta$ behave in an well-formed
manner. Suppose $\beta$ contains no incomplete transactions and let  $\Pi$ be the set of transactions in $\beta$. Suppose there exists an irreflexive partial ordering ($\prec$)  among  the transactions
 in $\Pi$, such that,
 \begin{enumerate}
  \item [$P1$] For any transaction $\pi \in \Pi$ there are only a finite number of transactions $\phi \in \Pi$ such that 
    $\phi \prec \pi$;
 \item [$P2$] If the response event for $\pi$ precedes the invocation event for $\phi$ in $\beta$, then it cannot be that $\phi \prec \pi$;
 \item [$P3$]If $\pi$ is a {\sc write} transaction  in $\pi$ and $\phi$ is any transaction in $\Pi$, then either $\pi \prec \phi$ or $\phi \prec \pi$; and 
 \item [$P4$] \sloppy A tuple 
 $ \mathbf{v} \equiv $$(v_{i_1}, v_{i_2}, \cdots, v_{i_q})$  
returned by a
$READ(o_{i_1}, o_{i_2}, \cdots, o_{i_q})$,  where $q$ is any positive integer, $1 \leq q \leq k$, 
 is such that  $v_{i_j}$  $j \in \{1, \cdots, q\}$ is written in $\beta$ by the last preceding (w.r.t. $\prec$)  {\sc write} transaction that contains a $\writeop{o_{i_j}}{*}$,
 or the initial value $v_{i_j}^0$ if no such {\sc write} exists in $\beta$. 
 \end{enumerate}
Then execution $\beta$ is strictly serializable.
\end{lemma}

\begin{proof}We discuss how to insert a serialization point $*_{\pi}$ in $\beta$ for every transaction $\pi \in \Pi$. 
First, we add  $*_{\pi}$ immediately after the latest of the invocations of $\pi$ or $\phi \in \Pi$ such that $\phi \prec \pi$.
Note that according to condition $P1$ for $\pi$ there are only finite number of such  invocations in
 $\beta$, therefore, $\pi_*$ is well-defined. Now, since the order of the invocation events of the 
transactions in $\Pi$ are already defined the order of the corresponding set of serialization points are 
well-defined except for the case when more than one serialization points are placed immediately after an 
invocation.
 In the case such multiple  serialization points corresponding to an invocation we order order these 
serialization points  in accordance with the $\prec$  relation of  the underlying transactions.

Next, we show that for any pair of transactions $\phi$, $\pi \in \Pi$ if $\phi \prec \pi$ then $*_{\phi}$ precedes $*_{\pi}$.
Suppose $\phi \prec \pi$. By construction,  each of $\pi_*$ and $\phi_*$ appear immediately after 
some invocation of some transaction in $\Pi$. If both $\pi_*$ and $\phi_*$ appear immediately  after 
the same invocation, then since $\phi \prec \pi$,  by construction of $\pi_*$, $\pi_*$ is ordered after 
$\phi_*$.  Also, if the invocations after which $\pi_*$ and $\phi_*$ appear are distinct,  then by 
construction of $\pi_*$, $\pi_*$ appear after $\phi_*$ since $\phi \prec \pi$.



Next we argue that each $*_{\pi}$  serialization point  for any $\pi \in \Pi$ is placed between the 
invocation $\INV{\pi}$ and responses $\RESP{\pi}$. By construction, $*_{\pi}$ is after $\INV{\pi}$. To 
show that $*_{\pi}$ is before $\RESP{\pi}$ for the sake   of contradiction assume that  $*_{\pi}$  
appears after $\RESP{\pi}$. By construction, $*_{\pi}$ must be after $\INV{\phi}$ for some 
$\phi \in \Pi$ and $\phi \neq \pi$, they by the condition of construction of $\pi_*$ we have $\phi \prec 
\pi$. But from above 
$\INV{\phi}$ occurs after $\RESP{\pi}$, i.e., $\pi$ completes before $\phi$ in invoked which means, by 
property $P2$,  we cannot have $\phi \prec \pi$, a contradiction.

Next, we show that 
if we were to shrink  the transactions intervals to  their corresponding serialization points, the 
 resulting  trace would be a trace of the underlying data type $\mathcal{O}_T$. 
In other words, we show any {\sc read}
$READ(o_{i_1}, o_{i_2}, \cdots, o_{i_q})$
returns the  values   $(v_{i_1}, v_{i_2}, \cdots, v_{i_q})$, such that each value
$v_{i_j}$, $j \in [q]$,  was written by the immediately preceding  (w.r.t. the serialization points)  {\sc 
write} that contained  $\writeop{o_{i_j}}{v_{i_j}}$ or the initial values if no such previous {\sc write} exists.
Let us denote the set of {\sc write}s that precedes (w.r.t. $\prec$) $\pi$ by $\Pi_W^{\prec\pi}$, i.e., 
$\phi \in \Pi^{\prec\pi}_W$  $\phi$ is a write and $\phi \prec \pi$.  By property $P3$, all transactions in 
$\Pi_{W}^{\prec\pi}$ are totally-ordered.  By property $P4$,  $v_{i_j}$ must be the value updated by
 the most recent {\sc write} in $\Pi_W^{\prec\pi}$.  Since the total order of serialization points are  consistent with 
 $\prec$ and hence the $v_{i_j}$ corresponds to the write operation of a {\sc write} transaction with 
  the most recent serialization point and  contains a operation of  type $\writeop{o_{i_j}}{*}$.
\end{proof}

\section{SNOW on MWSR with client-to-client messages} \label{mwsr}
In this section,  we present  algorithm  $A$ for  transaction processing  in the   \emph{multiple-writers single-reader} 
(MWSR) setting, and prove that any fair and well-formed execution  of $A$ satisfies  the SNOW properties.  
In practice, a system with a single reader may not be very useful but this algorithm serves as counter example algorithm to exhibit the point that if client-to-client communication is allowed it is still possible to implement the SNOW properties.
Algorithm $A$ 
shows that if client-to-client messaging is allowed, it is possible to have algorithms for transaction 
processing with two clients that satisfies the SNOW properties. 
We consider a system where there are $\ell \geq 1$ writers with ids $w_1, 
w_2 \cdots w_{\ell}$ (we denoted this set by $\mathcal{W}$), one reader with id $r$, and  $k \geq 1$ servers with ids $s_1, s_2\cdots s_k$ (denote as $\mathcal{S}$) that maintains the  objects $o_1, \cdots, o_k$, respectively. We assume writers can send 
messages to the reader, and the reader can respond back to the writers,  i.e., we allow client-to-client 
messages. Note that for a two-client system, when both  clients are of the same type, i.e., two writers or two reads, the SNOW properties are trivially satisfied.


The steps of algorithm $A$ are presented in Fig.\ref{fig:algo_a}. We assume that each of the processes are run in a single-threaded manner, and therefore, each of the servers or the clients executes the algorithmic steps sequentially. 	
For uniquely identifying a {\sc write} transaction  we use 
keys in algorithm $A$.  A key $\kappa$ is defined as a pair $(z, w)$, 
where $z \in \mathbb{N}$ and $w \in \mathcal{W}$ the  id of a writer. We use $\mathcal{K}$ to denote the set of all possible keys. Also, with each transaction we associate a tag $t \in \mathbb{N}$, which will help us define an order among the transactions. 
	

\emph{State Variables:} The state variables in  writer, reader and  server processes are as follows. 
$(i)$ Any  \emph{writer $w$} has  a counter $z$ to keep track of the
 number of {\sc write} transactions  it  has  invoked so far, initially $0$.
$(ii)$ The  \emph{reader} $r$ has an 
 ordered list  $List$  of elements  as $(\kappa, (b_1, \cdots, b_k))$,  where 
 $\kappa  \in \mathcal{K}$  and 
 $(b_1, \cdots b_k) \in  \{0, 1\}^k$. Initially,  
 $List= [ ({\kappa}^0, (1, \cdots 1) ]$, where ${\kappa}^0  \equiv (0, w_0)$, 
 where $w_0$ is any
  place holder identifier string for writer id. The $List$ can be though of as an array, with  $0$ as the starting index.
   $(iii)$ Each   \emph{server} $s_i \in \mathcal{S}$ there is  a set variable $Vals$ 
 with elements 
 that are  key-value pairs $({\kappa}, v_i) \in \mathcal{K} \times \mathcal{V}_i$. Initially,
  $Vals= \{ ({\kappa}^0, v_i^0)\}$. 
		
			
			\emph{ Writer steps:} 
The procedure  $\Writetr{ (o_{i_1}, v_{i_1}), (o_{i_2}, v_{i_2}), \cdots, (o_{i_p}, v_{i_p}) }$, 
for a {\sc write} transaction,
can be  invoked at any writer $w$, where  $I = \{i_1, i_2, \cdots, i_p\}$ is  any subset of $p$ indices of $[k]$. We define the set  $S_I\triangleq \{s_{i_1}, s_{i_2}, \cdots, s_{i_p}\}$.      
This procedure consists of two consecutive phases: {{\it write-value}} and {{\it inform-reader}}.  In the {{\it write-value}} phase,  $w$ creates a key ${\kappa}$ as  $ {\kappa}  \equiv (z + 1, w)$; and also increments the local counter $z$ by one.   Then it sends $(${{\sc write-value}}$, ({\kappa}, v_{i}))$ to each server $s_i$ in $S_I$, and awaits {{\sc acknowledge}}s  
from each server  in $S_I$.  After receiving {{\sc acknowledge}}s from each server in  $S_I$,    $w$ initiates the {{\it inform-reader}} phase during which  it sends 
({\sc inform-reader}, $({\kappa}, (b_{1}, \cdots b_{k})$) to $r$, where for any $i \in [k]$, $b_i$ is a boolean variable, such that $b_i=1$ if $s_i \in S_I$, otherwise $b_i=0$. 
   Essentially, such a $(k+1)$-tuple
   identifies the set of objects that are updated during that {\sc write} transaction, i.e., if $b_i=1$ then object 
   $o_i$ was updated 
during the execution of the  {\sc write} transaction, otherwise $b_i=0$.  
After $w$ receives    {{\sc acknowledge}} 
from $r$ it completes the {\sc write}. 

\emph{ Reader steps:}  
Note that we use the same notations for $I$ and $S_I$ as above for the set of indices and corresponding servers, possibly 
 different across transactions.
The procedure  \Readtr{$ o_{i_1},  o_{i_2}, \cdots, o_{i_p}$}, 
for any  {\sc read} transaction, 
is  initiated at  reader  $r$, where   $o_{i_1},  o_{i_2}, \cdots, o_{i_p}$  denotes the  subset  of  
objects $r$ 
intends to read. This procedure
consists of only one phase,  {{\it read-value}},  of communication 
between the reader and the servers in $S_I$.   Here $r$ sends  the message
({\sc read-value}, ${\kappa}_i$) to each server $s_i \in S_I$, where 
 the ${\kappa}_i$ is the key in  the tuple $({\kappa}_{i}, (b_{1}, \cdots, b_{k}))$  in  $List$ located at  index $j^*$ such that $b_i =1$ such that 
$i \in I$.
 After
 receiving the values $v_{i_1}$, $v_{i_2}, \cdots v_{i_p}$ from all  servers in $\mathcal{S_I}$,  where $S_I \triangleq \{s_{i_1},  s_{i_2}, \cdots, s_{i_p}\}$, the transaction completes by 
 returning $(v_{i_1}, \cdots v_{i_p})$.

Next,  if  reader $r$ receives a message  
({\sc inform-reader}, $({\kappa}, (b_{1}, \cdots, b_{k})$) from any writer $w$, then $r$ appends  
			 $({\kappa}, (b_{1}, \cdots, b_{k})$ to its  $List$,  and responds to $w$ with  
			 {{\sc acknowledge}} and $t_w = |List|$, i.e., number of elements in list $List$.
			 The order of the  elements in  $List$ corresponds to  the order  
the {\sc write} transactions, the order of the incoming  {{\sc inform-reader}} updates,  as seen by the reader.


\emph{Server steps:} The server protocol consists of two procedures corresponding to the messages containing the tags 
{{\sc write-value}} and {\sc read-value}.  The first procedure is used if a server $s_i$ receives a 
message  $(${{\sc write-value}}$, ({\kappa}, v_{i}))$  from a writer $w$,  it  adds $({\kappa}, v_i)$ to its set variable   $Vals$ and sends {{\sc acknowledge}} back to $w$.
The second procedure is used  if  $s_i$ receives a message such as  $(${{\sc read-value}}$, {\kappa}_{i})$ from $r$ then it responds back  with $v_i$ such that the pair $({\kappa}_{i}, v_i)$ is in its variable $Vals$.

\remove{
 and set the tag $t_r$ as  the latest index in $List$ corresponding to a {\sc write} that updated  one of the object in the {\sc read}, i.e., $\max_{1 \leq j \leq |List|} \{ j : List[j].b_i = 1 \wedge i \in I\}$.

 
During this phase, each of the contacted servers responds with one version of the object value to the reader. 
During  phase {{\it read-value}}, 	 the reader sends to each of the servers in 
$\mathcal{S}$, say $s_i$ the key ${\kappa}^{s_i}$ corresponding 
			 to $(k+1)$-tuple of $List$ with the latest  index $j^*$ such that $b_i =1$ such that 
$i \in I$, where $I \triangleq  \{{i_1},  {i_2}, \cdots, {i_p}\}$,  requesting the corresponding value.  Any server $s_i$ upon receiving 
such a message with $(${{\sc read-value}}$, {\kappa}^{s_i})$ responds with $v$ such that $({\kappa}^{s_i}, v_i)$ is in its variable $Vals$. After
 receiving the values $v_{i_1}$, $v_{i_2}, \cdots v_{i_p}$ from all  servers in $\mathcal{S_I}$,  where $S_I \triangleq \{s_{i_1},  s_{i_2}, \cdots, s_{i_p}\}$, the transaction completes by 
 returning $(v_{i_1}, \cdots v_{i_p})$, and set the tag $t_r$ as  the latest index in $List$ corresponding to a {\sc write} that updated  one of the object in the {\sc read}, i.e., $\max_{1 \leq j \leq |List|} \{ j : List[j].b_i = 1 \wedge i \in I\}$.


We define  $S_I\triangleq \{s_{i_1}, s_{i_2}, \cdots, s_{i_p}\}$.      

Then it sends $(${{\sc write-value}}$, ({\kappa}, v_{i}))$ to each server $s_i$ in $S_I$, and awaits {{\sc acknowledge}}  
from all  in $S_I$. Any server $s_i$, upon receiving such a message, adds $({\kappa}, v_i)$ to its set variable  
$Vals$ and sends {{\sc acknowledge}} back to $w$.

A {\sc write} transaction  $\Writetr{ (o_{i_1}, v_{i_1}),
(o_{i_2}, v_{i_2}), \cdots, (o_{i_p}, v_{i_p}) }$, initiated by writer $w$, where $I = \{i_1, i_2, \cdots, i_p\}$ is the set of indices of the $p$ objects to update,   consists of two phases: {{\it write-value}} and {{\it inform-reader}}.   We define  $S_I\triangleq \{s_{i_1}, s_{i_2}, \cdots, s_{i_p}\}$.   During the {{\it write-value}} phase,  $w$ creates a key ${\kappa}$ as 
 $ {\kappa}  \equiv (z + 1, w)$; and also increments the local counter $z$ by one.   
Then it sends $(${{\sc write-value}}$, ({\kappa}, v_{i}))$ to each server $s_i$ in $S_I$, and awaits {{\sc acknowledge}}  
from all  in $S_I$. Any server $s_i$, upon receiving such a message, adds $({\kappa}, v_i)$ to its set variable  
$Vals$ and sends {{\sc acknowledge}} back to $w$.

 After receiving {{\sc acknowledge}} from all servers in $S_I$ the writer  $w$
initiates the {{\it inform-reader}} phase where it sends 
({\sc inform-reader}, $({\kappa}, (b_{1}, \cdots b_{k})$) to $r$, where for any $i \in [k]$, $b_i$ is a boolean variable, such that $b_i=1$ if $s_i \in S_I$, otherwise $b_i=0$,   to the reader $r$ and awaits  acknowledgements  with {{\sc acknowledge}} and tag $t_w$ from $r$. 
		    Essentially, a $(k+1)$-tuple corresponds to a {\sc write} transaction and 
   identifies the set of objects that are updated during that {\sc write} transaction, i.e., if $b_i=1$ then object 
   $o_i$ was updated 
during the execution of the  {\sc write} transaction, otherwise $b_i=0$.  


 At $r$, upon receiving  
({\sc inform-reader}, $({\kappa}, (b_{1}, \cdots, b_{k})$) from any writer, the reader appends  
			 $({\kappa}, (b_{1}, \cdots, b_{k})$ to its  $List$,  and responds with  
			 {{\sc acknowledge}} and $t_w$ (set to be the number of elements in the local list $List$)  to $w$.
			 The order of the  elements in  $List$ corresponds to  the order  
the {\sc write} transactions, the order of the incoming  {{\sc inform-reader}} updates,  as seen by the reader.
			  After receiving an acknowledgement and tag $t_w$ from $r$,  $w$ completes the {\sc write} transaction.

\emph{ {\sc read} Transaction.}  A {\sc read} transaction  \Readtr{$ o_{i_1},  o_{i_2}, \cdots, o_{i_p}$} 
initiated by  reader  $r$, intending to read the object values from any 
subset $o_{i_1},  o_{i_2}, \cdots, o_{i_p}$ of the objects, 
consists of only one phase of communication 
between the reader and the relevant servers, i.e., during phase {{\it read-value}}. 
During this phase, each of the contacted servers responds with one version of the object value to the reader. 
During  phase {{\it read-value}}, 	 the reader sends to each of the servers in 
$\mathcal{S}$, say $s_i$ the key ${\kappa}^{s_i}$ corresponding 
			 to $(k+1)$-tuple of $List$ with the latest  index $j^*$ such that $b_i =1$ such that 
$i \in I$, where $I \triangleq  \{{i_1},  {i_2}, \cdots, {i_p}\}$,  requesting the corresponding value.  Any server $s_i$ upon receiving 
such a message with $(${{\sc read-value}}$, {\kappa}^{s_i})$ responds with $v$ such that $({\kappa}^{s_i}, v_i)$ is in its variable $Vals$. After
 receiving the values $v_{i_1}$, $v_{i_2}, \cdots v_{i_p}$ from all  servers in $\mathcal{S_I}$,  where $S_I \triangleq \{s_{i_1},  s_{i_2}, \cdots, s_{i_p}\}$, the transaction completes by 
 returning $(v_{i_1}, \cdots v_{i_p})$, and set the tag $t_r$ as  the latest index in $List$ corresponding to a {\sc write} that updated  one of the object in the {\sc read}, i.e., $\max_{1 \leq j \leq |List|} \{ j : List[j].b_i = 1 \wedge i \in I\}$.
	
	At the server, 
}
	\algremove{		
\begin{algorithm}[!ht]
	\begin{algorithmic}[2]
		\begin{multicols}{2}{\footnotesize
	
					 					\Statex {\bf At writer $w$}
		\Part{{\it State Variables at $w$}}{ 	
					\Statex $z \in \mathbb N$, initially   $0$
						}\EndPart
		\Statex\Statex
		{\bf  \Writetr{$(o_{i_1}, v_{i_1}), (o_{i_2}, v_{i_2}), \cdots, (o_{o_p},  v_{i_p})$}}
				\Part{ \underline{{\it write-value}}} {
				        \State ${\kappa} \leftarrow (z +1,  w)$; $z \leftarrow z +1 $
					\State $I\triangleq \{i_1, i_2, \cdots, i_p \}$
				
				         \For{$i \in I$} 
						\State Send {\sc write-value}, $({\kappa}, v_{s_i})$ to  $s_i$
					 \EndFor 
					\State  Await {{\sc acknowledge}}  from  $s_i$ for every $i \in I$.
				}\EndPart
				\Statex
			      \Part{ \underline{{\it inform-reader}}} {
                                      \For{$i \in [k]$} 
						\If{$i \in I$}
						 \State $b_i \leftarrow 1$
						 \Else
						   \State $b_i \leftarrow 0$
						\EndIf
					 \EndFor 
		
                                            \State  Send  ({\sc inform-reader}, $({\kappa}, (b_{1}, \cdots, b_{k}))$) to   $r$
					\State  Receive ({{\sc acknowledge}}, $t_w$) from  $r$
				}\EndPart
			}\end{multicols}





	


	
	\vspace{-1.0em} \\\hrulefill 	\vspace{-1.0em}
			\begin{multicols}{2}{\footnotesize	
					 					\Statex {\bf At reader $r$}
					 			\Part{{\it State Variables at $r$}}{ 	
					\Statex $List$, a list  of elements in  $\mathcal{K} \times \{ 0, 1 \}^k $,\\ ~~~~~initially  $[({\kappa}^0, 1, \cdots 1)]$
						}\EndPart
					
					\Statex
					\Statex  {\bf \Readtr{$ o_{i_1},  o_{i_2}, \cdots, o_{i_p}$}}	
					\Part{{\underline{{{\it read-value}}}}}{ 
					 
					 	\State $I\triangleq \{i_1, i_2, \cdots, i_p \}$
					 
				             \For{$i \in I$} 
				             \State $j^* \leftarrow \max_{1 \leq j \leq |List|} \{ j : List[j].b_i = 1\}$
				             \State ${\kappa}_i = List[j^*].{\kappa}$
						\State  Send ({\sc read-value}, ${\kappa}_i$) to $s_i$
					 \EndFor 
					\State  Await responses  $v_{i}$ from  $s_i$ for  each $i\in I$
					  \Statex /* $t_r \triangleq \max_{1 \leq j \leq |List|} \{ j : List[j].b_i = 1 \wedge i \in I\}$ */
					\State Return  $(v_{i_1}, v_{i_2}, \cdots, v_{i_p})$
					}\EndPart
			
					  \\\hrulefill
					  \Statex
					  \Statex {\bf Response routines}
					\Part{{\underline{On recv  ({\sc inform-reader}, $({\kappa}, (b_{1}, \cdots b_{k}))$) from  $w$}}}{ 
					         \Statex
					         \State $List  \leftarrow List \bigoplus~ ({\kappa}, (b_{1}, \cdots b_{k}))$ 
					         //$\bigoplus$ for append
					         \State $tag \leftarrow |List|$ // $| \cdot |$ size of the list
						\State Send  ({{\sc acknowledge}}, $tag$) to  $w$
					}\EndPart
				
				}\end{multicols}

	\vspace{-1.0em}
	         \\\hrulefill 	\vspace{-1.0em}
			\begin{multicols}{2}{\footnotesize
					\Statex {\bf At server $s_i$ for any $i \in [k]$}
						\Part{{\it State Variables}}{ 
							
							\Statex $Vals\subset \mathcal{K} \times \mathcal{V}_i$, initially   $\{(t^0_{key}, v_i^0)\}$
						
						
						}\EndPart
						\Statex

						\Part {\underline{On recv ({\sc write-value}, $({\kappa}, v)$) 
						from writer $w$}} {
						           \State   $Vals \gets   Vals \cup \{({\kappa}, v)\}$ 
							\Statex  Send {{\sc acknowledge}} to writer $w$.
						}\EndPart
						\Statex
						\Part{ \underline{On recv ({\sc read-value}, ${\kappa}$) from reader $r$ }} {
							\State   Send $v$ s.t. $({\kappa}, v) \in Vals$  to reader $r$
						}\EndPart	
					}\end{multicols}
				\end{algorithmic}	
				\caption{The protocol for a writer $w$, reader $r$ and server $s_i$ for  algorithm $A$.}\label{fig:algo_a}
			\end{algorithm}	
}

The following result states that algorithm $A$ respects SNOW properties.
Note that the liveness property of {\sc read} and {\sc write}  transactions are a part of the SNOW properties.
Consider any failure-free execution of algorithm $A$. In the steps for the reader assume the quantity
 $t_r \triangleq \max_{1 \leq j \leq |List|} \{ j : List[j].b_i = 1 \wedge i \in I\}$, which is presented as a comment in the pseudo-code for $A$.
We associate with any transaction $\phi$ a tag
$tag(\phi)$ such that if  $\phi$ is a {\sc write}  $tag(\phi)=t_w$, i.e., the value of $t_w$ before the completion of the operation, and $tag(\phi)=t_r$ when $\phi$ is a {\sc read}.
	
	\remove{
	Let $\beta$ be a well-formed execution of algorithm $A$. Also, let $\Pi$ denote the set of all client transactions that take place during $\beta$. Then every operation $\pi \in \Pi$ associated with a non-faulty client completes.
	In order to prove $S$ property of $C$  for any well-formed execution $\beta$, we define a partial order ($\prec$) in $\Pi$  and then show  that $\prec$  satisfies the properties $P1$, $P2$ and $P3$ given in Lemma \ref{lem:atom}. For every transaction $\pi$ in $\Pi$ corresponding to a non-faulty reader or writer, we associate a $(tag, value)$ pair that we denote as $(tag(\pi), value(\pi)))$. For a {\sc write} transaction $\pi$,  we define the $(tag(\pi), value(\pi)))$ pair as the message $(t_w, v)$ which the writer sends in the {\PutW} phase. If $\pi$ is a read, we define the $(tag(\pi), value(\pi)))$ pair as $(t_{read}, v)$ where $v$ is the value that gets returned in the {{ \it{read-complete}}} phase, and $t_{read}$ is the  associated tag. The partial order ($\prec$) in $\Pi$ is defined as follows: For any $\pi, \phi \in \Pi$, we say $\pi \prec \phi$  if one of the following holds: $(i)$  $tag(\pi)  < tag(\phi)$, or $(ii)$ $tag(\pi) = tag(\phi)$, and  $\pi$ and $\phi$ are write and {\sc read} transactions, respectively. }
					
	\begin{theorem} Any well-formed  and fair execution of algorithm $A$ is an wait-free implementation of  transaction processing in the MWSR setting with for objects of type $\mathcal{O}_T$, consisting of  objects $o_1, o_2, \cdots o_k$ maintained by the  servers $s_1, s_2, \cdots, s_k$, respectively; and it respects the SNOW properties and {\sc write}s transactions are live.
	\end{theorem}
	

	\begin{proof} Below we show that $A$ satisfies the  SNOW properties. 
	
	\noindent{\emph{\underline{S property:}}} 
	Let $\beta$ be any fair execution  of  $A$ and 
 suppose all clients in $\beta$ behave in an well-formed
manner. Suppose $\beta$ contains no incomplete transactions and let  $\Pi$ be the set of transactions in $\beta$.  We define an irreflexive partial ordering ($\prec$) among the transactions in $\Pi$ as follows:  if $\phi$ and $\pi$ are any two distinct transactions in $\Pi$ then we say 
	$\phi \prec \pi$ if either $(i)$ $tag(\phi) < tag(\pi)$ or $(ii)$ $tag(\phi) = tag(\pi)$ and $\phi$ is a {\sc write} and $\pi$ is a {\sc read}. We will prove the $S$  (strict-serializability) property of $A$ by proving that the properties $P1$, $P2$, $P3$ and $P4$ of Lemma~\ref{lem:equivalence} hold for $\beta$. 
	
	\emph{P1:}   If $\pi$ is a {\sc read} then since all {\sc read}s are invoked by a single reader $r$ and in a well-formed manner, 
	therefore, there cannot be an infinite number of {\sc read}s such that they all 
	precede $\pi$ (w.r.t $\prec$).
	 Now, suppose $\pi$ is a {\sc write}. Clearly, from an inspection of the algorithm, 
	 $tag(\pi) \in \mathbb{N}$. From inspection of the algorithm, each {\sc write} increases the size of 
	 $List$, and the value of the tags are  defined by the size of $List$. Therefore, there can be at 
	 most a finite number of {\sc write}s such that can precede $\pi$ (w.r.t. $\prec$) in $\beta$.
	  
	\emph{P2:}  Suppose $\phi$ and $ \pi$ are any two transactions in $\Pi$, such that, $\pi$ begins after $\phi$ completes. Then we show that we cannot have $\pi \prec \phi$. Now, we consider four cases, depending on whether $\phi$ and $\pi$ are {\sc read}s or {\sc write}s.	
	\begin{enumerate}
	    \item [$(a)$] $\phi$ and $\pi$ are {\sc write}s invoked by writers $w_{\phi}$ and $w_{\pi}$, respectively. Since the size of $List$, in $r$,  grows monotonically with each {\sc write}  hence  $w_{\pi}$ receives the  tag at least as high as $tag(\phi)$, so $\pi\not \prec \phi$.
	      %
	       \item [$(b)$] $\phi$ is a {\sc write}, $\pi$ is a {\sc read} transactions invoked by writer $w_{\phi}$ and $r$, respectively.  
	        Since the size of $List$, in $r$,  grows monotonically, and because  $w_{\pi}$ invokes $\pi$ after $\phi$ completes hence  $tag(\pi)$ is at least as high as $tag(\phi)$, so $\pi\not \prec \phi$.
	      %
	        \item[$(c)$] $\phi$ and $\pi$ are {\sc read}s  invoked by reader $r$. 
	           Since the size of $List$, in $r$,  grows monotonically,  hence  $w_{\pi}$ invoked $\pi$ after $\phi$ completes hence $tag(\pi)$ is at least as high as $tag(\phi)$, so $\pi\not \prec \phi$.
	        %
	         \item [$(d)$] $\phi$ is a {\sc read}, $\pi$ is a {\sc write}  invoked by reader $r$ and $w_{\pi}$, respectively.
	         This case is simple because new values are added to $List$  only  by writers, and $tag(\pi)$ is at least as large as the tag of $\phi$ and hence   $\pi\not \prec \phi$. 
	\end{enumerate}
	
	\emph{P3:} This is clear by the fact that any {\sc write} transaction always creates a unique tag and all tags are totally ordered since they all belong to $\mathbb{N}$
	
	\emph{P4:} Consider a {\sc read} $\rho$ as $READ(o_{i_1}, o_{i_2}, \cdots, o_{i_q})$, in $\beta$. 
Let the returned value from $\rho$ be $\mathbf{v} \equiv $$(v_{i_1}, v_{i_2}, \cdots, v_{i_q})$ such that 
$1 \leq {i_1} <  {i_2} <  \cdots <  {i_q} \leq k$, where value  $v_{i_j}$ corresponds to $o_{i_j}$. 
	Suppose $tag(\rho) \in \mathbb{N}$ was created during some {\sc write} transaction, say $\phi$, i.e., $\phi$ is the {\sc write} that 
	added the elements in index $(tag(\rho)-1)$ of $List$. Note that element in index $0$ contains the initial value.

	 Now we consider two cases:
	 
	\emph{Case $tag(\rho) = 1$.} We  know that it corresponds the initial default value $v_i^0$ at each sub-object $o_i$, and this equates to $\rho$ returning the default initial value for each sub-object.
	 %

	 
	 \emph{Case $tag(\rho) > 1$.} Then we argue that there exists no {\sc write} transaction, say $\pi$, that updated object $o_{i_j}$,   in $\beta$, such that,  $\pi \neq \phi$ and $\rho$ returns values written by $\pi$ and $\phi \prec \pi \prec \rho$. Suppose we assume the 	contrary, which means $tag(\phi) < tag(\pi) < tag(\rho)$. The latter implies $tag(\phi)  = tag(\pi)$ which is not possible because 
	this contradicts the fact that for any two distinct {\sc write}s $tag(\phi) \neq tag(\pi)$  in any execution of   $A$.
	
	\noindent{\emph{\underline{N property:}}}  By inspection of algorithm $A$ for the  response steps  of the servers to the reader.
	
	\noindent{\emph{\underline{O property:}}} By inspection of the  {{\it read-value}} phase: it consists of one round of communication between the reader and the servers, where the servers send only one version of the value of the object it maintains.
	
	\noindent{\emph{\underline{W property:}}}  By inspection of the {\sc write} transaction steps, and  and  that writers always get to complete the transactions they invoke.

	\end{proof}


 Note that the above theorem holds in the presence of any writer crashes.


\section{SNoW for MWMR setting}\label{mwmr}
In this section,  we present  algorithm  $B$ for  transaction processing in the   \emph{multiple-writers multi-reader} (MWMR) setting and show that   its execution  satisfies  SNoW  properties, where ``o'' means a {\sc read} may consist of more than one round trip of communications between the reader and the servers. We denote the type of object  that satisfies the SNoW properties by $\tilde{\mathcal{O}}_T$.   
The steps of the algorithm for the writers, readers and the servers  are presented in Fig.\ref{fig:algo_b}.
We assume there is a set of writers $\mathcal{W}$,  a set of readers $\mathcal{R}$ and a set of $k \geq 1$ servers,  $\mathcal{S}$, with ids $s_1, s_2\cdots s_k$ that stores the objects $o_1, o_2, \cdots, o_k$, respectively.  We define  key ${\kappa}$ is defined as a pair $(z, w)$, 
where $z \in \mathbb{N}$ and $w \in \mathcal{W}$ the  id of a writer. We use $\mathcal{K}$ to denote the set of all possible keys. Like in algorithm $A$ from Section~\ref{mwsr}, also in $B$, the keys are used to uniquely identify each transaction. Also, with each transaction we associate a tag $t \in \mathbb{N}$. 

\remove{				
For uniquely identifying a {\sc write} transaction  we use 
keys as in algorithm $A$.  A tag $t$ is defined as a pair $(z, w)$, 
where $z \in \mathbb{N}$ and $w \in \mathcal{W}$  ID of a writer. We use $\mathcal{K}$ to denote the set of all possible keys. Also, with each transaction we associate a tag $t \in \mathbb{N}$. 
			
		
		\emph{State Variables} $(i)$ \emph{server:} A list variable $List$  of $k+1$-tuples as $(t, \tilde{o}_1, \cdots, \tilde{o}_k)$,  where $t  \in \mathcal{T}$  and $\tilde{o}_i \in \{o_i, \bot\}$ and initially,  $List= [ (t^0, o_1, \cdots o_k) ]$; and  a set variable $Vals_s$ with elements 
 that are  tag and value pairs $(t, v_s) \in \mathcal{T} \times V_s$, initially $Vals = \{ (t^0, v_s^0\}$.  Essentially, a $k+1$-tuple corresponds to a write operation and  enumerates the set of objects that are updated during the write if the corresponding $\tilde{o}_{(\cdot)}$ is not $\bot$. The order of the list gives the order the the write operations. $(ii)$ \emph{writer:} a counter $z$ to keep track of the number of write operations the writer invoked, initially $0$.


					\paragraph{{\sc write} transaction} A {\sc write} transaction
					  $T_w \equiv $ $WRITE\{ \writeop{o_{i_1}}{v_{i_1}}, $ $\writeop{o_{i_2}}{v_{i_2}}, $ $\cdots, 
					  $$ \writeop{o_{i_p}}{v_{i_p} }\} $,
					 initiated by some writer $w$  consists of two phases: {{\it write-value}} and {{\it update-coord}}.  It begins with  the {{\it write-value}} phase, where it creates a new tag $t_w$ as $ t_w \equiv ( t_{max}.z + 1, w)$, where $w$ is the identity of the writer; and also increments the local counter $z$ by unity.   Then it sends $(${{\sc write-value}}$, (t_w, v_{s}))$ to each server $s$, and awaits {{\sc acknowledge}}  from all $k$ servers. Any server $s$, upon receiving such a message, adds $(t_w, v_{s})$ to its set variable  $Vals_s$ and sends {{\sc acknowledge}} back to $w$. One of the servers, denote by $s^*$, is designated as the  \emph{serializer}, say $s^*=s_1$ to maintain a unique order of the write operations. After receiving {{\sc acknowledge}} from all servers the writer initiates the {{\it update-coord}} phase where it sends ({\sc update-coord}, $(t_w, \tilde{o}_{1}, \cdots \tilde{o}_{k})$), where for any $i \in [k]$ $\tilde{o}_i=o_i$ if $i \in \{i_1, i_2, \cdots, i_p \}$   to  server $s^*\equiv s_1$ (it could be any of the $k$ servers) and awaits acknowledgements  with tags {{\sc acknowledge}} from it.  At $r$, upon receiving  ({\sc inform-reader}, $(t_w, \tilde{o}_{1}, \cdots \tilde{o}_{k})$) from any writer,  $s^*$ appends   $(t_w, \tilde{o}_{1}, \cdots \tilde{o}_{k})$ to its list $List$  and sends {{\sc acknowledge}} to $w$. After receiving such an acknowledgement  $w$ completes the transaction $T_w$.
			
			
			
	
		
	

			\paragraph{Read Transaction}  The {\sc read} transaction consists of two phases, viz., {{\it get-tag-array}} and  {{\it commit}}. 
During the {{\it get-tag}} phase a reader $r$ sends {{\sc get-tag-array}} messages to the serializer server $s^*$ and awaits responses from it.  Upon receiving such a message from the reader $s^*$ compute, form $List$,  for each of the objects a tag corresponding to the most recent update, or the initial value if no such update exists,  and  sends $(\hat{t}_1, \cdots \hat{t}_k)$ to $r$.  Once $r$ receives the array of tags from $s^*$ it initiates the 
  {{\it read-value}} phase, where it  sends \text{{\sc read-value}}, $t_r$ to each of the servers.  Any server $s$, upon receiving such a message, 
}

\algremove{
\begin{algorithm}[!ht]
	\begin{algorithmic}[2]
	
		\begin{multicols}{2}{\footnotesize
					\Statex  {\bf At writer $w$}
					\Part{{\it State Variables}}{ 	
					\Statex $z \in \mathbb N$, initially   $0$
						}\EndPart
		\Statex  {\bf  \Writetr{$(i_1, v_{i_1}), (i_2, v_{i_2}), \cdots, (i_p,  v_{i_p})$}   }
					\State $I\triangleq \{i_1, i_2, \cdots, i_p \}$
				
				\Part{ \underline{{\it write-value}}} {
				   
				        \State ${\kappa} \leftarrow (z +1,  w)$; $z \leftarrow z +1 $
				         \For{$i \in I$} 
						\State Send {\sc write-value}, $({\kappa}, v_{s_i})$ to server $s_i$
					 \EndFor 
					\State  Await {{\sc acknowledge}} from servers in  $S_I$.
				}\EndPart
				\Statex
			      \Part{ \underline{{\it update-coord}}} {

                                      \For{$i \in [k]$} 
						\If{$i \in I$}
						 \State $b_i \leftarrow 1$
						 \Else
						   \State $b_i \leftarrow 0$
						\EndIf
					 \EndFor 
		
                                            \State  Send  ({\sc update-coord}, $({\kappa}, (b_{1}, \cdots, b_{k}))$) to   $s^*$

	
                     
				
					\State Receive ({{\sc acknowledge}}, $t_w$) from  coordinator $s^*$
				}\EndPart
			}\end{multicols}





	


\vspace{-1.5em}
 \\\hrulefill
\vspace{-1.5em}
			\begin{multicols}{2}{\footnotesize		
					\Statex  {\bf At reader $r$}
					\Statex  {\bf \Readtr{$ o_{i_1},  o_{i_2}, \cdots, o_{i_p}$}}	
					\State $I\triangleq \{i_1, i_2, \cdots, i_p \}$
				
	
	
	
						\Part{ \underline{{\it get-tag-array}}} {
					\State  Send  ({\sc get-tag-array}) to server $s^*$
					\State  Receive response  $(t_r, ({\kappa}_1, {\kappa}_2, \cdots, {\kappa}_k))$ from  $s^*$
				}\EndPart	
						\Statex
					\Part{{\underline{{{\it read-value}}}}}{ 
					 
				             \For{$i \in  I$} 
						\State  Send ({\sc read-value}, ${\kappa}_i$) to $s_i$
					 \EndFor 
						\State  Wait responses as $v_{i}$ for each $s_i\in S$
						\State Return  $(v_{i_1}, v_{i_2}, \cdots, v_{i_p})$
					}\EndPart
				}\end{multicols}
	
	
	
	

		


\vspace{-1.7em}
\\\hrulefill
\vspace{-1.5em}
			\begin{multicols}{2}{\footnotesize
					\Statex {\bf At server $s_i$ for any $i \in [k]$}
						\Part{{\it State Variables}}{ 
							\Statex $Vals\subset \mathcal{K} \times \mathcal{V}_i$, initially   $\{({\kappa}^0, v_i^0)\}$
						
						
						
					
\Statex $List$, a list  of  $\mathcal{K} \times \{ 0, 1 \}^k $, initially  $[({\kappa}^0, (1, \cdots 1))]$
						}\EndPart
						\Statex
						\Part {\underline{On recv ({\sc write-value}, $({\kappa}, v)$) from  $w$}} {
						           \State   $Vals \gets   Vals \cup \{({\kappa}, v)\}$ 
							\State  Send {{\sc acknowledge}} to writer $w$.
						}\EndPart
						\Statex
						\Part{{\underline{On recv  ({\sc update-coord}, $({\kappa}, (b_{1}, \cdots b_{k}))$) from  $w$}}}{ 
					     
                                 \State $List  \leftarrow List \bigoplus~ ({\kappa}, (b_{1}, \cdots b_{k}))$ 
					         //$\bigoplus$ for append
				
					        \State $tag \leftarrow |List|$ // $| \cdot |$ size of the list
						\State Send  ({{\sc acknowledge}}, $tag$) to  $w$
					}\EndPart
				           
					              \Statex
						\Part{ \underline{On recv ({\sc read-value}, ${\kappa}$) from  $r$ }} {
							\State   Send $v_i$ s.t. $({\kappa}, v) \in Vals$  to  $r$
						}\EndPart	
					\Statex\Statex   /* used only by $s^*$ */
					
					\Part{ \underline{On recv {{\sc get-tag-array}} from  $r$ }} {
					\For{$i \in [k]$} 
				             \State $j^* \leftarrow \max \{ j : List[j].b_i =1 \}$
				             \State ${\kappa}_i = List[j^*].{\kappa}$
					
					 \EndFor 
					   \State  $t_r \triangleq \max_{1 \leq j \leq |List|} \{ j : List[j].b_i = 1 \wedge i \in I\}$ 
						\State  Send  ($t_r, ({\kappa}_1,{\kappa}_2, \cdots, {\kappa}_k)$) to $r$
						}\EndPart				
					}\end{multicols}
				\end{algorithmic}	
				\caption{The protocol for any  writer $w$, reader $r$ or server $s_i$ for  algorithm $B$.}\label{fig:algo_b}
			\end{algorithm}	

}
In algorithm $B$, we designate one of the servers as the coordinator, we denote as $s^*$,
 for the transactions. Essentially, the coordinator $s^*$ is used to maintain the order of the {\sc write}s and the objects that are updated during the {\sc write} in the variable $List$.  Note that in a system, where there are many objects 
different objects may be use different servers  as coordinators based on some load-balancing rule. 

\emph{State Variables:} Each of the writers and servers maintain a set of state variables as follows: $(i)$ At  any  \emph{writer $w$}, there is  a counter $z$ to keep track of the
 number of {\sc write} transaction  the writer has  invoked, initially $0$. $(ii)$ At any  \emph{server}, $s_i$, 
 for $i \in [k]$, there is  a set variable $Vals$ 
 with elements 
 that are  key-value pairs $({\kappa}, v_i) \in \mathcal{K} \times \mathcal{V}_i$. Initially,
  $Vals= \{ ({\kappa}^0, v_i^0)\}$.
A server also contains an
 ordered list variable $List$  of elements  as $({\kappa}, (b_1, \cdots, b_k))$,  where 
 ${\kappa}  \in \mathcal{K}$  and 
 $(b_1, \cdots b_k) \in  \{0, 1\}^k$. Initially,  
 $List= [ ({\kappa}^0, (1, \cdots 1) ]$, where ${\kappa}^0  \equiv (0, w_0)$, 
 where $w_0$ is any
  place holder identifier string for writer id. The elements in $List$ can be identified with an index, e.g., 
  $List[0] =({\kappa}^0, (1, \cdots, 1))$.  Essentially, a $(k+1)$-tuple  $(\kappa, (b_1, \cdots, b_k))$ in $List$ corresponds to a {\sc write} transaction and 
   identifies the set of objects that are updated during the {\sc write} transaction, i.e., if $b_i=1$ then object 
   $o_i$ was updated  during the execution of the  {\sc write} transaction, otherwise $b_i=0$.
		
			
			
			\emph{Writer steps:} A {\sc write} transaction that is meant to update
			a  list of $p$ objects $o_{i_1}, o_{i_2}, \cdots o_{i_p}$  with values
			 $v_{i_1}, v_{i_2}, \cdots v_{i_p}$, respectively, is invoked at $w$ via the procedure
			$\Writetr{ (o_{i_1}, v_{i_1}), (o_{i_2}, v_{i_2}), \cdots, (o_{i_p}, v_{i_p}) }$.
We use the notations:  $I \triangleq \{i_1, i_2, \cdots, i_p\}$  and $S_I\triangleq \{s_{i_1}, s_{i_2}, \cdots, s_{i_p}\}$.
This procedure  consists of two phases: {{\it write-value}} and {{\it update-coord}}. 
During the {{\it write-value}} phase,  $w$ creates a new key ${\kappa}$ as 
 $ {\kappa}  \equiv (z + 1, w)$, where $w$ is the identity of the writer; and also increments the local counter $z$ by one.  Then $w$ sends $(${{\sc write-value}}$, ({\kappa}, v_{i}))$ to each server in $S_I$, and awaits {{\sc acknowledge}}  
from all servers in $S_I$.
After receiving {{\sc acknowledge}} from all servers in $S_I$,  $w$
initiates the {{\it update-coord}} phase where it sends 
({\sc  update-coord}, $({\kappa}, (b_{1}, \cdots b_{k})$) to $s^*$, where for any $i \in [k]$,  $b_i=1$ if $s_i \in S_I$, 
otherwise $b_i=0$,   and completes the procedure after it receive a   {{\sc acknowledge}} message from $s^*$.  
	  After receiving message as ({{\sc acknowledge}}, $t_w$),  $w$ completes the {\sc write}.


\emph{Reader steps:}  
Note that we use the same notations for $I$ and $S_I$ as above by the set of indices are not necessarily similar across different 
transactions.
The procedure  \Readtr{$ o_{i_1},  o_{i_2}, \cdots, o_{i_p}$} can be 
initiated by  some reader  $r$,   as a {\sc read} transaction, intending to read the values of 
subset $o_{i_1},  o_{i_2}, \cdots, o_{i_p}$ of the objects. The procedure 
consists of two consecutively executed phases of communication rounds
between the $r$ and the  servers, viz.,  {{\it get-tag-array}} and {{\it read-value}}. 
During  the  phase {{\it get-tag-array}},  $r$ sends $s^*$ the message  {{\sc get-tag-array}}  
 requesting the  list of the latest added keys for each object. 
 Once $r$ receives a list of tags, such as, $(t_r, ({\kappa}_1, {\kappa}_2, \cdots,  {\kappa}_k))$ from $s^*$   the phase completes.
In the subsequence phase, {{\it read-value}},   $r$ requests each server $s_i$ in $S_I$ by sending the message 
$(\text{{\sc read-value}}, \kappa_i)$. 
After  receiving the values $v_{i_1}$, $v_{i_2}, \cdots v_{i_p}$ from the servers in $\mathcal{S_I}$, 
 $r$ completes the transaction  by 
 returning the tuple of values $(v_{i_1}, \cdots v_{i_p})$.


\emph{Server steps:}  
When a server $s_i$ receives a message of type $(${{\sc write-value}}$, ({\kappa}, v_{i}))$ from a writer $w$ then 
it  adds $({\kappa}, v_i)$ to its set variable  
$Vals$ and sends {{\sc acknowledge}} back to $w$.

If the coordinator $s^*$, receives  ({\sc  update-coord}, $({\kappa}, (b_{1}, \cdots, b_{k})$) from writer $w$, then it appends  
			 $({\kappa}, (b_{1}, \cdots, b_{k}))$ to its  $List$,  and responds with  
			 {{\sc acknowledge}} and $t_{w}$ (set to be the number of elements in the local list $List$)  to $w$.
			 The order of the  elements in  $List$ corresponds to  the order  
the {\sc write} transactions, the order of the incoming  {{\sc  update-coord}} updates,  as seen by $s^*$.
	
Again, when $s^*$  receives  the message  {{\sc get-tag-array}} from $r$  it responds with a message 
$(\kappa_1, \cdots, \kappa_k)$ such that for each $i \in [k]$, $\kappa_i$ is the key  part of the $(k+1)$-tuple that was modified
last, i.e., 	${\kappa}_i = List[j^*].{\kappa}$ such that 	 $j^* \triangleq\max \{ j : List[j].b_i =1 \}$, and 
$t_r$, $t_r \triangleq \max_{1 \leq j \leq |List|} \{ j : List[j].b_i = 1 \wedge i \in I\}$.

  	If any server $s_i$ receives a message  $(${{\sc read-value}}$, {\kappa})$ from a reader $r$ then it responds to $r$ with 
   the value $v_i$ corresponding to key with value  $\kappa$ in  $Vals$. 

	
Note the the following result states that algorithm $B$ respects SNoW  property.
Consider any failure-free and fair execution of algorithm $B$. 
For the purpose of proving the $S$ property, for every transaction transaction  $\phi$ in an execution of $B$ we associate a tag $tag(\phi)$ as described below.
If $\phi$ is a {\sc write} ({\sc read}) then  $tag(\phi)$ is the value of the variable $t_w$ ($t_r$) immediately before the 
operation completes.

	\begin{theorem} Any well-formed  and fair execution of algorithm $B$ is an implementation of  an object of type $\tilde{\mathcal{O}}_T$ in the MWMR setting, 
	with no client-to-client communication,  comprising of objects $o_1, o_2, \cdots o_k$ stored in servers $s_1, s_2, \cdots, s_k$, respectively; and it satisfies the SNoW  properties.
	\end{theorem}

\begin{proof} Below we show that algorithm $B$ satisfies the  SNoW properties. 
	
	\noindent{\emph{\underline{S property:}}} 
	Let $\beta$ be any fair execution  of  $B$ and 
 suppose all clients in $\beta$ behave in an well-formed
manner. Suppose $\beta$ contains no incomplete transactions and let  $\Pi$ be the set of transactions in $\beta$.  We define an irreflexive partial ordering ($\prec$) in $\Pi$ as follows:  if $\phi$ and $\pi$ are any two distinct transactions in $\Pi$ then we say 
	$\phi \prec \pi$ if either $(i)$ $tag(\phi) < tag(\pi)$ or $(ii)$ $tag(\phi) = tag(\pi)$ and $\phi$ is a {\sc write} and $\pi$ is a {\sc read}. Below we prove the $S$  property of $B$ by showing that  properties $P1$, $P2$, $P3$ and $P4$ of Lemma~\ref{lem:equivalence} hold for $\beta$. 
	
	\emph{P1:}   Clearly, from an inspection of the algorithm, 
	 $tag(\pi) \in \mathbb{N}$. From inspection of the algorithm, each {\sc write} increases the size of 
	 $List$, and the value of the tags are  defined by the size of $List$. Therefore, there can be at 
	 most a finite number of {\sc write}s such that can precede $\pi$ (w.r.t. $\prec$) in $\beta$.
	  On the other hand, if $\pi$ is a {\sc read} then since all {\sc read}s are invoked by readers  in a well-formed manner,  and there are only finite number of readers 
	therefore, there cannot be an infinite number of {\sc read}s such that they all 
	precede $\pi$ (w.r.t $\prec$).
	
	 
	  
	\emph{P2:}  Suppose $\phi$ and $ \pi$ are any two transactions in $\Pi$, such that, $\pi$ begins after $\phi$ completes. Then we show that we cannot have $\pi \prec \phi$. Now, we consider four cases, depending on whether $\phi$ and $\pi$ are {\sc read}s or {\sc write}s.	
	\begin{enumerate}
	    \item [$(a)$] $\pi$ and $\phi$ are {\sc write}s invoked by writers $w_{\phi}$ and $w_{\pi}$, respectively. Since the size of $List$, in $s^*$ grows monotonically due to each {\sc write}  hence  $w_{\pi}$ receives the  tag  from $s^*$ at least as high as $tag(\phi)$, so $\pi\not \prec \phi$.
	      %
	       \item [$(b)$] $\pi$ is a {\sc read}, $\phi$ is a {\sc write} invoked by reader  $r_{\pi}$ and writer $w_{\phi}$, respectively.  
	        Since the size of $List$, in $s^*$,  grows monotonically,  because  $r_{\pi}$  invokes $\pi$ after $\phi$ completes hence $tag(\pi)$ is at least as high as $tag(\phi)$, so $\pi\not \prec \phi$.
	      %
	        \item[$(c)$]$\pi$ and $\phi$ are both {\sc read}s  invoked by readers $r_{\pi}$ and $r_{\phi}$, respectively. 
	           Since the size of $List$, in $s^*$, grows monotonically,  because   $w_{\pi}$ invokes $\pi$ after $\phi$ completes hence $tag(\pi)$ is at least as high as $tag(\phi)$, so $\pi\not \prec \phi$.
	        %
	         \item [$(d)$] $\pi$ is a {\sc write}, $\phi$ is a {\sc read}  invoked by writer $w_{\pi}$ and reader $r_{\phi}$, respectively.
	         This case is simple because new values are added to $List$, in $s^*$,  only  by writers, and $tag(\pi)$ is at least as large as the tag of $\phi$ and hence   $\pi\not \prec \phi$. 
	\end{enumerate}
	
	
	\emph{P3:} This is from  the fact that any {\sc write} transaction always creates a unique tag and all tags are totally ordered since they all belong to $\mathbb{N}$
	
		\emph{P4:} Consider a {\sc read} $\rho$ as $READ(o_{i_1}, o_{i_2}, \cdots, o_{i_q})$, in $\beta$. 
Let the returned value from $\rho$ be $\mathbf{v} \equiv $$(v_{i_1}, v_{i_2}, \cdots, v_{i_q})$ such that 
$1 \leq {i_1} <  {i_2} <  \cdots <  {i_q} \leq k$, where value  $v_{i_j}$ corresponds to $o_{i_j}$. 
	Suppose $tag(\rho) \in \mathbb{N}$ was created during some {\sc write} transaction, say $\phi$, i.e., $\phi$ is the {\sc write} that 
	added the elements in index $(tag(\rho)-1)$ of $List$ at the coordinator $s^*$. Note that element in index $0$ contains the initial value.

	 Now we consider two cases:
	 
	\emph{Case $tag(\rho) = 1$.} We  know that it corresponds the initial default value $v_i^0$ at each sub-object $o_i$, and this equates to $\rho$ returning the default initial value for each sub-object.
	 %

	 
	 \emph{Case $tag(\rho) > 1$.} Then we argue that there exists no {\sc write} transaction, say $\pi$, that updated object $o_{i_j}$,   in $\beta$, such that,  $\pi \neq \phi$ and $\rho$ returns values written by $\pi$ and $\phi \prec \pi \prec \rho$. Suppose we assume the 	contrary, which means $tag(\phi) < tag(\pi) < tag(\rho)$. The latter implies $tag(\phi)  = tag(\pi)$ which is not possible because 
	this contradicts the fact that for any two distinct {\sc write}s $tag(\phi) \neq tag(\pi)$  in any execution of   $B$.

	\noindent{\emph{\underline{N, o and W properties:}}}  Evident from an inspection of the algorithm.

	\end{proof}




\remove{	
	\begin{proof} We prove that  SNW  + ``one version'' properties hold for algorithm $B$ below. 
	
	\noindent{\emph{\underline{S property:}}} We will show that the properties P1, P2 and P3 hold in any execution $\beta$ of the algorithm.  Observe that the result of Lemma~\ref{lem:atom} holds true even for crash failure of clients.
	
	\emph{P1:}  Suppose $\phi$ and $\pi$ are any two successful operations in $\beta$, such that, $\pi$ begins after $\phi$ completes. Now, we consider four cases, depending on whether $\phi$ and $\pi$ are reads or writes.
	
	\begin{enumerate}
	    \item  [] Case (i):  Operations $\phi$ and $\pi$ are {\sc write} transactions invoked by writers $w_{\phi}$ and $w_{\pi}$, respectively.  During the {{\it write-value}} phase of $\phi$ executed by  writer $w_{\phi}$,   each server $s\in \mathcal{S}$ adds triplets of  the tag $tag(\phi)$ (i.e. as, $t_w$), and the corresponding object value $v^{(s)}_{t_w}$,  and  the  \text{{\sc tentative}} state  to the $L$ variable of each server in $S$. Then in the immediately following, during the  {{\it commit}} phase each of these triplets  $(tag(\phi), v^{(s)}_{t_w}, \text{{\sc tentative}})$ in state variable  $L$, of every  server $s$,  are turned into  
	    $(tag(\phi), v^{(s)}_{t_w}, \text{{\sc commited}})$ 
	    Then since $\pi$ starts after the {{\it commit}} phase of $\phi$ ends, hence  during {{\it get-tag}} phase of $\pi$ each of the  servers returns commited tags at least as high as $tag(\phi)$ and since $w_{\pi}$ creates the new tag 
	       $tag(\pi)$ higher than $tag(\phi)$, so $\pi\not \prec \phi$.
	       
	       \item [] Case (ii): $\phi$ is a write, $\pi$ is a {\sc read} transactions invoked by writer $w_{\phi}$ and $r_{\pi}$, respectively.  
	       
	       As in the previous case, during the execution of $\phi$, we can argue about the addition of the triplet $(tag(\phi), v^{(s)}_{t_w}, \text{{\sc tentative}})$  to $L$ during {{\it write-value}} phase, and subsequent conversion of it to $(tag(\phi), v^{(s)}_{t_w}, \text{{\sc commited}})$   in the {{\it commit}} phase, at every server $s \in {\mathcal S}$.
	       Since 	   $\phi$ completes before $r_{\pi}$ invokes $\pi$, therefore, during {{\it get-tag}} phase of $\pi$ each of the  servers returns commited tags at least as high as $tag(\phi)$ and hence $tag(\pi)$ at least as  high as  $tag(\phi)$. But because $\phi$ is a write and $\pi$ is read hence by definition of $\prec$ we cannot have  $\pi  \prec \phi$.
	    
	        \item[] Case (iii): $\phi$ and $\pi$ are {\sc read} transactions invoked by readers $r_{\phi}$ and $r_{\pi}$, respectively. 
	        Note that in the {{\it get-tag}} phase of $\phi$, at $r_{\phi}$, the $tag(\phi)$  is created from the maximum of the 
	        responses from the servers. Note servers in this phase respond only with tags in {{\sc commited}}, an the fact that at least one commited tag exists in the $L$ variable of each server in $\mathcal{S}$, i.e., $(t_0, v^{(s)}, \text{{\sc commited}}) \in L$. 
	        Therefore, the corresponding values for tag $tag(\phi)$ exists in $L$ of every server in ${\mathcal S}$, either as 
	        {{\sc tentative}} or {{\sc commited}}. If they are in {{\sc tentative}} state at the end of the above {{\it get-tag}} phase then upon the arrival of the {{\sc read-value}} $t_r$, at any $s$, during the {{\it read-value}} phase, the triplet for the tag $tag(\phi)$ is converted to the {{\sc commited}} state. Now, since $\pi$ is invoked after $\phi$ terminates and   $tag(\pi)$ is created during the 
	        {{\it get-tag}} phase of $\pi$ hence the value of $tag(\pi)$ is at least as hight as $tag(\phi)$. But since both $\phi$ and $\pi$ are reads, by definition $tag(\phi) \leq tag(\pi)$, which implies $\pi \not\prec \phi$.
	        
	         \item [] Case (iv): $\phi$ is a read, $\pi$ is a {\sc write} transactions invoked by reader $r_{\phi}$ and $w_{\pi}$, respectively. 
	         Consider the value $v^{(s)}$, for any server $s \in \mathcal{S}$ returned as an element of the values
	          $(v^{(1)}, v^{(2)}, \cdots v^{(k)})$
	           at the end of transaction $\phi$. Now $v^{(s)}$ is sent to $r_{\phi}$  by $s$ in response to the
	          {{\sc read-value}}, $tag(\phi)$ message from $r_{\phi}$, during the {{\it read-value}} phase of $\phi$. Note that  at the point 
	          responding $(tag(\phi), v^{(s)})$, 
	          at server $s$, we have $(tag(\phi), v^{(s)}, \text{{\sc commited}})$.   Therefore, because   {\sc write} transaction $\pi$ starts after the {{\it commit}} phase of $\phi$ ends, hence  during {{\it get-tag}} phase of $\pi$ each of the  servers returns tags at least as high as $tag(\phi)$, therefore,  $w_{\pi}$ creates a new tag 
	       $tag(\pi)$ higher than $tag(\phi)$, so by definition of $\prec$,  $\pi\not \prec \phi$.
	\end{enumerate}
	
	\emph{P2:} This is clear by the fact that any {\sc write} transaction always creates a unique tag and all tags are totally ordered.
	
	\emph{P3:} Consider a {\sc read} transaction $\rho$,  then it tag $tag(\rho)$ was created during  some {\sc write} transaction, say $\phi$, because {\sc read} transactions do not create new tags. (Note that if $tag(\rho) = t_0$ we assume that there was an initial write that write $t_0$ at the beginning of the execution.) Therefore, $tag(\rho) = tag(\phi)$. 
	Then we argue that there exists no {\sc write} transaction, say $\pi$,  in $\beta$, such that,  $\pi \neq \phi$ and $\rho$ returns values written by $\pi$ and $\phi \prec \pi \prec \rho$. Suppose we assume the 
	contrary, which means $tag(\phi) < tag(\pi) < tag(\rho)$. The latter implies $tag(\phi)  = tag(\pi)$ which is not possible because tags of 
	distinct writes, such as, $\phi$ and $\pi$ are not alike in the execution of algorithm $C$.
	
	\noindent{\emph{\underline{N property:}}}  By inspection of the algorithm on the response functions of the servers we know that we have to argue the non-blocking  of the {{\it get-tag}} and {{\it read-value}} phase at the servers' response functions.
	    Note that in the {{\it get-tag}} phase of a {\sc read} transaction $\phi$, say invoked by a reader $r_{\phi}$, the $tag(\phi)$  is created from the maximum of the 
	        responses from the servers. Note servers in this phase respond only with tags in {{\sc commited}}, and the fact that at least one commited tag exists in the $L$ variable of any server $s$ in $\mathcal{S}$, for instance,  $(t_0, v^{(s)}, \text{{\sc commited}}) \in L$.  Therefore, {{\it get-tag}} phase of $\phi$ is non-blocking. 
	        For the {{\it read-value}} phase,  the corresponding values for tag $tag(\phi)$ exists in $L$ of every server in ${\mathcal S}$, either as     {{\sc tentative}} or {{\sc commited}}. If they are in {{\sc tentative}} state at the end of the above {{\it get-tag}} phase then upon the arrival of the {{\sc read-value}} $t_r$, at any $s$, during the {{\it read-value}} phase of $\phi$, the triplet for the tag $tag(\phi)$ is converted to the {{\sc commited}} state. Therefore, the send step  $(t_r, v^{(s)})$ s.t. $(t_r, v^{(s)}) \in L$  to reader $r_{\phi}$ is non-blocking.
		
		\noindent{\emph{\underline{W property:}}}  By inspection of the {\sc write} transaction steps, and supports writers that completes their transactions. Note that the completion of the {\sc write} transaction is clear since every server response only with the 
	{{\sc acknowledge}} message.
	
		\noindent{\emph{\underline{One Version property:}}} By inspection of the {\sc read} transaction which as two phases: {{\it get-tag}} and  {{\it read-value}}. Note that during {{\it get-tag}} no value is sent by the server and in the {{\it read-value}} phase  a server send only one version corresponding to the tag received.

	\end{proof}
}

\section{\text{SN$\bar{o}$W} for MWMR setting}\label{mwmr_snow}
In this section,  we present  algorithm  $C$ for  transaction processing in the   \emph{multiple-writers multi-reader} (MWMR) setting and show that   its execution  satisfies  SN$\bar{o}$W  properties, where ``$\bar{o}$'' means a {\sc read} consists of 
only one round trip of communications between the reader and the servers but the servers may respond with multiple versions of the data. We denote the type of object  that satisfies the SN$\bar{o}$W properties by $\bar{\mathcal{O}}_T$.   
The steps of the algorithm for the writers, readers and the servers  are presented in Fig.\ref{fig:algo_c}.
We assume there is a set of writers $\mathcal{W}$,  a set of readers $\mathcal{R}$ and a set of $k \geq 1$ servers,  $\mathcal{S}$, with ids $s_1, s_2\cdots s_k$ that stores the objects $o_1, o_2, \cdots, o_k$, respectively.  We define  key ${\kappa}$ is defined as a pair $(z, w)$, 
where $z \in \mathbb{N}$ and $w \in \mathcal{W}$ the  id of a writer. We use $\mathcal{K}$ to denote the set of all possible keys. As in the  algorithms presented in  Section~\ref{mwsr} and ~\ref{mwmr}, the keys are used to uniquely identify each transaction. Also, with each transaction we associate a tag $t \in \mathbb{N}$. 

\algremove{
\begin{algorithm}[!ht]
	\begin{algorithmic}[2]
	
		\begin{multicols}{2}{\footnotesize
					\Statex  {\bf At writer $w$}
					\Part{{\it State Variables}}{ 	
					\Statex $z \in \mathbb N$, initially   $0$
						}\EndPart
		\Statex  {\bf  \Writetr{$(i_1, v_{i_1}), (i_2, v_{i_2}), \cdots, (i_p,  v_{i_p})$}   }
					\State $I\triangleq \{i_1, i_2, \cdots, i_p \}$
				
				\Part{ \underline{{\it write-value}}} {
				   
				        \State ${\kappa} \leftarrow (z +1,  w)$; $z \leftarrow z +1 $
				         \For{$i \in I$} 
						\State Send {\sc write-value}, $({\kappa}, v_{s_i})$ to server $s_i$
					 \EndFor 
					\State  Await {{\sc acknowledge}} from servers in  $S_I$.
				}\EndPart
				\Statex
			      \Part{ \underline{{\it update-coord}}} {

                                      \For{$i \in [k]$} 
						\If{$i \in I$}
						 \State $b_i \leftarrow 1$
						 \Else
						   \State $b_i \leftarrow 0$
						\EndIf
					 \EndFor 
		
                                            \State  Send  ({\sc update-coord}, $({\kappa}, (b_{1}, \cdots, b_{k}))$) to   $s^*$

	
                     
				
					\State Receive ({{\sc acknowledge}}, $t_w$) from  coordinator $s^*$
				}\EndPart
			}\end{multicols}





	


\vspace{-1.5em}
 \\\hrulefill
\vspace{-1.5em}
			\begin{multicols}{2}{\footnotesize		
					\Statex  {\bf At reader $r$}
					\Statex  {\bf \Readtr{$ o_{i_1},  o_{i_2}, \cdots, o_{i_p}$}}	
					\State $I\triangleq \{i_1, i_2, \cdots, i_p \}$
				
	
	
	
						\Part{ \underline{{\it read-values-and-tags}}} {
					\State  Send  ({\sc get-tag-array}) to server $s^*$
				   \For{$i \in  I$} 
						\State  Send ({\sc read-values}) to $s_i$
						 \EndFor 
						 
					\State  Receive response  $(t_r, ({\kappa}_1, {\kappa}_2, \cdots, {\kappa}_k))$ from  $s^*$
					 
						\State  Wait responses as $Vals_{i}$ from each $s_i\in S_I$
						\State Return  $(v_{i_1}, v_{i_2}, \cdots, v_{i_p})$ s.t.  $({\kappa}_{j}, v_{j}) \in Vals_{j}$, $j\in I$
					}\EndPart
				}\end{multicols}
	
	
	
	

		


\vspace{-1.7em}
\\\hrulefill
\vspace{-1.5em}
			\begin{multicols}{2}{\footnotesize
					\Statex {\bf At server $s_i$ for any $i \in [k]$}
						\Part{{\it State Variables}}{ 
							\Statex $Vals\subset \mathcal{K} \times \mathcal{V}_i$, initially   $\{({\kappa}^0, v_i^0)\}$
						
						
						
					
\Statex $List$, a list  of  $\mathcal{K} \times \{ 0, 1 \}^k $, initially  $[({\kappa}^0, (1, \cdots 1))]$
						}\EndPart
						\Statex
						\Part {\underline{On recv ({\sc write-value}, $({\kappa}, v)$) from  $w$}} {
						           \State   $Vals \gets   Vals \cup \{({\kappa}, v)\}$ 
							\State  Send {{\sc acknowledge}} to writer $w$.
						}\EndPart
						\Statex
						\Part{{\underline{On recv  ({\sc update-coord}, $({\kappa}, (b_{1}, \cdots b_{k}))$) from  $w$}}}{ 
					     
                                 \State $List  \leftarrow List \bigoplus~ ({\kappa}, (b_{1}, \cdots b_{k}))$ 
					         //$\bigoplus$ for append
				
					        \State $tag \leftarrow |List|$ // $| \cdot |$ size of the list
						\State Send  ({{\sc acknowledge}}, $tag$) to  $w$
					}\EndPart
				           
					              \Statex
						\Part{ \underline{On recv ({{\sc read-values}}) from  $r$ }} {
							\State   Send $Vals$  to  $r$
						}\EndPart	
					\Statex\Statex   /* used only by $s^*$ */
					
					\Part{ \underline{On recv {{\sc get-tag-array}} from  $r$ }} {
					\For{$i \in [k]$} 
				             \State $j^* \leftarrow \max \{ j : List[j].b_i =1 \}$
				             \State ${\kappa}_i = List[j^*].{\kappa}$
					
					 \EndFor 
					   \State  $t_r \triangleq \max_{1 \leq j \leq |List|} \{ j : List[j].b_i = 1 \wedge i \in I\}$ 
						\State  Send  ($t_r, ({\kappa}_1,{\kappa}_2, \cdots, {\kappa}_k)$) to $r$
						}\EndPart				
					}\end{multicols}
				\end{algorithmic}	
				\caption{The protocol for any  writer $w$, reader $r$ or server $s_i$ for  algorithm $B$.}\label{fig:algo_c}
			\end{algorithm}	
}

In algorithm $C$, we designate one of the servers as the coordinator, we denote as $s^*$,
 for the transactions. In addition to managing some object, the server $s^*$ is used to maintain the order of the {\sc write}s and the objects that are updated during the {\sc write} in the variable $List$.  In any system, where there are many objects 
different objects may be use different servers  as coordinators based on some load-balancing rule. 

\emph{State Variables:} The state variables in algorithm $C$ is similar to those of algorithm $B$, therefore, we omit here.
			\emph{Writer steps:} The steps of a {\sc write} transaction is similarly to algorithm $B$, therefore, we omit here.



\emph{Reader steps:}  
The procedure  \Readtr{$ o_{i_1},  o_{i_2}, \cdots, o_{i_p}$} can be 
initiated by  some reader  $r$,   as a {\sc read} transaction, intending to read the values of 
subset $o_{i_1},  o_{i_2}, \cdots, o_{i_p}$ of the objects. 
We use the notations:  $I \triangleq \{i_1, i_2, \cdots, i_p\}$  and $S_I\triangleq \{s_{i_1}, s_{i_2}, \cdots, s_{i_p}\}$.
The procedure 
consists of only one  phase  of communication round
between the $r$ and the  servers, called  {{\it read-values-and-tags}}. 
During  the  phase {{\it read-values-and-tags}},  $r$ sends $s^*$ the message  {{\sc get-tag-array}}  
 requesting the  list of the latest added keys for each object, and also sends
    requests $(\text{{\sc read-values}})$  each server $s_i$ in $S_I$. Note that if $s^*$ is also one of the 
    servers in $S_I$ then the {{\sc get-tag-array}} and  {{\sc read-values}} messages to $s^*$ can be combined to create one message;     however, we keep them separate for clarity of presentation.
 Once $r$ receives a list of tags, such as, $(t_r, ({\kappa}_1, {\kappa}_2, \cdots,  {\kappa}_k))$ from $s^*$  and 
 the set of $Vals_{i}$ from each $s_i \in S_I$ then $r$ returns  the values 
 $v_{i_1}$, $v_{i_2}, \cdots v_{i_p}$ such that   $({\kappa}_{j}, v_{j}) \in Vals_{j}$, $j\in \{1, \cdots p\}$, and completes the 
{\sc read}.

\emph{Server steps:}  
When a server $s_i$ receives a message of type $(${{\sc write-value}}$, ({\kappa}, v_{i}))$ from a writer $w$; or if 
the coordinator $s^*$, receives  ({\sc  update-coord}, $({\kappa}, (b_{1}, \cdots, b_{k})$) from writer $w$ or 
 receives  a message as  {{\sc get-tag-array}} from $r$ the steps are similar to their counterparts in algorithm $B$. 
 Therefore, we omit them.
On the other hand, if any server $s_i$ receives a message  $(${{\sc read-values}}$)$ from a reader $r$ then it responds to $r$ with 
   the entire set of values, i.e., $Vals$. 
   
Note the the following result states that algorithm $C$ respects SN$\bar{o}$W  property.
Consider any failure-free and fair execution of algorithm $C$. 
For the purpose of proving the $S$ property, for every transaction transaction  $\phi$ in an execution of $C$ we associate a tag $tag(\phi)$ as described below.
If $\phi$ is a {\sc write} ({\sc read}) then  $tag(\phi)$ is the value of the variable $t_w$ ($t_r$) immediately before the 
operation completes.

	\begin{theorem} Any well-formed  and fair execution of algorithm $C$ is an implementation of  an object of type $\bar{\mathcal{O}}_T$ in the MWMR setting, 
	with no client-to-client communication,  comprising of objects $o_1, o_2, \cdots o_k$ stored in servers $s_1, s_2, \cdots, s_k$, respectively; and it satisfies the SN$\bar{o}$W  properties.
	\end{theorem}

\begin{proof} Below we show that algorithm $C$ satisfies the  SN$\bar{o}$W properties. 
	
	\noindent{\emph{\underline{S property:}}} 
	Let $\beta$ be any fair execution  of  $B$ and 
 suppose all clients in $\beta$ behave in an well-formed
manner. Suppose $\beta$ contains no incomplete transactions and let  $\Pi$ be the set of transactions in $\beta$.  We define an irreflexive partial ordering ($\prec$) in $\Pi$ as follows:  if $\phi$ and $\pi$ are any two distinct transactions in $\Pi$ then we say 
	$\phi \prec \pi$ if either $(i)$ $tag(\phi) < tag(\pi)$ or $(ii)$ $tag(\phi) = tag(\pi)$ and $\phi$ is a {\sc write} and $\pi$ is a {\sc read}. Below we prove the $S$  property of $B$ by showing that  properties $P1$, $P2$, $P3$ and $P4$ of Lemma~\ref{lem:equivalence} hold for $\beta$.  The properties $P1$-$P4$ can be proved to hold in a manner very similar to algorithm $B$ (Section~\ref{mwmr}). Therefore, we avoid repeating them. 

	\noindent{\emph{\underline{N, $\bar{o}$ and W properties:}}}  Evident from an inspection of the algorithm.

	\end{proof}


					{\small
						\bibliographystyle{plain}
						
\section{#1}
\newcommand{\Subsection}[1]{\subsection{#1}
\newcommand{\Subsubsection}[1]{\subsubsection{#1}
\newcommand{\Paragraph}[1]{\paragraph{#1}

\newcommand{{\mathbb N}}{{\mathbb N}}
\newcommand{\mathbb N}{\mathbb N}
\newcommand{\mathbb R}{\mathbb R}
\newcommand{{\mathbb R}^+}{{\mathbb R}^+}
\newcommand{\pm}{\pm}
\newcommand{C_{\bot}}{C_{\bot}}
\newcommand{\EXP}[1]{{\mathbb E}\left(#1\right)}
\newcommand{\Prob}[1]{{\mathbf P}{\mathbf r}\left(#1\right)}
\newcommand{\Var}[1]{Var\left(#1\right)}

\newcommand{\RAMBO}[1]{{\sc Rambo}$_{#1}$}
\newcommand{ack}{ack}
\newcommand{\ms}[1]{%
    \relax\ifmmode
        \mathord{\mathcode`\-="702D\it #1\mathcode`\-="2200}%
    \else
        {\it #1}%
    \fi
}

\newcommand{\lit}[1]{%
    \relax\ifmmode
        \mathord{\mathcode`\-="702D\sf #1\mathcode`\-="2200}%
    \else
        {\it #1}%
    \fi
}

\newcommand{\XA}[1]{#1}
\newcommand{\XD}[1]{#1}
\newcommand{\XDK}[1]{
\newcommand{\remove}[1]{}
\newcommand{\uselater}[1]{}
\newcommand{\viable}[1]{$#1${\it -viable\/}}

\renewcommand{\setminus}{-}

\newcommand{\igwsntp}[3]{\ms{ig({#1})_{#2}.w-sent({#3})}}
\newcommand{\igdsntp}[3]{\ms{ig(#1)_{#2}.d-sent(#3)}}

\newcommand{\ms{w-known}}{\ms{w-known}}
\newcommand{\igwknow}[2]{\ms{ig(#1)_{#2}.\ms{w-known}}}
\newcommand{\ms{d-known}}{\ms{d-known}}
\newcommand{\igdknow}[2]{\ms{ig(#1)_{#2}.\ms{d-known}}}

\newcommand{\ms{w-unack}}{\ms{w-unack}}
\newcommand{\igwunack}[2]{\ms{ig(#1)_{#2}.\ms{w-unack}}}
\newcommand{\ms{d-unack}}{\ms{d-unack}}
\newcommand{\igdunack}[2]{\ms{ig(#1)_{#2}.\ms{d-unack}}}
\newcommand{\igpack}[2]{\ms{ig(#1)_{#2}.\ms{p-ack}}}

\newcommand{\hmsg}[1]{\ms{h-msg}_{#1}}
\newcommand{\ms{h-MSG}}{\ms{h-MSG}}
\newcommand{\tup{W,v,t,cm,pns,pnr}}{\tup{W,v,t,cm,pns,pnr}}
\newcommand{\tup{W,v,t,cm,\ms{pm}}}{\tup{W,v,t,cm,\ms{pm}}}
\newcommand{{[h]}}{{[h]}}

\newcommand{\wdtp}[1]{\ms{w-sent(#1)}}
\newcommand{\ddtp}[1]{\ms{d-sent(#1)}}

\newcommand{\hrW}[1]{\ms{hrecv-W(#1)}}
\newcommand{\hsW}[1]{\ms{hsent-W(#1)}}
\newcommand{\hrD}[1]{\ms{hrecv-D(#1)}}
\newcommand{\hsD}[1]{\ms{hsent-D(#1)}}
\newcommand{\hsunack}[1]{\ms{hs-wunack(#1)}}
\newcommand{\hsdunack}[1]{\ms{hs-dunack(#1)}}
\newcommand{\hsknow}[1]{\ms{hs-wknow(#1)}}
\newcommand{\hsdknow}[1]{\ms{hs-dknow(#1)}}
\newcommand{\hsp}[1]{\ms{hs-pack(#1)}}
\newcommand{\hsworld}[1]{\ms{hs-world(#1)}}
\newcommand{\hsdep}[1]{\ms{hs-departed(#1)}}

\newcommand{$MSG_{{\scriptscriptstyle \mathrm{RA}}}$}{$MSG_{{\scriptscriptstyle \mathrm{RA}}}$}
\newcommand{$MSG_{{\scriptscriptstyle \mathrm{LR}}}$}{$MSG_{{\scriptscriptstyle \mathrm{LR}}}$}
\newcommand{$MSG_{{\scriptscriptstyle \mathrm{IG}}}$}{$MSG_{{\scriptscriptstyle \mathrm{IG}}}$}

\newcommand{\hat{n}}{\hat{n}}
\newcommand{\IGR}[1]{{\sc Atila{#1}}}
\newcommand{\HR}[1]{{\sc H}-\RAMBO{{#1}}}

\newcommand{\ms{world}}{\ms{world}}

\newcommand{\peter}[1]{\textcolor{red}{{\bf (Peter:)} #1}}
\newcommand{\cgc}[1]{#1
\newcommand{\cg}[1]{#1
\newcommand{\red}[1]{\textcolor{red}{{#1}}}
\newcommand{\blue}[1]{\textcolor{blue}{{#1}}}



\newcommand{\point}[1]{~\\\smallskip\noindent {\tt (*)} #1}

\newcommand{\ef}[2]{
    \begin{tabbing}
    XX\= XX\=XX\=XX\=XX\=XX\=  \kill
    \protect #1\\
    ~ Effect: \+ \\
      #2 \- 
\end{tabbing}}

\newcommand{\prcef}[3]{
    \begin{tabbing}
    XX\= XX\=XX\=XX\=XX\= \kill
    \protect #1\\
    ~ Precondition: \+ \\
     #2 \- \\
    ~ Effect: \+ \\
     #3 \- 
\end{tabbing}}

\newenvironment{mylisting}
{\begin{list}{}{\setlength{\leftmargin}{1em}}\item\scriptsize\bfseries}
{\end{list}}

\newenvironment{mytinylisting}
{\begin{list}{}{\setlength{\leftmargin}{1em}}\item\tiny\bfseries}
{\end{list}}

