[darcs-devel] camp conflictors aka RepoPatchV3

[Benjamin Franksen]

On 09/10/2018 10:28 AM, Ben Franksen wrote:
> Am 08.09.2018 um 19:34 schrieb Ben Franksen:
> tl;dr: I managed to fix it by adding inverse conflictors and this time
> made sure all property tests are enabled.

I have since been working on understanding, implementing, and testing
what Ian states (in the paper) as "repo invariants". Here is what I learned.

First, note that "repo" here does not mean "sequence of named patches"
but rather what get by flattening them into a single large RL of
RepoPatchV3. So this ignores the grouping of patches into named patches
with meta-data.

There are a few invariants that are simple to state and verify: all
patches in the repo must have a unique identifier which furthermore must
be positive. (Patch identifiers are either positive or negative, they
are always created positive and inverting a patch also inverts its
identifier).

The more interesting invariants concern the ingredients of a conflictor
at the end of a repo and how they relate to the preceding patches.

This starts with the claim that if we take the identifiers of all
patches that the conflictor says it conflicts with, then we can find all
of them in the preceding patches. This is pretty clear once you have an
understanding of the commute algorithm which goes to great pains in
order to ensure that everything reference by a conflictor is found to
the left of it.

Furthermore, it is stated that it is possible to commute them to the end
of the repo, right before our conflictor. Initially I found this to be a
pretty bold statement, but to my surprise the tests agreed with it.

The paper goes on to claim that we can now take the patch IDs of the
effect of our conflictor (the changes it reverts) and that again we can
commute them to the end. This fails and --with hindsight-- is easy to
disprove: just merge a patch that conflicts with a normal patch which is
behind a conflictor that depends on it.

The rest of the invariants in the paper now partly become type errors,
due to the mistake above. When I started to think how to fix i.e.
re-formulate these properties in light of this failure, it started to
look more and more like the algorithm for commuting conflicted paches!

Indeed, all the details obscure that there is a simple high-level
statement that captures their essence succinctly. It says:

  All patches that a conflictor tells us it conflicts with, can be
  commuted past that conflictor, thereby turning it into a normal patch.

Formulating it in this way makes it sound like something we could
reasonably expect to be true. I think it could be proven, given
permutivity and the merge-commute law (which states that both branches
of a merge commute to each other), and a few more properties of the
merge and commute algorithms. For now I am satisfied that it holds up in
the testsuite with -q 50000.

Cheers
Ben