\makedraft{timestamps.tex}
\chapter{Timestamp Algorithms}
\label{timestamp_chapter}
\label{timestamp-chapter}
\label{timestamps-chapter}

\section{Introduction}

%[[[Also in hybrid chapter, change the name H_X(C) which now conflicts with herlihy object.
%I suggest D_X(C) for dependency. 
%A 5/91]]]

%[[[I changed some postconditions to avoid mentioning 
%components that don't change.  (Mostly when state components
%are functions, I removed mention of the part of the function
%that doesn't change.  This is pretty clear from our discussion
%of notation earlier, and I'd rather leave it as is, or
%mention the first time we do it that updating one
%(argument, value) pair leaves the rest unchanged. M.]]]
%Alan checked and apparantly concurred 7/90
%[[[Is this carried consistently throughout the book?  N. 5/91]]]
%[[[A 7/91 I do NOT like this. I prefer use of functional
%modification using an overwrite operator (I think \oplus is
%used in Z).]]]

%[[[We need to go through all code carefully, for consistency regarding
%variables not bound in the action name. We do not always indicate when
%we mean universal quantification A 5/91]]]
%[[[I find the ``Let...'' construct used in the code for H_X to be ugly.
%I prefer ``...., where ...'' A 5/91]]]


%[[[We might use ``timestamp'' everywhere in this book where we have
%timestamp-like objects, instead of ``pseudotime'' in some places and
%``timestamp'' in others.  I don't have a good general policy here. N. 5/91]]]
%[[[A 7/91 I have a concept here: a pseudotime indicates the apparent 
%point in serial schedule.; a timestamp is any value assigned to a 
%transaction; one construction of pseudotime is to give each T its pseudotime
%as a timestamp, but there are other constructions too. I have tried to
%explain this]]]

%[[[A 7/91
%As pointed out by Jeff, our terms were very bad: the generic system
%consists of generic controller and g. objects, but pseudotime controller
%and ps. objects formed a ``distributed pseudotime system''. I have deleted
%the word distributed, and have renamed the former pseudotime system as
% a simple-pseudotime system; this also means that the important
%concept has the shorter name]]]

%[[[We use here the relations \ms{pseudotime-order} and \ms{local-pseudotime-order}, 
%but elsewhere we name our relations
%\ms{completion}, not \ms{completion-order}, etc. 
%We should be uniform A 5/91]]]

%[[[I have simplified our discussion of Reed's algorithm,
%from a serial object with a classification, to just for a read/write
%serial object A 5/91]]]

Most database management systems implement transactions using locking algorithms
like those described in Chapter \ref{locking_chapter}. However the
research prototype SDD-1 \cite{?SDD1} used a different
technique, where each transaction is given a timestamp, and the serial
execution that the concurrent execution looks like is the execution in
the order of the timestamps. In this algorithm, each object maintains
the highest timestamp of the accesses that have read it, and also the timestamp of the
transaction that wrote the current version. Accesses are disallowed if their
timestamps are not appropriate (for example, attempting to read with a
timestamp less than  that of the writer of the current version).
A number of similar algorithms have been
suggested. Practical experience and simulation
studies have cast doubt on the performance of timestamp algorithms,
but the ideas have undoubted appeal, especially because in
many variants deadlocks
are not possible (so the expense of deadlock detection can be avoided).

The first implementation of a nested transaction system (by D. Reed
in 1978 \cite{Reed78}) did not use an algorithm based on locks. Instead it used an
algorithm where each transaction is assigned an {\em effective interval} of
{\em pseudotime}.
%[[[A 7/91
One can think of this as being a time period within which the transaction
{\em appears} to execute. That is, the correctness condition (atomicity)
requires that there be a serial execution that looks the same 
as the actual execution. If one
were to record time passing in the serial execution, each transaction
would be active during a particular
interval. Since the serial execution is only {\em apparent}
(it does not actually occur), the intervals
are referred to as being periods
of {\em pseudotime}.
We remark that the structure of a serial execution means that
these pseudotime intervals will satisfy some constraints:
for example, the interval in which a subtransaction appears to
be active must lie within the interval in which its parent
appears to be active, and it must be disjoint from the period in
which any sibling appears to be active.

In Reed's system,
the assignment of an effective interval to a transaction
takes place at the transaction's initiation.
The concurrency control mechanism  uses these intervals to
control the responses given to
accesses, in a way that provides atomicity; it
ensures that the serial system has an execution that could be
observed with the times assigned.
Reed's algorithm is a {\em multiversion} algorithm,
based on the realization that since recovery from transaction abort requires
the system to maintain information about earlier versions of the object,
read accesses can be allowed to see those versions, and thus read transactions
can run even with pseudotimes 
earlier than other transactions concurrently in the  system.


This chapter applies the Atomicity Theorem to prove correctness
of some algorithms that are based on the use of pseudotime intervals.
Each algorithm serializes transactions in the order given by
these intervals.
As in Chapter \ref{locking-chapter}, different algorithms that use
the same serialization order can coexist in a single system
without atomicity being endangered, and our correctness proofs are
structured to allow modular verification of a system.
%]]]

\subsubsection{Syntactic Contraints: Simple-Pseudotime Systems}
In the development of Chapter \ref{serializability-chapter},
{\em simple systems} were defined, which consisted of the (user-defined)
transaction automata composed with a {\em simple database} automaton.
The latter imposed only simple syntactic constraints on the
behaviors of simple systems. The Atomicity Theorem 
then stated specific semantic conditions on simple behaviors
which are sufficient to maintain atomicity.

To apply this theory to algorithms like Reed's, 
it is convenient to ``expose'' the assignment of pseudotime intervals to
transactions at the external interface of the system.
This is done by defining a new class of systems, {\em simple-pseudotime 
systems},
in which the simple database automaton has been replaced by
a {\em simple-pseudotime database automaton}.  This automaton extends the
simple database by adding events which assign intervals to
transactions.
The simple-pseudotime database provides enough information to define and reason
about the sibling order used by the algorithms in this chapter.
It is also general enough that it applies to other system organizations
as well, such as one presented in Chapter \ref{optimism-chapter}.
As with the simple database, the simple-pseudotime database
imposes only syntactic restrictions on behaviors of simple-pseudotime systems.
In particular, when the extra events are removed, behaviors of
pseudotime systems are also simple behaviors.
This relationship allows us to apply the Atomicity Theorem,
which refers to simple behaviors, to behaviors of simple-pseudotime
systems.

\subsubsection{Sufficient Conditions for Correctness: 
Static and Local Static Atomicity}

Just as generic systems decompose simple systems by replacing
the simple database with a generic controller and generic objects,
{\em pseudotime systems} decompose the simple-pseudotime
database into a {\em pseudotime controller} and 
{\em pseudotime objects}.
The pseudotime controller is an automaton similar to the generic controller,
with additional actions that assign pseudotime intervals to transactions.
The substantive concurrency control and recovery algorithms
are implemented in the pseudotime objects, just as locking
algorithms are implemented in generic objects.
{\em Static atomicity},  a condition on pseudotime objects, 
guarantees atomicity.  This condition corresponds
to the dynamic atomicity condition on generic objects,
%[[[
except that the serialization order is that of the pseudotime
intervals and not the completion order.
%]]]
Finally, corresponding to the local dynamic atomicity condition which
is sufficient for dynamic atomicity, {\em local static atomicity} is 
a sufficient condition for static atomicity.
Like local dynamic atomicity,
this local condition affords modularity:  
different concurrency
control and recovery algorithms can be used at different objects,
as long as each object ensures local static atomicity. Note
that one cannot in general combine correct algorithms and
be certain of retaining correctness;
for example using Moss's algorithm described in Chapter \ref{locking_chapter}
for some objects, and Reed's algorithm for others can lead to 
behavior that is not atomic (see Exercise \ref{moss-not-static}).

\subsubsection{Two Algorithms}
Next, two timestamp-based concurrency control algorithms are studied, both
of which ensure local static atomicity.
The results of this chapter imply that one of the algorithms could be used at
some objects in a system, and the other at other objects,
and global correctness would still be guaranteed.
Such modularity is essential in distributed or object-oriented
databases, in which different objects are implemented independently.
Specifically, formal descriptions and correctness proofs are given for
two algorithms:  a multi-version timestamp-based algorithm
based on Reed's \cite{Reed78},
and a
type-specific timestamp-based
algorithm 
that is a generalization to nested transactions of an algorithm
of Herlihy \cite{Herlihy87}.
The latter algorithm uses the semantics of operations to permit
a higher level of concurrency than can be achieved 
%[[[
when the operations are simply reads and writes.
%A 5/91]]]
In both cases, the algorithms are described in a general fashion
that permits a high level of concurrency and requires relatively few aborts
by maintaining  precise information about what transpires during
an execution.

\subsubsection{Parallels to Earlier Material}
The theory developed in the early sections of this
chapter parallels material found
earlier in the book.
Section \ref{ts_simple-pseudotime-systems}, introducing 
simple-pseudotime systems,
is identical in outline to Section \ref{simple-systems-section},
where simple systems are introduced.
Section \ref{static-atomicity-section}, introducing 
pseudotime systems, static atomicity, and local static atomicity,
has the same organization as 
Section \ref{dynamic-atomicity-section}, where
generic systems, dynamic atomicity, and local dynamic atomicity
are developed.
Differences between the latter two sections can be attributed
to the total ordering information available to objects in
the context of timestamp algorithms, while only partial
ordering information is available to objects in locking
algorithms.  (Contrast 
Lemma \ref{ts_orders-all} with Lemma \ref{completion-partial},
and 
Lemma \ref{ts-order-at-X-order-relate} with \ref{locking_order_at_X_order_relate}.)
%M:1/91]]]

\subsection{Timestamps: Pseudotime Intervals}
\label{pseudotime-interval-section}

The essential feature of the systems considered in this chapter is the explicit
construction of a sibling order representing the intended
serialization of an execution.  This order is represented in terms of
intervals of \df{pseudotime}, an arbitrarily-chosen totally-ordered set.
\index{pseudotime}
Formally, let $\cal P$ be the set of pseudotimes, ordered by $<$.  
Pseudotime intervals are represented as half-open intervals [p,q) in $\cal P$, 
are referred to by capital letters. 
If $P$ = [p,q), then write $P_{min}$ for p and $P_{max}$ for q.  
If $P$ and $Q$ are intervals of pseudotime,
write $P < Q$ if $P_{max} \leq Q_{min}$.  Clearly, if $P < Q$,
then $P$ and $Q$ are disjoint.

%[[[A 7/91
One obvious choice for pseudotimes is  the set of positive real numbers.
This set has the advantage that it is dense,
so that one can always find a subinterval
within a given interval (as might be required if the transaction tree
is arbitrarily deep).
Due to the finite precision of computer representations, an alternative might
be to use integers as pseudotimes. In this case both the depth of
nesting and the number of children invoked by any transaction
would need to be restricted, or in some execution it
would not be possible to assign a satisfactory interval to a transaction
that had been invoked.

A more complex choice for pseudotimes, that is actually
particularly suitable for distributed systems, is the set
of all finite sequences of positive integers ordered
lexicographically. Thus if $p = 2,4,1,2,5,3$ and $q=2,4,1,4,3$, then $p < q$
(since the first entry that is different is the fourth, which is 2 in $p$
and 4 in $q$). In this case, some pseudotime intervals
are particularly easy to specify: those that consist
of all sequences with a given prefix.
We introduce the notation $p,\star$ to represent the
set consisting of those sequences with $p$ as prefix.
For example, when $p = 2,4,1,2,5,3$, then 
$p,\star$ is a set that contains pseudotimes such as $2,4,1,2,5,3,6$ and 
$2,4,1,2,5,3,3,1$; the reader can check that in this case
$p,\star = [p,p')$ where  
$p' = 2,4,1,2,5,4$, showing that $p,\star$ is indeed a pseudotime interval.

It is fairly easy to design a system which gives 
each transaction a {\em timestamp} which is a positive integer greater 
than any timestamp  already given to a sibling.
The pseudotime interval assigned to a transaction can be 
the interval of all pseudotimes which have 
as prefix the sequence of timestamps given to the 
transaction's ancestors (in order from $T_0$ to the 
transaction itself). Assigning pseudotime intervals in this way
ensures that each transaction's pseudotime interval is contained
within its parent's pseudotime interval, 
and is disjoint from any sibling's pseudotime interval.
%]]]

\section{Simple-Pseudotime Systems}
\label{ts_simple-pseudotime-systems}

This section describes the interval generation
mechanism, as an extension to the simple database
introduced in Section \ref{simple-database-section}.
In addition to the simple syntactic properties 
guaranteed by the simple database, 
the {\em simple-pseudotime database} guarantees that siblings are assigned
disjoint intervals of pseudotime, and that each transaction's interval is a
subset of that of its parent. 
%[[[A 7/91
The serialization order for the system will be the comparative
order of pseudotime intervals.
%former version (too technical):
%It is not difficult to show that any
%assignment corresponding to these conditions imposes an order on
%transactions that is the descendant closure of a sibling order.
%]]]

\subsection{Simple-Pseudotime Database}
\index{simple-pseudotime database}

The \df{simple-pseudotime database} for a given system type,
like the simple database, is a specific automaton. 
This automaton generates pseudotime intervals for transactions in the way 
suggested by Reed; that is, each transaction after creation is assigned
an interval of values from a domain of pseudotimes, chosen so as to
be a subinterval of the parent transaction's interval and disjoint
from (and following) the intervals of previously assigned sibling
transactions.
%[[[
These restrictions reflect the way the actions of the transaction
must appear in a schedule of a serial system: they must all be during
the period in which the parent is active, but in a period disjoint from
that when any sibling is active.
The simple-pseudotime database %A 5/91]]]
has the actions of the simple database
together with an extra class of output actions \ASPS{T}{P}
for $T \neq T_{0}$ and $P$ a pseudotime interval.
A state $s$ of the simple-pseudotime database has the same components as
a state of the simple database,
together with an additional
component $\ms{s.interval}$, which is a
partial function from $\cal T$ to the set of pseudotime intervals.
%[[[A 7/91
This component records the pseudotime interval that has been assigned
to each transaction.
%]]]
In the initial state of the simple-pseudotime database, 
$\ms{interval} = \{(T_{0},P_{0})\}$, for some pseudotime interval $P_{0}$; 
and all
other components are as in the initial state of the simple database.

