strategy: traversal wip proofs

[topbloke-formulae.git] / strategy.tex

Here we describe the update algorithm.  This is responsible for
refreshing patches against updated versions of their dependencies,
for merging different versions of the various braches created by
distributed development, and for implementing decisions to add and
remove dependencies from patches.

Broadly speaking the update proceeds as follows: during the Ranking
phase we construct the intended graph of dependencies between patches
(and incidentally select a merge order for the base branch of each
patch).  Then during the Traversal phase we walk that graph from the
bottom up, constructing for each patch by a series of merges and other
operations first a new base branch head commit and then a new tip
branch head commit.  These new head commits are maximums - that is,
each has as ancestors all of its branches' sources and indeed all
relevant commits in that branch.

We have two possible strategies for constructing new base branch
heads: we can either Merge (works incrementally even if there the
patch has multiple dependencies, but may sometimes not be possible) or
we can Regenerate (trivial if there is a single dependency, and is
always possible, but may involve the user re-resolving conflicts if
there are multiple dependencies).

\section{Notation}

\begin{basedescript}{
\desclabelwidth{5em}
\desclabelstyle{\nextlinelabel}
}
\item[ $\depsreqof{K}$ ]
The set of direct dependencies (in the form $\py$)
requested in the commit $K$ ($K \in \pn$) for the patch $\p$.

\item[ $\pc \hasdirdep \p$ ]
The patch $\pc$ has as a direct dependency the
patch $\p$.  This is an acyclic relation.

\item[ $\p \hasdep \pq$ ]
The patch $\p$ has as direct or indirect dependency the
patch $\pq$.
Acyclic; the completion of $\hasdirdep$ into a
partial order.

\item[ $\pendsof{\set J}{\p}$ ]
Convenience notation for
the $\le$-maximal elements of $\bigcup_{J \in \set J} \pendsof{J}{\p}$
(where $\set J$ is some set of commits).

\item[ $\pendsof{\set X}{\p} \le T$ ]
Convenience notation for
$\bigforall_{E \in \pendsof{\set X}{\p}} E \le T$

%\item[ $\set E_{\pc}$ ]
%$ \bigcup_i \pendsof{S_{\pc,i}}{\pc} $.
%All the ends of $\pc$ in the sources.

%\item[ $ \tipzc, \tipcc, \tipuc, \tipfc $ ]
%The git ref for the Topbloke commit set $\pc$: respectively,
%the original, current, updated, and final values.

\end{basedescript}

\stdsection{Inputs to the update algorithm}

\begin{basedescript}{
\desclabelwidth{5em}
\desclabelstyle{\nextlinelabel}
}
\item[ $\pc_0$ ]
The topmost patch which we are trying to update.  This and
all of its dependencies will be updated.

\item[ $h : \pc^{+/-} \mapsto \set H_{\pc^{+/-}}$ ]
Function for getting the existing heads $\set H$ of the branch $\pc^{+/-}$.
These are the heads which will be merged and used in this update.
This will include the current local and remote git refs, as desired.

