chiark / gitweb /
strategy: split into more files
[topbloke-formulae.git] / ranking.tex
1 \section{Ranking phase}
2
3 We run the following algorithm:
4 \begin{enumerate}
5 \item Set $\allpatches = \{ \}$.
6 \item Repeatedly:
7 \begin{enumerate}
8 \item Clear out the graph $\hasdirdep$ so it has no edges.
9 \item Execute $\alg{Rank-Recurse}(\pc_0)$
10 \item Until $\allpatches$ remains unchanged.
11 \end{enumerate}
12 \end{enumerate}
13
14 $\alg{Rank-Recurse}(\pc)$ is:
15 \begin{enumerate}
16
17 \item If we have already done $\alg{Rank-Recurse}(\pc)$ in this
18 ranking iteration, do nothing.  Otherwise:
19
20 \item Add $\pc$ to $\allpatches$ if it is not there already.
21
22 \item Set
23 $$
24   \set S \iassign h(\pcn)
25      \cup 
26         \bigcup_{\p \in \allpatches}
27         \bigcup_{H \in h(\pn) \lor H \in h(\py)}
28          \{ \baseof{E} \; | \; E \in \pendsof{H}{\pcy} \}
29 $$
30
31 and $W \iassign w(h(\pcn))$
32
33 \item While $\exists_{S \in \set S} S \ge W$,
34 update $W \assign S$ and $\set S \assign \set S \, \backslash \{ S \}$
35
36 (This will often remove $W$ from $\set S$.  Afterwards, $\set S$
37 is a collection of heads to be merged into $W$.)
38
39 \item Choose an ordering of $\set S$, $S_i$ for $i=1 \ldots n$.
40
41 \item For each $S_i$ in turn, choose a corresponding $M_i$
42 such that $$
43    M_i \le S_i \land \left[
44    M_i \le W \lor \bigexists_{j<i} M_i \le S_j
45    \right]
46 $$
47
48 \item Set $\Gamma \iassign \depsreqof{W}$.
49
50 If there are multiple candidates we prefer $M_i \in \pcn$
51 if available.
52
53 \item For each $i \ldots 1..n$, update our putative direct
54 dependencies:
55 $$
56 \Gamma \assign \setmergeof{
57     \Gamma
58   }{
59     \begin{cases}
60      M_i \in \pcn :     & \depsreqof{M_i} \\
61      M_i \not\in \pcn : & \{ \}
62     \end{cases}
63   }{
64     \depsreqof{S_i}
65   }
66 $$
67
68 TODO define $\setmerge$
69
70 \item Finalise our putative direct dependencies
71 $
72 \Gamma \assign g(\pc, \Gamma)
73 $
74
75 \item For each direct dependency $\pd \in \Gamma$,
76
77 \begin{enumerate}
78 \item Add an edge $\pc \hasdirdep \pd$ to the digraph (adding nodes
79 as necessary).
80 If this results in a cycle, abort entirely (as the function $g$ is
81 inappropriate; a different $g$ could work).
82 \item Run $\alg{Rank-Recurse}(\pd)$.
83 \end{enumerate}
84
85 \end{enumerate}
86
87 \subsection{Results of the ranking phase}
88
89 By the end of the ranking phase, we have recorded the following
90 information:
91
92 \begin{itemize}
93 \item
94 $ \allpatches, \hasdirdep $ and hence the completion of $\hasdirdep$
95 into the partial order $\hasdep$.
96
97 \item
98 For each $\pc \in \allpatches$,
99 the base branch starting point commit $W^{\pcn} = W$.
100
101 \item
102 For each $\pc$,
103 the direct dependencies $\Gamma^{\pc} = \Gamma$.
104
105 \item
106 For each $\pc$,
107 the ordered set of base branch sources $\set S^{\pcn} = \set S,
108 S^{\pcn}_i = S_i$
109 and corresponding merge bases $M^{\pcn}_i = M_i$.
110
111 \end{itemize}
112
113 \subsection{Proof of termination}
114
115 $\alg{Rank-Recurse}(\pc)$ recurses but only downwards through the
116 finite graph $\hasdirdep$, so it must terminate.  
117
118 The whole ranking algorithm iterates but each iteration involves
119 adding one or more patches to $\allpatches$.  Since there are
120 finitely many patches and we never remove anything from $\allpatches$
121 this must complete eventually.
122
123 $\qed$
124