The transition relation is the same as that for the simple database,
except in the following ways:
%[[[A 7/91 itemized as suggested by reading group]]]
\begin{itemize}
\item
the actions \CRT{T} and \AB{T} have an additional precondition:
$T \in \ms{domain(s'.interval)}$, 
\item
and the 
additional \asps{} actions are 
determined as follows:

\iocode{
%DO NOT put this in a figure
\prcef{\ASPSntab{T}{P}}
{%Precondition:
     $T \in \ms{s'.create-requested}$\\
     $T \notin \ms{domain(s'.interval)}$\\
%[[[A 7/91 makes things nicer
     $\ms{parent}(P) \in \ms{domain}(\ms{s'.interval})$\\
%]]]
     $P \subseteq \ms{s'.interval}(\ms{parent}(T))$\\
     $P > \ms{s'.interval}(T')$ for every $T'$ in $\ms{siblings}(T) \cap \ms{domain}(\ms{s'.interval})$}
{%Effect:
     $\ms{s.interval} = \ms{s'.interval} \cup \{(T,P)\}$}}{}

\end{itemize}

%[[[A 7/91
This ensures that  before being
created or aborted, any transaction has been assigned
a pseudotime interval, and that the intervals are related
in the way needed to represent a serialization order.
Also, the order of the intervals among a group of
siblings is the same as the order of a set of events (the \asps{}
events) that occur each after the corresponding \rqcr{}; this
is needed for the sibling order defined to be suitable.
In essense, this is what ensures {\em external
consistency}; i.e. that the serial order
is consistent with the observed order (for example, when
one subtransaction's \crt{} follows another's \rpcm{}, the parent
knows the relative order).
%]]]

%[[[A 11/91
\begin{example}{A Message Queue System}
\label{ts-queue-system-ex1}
Consider the message queue system of Example
\ref{ss-queue-system-example}.
We will use as the set of pseudotimes, the set of finite
sequences of positive integers, ordered lexicographically, as discussed
in Section \ref{pseudotime-interval-section}.
Here is a schedule of the simple-pseudotime database constructed 
for that system type and pseudotime domain.

\schedlist{
\CRT{T_0}\\
\>\RQCRntab{T_{G3}}\\
\>\>\RQCRntab{T_{G2}}\\
\>\>\>\RQCRntab{T_{R1}}\\
\>\>\ASPSntab{T_{G2}}{1,\star}\\
\>\>\>\ASPSntab{T_{R1}}{2,\star}\\
\>\ASPSntab{T_{G3}}{3,\star}\\
\>\CRT{T_{G3}}\\
\>\RQCMntab{T_{G3}}{\qms{OK}}\\
\>\>\>\>\>\RQCRntab{T_{R2}}\\
\>\>\CRT{T_{G2}}\\
\>\CM{T_{G3}}\\
\>\>\RQCMntab{T_{G2}}{\qms{OK}}\\
\>\>\>\CRT{T_{R1}}\\
\>\>\>\>\RQCRntab{T_{R1.0}}\\
\>\>\>\>\ASPSntab{T_{R1.0}}{2,1,\star}\\
\>\>\>\>\CRT{T_{R1.0}}\\
\>\>\>\>\>\ASPSntab{T_{R2}}{4,\star}\\
\>\>\>\>\>\CRT{T_{R2}}\\
\>\>\>\>\>\>\RQCRntab{T_{R2.0}}\\
\>\>\>\>\>\>\ASPSntab{T_{R2.0}}{4,1,\star}\\
\>\>\>\>\>\>\CRT{T_{R2.0}}\\
\>\>\>\>\>\>\RQCMntab{T_{R2.0}}{3}\\
\>\>\>\>\RQCMntab{T_{R1.0}}{2}\\
\>\>\>\>\>\>\CM{T_{R2.0}}\\
\>\>\>\>\>\>\RPCMntab{T_{R2.0}}{3}\\
\>\>\>\>\>\>\>\RQCRntab{T_{R2.A3}}\\
\>\>\>\>\>\>\>\>\RQCRntab{T_{R2.B3}}\\
\>\>\>\>\>\>\>\>\ASPSntab{T_{R2.B3}}{4,2,\star}\\
\>\>\>\>\>\>\>\ASPSntab{T_{R2.A3}}{4,3,\star}\\
\>\>\>\>\>\>\>\CRT{T_{R2.A3}}\\
\>\>\>\>\>\>\>\RQCMntab{T_{R2.A3}}{\qms{OK}}\\
\>\>\>\>\>\>\>\CM{T_{R2.A3}}\\
\>\>\>\>\>\>\>\>\CRT{T_{R2.B3}}\\
\>\>\>\>\>\>\>\RPCMntab{T_{R2.A3}}{\qms{OK}}\\
\>\>\>\>\>\>\>\>\RQCMntab{T_{R2.B3}}{\qms{OK}}\\
\>\>\>\>\>\>\>\>\CM{T_{R2.B3}}\\
\>\>\>\>\>\>\>\>\RPCMntab{T_{R2.B3}}{\qms{OK}}\\
\>\>\>\>\>\RQCMntab{T_{R2}}{\qms{OK}}\\
\>\>\>\>\>\CM{T_{R2}}
}

This schedule can leave the simple-pseudotime database in a state $s$
where
$s.\ms{interval}(T_{G3})= 1,\star$,
$s.\ms{interval}(T_{R1})= 2,\star$,
$s.\ms{interval}(T_{R1.0})= 2,1,\star$,
$s.\ms{interval}(T_{G2})= 3,\star$,
$s.\ms{interval}(T_{R2})= 4,\star$,
$s.\ms{interval}(T_{R2.0})= 4,1,\star$,
$s.\ms{interval}(T_{R2.A3})= 4,3\star$,
$s.\ms{interval}(T_{R2.B3})= 4,2,\star$,
and $s.\ms{interval}(T)$ is undefined for other values of $T$.

The reader should notice some features of this schedule.
Firstly, the pseudotime intervals assigned to the siblings $T_{R2.0}$, $T_{R2.A3}$,
and $T_{R2.B3}$ are related (by the order induced by the lexicographic order on
pseudotimes) in the same order as the occurrence of the $\asps${} events for those siblings,
which is different from the order of $\rqcr${} events or $\crt${} events.
Secondly, the pseudotime interval assigned to $T_{R1.0}$ is less than the pseudotime 
interval assigned to $T_{G3}$ because of the order
in which the $\asps${} events occurred for their sibling ancestors $T_{R1}$ and $T_{G3}$,
despite the fact that the $\asps${} events for the accesses themselves occurred in
the reverse order.
\end{example}
%]]]

\subsubsection{Basic Properties of the Simple-Pseudotime Database}

%[[[A 7/91
The following simple lemma follows the pattern of
Lemma \ref{gt_simple_database_states} for the simple database.
It relates a schedule of the
simple-pseudotime database to the resulting states, and gives
simple invariants.
The extra facts (parts \ref{ts_simp_cond_spec1},
\ref{ts_simp_cond_spec2}, and
\ref{ts_simp_cond_spec3}) relate to the additional actions and state component,
compared to the simple database.
%]]]

\begin{lemma}
\label{ts_simple-pseudotime_database_schedules_1}
If $\beta$ is a finite schedule of the simple-pseudotime database
that can lead to state $s$,
then the following conditions are true.
\begin{enumerate}
\item $T$ is in $\ms{s.create\_requested}$ if and only if
either $T = T_{0}$ or $\beta$ contains a \RQCR{T} event.

\item $T$ is in $\ms{s.created}$ if and only if
$\beta$ contains a \CRT{T} event.


%[[[A 7/91
\item
\label{ts_simp_cond_spec1}
$(T,P)$ is in $\ms{s.interval}$ if and only if
either $(T,P) = (T_0, P_0)$ or $\beta$ contains
an \ASPS{T}{P} event.
%]]]

\item $(T,v)$ is in $\ms{s.commit\_requested}$ if and only if
$\beta$ contains a \RQCM{T}{v} event.

\item $T$ is in $\ms{s.committed}$ if and only if $\beta$ contains a \CM{T} event.

\item $T$ is in $\ms{s.aborted}$ if and only if $\beta$ contains an \AB{T} event.

\item $T$ is in $\ms{s.reported}$ if and only if $\beta$ contains a report event for $T$.

\item $\ms{s.committed} \cap \ms{s.aborted} = \emptyset$.

\item $\ms{s.reported} \subseteq \ms{s.committed} \cup \ms{s.aborted}$.

%[[[
\item
\label{ts_simp_cond_spec2}
if $T$ and $T'$ are sibling transactions in $\ms{domain}(\ms{s.interval})$,
then $\ms{s.interval}(T)$ is disjoint from $\ms{s.interval}(T')$.

\item
\label{ts_simp_cond_spec3}
if $T$ is in $\ms{domain}(\ms{s.interval})$,
then $\ms{parent}(T)$ is in  $\ms{domain}(\ms{s.interval})$, and
$\ms{s.interval}(T) \subseteq \ms{s.interval}(\ms{parent}(T))$.
%]]]
\end{enumerate}
\end{lemma}

%[[[A 7/91
We next give some immediate consequences of the previous lemma 
and the preconditions of the actions of the
simple-pseudotime database.
%]]]

\begin{lemma}
\label{ts_simple-pseudotime_database_schedules_2}
Let $\beta$ be a %finite[[[M. 1/91]]] 
schedule of the simple-pseudotime database.
Then all of the following hold:
%[[[added ``for $T \neq T_0$,''  below. M:1/91]]]
\begin{enumerate}
\item If an \ASPS{T}{P} event appears in $\beta$ for $T \neq T_0$, 
then a \rqcr{} event for $T$ precedes it in $\beta$.

\item If a \CRT{T} event appears in $\beta$ for $T \neq T_0$, 
then an \asps{} event for $T$ precedes it in $\beta$.

\item If an \AB{T} event appears in $\beta$, then an
\asps{} event for $T$ precedes it in $\beta$.

\item If an \asps{} event for $T$ appears in $\beta$, and
$\ms{parent}(T) \neq T_{0}$, then an \asps{} event
for $\ms{parent}(T)$ precedes it in $\beta$.

\item At most one \asps{} event appears in $\beta$ for each
transaction.

\item If $T$ and $T'$ are sibling transactions, and \ASPS{T}{P} precedes \ASPS{T'}{P'} 
in $\beta$, then $P < P'$.

\item $T \in \ms{s.interval}$ if and only if $T = T_{0}$ or if an \asps{}
event for $T$ appears in $\beta$.

\item If $T \in \ms{domain}(\ms{s.interval})$ and $T$ is a descendant of $T'$,
then $T' \in \ms{domain}(\ms{s.interval})$ and $\ms{s.interval}(T) \subseteq
\ms{s.interval}(T')$.
\end{enumerate}
\end{lemma}

\subsection{Simple-Pseudotime Systems, Executions, Schedules and Behaviors}

A \df{simple-pseudotime system} is the composition of a set of automata
\index{simple-pseudotime system}
indexed by the  set of non-access transaction names and
the single name \df{SPD} (for {\em simple-pseudotime database}).
Associated with each non-access transaction name $T$ is a transaction
automaton $A_{T}$ for $T$.
Also, associated with the name  \df{SPD} is the simple-pseudotime database
automaton for the given system type.

When the particular simple-pseudotime system is 
understood from context, the terms \df{simple-pseudotime 
executions}, \df{simple-pseudotime schedules}, and \df{simple-pseudotime behaviors} are 
used for the system's executions, schedules, and behaviors, respectively.

The following is immediate.\footnote{Recall 
from Section
\ref{serial_basic_defs_section}
that $\ms{serial}(\beta)$ denotes the subsequence of 
$\beta$ obtained by removing those actions that are not
serial actions. In this case, the actions
removed are the \asps{} actions.}
%[[[A 7/91 footnote added]]]

\begin{proposition}
\label{ts_simple-pseudotime_simple}
If $\beta$ is a simple-pseudotime behavior, then
$\ms{serial}(\beta)$ is a simple behavior and
$\ms{serial}(\beta)|T = \beta|T$ for all transaction names $T$.
\end{proposition}

%[[[A 7/91
We also have the following straightforward result, whose
proof is left as Exercise \ref{ts-simple-exc}.
%]]]

\begin{lemma}
\label{ts_pseudotime_assigned}
Let $\beta$ be a simple-pseudotime behavior, 
and let $T$ be a transaction name such that
$\ms{serial}(\beta)$ contains an event $\pi$ with lowtransaction a descendant of $T$.
Then an \asps{} event for $T$ precedes $\pi$ in $\beta$.
\end{lemma}

%[[[A 11/91
\begin{example}{Simple-Pseudotime Behavior In A Message Queue System}
Consider the serial system described in Example \ref{ss-queue-system-example}.
The schedule given in Example \ref{ts-queue-system-ex1} is a simple-pseudotime behavior.
\end{example}
%]]]

\section{Static Atomicity}
\label{static-atomicity-section}

This section tailors the concepts of Chapter \ref{serializability-chapter}
to algorithms like Reed's.  In these algorithms, siblings are  
ordered by explicitly assigned pseudotimes.
Transactions
with conflicting accesses to objects are serialized by those
objects in the order of the transactions'
pseudotimes.
%[[[A 7/91
Hence, we define the appropriate sibling order,
and then model the system
containing objects that use this order.
%]]]

\subsection{Pseudotime Order}

\sloppy
The purpose of the \asps{} actions is to construct, at
run-time, a sibling order that specifies the apparent serial
ordering of transactions.  
If $\beta$ is a sequence of events, 
then define the relation \df{$\ms{pseudotime-order}(\beta)$} as follows.
\index{pseudotime-order($\beta$)}
Say that $(T,T') \in \ms{pseudotime-order}(\beta)$
exactly if $T$ and $T'$ are siblings,
and \ASPS{T}{P} and \ASPS{T'}{P'} 
occur in $\beta$ with $P < P'$.
%[[[A 7/91
Notice that what is defined here relates only siblings to one another.
%]]]
\fussy

The following is immediate.

\begin{lemma}
\label{ts_pseudotime_order}
If $\beta$ be a simple-pseudotime behavior, 
then $\ms{pseudotime-order}(\beta)$ is a sibling order.
\end{lemma}
				   
The next few lemmas show that the pseudotime order is suitable,
which allows application of the Atomicity Theorem.
The first shows that events of one transaction $T$ can
affect (in the technical sense of the $\ms{affects}(\ms{serial}(\beta))$ relation,
%[[[A 7/91 replacing previous irrelevant remark about completions
defined in Section \ref{gt_affects_section})
events of an unrelated transaction $T'$ only if $T$ is ordered before $T'$
by the descendant closure of the pseudotime order.
In essense, this is because the least common ancestor must
recieve the report of  the completion of the ancestor of $T$
before requesting the creation of
the ancestor of $T'$; since the \asps{} event for
one transaction must precede its completion,
and the asps{} event for the other must follow the request to create it,
we see that the sibling ancestors of $T$ and $T'$ have their
\asps{} events in that order. Since pseudotime intervals are
assigned among siblings in increasing order, the pseudotime
intervals of the ancestors of $T$ and $T'$ are in that order. and
since the intervals of $T$ and $T'$ are subintervals of those 
of their respective ancestors, the result follows.
%]]]


\begin{lemma}
\label{ts_affects_unrelated}
Let $\beta$ be a simple-pseudotime behavior
and let $R = \ms{pseudotime-order}(\beta)$.
Let $\pi$ and $\pi'$ be distinct events in $\ms{serial}(\beta)$ 
with lowtransactions $T$ and $T'$ respectively.
If $T$ is neither an ancestor nor a descendant of $T'$, 
and $(\pi,\pi') \in \ms{affects}(\ms{serial}(\beta))$,
then $(\pi,\pi') \in R_{\ms{event}}(\ms{serial}(\beta))$.
\end{lemma}

\begin{proof}
Since $T$ is neither an ancestor nor a descendant of $T'$, 
there must be siblings $U$ and $U'$ such that
$T$ is a descendant of $U$, and $T'$ is a descendant of $U'$.  
Let $U''$  denote $\ms{parent}(U) =\ms{parent}(U') = \ms{lca}(T,T')$.
By Lemma \ref{ts_pseudotime_assigned}, $\beta$ contains events
\ASPS{U}{P} and \ASPS{U'}{P'}.

By Lemmas \ref{gt_affects_limited_completion} and 
\ref{gt_affects_limited_create},
there must be events $\phi$ and $\phi'$ in $\ms{serial}(\beta)$ such that
$\phi$ is a report
event for $U, \phi'$ is \RQCR{U'}, and
$(\pi,\phi), (\phi,\phi'), \rms{and}\ (\phi',\pi')$ are all in 
$\ms{affects}(\ms{serial}(\beta))$.
Thus, $\phi$ occurs before $\phi'$ in $\beta$.
The preconditions of the simple-pseudotime database
ensure that $\phi$ is preceded by a completion event for $U$,
and Lemma \ref{ts_pseudotime_assigned} shows that this
is preceded by an \ASPS{U}{P} event.
The simple-pseudotime database
preconditions ensure that \ASPS{U'}{P'}
follows $\phi'$.
Thus the \ASPS{U}{P} event precedes the \ASPS{U'}{P'} event.
By Lemma \ref{ts_simple-pseudotime_database_schedules_2}, $P < P'$.
Thus $(U,U') \in R$.
The result follows.
\end{proof}

We now show that the two partial orders
defined on the events of $\ms{serial}(\beta)$ are consistent.


\begin{lemma}
\label{ts_pseudotime_order_1}
Let $\beta$ be a simple-pseudotime behavior,
and let $R = \ms{pseudotime-order}(\beta)$.
Then $R_{\ms{event}}(\ms{serial}(\beta))$ 
and $\ms{affects}(\ms{serial}(\beta))$ are
consistent partial orders on the events in 
%[[[
$\ms{serial}(\beta)$.
%]]]
\end{lemma}

\begin{proof}
This is immediate by Lemmas \ref{ts_affects_unrelated} and
\ref{gt_order_affects_consistent}.
\end{proof}

\begin{lemma}
\label{ts_pseudotime_total}
Let $\beta$ be a simple-pseudotime behavior and $T$ a transaction name.
If $T$ and $T'$ are siblings that are lowtransactions of actions 
in $\ms{serial}(\beta)$, then either $(T,T')$ or $(T',T) \in 
\ms{pseudotime-order}(\beta)$.
\end{lemma}

\begin{proof}
By Lemmas \ref{ts_pseudotime_assigned} and \ref{ts_simple-pseudotime_database_schedules_2}.
\end{proof}

Now one can conclude that the pseudotime order is suitable.

\begin{lemma}
\label{ts_pseudotime_order_suitable}
Let $\beta$ be a simple-pseudotime behavior and $T$ a transaction name.
Then $\ms{pseudotime-order}(\beta)$ is suitable for $\ms{serial}(\beta)$ 
and $T$.
\end{lemma}

\begin{proof}
By Lemmas \ref{ts_pseudotime_total} and \ref{ts_pseudotime_order_1}.
\end{proof}
				   
The following variant of Corollary \ref{gt_serializability_corollary}
to the Atomicity Theorem
applies to the special case where $R$ is the pseudotime
order and the system is a simple-pseudotime system.

\begin{proposition}
\label{ts_main_simple}
Let $\beta$ be a finite simple-pseudotime behavior,
$T$ a transaction name such that $T$ is not an orphan in $\beta$,
and let $R = \ms{pseudotime-order}(\beta)$.
Suppose that for each object name $X$,
$\ms{view}(\ms{serial}(\beta),T,R,X)$ is a behavior of $S_X$.
Then $\beta$ is atomic for $T$.
\end{proposition}

\begin{proof}
Proposition \ref{ts_simple-pseudotime_simple} implies that $\ms{serial}(\beta)$ is 
a simple behavior, 
and Lemma \ref{ts_pseudotime_order_suitable} implies that $R$ is suitable for
$\ms{serial}(\beta)$ and $T$.
The result is immediate from Corollary \ref{gt_serializability_corollary}.
\end{proof}

%[[[A 11/91
\begin{example}{Atomicity In A Message Queue System}
Let  $\beta$ be the sequence given in Example \ref{ts-queue-system-ex1}.
We leave 
the calculation of $\ms{view}(\ms{serial}(\beta),T_0,R,X)$, where 
$R = \ms{pseudotime-order}(\beta)$, as Exercise \ref{ts-queue-exercise1}.
The reader is invited to check that $\beta$ is atomic for $T_0$.
\end{example}
%]]]

\subsection{Pseudotime Systems}
\label{ts_pseudotime-systems}

This subsection defines the system decomposition appropriate 
for describing many timestamp-based algorithms.
Analagous to the {\em generic systems} used for modelling
locking algorithms, these algorithms
are formulated as 
%[[[A 7/91
objects in
%]]]
{\em pseudotime systems}.
These systems are composed of transaction automata,
{\em pseudotime object automata} and a {\em pseudotime controller}.
The general structure of the system is the same as that given in Figure 
\ref{serial_system_structure} for serial systems.

A separate {\em pseudotime object} automaton for
each object name handles the concurrency control and data for
that object in an as-yet unspecified way, using information about
pseudotimes of accesses and the fates of transactions.
The {\em pseudotime controller} assigns pseudotime intervals and passes 
requests and information around the system.

\subsubsection{Pseudotime Object Automata}

A \df{pseudotime object automaton} $P_X$ for an
object name $X$ of a given system
type is an automaton with the following external action signature.

\io{%%Input:
    \CRT{T}, for $T$ an access to $X$\\
    \INFCMntab{X}{T}, for $T \neq T_{0}$\\
    \INFABntab{X}{T}, for $T \neq T_{0}$\\
    \INFTMntab{X}{T,p}, for $T \in \ms{accesses}(X), p \in \cal P$}
{%%Output:
    \RQCMntab{T}{v}, for $T$ and access to $X$ and $v$ a value for $T$}

In addition, $P_X$ may have an arbitrary set of internal actions.

The actions \CRT{T} and \RQCM{T}{v} correspond to invocations
of accesses and responses to accesses, 
just as for a serial object $S_X$. 
In addition,
a pseudotime object has input actions that correspond to the
receipt of information about the commit or abort of a transaction, and
about the pseudotime\footnote{We have made the decision to transfer
to an object only a single pseudotime for each access,
rather than a whole interval. Similarly, our model
does not include any transfer of information
about the intervals assigned to non-access transactions,
except what can be inferred from the
pseudotimes of their descendant accesses. These decisions were
made for convenience. 
The entire development of this chapter could have been done differently,
with only minor changes in proofs.}
%[[[A 7/91 footnote added]]]
assigned to an access transaction.

A pseudotime object automaton
$P_X$ is required to preserve {\em pseudotime object well-formedness},
defined as follows.
A sequence $\beta$ of actions $\pi$ in the external signature of $P_X$
is said to be \df{pseudotime object well-formed} for $X$ provided that the
following conditions hold. 
%[[[A 7/91
These conditions are similar to those used to define generic object well-formedness,
in Section \ref{generic-system-section}. The additional conditions
constrain the object not to
respond to an access until the pseudotime is known,
and also constrain the environment not to
provide contradictory information about pseudotimes.\footnote{We remark that 
there are other conditions that will be true in every behavior in a 
pseudotime system; for example, that for
any transaction, the pseudotimes known for its descendants will
not be separated from one another by the pseudotime  known for an access
that is not a descendant. The conditions listed here are a straightforward 
collection that have been adequate for our purposes, by simplifying
local reasoning for the algorithms chosen.}
%]]]

\begin{enumerate}
\item There is at most one \CRT{T} event in $\beta$ for any access $T$.

\item There is at most one \rqcm{} event in $\beta$ for any access $T$.

\item If there is a \rqcm{} event for an access
$T$ in $\beta$, then there is a
preceding \CRT{T} in $\beta$ 
and also a preceding \INFTM{X}{T,p} event, for some pseudotime $p$.

\item There is no access $T$ for which there are two different pseudotimes, $p$
and $p'$, such that \INFTM{X}{T,p} and \INFTM{X}{T,p'} both
occur in $\beta$.

\item There is no pseudotime $p$ for which there are two different accesses, $T$
and $T'$, such that \INFTM{X}{T,p} and \INFTM{X}{T',p} both
occur in $\beta$.

\item There is no transaction $T$ for which both an \INFCM{X}{T}
and an \INFAB{X}{T} event occur in $\beta$.

\item If an \INFCM{X}{T} event occurs in $\beta$ and $T$ is an access to $X$, 
then there is a preceding \rqcm{} event for $T$.
\end{enumerate}

As with previous well-formedness properties, there is an alternative form of the
definition.

\begin{lemma}
\label{ts_pseudotime_object_wellformed}
A sequence $\beta$ of actions in the external signature of
a pseudotime object for object name $X$ is
pseudotime object well-formed for $X$ exactly if 
for every finite prefix $\gamma\pi$ of $\beta$, where $\pi$ is a single
action, the following conditions hold.

\begin{enumerate}
\item If $\pi$ is \CRT{T}, then
\begin{enumerate}
\item there is no \crt{} event for $T$ in $\gamma$.
\end{enumerate}

\item If $\pi$ is \INFCM{X}{T}, then
\begin{enumerate}
\item if $T$ is an access to $X$, then there is a \rqcm{} for $T$ in $\gamma$, and

\item there is no \INFAB{X}{T} in $\gamma$.
\end{enumerate}

\item If $\pi$ is \INFAB{X}{T}, then
\begin{enumerate}
\item there is no \INFCM{X}{T} in $\gamma$.
\end{enumerate}

\item If $\pi$ is \INFTM{X}{T,p}, then
\begin{enumerate}
\item there is no \INFTM{X}{T',p} event in $\gamma$, 
where $T \neq T'$ , and

\item there is no \INFTM{X}{T,p'} event in $\gamma$, 
where $p \neq p'$.
\end{enumerate}

\item If $\pi$ is \RQCM{T}{v}, then
\begin{enumerate}
\item there is a \CRT{T} in $\gamma$,

\item there is no \rqcm{} for $T$ in $\gamma$, and

\item there is an \INFTM{X}{T,p} in $\gamma$ for some $p$.
\end{enumerate}
\end{enumerate}
\end{lemma}

\subsubsection{Pseudotime Controller}
\label{timestamps_pseudotime_controller_section}

There is a single pseudotime controller for each system type.
As with the generic controller of Chapter \ref{locking_chapter},
the pseudotime controller
passes requests
for the creation of subtransactions to the appropriate recipient,
makes decisions about the commit or abort of transactions,
passes reports about the completion of children back to their parents,
and informs objects of the fate of transactions.
In addition to these functions of the generic
controller, the pseudotime controller assigns
pseudotime intervals to transactions and informs objects
of the pseudotimes of relevant accesses.
Again like the generic controller, and 
unlike the serial scheduler, it does not prevent sibling transactions
from being live simultaneously,
nor does it prevent the same transaction
from being both created and aborted.
Rather, it leaves the task of coping with concurrency and recovery to
the pseudotime objects.

The pseudotime controller has the following action signature.

\io{%%Input:
    \RQCRntab{T}, $T \neq T_{0}$\\
    \RQCMntab{T}{v}, $v$ a value for $T$}
{%%Output:
    \ASPSntab{T}{P}, $P$ a pseudotime interval, $T \neq T_{0}$\\
    \CRT{T} \\
    \CM{T}, $T \neq T_{0}$\\
    \AB{T}, $T \neq T_{0}$\\
    \RPCMntab{T}{v}, $T \neq T_{0}$, $v$ a value for $T$\\
    \RPABntab{T}, $T \neq T_{0}$\\
    \INFCMntab{X}{T}, $T \neq T_{0}$\\
    \INFABntab{X}{T}, $T \neq T_{0}$\\
    \INFTMntab{X}{T,p}, $T$ an access to $X$}

A state $s$ of the pseudotime controller has the same components as that
of the pseudotime database, with the same initialization.
The actions of the pseudotime controller are the same as the corresponding
actions of the pseudotime database, except for \rqcm{} and \infr{}
actions.\footnote{Notice that for accesses, \rqcm{} actions
are {\em outputs} of the pseudotime database, but they
are {\em inputs} to the pseudotime controller,
just as they are outputs of the simple database, but 
inputs to the generic controller.
These actions are outputs of the object automata.}
For those actions, the transition relation is as follows.

\iocode{
\ef{\RQCMntab{T}{v}}
{%%Effect:
     $\ms{s.commit-requested}$\\ \> $= \ms{s'.commit-requested} \cup \{(T,v)\}$}

\prc{\INFCMntab{X}{T}}
{%%Precondition:
     $T \in \ms{s'.committed}$}
}{
\prc{\INFABntab{X}{T}}
{%%Precondition:
     $T \in \ms{s'.aborted}$}

\prc{\INFTMntab{X}{T,p}}
{%%Precondition:
     $(T,P) \in \ms{s'.interval}$\\
     $p = P_{\ms{min}}$}
}

Except for the new \inftm{} action, the actions are also the same
as the corresponding actions of the generic controller.
%[[[A 7/91
Notice that the \inftm{} events only provide the
lowest pseudotime within the assigned interval, and this
information is only given to the object to which the transaction is an access.
%]]]

\subsubsection{Basic Properties of the Pseudotime Controller}
The following simple lemmas are analogous to those given for
the generic controller and the simple-pseudotime database.
The first relates a schedule of the
pseudotime controller to the resulting states,
and second gives some simple properties
of schedules of the pseudotime controller.

\begin{lemma}
%[[[A 7/91 check for consistency with similar lemmas]]]
\label{ts_controller_schedules_1}
If $\beta$ is a finite schedule of the pseudotime controller
that can lead to state $s$,
then the following conditions are true.
\begin{enumerate}
\item $T$ is in $\ms{s.create\_requested}$ if and only if
either $T = T_{0}$ or $\beta$ contains a \RQCR{T} event.

\item $T$ is in $\ms{s.created}$ if and only if
$\beta$ contains a \CRT{T} event.

%[[[A 7/91
\item
\label{ts_cond_spec1}
$(T,P)$ is in $\ms{s.interval}$ if and only if
either $(T,P) = (T_0, P_0)$ or $\beta$ contains
an \ASPS{T}{P} event.
%]]]

\item $(T,v)$ is in $\ms{s.commit\_requested}$ if and only if
$\beta$ contains a \RQCM{T}{v} event.

\item $T$ is in $\ms{s.committed}$ if and only if $\beta$ contains a \CM{T} event.

\item $T$ is in $\ms{s.aborted}$ if and only if $\beta$ contains an \AB{T} event.

\item $T$ is in $\ms{s.reported}$ if and only if $\beta$ contains a report event for $T$.

\item $\ms{s.committed} \cap \ms{s.aborted} = \emptyset$.

\item $\ms{s.reported} \subseteq \ms{s.committed} \cup \ms{s.aborted}$.

%[[[
\item
\label{ts_cond_spec2}
if $T$ and $T'$ are sibling transactions in $\ms{domain}(\ms{s.interval})$,
then $\ms{s.interval}(T)$ is disjoint from $\ms{s.interval}(T')$.

\item
\label{ts_cond_spec3}
if $T$ is in $\ms{domain}(\ms{s.interval})$,
then $\ms{parent}(T)$ is in  $\ms{domain}(\ms{s.interval})$, and
$\ms{s.interval}(T) \subseteq \ms{s.interval}(\ms{parent}(T))$.
%]]]

\end{enumerate}
\end{lemma}

\begin{lemma}
\label{ts_controller_schedules_2}
Let $\beta$ be a %finite [[[M: 1/91]]]
schedule of the pseudotime controller.
Then all of the following hold:
%[[[added ``for $T \neq T_0$,''  below. M:1/91]]]
\begin{enumerate}
\item If an \ASPS{T}{P} event appears in $\beta$, for $T \neq T_0$,
then a \rqcr{} event for $T$ precedes it in $\beta$.

\item If a \CRT{T} event appears in $\beta$, for $T \neq T_0$, 
then an \asps{} event for $T$ precedes it in $\beta$.

\item If an \AB{T} event appears in $\beta$, then an
\asps{} event for $T$ precedes it in $\beta$.

\item If an \asps{} event for $T$ appears in $\beta$, and
$\ms{parent}(T) \neq T_{0}$, then an \asps{} event
for $\ms{parent}(T)$ precedes it in $\beta$.

\item At most one \asps{} event appears in $\beta$ for each
transaction.

\item If $T$ and $T'$ are sibling transactions, and \ASPS{T}{P} precedes \ASPS{T'}{P'} 
in $\beta$, then $P < P'$.

\item $T \in \ms{s.interval}$ if and only if $T = T_{0}$ or if an \asps{}
event for $T$ appears in $\beta$.

\item If $T \in \ms{domain}(\ms{s.interval})$ and $T$ is a descendant of $T'$,
then $T' \in \ms{domain}(\ms{s.interval})$ and $\ms{s.interval}(T) \subseteq
\ms{s.interval}(T')$.

\item If an \INFCM{X}{T} event appears in $\beta$, 
then a \cm{} event for $T$ precedes it in $\beta$.

\item If an \INFAB{X}{T} event appears in $\beta$, then 
an \ab{} event for $T$ precedes it in $\beta$.

\item If an \INFTM{X}{T,p} event appears in $\beta$, then
an 
\ASPS{T}{P} event appears in $\beta$ with
$p = P_{\ms{min}}$.

\end{enumerate}
\end{lemma}


\subsubsection{Pseudotime Systems}

A \df{pseudotime system} is the composition of a set of
automata indexed by the union of the set of non-access transaction names,
the set of object names, and the singleton set $\ms{PC}$
(for {\em pseudotime controller}).
Associated with each non-access transaction name $T$ is a transaction
automaton $A_{T}$ for $T$.
Associated with each object name $X$ is a pseudotime object automaton $P_X$.
Also, associated with the name $\ms{PC}$ is the pseudotime controller for the
given system type.

The external actions of a pseudotime system are called
\df{pseudotime actions},
and the executions, schedules and behaviors of a pseudotime system are
called \df{pseudotime executions},
\df{pseudotime schedules} and \df{pseudotime behaviors}, 
respectively.

If $\beta$ is a sequence of external actions of a  
pseudotime system, then
define $\ms{pseudo}(\beta)$ by removing from $\beta$ all \infr{} actions.
\index{pseudo($\beta$)}

Since the pseudotime controller, the transaction automata 
and each pseudotime object automaton all
preserve transaction and pseudotime object well-formedness, 
we have the following result.

\begin{proposition}
\label{ts_behavior_well-formed}
If $\beta$ is a pseudotime behavior, 
then the following conditions hold.
\begin{enumerate}
\item For every transaction name $T$, $\beta|T$ is transaction well-formed for $T$.

\item For every object name $X$, $\beta|P_X$ is pseudotime object well-formed for $X$.
\end{enumerate}
\end{proposition}

The following captures the relationship between a 
pseudotime system and the simple-pseudotime system.

\begin{proposition}
\label{ts_pseudotime_simple-pseudotime}
If $\beta$ is a  pseudotime behavior, then
$\ms{pseudo}(\beta)$ is a pseudotime behavior and
$\ms{pseudo}(\beta)|T = \beta|T$ for all transaction names $T$.
\end{proposition}

%[[[This lemma is no longer needed if Alan's new proof of
%\ref{ts_main_distributed} is used.  I've commented both
%this lemma and the old proof out in case Bill or Nancy want
%to check it out.  M 8/8/90
%[[[I vote to omit the following lemma completely -A]]]
%\begin{lemma}
%\label{ts_d_pseudotime_order_suitable}
%Let $\beta$ be a finite distributed pseudotime behavior and $T$ a transaction name.
%Then $\ms{pseudotime-order}(\beta)$ is suitable for $\ms{serial}(\beta)$ and $T$.
%\end{lemma}]]]
%\begin{proof}
%By Lemmas \ref{ts_pseudotime_order_suitable} and 
%\ref{ts_distributed-pseudotime_pseudotime}.
%\end{proof}

The earlier results on simple-pseudotime behaviors can now
be applied to obtain a sufficient condition 
for proving the atomicity of a pseudotime behavior.

\begin{proposition}
\label{ts_main}
Let $\beta$ be a finite  pseudotime behavior,
$T$ a transaction name such that $T$ is not an orphan in $\beta$,
and let $R = \ms{pseudotime-order}(\beta)$.
Suppose that for each object name $X$,
$\ms{view}(\ms{serial}(\beta),T,R,X)$ is a behavior of $S_X$.
Then $\beta$ is atomic for $T$.
\end{proposition}

\begin{proof}
By Propositions \ref{ts_main_simple} and \ref{ts_pseudotime_simple-pseudotime}.
%[[[old proof:
%By Proposition \ref{ts_distributed-pseudotime_pseudotime},
%$\ms{pseudo}(\beta)$ is a pseudotime behavior and hence
%by Proposition \ref{ts_pseudotime_simple}, $\ms{serial}(\beta)$ is a simple behavior.
%Lemma \ref{ts_d_pseudotime_order_suitable} implies that $R$ is suitable for
%$\ms{serial}(\beta)$ and $T$.
%The result is immediate from Corollary \ref{gt_serializability_corollary}.]]]
\end{proof}

\subsection{Static Atomicity}
\label{ts_static-atomicity}

When designing a distributed database management system,
the choice of concurrency control and recovery
algorithms should guarantee the atomicity of all
the finite behaviors of the system.  Also, it is advantageous
to consider the algorithm used in implementing one object
without reasoning about the implementations of all the other objects.
Thus, one is lead to define the local property of {\em static atomicity}.
%[[[A 7/91
Like dynamic atomicity, this is a property that can be
checked for each object separately. A static atomic object is one
that uses the order of accesses' pseudotimes to serilize them.\footnote{The 
name reflects the idea that the position
of a transaction in the serialization order is that of the pseudotime 
interval, and this is determined earlier in an execution than the 
completion order used in dynamic atomicity; 
in particular, it is not influenced by the activity of the transaction
itself.}
%]]]

Let $P_X$ be a pseudotime object automaton for object name $X$.
Say that $P_X$ is \df{static atomic} for a given system type
if for all pseudotime systems $\cal S$ of the given type
in which $P_X$ is associated with $X$,
the following is true.
Let $\beta$ be a finite behavior of $\cal S$, 
$R = \ms{pseudotime-order}(\beta)$ and
$T$ a transaction name that is not an orphan in $\beta$.
Then $\ms{view}(\ms{serial}(\beta),T,R,X)$ is a behavior of $S_X$.

\begin{theorem}
\label{static-atomic_serially-correct}
(Static Atomicity Theorem)
Let $\cal S$ be a  pseudotime system in which all pseudotime objects are
static atomic.
Let $\beta$ be a finite behavior of $\cal S$.
Then $\beta$ is atomic for every non-orphan transaction name.
\end{theorem}

\begin{proof}
Immediate from Proposition \ref{ts_main}
and the definition of static atomicity.
\end{proof}

\subsection{Local Static Atomicity}
\label{ts_local-static-atomicity}

This subsection defines another property of pseudotime object automata 
called {\em local static atomicity}, which is a convenient 
sufficient condition for showing static atomicity.
For each pseudotime object automaton $P$, static atomicity is a local
condition in that it only depends on $P$.
However, the form in which the condition is stated may be difficult to
check directly: one must be able to verify a condition involving
$\ms{view}(\ms{serial}(\beta),T,\ms{pseudotime-order}(\beta),X)$ for all
finite behaviors $\beta$ of all  pseudotime systems containing $P$.
Local static atomicity is defined more
directly in terms of the behaviors of $P$.
(This parallels the development in Chapter \ref{locking-chapter},
where local dynamic atomicity is used to prove dynamic atomicity.)

First some terms are introduced to describe information 
about the status of transactions
that is deducible from the behavior of a particular  pseudotime object.
Let $P_X$ be a pseudotime object automaton for $X$,
$\beta$ a sequence of external actions of $P_X$,
and  $T$ and $T'$ transaction names.
Then $T$ is \df{locally visible at $X$} to $T'$  in $\beta$ 
if $\beta$ contains an \INFCM{X}{U} event for every $U$ in
$\ms{ancestors}(T) - \ms{ancestors}(T')$.
Also, $T$ is a \df{local orphan at $X$} in $\beta$ if $\beta$ contains an
\INFAB{X}{U} event for some ancestor $U$ of $T$.
These definitions are essentially the same as the corresponding definitions
in Section \ref{locking_local_defs_section}.\footnote{The 
only difference is in
the signatures of the objects, and therefore in the types
of actions that appear in the sequences considered.}
%[[[A 7/91 footnote added]]]

%[[[A 7/91
We have results analogous to those in Section
\ref{locking_local_defs_section}.
%]]]

\begin{lemma}
\label{ts_vis_atX_trans}
Let $P_X$ be a pseudotime object automaton for $X$.
Let $\beta$ be a sequence of external actions of $P_X$, 
and let $T, T'$  and $T''$ be transaction names. 
If $T$ is locally visible at $X$ to $T'$  in $\beta$, 
and $T'$  is locally visible at $X$ to $T''$ in $\beta$, 
then $T$ is locally visible at $X$ to $T''$ in $\beta$.
\end{lemma}

%[[[I made the lemma positive.  N. 5/91]]]

\begin{lemma}
\label{ts_local_visibility_nonorphaness}
Let $P_X$ be a pseudotime object automaton for $X$.
Let $\beta$ be a pseudotime object well-formed sequence of external actions of 
$P_X$, 
and let $T$ and $T'$ be transaction names. 
If $T$ is locally visible at $X$ to $T'$ in $\beta$, and
$T$ is a local orphan at $X$ in $\beta$, 
then $T'$ is a local orphan at $X$ in $\beta$.
\end{lemma}

The names introduced above are justified by the relationships between
the local properties defined above
and the corresponding global properties. 
%[[[A 7/91
This shows that the definitions express
safe deductions from local information.
%]]]

\begin{lemma}
\label{ts-visible-at-X-visible-relate}
Let $\beta$ be a behavior of a  pseudotime system in which 
pseudotime object automaton $P_X$ is associated with $X$.
If $T$ is locally visible at $X$ to $T'$ in $\beta|P_X$,
then $T$ is visible to $T'$ in $\beta$.
Similarly, if $T$ is a local orphan at $X$ in $\beta|P_X$
then $T$ is an orphan in $\beta$. 
\end{lemma}

\begin{proof}
These are immediate consequences of the pseudotime controller preconditions,
which imply that any \INFCM{X}{T} event in $\beta$
must be preceded by an \CM{T} event
and that any \INFAB{X}{T} is preceded by \AB{T}.
\end{proof}

Next, a relation on accesses to $X$ is defined to describe
information about the pseudotime order
that is deducible from the behavior of $P_X$.
Given a sequence $\beta$ of external actions of $P_X$,
define a binary relation \df{$\ms{local-pseudotime-order}(\beta)$} 
on accesses to $X$,
where $(U,U') \in \ms{local-pseudotime-order}(\beta)$ 
exactly when $\beta$ contains both \INFTM{X}{U,p} and
\INFTM{X}{U',p'} events for some $p$ and $p'$ with $p < p'$.
%[[[A 7/91
The reader should note that unlike $\ms{pseudotime-order}$, this
definition relates access to $X$ rather than siblings. Also,
unlike the $\ms{local-completion}$ order of Section
\ref{locking_local_defs_section}, $\ms{local-pseudotime-order}$
relates every pair of distinct accesses for which
operations occur.
%]]]

\begin{lemma}
\label{ts_orders-all}
If $\beta$ is a pseudotime object well-formed sequence of external
actions of pseudotime object automaton for $X$,
then $\ms{local-pseudotime-order}(\beta)$ is an irreflexive
total order on accesses to $X$ 
having \rqcm{} actions in $\beta$.
\end{lemma}

The relationship between the local-pseudotime-order and the global 
pseudotime-order in a  pseudotime system is as follows.
%[[[A 7/91
The reader should notice that this result is much stronger than
the corresponding Lemma \ref{locking_order_at_X_order_relate}.
In particular, the local information is a correct reflection
of the global pseudotime-order, even for orphans.
%]]]

\begin{lemma}
\label{ts-order-at-X-order-relate}
Let $\beta$ be a behavior of a 
pseudotime system in which pseudotime
object automaton $P_X$ is associated with $X$.
Let $R = \ms{pseudotime-order}(\beta)$ and
$R' = \ms{local-pseudotime-order}(\beta|P_X)$.
Then the following are true.
\begin{enumerate}
\item $R' = R'_{trans} \subseteq R_{trans}$.

\item $R'_{event}(\beta|P_X) \subseteq R_{event}(\beta)$.
\end{enumerate}
\end{lemma}

\begin{proof}
The equality $R' = R'_{trans}$ 
is immediate, since $R'$ is a relation on accesses. To show the inclusion
$R' \subseteq R_{trans}$, suppose $(T,T') \in R'$. Then
$\beta$ contains \INFTM{X}{T,p} and \INFTM{X}{T',p'} events
with $p < p'$. By the pseudotime controller preconditions,
there are pseudotime intervals $P$ and $P'$ such that
$\beta$ contains \ASPS{T}{P} and \ASPS{T'}{P'}, and $p = P_{min}$ and
$p' = P'_{min}$. Now let $U$ and $U'$ be siblings that
are ancestors of $T$ and $T'$ respectively. Lemma
\ref{ts_controller_schedules_2} shows that $\beta$ contains
\ASPS{U}{Q} and \ASPS{U'}{Q'} events, with $Q$ and $Q'$ such that
$P \subseteq Q$ and $P' \subseteq Q'$. Since $Q$ and $Q'$ are disjoint
and $p < p'$ with $p \in Q$ and $p' \in Q'$, if follows that $Q < Q'$.
Thus $(U,U') \in R$ and so $(T,T') \in R_{trans}$. 

The inclusion of $R'_{event}(\beta|P_X)$ in $R_{event}(\beta)$ follows
immediately.
\end{proof}

Now we give a definition to describe how to reorder the external
actions of a pseudotime object automaton according to a given local-pseudotime
order.
%[[[A 7/91
This definition is similar to that used to define the view condition
that is given in Theorem \ref{ts_main}, except that it
uses local approximations rather than the global facts like
visibility and the pseudotime order.
%]]]
Suppose $\beta$ is a finite
pseudotime object well-formed sequence of external 
actions of a pseudotime object automaton for $X$ and $T$ is a transaction name.
Let $\ms{local-view}(\beta,T)$ be the unique sequence
\index{local-view($\beta,T$)}
defined as follows.
Let $Z$ be the set of operations occurring in  
$\beta$ whose transactions are locally visible at $X$
to $T$ in $\beta$.
Then $\ms{local-view}(\beta,T) = \ms{perform}(\xi)$, where $\xi$ is the 
result of reordering $Z$ according to the order 
$\ms{local-pseudotime-order}(\beta)$ on the transaction components.
(Note that Lemma \ref{ts_orders-all} implies that this reordering
is unique.)
The following is straightforward from the definitions.

\begin{lemma}
If $\beta$ is a finite pseudotime object well-formed 
sequence of external actions
of pseudotime object automaton $P_X$, 
and $T$ is a transaction name,
then $\ms{local-view}(\beta,T)$ is serial object well-formed.
\end{lemma}

Finally, {\em local static atomicity} can be defined.
%[[[A 7/91
This is defined like static atomicity, but using the local
approximations to visibility, the pseudotime
order and so on.
%]]
Say that pseudotime object automaton $P_X$ for object name $X$
is \df{locally static atomic}
if whenever $\beta$ is a finite
pseudotime object well-formed behavior of $P_X$, 
and $T$ is a transaction name
that is not a local orphan at $X$ in $\beta$,
then $\ms{local-view}(\beta,T)$ is a behavior of $S_X$. 
That is, the result of reordering a behavior of $P_X$ according to the
given local-pseudotime order is a finite behavior of the corresponding
serial object automaton.

The main result of this subsection says
that local static atomicity is a sufficient condition 
for static atomicity.

\begin{theorem}
\label{ts_local_static_implies_static}
If $P_X$ is a pseudotime object automaton for object name $X$
that is locally static atomic
then $P_X$ is static atomic.
\end{theorem}

\begin{proof}
Let $\cal S$ be a  pseudotime system in which $P_X$ is
associated with $X$.
Let $\beta$ be a finite behavior of $\cal S$,
$R = \ms{pseudotime-order}(\beta)$ 
and $T$ a transaction name that is not an orphan in $\beta$. 
The proof must establish
that $\ms{view}(\ms{serial}(\beta),T,R,X)$ is a behavior of $S_X$.
By definition, $\ms{view}(\ms{serial}(\beta),T,R,X) = \ms{perform}(\xi)$, where $\xi$
is the sequence of operations occurring in $\beta$
whose transactions are visible to $T$ in $\beta$,
arranged in the order given by $R_{trans}$ on the transaction component.

\sloppy
Let $\gamma$ be a finite sequence of actions consisting of exactly one
\INFCM{X}{U} for each \CM{U} that occurs in $\beta$. 
Then $\beta\gamma$ is a behavior of the system $\cal S$, 
since each action in $\gamma$ is an enabled output of the pseudotime controller,
by Lemma \ref{ts_controller_schedules_1}.
Then $\beta\gamma|P_X$ is a behavior of $P_X$, and
Proposition \ref{ts_behavior_well-formed} implies that it is
pseudotime object well-formed.
\fussy

Since \INFCM{X}{U} occurs in $\beta\gamma|P_X$
if and only if \CM{U} occurs in $\beta$, 
an access $T'$ to $X$ is visible to $T$ in $\beta$ if and only if it is
locally visible at $X$ to $T$ in $\beta\gamma|P_X$. 
Also, $R = \ms{pseudotime-order}(\beta) = 
\ms{pseudotime-order}(\beta\gamma)$.
Moreover, Lemma \ref{ts-order-at-X-order-relate} implies
that if accesses are ordered by 
$\ms{local-pseudotime-order}(\beta\gamma|P_X)$  
they are also ordered in the same way by $R_{trans}$.

Comparing the definitions of $\ms{view}(\ms{serial}(\beta),T,R,X)$ and
$\ms{local-view}(\beta\gamma|P_X,T)$,
one sees the correspondences given above imply that they are the same.
Since $T$ is not an orphan in $\beta$, 
it is not an orphan in $\beta\gamma$,
and thus not a local orphan in $\beta\gamma|P_X$.
Since $P_X$ is locally static atomic,
$\ms{local-view}(\beta\gamma|P_X,T)$ 
is a behavior of $S_X$. That is,
$\ms{view}(\ms{serial}(\beta),T,R,X)$ 
is a behavior of  $S_X$, as required to satisfy the definition of
static atomicity.
\end{proof} 

\section{Reed's Algorithm}
\label{reed-alg--section}

This section formally describes a
multi-version timestamp-based algorithm that is based on one
proposed by Reed \cite{Reed78}.
%[[[A 7/91
The algorithm works for object names where the serial specification
is a read/write serial object, as defined in Example
\ref{read-write-serial-object}.

Here is an informal sketch of Reed's algorithm.
The system keeps a separate {\em version} (containing the value written)
for each write access
that has occurred. Each version whose writer is not
an orphan is
regarded as being the {\em effective} version for an interval of
pseudotime, starting at the pseudotime assigned to the
write access that produced the version, and extending
to the highest pseudotime assigned to any non-orphan read access
that returned the version.\footnote{If no read has yet returned the value
from a version written by a non-orphan, that version 
is effective at a single pseudotime -- the one assigned
to the writer.}
The effective intervals of different
versions must be disjoint, and each read access
must return the version that is effective at the pseudotime 
assigned to the reader. To ensure that these key properties are maintained,
a write access
is prevented from occurring if there is already
an effective version at the pseudotime assigned to the writer.
A read access returns the version 
written by the non-orphan write access 
whose pseudotime most closely precedes the time assigned to the reader;
however the read must not return unless the writer involved 
is visible to it.\footnote{This ensures that the writer cannot become an 
orphan except when the reader also becomes an orphan.}
%]]]

Below, we present an abstract form of the algorithm as a pseudotime object
automaton; this is shown
to be a locally static atomic object.
Then correctness of a more concrete algorithm, closer to Reed's original proposal,
is discussed.

\subsection{Reed Objects}
\label{ts_read-write_section}

A pseudotime object automaton $R_X$ (a {\em Reed object})
is described, for 
%[[[
any object name $X$ where $S_X$ is a read/write serial object.
%A 5/91]]]
The automaton $R_X$ maintains
%[[[
multiple versions of data,
%A 5/91]]]
the names of the readers and writers of each version,
and their corresponding timestamps.

%[[[A 7/91 moved from above
Recall from
Example
\ref{read-write-serial-object}
that for a read/write serial object there is a domain $D$ of values, an initial
value $d_0$, a function $\ms{kind}$ which indicates whether an access is
reading or writing, and a function $\ms{data}$ which indicates the value
to which each write access sets the serial object.
%]]]

%[[[I deleted a paragraph concerning permissible classifications A 5/91]]]

Let $T_X$ be a {\em dummy} transaction name (a name not in {$\cal T$}),
regarded as the writer of the 
%[[[
initial version.
%A 5/91]]]
Also  let
$-\infty$ be a {\em dummy} pseudotime (not in $\cal P$) that
is regarded as being less
than any pseudotime in $\cal P$ and is used to represent the time at 
which the initial version of $S_X$ is written.

Each state $s$ of $R_X$  has the following components:
$\ms{s.created}$, $\ms{s.committed}$, $\ms{s.aborted}$, $\ms{s.commit-requested}$,
$\ms{s.time}$, $\ms{s.version}$ and $\ms{s.reads-from}$.
%[[[A 7/91
The components
$\ms{s.created}$ and $\ms{s.commit-requested}$,
which are sets of accesses to $X$, record the occurrence of
the appropriate actions. Thus the active accesses in any state $s$
are those in $\ms{s.created} - \ms{s.commit-requested}$.
The components $\ms{s.committed}$ and $\ms{s.aborted}$ are
sets of transactions, that record
the information received about the outcome of transactions; this information
is kept for all transactions, not only for accesses.
The component $\ms{s.time}$ is
a partial function from $\ms{accesses}(X) \cup \{T_X\}$ to $\cal P$
$\cup \{-\infty\}$. The fact that $\ms{s.time}(T)=p$ reflects
the knowledge at the object that the pseudotime assigned to the
access $T$ is $p$; we will see that $\ms{s.time}(T_X)= -\infty$
since the initial version is regarded as written by $T_X$ before
any genuine pseudotime.
The component $\ms{s.version}$ is a partial mapping from 
\{$T$: $T$ is a write accesses to $X$\} $\cup \{T_X\}$ to 
$D$, the domain of values of $S_X$. The fact that $\ms{s.version}(T) = d$
%[[[A 11/91
(equivalently,\footnote{Recall from mathematics that a partial function, like any relation,
can be treated as a set of pairs.}
that $(T,d) \in s.\ms{version}$) %]]]
represents the maintainance of a version with value $d$ that was
written by access $T$; we will see that $\ms{s.version}(T_X) = d_0$
since $d_0$ is the initial version.
The component $\ms{s.reads-from}$ is
a partial function from 
\{$T$: $T$ is a write access to $X$\} $\cup \{T_X\}$ 
to the set of sets of read accesses to $X$. The
set $\ms{s.reads-from}(T)$ records the collection
of read accesses that have returned the version written by $T$; we will
see that $\ms{domain}(\ms{s.reads-from}) = \ms{domain}(\ms{s.reads-from})$.
%]]]

An initial state $s_{0}$ of $R_X$ is one where
$s_{0}.\ms{time} = \{(T_X,-\infty)\}$, 
%[[[
$s_{0}.\ms{version} = \{(T_X,d_{0})\}$
(where $d_{0}$ is the initial value from the domain $D$),
%A 5/91]]]
$s_{0}.\ms{reads-from} = \{(T_X,\emptyset)\}$, and
all other components of $s_{0}$ are empty.

In a state $s$, the components $\ms{s.created},
\ms{s.committed}$, and $\ms{s.aborted}$
keep track of those transactions for which the object has received a
\crt, \infcm{} 
and \infab, respectively.  
In addition, the component $\ms{s.time}$ keeps track of the pseudotime 
associated with each access
transaction for which an \inftm{} has been received.
The component
$\ms{s.commit-requested}$ records all transactions for which the object has
sent out a \rqcm.  
The $\ms{s.version}$ component
keeps track of the versions
%[[[
produced by different write accesses,
%A 5/91]]]
while the $\ms{s.reads-from}$ component records, for each write access and
the version it creates, the set of read accesses which read that version.

In describing the pseudotime object algorithm, it will be useful to
use some shorthand.
Given a state $s$, define
%[[[
$\ms{s.nonorphans} = \{T : \ms{ancestors}(T) \cap \ms{s.aborted} = \emptyset\}$.
%A 5/91]]]
If $T_{1}$ and $T_{2}$ are accesses of $X$,
say $T_{1}$ is \df{visible in $s$} to $T_{2}$ if
$\ms{ancestors}(T_{1}) - \ms{ancestors}(T_{2}) \subseteq \ms{s.committed}$.

The actions are as follows.

\iocode{
\ef{\CRT{T}}
{%%Effect:
     $\ms{s.created} = \ms{s'.created} \cup \{T\}$}

\ef{\INFCMntab{X}{T}}
{%Effect:
     $\ms{s.committed} = \ms{s.committed} \cup \{T\}$}

\ef{\INFABntab{X}{T}}
{%%Effect:
     $\ms{s.aborted} = \ms{s'.aborted} \cup \{T\}$}

\ef{\INFTMntab{X}{T,p}}
{%%Effect:
    $\ms{s.time}(T) = p$}  

\prcef{\RQCMntab{T}{\qms{OK}},\\
	 \>\> $\ms{kind}(T) = \qms{write}$}
{%%Precondition:
     $T \in \ms{s'.created}$\\
     $T \notin \ms{s'.commit-requested}$\\
     $T \in \ms{domain}(\ms{s'.time})$\\
%[[[following condition changed to standard format A 7/91]]]
     there do not exist $T'$ and $T''$ such that\\
     \> $T'' \in \ms{s'.reads-from}(T')$ \\
     \> $T'' \in \ms{s'.nonorphans}$\\
     \> $\ms{s'.time}(T') < \ms{s'.time}(T) < \ms{s'.time}(T'')$}
{%%Effect:
     $\ms{s.commit-requested}$\\ \> $ = \ms{s'.commit-requested} \cup \{T\}$\\
%[[[following condition changed A 5/91]]]
     $\ms{s.version}(T) = \ms{data}(T)$\\  
     $\ms{s.reads-from}(T) = \emptyset$}
}{
\prcef{\RQCMntab{T}{v},\\
	\>\> $\ms{kind}(T) = \qms{read}$}
{%%Precondition:
     $T \in \ms{s'.created}$\\
     $T \notin \ms{s'.commit-requested}$\\
     $T \in \ms{domain}(\ms{s'.time})$\\
     $T' \in \ms{domain}(\ms{s'.version})$\\
     $\ms{s'.time}(T') < \ms{s'.time}(T)$\\
%[[[changes to following conditions A 7/91]]]
     there does not exist  $T''$ such that\\
     \> $T'' \in \ms{domain}(\ms{s'.version})$ \\
     \> $T'' \in \ms{s'.nonorphans}$\\
     \> $\ms{s'.time}(T') < \ms{s'.time}(T'') < \ms{s'.time}(T)$\\ 
     either $T' = T_X$ or $T'$ is visible to $T$ in $s'$\\
     $v = \ms{s'.version}(T')$}
{%%Effect:
     $\ms{s.commit-requested}$\\ \> $ = \ms{s'.commit-requested} \cup \{T\}$\\
     $\ms{s.reads-from}(T')$\\ \> $ = \ms{s'.reads-from}(T') \cup \{T\}$} 
}

The principle that underlies the
action of $R_X$  is straightforward.  
The versions and reads-from relationships
give partial information about an execution of $S_X$, 
viewed as taking place in pseudotime order rather than real time order.  
If $s$ is a state of $R_X$, the facts that $\ms{s.version}(T') = r$ and
$T \in \ms{s.reads-from}(T')$ mean that
(provided the accesses involved are not aborted)  %%AAAAA
%[[[
$r$ is the effective version during the interval of pseudotime [$\ms{s.time}(T'),\ms{s.time}(T)$).
%A 5/91]]]

Regions of $\cal P$ that are not covered by any interval
%[[[
[$\ms{s.time}(T'),\ms{s.time}(T'')$),
%A 5/91]]]
for nonorphan write $T'$ and nonorphan read $T''$ with $T''$ 
in $\ms{s.reads-from}(T')$,
represent those regions in which no particular
state must hold; thus write accesses 
can safely occur only in those regions. 
Thus a \RQCM{T}{v} action for a write access
has a precondition that checks that the pseudotime associated with the
write does not lie in any interval [$\ms{s.time}(T'),\ms{s.time}(T'')$),
for nonorphan write $T'$ and nonorphan read $T''$ with $T''$ in 
$\ms{s.reads-from}(T')$.
%[[[
The 
effect of the action is to record 
a new version, $\ms{s.version}(T)$, whose value is $\ms{data}(T)$.

If $T$ is a read access, it should return 
the value produced by the nonorphan write access $T'$
whose pseudotime is closest to (but preceding) the pseudotime
associated with $T$. 
To preclude the write from aborting after the read has
committed (an event that could violate atomicity for $T$,
since the writer's actions would then not be in the view of $T$)
the read access must be blocked until $T'$ is 
visible to $T$. Notice how the
code for the \rqcm{} for a read mentions a variable $T'$
(representing the writer whose version is returned) in both precondition
and effect, but no quantification is given for $T'$. Recall
that this usage
is an abbreviation; the action can occur when some transaction name $T'$
can be found satisfying the clauses listed in precondition, 
and the effect then refers to
the value of $T'$ which made the precondition true.
%A 5/91 People should check if the explanation of the free variable is clear enough]]]

%[[[A 11/91
\begin{example}{Reed's Algorithm In A Message Queue System}
\label{reed-example}
Consider the message queue system of Example
\ref{ss-queue-system-example}. This system contains a read/write serial object
$X_A$, which is accessed by transaction names $T_{Rj.Ax}$ (with $\ms{kind}(T_{Rj.Ax}) = \qms{write}$
and $\ms{data}(T_{Rj.Ax})=x$) and $T_{Vk.A}$ (with $\ms{kind}(T_{Vk.A})= \qms{read}$).
When we use the set of finite sequences of positive integers, ordered lexicographically,
as pseudotimes, we
can construct the pseudotime object automaton $R_{X_A}$ using Reed's algorithm
for this serial object. The following sequence $\beta$ is a schedule of $R_{X_A}$.
\schedlist{
\INFTMntab{X_A}{T_{R1.A3}, 2,2}\\
\CRT{T_{R1.A3}}\\
\>\CRT{T_{V1.A}}\\
\RQCMntab{T_{R1.A3}}{\qms{OK}}\\
\>\INFTMntab{X_A}{T_{V1.A}, 8,3}\\
\>\>\CRT{T_{V3.A}}\\
\>\>\INFTMntab{X_A}{T_{V3.A}, 3,5}\\
\INFCMntab{X_A}{T_{R1.A3}}\\
\INFCMntab{X_A}{T_{R1}}\\
\>\>\RQCMntab{T_{V3.A}}{3}\\
\>\RQCMntab{T_{V1.A}}{3}\\
\>\>\INFCMntab{X_A}{T_{V3.A}}\\
\>\>\>\CRT{T_{R2.A1}}\\
\>\>\>\>\INFTMntab{X_A}{T_{V6.A}, 6,1}\\
\>\>\>\>\CRT{T_{V6.A}}\\
\>\>\>\>\>\CRT{T_{V5.A}}\\
\>\>\>\>\>\>\INFTMntab{X_A}{T_{R4.A9}, 7,2}\\
\>\>\>\>\>\INFTMntab{X_A}{T_{V5.A}, 4,3}\\
\>\>\>\>\>\>\CRT{T_{R4.A9}}\\
\>\INFABntab{X_A}{T_{V1}}\\
\>\>\>\INFTMntab{X_A}{T_{R2.A1}, 5,2}\\
\>\>\>\RQCMntab{T_{R2.A1}}{\qms{OK}}.
}
The schedule $\beta$ can leave $R_{X_A}$ in state $s$ where
$\ms{s.created} = \{T_{R1.A3}, T_{V1.A}, T_{V3.A}, T_{R2.A1}, T_{V6.A}, T_{V5.A}, T_{R4.A9} \}$, 
$\ms{s.committed} = \{T_{R1.A3}, T_{R1}, T_{V3.A}, \}$, 
$\ms{s.aborted} = \{T_{V1} \}$, 
$\ms{s.commit-requested} = \{T_{R1.A3}, T_{V3.A}, T_{V1.A}, T_{R2.A1} \}$,
$\ms{s.time}(T_{X_A}) = -\infty$, 
$\ms{s.time}(T_{R1.A3}) = 2,2$, 
$\ms{s.time}(T_{V1.A}) = 8,3$, 
$\ms{s.time}(T_{V3.A}) = 3,5$, 
$\ms{s.time}(T_{V6.A}) = 6,1$, 
$\ms{s.time}(T_{R4.A9}) = 7,2$, 
$\ms{s.time}(T_{V5.A}) = 4,3$, 
$\ms{s.time}(T_{R2.A1}) = 5,2$, 
$\ms{s.version}(T_{X_A}) = 0$,
$\ms{s.version}(T_{R1.A3}) = 3$ 
$\ms{s.version}(R2.A1) = 1$ 
and $\ms{s.reads-from}(T_{X_A}) = \emptyset$,
$\ms{s.reads-from}(T_{R1.A3}) =\{T_{V3.A},T_{V1.A} \}$,
$\ms{s.reads-from}(T_{R2.A1}) = \emptyset$.

%[[[We should do a diagram of the state after $s$ as a time line]]]

In the state $s$, the action $\RQCM{T_{V5.A}}{3}$ is enabled, returning the value
of the version written by $T_{R1.A3}$, since the pseudotime recorded for that transaction 
(2,2) is the highest that is less than the pseudotime recorded
for $T_{V5.A}$ among those recorded for write accesses that are in $s.\ms{nonorphans}$. 
Notice that since $T_{R1.A3}$ and $T_{R1}$ are
in $s.\ms{committed}$, the writer of the version is visible in $s$ to $T_{V5.A}$.

In the state $s$, the action $\RQCM{T_{R4.A9}}{\qms{OK}}$ is enabled. Notice that although
the pseudotime recorded for $T_{R4.A9}$ lies in between the times recorded for
the write access $T_{R1.A3}$ and the access $T_{V1.A}$ that read from that version,
the precondition is satisfied because $T_{V1.A}$ is not in $s.\ms{nonorphans}$.

By contrast, in the state $s$ there is no value $v$ for which $\RQCM{T_{V6.A}}{v}$ is
enabled, since the version written by a nonorphan with the highest recorded
pseudotime less than $6,1$ (the pseudotime of $T_{V6.A}$) is the version written by
$T_{R2.A1}$, which is {\em not} visible in $s$ to $T_{V6.A}$.
As more information arrives about the fate of transactions, the correct return
value can be determined.
For example, the sequence $\beta\INFAB{X_A}{T_{R2.A1}}$ can leave the automaton in
a state where $\RQCM{T_{V6.A}}{3}$ is enabled; on the other hand the
sequence $\beta\INFCM{X_A}{T_{R2.A1}}\INFCM{X_A}{T_{R2}}$ can leave the
automaton in a state where $\RQCM{T_{V6.A}}{1}$ is enabled.

Let
 $\beta'$  denote the sequence
\schedlist{
\INFCMntab{X_A}{T_{R2.A1}}\\
\INFCMntab{X_A}{T_{R2}}\\
\RQCMntab{T_{V6.A}}{1}\\
\RQCMntab{T_{V5.A}}{3}\\
\INFCMntab{X_A}{T_{V5.A}}\\
\INFCMntab{X_A}{T_{V5}}
}
We leave the reader to check (as Exercise \ref{reed-example-exercise}) that
$\ms{local-view}(\beta\beta',T_{V6.A}) = \ms{perform}(\xi)$
where $\xi = (T_{R1.A3},\qms{OK}) (T_{V5.A},3)  (T_{R2.A1},\qms{OK}) (T_{V6.A},1)$.
The order\footnote{The reader should note that this order is not consistent 
with what can be deduced about 
the completion order in the system; for example, $T_{R2}$ must commit before the
\infcm{} for it occurs, which is before the \rqcm{} for $T_{V5}$, which must be
before $T_{V5}$ commits. This reflects the distinction between static atomicity
and dynamic atomicity.}
of operations in $\xi$ is given by $\ms{local-pseudotime-order}(\beta\beta')$.

\end{example}
%]]]

\subsection{Correctness Proof}
\subsubsection{Basic Properties of $R_X$}

%[[[A 7/91
We have the following straightforward lemmas.
The first gives connections
between a schedule and the record kept
in the state.
The second gives the main invariants of the state.
%]]]

\begin{lemma}
\label{ts_pseudotime_object_state_1}
Let $\beta$ be a finite pseudotime object well-formed schedule of $R_X$.
Suppose that $\beta$ can leave $R_X$ in state $s$.  
Then the following conditions hold.

\begin{enumerate}
\item $T \in \ms{s.created}$ if and only if \CRT{T} appears in $\beta$.

\item $T \in \ms{s.committed}$ if and only if \INFCM{X}{T} appears in 
$\beta$.

\item $T \in \ms{s.aborted}$ if and only if \INFAB{X}{T} appears in 
$\beta$.

\item $\ms{s.time}(T) = p$ if and only if either $T = T_X$ and $p = -\infty $
or else \\ 
\INFTM{X}{T,p} appears in $\beta$.

\item $T \in \ms{s.commit-requested}$ if and only if a \rqcm{} for $T$
appears in $\beta$.
\end{enumerate}
\end{lemma}

\begin{proof}
By induction on the length of $\beta$.
\end{proof}


\begin{lemma}
\label{ts_pseudotime_object_state_2}
Let $\beta$ be a finite pseudotime object well-formed schedule of $R_X$ .
Suppose that $\beta$ can leave $R_X$ in state $s$.  
Then the following conditions hold.
\begin{enumerate}
\item If $\ms{s.time}(T) = \ms{s.time}(T')$ then $T = T'$.

\item $\ms{s.commit-requested} \subseteq \ms{domain}(\ms{s.time})$.

\item $T_X \in \ms{domain}(\ms{s.version})$ and
%[[[
$\ms{s.version}(T_X) = d_{0}$.
%A 5/91]]]

\item If $T \in \ms{domain}(\ms{s.version})$ and $T \neq T_X$ then
\begin{enumerate}
\item $T$ is a write access to $X$, and 

\item \RQCM{T}{\qms{OK}} occurs in $\beta$ and\\ %%anna
%[[[
$\ms{s.version}(T) = \ms{data}(T)$.
%A 5/91]]]
\end{enumerate}

\item If $T$ is a write access to $X$
and $T \in \ms{s.commit-requested}$
then $T \in \ms{domain}(\ms{s.version})$.

\item $\ms{domain}(\ms{s.reads-from}) = \ms{domain}(\ms{s.version})$.

\item If $T \in \ms{s.reads-from}(T')$, then
\begin{enumerate}
\item $T$ is a read access,

\item either $T' = T_X$ or $T'$ is visible to $T$ in $s$,

\item $\ms{s.time}(T') < \ms{s.time}(T)$ 

\item if $T'' \in \ms{domain}(\ms{s.version}), T \in \ms{s.nonorphans}$
and $\ms{s.time}(T') < \ms{s.time}(T'') < \ms{s.time}(T) $
%[[[
then $T'' \not\in \ms{s.nonorphans}$, and
%A 5/91]]]

%[[[
\item \RQCM{T}{v} occurs in $\beta$
where $v = \ms{s.version}(T')$.
%A 5/91]]]
\end{enumerate}

\item Suppose $T$ is a read access to $X$
and $T \in \ms{s.commit-requested}$.
Then $T \in \ms{s.reads-from}(T')$ for some $T'$.

\item Suppose $T$ and $T'$ are write accesses to $X$
in $\ms{s.commit-requested}$.
Then $\ms{s.reads-from}(T) \cap \ms{s.reads-from}(T') = \emptyset$.

\item Suppose $T \in \ms{s.nonorphans}$, and
$T \in \ms{s.reads-from}(T')$.  
Then either $T' = T_X$ or else $T' \in \ms{s.nonorphans}$.
\end{enumerate}
\end{lemma}

\begin{proof}
By induction on the length of $\beta$.
\end{proof}

We can use these
facts to see that $R_X$ preserves pseudotime object well-formedness.
The details are left as Exercise \ref{reed-well-formed-exc}.

\begin{lemma}
\label{ts_pseudotimeobject_is_well-formed}
$R_X$ is a pseudotime object for $X$.
\end{lemma}


\subsubsection{Proving Local Static Atomicity}

The following results demonstrate that this algorithm is satisfactory for
use in a system that uses timestamp order for serialization.
%[[[I deleted a sentence here A 5/91]]]

First a technical notion is defined, 
%[[[A 7/91
reflecting %]]]
the intuition of a mutually
consistent collection of non-orphan accesses,
that is, a set of accesses that might comprise those visible
to a particular transaction.\footnote{The definition given is somewhat more
permissive than one that would exactly capture this intuition. However, it
is safe, in the sense that the collection visible to
a given transaction will be {\em allowable}.}
%[[[A 7/91 above footnote added]]]
%[[[A 7/91
Recall that a read access was blocked
until the writer whose value it returns is visible
to it; this implies that the writer will be visible to a transaction
if the reader is visible to it. This motivates the third condition
in the following definition.
%]]]

If $\ms{s}$ is a state of $R_X$, then 
define ${\cal U}$ to be an \df{allowable} set of accesses to $X$
\index{allowable}
for $\ms{s}$ provided that the following conditions hold.
\begin{itemize} 
\item All accesses in $\cal U$ are in $\ms{s.nonorphans}$.

\item All accesses in $\cal U$ are in $\ms{s.commit-requested}$.

\item
%[[[I deleted the use of ``closed'' here, since it was technically incorrect A 5/91]]]
If $T' \in \ms{s.reads-from}(T)$ and $T' \in$
$\cal U$, then either $T = T_X$ or $T \in \cal U$.
\end{itemize}


%[[[A 11/91
\begin{example}{Allowable Set of Accesses}
Consider the pseudotime object $R_{X_A}$ and its schedule $\beta$, discussed in Example
\ref{reed-example}. Let $s_1$ denote the state in which
the schedule $\beta\RQCM{T_{V5.A}}{3}$ can leave the automaton.
For $s_1$, an allowable set of
accesses is $\{T_{R1.A3}, T_{V5.A}, T_{R2.A1} \}$. Another
allowable set is $\{T_{R1.A3}, T_{V5.A}, T_{V3.A}\}$. However the set
 $\{T_{R1.A3}, T_{V5.A}, T_{V1.A}\}$ is not allowable, because $T_{V1.A}$ is is
not in $s_1.\ms{nonorphans}$.
Also, $\{T_{R2.A1}, T_{V5.A}\}$ is not allowable because the write access $T_{R2.A3}$ (whose
version $T_{V5.A}$ read) is absent.
\end{example}
%]]]

%[[[A 7/91
The value of variable $\ms{s.time}$ can be used to define a 
derived partial order $\ms{s.timeorder}$
on accesses to $X$, as follows.
If $T$ and $T'$ are distinct accesses to $X$,
$\ms{s.time}(T)$ and $\ms{s.time}(T')$ are both defined,
and $\ms{s.time}(T) < \ms{s.time}(T')$,
then $(T,T')$ is included in $\ms{s.timeorder}$.
This is a reflection of \ms{local-pseudotime-order}, except that it
uses the time recorded in the state rather
than the time information in \inftm{} events in the schedule. This 
alternative order makes it easier to reason inductively using the
state of the automaton.
%]]]

The following lemma shows that the operations of 
an allowable set of accesses, 
arranged in the order of the recorded pseudotimes,
provide a behavior of $S_X$.
This is the key to the proof that the algorithm provides 
static atomicity.


\begin{lemma}
\label{ts_allowable_serial}
%[[[
Let $\beta$ be any finite schedule of $R_X$  
that is pseudotime object well-formed for $X$, 
and suppose $\beta$ can lead to state $s$.
Let $\cal U$ be an allowable set of accesses to $X$ for $s$.
Let $Z$ be the set of operations occurring in $\beta$ whose transaction
components are in $\cal U$.
Let $\xi$ be the sequence that results when $Z$ is arranged
in an order consistent with that determined by
$\ms{s.timeorder}$ on the transaction components.
Let $\gamma = \ms{perform}(\xi)$.
Then $\gamma$ is a behavior of $S_X$.
% Reworded A 5/91]]]
\end{lemma}

\begin{proof}
By pseudotime object well-formedness,
no transaction has more than one \rqcm{} in $\beta$,
and thus all operations in $S$ have distinct transaction components.
Thus
$\ms{perform}(\xi)$ is serial object well-formed.

Proceed by induction on the length of prefixes $\zeta$ of $\xi$,
showing that for each such $\zeta, \ms{perform}(\zeta)$ is a behavior of $S_X$.
The basis is trivial, so suppose that $\zeta = \zeta'(T,v)$,
where $\zeta$ is a prefix of $\xi$,
$\ms{perform}(\zeta')$ is a behavior of $S_X$ 
and $(T,v)$ is an operation in $S$.
There are two cases.
				   
\begin{enumerate}

\item $T$ is a write access.

%[[[
By the preconditions of \RQCM{T}{v} in $R_X$,
$v = \qms{OK}$.
In Example \ref{read-write-obliterating} we showed that $(T,v)$ is an obliterating
operation of $S_X$. That is,
$\ms{perform}(\zeta) = \ms{perform}(\zeta'(T,v))$ is equieffective to $\ms{perform}(T,v)$.
By the code of $S_X$, $\ms{perform}(T,v)$ is a behavior of $S_X$.
Since $\ms{perform}(\zeta)$ is equieffective to $\ms{perform}(T,v)$,
$\ms{perform}(\zeta)$ is also a behavior of $S_X$.
% A 5/91]]]

\item $T$ is a read access.

Since $\cal U$ is allowable for $s$, $T$ is in $\ms{s.reads-from}(T')$ for some
$T'$ which is either $T_X$ or else is a write access in $\cal U$.

If $T' = T_X$ then $\ms{s.time}(T') = -\infty$, 
so by part 7 of Lemma \ref{ts_pseudotime_object_state_2},
$\zeta'$ is a sequence of operations of the form $(T'',v'')$ where
each $T''$ is a read access.
%[[[
By Example \ref{read-write-transparent}, each operation in $\zeta'$ is transparent.
Thus,
% A 5/91]]]
Proposition \ref{ss_reads}
implies that
$\ms{perform}(\zeta')$ is equieffective to the empty sequence. 
By Proposition \ref{ss_equieffective_extension},
$\ms{perform}(\zeta) = \ms{perform}(\zeta'(T,v))$ is equieffective to $\ms{perform}(T,v)$.
Since $T \in \ms{s.reads-from}(T_X)$,
Parts 3 and 7 of Lemma \ref{ts_pseudotime_object_state_2}
imply that 
%[[[
$v = \ms{s.version}(T_X) = d_{0}$.
By the code of $S_X$,
%]]]
$\ms{perform}(T,v) \in \ms{behs}(S_X)$.
Since $\ms{perform}(\zeta)$ is equieffective to $\ms{perform}(T,v)$,
$\ms{perform}(\zeta) \in \ms{behs}(S_X)$.

If on the other hand  $T' \neq T_X$, 
then $T' \in \cal U$.
%[[[
Then parts 4 and 7 of Lemma \ref{ts_pseudotime_object_state_2}
imply that $\beta$ contains a \RQCM{T'}{v'} where $v' = \qms{OK}$
action, and $\ms{s.time}(T') < \ms{s.time}(T)$.
Thus, $\zeta'$ also contains the operation $(T',v')$, 
i.e. $\zeta'$ is of the form $\eta(T',v')\eta'$.
By part 7 of Lemma \ref{ts_pseudotime_object_state_2},
$\eta'$ is a sequence of operations of the form $(T'',v'')$, where
each $T''$ is a read access.
By Example \ref{read-write-transparent}, each operation in $\eta'$ is transparent.
Thus,
Proposition \ref{ss_reads} implies that
$\ms{perform}(\zeta') = \ms{perform}(\eta(T',v')\eta')$
is equieffective to $\ms{perform}(\eta(T',v'))$;
this in turn is equieffective to
$\ms{perform}(T',v')$ since $(T',v')$ is obliterating by Example \ref{read-write-obliterating}.
Thus, $\ms{perform}(\zeta')$ is equieffective to $\ms{perform}(T',v')$.
Then Proposition \ref{ss_equieffective_extension} implies that
$\ms{perform}(\zeta)$ is equieffective to $\ms{perform}(T',v')\ms{perform}(T,v)$.

Since $T \in \ms{s.reads-from}(T')$,
part 7 of Lemma \ref{ts_pseudotime_object_state_2}
implies that  $v = \ms{s.version}(T')$.
Also, since $T' \in \ms{domain}(\ms{s.version})$,
part 4 of Lemma \ref{ts_pseudotime_object_state_2}
implies that $\ms{s.version}(T) = \ms{data}(T)$.
Thus by the code of $S_X$, $\ms{perform}(T',v')\ms{perform}(T,v)$ is in $\ms{behs}(S_X)$.
Since $\ms{perform}(\zeta)$ is equieffective to $\ms{perform}(T',v')\ms{perform}(T,v)$,
$\ms{perform}(\zeta) \in \ms{behs}(S_X)$.
%A 5/91]]]
\end{enumerate}
\end{proof}

Now one can prove that a data object is locally static atomic if it
is implemented using the algorithm described in this section.

\begin{proposition}
$R_X$  is locally static atomic.
\end{proposition}

\begin{proof}
%[[[
Let $\beta$ be a finite pseudotime object well-formed behavior of $R_X$ ,
and $T$ a transaction name that is not a local orphan in $\beta$.
Let $Z$ be the set of operations occurring in $\beta$ whose
transactions are locally visible to $T$ in $\beta$.
Then $\ms{local-view}(\beta,T) = \ms{perform}(\xi)$, where $\xi$ is the
result of ordering $Z$ according to the order 
$\ms{local-pseudotime-order}(\beta)$ on the transaction components.
The proof must show that $\ms{local-view}(\beta,T)$ is
a behavior of $S_X$.

Since $R_X$  has no internal actions, $\beta$ is also a schedule of $R_X$ .
Choose state $s$ of $R_X$  such that $\beta$ can lead to $s$.
Let $\cal U$ be the set of transaction components of operations in $Z$.
The proof shows that $\cal U$ is an allowable set of accesses to $X$ for $s$.

Let $T'$ be an access in $\cal U$.
If $T' \not\in \ms{s.nonorphans}$, then $T'$ is a local orphan at $X$ in $\beta$
by Lemma \ref{ts_pseudotime_object_state_1}.
Since $T'$ is locally visible at $X$ to $T$ in $\beta$,
Lemma \ref{ts_local_visibility_nonorphaness} implies that $T$ is a local
orphan in $\beta$, a contradiction.
Thus, $T' \in \ms{s.nonorphans}$.
				   
Since a \rqcm{} for $T'$ occurs in $\beta, T' \in
\ms{s.commit-requested}$.

Now suppose $T' \in \ms{s.reads-from}(T'')$ and $T'' \neq T_X$.
Then part 7 of Lemma \ref{ts_pseudotime_object_state_2}
implies that $T''$ is visible to $T'$ in $s$,
so that $T''$ is locally visible at $X$ to $T'$ in $\beta$,
by Lemma \ref{ts_pseudotime_object_state_1}.
Thus, $T''$ is locally visible at $X$ to $T$ in $\beta$, by Lemma 
\ref{ts_vis_atX_trans}.
Also by part 7 of Lemma \ref{ts_pseudotime_object_state_2}, 
there is a \rqcm{} for $T''$ in $\beta$,
i.e. $T'' \in \cal U$.
It follows that $\cal U$ is an allowable set of accesses to $X$, for $s$.
				   
Now let $Z'$ be the set of operations occurring in $\beta$ whose 
transaction components are in $\cal U$.
Let $\xi'$ be the result of ordering $Z'$ consistent with $\ms{s.timeorder}$ on the transaction
components.
Let $\gamma' = \ms{perform}(\xi')$.
Then Lemma \ref{ts_allowable_serial}
implies that $\gamma'$ is a behavior of $S_X$.

However, observe that pseudotime object well-formedness implies that each
access in $\cal U$ has at most one \rqcm{} in $\beta$.
Thus, $Z = Z'$.
Furthermore, $\ms{local-pseudotime-order}(\beta)$ is the same as 
%[[[
$\ms{s.timeorder}$.
%A 5/91]]]
Therefore, $\xi = \xi'$ and hence $\gamma = \gamma'$.
Therefore, $\gamma$ is a behavior of $S_X$, as required.
%Changed $S$ to $Z$ etc A 5/91]]]
\end{proof}

\subsection{A Concrete Implementation}
\label{ts-reed-concrete-section}

The algorithm described by Reed in \cite{Reed78} differs from 
the abstract algorithm in the Section \ref{ts_read-write-section}
primarily in the way in which the reads-from component
of the state is maintained.
$R_X$ maintains, for each version
of the object written by a write access,
the entire set of read accesses that read that version.
Reed's concrete algorithm maintains instead simply the maximum timestamp
of all accesses that read a given version,
and hence may be much more space-efficient.
We will see that Reed's algorithm is 
%[[[A 7/91 remember it isn't actually an implementation
(speaking loosely) %]]]
an implementation of the previous one,
in the sense that behavior permitted by Reed's is permitted by it.
However, there are behaviors permitted by the abstract algorithm that are not
permitted by Reed's implementation.
For example, if a read access $T$ returns 
a version written by $T'$ and then aborts,
$R_X$ permits a later writer $T''$ whose timestamp falls between the
timestamps for $T'$ and $T$ to create a new version.
Reed's implementation would force $T''$ to abort in this situation,
since the maximum timestamp of readers for a given version is not
decreased when a reader aborts.
If aborts are rare, then Reed's implementation is probably adequate.
If aborts are more frequent, however, then one might prefer an implementation
%[[[A 7/91
closer to the abstract algorithm given above,
%]]]
that kept more precise information
about the set of readers for each version,
and thus could avoid some unnecessary aborts.
%[[[A 7/91
Another way in which this concrete implementation is more space-efficient is 
that it removes versions created by write accesses that are orphaned,
rather than keeping them in the state and merely not checking them
in preconditions.

Reed's implementation is modeled using an automaton $\rms{R1}_X$.
The external action signature of $\rms{R1}_{X}$ is the same as that of any
pseudotime object for $X$.
In addition, $\rms{R1}_X$ has the following internal actions, each
representing
the discarding of a version created by an orphan writer.

\intr{%%Internal:
\DSCR{T}, $T$ an access to $X$}

The state of $\rms{R1}_X$ has components
$\ms{s.created}, \ms{s.committed}, \ms{s.aborted}, \ms{s.commit-requested},$
$\ms{s.time}$ and $\ms{s.version}$, with the same types as before.
Instead of $\ms{s.reads-from}$, there is
$\ms{s.max-reads-from}$, which is a partial mapping from
$\{T: T$ is a write access to $X \} \cup \{T_X\}$ to $\cal P$
$\cup \{-\infty\}$.
It represents the maximum timestamp for any read access that has
read a particular version.
%[[[
(If no access has read the version written by $T$, $\ms{max-reads-from}(T)$ is just
$\ms{time}(T)$.)
%A 5/91]]]

%[[[
We use some shorthand.  
Given a state $s$, define
$\ms{s.nonorphans}$ and 
``$T_{1}$ is visible in $s$ to $T_{2}$'' exactly
as for $R_X$.
%A 5/91]]]

In the initial state $s_{0}$ of $\rms{R1}_X, s_{0}.\ms{time}(T_X) = -\infty,$
%[[[
$s_{0}.\ms{version}(T_X) = d_{0}$, where $d_{0}$ is the initial value from the domain $D$,
%A 5/91]]]
and $s_{0}.\ms{max-reads-from}(T_X) = -\infty$. Furthermore, $s_{0}.\ms{time}$,
$s_{0}.\ms{version},$ and $s_{0}.\ms{max-reads-from}$ are otherwise undefined, and
all other components of $s_{0}$ are empty.

\iocode{
\ef{\CRT{T}}
{%%Effect:
      $\ms{s.created} = \ms{s'.created} \cup \{T\}$}

\ef{\INFCMntab{X}{T}}
{%%Effect:
      $\ms{s.committed }= \ms{s.committed} \cup \{T\}$}

\ef{\INFABntab{X}{T}}
{%%Effect:
      $\ms{s.aborted} = \ms{s'.aborted} \cup \{T\}$}

\ef{\INFTMntab{X}{T,p}}
{%%Effect:
      $\ms{s.time}(T) = p$}  
      
\prcef{\RQCMntab{T}{\qms{OK}},\\
      \>\> $\ms{kind}(T) = \qms{write}$}
{%%Precondition:
      $T \in \ms{s'.created}$\\
      $T \notin \ms{s'.commit-requested}$\\
      $T \in \ms{domain}(\ms{s'.time})$\\
%[[[A 7/91 next condition reworded]]]
      there does not exist $T'$ such that\\
      \> $T' \in \ms{domain}(\ms{s'.max-reads-from})$\\  
	\> $\ms{s'.time}(T') < \ms{s'.time}(T) < \ms{s'.max-reads-from}(T')$}
{%%Effect:
      $\ms{s.commit-requested} = \ms{s'.commit-requested} \cup \{T\}$\\
      $\ms{s.version}(T) = \ms{data}(T)$\\
      $\ms{s.max-reads-from}(T) = \ms{s'.time}(T)$}
}{
\prcef{\RQCMntab{T}{v},\\
      \>\> $\ms{kind}(T) = \qms{read}$}
{%%Precondition:
      $T \in \ms{s'.created}$\\
      $T \notin \ms{s'.commit-requested}$\\
      $T \in \ms{domain}(\ms{s'.time})$\\
      $T' \in \ms{domain}(\ms{s'.version})$\\
      $\ms{s'.time}(T') < \ms{s'.time}(T)$\\
      there does not exist $T''$ such that\\
       \> $T'' \in \ms{domain}(\ms{s'.version})$\\ 
	\> $\ms{s'.time}(T') < \ms{s'.time}(T'') < \ms{s'.time}(T)$\\
      either $T' = T_X$ or $T'$ is visible to $T$ in $s'$\\
      $v = \ms{s'.version}(T')$}
{%%Effect:
      $\ms{s.commit-requested} = \ms{s'.commit-requested} \cup \{T\}$\\
      $\ms{s.max-reads-from}(T')$\\ 
	\> $ = \ms{max}(\ms{s'.max-reads-from}(T'),\ms{s'.time}(T))$}
      
\prcef{\DSCR{T}, $T$ a write access to $X$}
{%%Precondition:
      $T \in \ms{domain}(\ms{s'.version})$\\
      $T \not\in \ms{s'.nonorphans}$}
{%%Effect:
      $\ms{s.version}(T) = \ms{undefined}$\\
      $\ms{s.max-reads-from}(T) = \ms{undefined}$}
}

%[[[Should we say ``= undefined'' as effect? 
% better: $\ms{s.version} = \ms{s'.version} \dagger T$ A 7/91]]]

\subsection{Correctness Proof}
\subsubsection{Basic Properties of $\rms{R1}_X$}

\begin{lemma}
\label{ts_Reed_state}
Let $\beta$ be a finite schedule of $\rms{R1}_X$ that can lead to state $s$
such that
$\beta|\ms{ext}(\rms{R1}_X)$ is pseudotime object well-formed for $X$.
Then the following conditions hold.
\begin{enumerate}
\item $\ms{domain}(\ms{s.version}) = \ms{domain}(\ms{s.max-reads-from})$.

\item If $T \in \ms{domain}(\ms{s.max-reads-from})$ then $\ms{s.time}(T)$ is defined
and either $T = T_X$ or $T \in \ms{s.commit-requested}$.

\item If $T \in \ms{domain}(\ms{s.max-reads-from})$ and $\ms{s.max-reads-from}(T)$
$\neq \ms{s.time}(T)$,
then there is a read access $T'$ to $X$ 
such that $\ms{s.time}(T') =
\ms{s.max-reads-from}(T)$.

\item If $\ms{s.max-reads-from}(T) = \ms{s.time}(T')$ and $T' \neq T$, then
$T' \in \ms{s.commit-requested}$.
\end{enumerate}
\end{lemma}

\subsubsection{Proving Implementation}
%[[[I deleted the mention of ``relative implementation'' A 5/91]]]
It is interesting to note that the automaton $\rms{R1}_X$
{\em does not} implement $R_X$ 
%[[[A 7/91
in the technical sense
defined in Section
\ref{implements-section}, which
requires {\em every}
finite
behavior of $\rms{R1}_X$ to also
be a behavior of $R_X$; rather, it is in the context of
a pseudotime system that their behaviors are indistinguishable.
Thus the proof of correctness
uses a possibilities mapping between entire
pseudotime systems, rather than between single pseudotime 
objects.\footnote{For an example in which the behavior of $\rms{R1}_X$ can differ
from that of $R_X$, 
suppose in both $R_X$  and $\rms{R1}_X$
a read access $T_{2}$ reads from an earlier $T_{1}$.  
Suppose also that a write access $T_{3}$ with a later timestamp 
than $T_{2}$'s is pending.  
Now suppose a second \INFTM{X}{T_{2},p} 
changes $T_{2}$'s timestamp to a time $p$ later than that of $T_{3}$.
Because $\ms{max-reads-from}(T_{1})$ is unchanged, $\rms{R1}_X$ will still
permit a \rqcm{} for $T_{3}$.  But $R_X$  will not, because
the precondition for \rqcm{} depends on the new value
of $\ms{time}(T_{2})$.  But in a  pseudotime system,
the second \INFTM{X}{T_{2},p} cannot occur,
no change to $T_{2}$'s timestamp can occur, 
and this difference in behavior cannot arise.}
%]]]

First we mention the following invariant.
\begin{lemma}
\label{ts_no_time_conflicts}
\sloppy
Let $\cal S$ be a  pseudotime system in which $\rms{R1}_X$ is
associated with $X$.
If s is a reachable state of $\cal S$, $T \in \ms{domain}(s[X].\ms{time})$
and \INFTM{X}{T,p} is enabled in $s$, then $p = s[X].\ms{time}$.
\fussy
\end{lemma}

Now we prove  the correctness of $\rms{R1}_X$.

\begin{theorem}
\label{ts_R1_implements}
Let $\cal S$ be a  pseudotime system in which $\rms{R1}_X$ is
associated with $X$, and
$\cal T$ be the same system with $R_X$  associated with $X$.
Then $\cal T$ implements $\cal S$.
\end{theorem}

\begin{proof}
The proof uses a possibilities mapping $f$ from states of $\cal S$
to the power set of states of $\cal T$.
If $s$ is a state of $\cal T$, define $f(s)$ to be the set of states $t$
of $\cal T$ such that:
\begin{enumerate}
\item For all component names $i$ except $X, s[i] = t[i]$.

\item $s[X].\ms{created} = t[X].\ms{created}$, and likewise for 
$\ms{committed, aborted, time}$ and $\ms{commit-requested}$.

\item $\ms{domain}(s[X].\ms{version}) \subseteq \ms{domain}(t[X].\ms{version}) \subseteq$
$\ms{domain}(s[X].\ms{version}) \cup (s[X].\ms{orphans})$.

\item If $T \in \ms{domain}(s[X].\ms{version})$ then $t[X].\ms{version}(T) = s[X].\ms{version}(T)$.

\item If $T \in \ms{domain}(s[X].\ms{max-reads-from})$ then 
\begin{enumerate}
\item if $s[X].\ms{max-reads-from}(T) = s[X].\ms{time}(T)$ then 
$t[X].\ms{reads-from}(T) = \emptyset$,

\item if $\ms{s[X].max-reads-from}(T) = \ms{s[X].time}(T')$, where $T' \neq T$,
then $T' \in \ms{t[X].reads-from}(T)$, and

\item if $T' \in \ms{t[X].reads-from}(T)$ 
then $\ms{s[X].time}(T') \leq \ms{s[X].max-reads-from}(T)$.
\end{enumerate}
\end{enumerate}

The proof now shows that $f$ is a possibilities mapping.

%[[[Alan and I propose leaving most of this proof out, as in
%the section below.  The original proof follows, commented out.  M.]]]
%[[[New proof:]]]
First suppose that $s$ is a start state of $\cal S$.
Define $t$ so that $t[i] = s[i]$ for all $i \neq X$.
Also, $t[X].\ms{created}, t[X].\ms{committed}, t[X].\ms{aborted}, t[X].\ms{time}$ and 
$t[X].\ms{commit-requested}$ are all empty.
Define $t[X].\ms{version}$ to be $\{(T_X,r_{0})\}$ and
$t[X].\ms{reads-from}$ to be $\{(T_X,\emptyset)\}$.
Clearly, $t$ is a start state of $\cal T$
and $s$ and $t$ are related as required by the definition of $f$.

Now consider a reachable state $s'$ of $\cal S$,
a step $(s',\pi,s)$ of $\cal S$ and a reachable state $t'$
$\in f(s')$ of $\cal T$.
The proof must show that there is an extended step $(t',\gamma,t)$
of $\cal T$ such that $T \in f(s)$.

The proof now proceeds by case analysis, examining
the different actions of $\cal S$ of which $\pi$ could
be an instance.  Checking the necessary conditions is straightforward,
and is left as Exercise \ref{ts_possibilities-check-exercise}.

One case is examined in detail: 
$\pi =$ \INFTM{X}{T,p}.  
This case is interesting because it relies on
the global system invariant summarized in the previous lemma.

Since $\pi$ is an output of the pseudotime controller
that is enabled in $s'$ and the pseudotime controller states
are the same in $s'$ and $t', \pi$ is also enabled in $t'$.
Choose $T$ so that $(t',\pi,t)$ is a step of $\cal T$.
Again, $T' \in f(s')$.
Now $T$ is the same as $T'$ except that $(T,p) \in t.\ms{time}$, and
$s$ is the same as $s'$ except that $(T,p) \in \ms{s.time}$,.
In checking that $T \in f(s)$, all properties are immediate
except for the last.
So suppose that $U \in \ms{domain}(s[X].\ms{max-reads-from})$.
Then $U \in \ms{domain}(s'[X].\ms{max-reads-from})$ and
$s[X].\ms{max-reads-from}(U) = s'[X].\ms{max-reads-from}(U)$.
Lemma \ref{ts_Reed_state} implies that $s'[X].\ms{time}(U)$ is defined.

Suppose that $s[X].\ms{time}(U) = s[X].\ms{max-reads-from}(U)$.
If $U = T$, then $s[X].\ms{time}(U) = p$,
$= s'[X].\ms{time}(U)$ by Lemma \ref{ts_no_time_conflicts}.
Thus, $s'[X].\ms{time}(U) = s[X].\ms{max-reads-from}(U)$ 
$= s'[X].\ms{max-reads-from}(U)$.
On the other hand, if $U \neq T$, then it is immediate that
$s'[X].\ms{time}(U) = s'[X].\ms{max-reads-from}(U),$ 
Thus in either case, $s'[X].\ms{time}(U) = s'[X].\ms{max-reads-from}(U),$ 
so that $t'.\ms{reads-from}(U) = \emptyset$,
so $t.\ms{reads-from}(U) = \emptyset$.

Now suppose that $\ms{s[X].max-reads-from}(U) = \ms{s[X].time}(U')$, where
$U' \neq U$.
Then $\ms{s'[X].max-reads-from}(U) = \ms{s.[X].max-reads-from}(U)$
$= \ms{s[X].time}(U') \neq s'[X].\ms{time}(U)$, by Lemma 
\ref{ts_pseudotime_object_state_2},
$= s[X].\ms{time}(U')$.
Then Lemma \ref{ts_Reed_state} implies that
there is a read access $U''$ to $X$ such that $s'[X].\ms{time}(U'') =$
$s'[X].\ms{max-reads-from}(U)$. 
Then $s[X].\ms{time}(U'') = s'[X].\ms{time}(U'') = s'[X]\ms{.max-reads-from}(U)$
$= s[X]\ms{.max-reads-from}(U) = s[X].\ms{time}(U')$,
so that $U' = U''$.
Thus, $\ms{s'[X].max-reads-from}(U) = s'[X].\ms{time}(U')$.
so $U' \in \ms{t'[X].reads-from}(U)$, so 
$U' \in \ms{t.reads-from}(U)$.

Finally, suppose that $U' \in \ms{t[X].reads-from}(U)$.
Then $U' \in \ms{t'[X].reads-from}(U)$,
so $s'[X].\ms{time}(U') \leq \ms{s'[X].max-reads-from}(U)$.
Thus, $\ms{s[X].time}(U') \leq \ms{s[X].max-reads-from}(U)$.
\end{proof}
%[[[end of new proof]]]
%[[[Original proof between brackets below. M.]]]
%[[[First suppose that s is a start state of $\cal S$.
%Define $t$ so that $t[i] = s[i]$ for all $i \neq X$.
%Also, $\ms{t[X].created}, \ms{t[X].committed},$ $\ms{t[X].aborted}, \ms{t[X].time}$ and 
%$\ms{t[X].commit-requested}$ are all empty.
%Define $\ms{t[X].version}$ to be $\{(T_X,r_{0})\}$ and
%$\ms{t[X].reads-from}$ to be $\{(T_X,\emptyset)\}$.
%Clearly, $T$ is a start state of $\cal T$
%and $s$ and $T$ are related as required by the definition of $f$.
%
%Now consider a reachable state $s'$ of $\cal S$,
%a step $(s',\pi,s)$ of $\cal S$  and a reachable state $t'$
%$\in f(s')$ of $\cal T$.
%
%First suppose $\pi \notin \ms{acts}(\cal T)$.
%Then $\pi$ is of the form \DSCR{T}.
%We must show that $t' \in f(s)$.
%Note that $s$ is the same as $s'$ except 
%that $T \notin \ms{domain}(\ms{s[X].version})$
%and $T \notin \ms{domain}(\ms{s[X].max-reads-from})$.
%All conditions in the definition of $f$ except for the third are
%immediate.
%For the third, we have
%$\ms{domain}(\ms{s[X].version}) \subseteq \ms{domain}(\ms{s'[X].version})$
%$\subseteq \ms{domain}(\ms{t'[X].version})$, showing the left-hand containment.
%Also, $\ms{domain}(\ms{t'[X].version}) \subseteq$
%$\ms{domain}$ $(\ms{s'[X].version}) \cup \ms{s'[X].orphans}$
%$\subseteq \ms{domain}(\ms{s[X].version}) \cup \{T\} \cup
%\ms{s'[X].orphans}$,
%$= \ms{domain}(\ms{s[X].version}) \cup \ms{s'[X].orphans}$ since $T \in
%\ms{s'[X].orphans}$,
%$= \ms{domain}(\ms{s[X].version}) \cup \ms{s[X].orphans}$.
%This shows the right-hand containment.
%
%Now suppose that $\pi \in \ms{acts}(\cal T)$.
%We must show that there is a step $(t',\pi,t)$ of $\cal T$ such
%that $t \in f(s)$.
%We consider cases.
%
%\begin{enumerate}
%\item $\pi \notin \ms{acts}(R_X)$.
%
%Then define $t[X] = t'[X]$ and $t[i] = s[i]$ for all $i \neq X$.
%
%To see that $(t',\pi,t)$ is a step of $\cal T$, consider each index
%$i$.
%If $i = X$, then $i$ is not in the action signature of the automaton
%associated with $i$ in $\cal T$, and $t[i] = t'[i]$.
%If $i \neq X$ and $i$ is not in the action signature of the automaton
%associated with $i$ in $\cal T$, then $t[i] = s[i] = s'[i] = t'[i]$.
%Finally, if $i \neq X$ and $i$ is in the action signature of the 
%automaton associated with $i$ in $\cal T$,
%then $t[i] = s[i]$ and $t'[i] = s'[i]$.
%Since $(s'[i],\pi,s[i])$ is a step of this automaton,
%so is $(t'[i],\pi,t[i])$.
%
%To see that $t \in f(s)$, we check the properties in turn.
%If $i \neq X$, then $t[i] = s[i]$ by definition.
%For the remaining properties, note that $t[X] = t'[X]$ and $s[X] = s'[X]$; 
%since $T' \in f(s')$ and the remaining properties only
%depend on the X-component of the state, the properties hold for
%$t$ and $s$ also.
%
%\item $\pi =$ \CRT{T}, $T$ an access to $X$.
%
%Since $\pi$ is an output of the pseudotime controller
%that is enabled in $s'$ and the pseudotime controller states
%are the same in $s'$ and $t', \pi$ is also enabled in $t'$.
%Choose $t$ so that $(t',\pi,t)$ is a step of $\cal T$.
%Since $t' \in f(s')$,
%$t$ is the same as $t'$ except that $T \in \ms{t.created}$, and
%$s$ is the same as $s'$ except that $T \in \ms{s.created}$, 
%it is easy to check that $t \in f(s)$.
%
%\item $\pi =$ \INFCM{X}{T}
%
%As in the \crt{} case, $\pi$ is enabled in $t'$.
%Choose $t$ so that $(t',\pi,t)$ is a step of $\cal T$.
%Since $t' \in f(s')$,
%$t$ is the same as $t'$ except that $t \in \ms{t.committed}$, and
%$s$ is the same as $s'$ except that $T \in \ms{s.committed}$, 
%it is easy to check that $t \in f(s)$.
%
%\item $\pi =$ \INFAB{X}{T} 
%
%As in the \crt{} case, $\pi$ is enabled in $t'$.
%Choose $t$ so that $(t',\pi,t)$ is a step of $\cal T$.
%Since $t' \in f(s')$,
%$t$ is the same as $t'$ except that $T \in \ms{t.aborted}$, and
%$s$ is the same as $s'$ except that $T \in \ms{s.aborted}$, 
%it is easy to check that $t \in f(s)$.
%
%\item $\pi = $\INFTM{X}{T,p}
%
%As in the \crt{} case, $\pi$ is enabled in $t'$.
%Choose $t$ so that $(t',\pi,t)$ is a step of $\cal T$.
%Again, $t' \in f(s')$.
%Now $t$ is the same as $t'$ except that $(T,p) \in \ms{t.time}$, and
%s is the same as $s'$ except that $(T,p) \in \ms{s.time}$,.
%In checking that $t \in f(s)$, all properties are immediate
%except for the last.
%So suppose that $U \in \ms{domain}(\ms{s[X].max-reads-from})$.
%Then $U \in \ms{domain}(\ms{s'[X].max-reads-from})$ and
%$\ms{s[X].max-reads-from}(U) = \ms{s'[X].max-reads-from}(U)$.
%Lemma \ref{ts_Reed_state} implies that $s'[X].\ms{time}(U)$ is defined.
%
%Suppose that $\ms{s[X].time}(U) = \ms{s[X].max-reads-from}(U)$.
%If $U = T$, then $\ms{s[X].time}(U) = p$,
%$= \ms{s'[X].time}(U)$ by Lemma \ref{ts_no_time_conflicts}.
%Thus, $\ms{s'[X].time}(U) = \ms{s[X].max-reads-from}(U)$ 
%$= \ms{s'[X].max-reads-from}(U)$.
%On the other hand, if $U \neq T$, then it is immediate that
%$\ms{s'[X].time}(U) = \ms{s'[X].max-reads-from}(U)$, 
%Thus in either case, $\ms{s'[X].time}(U) = \ms{s'[X].max-reads-from}(U)$, 
%so that $\ms{t'.reads-from}(U) = \emptyset$,
%so $\ms{t.reads-from}(U) = \emptyset$.
%
%
%Now suppose that $\ms{s[X].max-reads-from}(U) = \ms{s[X].time}(U')$, where
%$U' \neq U$.
%Then $\ms{s'[X].max-reads-from}(U) = \ms{s.[X].max-reads-from}(U)$
%$= \ms{s[X].time}(U') \neq \ms{s'[X].time}(U)$, by Lemma 
%\ref{ts_pseudotime_object_state_2},
%$= \ms{s[X].time}(U')$.
%Then Lemma \ref{ts_Reed_state} implies that
%there is a read access $U''$ to $X$ such that $\ms{s'[X].time}(U'') =$
%$\ms{s'[X].max-reads-from}(U)$.
%Then $\ms{s[X].time}(U'') = \ms{s'[X].time}(U'')$ $= \ms{s'[X].max-reads-from}(U)$
%$= \ms{s[X].max-reads-from}(U) = \ms{s[X].time}(U')$,
%so that $U' = U''$.
%Thus, $\ms{s'[X].max-reads-from}(U) = \ms{s'[X].time}(U')$.
%so $U' \in \ms{t'[X].reads-from}(U)$, so 
%$U' \in \ms{t.reads-from}(U)$.
%
%\sloppy
%Finally, suppose that $U' \in \ms{t[X].reads-from}(U)$.
%Then $U' \in \ms{t'[X].reads-from}(U)$,
%so $\ms{s'[X].time}(U') \leq \ms{s'[X].max-reads-from}(U)$.
%Thus, $\ms{s[X].time}(U') \leq$ $ \ms{s[X].max-reads-from}(U)$.
%\fussy
%
%\item $\pi =$ \RQCM{T}{v}, $T$ a write access to $X$.
%
%First we show that $\pi$ is enabled in $t'$.
%Most of the conditions follow immediately from the fact that
%$\pi$ is enabled in $s'$.
%The only interesting thing we have to show is:
%if $T'' \in \ms{t'[X].reads-from}(T')$ and 
%$\ms{t'[X].time}(T') < \ms{t'[X].time}(T) < \ms{t'[X].time}(T'')$ then
%$T'' \in \ms{t'[X].orphans}$.
%So suppose for the sake of contradiction
%that $T'' \in \ms{t'[X].reads-from}(T')$,
%$\ms{t'[X].time}(T') < \ms{t'[X].time}(T) < \ms{t'[X].time}(T'')$,
%and $T'' \in \ms{t'[X].nonorphans}$.
%Then either $T' = T_X$ or else $T' \in \ms{t'[X].nonorphans}$,
%by Lemma \ref{ts_pseudotime_object_state_2}.
%In either case, $T' \notin \ms{t'[X].orphans}$.
%
%Since $T' \in \ms{domain}(\ms{t'.reads-from})$,
%the definition of $f$ implies that 
%either $T' \in \ms{domain}(\ms{s'[X].max-reads-from})$
%or $T' \in \ms{s'[X].orphans}$.
%But the latter possibility implies that $T' \in \ms{t'[X].orphans}$,
%which we have already shown to be false.
%Therefore, $T' \in \ms{domain}(\ms{s'[X].max-reads-from})$.
%
%Now, $\ms{s'[X].time}(T') = \ms{t'[X].time}(T')$,
%$< \ms{t'[X].time}(T) = \ms{s'[X].time}(T)$,
%so that $\ms{s'[X].time}(T') < \ms{s'[X].time}(T)$.
%
%Also, $\ms{s'[X].time}(T) = \ms{t'[X].time}(T) < \ms{t'[X].time}(T'')$
%$= \ms{s'[X].time}(T'')$,
%$\leq \ms{s'[X].max-reads-from}(T')$ by the definition of $f$.
%Thus, $\ms{s'[X].time}(T) < \ms{s'[X]}$$.\ms{max-reads-from}(T')$.
%
%It follows that $\pi$ is not enabled in $s'[X]$, a contradiction.
%Thus, $\pi$ is enabled in $t'[X]$.
%
%It remains to show that the changes correspond.
%The only interesting case of the definition of $f$ is case 5a.
%We have $T \in \ms{domain}(\ms{s[X].max-reads-from})$ and
%$\ms{s[X].max-reads-from}(T) = \ms{s'[X].time}(T)$.
%But we also have $\ms{t[X].reads-from}(T) = \emptyset$, as needed.
%
%\item $\pi =$ \RQCM{T}{v}, $T$ a read access to $X$.
%
%First we show that $\pi$ is enabled in $t'$, for a particular $T'$.
%Most of the conditions follow immediately from the fact that
%$\pi$ is enabled in $s'$.
%The only interesting thing we have to show is:
%if $T'' \in \ms{domain}(\ms{t'[X].version})$ and 
%$\ms{t'[X].time}(T') < \ms{t'[X].time}(T'') < \ms{t'[X].time}(T)$ then
%$T'' \in \ms{t'[X].orphans}$.
%So suppose for the sake of contradiction
%that $T'' \in \ms{domain}(\ms{t'[X].version})$,
%$\ms{t'[X].time}(T') < \ms{t'[X].time}(T'') < \ms{t'[X].time}(T)$,
%and $T'' \notin \ms{t'[X].orphans}$.
%
%The definition of $f$ implies that either $T'' \in $
%$\ms{domain}(\ms{s'[X].version})$ of $T'' \in \ms{s'[X].orphans}$.
%Since the latter is impossible,
%$T'' \in \ms{domain}(\ms{s'[X].versions})$.
%Since $\ms{s'[X].time}(T') = \ms{t'[X].time}(T')$ and likewise for $T''$ and $T$,
%we have
%$\ms{s'[X].time}(T') < \ms{s'[X].time}(T'') < \ms{s'[X].time}(T)$.
%But this contradicts the assumption that $\pi$ is enabled in $s'$.
%It follows that $\pi$ is enabled in $t'$.
%
%It remains to show that the changes correspond.
%The only interesting things to show are cases 5b and 5c of the
%definition of $f$.
%Both are straightforward to check.
%
%\end{enumerate}]]]

The previous theorem implies that $\rms{R1}_X$ is static atomic.
\begin{corollary}
$\rms{R1}_X$ is static atomic.
\end{corollary}

\section{Type-specific Concurrency Control}

\label{herlihy-section}
The previous section described an algorithm that could be used for an object
whose serial specification (its type) 
%[[[
was given as a read/write serial object.
%A 5/91]]]
This section describes an algorithm 
due to Herlihy that applies to 
any object and that uses more information about the semantics of
the operations of the object \cite{Herlihy87}.
%[[[more detail left to bib section M.  12/90]]]
In fact, what is discussed here is a family
of algorithms, one for each possible choice of serial
dependency relation among
the accesses.\footnote{See Section \ref{serial_dependency_section} of Chapter 
\ref{examples-chapter}
for the definition and examples of serial dependency relations.}

%[[[A 7/91
Unlike Reed's algorithm described earlier, this algorithm does not
keep explicit versions of the serial object; instead it keeps track of 
all the operations that have occurred. A version is given implicitly, as
the result on the serial object of applying in timestamp sequence 
all the operations of nonorphan accesses whose pseudotime is less than a
given value.
The algorithm is based on the following idea
%[[[A 11/91 Changed to reflect the code rather than a different algorithm!
an access $T$ receives
a return value based on all the non-orphan accesses that are visible to it
and have pseudotimes less than that of $T$. The access $T$ is blocked
until every non-orphan access which has pseudotime less than that of $T$
and on which $T$ depends
is visible to $T$. This prevents $T$ receiving a result that will be 
lead to a failure of the view condition in the Atomicity Theorem.\footnote{Recall
that the view condition refers to the arrangement (in pseudotime order) of operations visible to
some transaction.
The operation of $T$ will be placed in that sequence after those operations
used to compute it, and also after operations with lower pseudotimes that
are not visible to $T$ at the time of the response, but become visible to the
given transaction. Since $T$ does not depend on such an operation,
the definition of serial dependency relation ensures that the sequence in the view condition
is a serial behavior.}
%]]]
In addition, the response to an access $T$ cannot be given
if any previous operation has occcurred for a
transaction with a pseudotime greater than $T$'s, unless 
the response to $T$ does not interfere with the appropriateness of that 
previous operation.\footnote{Suppose a response is given for $T$.
Recall that the previous operation includes
a return value, computed using a collection of operations. When the accesses
are serialized in pseudotime order, the resulting sequence will
place the previous operation after a collection
that includes those used to compute it, but
also includes the operation of $T$ (since the
serialization uses pseudotime order rather than the order of occurrence
in the pseudotime system). Thus inserting the operation
of $T$ in a sequence must not change the legality of the sequence
as a behavior of $S_X$. This is what the
serial dependency relation expresses.}
%]]]

\subsection{Herlihy Objects}

%[[[I changed the uses of SDR to represent a relation to just R.  N. 5/91]]]
%[[[Since the algorithm depends on R, I have added a papameter to the name H_X(R) A 5/91]]]
%[[[
Let $X$ be any object name, and
let $R$ be a serial dependency relation for serial object automaton $S_X$,
as defined in
Section \ref{serial_dependency_section}.
A particular pseudotime object automaton $H_X(R)$  
(a \df{Herlihy object}) is described, as a pseudotime object automaton.
%A 5/91]]]

Each state $s$ of $H_X(R)$ has the following components:
$\ms{s.created}, \ms{s.committed}, \ms{s.aborted}$, which are sets of transactions,
$\ms{s.commit-requested}$, which is a set of operations,
and $\ms{s.time}$, which is a partial mapping from $\ms{accesses}(X)$ to $\cal P$.
%[[[A 7/91
Notice that unlike Reed objects, here $\ms{commit-requested}$ stores operations,
that is return values as well as accesses are retained.
%]]]

Initially, all sets are empty and $\ms{s.time}$ is undefined everywhere.

As for $R_X$, some shorthand is useful, 
%[[[A 7/91
to correspond to
the concepts of local orphan and
local visibility, but using the information recorded in the state of $H_X(R)$
rather than the actions in the schedule.
%]]]
Given a state $s$, define
%[[[
$\ms{s.nonorphans} = \{T : \ms{ancestors}(T) \cap \ms{s.aborted} =
\emptyset\}$.
%A 5/91]]]
If $T_{1}$ and $T_{2}$ are accesses of $X$,
say $T_{1}$ is \df{visible in s} to $T_{2}$ if 
\index{visible in s}
$\ms{ancestors}(T_{1}) - \ms{ancestors}(T_{2}) \subseteq \ms{s.committed}$.
The actions are as follows.

\iocode{
\ef{\CRT{T}}
{%%Effect: 
     $\ms{s.created} = \ms{s'.created} \cup \{T\}$}

\ef{\INFCMntab{X}{T}}
{%%Effect:
     $\ms{s.committed} = \ms{s'.committed} \cup \{T\}$}

\ef{\INFABntab{X}{T}}
{%%Effect:
     $\ms{s.aborted} = \ms{s'.aborted} \cup \{T\}$}

\ef{\INFTMntab{X}{T,p}}
{%%Effect:
     $\ms{s.time}(T) = p$} 
}{
\prcef{\RQCMntab{T}{v}}
{%%Precondition:
     $T \in \ms{s'.created}$\\
     $(T,w) \notin \ms{s'.commit-requested}$ for any $w$\\
     $T \in \ms{domain}(\ms{s'.time})$\\
%[[[A 7/91 reworded in standard form]]]
    there do not exist $T'$ and $v'$ such that\\
    \> $(T',v') \in \ms{s'.commit-requested},$\\
	\>$ T' \in \ms{s'.nonorphans}$,\\
	\> $\ms{s'.time}(T) \leq \ms{s'.time}(T')$\\
	\> $((T,v),(T',v')) \in R$,\\ 
     there do not exist $T'$ and $v'$ such that\\
     \>$(T',v') \in \ms{s'.commit-requested}$\\ 
	\>$T' \in \ms{s'.nonorphans}$\\
	\>$\ms{s'.time}(T') < \ms{s'.time}(T)$\\
     \>$((T',v'),(T,v)) \in R$,\\
     \>$T'$ is not visible to $T$ in $s'$\\
     $\ms{perform}(\xi(T,v))$ is a behavior of $S_X$\\
     \>where $\xi$ is the result of ordering,\\
     \>\>in $\ms{s'.time}$ order,\\
     \>\>the set of operations $(T',v')$ such that\\
     \>\>\>$(T',v') \in \ms{s'.commit-requested}$\\ 
     \>\>\>$T' \in \ms{s'.nonorphans}$\\
     \>\>\>$T'$ is visible to $T$ in $s'$\\
     \>\>\>$\ms{s'.time}(T') < \ms{s'.time}(T)$}
{%%Effect:
     $\ms{s.commit-requested}$\\
	\> $= \ms{s'.commit-requested} \cup \{(T,v)\}$}
}

The precondition for \RQCM{T}{v} deserves some explanation.
The first three conditions simply require that $T$ is active and
its pseudotime is known to the object.
The next condition requires that no nonorphan access with a later
pseudotime depend on $T$; this 
%[[[A 7/91
is called the {\em ratchet lock} condition, since it
prevents an access from occuring unless its pseudotime is
sufficiently advanced.\footnote{The term is taken from the algorithm
described in \cite{Herlihy87}, where the corresponding limit on
pseudotime never decreases during an execution, in the same way that
a ratchet turns only one way. See Exercise \ref{herlihy-exercise}.}
The fourth condition requires that $T$ not depend on any operation
of a nonorphan  access
with an earlier pseudotime, unless that access is visible to $T$.
This is called the {\em no dirty data} condition.
The final condition requires that the return value be
appropriate for the version of $S_X$ based on
applying all the the operations of accesses that are visible to $T$ 
and have earlier pseudotimes.
%]]]

\begin{example}{A FIFO Queue Object}
\label{herlihy-example}
Consider the message queue system of Example
\ref{ss-queue-system-example}. This system contains a FIFO Queue serial object
$X_Q$, which is accessed by transaction names $T_{Gx}$ (with $\ms{kind}(T_{Gx}) = \qms{insert}$
and $\ms{data}(T_{Gx})=x$) and $T_{Ri.0}$ (with $\ms{kind}(T_{Ri.0})= \qms{delete}$).
Let $R_2$ denote the serial dependency relation for this object given in
Example \ref{examples-fifo-queue-sdr}, so that
$R_2$ contains all pairs 
$((T,v),(T',v'))$ where $T \neq T'$, $\ms{kind}(T') = \qms{delete}$, and either
of the following holds: $\ms{kind}(T) 
= \qms{insert}$ and $\ms{data}(T) \neq v'$;
or $\ms{kind}(T) 
= \qms{delete}$ and $v = v'$.
When we use the set of finite sequences of positive integers, ordered lexicographically,
as pseudotimes, we
can construct the pseudotime object automaton $H_{X_Q}(R_2)$ using Herlihy's algorithm
for this serial object. The following sequence $\beta$ is a schedule of $H_{X_Q}(R_2)$.
\schedlist{
\CRT{T_{G3}}\\
\INFTMntab{X_Q}{T_{G3},1}\\
\>\INFTMntab{X_Q}{T_{G6},2}\\
\>\CRT{T_{G6}}\\
\>\>\CRT{T_{R2.0}}\\
\>\RQCMntab{T_{G6}}{\qms{OK}}\\
\RQCMntab{T_{G3}}{\qms{OK}}\\
\INFCMntab{X_Q}{T_{G3}}\\
\>\>\INFTMntab{X_Q}{T_{R2.0}, 3,1}\\
\>\INFCMntab{X_Q}{T_{G6}}\\
\>\>\RQCMntab{T_{R2.0}}{3}\\
\>\>\INFABntab{X_Q}{T_{R2.0}}\\
\>\>\>\CRT{T_{R1.0}}\\
\>\>\>\INFTMntab{X_Q}{T_{R1.0}, 5,1}\\
\>\>\>\RQCMntab{T_{R1.0}}{3}\\
\>\>\>\>\CRT{T_{R3.0}}\\
\>\>\>\>\INFTMntab{X_Q}{T_{R3.0}, 11,1}\\
\>\>\>\INFCMntab{X_Q}{T_{R1.0}}\\
\>\>\>\INFCMntab{X_Q}{T_{R1}}\\
\>\>\>\>\RQCMntab{T_{R3.0}}{6}\\
\>\>\>\>\INFABntab{X_Q}{T_{R3}}\\
\>\>\>\>\>\CRT{T_{G4}}\\
\>\>\>\>\>\>\CRT{T_{G1}}\\
\>\>\>\>\>\>\INFTMntab{X_Q}{T_{G1},7}\\
\>\>\>\>\>\INFTMntab{X_Q}{T_{G4}, 8}\\
\>\>\>\>\>\RQCMntab{T_{G4}}{\qms{OK}}\\
\>\>\>\>\>\>\>\CRT{T_{G2}}\\
\>\>\>\>\>\>\>\INFTMntab{X_Q}{T_{G2},4}\\
\>\>\>\>\>\>\>\>\CRT{T_{G9}}\\
\>\>\>\>\>\>\>\>\INFTMntab{X_Q}{T_{G9},10}\\
\>\>\>\>\>\>\>\>\>\CRT{T_{R6.0}}\\
\>\>\>\>\>\>\>\>\>\INFTMntab{X_Q}{T_{R6.0}, 6,1}\\
\>\>\>\>\>\>\>\>\>\>\CRT{T_{R4.0}}\\
\>\>\>\>\>\>\>\>\>\>\INFTMntab{X_Q}{T_{R4.0}, 9,1}.
}
The schedule $\beta$ can leave $H_{X_Q}(R_2)$ in state $s$ where
$s.\ms{created} = \{T_{G3}, T_{G6}, T_{R2.0}, T_{R1.0},  T_{R3.0}, T_{G4}, T_{G1}, T_{G2},  T_{G9},
T_{R6.0}, T_{R4.0}\}$,
$s.\ms{committed} = \{T_{G3}, T_{G6}, T_{R1.0}, T_{R1}\}$,
$s.\ms{aborted} = \{T_{R2.0}, T_{R3}\}$,
$s.\ms{commit-requested} = \{(T_{G6},\qms{OK}), (T_{G3},\qms{OK}), (T_{R2.0},3), (T_{R1.0},3), 
(T_{R3.0},6), (T_{G4},\qms{OK})\}$,
$s.\ms{time}(T_{G3}) = 1$,
$s.\ms{time}(T_{G6}) = 2$,
$s.\ms{time}(T_{R2.0}) = 3,1$,
$s.\ms{time}(T_{R1.0}) = 5,1$,
$s.\ms{time}(T_{R3.0}) = 11,1$,
$s.\ms{time}(T_{G1}) = 7$,
$s.\ms{time}(T_{G4}) = 8$,
$s.\ms{time}(T_{G2}) = 4$,
$s.\ms{time}(T_{G9}) = 10$,
$s.\ms{time}(T_{R6.0}) = 6,1$,
$s.\ms{time}(T_{R4.0}) = 9,1$,
and $s.\ms{time}(T)$ is undefined for other access names $T$.

In the state $s$, the action $\RQCM{T_{G9}}{\qms{OK}}$ is enabled. This is because the
only operation that is in
$s.\ms{commit-requested}$ for a nonorphan access that is not visible in $s$
to $T_{G9}$ and has recorded pseudotime than 10 is 
$(T_{G4},\qms{OK})$ and $((T_{G4},\qms{OK}),(T_{G9},\qms{OK})) \not\in R_2$ (as both
accesses are inserts), and also there is no operation in $s.\ms{commit-requested}$
for a nonorphan access whose recorded pseudotime is greater than 10. Notice that 
the return value is
calculated using all operations with timestamps lower than 10, that are visible in $s$ to $T_{G9}$,
that is, it is $\qms{OK}$ because the sequence $\ms{perform}(\xi)$ be a finite behavior of $S_{X_Q}$,
where $\xi = (T_{G3},\qms{OK})(T_{G6},\qms{OK})(T_{R1.0},3)(T_{G9},\qms{OK})$. Notice also
that the order of operations in $\xi$ is that given by the recorded pseudotimes,
rather than the order in which the \rqcm{} actions occur.

Similarly $\RQCM{T_{G1}}{\qms{OK}}$ is enabled in $s$.  This is because there is no
operation that is in
$s.\ms{commit-requested}$ for a nonorphan access that is not visible in $s$
to $T_{G9}$ and has recorded pseudotime than 10,
and also the only operation in $s.\ms{commit-requested}$
for a nonorphan access whose recorded pseudotime is greater than 10 is $(T_{G4},\qms{OK})$
but $((T_{G1},\qms{OK}),(T_{G4},\qms{OK}))$ is not in $R_2$.

By contrast, $\RQCM{T_{G2}}{\qms{OK}}$ is not enabled in $s$, because of the
existence of $(T_{R1.0},3)$ in $s.\ms{commit-requested}$. Notice that
$((T_{G2},\qms{OK}),(T_{R1.0},3))$ is an element of the serial dependency relation $R_2$.


We leave as Exercise \ref{ts-herlihy-example-ex} the determination that in $s$,
$\RQCM{T_{R6.0}}{6}$ is enabled, but there is no value $v$ for
which $\RQCM{T_{R4.0}}{v}$ is enabled.
\end{example}

\subsection{Correctness Proof}
\subsubsection{Basic Properties of $H_X(R)$}

We begin by stating immediate connections
between the actions in a schedule of $H_X(R)$ and the
state to which it can lead.
The proof of this lemma is a simple induction.

\begin{lemma}
\label{ts_Herlihy_object_state_1}
Let $\beta$ be a finite
pseudotime object well-formed.
 schedule of $H_X(R)$.
%[[[A 7/91 removed mention of ext(H_X(R)]]]
Suppose that $\beta$ can lead to state $s$.
Then the following conditions hold.
\begin{enumerate}
\item $T \in \ms{s.created}$ if and only if \CRT{T} appears in $\beta$.

\item $T \in \ms{s.committed}$ if and only if \INFCM{X}{T} appears in 
$\beta$.

\item $T \in \ms{s.aborted}$ if and only if \INFAB{X}{T} appears in 
$\beta$.

\item $\ms{s.time}(T) = p$ if and only if \INFTM{X}{T,p} appears in $\beta$.

\item $(T,v) \in \ms{s.commit-requested}$ if and only if \RQCM{T}{v}
appears in $\beta$.
\end{enumerate}
\end{lemma}

By using the previous lemma and the preconditions of the actions,
it is easy to see that $H_X(R)$ preserves
pseudotime-object well-formedness.

\begin{lemma}
\label{ts_H_pseudotime object well-formed}
$H_X(R)$ is a pseudotime object for $X$.
\end{lemma}

\subsubsection{Proving Local Static Atomicity}				   

The next two lemmas give the main properties of the algorithm that are
used to prove its correctness.
The first lemma shows that the conditions checked
in the preconditions of a \RQCM{T}{v} action remain true as long as
$T$ is not an orphan.

\begin{lemma}
\label{ts_Herlihy_object_state_2}
%[[[WARNING. The claims are mentioned by
%number elsewhere in this subsection. Do not reorder them.]]]
Let $\beta$ be a finite pseudotime object well-formed
schedule of $H_X(R)$.
%[[[A 7/91 removed mention of ext(H_X]]]
Suppose that $\beta$ can lead to state $s$.
Then the following conditions hold.
\begin{enumerate}
\item If $\ms{s.time}(T) = \ms{s.time}(T')$ then $T = T'$.

\item $\{T:(T,v) \in \ms{s.commit-requested} \rms{for\ some} v\}$
$\subseteq \ms{domain}(\ms{s.time})$. 

\item Suppose $(T,v) \in \ms{s.commit-requested}$, $T \in \ms{s.nonorphans}$,
$(T',v') \in \ms{s.commit-requested}$, $T' \in \ms{s.nonorphans}$,
$\ms{s.time}(T') < \ms{s.time}(T)$ and $((T',v'),$ $(T,v)) \in R$.
Then $T'$ is visible to $T$ in $s$.

\item Suppose $(T,v) \in \ms{s.commit-requested}$ and $T \in \ms{s.nonorphans}$.
Let $S = \{(T',v') \in \ms{s.commit-requested}$: 
$T'$ is visible to $T$ in $s$ and $\ms{s.time}(T') \leq \ms{s.time}(T)\}$.
Let $\zeta$ be the result of ordering the operations in $S$ in $\ms{s.time}$ order.
Then $\ms{perform}(\zeta) \in \ms{behs}(S_X)$.
\end{enumerate}
\end{lemma}
				   
\begin{proof}
The proof is by induction on the length of $\beta$.
The base is obvious, so consider the inductive step.
Let $\beta = \beta'\pi$, where $\pi$ is a single action, where $\beta'$
can lead to state $s'$, and where $(s',\pi,s)$ is a step of $H_X(R)$.
The first two claims are straightforward.

Let $(T,v)$ and $(T',v')$ satisfy the hypothesis of Claim 3.
Since $T$ and $T'$ are in $\ms{s.nonorphans}$, they are in $\ms{s'.nonorphans}$ also.
By well-formedness and the fact that $T$ and $T'$ are in $\ms{s.commit-requested}$,
it follows that $T$ and $T'$ are in $\ms{domain}(\ms{s'.time})$, and that
$\ms{s'.time}(T) = \ms{s.time}(T)$ and $\ms{s'.time}(T') = \ms{s.time}(T')$.
There are three cases.
\begin{enumerate}

\item $(T,v)$ and $(T',v')$ are both in $\ms{s'.commit-requested}$.

Then the inductive hypothesis
implies that $T'$ is visible to $T$ in $s'$ and therefore in $s$.

\item $(T,v) \in \ms{s'.commit-requested}$ and $\pi$ is \RQCM{T'}{v'}.

This contradicts the {\em ratchet lock} clause in the precondition of $\pi$.


\item $(T',v') \in \ms{s'.commit-requested}$ 
and $\pi$ is \RQCM{T}{v}.

Then the {\em no dirty data} clause
in the precondition of $\pi$ ensures
that $T'$ is visible to $T$ in $s'$ and hence in $s$.

\end{enumerate}
Claim 3 follows.

Now let $(T,v)$, $S$ and $\zeta$ satisfy the hypothesis of Claim 4.
Let $S' = \{(T',v') \in \ms{s'.commit-requested}$:
$T'$ is visible to $T$ in $s'$ and $\ms{s'.time}(T') \leq \ms{s'.time}(T)\}$.
Let $\zeta'$ be the result of ordering the operations in $S'$
in $\ms{s'.time}$ order.
(Thus, $S'$ and $\zeta'$ are
defined just like $S$ and $\zeta$ but using $s'$ rather than $s$.)  

If $\pi$ is \RQCM{T}{v}, then $S = S' \cup \{(T,v)\}$, 
$\zeta = \zeta'(T,v)$, 
and the operation sequence called $\beta$ in the preconditions
of $\pi$ is equal to $\zeta'$.  %%stop
Thus the claim is guaranteed by the preconditions of $\pi$.
So assume that $\pi$ is not \RQCM{T}{v}.
Then $(T,v) \in \ms{s'.commit-requested}$.
Since $T \in \ms{s'.nonorphans}$,
the inductive hypothesis ensures that $\ms{perform}(\zeta')$ is in $\ms{behs}(S_X)$.

Now consider cases.
\begin{enumerate}

\item $\pi$ is neither a \RQCM{T'}{v'} action nor
an \INFCM{X}{U} for $U$ a child of an ancestor of $T$.

Then $S' = S$ and $\zeta' = \zeta$, so the result follows.

\item $\pi =$ \RQCM{T'}{v'}, where $T' \neq T$.

Then pseudotime object well-formedness implies that $S = S'$ and 
$\zeta = \zeta'$, so again the result follows.
($T'$ cannot become visible to $T$ as a result of this action, since
\INFCM{X}{T'} cannot precede \RQCM{T'}{v'}
in a pseudotime object well-formed sequence.)

\item $\pi =$ \INFCM{X}{U} for $U$ a child of an ancestor of $T$.

Then consider the operations in $S - S'$. 
Let $T''$ be the access with the largest
value of $\ms{s'.time}$ among those which appear as first component in 
$S - S'$. 
Clearly, $(T'',v'') \in \ms{s'.commit-requested}$ for some $v''$
and $T'' \in \ms{s'.nonorphans}$.
Let $S'' = \{(T',v') \in \ms{s'.commit-requested}:
T'$ is visible to $T''$ in $s'$ and $\ms{s'.time}(T') \leq \ms{s'.time}(T'')\}$.
Let $\zeta''$ be the result of ordering the operations in $S''$
in $\ms{s'.time}$ order.
(Thus, $S''$ and $\zeta''$ are
defined just like $S$ and $\zeta$ but using $s'$ rather than $s$ and $T''$ instead
of $T$.)
The inductive hypothesis ensures that $\ms{perform}(\zeta'')$ is in $\ms{behs}(S_X)$.
Also note that $S = S' \cup S''$; since $T''$ is visible to $T$
in $s$, $T''$ is visible to $U$ in $s'$, and an access is
visible to $U$ in $s'$ if and only if it is visible to $T''$ in $s'$. 
Thus, $\zeta'$ and $\zeta''$ are both subsequences of $\zeta$,
and each operation in $\zeta$ is in at least one of the two subsequences.

If $(T_{1},v_{1}) \in \zeta'' - \zeta',
(T_{2},v_{2}) \in \zeta' - \zeta''
\rms{and} \ms{s'.time}(T_{1}) < \ms{s'.time}(T_{2})$,
then Claim 3 
implies that $((T_{1},v_{1}),(T_{2},v_{2})) \notin R$.
Likewise, if $(T_{1},v_{1}) \in \zeta' - \zeta'',
(T_{2},v_{2}) \in \zeta' - \zeta''
\rms{and} \ms{s'.time}(T_{1}) < \ms{s'.time}(T_{2})$,
then $((T_{1},v_{1}),(T_{2},v_{2})) \notin R$.

Then Proposition~\ref{ts_merge}
implies that $\ms{perform}(\zeta) \in \ms{behs}(S_X)$.
\end{enumerate}
\end{proof}



One can use the preceding lemma to obtain the following corollary,
proving a property very similar to local static atomicity, 
but stated using components of the object's state rather than
properties of the behavior when determining
which accesses are visible and non-orphans, 
and the order to use in arranging operations.

\begin{lemma}
\label{ts_Herlihy_pre_local_atomicity}
Let $\beta$ be a finite schedule of $H_X(R)$ such that
the behavior of $\beta$ is pseudotime object well-formed.
Suppose that $\beta$ can lead to state $s$.
Let $T$ be in $\ms{s.nonorphans}$.
Let $\xi$ be the result of ordering the operations $(T',v') $
in $\ms{s.commit-requested}$ such
that $T'$ is visible to $T$ in s in $\ms{s.time}$ order.
Then $\ms{perform}(\xi)$ is a behavior of $S_X$.
\end{lemma}  

\begin{proof}
Consider any operation $(T',v')$ in $\xi$.
By claim 4 of Lemma \ref{ts_Herlihy_object_state_2},
$\ms{perform}(\eta)$ is a behavior of $S_X$,
where $\eta$ is the result of ordering the operations $(T'',v'') 
\in \ms{s.commit-requested}$ with $T''$ visible to $T'$ in $s$ and
$\ms{s.time}(T'') \leq \ms{s.time}(T')$, in $\ms{s.time order}$.
Since (by Claim 3 of Lemma \ref{ts_Herlihy_object_state_2}),
$\eta$ is an $R$-closed subsequence of $\xi$ containing $(T',v')$,
the fact that $R$ is a serial dependency relation implies that
$\ms{perform}(\xi)$ is a behavior of $S_X$.
\end{proof}

Now one can prove that a data object is locally static atomic if it
is implemented using the algorithm described in this section.

\begin{proposition}
\label{ts_Herlihy_local_atomicity}
$H_X(R)$ is locally static atomic.
\end{proposition}    

\begin{proof}
Let $\beta$ be a finite pseudotime object well-formed behavior of $H_X(R)$,
and $T$ a transaction name that is not a local orphan in $\beta$.
Let $S$ be the set of operations occurring in $\beta$ whose
transactions are locally visible to $T$ in $\beta$.
Then $\ms{local-view}(\beta,T) = \ms{perform}(\xi)$, where $\xi$ is the
result of ordering $S$ according to the order $R =
\ms{local-pseudotime-order}(\beta)$ on the transaction components.
The proof must show that $\ms{local-view}(\beta,T)$ is
a behavior of $S_X$.

Since $H_X(R)$ has no internal actions, $\beta$ is a schedule of $H_X(R)$.
Choose a state $s$ of $H_X(R)$ such that $\beta$ can lead to $s$.
Since $T$ is not a local orphan in $\beta$, $T$ is not in $\ms{s.nonorphans}$,
by Lemma \ref{ts_Herlihy_object_state_1}.
Furthermore any transaction is locally visible to $T$ in $\beta$ if and
only if it is visible to $T$ in $s$, and the order defined by $\ms{s.time}$
is the same as $R$.

Now the result is immediate from Lemma \ref{ts_Herlihy_pre_local_atomicity}. 
\end{proof}       

As a consequence, using Theorem \ref{ts_local_static_implies_static},
one sees that $H_X(R)$ is static atomic.

\section{Discussion}

This chapter focussed the ideas developed in Chapter
\ref{serializability-chapter} to apply to many timestamp-based algorithms.
It defined a local correctness property,
static atomicity,
that affords useful modularity,
both in decomposing proofs and in building systems.
Using this modularity,
correctness proofs of particular algorithms are split into two parts:  
one showing
that static atomicity is sufficient to ensure global atomicity,
and another showing that particular algorithms ensure static atomicity.
(The two main
algorithms considered in this chapter actually satisfy 
a sufficient condition for static atomicity, called local static atomicity.)
The first part of the proof need be done only once;
the second part must be done for each separate algorithm.
In building systems, this decomposition allows us to use different
algorithms at different objects, as long as each ensures
static atomicity.

The chapter began with appropriate definitions culminating in
the Static Atomicity Theorem, which shows 
that static atomicity is sufficient to ensure global atomicity,
Then local static atomicity is defined and shown to imply static 
atomicity.
Finally, generalizations of algorithms due to
Reed and Herlihy are presented,
and shown to ensure local static atomicity.
%In later chapters,
%the algorithms and proof techniques are extended to provide
%an integrated treatment of optimistic and pessimistic techniques,
%with each access making an independent decision whether
%to run optimistically or pessimistically.


\subsection{Bibliographic Notes}
The local static atomicity
condition generalizes work of Weihl for transaction systems
without nesting  \cite{Weihl84,Weihl89a}.

Herlihy's algorithm was originally described for single-level
transaction systems \cite{Herlihy87}.
It is extended here to encompass nested transactions,
and generalized slightly,
by testing for conflicts on {\em ratchet locks} only for non-orphan transactions.
Herlihy's algorithm does not release ratchet locks when a transaction aborts,
so conflicts on ratchet locks are tested against all transactions,
aborted or not.
This is similar to the way Reed's algorithm \cite{Reed78}
maintains only the maximum timestamp for a reader of a given version,
regardless of whether the readers have committed or aborted.

\section{Exercises}

\begin{enumerate}
%[[[A 7/91
\item
\label{ts-simple-exc}
Prove Lemma \ref{ts_pseudotime_assigned}.

%[[[A 11/91
\item
\label{ts-queue-exercise1}
Show that for the sequence $\beta$ given in Example 
\ref{ts-queue-system-ex1}, and for each object name $X$ in the system,
$\ms{view}(\ms{serial}(\beta),T_0,R,X)$ is 
a behavior of $S_{X}$, where 
$R = \ms{pseudotime-order}(\beta)$.
%]]]

\item
\label{reed-well-formed-exc}
Prove Lemma \ref{ts_pseudotimeobject_is_well-formed}.

%[[[A 11/91
\item
\label{reed-example-exercise1}
For the pseudotime object $R_{X_A}$ of Example \ref{reed-example}, and the
sequences $\beta$ and $\beta'$ given there, show
that $\ms{local-view}(\beta\beta',T_{V6.A})$ has the value given.
Also calculate $\ms{local-view}(\beta\beta',T_{V5.A})$. Show that
both are finite behaviors of the read/write serial object automaton $S_{X_A}$.
%]]]

\item
\label{ts_possibilities-check-exercise}
Complete the details of the proof of Theorem
\ref{ts_R1_implements}.
%]]]

%[[[A 11/91
\item
Consider the read/write object $X_A$ in the message queue system of Example
\ref{ss-queue-system-example}, and let $R1_{X_A}$ be the pseudotime object automaton
corresponding to $X_A$, using the concrete version of Reed's algorithm
presented in Section \ref{ts-reed-concrete-section}. Show that the sequence $\beta$
of Example \ref{reed-example} is {\em not} a schedule of $R1_{X_A}$. This implies that
$R_{X_A}$ does not implement $R_{X_A}$, since $\beta$ is a schedule of $R_{X_A}$.
%]]]


\item
Design and verify a more space-efficient but restrictive variant of
Reed's concrete implementation $\rms{R1}_X$, 
where the maximum time of a reading transaction is kept only 
for the {\em current} version (that whose writer has the highest timestamp
among non-orphan writers) and all other versions are presumed to exist
in the pseudotime interval from their writer until the timestamp of the 
writer with the closest higher timestamp.

%[[[
\item
Design and verify an algorithm similar to Reed's for a general serial object.
Accesses that are obliterating should be treated like writes (they cause a new version to be
produced), accesses that
are transparent like  reads (they return a value based on the closest
preceding version in timestamp order), and other
accesses, that are neither transparent nor obliterating, are treated as a combination
of read and write.
% A 5/91]]]

%[[[
\item
Suppose $X$ is an object name where the serial object $S_X$ is a read/write object.
Let $R$ be the serial dependency relation  described in Example \ref{rw-object-serial-depend},
and $H_X(R)$ be the object constructed using Herlihy's algorithm with
the relation.
Show that $R_X$ is not an implementation of $H_X(R)$, that is Reed's algorithm allows
some behaviors not allowed by Herlihy's.
%A 5/91]]] Answer: Herlihy's waits till all writers with lower timestamps are visible to
%a reader, not only the closest writer as with Reed

%[[[A 11/91
\item
\label{ts-herlihy-example-ex}
Consider the pseudotime object $H_{X_Q}(R_2)$ and its schedule $\beta$ that leads to
state $s$, as given
in Example \ref{herlihy-example}. Show that in $s$
$\RQCM{T_{R6.0}}{6}$ is enabled, but there is no value $v$ for
which $\RQCM{T_{R4.0}}{v}$ is enabled.
%]]]

%[[[A 7/91
\item
\label{herlihy-exercise}
Design a space-efficient implementation of a Herlihy object,
using ideas similar to those for Reed's implementation $\rms{R1}_X$.
The algorithm
should group operations together (for example,
an object based on a bank account serial object
might treat all deposit accesses as one group,
all withdrawals with non-zero return value as another, and so on).
The object should maintain pseudotime information for active accesses;
for those that have requested to commit, it 
should keep a single pseudotime
for each group, representing the largest pseudotime of an access 
belonging to the group.
Prove the implementation correct using a possibilities mapping.
%]]]
%[[[A 11/91
\item
\label{exercise-static-mixed}
Consider the pseudotime system that uses the system type and transaction automata
of the message queue system of Example \ref{ss-queue-system-example}, with
pseudotime objects $R_{X_A}$
(as given in Example \ref{reed-example}), $H_{X_Q}(R_2)$ (as given in Example \ref{herlihy-example})
and $R_{X_B}$ (using Reed's algorithm).
Let $\beta_1$ denote the sequence
\schedlist{
\CRT{T_{R1.A3}}\\
\INFTMntab{X_A}{T_{R1.A3}, 4,1}\\
\INFTMntab{X_A}{T_{V1.A}, 3,3}\\
\CRT{T_{V1.A}}\\
\RQCMntab{T_{R1.A3}}{\qms{OK}}\\
\INFCMntab{X_A}{T_{R1.A3}}\\
\RQCMntab{T_{V1.A}}{0}\\
\INFCMntab{X_A}{T_{V1.B}}.
}
Let $beta_2$ denote
\schedlist{
\INFTMntab{X_Q}{T_{G6},2}\\
\INFTMntab{X_Q}{T_{R1.X}, 4,1}\\
\CRT{T_{G6}}\\
\RQCMntab{T_{G6}}{\qms{OK}}\\
\INFCMntab{X_Q}{T_{G6}}\\
\RQCMntab{T_{R1.X}}{6}\\
\INFCMntab{X_Q}{T_{V1}}\\
\INFCMntab{X_Q}{T_{R1.X}}\\
\INFCMntab{X_Q}{T_{V1.A}},
}
and let $\beta_3$ denote
\schedlist{
\CRT{T_{R1.B3}}\\
\INFTMntab{X_B}{T_{R1.B3}, 4,2}\\
\INFTMntab{X_B}{T_{V1.B}, 3,1}\\
\CRT{T_{V1.B}}\\
\RQCMntab{T_{R1.B3}}{\qms{OK}}\\
\INFCMntab{X_B}{T_{R1.B3}}\\
\INFCMntab{X_B}{T_{R1}}\\
\RQCMntab{T_{V1.B}}{0}\\
\INFCMntab{X_B}{T_{V1.A}}.
}
Show that each $\beta_i$ is a behavior of the appropriate pseudotime object.
Construct a behavior $\beta$ of the system, so that
$\beta|R_{X_A} = \beta_1$, $\beta|H_{X_Q}(R_2) = \beta_2$, and
$\beta|R_{X_B} = \beta_3$. 
Show that $\beta$ is atomic for $T_0$ 
by giving a serial behavior with the same projection as $\beta$ on $T_0$.
%]]]


\item
\label{moss-not-static}
Develop a pseudotime object for
a read/write serial object $S_X$
using Moss's algorithm as described in
Section \ref{rw-section}. The object should be almost identical
to $\rms{M1}_X$ presented there, except that there should
be extra
\inftm{} actions which have no effect on the state.
Show that this object is {\em not} locally static atomic.
Consider the pseudotime system like that in Exercise
\ref{static-exercise-mixed}, except that (for the object name $X_B$)
Moss's algorithm is used
instead of $R_{X_B}$.
Find an execution of this system that is not atomic for $T_0$.
Hint: use the same $\beta_1$ and $\beta_2$ as in exercise \ref{static-exercise-mixed},
and use for $X_B$ a sequence just like $\beta_3$ except
 with a different return value for $T_{V1.B}$.
\end{enumerate}