\item[ $g : \pc, \Gamma \mapsto \Gamma'$ ]
Function to allow explicit adjustment of the direct dependencies
of $\pc$.  It is provided with a putative set of direct dependencies
$\Gamma$ computed as an appropriate merge of the dependencies requested by the
sources and should return the complete actual set $\Gamma'$ of direct
dependencies to use.  This allows the specification of any desired
(acyclic) relations $\hasdirdep$ and $\hasdep$.

\end{basedescript}

\stdsection{Important variables and values in the update algorithm}

\begin{basedescript}{
\desclabelwidth{5em}
\desclabelstyle{\nextlinelabel}
}
\item[ $\Gamma_{\pc}$ ]
The desired direct dependencies of $\pc$, a set of patches.

\item[ $\allpatches$ ]
The set of all the patches we are dealing with (constructed
during the update algorithm).

\item[ $\tipcn, \tipcy$ ]
The new tips of the git branches $\pcn$ and $\pcy$, containing
all the correct commits (and the correct other patches), as
generated by the Traversal phase of the update algorithm.

\end{basedescript}

\section{Ranking phase}

We run the following algorithm:
\begin{enumerate}
\item Set $\allpatches = \{ \}$.
\item Repeatedly:
\begin{enumerate}
\item Clear out the graph $\hasdirdep$ so it has no edges.
\item Execute $\alg{Rank-Recurse}(\pc_0)$
\item Until $\allpatches$ remains unchanged.
\end{enumerate}
\end{enumerate}

$\alg{Rank-Recurse}(\pc)$ is:
\begin{enumerate}

\item If we have already done $\alg{Rank-Recurse}(\pc)$ in this
ranking iteration, do nothing.  Otherwise:

\item Add $\pc$ to $\allpatches$ if it is not there already.

\item Set
$$
  \set S \iassign h(\pcn)
     \cup 
        \bigcup_{\p \in \allpatches}
        \bigcup_{H \in h(\pn) \lor H \in h(\py)}
         \{ \baseof{E} \; | \; E \in \pendsof{H}{\pcy} \}
$$

and $W \iassign w(h(\pcn))$

\item While $\exists_{S \in \set S} S \ge W$,
update $W \assign S$ and $\set S \assign \set S \, \backslash \{ S \}$

(This will often remove $W$ from $\set S$.  Afterwards, $\set S$
is a collection of heads to be merged into $W$.)

\item Choose an ordering of $\set S$, $S_i$ for $i=1 \ldots n$.

\item For each $S_i$ in turn, choose a corresponding $M_i$
such that $$
   M_i \le S_i \land \left[
   M_i \le W \lor \bigexists_{j<i} M_i \le S_j
   \right]
$$

\item Set $\Gamma \iassign \depsreqof{W}$.

If there are multiple candidates we prefer $M_i \in \pcn$
if available.

\item For each $i \ldots 1..n$, update our putative direct
dependencies:
$$
\Gamma \assign \setmergeof{
    \Gamma
  }{
    \begin{cases}
     M_i \in \pcn :     & \depsreqof{M_i} \\
     M_i \not\in \pcn : & \{ \}
    \end{cases}
  }{
    \depsreqof{S_i}
  }
$$

TODO define $\setmerge$

\item Finalise our putative direct dependencies
$
\Gamma \assign g(\pc, \Gamma)
$

\item For each direct dependency $\pd \in \Gamma$,

\begin{enumerate}
\item Add an edge $\pc \hasdirdep \pd$ to the digraph (adding nodes
as necessary).
If this results in a cycle, abort entirely (as the function $g$ is
inappropriate; a different $g$ could work).
\item Run $\alg{Rank-Recurse}(\pd)$.
\end{enumerate}

\end{enumerate}

\subsection{Results of the ranking phase}

By the end of the ranking phase, we have recorded the following
information:

\begin{itemize}
\item
$ \allpatches, \hasdirdep $ and hence the completion of $\hasdirdep$
into the partial order $\hasdep$.

\item
For each $\pc \in \allpatches$,
the base branch starting point commit $W^{\pcn} = W$.

\item
For each $\pc$,
the direct dependencies $\Gamma^{\pc} = \Gamma$.

\item
For each $\pc$,
the ordered set of base branch sources $\set S^{\pcn} = \set S,
S^{\pcn}_i = S_i$
and corresponding merge bases $M^{\pcn}_i = M_i$.

\end{itemize}

\subsection{Proof of termination}

$\alg{Rank-Recurse}(\pc)$ recurses but only downwards through the
finite graph $\hasdirdep$, so it must terminate.  

The whole ranking algorithm iterates but each iteration involves
adding one or more patches to $\allpatches$.  Since there are
finitely many patches and we never remove anything from $\allpatches$
this must complete eventually.

$\qed$

\section{Traversal phase --- algorithm}

(In general, unless stated otherwise below, when we generate a new
commit $C$ using one of the commit kind algorith, we update
$W \assign C$.  In any such case where we say we're going to Merge
with $L = W$, if $R \ge W$ we do not Merge but instead simply set
$W \assign R$.)


For each patch $\pc \in \allpatches$ in topological order by $\hasdep$,
lowest first:

\begin{enumerate}

\item Optionally, attempt
 $\alg{Merge-Base}(\pc)$.  This may or may not succeed.

\item If this didn't succeed, or was not attempted, execute
 $\alg{Recreate-Base}(\pc)$.

\item Then in any case, execute
 $\alg{Merge-Tip}(\pc)$.

\end{enumerate}

After processing each $\pc$ we will have created:

\begin{itemize}

\item $\tipcn$ and $\tipcy$ such that $\baseof{\tipcy} = \tipcn$.

\end{itemize}

\subsection{$\alg{Merge-Base}(\pc)$}

This algorithm attempts to construct a suitably updated version of the
base branch $\pcn$ using some existing version of $\pcn$ as a starting
point.

It should be executed noninteractively.  Specifically, if any step
fails with a merge conflict, the whole thing should be abandoned.
This avoids asking the user to resolve confusing conflicts.  It also
avoids asking the user to pointlessly resolve conflicts in situations
where we will later discover that $\alg{Merge-Base}$ wasn't feasible
after all.

If $\pc$ has only one direct dependency, this algorithm should not be
used as in that case $\alg{Recreate-Base}$ is trivial and guaranteed
to generate a perfect answer, whereas this algorithm might involve
merges and therefore might not produce a perfect answer if the
situation is complicated.

Initially, set $W \iassign W^{\pcn}$.

\subsubsection{Bases and sources}

In some order, perhaps interleaving the two kinds of merge:

\begin{enumerate}

\item For each $\pd \isdirdep \pc$, find a merge base
$M \le W,\; \le \tipdy$ and merge $\tipdy$ into $W$.
That is, use $\alg{Merge}$ with $L = W,\; R = \tipdy$.
(Dependency Merge.)

\item For each $S \in S^{\pcn}_i$, merge it into $W$.
That is, use $\alg{Merge}$ with $L = W,\; R = S,\; M = M^{\pcn}_i$.
(Base Sibling Merge.)

\end{enumerate}

\subsubsection{Fixup}

Execute $\alg{Fixup-Base}(W,\pc)$.


\subsection{$\alg{Recreate-Base}(\pc)$}

\begin{enumerate}

\item

Choose a $\hasdep$-maximal direct dependency $\pd$ of $\pc$.

\item

Use $\alg{Create Base}$ with $L$ = $\pdy,\; \pq = \pc$ to generate $C$
and set $W \iassign C$.  (Recreate Base Beginning.)

\item

Execute the subalgorithm $\alg{Recreate-Recurse}(\pc)$.

\item

Declare that we contain all of the relevant information from the
sources.  That is, use $\alg{Pseudo-merge}$ with $L = W, \;
\set R = \{ W \} \cup \set S^{\pcn}$.
(Recreate Base Final Declaration.)

\end{enumerate}

\subsubsection{$\alg{Recreate-Recurse}(\pd)$}

\begin{enumerate}

\item Is $W \haspatch \pd$ ?  If so, there is nothing to do: return.

\item TODO what about non-Topbloke base branches

\item Use $\alg{Pseudo-Merge}$ with $L = W,\; \set R = \{ \tipdn \}$.
(Recreate Base Dependency Base Declaration.)

\item For all $\hasdep$-maximal $\pd' \isdirdep \pd$,
execute $\alg{Recreate-Recurse}(\pd')$.

\item Use $\alg{Merge}$ to apply $\pd$ to $W$.  That is,
$L = W, \; R = \tipdy, \; M = \baseof{R} = \tipdn$.
(Recreate Reapply.)

\end{enumerate}


\subsection{$\alg{Merge-Tip}(\pc)$}

\begin{enumerate}

\item TODO CHOOSE/REFINE W AND S as was done during Ranking for bases

\item $\alg{Merge}$ from $\tipcn$.  That is, $L = W, \;
R = \tipcn$ and choose any suitable $M$.  (Tip Base Merge.)

\item For each source $S \in \set S^{\pcy}$,
$\alg{Merge}$ with $L = W, \; R = S$ and any suitable $M$.
(Tip Source Merge.)

\end{enumerate}


\section{Traversal phase --- proofs}

For each operation called for by the traversal algorithms, we prove
that the commit generation preconditions are met.

\subsection{Tip Base Merge}