Next: Regexps, Previous: Rebuilding ancestry, Up: Special Topics
Monotone makes use of the Mark-Merge (also known as *-merge) algorithm. The emails reproduced below document the algorithm. Further information can be found at revctrl.org.
From: Nathaniel Smith <njs <at> pobox.com> Subject: [cdv-devel] more merging stuff (bit long...) Newsgroups: gmane.comp.version-control.codeville.devel, gmane.comp.version-control.monotone.devel Date: 2005-08-06 09:08:09 GMT I set myself a toy problem a few days ago: is there a really, truly, right way to merge two heads of an arbitrary DAG, when the object being merged is as simple as possible: a single scalar value? I assume that I'm given a graph, and each node in the graph has a value, and no other annotation; I can add annotations, but they have to be derived from the values and topology. Oh, and I assume that no revision has more than 2 parents; probably things can be generalized to the case of indegree 3 or higher, but it seems like a reasonable restriction... So, anyway, here's what I came up with. Perhaps you all can tell me if it makes sense. User model ---------- Since the goal was to be "really, truly, right", I had to figure out what exactly that meant... basically, what I'm calling a "user model" -- a formal definition of how the user thinks about merging, to give an operational definition of "should conflict" and "should clean merge". My rules are these: 1) whenever a user explicitly sets the value, they express a claim that their setting is superior to the old setting 2) whenever a user chooses to commit a new revision, they implicitly affirm the validity of the decisions that led to that revision's parents Corollary of (1) and (2): whenever a user explicitly sets the value, they express that they consider their new setting to be superior to _all_ old settings 3) A "conflict" should occur if, and only if, the settings on each side of the merge express parallel claims. This in itself is not an algorithm, or anything close to it; the hope is that it's a good description of what people actually want out of a merge algorithm, expressed clearly enough that we can create an algorithm that fits these desiderata. Algorithm --------- I'll use slightly novel notation. Lower case letters represent values that scalar the scalar takes. Upper case letters represent nodes in the graph. Now, here's an algorithm, that is supposed to just be a transcription of the above rules, one step more formal: First, we need to know where users actively expressed an intention. Intention is defined by (1), above. We use * to mark where this occurred: i) a* graph roots are always marked a ii) | no mark, value was not set a a iii) | b != a, so b node marked b* a b iv) \ / c* c is totally new, so marked a a \ / c* a b we're marking places where users expressed v) \ / intention; so b should be marked iff this b? was a conflict (!) a a for now I'm not special-casing the coincidental vi) \ / clean merge case, so let's consider this to be a? a subclass of (v). That's all the cases possible. So, suppose we go through and annotate our graph with *s, using the above rules; we have a graph with some *s peppered through it, each * representing one point that a user took action. Now, a merge algorithm per se: Let's use *(A) to mean the unique nearest marked ancestor of node A. Suppose we want to merge A and B. There are exactly 3 cases: - *(A) is an ancestor of B, but not vice versa: B wins. - *(B) is an ancestor of A, but not vice versa: A wins. - *(A) is _not_ an ancestor of B, and vice versa: conflict, escalate to user Very intuitive, right? If B supercedes the intention that led to A, then B should win, and vice-versa; if not, the user has expressed two conflicting intentions, and that, by definition, is a conflict. This lets us clarify what we mean by "was a conflict" in case (v) above. When we have a merge of a and b that gives b, we simple calculate *(a); if it is an ancestor of 'b', then we're done, but if it isn't, then we mark the merge node. (Subtle point: this is actually not _quite_ the same as detecting whether merging 'a' and 'b' would have given a conflict; if we somehow managed to get a point in the graph that would have clean merged to 'a', but in fact was merged to 'b', then this algorithm will still mark the merge node.) For cases where the two parents differ, you have to do this using the losing one; for cases where the two parents are the same, you should check both, because it could have been a clean merge two different ways. If *(a1) = *(a2), i.e., both sides have the same nearest marked ancestor, consider that a clean merge. That's all. Examples -------- Of course, I haven't shown you this is well-defined or anything, but to draw out the suspense a little, have some worked examples (like most places in this document, I draw graphs with two leaves and assume that those are being merged): graph: a* / \ a b* result: *(a) is an ancestor of b, but *(b) is not an ancestor of a; clean merge with result 'b'. graph: a* / \ b* c* result: *(b) = b is not an ancestor of c, and *(c) = c is not an ancestor of c; conflict. graph: a* / \ b* c* <--- these are both marked, by (iii) |\ /| | X | |/ \| b* c* <--- which means these were conflicts, and thus marked result: the two leaves are both marked, and thus generate a conflict, as above. Right, enough of that. Math time. Math ---- Theorem: In a graph marked following the above rules, every node N will have a unique least marked ancestor M, and the values of M and N will be the same. Proof: By downwards induction on the graph structure. The base case are graph roots, which by (i) are always marked, so the statement is trivially true. Proceeding by cases, (iii) and (iv) are trivially true, since they produce nodes that are themselves marked. (ii) is almost as simple; in a graph 'a' -> 'a', the child obviously inherits the parent's unique least marked ancestor, which by inductive hypothesis exists. The interesting case is (v) and (vi): a b \ / b If the child is marked, then again the statement is trivial; so suppose it is not. By definition, this only occurs when *(a) is an ancestor of 'b'. But, by assumption, 'b' has a unique nearest ancestor, whose value is 'b'. Therefore, *(a) is also an ancestor of *(b). If we're in the weird edge case (vi) where a = b, then these may be the same ancestor, which is fine. Otherwise, the fact that a != b, and that *(a)'s value = a's value, *(b)'s value = b's value, implies that *(a) is a strict ancestor of *(b). Either way, the child has a unique least marked ancestor, and it is the same ULMA as its same-valued parent, so the ULMA also has the right value. QED. Corollary: *(N) is a well-defined function. Corollary: The three cases mentioned in the merge algorithm are the only possible cases. In particular, it cannot be that *(A) is an ancestor of B and *(B) is an ancestor of A simultaneously, unless the two values being merged are identical (and why are you running your merge algorithm then?). Or in other words: ambiguous clean merge does not exist. Proof: Suppose *(A) is an ancestor of B, and *(B) is an ancestor of A. *(B) is unique, so *(A) must also be an ancestor of *(B). Similarly, *(B) must be an ancestor of *(A). Therefore: *(A) = *(B) We also have: value(*(A)) = value(A) value(*(B)) = value(B) which implies value(A) = value(B). QED. Therefore, the above algorithm is well-defined in all possible cases. We can prove another somewhat interesting fact: Theorem: If A and B would merge cleanly with A winning, then any descendent D of A will also merge cleanly with B, with D winning. Proof: *(B) is an ancestor of A, and A is an ancestor of D, so *(B) is an ancestor of D. I suspect that this is enough to show that clean merges are order invariant, but I don't have a proof together ATM. Not sure what other properties would be interesting to prove; any suggestions? It'd be nice to have some sort of proof about "once a conflict is resolved, you don't have to resolve it again" -- which is the problem that makes ambiguous clean merge so bad -- but I'm not sure how to state such a property formally. Something about it being possible to fully converge a graph by resolving a finite number of conflicts or something, perhaps? Funky cases ----------- There are two funky cases I know of. Coincidental clean merge: | a / \ b* b* Two people independently made the same change. When we're talking about textual changes, some people argue this should give a conflict (reasoning that perhaps the same line _should_ be inserted twice). In our context that argument doesn't even apply, because these are just scalars; so obviously this should be a clean merge. Currently, the only way this algorithm has to handle this is to treat it as an "automatically resolved conflict" -- there's a real conflict here, but the VCS, acting as an agent for the user, may decide to just go ahead and resolve it, because it knows perfectly well what the user will do. In this interpretation, everything works fine, all the above stuff applies; it's somewhat dissatisfying, though, because it's a violation of the user model -- the user has not necessarily looked at this merge, but we put the * of user-assertion on the result anyway. Not a show-stopper, I guess... It's quite possible that the above stuff could be generalized to allow non-unique least marked ancestors, that could only arise in exactly this case. I'm not actually sure what the right semantics would be, though. If we're merging: | a / \ b b \ / \ b c Should that be a clean merge? 'b' was set twice, and only one of these settings was overridden; is that good enough? Do you still have the same opinion if the graph is: | a | b / \ c b | / \ b b c \ / b ? Here the reason for the second setting of 'b' was that a change away from it was reverted; to make it extra cringe-inducing, I threw in that change being reverted was another change to 'c'... (this may just be an example of how any merge algorithm has some particular case you can construct where it will get something wrong, because it doesn't _actually_ know how to read the users's minds). Supporting these cases may irresistably lead back to ambiguous clean, as well: | a / \ b* c* / \ / \ c* X b* \ / \ / c b The other funky case is this thing (any clever name suggestions?): a / \ b* c* \ / \ c* d* Merging here will give a conflict, with my algorithm; 3-way merge would resolve it cleanly. Polling people on #monotone and #revctrl, the consensus seems to be that they agree with 3-way merge, but giving a conflict is really not _that_ bad. (It also seems to cause some funky effects with darcs-merge; see zooko's comments on #revctrl and darcs-users.) This is really a problem with the user model, rather than the algorithm. Apparently people do not interpret the act of resolving the b/c merge to be "setting" the result; They seem to interpret it as "selecting" the result of 'c'; the 'c' in the result is in some sense the "same" 'c' as in the parent. The difference between "setting" and "selecting" is the universe of possible options; if you see a b \ / c then you figure that the person doing the merge was picking from all possible resolution values; when you see a b \ / b you figure that the user was just picking between the two options given by the parents. My user model is too simple to take this into account. It's not a huge extension to the model to do so; it's quite possible that an algorithm could be devised that gave a clean merge here, perhaps by separately tracking each node's nearest marked ancestor and the original source of its value as two separate things. Relation to other work ---------------------- This algorithm is very close to the traditional codeville-merge approach to this problem; the primary algorithmic difference is the marking of conflict resolutions as being "changes". The more important new stuff here, I think, are the user model and the proofs. Traditionally, merge algorithms are evaluated by coming up with some set of examples, eyeballing them to make some guess as to what the "correct" answer was, comparing that to the algorithm's output, and then arguing with people whose intuitions were different. Fundamentally, merging is about deterministically guessing the user's intent in situations where the user has not expressed any intent. Humans are very good at guessing intent; we have big chunks of squishy hardware designed to form sophisticated models of others intents, and it's completely impossible for a VCS to try and duplicate that in full. My suggestion here, with my "user model", is to seriously and explicitly study this part of the problem. There are complicated trade-offs between accuracy (correctly modeling intention), conservatism (avoiding incorrectly modeling intention), and implementability (describing the user's thought processes exactly isn't so useful if you can't apply it in practice). It's hard to make an informed judgement when we don't have a name for the thing we're trying to optimize, and hard to evaluate an algorithm when we can't even say what it's supposed to be doing. I suspect the benefit of the proofs is obvious to anyone who has spent much time banging their head against this problem; until a few days ago I was skeptical there _was_ a way to design a merge algorithm that didn't run into problems like ambiguous clean merge. I'm still skeptical, of course, until people read this; merging is like crypto, you can't trust anything until everyone's tried to break it... so let's say I'm cautiously optimistic . If this holds up, I'm quite happy; between the user model and the proofs, I'm far more confident that this does something sensible in all cases and has no lurking edge cases than I have been in any previous algorithm. The few problem cases I know of display a pleasing conservatism -- perhaps more cautious than they need to be, but even if they do cause an occasional unnecessary conflict, once the conflict is resolved it should stay resolved. So... do your worst! -- Nathaniel -- So let us espouse a less contested notion of truth and falsehood, even if it is philosophically debatable (if we listen to philosophers, we must debate everything, and there would be no end to the discussion). -- Serendipities, Umberto Eco
Replies and further discussion concerning this email can be found in the monotone-devel archives.
From: Nathaniel Smith <njs@...> Subject: improvements to *-merge Newsgroups: gmane.comp.version-control.revctrl, gmane.comp.version-control.monotone.devel Date: 2005-08-30 09:21:18 GMT This is a revised version of *-merge: http://thread.gmane.org/gmane.comp.version-control.monotone.devel/4297 that properly handles accidental clean merges. It does not improve any of the other parts, just the handling of accidental clean merges. It shows a way to relax the uniqueness of the *() operator, while still preserving the basic results from the above email. For clarity, I'll say 'unique-*-merge' to refer to the algorithm given above, and 'multi-*-merge' to refer to this one. This work is totally due to Timothy Brownawell <tbrownaw@...>. All I did was polish up the proofs and write it up. He has a more complex version at: http://article.gmane.org/gmane.comp.version-control.monotone.devel/4496 that also attempts to avoid the conflict with: a / \ b* c* \ / \ c* d* and has some convergence in it, but the analysis for that is not done. So: User model ---------- We keep exactly the same user model as unique-*-merge: 1) whenever a user explicitly sets the value, they express a claim that their setting is superior to the old setting 2) whenever a user chooses to commit a new revision, they implicitly affirm the validity of the decisions that led to that revision's parents Corollary of (1) and (2): whenever a user explicitly sets the value, they express that they consider their new setting to be superior to _all_ old settings 3) A "conflict" should occur if, and only if, the settings on each side of the merge express parallel claims. The difference is that unique-*-merge does not _quite_ fulfill this model, because in real life your algorithm will automatically resolve coincidental clean merge cases without asking for user input; but unique-* is not smart enough to take this into account when inferring user intentions. Algorithm --------- We start by marking the graph of previous revisions. For each node in the graph, we either mark it (denoted by a *), or do not. A mark indicates our inference that a human expressed an intention at this node. i) a* graph roots are always marked a1 ii) | no mark, value was not set a2 a iii) | b != a, so 'b' node marked b* a b iv) \ / c* 'c' is totally new, so marked a1 a2 \ / c* a b1 we're marking places where users expressed v) \ / intention; so 'b' should be marked iff this b2? was a conflict a1 a2 'a' matches parents, and so is not marked vi) \ / (alternatively, we can say this is a special a3 case of (v), that is never a conflict) Case (vi) is the only one that differs from unique-* merge. However, because of it, we must use a new definition of *(): Definition: By *(A), we mean we set of minimal marked ancestors of A. "Minimal" here is used in the mathematical sense of a node in a graph that has no descendents in that graph. Algorithm: Given two nodes to merge, A and B, we consider four cases: a) value(A) = value(B): return the shared value b) *(A) > B: return value(B) c) *(B) > A: return value(A) d) else: conflict; escalate to user Where "*(A) > B" means "all elements of the set *(A) are non-strict ancestors of the revision B". The right way to read this is as "try (a) first, and then if that fails try (b), (c), (d) simultaneously". Note that except for the addition of rule (a), this is a strict generalization of the unique-* algorithm; if *(A) and *(B) are single-element sets, then this performs _exactly_ the same computations as the unique-* algorithm. Now we can say what we mean by "was a conflict" in case (v) above: given a -> b2, b1 -> b2, we leave b2 unmarked if and only if *(a) > b1. Examples -------- 1. a1* / \ a2 b* result: *(a2) = {a1}, a1 > b, so b wins. 2. a* / \ b* c* result: *(b) = {b}, *(c) = {c}, neither *(b) > c nor *(c) > b, so conflict. 3. a* / \ b1* b2* \ / \ b3 c1* result: *(b3) = {b1, b2}; b2 > c1, but b1 is not > c, so c does not win. *(c1) = {c1}, which is not > b3. conflict. note: this demonstrates that this algorithm does _not_ do convergence. Instead, it takes the conservative position that for one node to silently beat another, the winning node must pre-empt _all_ the intentions that created the losing node. While it's easy to come up with just-so stories where this is the correct thing to do (e.g., b1 and b2 each contain some other changes that independently require 'a' to become 'b'; c1 will have fixed up b2's changes, but not b1's), this doesn't actually mean much. Whether this is good or bad behavior a somewhat unresolved question, that may ultimately be answered by which merge algorithms turn out to be more tractable... 4. a* / \ b1* b2* |\ /| | X | |/ \| b3 c* result: *(b3) = {b1, b2} > c. *(c) = {c}, which is not > b3. c wins cleanly. 5. a* / \ b1* c1* / \ / \ c2* X b2* \ / \ / c3 b3 result: *(c3) = {c1, c2}; c1 > b3 but c2 is not > b3, so b3 does not win. likewise, *(b3) = {b1, b2}; b1 > c3 but b2 is not > c3, so c3 does not win either. conflict. 6. a* / \ b1* c1* / \ / \ c2* X b2* \ / \ / c3 b3 |\ /| | X | |/ \| c4* b4* (this was my best effort to trigger an ambiguous clean merge with this algorithm; it fails pitifully:) result: *(c4) = {c4}, *(b4) = {b4}, obvious conflict. Math ---- The interesting thing about this algorithm is that all the unique-* proofs still go through, in a generalized form. The key one that makes *-merge tractable is: Theorem: In a graph marked by the above rules, given a node N, all nodes in *(N) will have the same value as N. Proof: By induction. We consider the cases (i)-(vi) above. (i) through (iv) are trivially true. (v) is interesting. b2 is marked when *(a) not > b1. b2 being marked makes that case trivial, so suppose *(a) > b1. All elements of *(a) are marked, and are ancestors of b1; therefore, by the definition of *() and "minimal", they are also all ancestors of things in *(b1). Thus no element of *(a) can be a minimal marked ancestor of b2. (vi) is also trivial, because *(a3) = *(a1) union *(a2). QED. We also have to do a bit of extra work because of the sets: Corollary 1: If *(A) > B, and any element R of *(B) is R > A, then value(A) = value(B). Proof: Let such an R be given. R > A, and R marked, imply that there is some element S of *(A) such that R > S. On the other hand, *(A) > B implies that S > B. By similar reasoning to the above, this means that there is some element T of *(B) such that S > T. So, recapping, we have: nodes: R > S > T from: *(B) *(A) *(B) *(B) is a set of minimal nodes, yet we have R > T and R and T both in *(B). This implies that R = T. R > S > R implies that S = R, because we are in a DAG. Thus value(A) = value(S) = value(R) = value(B) QED. Corollary 2: If *(A) > B and *(B) > A, then not only does value(A) = value(B), but *(A) = *(B). Proof: By above, each element of *(B) is equal to some element of *(A), and vice-versa. This is good, because it means our algorithm is well-defined. The only time when options (b) and (c) (in the algorithm) can simultaneously be true, is when the two values being merged are identical to start with. I.e., no somewhat anomalous "4th case" of ambiguous clean merge. Actually, this deserves some more discussion. With *() returning a set, there are some more subtle "partial ambiguous clean" cases to think about -- should we be worrying about cases where some, but not all, of the marked ancestors are pre-empted? This is possible, as in example 5 above: a* / \ b1* c1* / \ / \ c2* X b2* \ / \ / c3 b3 A hypothetical (convergence supporting?) algorithm that said A beats B if _any_ elements of *(A) are > B would give an ambiguous clean merge on this case. (Maybe that wouldn't be so bad, so long as we marked the result, but I'm in no way prepared to do any sort of sufficient analysis right now...) The nastiest case of this is where *(A) > B, but some elements of *(B) are > A -- so we silently make B win, but it's really not _quite_ clear that's a good idea, since A also beat B sometimes -- and we're ignoring those user's intentions. This is the nice thing about Corollary 1 (and why I didn't just collapse it into Corollary 2) -- it assures us that the only time this _weak_ form of ambiguous clean can happen is when A and B are already identical. This _can_ happen, for what it's worth: a* /|\ / | \ / | \ / | \ b1* b2* d* |\ /\ / | \ / \/ | X b3* | / \ / |/ b4 b5 Here *(b5) = {b3, b2}, *(b6) = {b2, b4}. If we ignore for a moment that b4 and b5 have the same value, this is a merge that b4 would win and b5 would lose, even though one of b4's ancestors, i.e. b1, is pre-empted by b5. However, it can _only_ happen if we ignore that they have the same value... The one other thing we proved about unique-* merge also still applies; the proof goes through word-for-word: Theorem: If A and B would merge cleanly with A winning, then any descendent D of A will also merge cleanly with B, with D winning. Proof: *(B) > A, and A > D, so *(B) > D. Discussion ---------- This algorithm resolves one of the two basic problems I observed for unique-* merge -- coincidental clean merges are now handled, well, cleanly, and the user model is fully implemented. However, we still do not handle the unnamed case (you guys totally let me down when I requested names for this case last time): a / \ b* c* \ / \ c* d* which still gives a conflict. We also, of course, continue to not support more exotic features like convergence or implicit rollback. Not the most exciting thing in the world. OTOH, it does strictly increase the complexity of algorithms that are tractable to formal analysis. Comments and feedback appreciated. -- Nathaniel -- "The problem...is that sets have a very limited range of activities -- they can't carry pianos, for example, nor drink beer."
Replies and further discussion concerning this email can be found in the monotone-devel archives.
From: Timothy Brownawell <tbrownaw@...> Subject: more on "mark-merge" Newsgroups: gmane.comp.version-control.revctrl, gmane.comp.version-control.monotone.devel Prerequisite: http://thread.gmane.org/gmane.comp.version-control.monotone.devel/4297 A user can make 2 types of merge decisions: (1): One parent is better than the other (represented by *) (2): Both parents are wrong (represented by ^) Since there are 2 types of merge decisions, it would be bad to treat all merge decisions the same. Also, in the case of merge(a, a) = a, it is possible for there to be multiple least decision ancestors. ===== Define: ^(A) is the set of ancestors of A that it gets its value from (found by setting N=A and iterating N = *(N) until there is no change) *(A) is the set of least ancestors of A in which the user made a decision note that erase_ancestors(^(A)) = ^(A), and erase_ancestors(*(A)) = *(A) ===== & is intersection, | is union *(A) has the same properties as before, except that it is not a single ancestor, but a set. This set can acquire more than one member only in the case of Aa Ba \ / Ca , where *(A) and *(B) are different; *(C) will be erase_ancestors(*(A) | *(B)) The ancestory corollary becomes: any ancestor C of A with value(C) != value(A) will be an ancestor of at least one member of *(A) When merging A and B: # if one side knows of _all_ places that the other side was chosen, it wins (1) set X = erase_ancestors(*(A) | *(B)) if X & *(B) = {}, A wins if X & *(A) = {}, B wins else, X contains members of both *(A) and *(B) # if one side knows of _all_ places that the other side originated, it wins (2) set Y = erase_ancestors(*(A) | ^(B)) set Z = erase_ancestors(*(B) | ^(A)) if Y & ^(B) = {} and Z & ^(A) = {}, conflict if Y & ^(B) = {}, A wins if Z & ^(A) = {}, B wins # if one side knows of _any_ places that the other side originated, it wins (3) if Y & ^(B) != ^(B) and Z & ^(A) != ^(A), conflict if Y & ^(B) != ^(B), A wins if Z & ^(A) != ^(A), B wins # else, nobody knows anything (4) conflict (3) is convergence, and can be safely left out if unwanted ==== "Funky cases" Coincidental clean does not exist; a mark is only needed when there is user intervention. | a / \ b b \ / \ b c and the example after it will resolve cleanly iff (3) is included. | a / \ b* c* / \ / \ c* X b* \ / \ / c b will be a conflict. a / \ b* c* \ / \ c* d* This ("the other funky case") is handled by (2), and resolves cleanly. Tim
Replies and further discussion concerning this email can be found in the monotone-devel archives.