\newtheorem{property}{Property}

Specifying the desired consistency properties of our system requires
introducing a few new definitions. The first requirement we set forth
is a standard one:

\begin{property}[Global Serializability]
  There exists a global serial ordering of all transactions such that
  the results of all transactions are consistent with this ordering.
\end{property}

Note that, although a serial ordering exists, we have not stated
\emph{what} that serial ordering may be. In particular, the serial
schedule may not correspond to the wall-clock-ordering of transaction
commit times.

We require that the staleness of data seen by a transaction can be
limited. (This also eliminates several vacuous solutions!)
Specifically:

\begin{property}[Freshness]
  A read-only transaction sees a consistent state of the database at a
  time no earlier than $\epsilon$ before the time it began, where
  $\epsilon$ is a property of the transaction.
\end{property}

If a single user (or program) ran a succession of transactions, and
their results were executed out of order, chaos would ensue, so we
need the following property:

\begin{property}[Local Causality]
  A transaction will see the effects of all transactions on the local
  node that committed before it started.
\end{property}

This local causality property stands in contrast to the typical
causality property of distributed transaction systems, where a
transaction will see the effects of \emph{all} transactions that
committed before it started. Section~\ref{sec:overview} argues that
this is a reasonable property.

Finally, our protocol allows the following nice property:

\begin{property}[Conflict-freeness]
  Read-only transactions are never aborted, and can be executed
  without blocking for another transaction.
\end{property}

Knowing that read-only transactions cannot be aborted can greatly
simplify programming, since there is no need to be prepared to retry
the transaction. 


%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "report"
%%% TeX-PDF-mode: t
%%% End: