strategy: traversal wip proofs

[topbloke-formulae.git] / strategy.tex

diff --git a/strategy.tex b/strategy.tex
index a1632cb42602b161221d7eafd774976e5f1cba68..0f03ddb9883200fed514b821df14948994e78aca 100644 (file)
--- a/strategy.tex
+++ b/strategy.tex
@@ -98,6 +98,11 @@ The desired direct dependencies of $\pc$, a set of patches.
 The set of all the patches we are dealing with (constructed
 during the update algorithm).
 
 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}
 \end{basedescript}
 
 \section{Ranking phase}


@@ -212,176 +217,161 @@ and corresponding merge bases $M^{\pcn}_i = M_i$.
 
 \end{itemize}
 
 
 \end{itemize}
 

-\section{Traversal phase}
+\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 $C \in \allpatches$ in topological order by $\hasdep$,
+For each patch $\pc \in \allpatches$ in topological order by $\hasdep$,

 lowest first:
 
 \begin{enumerate}
 
 lowest first:
 
 \begin{enumerate}
 

-\item Optionally, attempt $\alg{Merge-Base}(\pc)$.
+\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}
 
 
 \end{enumerate}
 

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

 
 

-\section{Planning phase}
+\begin{itemize}

 
 

-The results of the planning phase consist of: 
-\begin{itemize*}
-\item{ The relation $\hasdirdep$ and hence the partial order $\hasdep$. }
-\item{ For each commit set $\pc$, a confirmed set of sources $\set S_{\pc}$. }
-\item{ For each commit set $\pc$, the order in which to merge the sources
-        $E_{\pc,j} \in \set E_{\pc}$. }
-\item{ For each $E_{\pc,j}$ an intended merge base $M_{\pc,j}$. }
-\end{itemize*}
+\item $\tipcn$ and $\tipcy$ such that $\baseof{\tipcy} = \tipcn$.

 
 

-We use a recursive planning algorith, recursing over Topbloke commit
-sets (ie, sets $\py$ or $\pn$).  We'll call the commit set we're
-processing at each step $\pc$.
-At each recursive step 
-we make a plan to merge all $\set E_{\pc} = \{ E_{\pc,j \ldots} \}$
-and all the direct contributors of $\pc$ (as determined below)
-into $\tipzc$, to make $\tipfc$.
+\end{itemize}

 
 

-We start with $\pc = \pl$ where $\pl = \patchof{L}$.
+\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.

 
 

-\subsection{Direct contributors for $\pc = \pcn$}
+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.

 
 

-The direct contributors of $\pcn$ are the commit sets corresponding to
-the tip branches for the direct dependencies of the patch $\pc$.  We
-need to calculate what the direct dependencies are going to be.
+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.

 
 

-Choose an (arbitrary, but ideally somehow optimal in
-a way not discussed here) ordering of $\set E_{\pc}$, $E_{\pc,j}$
-($j = 1 \ldots m$).
-For brevity we will write $E_j$ for $E_{\pc,j}$.
-Remove from that set (and ordering) any $E_j$ which
-are $\le$ and $\neq$ some other $E_k$.
+Initially, set $W \iassign W^{\pcn}$.

 
 

-Initially let $\set D_0 = \depsreqof{\tipzc}$.
-For each $E_j$ starting with $j=1$ choose a corresponding intended
-merge base $M_j$ such that $M_j \le E_j \land M_j \le T_{\pc,j-1}$.
-Calculate $\set D_j$ as the 3-way merge of the sets $\set D_{j-1}$ and
-$\depsreqof{E_j}$ using as a base $\depsreqof{M_j}$.  This will
-generate $D_m$ as the putative direct contributors of $\pcn$.
+\subsubsection{Bases and sources}
+
+In some order, perhaps interleaving the two kinds of merge:
+
+\begin{enumerate}

 
 

-However, the invocation may give instructions that certain direct
-dependencies are definitely to be included, or excluded.  As a result
-the set of actual direct contributors is some arbitrary set of patches
-(strictly, some arbitrary set of Topbloke tip commit sets).
+\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.)

 
 

-\subsection{Direct contributors for $\pc = \pcy$}
+\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.)

 
 

-The sole direct contributor of $\pcy$ is $\pcn$.
+\end{enumerate}

 
 

-\subsection{Recursive step}
+\subsubsection{Fixup}

 
 

-For each direct contributor $\p$, we add the edge $\pc \hasdirdep \p$
-and augment the ordering $\hasdep$ accordingly.
+Execute $\alg{Fixup-Base}(W,\pc)$.

 
 

-If this would make a cycle in $\hasdep$, we abort . The operation must
-then be retried by the user, if desired, but with different or
-additional instructions for modifying the direct contributors of some
-$\pqn$ involved in the cycle.

 
 

-For each such $\p$, after updating $\hasdep$, we recursively make a plan
-for $\pc' = \p$.
+\subsection{$\alg{Recreate-Base}(\pc)$}

 
 

+\begin{enumerate}

 
 

+\item

 
 

-\section{Execution phase}
+Choose a $\hasdep$-maximal direct dependency $\pd$ of $\pc$.

 
 

-We process commit sets from the bottom up according to the relation
-$\hasdep$.  For each commit set $\pc$ we construct $\tipfc$ from
-$\tipzc$, as planned.  By construction, $\hasdep$ has $\patchof{L}$
-as its maximum, so this operation will finish by updating
-$\tipca{\patchof{L}}$ with $\tipfa{\patchof{L}}$.
+\item

 
 

-After we are done with each commit set $\pc$, the
-new tip $\tipfc$ has the following properties:
-\[ \eqn{Tip Sources}{
-  \bigforall_{E_i \in \set E_{\pc}} \tipfc \ge E_i
-}\]
-\[ \eqn{Tip Dependencies}{
-  \bigforall_{\pc \hasdep \p} \tipfc \ge \tipfa \p
-}\]
-\[ \eqn{Perfect Contents}{
-  \tipfc \haspatch \p \equiv \pc \hasdep \py
-}\]
+Use $\alg{Create Base}$ with $L$ = $\pdy,\; \pq = \pc$ to generate $C$
+and set $W \iassign C$.  (Recreate Base Beginning.)

 
 

-For brevity we will sometimes write $\tipu$ for $\tipuc$, etc.  We will start
-out with $\tipc = \tipz$, and at each step of the way construct some
-$\tipu$ from $\tipc$.  The final $\tipu$ becomes $\tipf$.
+\item

 
 

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

 
 

-Firstly, we will check each $E_i$ for being $\ge \tipc$.  If
-it is, are we fast forward to $E_i$
---- formally, $\tipu = \text{max}(\tipc, E_i)$ ---
-and drop $E_i$ from the planned ordering.
+\item

 
 

-Then we will merge the direct contributors and the sources' ends.
-This generates more commits $\tipuc \in \pc$, but none in any other
-commit set.  We maintain
-$$
- \bigforall_{\p \isdep \pc}
- \pancsof{\tipcc}{\p} \subset
-   \pancsof{\tipfa \p}{\p}
-$$
-\proof{
- For $\tipcc = \tipzc$, $T$ ...WRONG WE NEED $\tipfa \p$ TO BE IN $\set E$ SOMEHOW
-}
+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.)

 
 

-\subsection{Merge Contributors for $\pcy$}
+\end{enumerate}

 
 

-Merge $\pcn$ into $\tipc$.  That is, merge with
-$L = \tipc, R = \tipfa{\pcn}, M = \baseof{\tipc}$.
-to construct $\tipu$.
+\subsubsection{$\alg{Recreate-Recurse}(\pd)$}

 
 

-Merge conditions:
+\begin{enumerate}

 
 

-Ingredients satisfied by construction.
-Tip Merge satisfied by construction.  Merge Acyclic follows
-from Perfect Contents and $\hasdep$ being acyclic.
+\item Is $W \haspatch \pd$ ?  If so, there is nothing to do: return.

 
 

-Removal Merge Ends: For $\p = \pc$, $M \nothaspatch \p$; OK.
-For $\p \neq \pc$, by Tip Contents,
-$M \haspatch \p \equiv L \haspatch \p$, so we need only
-worry about $X = R, Y = L$; ie $L \haspatch \p$,
-$M = \baseof{L} \haspatch \p$.
-By Tip Contents for $L$, $D \le L \equiv D \le M$.  OK.~~$\qed$
+\item TODO what about non-Topbloke base branches

 
 

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

 
 

-Addition Merge Ends: If $\py \isdep \pcn$, we have already
-done the execution phase for $\pcn$ and $\py$.  By
-Perfect Contents for $\pcn$, $\tipfa \pcn \haspatch \p$ i.e.
-$R \haspatch \p$.  So we only need to worry about $Y = R = \tipfa \pcn$.
-By Tip Dependencies $\tipfa \pcn \ge \tipfa \py$.
-And by Tip Sources $\tipfa \py \ge $
+\item For all $\hasdep$-maximal $\pd' \isdirdep \pd$,
+execute $\alg{Recreate-Recurse}(\pd')$.

 
 

-want to prove $E \le \tipfc$ where $E \in \pendsof{\tipcc}{\py}$
+\item Use $\alg{Merge}$ to apply $\pd$ to $W$.  That is,
+$L = W, \; R = \tipdy, \; M = \baseof{R} = \tipdn$.
+(Recreate Reapply.)

 
 

-$\pancsof{\tipcc}{\py} = $
+\end{enumerate}

 
 
 
 

-computed $\tipfa \py$, and by Perfect Contents for $\py$
+\subsection{$\alg{Merge-Tip}(\pc)$}

 
 

+\begin{enumerate}

 
 

-with $M=M_j, L=T_{\pc,j-1}, R=E_j$,
-and calculate what the resulting desired direct dependencies file
-(ie, the set of patches $\set D_j$)
-would be.  Eventually we 
+\item TODO CHOOSE/REFINE W AND S as was done during Ranking for bases

 
 

-So, formally, we select somehow an order of sources $S_i$.  For each 
+\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.)

 
 

-Make use of the following recursive algorithm, Plan 
+\end{enumerate}

 
 
 
 

+\section{Traversal phase --- proofs}

 
 

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

 
 

- recursively make a plan to merge all $E = \pends$
+\subsection{Tip Base Merge}

 
 

-Specifically, in