chiark / gitweb /
c8a0bfe41846f830e22019a152b950ac53648286
[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 {\bf Ranking} is:
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 (We write $\set S = \set S_{\pcn}$ when it's not ambiguous.)
110 \end{enumerate}
111
112 \section{Planning phase}
113
114 The results of the planning phase consist of: 
115 \begin{itemize*}
116 \item{ The relation $\hasdirdep$ and hence the partial order $\hasdep$. }
117 \item{ For each commit set $\pc$, a confirmed set of sources $\set S_{\pc}$. }
118 \item{ For each commit set $\pc$, the order in which to merge the sources
119         $E_{\pc,j} \in \set E_{\pc}$. }
120 \item{ For each $E_{\pc,j}$ an intended merge base $M_{\pc,j}$. }
121 \end{itemize*}
122
123 We use a recursive planning algorith, recursing over Topbloke commit
124 sets (ie, sets $\py$ or $\pn$).  We'll call the commit set we're
125 processing at each step $\pc$.
126 At each recursive step 
127 we make a plan to merge all $\set E_{\pc} = \{ E_{\pc,j \ldots} \}$
128 and all the direct contributors of $\pc$ (as determined below)
129 into $\tipzc$, to make $\tipfc$.
130
131 We start with $\pc = \pl$ where $\pl = \patchof{L}$.
132
133
134 \subsection{Direct contributors for $\pc = \pcn$}
135
136 The direct contributors of $\pcn$ are the commit sets corresponding to
137 the tip branches for the direct dependencies of the patch $\pc$.  We
138 need to calculate what the direct dependencies are going to be.
139
140 Choose an (arbitrary, but ideally somehow optimal in
141 a way not discussed here) ordering of $\set E_{\pc}$, $E_{\pc,j}$
142 ($j = 1 \ldots m$).
143 For brevity we will write $E_j$ for $E_{\pc,j}$.
144 Remove from that set (and ordering) any $E_j$ which
145 are $\le$ and $\neq$ some other $E_k$.
146
147 Initially let $\set D_0 = \depsreqof{\tipzc}$.
148 For each $E_j$ starting with $j=1$ choose a corresponding intended
149 merge base $M_j$ such that $M_j \le E_j \land M_j \le T_{\pc,j-1}$.
150 Calculate $\set D_j$ as the 3-way merge of the sets $\set D_{j-1}$ and
151 $\depsreqof{E_j}$ using as a base $\depsreqof{M_j}$.  This will
152 generate $D_m$ as the putative direct contributors of $\pcn$.
153
154 However, the invocation may give instructions that certain direct
155 dependencies are definitely to be included, or excluded.  As a result
156 the set of actual direct contributors is some arbitrary set of patches
157 (strictly, some arbitrary set of Topbloke tip commit sets).
158
159 \subsection{Direct contributors for $\pc = \pcy$}
160
161 The sole direct contributor of $\pcy$ is $\pcn$.
162
163 \subsection{Recursive step}
164
165 For each direct contributor $\p$, we add the edge $\pc \hasdirdep \p$
166 and augment the ordering $\hasdep$ accordingly.
167
168 If this would make a cycle in $\hasdep$, we abort . The operation must
169 then be retried by the user, if desired, but with different or
170 additional instructions for modifying the direct contributors of some
171 $\pqn$ involved in the cycle.
172
173 For each such $\p$, after updating $\hasdep$, we recursively make a plan
174 for $\pc' = \p$.
175
176
177
178 \section{Execution phase}
179
180 We process commit sets from the bottom up according to the relation
181 $\hasdep$.  For each commit set $\pc$ we construct $\tipfc$ from
182 $\tipzc$, as planned.  By construction, $\hasdep$ has $\patchof{L}$
183 as its maximum, so this operation will finish by updating
184 $\tipca{\patchof{L}}$ with $\tipfa{\patchof{L}}$.
185
186 After we are done with each commit set $\pc$, the
187 new tip $\tipfc$ has the following properties:
188 \[ \eqn{Tip Sources}{
189   \bigforall_{E_i \in \set E_{\pc}} \tipfc \ge E_i
190 }\]
191 \[ \eqn{Tip Dependencies}{
192   \bigforall_{\pc \hasdep \p} \tipfc \ge \tipfa \p
193 }\]
194 \[ \eqn{Perfect Contents}{
195   \tipfc \haspatch \p \equiv \pc \hasdep \py
196 }\]
197
198 For brevity we will sometimes write $\tipu$ for $\tipuc$, etc.  We will start
199 out with $\tipc = \tipz$, and at each step of the way construct some
200 $\tipu$ from $\tipc$.  The final $\tipu$ becomes $\tipf$.
201
202 \subsection{Preparation}
203
204 Firstly, we will check each $E_i$ for being $\ge \tipc$.  If
205 it is, are we fast forward to $E_i$
206 --- formally, $\tipu = \text{max}(\tipc, E_i)$ ---
207 and drop $E_i$ from the planned ordering.
208
209 Then we will merge the direct contributors and the sources' ends.
210 This generates more commits $\tipuc \in \pc$, but none in any other
211 commit set.  We maintain
212 $$
213  \bigforall_{\p \isdep \pc}
214  \pancsof{\tipcc}{\p} \subset
215    \pancsof{\tipfa \p}{\p}
216 $$
217 \proof{
218  For $\tipcc = \tipzc$, $T$ ...WRONG WE NEED $\tipfa \p$ TO BE IN $\set E$ SOMEHOW
219 }
220
221 \subsection{Merge Contributors for $\pcy$}
222
223 Merge $\pcn$ into $\tipc$.  That is, merge with
224 $L = \tipc, R = \tipfa{\pcn}, M = \baseof{\tipc}$.
225 to construct $\tipu$.
226
227 Merge conditions:
228
229 Ingredients satisfied by construction.
230 Tip Merge satisfied by construction.  Merge Acyclic follows
231 from Perfect Contents and $\hasdep$ being acyclic.
232
233 Removal Merge Ends: For $\p = \pc$, $M \nothaspatch \p$; OK.
234 For $\p \neq \pc$, by Tip Contents,
235 $M \haspatch \p \equiv L \haspatch \p$, so we need only
236 worry about $X = R, Y = L$; ie $L \haspatch \p$,
237 $M = \baseof{L} \haspatch \p$.
238 By Tip Contents for $L$, $D \le L \equiv D \le M$.  OK.~~$\qed$
239
240 WIP UP TO HERE
241
242 Addition Merge Ends: If $\py \isdep \pcn$, we have already
243 done the execution phase for $\pcn$ and $\py$.  By
244 Perfect Contents for $\pcn$, $\tipfa \pcn \haspatch \p$ i.e.
245 $R \haspatch \p$.  So we only need to worry about $Y = R = \tipfa \pcn$.
246 By Tip Dependencies $\tipfa \pcn \ge \tipfa \py$.
247 And by Tip Sources $\tipfa \py \ge $
248
249 want to prove $E \le \tipfc$ where $E \in \pendsof{\tipcc}{\py}$
250
251 $\pancsof{\tipcc}{\py} = $
252
253
254 computed $\tipfa \py$, and by Perfect Contents for $\py$
255
256
257 with $M=M_j, L=T_{\pc,j-1}, R=E_j$,
258 and calculate what the resulting desired direct dependencies file
259 (ie, the set of patches $\set D_j$)
260 would be.  Eventually we 
261
262 So, formally, we select somehow an order of sources $S_i$.  For each 
263
264
265 Make use of the following recursive algorithm, Plan 
266
267
268
269
270  recursively make a plan to merge all $E = \pends$
271
272 Specifically, in