chiark / gitweb /
1 \documentclass[a4paper,leqno]{strayman}
2 \errorcontextlines=50
3 \let\numberwithin=\notdef
4 \usepackage{amsmath}
5 \usepackage{mathabx}
6 \usepackage{txfonts}
7 \usepackage{amsfonts}
8 \usepackage{mdwlist}
9 %\usepackage{accents}
11 \renewcommand{\ge}{\geqslant}
12 \renewcommand{\le}{\leqslant}
13 \newcommand{\nge}{\ngeqslant}
14 \newcommand{\nle}{\nleqslant}
16 \newcommand{\has}{\sqsupseteq}
17 \newcommand{\isin}{\sqsubseteq}
19 \newcommand{\nothaspatch}{\mathrel{\,\not\!\not\relax\haspatch}}
20 \newcommand{\notpatchisin}{\mathrel{\,\not\!\not\relax\patchisin}}
21 \newcommand{\haspatch}{\sqSupset}
22 \newcommand{\patchisin}{\sqSubset}
24         \newif\ifhidehack\hidehackfalse
25         \DeclareRobustCommand\hidefromedef[2]{%
26           \hidehacktrue\ifhidehack#1\else#2\fi\hidehackfalse}
27         \newcommand{\pa}[1]{\hidefromedef{\varmathbb{#1}}{#1}}
29 \newcommand{\set}[1]{\mathbb{#1}}
30 \newcommand{\pay}[1]{\pa{#1}^+}
31 \newcommand{\pan}[1]{\pa{#1}^-}
33 \newcommand{\p}{\pa{P}}
34 \newcommand{\py}{\pay{P}}
35 \newcommand{\pn}{\pan{P}}
37 \newcommand{\pr}{\pa{R}}
38 \newcommand{\pry}{\pay{R}}
39 \newcommand{\prn}{\pan{R}}
41 %\newcommand{\hasparents}{\underaccent{1}{>}}
42 %\newcommand{\hasparents}{{%
43 %  \declareslashed{}{_{_1}}{0}{-0.8}{>}\slashed{>}}}
44 \newcommand{\hasparents}{>_{\mkern-7.0mu _1}}
45 \newcommand{\areparents}{<_{\mkern-14.0mu _1\mkern+5.0mu}}
47 \renewcommand{\implies}{\Rightarrow}
48 \renewcommand{\equiv}{\Leftrightarrow}
49 \renewcommand{\land}{\wedge}
50 \renewcommand{\lor}{\vee}
52 \newcommand{\pancs}{{\mathcal A}}
53 \newcommand{\pends}{{\mathcal E}}
55 \newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
56 \newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }
58 \newcommand{\merge}{{\mathcal M}}
59 \newcommand{\mergeof}[4]{\merge(#1,#2,#3,#4)}
60 %\newcommand{\merge}[4]{{#2 {{\frac{ #1 }{ #3 } #4}}}}
62 \newcommand{\patch}{{\mathcal P}}
63 \newcommand{\base}{{\mathcal B}}
65 \newcommand{\patchof}[1]{\patch ( #1 ) }
66 \newcommand{\baseof}[1]{\base ( #1 ) }
68 \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }
69 \newcommand{\corrolary}[1]{ #1 \tag*{\mbox{\it Corrolary.}} }
71 %\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}}
72 \newcommand{\bigforall}{%
73   \mathop{\mathchoice%
74     {\hbox{\huge$\forall$}}%
75     {\hbox{\Large$\forall$}}%
76     {\hbox{\normalsize$\forall$}}%
77     {\hbox{\scriptsize$\forall$}}}%
78 }
80 \newcommand{\Largeexists}{\mathop{\hbox{\Large$\exists$}}}
81 \newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}}
83 \newcommand{\qed}{\square}
84 \newcommand{\proof}[1]{{\it Proof.} #1 $\qed$}
86 \newcommand{\gathbegin}{\begin{gather} \tag*{}}
87 \newcommand{\gathnext}{\\ \tag*{}}
89 \newcommand{\true}{t}
90 \newcommand{\false}{f}
92 \begin{document}
94 \section{Notation}
96 \begin{basedescript}{
97 \desclabelwidth{5em}
98 \desclabelstyle{\nextlinelabel}
99 }
100 \item[ $C \hasparents \set X$ ]
101 The parents of commit $C$ are exactly the set
102 $\set X$.
104 \item[ $C \ge D$ ]
105 $C$ is a descendant of $D$ in the git commit
106 graph.  This is a partial order, namely the transitive closure of
107 $D \in \set X$ where $C \hasparents \set X$.
109 \item[ $C \has D$ ]
110 Informally, the tree at commit $C$ contains the change
111 made in commit $D$.  Does not take account of deliberate reversions by
112 the user or reversion, rebasing or rewinding in
113 non-Topbloke-controlled branches.  For merges and Topbloke-generated
114 anticommits or re-commits, the change made'' is only to be thought
115 of as any conflict resolution.  This is not a partial order because it
116 is not transitive.
118 \item[ $\p, \py, \pn$ ]
119 A patch $\p$ consists of two sets of commits $\pn$ and $\py$, which
120 are respectively the base and tip git branches.  $\p$ may be used
121 where the context requires a set, in which case the statement
122 is to be taken as applying to both $\py$ and $\pn$.
123 All these sets are distinct.  Hence:
125 \item[ $\patchof{ C }$ ]
126 Either $\p$ s.t. $C \in \p$, or $\bot$.
127 A function from commits to patches' sets $\p$.
129 \item[ $\pancsof{C}{\set P}$ ]
130 $\{ A \; | \; A \le C \land A \in \set P \}$
131 i.e. all the ancestors of $C$
132 which are in $\set P$.
134 \item[ $\pendsof{C}{\set P}$ ]
135 $\{ E \; | \; E \in \pancsof{C}{\set P} 136 \land \mathop{\not\exists}_{A \in \pancsof{C}{\set P}} 137 E \neq A \land E \le A \}$
138 i.e. all $\le$-maximal commits in $\pancsof{C}{\set P}$.
140 \item[ $\baseof{C}$ ]
141 $\pendsof{C}{\pn} = \{ \baseof{C} \}$ where $C \in \py$.
142 A partial function from commits to commits.
143 See Unique Base, below.
145 \item[ $C \haspatch \p$ ]
146 $\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C$.
147 ~ Informally, $C$ has the contents of $\p$.
149 \item[ $C \nothaspatch \p$ ]
150 $\displaystyle \bigforall_{D \in \py} D \not\isin C$.
151 ~ Informally, $C$ has none of the contents of $\p$.
153 Non-Topbloke commits are $\nothaspatch \p$ for all $\p$; if a Topbloke
154 patch is applied to a non-Topbloke branch and then bubbles back to
155 the Topbloke patch itself, we hope that git's merge algorithm will
156 DTRT or that the user will no longer care about the Topbloke patch.
158 \item[ $\displaystyle \mergeof{C}{L}{M}{R}$ ]
159 The contents of a git merge result:
161 $\displaystyle D \isin C \equiv 162 \begin{cases} 163 (D \isin L \land D \isin R) \lor D = C : & \true \\ 164 (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\ 165 \text{otherwise} : & D \not\isin M 166 \end{cases} 167 169 \end{basedescript} 170 \newpage 171 \section{Invariants} 173 We maintain these each time we construct a new commit. \\ 174 $\eqn{No Replay:}{ 175 C \has D \implies C \ge D 176 }$ 177 $\eqn{Unique Base:}{ 178 \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \} 179 }$ 180 $\eqn{Tip Contents:}{ 181 \bigforall_{C \in \py} D \isin C \equiv 182 { D \isin \baseof{C} \lor \atop 183 (D \in \py \land D \le C) } 184 }$ 185 $\eqn{Base Acyclic:}{ 186 \bigforall_{B \in \pn} D \isin B \implies D \notin \py 187 }$ 188 $\eqn{Coherence:}{ 189 \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p 190 }$ 191 $\eqn{Foreign Inclusion:}{ 192 \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C 193 }$ 195 \section{Some lemmas} 197 $\eqn{Exclusive Tip Contents:}{ 198 \bigforall_{C \in \py} 199 \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C ) 200 \Bigr] 201 }$ 202 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive. 204 \proof{ 205 Let$B = \baseof{C}$in$D \isin \baseof{C}$. Now$B \in \pn$. 206 So by Base Acyclic$D \isin B \implies D \notin \py$. 207 } 208 $\corrolary{ 209 \bigforall_{C \in \py} D \isin C \equiv 210 \begin{cases} 211 D \in \py : & D \le C \\ 212 D \not\in \py : & D \isin \baseof{C} 213 \end{cases} 214 }$ 216 $\eqn{Tip Self Inpatch:}{ 217 \bigforall_{C \in \py} C \haspatch \p 218 }$ 219 Ie, tip commits contain their own patch. 221 \proof{ 222 Apply Exclusive Tip Contents to some$D \in \py$: 223$ \bigforall_{C \in \py}\bigforall_{D \in \py}
224   D \isin C \equiv D \le C $225 } 227 $\eqn{Exact Ancestors:}{ 228 \bigforall_{ C \hasparents \set{R} } 229 D \le C \equiv 230 ( \mathop{\hbox{\huge{\vee}}}_{R \in \set R} D \le R ) 231 \lor D = C 232 }$ 234 $\eqn{Transitive Ancestors:}{ 235 \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv 236 \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right] 237 }$ 239 \proof{ 240 The implication from right to left is trivial because 241$ \pends() \subset \pancs() $. 242 For the implication from left to right: 243 by the definition of$\mathcal E$, 244 for every such$A$, either$A \in \pends()$which implies 245$A \le M$by the LHS directly, 246 or$\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $247 in which case we repeat for$A'$. Since there are finitely many 248 commits, this terminates with$A'' \in \pends()$, ie$A'' \le M$249 by the LHS. And$A \le A''$. 250 } 251 $\eqn{Calculation Of Ends:}{ 252 \bigforall_{C \hasparents \set A} 253 \pendsof{C}{\set P} = 254 \left\{ E \Big| 255 \Bigl[ \Largeexists_{A \in \set A} 256 E \in \pendsof{A}{\set P} \Bigr] \land 257 \Bigl[ \Largenexists_{B \in \set A} 258 E \neq B \land E \le B \Bigr] 259 \right\} 260 }$ 261 XXX proof TBD. 263 \subsection{No Replay for Merge Results} 265 If we are constructing$C$, given 266 \gathbegin 267 \mergeof{C}{L}{M}{R} 268 \gathnext 269 L \le C 270 \gathnext 271 R \le C 272 \end{gather} 273 No Replay is preserved. {\it Proof:} 275 \subsubsection{For$D=C$:}$D \isin C, D \le C$. OK. 277 \subsubsection{For$D \isin L \land D \isin R$:} 278$D \isin C$. And$D \isin L \implies D \le L \implies D \le C$. OK. 280 \subsubsection{For$D \neq C \land D \not\isin L \land D \not\isin R$:} 281$D \not\isin C$. OK. 283 \subsubsection{For$D \neq C \land (D \isin L \equiv D \not\isin R)
284  \land D \not\isin M$:} 285$D \isin C$. Also$D \isin L \lor D \isin R$so$D \le L \lor D \le
286 R$so$D \le C$. OK. 288 \subsubsection{For$D \neq C \land (D \isin L \equiv D \not\isin R)
289  \land D \isin M$:} 290$D \not\isin C$. OK. 292$\qed$294 \section{Commit annotation} 296 We annotate each Topbloke commit$C$with: 297 \gathbegin 298 \patchof{C} 299 \gathnext 300 \baseof{C}, \text{ if } C \in \py 301 \gathnext 302 \bigforall_{\pa{Q}} 303 \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q} 304 \gathnext 305 \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}} 306 \end{gather} 308 We do not annotate$\pendsof{C}{\py}$for$C \in \py$. Doing so would 309 make it wrong to make plain commits with git because the recorded$\pends$310 would have to be updated. The annotation is not needed because 311$\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$. 313 \section{Simple commit} 315 A simple single-parent forward commit$C$as made by git-commit. 316 \begin{gather} 317 \tag*{} C \hasparents \{ A \} \\ 318 \tag*{} \patchof{C} = \patchof{A} \\ 319 \tag*{} D \isin C \equiv D \isin A \lor D = C 320 \end{gather} 322 \subsection{No Replay} 323 Trivial. 325 \subsection{Unique Base} 326 If$A, C \in \py$then$\baseof{C} = \baseof{A}$.$\qed$328 \subsection{Tip Contents} 329 We need to consider only$A, C \in \py$. From Tip Contents for$A$: 330 $D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )$ 331 Substitute into the contents of$C$: 332 $D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) 333 \lor D = C$ 334 Since$D = C \implies D \in \py$, 335 and substituting in$\baseof{C}$, this gives: 336 $D \isin C \equiv D \isin \baseof{C} \lor 337 (D \in \py \land D \le A) \lor 338 (D = C \land D \in \py)$ 339 $\equiv D \isin \baseof{C} \lor 340 [ D \in \py \land ( D \le A \lor D = C ) ]$ 341 So by Exact Ancestors: 342 $D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C 343 )$ 344$\qed$346 \subsection{Base Acyclic} 348 Need to consider only$A, C \in \pn$. 350 For$D = C$:$D \in \pn$so$D \not\in \py$. OK. 352 For$D \neq C$:$D \isin C \equiv D \isin A$, so by Base Acyclic for 353$A$,$D \isin C \implies D \not\in \py$.$\qed$355 \subsection{Coherence and patch inclusion} 357 Need to consider$D \in \py$359 \subsubsection{For$A \haspatch P, D = C$:} 361 Ancestors of$C$: 362$ D \le C $. 364 Contents of$C$: 365$ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $. 367 \subsubsection{For$A \haspatch P, D \neq C$:} 368 Ancestors:$ D \le C \equiv D \le A $. 370 Contents:$ D \isin C \equiv D \isin A \lor f $371 so$ D \isin C \equiv D \isin A $. 373 So: 374 $A \haspatch P \implies C \haspatch P$ 376 \subsubsection{For$A \nothaspatch P$:} 378 Firstly,$C \not\in \py$since if it were,$A \in \py$. 379 Thus$D \neq C$. 381 Now by contents of$A$,$D \notin A$, so$D \notin C$. 383 So: 384 $A \nothaspatch P \implies C \nothaspatch P$ 385$\qed$387 \subsection{Foreign inclusion:} 389 If$D = C$, trivial. For$D \neq C$: 390$D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$.$\qed$392 \section{Anticommit} 394 Given$L, R^+, R^-$where 395$R^+ \in \pry, R^- = \baseof{R^+}$. 396 Construct$C$which has$\pr$removed. 397 Used for removing a branch dependency. 398 \gathbegin 399 C \hasparents \{ L \} 400 \gathnext 401 \patchof{C} = \patchof{L} 402 \gathnext 403 \mergeof{C}{L}{R^+}{R^-} 404 \end{gather} 406 \subsection{Conditions} 408 $\eqn{ Unique Tip }{ 409 \pendsof{L}{\pry} = \{ R^+ \} 410 }$ 411 $\eqn{ Currently Included }{ 412 L \haspatch \pry 413 }$ 414 $\eqn{ Not Self }{ 415 L \not\in \{ R^+ \} 416 }$ 418 \subsection{No Replay} 420 By Unique Tip,$R^+ \le L$. By definition of$\base$,$R^- \le R^+$421 so$R^- \le L$. So$R^+ \le C$and$R^- \le C$and No Replay for 422 Merge Results applies.$\qed$424 \subsection{Desired Contents} 426 $D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C$ 427 {\it Proof.} 429 \subsubsection{For$D = C$:} 431 Trivially$D \isin C$. OK. 433 \subsubsection{For$D \neq C, D \not\le L$:} 435 By No Replay$D \not\isin L$. Also$D \not\le R^-$hence 436$D \not\isin R^-$. Thus$D \not\isin C$. OK. 438 \subsubsection{For$D \neq C, D \le L, D \in \pry$:} 440 By Currently Included,$D \isin L$. 442 By Tip Self Inpatch,$D \isin R^+ \equiv D \le R^+$, but by 443 by Unique Tip,$D \le R^+ \equiv D \le L$. 444 So$D \isin R^+$. 446 By Base Acyclic,$D \not\isin R^-$. 448 Apply$\merge$:$D \not\isin C$. OK. 450 \subsubsection{For$D \neq C, D \le L, D \notin \pry$:} 452 By Tip Contents for$R^+$,$D \isin R^+ \equiv D \isin R^-$. 454 Apply$\merge$:$D \isin C \equiv D \isin L$. OK. 456$\qed$458 \subsection{Unique Base} 460 Need to consider only$C \in \py$, ie$L \in \py$. 462 xxx tbd 464 xxx need to finish anticommit 466 \section{Merge} 468 Merge commits$L$and$R$using merge base$M$($M < L, M < R$): 469 \gathbegin 470 C \hasparents \{ L, R \} 471 \gathnext 472 \patchof{C} = \patchof{L} 473 \gathnext 474 \mergeof{C}{L}{M}{R} 475 \end{gather} 477 \subsection{Conditions} 479 $\eqn{ Tip Merge }{ 480 L \in \py \implies 481 \begin{cases} 482 R \in \py : & \baseof{R} \ge \baseof{L} 483 \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\ 484 R \in \pn : & R \ge \baseof{L} 485 \land M = \baseof{L} \\ 486 \text{otherwise} : & \false 487 \end{cases} 488 }$ 490 \subsection{No Replay} 492 See No Replay for Merge Results. 494 \subsection{Unique Base} 496 Need to consider only$C \in \py$, ie$L \in \py$, 497 and calculate$\pendsof{C}{\pn}$. So we will consider some 498 putative ancestor$A \in \pn$and see whether$A \le C$. 500 By Exact Ancestors for C,$A \le C \equiv A \le L \lor A \le R \lor A = C$. 501 But$C \in py$and$A \in \pn$so$A \neq C$. 502 Thus$A \le C \equiv A \le L \lor A \le R$. 504 By Unique Base of L and Transitive Ancestors, 505$A \le L \equiv A \le \baseof{L}$. 507 \subsubsection{For$R \in \py$:} 509 By Unique Base of$R$and Transitive Ancestors, 510$A \le R \equiv A \le \baseof{R}$. 512 But by Tip Merge condition on$\baseof{R}$, 513$A \le \baseof{L} \implies A \le \baseof{R}$, so 514$A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$. 515 Thus$A \le C \equiv A \le \baseof{R}$. 516 That is,$\baseof{C} = \baseof{R}$. 518 \subsubsection{For$R \in \pn$:} 520 By Tip Merge condition on$R$, 521$A \le \baseof{L} \implies A \le R$, so 522$A \le R \lor A \le \baseof{L} \equiv A \le R$. 523 Thus$A \le C \equiv A \le R$. 524 That is,$\baseof{C} = R$. 526$\qed$528 \subsection{Coherence and patch inclusion} 530 Need to determine$C \haspatch P$based on$L,M,R \haspatch P$. 531 This involves considering$D \in \py$. 533 We will use$X,Y$s.t.$\{X,Y\} = \{L,R\}$. 535 \subsubsection{For$L \nothaspatch P, R \nothaspatch P$:} 536$D \not\isin L \land D \not\isin R$.$C \not\in \py$(otherwise$L
537 \in \py$ie$L \haspatch P$by Tip Self Inpatch). So$D \neq C$. 538 Applying$\merge$gives$D \not\isin C$i.e.$C \nothaspatch P$. 540 \subsubsection{For$L \haspatch P, R \haspatch P$:} 541$D \isin L \equiv D \le L$and$D \isin R \equiv D \le R$. 542 (Likewise$D \isin X \equiv D \le X$and$D \isin Y \equiv D \le Y$.) 544 Consider$D = C$:$D \isin C$,$D \le C$, OK for$C \haspatch P$. 546 For$D \neq C$:$D \le C \equiv D \le L \lor D \le R
547  \equiv D \isin L \lor D \isin R$. 548 (Likewise$D \le C \equiv D \le X \lor D \le Y$.) 550 Consider$D \neq C, D \isin X \land D \isin Y$: 551 By$\merge$,$D \isin C$. Also$D \le X$552 so$D \le C$. OK for$C \haspatch P$. 554 Consider$D \neq C, D \not\isin X \land D \not\isin Y$: 555 By$\merge$,$D \not\isin C$. 556 And$D \not\le X \land D \not\le Y$so$D \not\le C$. 557 OK for$C \haspatch P$. 559 Remaining case, wlog, is$D \not\isin X \land D \isin Y$. 560$D \not\le X$so$D \not\le M$so$D \not\isin M$. 561 Thus by$\merge$,$D \isin C$. And$D \le Y$so$D \le C$. 562 OK for$C \haspatch P$. 564 So indeed$L \haspatch P \land R \haspatch P \implies C \haspatch P\$.
566 \end{document}