traversal.tex

   1 \section{Traversal phase --- algorithm}
   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 For each patch $\pc \in \allpatches$ in topological order by $\hasdep$,
  13 lowest first:
  14
  15 \begin{enumerate}
  16
  17 \item Optionally, attempt
  18  $\alg{Merge-Base}(\pc)$.  This may or may not succeed.
  19
  20 \item If this didn't succeed, or was not attempted, execute
  21  $\alg{Recreate-Base}(\pc)$.
  22
  23 \item Then in any case, execute
  24  $\alg{Merge-Tip}(\pc)$.
  25
  26 \end{enumerate}
  27
  28 After processing each $\pc$ we will have created $\tipcn$ and $\tipcy$
  29 such that:
  30
  31 \statement{Correct Base}{
  32   \baseof{\tipcy} = \tipcn
  33 }
  34 \statement{Base Correct Contents}{
  35   \tipcn \haspatch \pa E
  36    \equiv
  37   \pa E \isdep \pc
  38 }
  39 \statement{Tip Covers Reachable}{
  40   \tipcy \ge \pendsof{\allreachof{\pcy}}{\pcy}
  41 }
  42 \statement{Base Covers Inputs' Bases}{
  43   \bigforall_{E \in \pendsof{\allsrcs}{\pcy}} \tipcn \ge \baseof{E}
  44 }
  45 \statement{Base Covers Base Inputs}{
  46   \bigforall_{H \in \set H^{\pn}} \tipcn \ge H
  47 }
  48
  49 \subsection{Reachability and coverage}
  50
  51 We ensure Tip Covers Reachable as follows:
  52
  53 \begin{itemize}
  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.
  60 \end{itemize}
  61
  62 A corrolary is as follows:
  63 \statement{Tip Covers Superior Reachable} {
  64   \bigforall_{\pd \isdep \pc}
  65     \tipdy \ge \pendsof{\allreachof{\pcy}}{\pdy}
  66 }
  67 \proof{
  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}$.
  73 }
  74
  75 \subsection{Traversal Lemmas}
  76
  77 \statement{Tip Correct Contents}{
  78   \tipcy \haspatch \pa E
  79     \equiv
  80   \pa E = \pc \lor \pa E \isdep \pc
  81 }
  82 \proof{
  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$.
  87 }
  88
  89 \subsection{$\alg{Merge-Base}(\pc)$}
  90
  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
  93 point.
  94
  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
 100 after all.
 101
 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.
 107
 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}.
 111
 112 Initially, set $W \iassign W^{\pcn}$.
 113
 114 \subsubsection{Bases and sources}
 115
 116 In some order, perhaps interleaving the two kinds of merge:
 117
 118 \begin{enumerate}
 119
 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$.
 123
 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.)
 127
 128 \end{enumerate}
 129
 130 \subsubsection{Fixup}
 131
 132 Execute $\alg{Fixup-Base}(W,\pc)$.
 133
 134 TODO define Fixup-Base
 135
 136 \subsubsection{Result}
 137
 138 If all of that was successful, let $\tipcn = W$.
 139
 140 \subsection{$\alg{Recreate-Base}(\pc)$}
 141
 142 \begin{enumerate}
 143
 144 \item
 145
 146 Choose a $\hasdep$-maximal direct dependency $\pd$ of $\pc$.
 147
 148 \item
 149
 150 Use $\alg{Create Base}$ with $L$ = $\tipdy,\; \pq = \pc$ to generate $C$
 151 and set $W \iassign C$.
 152
 153  \commitproof{
 154   \condproof{Create Acyclic}{
 155    by Tip Correct Contents of $L$,
 156    $L \haspatch \pa E \equiv \pa E = \pd \lor \pa E \isdep \pd$.
 157    Now $\pd \isdirdep \pc$,
 158    so by Coherence, and setting $\pa E = \pc$,
 159    $L \nothaspatch \pc$. I.e. $L \nothaspatch \pq$.  OK.
 160   }
 161   That's everything for Create Base.
 162  }
 163
 164 \item
 165
 166 Execute the subalgorithm $\alg{Recreate-Recurse}(\pc)$.
 167
 168 \item
 169
 170 Declare that we contain all of the relevant information from the
 171 sources.  That is, use $\alg{Pseudo-Merge}$ with $L = W, \;
 172 \set R = \{ W \} \cup \set S^{\pcn}$.
 173
 174  \commitproof{
 175   \condproof{Base Only}{ $\patchof{W} = \patchof{L} = \pn$.  OK. }
 176
 177   \condproof{Unique Tips}{
 178    Want to prove that for any $\p \isin C$, $\tipdy$ is a suitable $T$.
 179    WIP TODO
 180   }
 181
 182   WIP TODO INCOMPLETE
 183  }
 184
 185 \end{enumerate}
 186
 187 \subsubsection{$\alg{Recreate-Recurse}(\pd)$}
 188
 189 \begin{enumerate}
 190
 191 \item Is $W \haspatch \pd$ ?  If so, there is nothing to do: return.
 192
 193 \item TODO what about non-Topbloke base branches
 194
 195 \item For all $\hasdep$-maximal $\pd' \isdirdep \pd$,
 196 execute $\alg{Recreate-Recurse}(\pd')$.
 197
 198 \item Use $\alg{Pseudo-Merge}$ with $L = W,\; \set R = \{ \tipdn \}$.
 199 (Recreate Base Dependency Base Declaration.)
 200
 201 \item Use $\alg{Merge}$ to apply $\pd$ to $W$.  That is,
 202 $L = W, \; R = \tipdy, \; M = \baseof{R} = \tipdn$.
 203 (Recreate Reapply.)
 204
 205 \end{enumerate}
 206
 207
 208 \subsection{$\alg{Merge-Tip}(\pc)$}
 209
 210 \begin{enumerate}
 211
 212 \item TODO CHOOSE/REFINE W AND S as was done during Ranking for bases
 213
 214 \item $\alg{Merge}$ from $\tipcn$.  That is, $L = W, \;
 215 R = \tipcn$ and choose any suitable $M$.
 216
 217  \commitproof{
 218   $L = W$, $R = \tipcn$.
 219   TODO TBD
 220
 221   Afterwards, $\baseof{W} = \tipcn$.
 222  }
 223
 224 \item For each source $S \in \set S^{\pcy}$,
 225 $\alg{Merge}$ with $L = W, \; R = S$ and any suitable $M$.
 226
 227  \commitproof{
 228   In fact, we do this backwards: $L = S$, $R = W$.
 229   Since $S \in \pcy$,
 230   the resulting $C \in \pcy$ and the remaining properties of the Merge
 231   commit construction are symmetrical in $L$ and $R$ so this is fine.
 232
 233   By the results of Tip Base Merge, $\baseof{W} = \tipcn$.
 234
 235   By Base Ends Supreme, $\tipcn \ge \baseof{S}$ i.e.
 236   $\baseof{R} \ge \baseof{L}$.
 237
 238   Either $\baseof{L} = \baseof{M}$, or we must choose a different $M$ in
 239   which case $M = \baseof{S}$ will suffice.
 240  }
 241
 242 \end{enumerate}