X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke-formulae.git;a=blobdiff_plain;f=strategy.tex;h=0f03ddb9883200fed514b821df14948994e78aca;hp=a1632cb42602b161221d7eafd774976e5f1cba68;hb=0c3db5a204f508f8a8a59c74ea8a9bf56d3ab59e;hpb=ed18b8e28af4811ea9854499baf725d1615f9391 diff --git a/strategy.tex b/strategy.tex index a1632cb..0f03ddb 100644 --- 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). +\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} @@ -212,176 +217,161 @@ and corresponding merge bases $M^{\pcn}_i = M_i$. \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} -\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} +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