monotone's LCA+DOM algo for selecting a merge base

[Denys Duchier]

Aaron asked about monotone's LCA+DOM algo for selecting a merge base.  I know
essentially squat about monotone, but his question made think about why their
selection algorithm might be correct.  In this email, I'd like to write up what
I have thought of so far and offer it up for criticism and corrections.

My understanding of LCA+DOM is that given two revisions r1 and r2 to be merged,
it picks a least common ancestor of r1 and r2 that is also a dominator of one of
them.  A dominator of r is an ancestor of r that occurs on all paths to the root
ancestor.  There is obviously always at least one dominator, namely the root
ancestor.

The following message from the monotone list explains the issues arising in the
criss-cross merge case:

    http://article.gmane.org/gmane.comp.version-control.monotone.devel/3256

The gist of the problem is that, whenever you merge, you may need to resolve a
conflict by choosing one of a pair of conflicting hunks.  However, it is clear
that choosing is NOT making a change.  When I pick a merge base, I should not
pick a revision such that in one history it appears unchanged because I always
choose the same hunk when resolving while in the other it appears new because I
chose another hunk.

Instead, it might be better to pick a base that dominates the origins of both
hunks.

More precisely, when merging r1 and r2, I need to pick a base r0 that dominates
both r1 and r2 and such that the set of paths from the root to r1 not going
through r0, and the set of paths from the root to r2 not going through r0 are
disjoint (I think).

INVARIANT (I suspect that in a full proof, this invariant might be important):
at any merge point, there cannot be a conflict hunk1/hunk2 where hunk1
originates in rev1 and hunk2 in rev2 and rev1<rev2 or rev2<rev1 (where < is the
partial order among revisions) - in other words, there can be conflicts only
with hunks originating in incomparable revisions. (this needs proof)

By selecting an r0 as described earlier, I am sure that, when merging r1 and r2,
I get conflicts only for hunks originating on the two disjoint sets of history
lines.  Those are true conflicts, not spurious ones.

Choosing such a r0 is difficult.  A simplification is to pick r0 so that, at
least on one side, there are no paths to the root not going through r0.  This is
what LCA+DOM does.

--Denys