1 \section{Traversal phase --- algorithm}
3 (In general, unless stated otherwise below, when we generate a new
4 commit $C$ using one of the commit kind recipies, we update
5 $W \assign C$. In any such case where we say we're going to Merge
6 with $L = W$, if $R \ge W$ we do not Merge but instead simply set
9 For each commit generation operation called for by the traversal
10 algorithms, we prove that the commit generation preconditions are met.)
12 For each patch $\pc \in \allpatches$ in topological order by $\hasdep$,
17 \item Optionally, attempt
18 $\alg{Merge-Base}(\pc)$. This may or may not succeed.
20 \item If this didn't succeed, or was not attempted, execute
21 $\alg{Recreate-Base}(\pc)$.
23 \item Then in any case, execute
24 $\alg{Merge-Tip}(\pc)$.
28 After processing each $\pc$ we will have created $\tipcn$ and $\tipcy$
31 \statement{Correct Base}{
32 \baseof{\tipcy} = \tipcn
34 \statement{Base Correct Contents}{
35 \tipcn \haspatch \pa E
39 \statement{Tip Covers Reachable}{
40 \tipcy \ge \pendsof{\allreachof{\pcy}}{\pcy}
42 \statement{Base Covers Inputs' Bases}{
43 \bigforall_{E \in \pendsof{\allsrcs}{\pcy}} \tipcn \ge \baseof{E}
45 \statement{Base Covers Base Inputs}{
46 \bigforall_{H \in \set H^{\pn}} \tipcn \ge H
49 \subsection{Reachability and coverage}
51 We ensure Tip Covers Reachable as follows:
54 \item We do not generate any commits $\in \py$ other than
55 during $\alg{Merge-Tip}(\py)$;
56 \item So at the start of $\alg{Merge-Tip}(\py)$,
57 $ \pendsof{\allreach}{\py} = \pendsof{\allsrcs}{\py} $
58 \item $\alg{Merge-tip}$ arranges that when it is done
59 $\tippy \ge \pendsof{\allreach}{\py}$ --- see below.
62 A corrolary is as follows:
63 \statement{Tip Covers Superior Reachable} {
64 \bigforall_{\pd \isdep \pc}
65 \tipdy \ge \pendsof{\allreachof{\pcy}}{\pdy}
68 No commits $\in \pdy$ are created other than during
69 $\alg{Merge-Tip}(\pd)$, which runs (and has thus completed)
70 before $\alg{Merge-Tip}(\pcy)$
71 So $\pendsof{\allreachof{\pcy}}{\pdy} =
72 \pendsof{\allreachof{\pdy}}{\pdy}$.
75 \subsection{Traversal Lemmas}
77 \statement{Tip Correct Contents}{
78 \tipcy \haspatch \pa E
80 \pa E = \pc \lor \pa E \isdep \pc
83 For $\pc = \pa E$, Tip Own Contents suffices.
84 For $\pc \neq \pa E$, Exclusive Tip Contents
85 gives $D \isin \tipcy \equiv D \isin \baseof{\tipcy}$
86 which by Correct Base $\equiv D \isin \tipcn$.
89 \subsection{$\alg{Merge-Base}(\pc)$}
91 This algorithm attempts to construct a suitably updated version of the
92 base branch $\pcn$ using some existing version of $\pcn$ as a starting
95 It should be executed noninteractively. Specifically, if any step
96 fails with a merge conflict, the whole thing should be abandoned.
97 This avoids asking the user to resolve confusing conflicts. It also
98 avoids asking the user to pointlessly resolve conflicts in situations
99 where we will later discover that $\alg{Merge-Base}$ wasn't feasible
102 If $\pc$ has only one direct dependency, this algorithm should not be
103 used as in that case $\alg{Recreate-Base}$ is trivial and guaranteed
104 to generate a perfect answer, whereas this algorithm might involve
105 merges and therefore might not produce a perfect answer if the
106 situation is complicated.
108 For \alg{Merge-Base} we do not prove that the preconditions are met.
109 Instead, we check them at runtime. If they turn out not to be met, we
110 abandon \alg{Merge-Base} and resort to \alg{Recreate-Base}.
112 Initially, set $W \iassign W^{\pcn}$.
114 \subsubsection{Bases and sources}
116 In some order, perhaps interleaving the two kinds of merge:
120 \item For each $\hasdep$-maximal $\pd \isdirdep \pc$, find a merge base
121 $M \le W,\; \le \tipdy$ and merge $\tipdy$ into $W$.
122 That is, use $\alg{Merge}$ with $L = W,\; R = \tipdy$.
124 \item For each $S \in S^{\pcn}_i$, merge it into $W$.
125 That is, use $\alg{Merge}$ with $L = W,\; R = S,\; M = M^{\pcn}_i$.
126 (Base Sibling Merge.)
130 \subsubsection{Fixup}
132 Execute $\alg{Fixup-Base}(W,\pc)$.
134 TODO define Fixup-Base
136 \subsubsection{Result}
138 If all of that was successful, let $\tipcn = W$.
140 \subsection{$\alg{Recreate-Base}(\pc)$}
146 Choose a $\hasdep$-maximal direct dependency $\pd$ of $\pc$.
150 Use $\alg{Create Base}$ with $L$ = $\tipdy,\; \pq = \pc$ to generate $C$
151 and set $W \iassign C$.
154 Create Acyclic: by Tip Correct Contents of $L$,
155 $L \haspatch \pa E \equiv \pa E = \pd \lor \pa E \isdep \pd$.
156 Now $\pd \isdirdep \pc$,
157 so by Coherence, and setting $\pa E = \pc$,
158 $L \nothaspatch \pc$. I.e. $L \nothaspatch \pq$. OK.
160 That's everything for Create Base.
165 Execute the subalgorithm $\alg{Recreate-Recurse}(\pc)$.
169 Declare that we contain all of the relevant information from the
170 sources. That is, use $\alg{Pseudo-Merge}$ with $L = W, \;
171 \set R = \{ W \} \cup \set S^{\pcn}$.
174 Base Only: $\patchof{W} = \patchof{L} = \pn$. OK.
177 Want to prove that for any $\p \isin C$, $\tipdy$ is a suitable $T$.
185 \subsubsection{$\alg{Recreate-Recurse}(\pd)$}
189 \item Is $W \haspatch \pd$ ? If so, there is nothing to do: return.
191 \item TODO what about non-Topbloke base branches
193 \item For all $\hasdep$-maximal $\pd' \isdirdep \pd$,
194 execute $\alg{Recreate-Recurse}(\pd')$.
196 \item Use $\alg{Pseudo-Merge}$ with $L = W,\; \set R = \{ \tipdn \}$.
197 (Recreate Base Dependency Base Declaration.)
199 \item Use $\alg{Merge}$ to apply $\pd$ to $W$. That is,
200 $L = W, \; R = \tipdy, \; M = \baseof{R} = \tipdn$.
206 \subsection{$\alg{Merge-Tip}(\pc)$}
210 \item TODO CHOOSE/REFINE W AND S as was done during Ranking for bases
212 \item $\alg{Merge}$ from $\tipcn$. That is, $L = W, \;
213 R = \tipcn$ and choose any suitable $M$.
216 $L = W$, $R = \tipcn$.
219 Afterwards, $\baseof{W} = \tipcn$.
222 \item For each source $S \in \set S^{\pcy}$,
223 $\alg{Merge}$ with $L = W, \; R = S$ and any suitable $M$.
226 In fact, we do this backwards: $L = S$, $R = W$.
228 the resulting $C \in \pcy$ and the remaining properties of the Merge
229 commit construction are symmetrical in $L$ and $R$ so this is fine.
231 By the results of Tip Base Merge, $\baseof{W} = \tipcn$.
233 By Base Ends Supreme, $\tipcn \ge \baseof{S}$ i.e.
234 $\baseof{R} \ge \baseof{L}$.
236 Either $\baseof{L} = \baseof{M}$, or we must choose a different $M$ in
237 which case $M = \baseof{S}$ will suffice.