papers/lp-010-quasar-stm-3/sections/05-visibility-rule.tex

\section{Visibility Rule}

\label{sec:visibility}
%% ============================================================================

QuasarSTM serves both Nova (linear consensus order) and Nebula (DAG
consensus order) execution modes. The visibility rule is parameterised
over a mode-specific \emph{ordering oracle}.

\subsection{Ordering Oracle}

\begin{definition}[Ordering oracle]
\label{def:order-oracle}
An ordering oracle is a tuple
$\mathit{StmOrderOracle} = (\mathit{mode},\, {\preceq_{\mathrm{can}}},\,
\mathit{idx})$ where
\begin{itemize}[leftmargin=2em,nosep]
\item $\mathit{mode} \in \{\textsc{Nova},\, \textsc{Nebula}\}$;
\item $\preceq_{\mathrm{can}}$ is a total order over committed
      transactions (Nova) or a strict partial order with deterministic
      linear extension over the ready cut (Nebula);
\item $\mathit{idx}$ is a canonical-index function from transaction
      identifiers to $\mathbb{N}$ that respects
      $\preceq_{\mathrm{can}}$.
\end{itemize}
The oracle is supplied by Quasar before the round begins; it is
fixed for the duration of the round.
\end{definition}

The oracle is the only consensus-order surface the STM engine
consumes. It abstracts the linear/DAG distinction at a single point.

\subsection{Nova Visibility}

\begin{definition}[Nova visible version]
\label{def:visible-nova}
Let $T_i$ be a transaction with canonical index $i$ and let $k$ be a
storage key. Under Nova,
\[
\mathit{visible\_version}(T_i, k) =
v(\,T_j,\, k\,) \quad \text{where} \quad
j = \max \bigl\{\, j' < i \;:\; T_{j'} \text{ wrote } k,\;
\text{and } v(T_{j'},k) \text{ is valid} \,\bigr\}.
\]
If no such $j$ exists, the visible version is the parent-state
baseline of $k$.
\end{definition}

A version $v(T_j, k)$ is \emph{valid} if the latest incarnation of
$T_j$ that wrote $k$ has not been invalidated by a subsequent repair
(\S\ref{sec:repair}, repair monotonicity). Speculative versions of
later incarnations supersede earlier ones; only the topmost valid
incarnation participates in visibility.

\subsection{Nebula Visibility}

In Nebula, transactions are vertices in a causal DAG; the canonical
order is a deterministic linear extension over the Prism cut.

\begin{definition}[Nebula visible version]
\label{def:visible-nebula}
Let $v_i$ be a vertex (transaction) in a Nebula round and let $k$ be
a storage key. Let
$\mathit{Pred}^*(v_i)$ be the set of vertices causally before $v_i$ in
the DAG (transitive predecessors under the happens-before relation).
Under Nebula,
\[
\mathit{visible\_version}(v_i, k) =
v(\,v_j,\, k\,) \quad \text{where} \quad
v_j = \mathrm{argmax}_{\preceq_{\mathrm{can}}}
      \bigl\{\, v_{j'} \in \mathit{Pred}^*(v_i)\,:\,
      v_{j'} \text{ wrote } k,\;
      v(v_{j'},k) \text{ valid} \,\bigr\}.
\]
The argmax is taken under the deterministic linear extension supplied
by the ordering oracle, which decides ties between concurrent (DAG-
incomparable) writers.
\end{definition}

\begin{lemma}[Tie-break determinism]
\label{lem:tie-determinism}
For any two concurrent vertices $v_a, v_b \in \mathit{Pred}^*(v_i)$
with $v_a \,\|\, v_b$ in the DAG, the ordering oracle's linear
extension yields a fixed total order independent of execution
ordering, scheduling, or non-determinism on the GPU.
\end{lemma}

\begin{proof}[Sketch]
The Nebula linear extension is computed deterministically from the
DAG structure (Photon proposal hashes, Wave finalization indices)
together with a fixed tie-break rule on \textsf{(round, vertex hash)}.
None of those inputs depend on execution. The lemma is structural.
\end{proof}

\subsection{Mode-Independent Statement}

\begin{definition}[Visible version]
\label{def:visible}
For an ordering oracle $\mathcal{O}$ and a transaction-key pair
$(T, k)$, the visible version $\mathit{visible\_version}_\mathcal{O}(T,
k)$ is given by Definition~\ref{def:visible-nova} when
$\mathcal{O}.\mathit{mode} = \textsc{Nova}$ and by
Definition~\ref{def:visible-nebula} when $\mathcal{O}.\mathit{mode} =
\textsc{Nebula}$.
\end{definition}

The Tier-2 validation predicate (Definition~\ref{def:tier2}) refers to
exactly this $\mathit{visible\_version}_\mathcal{O}$.

\subsection{Canonical Version Order}

\begin{definition}[Canonical version order]
\label{def:version-order}
Versions are totally ordered by the lexicographic key
$(\mathit{key},\, \mathit{tx\_index},\, \mathit{incarnation})$. The
visible-chain on each key, projected from the global version arena,
respects this order under collision-free indexing.
\end{definition}

\begin{remark}[No race-dependent visibility]
\label{rem:no-race}
Two GPU threads writing speculative versions for the same key under
the same canonical index but different incarnations produce a
deterministically sorted visible chain. There is no tie-break by
write timestamp, no first-writer-wins, no last-writer-wins. The
ordering is structural.
\end{remark}


%% ============================================================================