chiark / gitweb /
strategy: Define H in notation
[topbloke-formulae.git] / traversal.tex
1 \section{Traversal phase}
2
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
7 $W \assign R$.
8
9 For each commit generation operation called for by the traversal
10 algorithms, we prove that the commit generation preconditions are met.
11
12 \subsection{Algorithm}
13
14 For each patch $\pc \in \allpatches$ in topological order by $\hasdep$,
15 lowest first:
16
17 \begin{enumerate}
18
19 \item Optionally, attempt
20  $\alg{Merge-Base}(\pc)$.  This may or may not succeed.
21
22 \item If this didn't succeed, or was not attempted, execute
23  $\alg{Recreate-Base}(\pc)$.
24
25 \item Then in any case, execute
26  $\alg{Merge-Tip}(\pc)$.
27
28 \end{enumerate}
29
30 \subsection{Results}
31
32 After processing each $\pc$ we will have created $\tipcn$ and $\tipcy$
33 such that:
34 \statement{Correct Base}{
35   \baseof{\tipcy} = \tipcn
36 }
37 \statement{Base Correct Contents}{
38   \tipcn \haspatch \pa E
39    \equiv
40   \pa E \isdep \pc
41 }
42 \statement{Tip Covers Reachable}{
43   \tipcy \ge \pendsof{\allreachof{\pcy}}{\pcy}
44 }
45 \statement{Base Covers Inputs' Bases}{
46   \bigforall_{E \in \pendsof{\allsrcs}{\pcy}} \tipcn \ge \baseof{E}
47 }
48 \statement{Base Covers Base Inputs}{
49   \bigforall_{H \in \set H^{\pn}} \tipcn \ge H
50 }
51
52 \subsection{Reachability and coverage}
53
54 We ensure Tip Covers Reachable as follows:
55
56 \begin{itemize}
57 \item  We do not generate any commits $\in \py$ other than
58        during $\alg{Merge-Tip}(\py)$;
59 \item  So at the start of $\alg{Merge-Tip}(\py)$,
60        $ \pendsof{\allreach}{\py} = \pendsof{\allsrcs}{\py} $
61 \item  $\alg{Merge-tip}$ arranges that when it is done
62        $\tippy \ge \pendsof{\allreach}{\py}$ --- see below.
63 \end{itemize}
64
65 A corrolary is as follows:
66 \statement{Tip Covers Superior Reachable} {
67   \bigforall_{\pd \isdep \pc}
68     \tipdy \ge \pendsof{\allreachof{\pcy}}{\pdy}
69 }
70 \proof{
71   No commits $\in \pdy$ are created other than during
72   $\alg{Merge-Tip}(\pd)$, which runs (and has thus completed)
73   before $\alg{Merge-Tip}(\pcy)$
74   So $\pendsof{\allreachof{\pcy}}{\pdy} =
75       \pendsof{\allreachof{\pdy}}{\pdy}$.
76 }
77
78 \subsection{Traversal Lemmas}
79
80 \statement{Tip Correct Contents}{
81   \tipcy \haspatch \pa E
82     \equiv
83   \pa E = \pc \lor \pa E \isdep \pc
84 }
85 \proof{
86   For $\pc = \pa E$, Tip Own Contents suffices.
87   For $\pc \neq \pa E$, Exclusive Tip Contents
88   gives $D \isin \tipcy \equiv D \isin \baseof{\tipcy}$
89   which by Correct Base $\equiv D \isin \tipcn$.
90 }
91
92 \subsection{$\alg{Merge-Base}(\pc)$}
93
94 This algorithm attempts to construct a suitably updated version of the
95 base branch $\pcn$ using some existing version of $\pcn$ as a starting
96 point.
97
98 It should be executed noninteractively.  Specifically, if any step
99 fails with a merge conflict, the whole thing should be abandoned.
100 This avoids asking the user to resolve confusing conflicts.  It also
101 avoids asking the user to pointlessly resolve conflicts in situations
102 where we will later discover that $\alg{Merge-Base}$ wasn't feasible
103 after all.
104
105 If $\pc$ has only one direct dependency, this algorithm should not be
106 used as in that case $\alg{Recreate-Base}$ is trivial and guaranteed
107 to generate a perfect answer, whereas this algorithm might involve
108 merges and therefore might not produce a perfect answer if the
109 situation is complicated.
110
111 For \alg{Merge-Base} we do not prove that the preconditions are met.
112 Instead, we check them at runtime.  If they turn out not to be met, we
113 abandon \alg{Merge-Base} and resort to \alg{Recreate-Base}.
114
115 Initially, set $W \iassign W^{\pcn}$.
116
117 \subsubsection{Bases and sources}
118
119 In some order, perhaps interleaving the two kinds of merge:
120
121 \begin{enumerate}
122
123 \item For each $\hasdep$-maximal $\pd \isdirdep \pc$, find a merge base
124 $M \le W,\; \le \tipdy$ and merge $\tipdy$ into $W$.
125 That is, use $\alg{Merge}$ with $L = W,\; R = \tipdy$.
126
127 \item For each $S \in S^{\pcn}_i$, merge it into $W$.
128 That is, use $\alg{Merge}$ with $L = W,\; R = S,\; M = M^{\pcn}_i$.
129 (Base Sibling Merge.)
130
131 \end{enumerate}
132
133 \subsubsection{Fixup}
134
135 Execute $\alg{Fixup-Base}(W,\pc)$.
136
137 TODO define Fixup-Base
138
139 \subsubsection{Result}
140
141 If all of that was successful, let $\tipcn = W$.
142
143 \subsection{$\alg{Recreate-Base}(\pc)$}
144
145 \begin{enumerate}
146
147 \item
148
149 Choose a $\hasdep$-maximal direct dependency $\pd$ of $\pc$.
150
151 \item
152
153 Use $\alg{Create Base}$ with $L$ = $\tipdy,\; \pq = \pc$ to generate $C$
154 and set $W \iassign C$.
155
156  \commitproof{
157   \condproof{Create Acyclic}{
158    by Tip Correct Contents of $L$,
159    $L \haspatch \pa E \equiv \pa E = \pd \lor \pa E \isdep \pd$.
160    Now $\pd \isdirdep \pc$,
161    so by Coherence, and setting $\pa E = \pc$,
162    $L \nothaspatch \pc$. I.e. $L \nothaspatch \pq$.  OK.
163   }
164   That's everything for Create Base.
165  }
166
167 \item
168
169 Execute the subalgorithm $\alg{Recreate-Recurse}(\pc)$.
170
171 \item
172
173 Declare that we contain all of the relevant information from the
174 sources.  That is, use $\alg{Pseudo-Merge}$ with $L = W, \;
175 \set R = \{ W \} \cup \set S^{\pcn}$.
176
177  \commitproof{
178   \condproof{Base Only}{ $\patchof{W} = \patchof{L} = \pn$.  OK. }
179
180   \condproof{Unique Tips}{
181    Want to prove that for any $\p \isin C$, $\tipdy$ is a suitable $T$.
182    WIP TODO
183   }
184
185   WIP TODO INCOMPLETE
186  }
187
188 \end{enumerate}
189
190 \subsubsection{$\alg{Recreate-Recurse}(\pd)$}
191
192 \begin{enumerate}
193
194 \item Is $W \haspatch \pd$ ?  If so, there is nothing to do: return.
195
196 \item TODO what about non-Topbloke base branches
197
198 \item For all $\hasdep$-maximal $\pd' \isdirdep \pd$,
199 execute $\alg{Recreate-Recurse}(\pd')$.
200
201 \item Use $\alg{Pseudo-Merge}$ with $L = W,\; \set R = \{ \tipdn \}$.
202 (Recreate Base Dependency Base Declaration.)
203
204 \item Use $\alg{Merge}$ to apply $\pd$ to $W$.  That is,
205 $L = W, \; R = \tipdy, \; M = \baseof{R} = \tipdn$.
206 (Recreate Reapply.)
207
208 \end{enumerate}
209
210
211 \subsection{$\alg{Merge-Tip}(\pc)$}
212
213 \begin{enumerate}
214
215 \item TODO CHOOSE/REFINE W AND S as was done during Ranking for bases
216
217 \item $\alg{Merge}$ from $\tipcn$.  That is, $L = W, \;
218 R = \tipcn$ and $M = \baseof{W}$.
219
220  \commitproof{
221   \condproof{Ingredients}{
222    $M \le L$ is trivial.  For $M \le R$ we want
223    $\tipcn \ge \baseof{W}$.
224    Well $W \in \set S^{\pcy}$ so $W \in \allreachof{\pcn}$
225    and $W \in \pcy$.  So $W \in \pendsof{\allreachof{\pcn}}{\pcy}$
226    so Base Covers Reachable indeed
227    $\tipcn \ge \baseof{W}$.
228   }
229   \condproof{Tip Merge}{ Trivial. }
230   \condproof{Merge Acyclic}{
231    By Base Acyclic, $\tipcn \nothaspatch \p$.
232   }
233   \condproof{Foreign Merges}{ Not applicable. }
234
235   TODO TBD
236
237   Afterwards, $\baseof{W} = \tipcn$.
238  }
239
240 \item For each source $S \in \set S^{\pcy}$,
241 $\alg{Merge}$ with $L = W, \; R = S$ and any suitable $M$.
242
243  \commitproof{
244   In fact, we do this backwards: $L = S$, $R = W$.
245   Since $S \in \pcy$,
246   the resulting $C \in \pcy$ and the remaining properties of the Merge
247   commit construction are symmetrical in $L$ and $R$ so this is fine.
248
249   By the results of Tip Base Merge, $\baseof{W} = \tipcn$.
250
251   By Base Ends Supreme, $\tipcn \ge \baseof{S}$ i.e.
252   $\baseof{R} \ge \baseof{L}$.
253
254   Either $\baseof{L} = \baseof{M}$, or we must choose a different $M$ in
255   which case $M = \baseof{S}$ will suffice.
256  }
257
258 \end{enumerate}