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}