chiark / gitweb /
6fb4b4f9d2b72837ccfc8b602c7696cb93c74fd6
[topbloke-formulae.git] / strategy.tex
1 Here we describe the update algorithm.  This is responsible for
2 refreshing patches against updated versions of their dependencies,
3 for merging different versions of the various braches created by
4 distributed development, and for implementing decisions to add and
5 remove dependencies from patches.
6
7 Broadly speaking the update proceeds as follows: during the Ranking
8 phase we construct the intended graph of dependencies between patches
9 (which involves select a merge order for the base branch of each
10 patch).  Then during the Traversal phase we walk that graph from the
11 bottom up, constructing for each patch by a series of merges and other
12 operations first a new base branch head commit and then a new tip
13 branch head commit.  These new head commits are maximums - that is,
14 each has as ancestors all of its branches' sources and indeed all
15 relevant commits in that branch.
16
17 We have two possible strategies for constructing new base branch
18 heads: we can either Merge (works incrementally even if there the
19 patch has multiple dependencies, but may sometimes not be possible) or
20 we can Regenerate (trivial if there is a single dependency, and is
21 always possible, but may involve the user re-resolving conflicts if
22 there are multiple dependencies).
23
24 \section{Notation}
25
26 \begin{basedescript}{
27 \desclabelwidth{5em}
28 \desclabelstyle{\nextlinelabel}
29 }
30 \item[ $\depsreqof{K}$ ]
31 The set of direct dependencies (in the form $\py$)
32 requested in the commit $K$ ($K \in \pn$) for the patch $\p$.
33
34 \item[ $\pc \hasdirdep \p$ ]
35 The Topbloke commit set $\pc$ has as a direct contributor the
36 commit set $\p$.  This is an acyclic relation.
37
38 \item[ $\p \hasdep \pq$ ]
39 The commit set $\p$ has as direct or indirect contributor the commit
40 set $\pq$.
41 Acyclic; the completion of $\hasdirdep$ into a
42 partial order.
43
44 \item[ $\pendsof{\set J}{\p}$ ]
45 Convenience notation for
46 the maximal elements of $\bigcup_{J \in \set J} \pendsof{J}{\p}$
47 (where $\set J$ is some set of commits).
48
49 \item[ $\pendsof{\set X}{\p} \le T$ ]
50 Convenience notation for
51 $\bigforall_{E \in \pendsof{\set X}{\p}} E \le T$
52
53 %\item[ $\set E_{\pc}$ ]
54 %$ \bigcup_i \pendsof{S_{\pc,i}}{\pc} $.
55 %All the ends of $\pc$ in the sources.
56
57 %\item[ $ \tipzc, \tipcc, \tipuc, \tipfc $ ]
58 %The git ref for the Topbloke commit set $\pc$: respectively,
59 %the original, current, updated, and final values.
60
61 \end{basedescript}
62
63 \stdsection{Inputs to the update algorithm}
64
65 \begin{basedescript}{
66 \desclabelwidth{5em}
67 \desclabelstyle{\nextlinelabel}
68 }
69 \item[ $\pc_0$ ]
70 The topmost patch which we are trying to update.  This and
71 all of its dependencies will be updated.
72
73 \item[ $h : \pc^{+/-} \mapsto \set H_{\pc^{+/-}}$ ]
74 Function for getting the existing heads $\set H$ of the branch $\pc^{+/-}$.
75 This will include the current local and remote git refs, as desired.
76
77 \item[ $g : \pc, \Gamma \mapsto \Gamma'$ ]
78 Function to allow explicit adjustment of the direct dependencies
79 of $\pc$.  It is provided with a putative set of direct dependencies
80 $\Gamma$ computed as an appropriate merge of the dependencies requested by the
81 sources and should return the complete actual set $\Gamma'$ of direct
82 dependencies to use.  This allows the specification of any desired
83 (acyclic) relation $\hasdirdep$.
84
85 \end{basedescript}
86
87 \section{Ranking phase}
88
89 We run the following algorithm:
90 \begin{enumerate}
91 \item Set $\allpatches = \{ \}$.
92 \item Repeatedly:
93 \begin{enumerate}
94 \item Clear out the graph $\hasdirdep$ so it has neither nodes nor edges.
95 \item Execute {\bf Rank-Recurse}($\pc_0$)
96 \item Until $\allpatches$ remains unchanged.
97 \end{enumerate}
98 \end{enumerate}
99
100 {\bf Rank-Recurse}($\pc$) is:
101 \begin{enumerate}
102 \item Add $\pc$ to $\allpatches$ if it is not there already.
103 \item Let $\set S_{\pcn} = h(\pcn)
104      \cup 
105         \bigcup_{\p \in \allpatches}
106         \bigcup_{H \in h(\pn) \lor H \in h(\py)}
107          \{ \baseof{E} \; | \; E \in \pendsof{H}{\pcy} \} $
108
109 and $W = w(h(\pcn))$
110
111 We write $\set S = \set S_{\pcn}$ where unambiguous.
112 \item While $\exists_{S \in \set S} S \ge W$:
113
114 Update $W \assign S$ and $\set S \assign \set S \, \backslash \{ S \}$
115 \end{enumerate}
116
117 \section{Planning phase}
118
119 The results of the planning phase consist of: 
120 \begin{itemize*}
121 \item{ The relation $\hasdirdep$ and hence the partial order $\hasdep$. }
122 \item{ For each commit set $\pc$, a confirmed set of sources $\set S_{\pc}$. }
123 \item{ For each commit set $\pc$, the order in which to merge the sources
124         $E_{\pc,j} \in \set E_{\pc}$. }
125 \item{ For each $E_{\pc,j}$ an intended merge base $M_{\pc,j}$. }
126 \end{itemize*}
127
128 We use a recursive planning algorith, recursing over Topbloke commit
129 sets (ie, sets $\py$ or $\pn$).  We'll call the commit set we're
130 processing at each step $\pc$.
131 At each recursive step 
132 we make a plan to merge all $\set E_{\pc} = \{ E_{\pc,j \ldots} \}$
133 and all the direct contributors of $\pc$ (as determined below)
134 into $\tipzc$, to make $\tipfc$.
135
136 We start with $\pc = \pl$ where $\pl = \patchof{L}$.
137
138
139 \subsection{Direct contributors for $\pc = \pcn$}
140
141 The direct contributors of $\pcn$ are the commit sets corresponding to
142 the tip branches for the direct dependencies of the patch $\pc$.  We
143 need to calculate what the direct dependencies are going to be.
144
145 Choose an (arbitrary, but ideally somehow optimal in
146 a way not discussed here) ordering of $\set E_{\pc}$, $E_{\pc,j}$
147 ($j = 1 \ldots m$).
148 For brevity we will write $E_j$ for $E_{\pc,j}$.
149 Remove from that set (and ordering) any $E_j$ which
150 are $\le$ and $\neq$ some other $E_k$.
151
152 Initially let $\set D_0 = \depsreqof{\tipzc}$.
153 For each $E_j$ starting with $j=1$ choose a corresponding intended
154 merge base $M_j$ such that $M_j \le E_j \land M_j \le T_{\pc,j-1}$.
155 Calculate $\set D_j$ as the 3-way merge of the sets $\set D_{j-1}$ and
156 $\depsreqof{E_j}$ using as a base $\depsreqof{M_j}$.  This will
157 generate $D_m$ as the putative direct contributors of $\pcn$.
158
159 However, the invocation may give instructions that certain direct
160 dependencies are definitely to be included, or excluded.  As a result
161 the set of actual direct contributors is some arbitrary set of patches
162 (strictly, some arbitrary set of Topbloke tip commit sets).
163
164 \subsection{Direct contributors for $\pc = \pcy$}
165
166 The sole direct contributor of $\pcy$ is $\pcn$.
167
168 \subsection{Recursive step}
169
170 For each direct contributor $\p$, we add the edge $\pc \hasdirdep \p$
171 and augment the ordering $\hasdep$ accordingly.
172
173 If this would make a cycle in $\hasdep$, we abort . The operation must
174 then be retried by the user, if desired, but with different or
175 additional instructions for modifying the direct contributors of some
176 $\pqn$ involved in the cycle.
177
178 For each such $\p$, after updating $\hasdep$, we recursively make a plan
179 for $\pc' = \p$.
180
181
182
183 \section{Execution phase}
184
185 We process commit sets from the bottom up according to the relation
186 $\hasdep$.  For each commit set $\pc$ we construct $\tipfc$ from
187 $\tipzc$, as planned.  By construction, $\hasdep$ has $\patchof{L}$
188 as its maximum, so this operation will finish by updating
189 $\tipca{\patchof{L}}$ with $\tipfa{\patchof{L}}$.
190
191 After we are done with each commit set $\pc$, the
192 new tip $\tipfc$ has the following properties:
193 \[ \eqn{Tip Sources}{
194   \bigforall_{E_i \in \set E_{\pc}} \tipfc \ge E_i
195 }\]
196 \[ \eqn{Tip Dependencies}{
197   \bigforall_{\pc \hasdep \p} \tipfc \ge \tipfa \p
198 }\]
199 \[ \eqn{Perfect Contents}{
200   \tipfc \haspatch \p \equiv \pc \hasdep \py
201 }\]
202
203 For brevity we will sometimes write $\tipu$ for $\tipuc$, etc.  We will start
204 out with $\tipc = \tipz$, and at each step of the way construct some
205 $\tipu$ from $\tipc$.  The final $\tipu$ becomes $\tipf$.
206
207 \subsection{Preparation}
208
209 Firstly, we will check each $E_i$ for being $\ge \tipc$.  If
210 it is, are we fast forward to $E_i$
211 --- formally, $\tipu = \text{max}(\tipc, E_i)$ ---
212 and drop $E_i$ from the planned ordering.
213
214 Then we will merge the direct contributors and the sources' ends.
215 This generates more commits $\tipuc \in \pc$, but none in any other
216 commit set.  We maintain
217 $$
218  \bigforall_{\p \isdep \pc}
219  \pancsof{\tipcc}{\p} \subset
220    \pancsof{\tipfa \p}{\p}
221 $$
222 \proof{
223  For $\tipcc = \tipzc$, $T$ ...WRONG WE NEED $\tipfa \p$ TO BE IN $\set E$ SOMEHOW
224 }
225
226 \subsection{Merge Contributors for $\pcy$}
227
228 Merge $\pcn$ into $\tipc$.  That is, merge with
229 $L = \tipc, R = \tipfa{\pcn}, M = \baseof{\tipc}$.
230 to construct $\tipu$.
231
232 Merge conditions:
233
234 Ingredients satisfied by construction.
235 Tip Merge satisfied by construction.  Merge Acyclic follows
236 from Perfect Contents and $\hasdep$ being acyclic.
237
238 Removal Merge Ends: For $\p = \pc$, $M \nothaspatch \p$; OK.
239 For $\p \neq \pc$, by Tip Contents,
240 $M \haspatch \p \equiv L \haspatch \p$, so we need only
241 worry about $X = R, Y = L$; ie $L \haspatch \p$,
242 $M = \baseof{L} \haspatch \p$.
243 By Tip Contents for $L$, $D \le L \equiv D \le M$.  OK.~~$\qed$
244
245 WIP UP TO HERE
246
247 Addition Merge Ends: If $\py \isdep \pcn$, we have already
248 done the execution phase for $\pcn$ and $\py$.  By
249 Perfect Contents for $\pcn$, $\tipfa \pcn \haspatch \p$ i.e.
250 $R \haspatch \p$.  So we only need to worry about $Y = R = \tipfa \pcn$.
251 By Tip Dependencies $\tipfa \pcn \ge \tipfa \py$.
252 And by Tip Sources $\tipfa \py \ge $
253
254 want to prove $E \le \tipfc$ where $E \in \pendsof{\tipcc}{\py}$
255
256 $\pancsof{\tipcc}{\py} = $
257
258
259 computed $\tipfa \py$, and by Perfect Contents for $\py$
260
261
262 with $M=M_j, L=T_{\pc,j-1}, R=E_j$,
263 and calculate what the resulting desired direct dependencies file
264 (ie, the set of patches $\set D_j$)
265 would be.  Eventually we 
266
267 So, formally, we select somehow an order of sources $S_i$.  For each 
268
269
270 Make use of the following recursive algorithm, Plan 
271
272
273
274
275  recursively make a plan to merge all $E = \pends$
276
277 Specifically, in