darcs

Patch 1843 bugfix in V3.commuteNoConflicts

Title bugfix in V3.commuteNoConflicts
Superseder Nosy List bfrk
Related Issues
Status accepted Assigned To
Milestone

Created on 2019-06-24.15:30:49 by bfrk, last changed 2019-07-29.09:59:20 by bfrk.

Files
File name Status Uploaded Type Edit Remove
bugfix-in-v3_commutenoconflicts.dpatch bfrk, 2019-06-25.09:29:11 application/x-darcs-patch
patch-preview.txt bfrk, 2019-06-25.09:29:11 text/x-darcs-patch
unnamed bfrk, 2019-06-25.09:29:11 text/plain
See mailing list archives for discussion on individual patches.
Messages
msg20871 (view) Author: bfrk Date: 2019-06-24.15:30:49
See the mailing list thread "new test case generator".

1 patch for repository http://darcs.net/screened:

patch 45dea0474f011b82e354a7554c064351d940e6ff
Author: Ben Franksen <ben.franksen@online.de>
Date:   Mon Jun 24 10:09:20 CEST 2019
  * bugfix in V3.commuteNoConflicts
  
  I made a logical error when I derived the mixed Conflictor/Rotcilfnoc cases
  for commuteNoConflicts from the Conflictor/Conflictor case. This could lead
  to the creation of invalid Conflictors during an unconflicted merge of two
  Conflictors. Specifically, we could create Conflictors that undo prims that
  are already undone by a previous Conflictor.
Attachments
msg20872 (view) Author: bfrk Date: 2019-06-24.19:56:36
Please don't screen yet. I think I have made yet another mistake and
"fixed" one case too many. And I think the reason this doesn't lead to
failures in the tests is that mergeNoConflicts always commutes "invert
lhs:> rhs", so we don't run into the Conflictor:\/:Rotcilfnoc case. I
will try to find a way to make sure we test that case, too. I should
also instrument darcs-test to get coverage information.
msg20873 (view) Author: bfrk Date: 2019-06-25.08:02:54
This obsoletes the patch I sent earlier.

1 patch for repository http://darcs.net/screened:

patch 230fd522fb61feaf4ae4f50d0f0c55beee788bf8
Author: Ben Franksen <ben.franksen@online.de>
Date:   Mon Jun 24 10:09:20 CEST 2019
  * bugfix in V3.commuteNoConflicts
  
  I made a logical error when I derived the mixed Rotcilfnoc/Conflictor case
  for commuteNoConflicts from the Conflictor/Conflictor case. This could lead
  to the creation of invalid Conflictors during an unconflicted merge of two
  Conflictors. Specifically, we could create Conflictors that undo prims that
  are already undone by a previous Conflictor.
  The only reason we need this case at all is because mergeNoConflicts
  triggers it when applied to a pair of Conflictors. This means that the
  mirror case Conflictor/Rotcilfnoc is not needed, since we currently have no
  need for an inverse operation to mergeNoConflicts. So this case is now
  commented out and replaced with an error call.
Attachments
msg20874 (view) Author: bfrk Date: 2019-06-25.09:29:11
...remembering that leaving obsolete code in comments is a bad idea. We can
always roll back or view the patch to see what was there.

1 patch for repository http://darcs.net/screened:

patch 3e205eb49da2c391498d4c8e922a1e4f675b6622
Author: Ben Franksen <ben.franksen@online.de>
Date:   Mon Jun 24 10:09:20 CEST 2019
  * bugfix in V3.commuteNoConflicts
  
  I made a logical error when I derived the mixed Rotcilfnoc/Conflictor case
  for commuteNoConflicts from the Conflictor/Conflictor case. This could lead
  to the creation of invalid Conflictors during an unconflicted merge of two
  Conflictors. Specifically, we could create Conflictors that undo prims that
  are already undone by a previous Conflictor.
  The only reason we need this case at all is because mergeNoConflicts
  triggers it when applied to a pair of Conflictors. This means that the
  mirror case Conflictor/Rotcilfnoc is not needed, since we currently have no
  need for an inverse operation to mergeNoConflicts. So this case is now
  replaced with an error call.
Attachments
msg20988 (view) Author: ganesh Date: 2019-07-28.13:58:27
For now I'm just going to believe this is correct, as I haven't
understood the core of the V3 logic well enough to know either way.
msg21000 (view) Author: bfrk Date: 2019-07-29.09:59:19
> For now I'm just going to believe this is correct, as I haven't
> understood the core of the V3 logic well enough to know either way.

;-)

What happens here is this: when we commute two conflictors we need to
ensure that we maintain the invariant that a Conflictor reverts only
prims that have not already been reverted by any earlier Conflictor.

The case in question is the non-conflicting commute. We want to commute
A :> B, where effect A = r and effect B = s. We cannot just commute the
effects (r :> s), as this may violate the invariant. Instead we first
need to split r into those prims that B /also/ conflicts with, say c,
and the rest r'. We then commute (r' :> s), getting say (s' :> r'') and
then construct the effect of B' as (c +>+ s') and that of A' as r''.

The initial call to commuteToPrefix does the splitting. The subtlety
here is that what we store in the Conflictor is the effect, i.e.
/inverted/ prims. So when we test membership of PrimPatchIds of elements
of r in the set of PrimPatchIds of those that B conflicts with, we have
to invert either the identifiers from r or those we get from the
conflicts of B.

This was all correct for the case of commuting two Conflictors. For
commuting an inverted Conflictor with a plain Conflictor, I got confused
and thought that -- since the conflictor was already inverted -- I would
not have to invert the PrimPatchIds in the predicate passed to
commuteToPrefix. This was wrong, since we explicitly invert the effect
of the left hand side before passing it to commuteToPrefix, which
cancels the implicit inversion inherent in the inverted conflictor.

I am seriously considering the move from CommuteNoConflicts toward
MergeNoConflicts aka CleanMerge as the primitive notion, as you
suggested a while back. This would relieve us from ever having to handle
the internals of a Rotcilfnoc directly, avoiding mistakes like the one I
made. The direct definition of mergeNoConflicts aka cleanMerge of two
Conflictors is a lot easier to write and understand than the indirect
one of commuteNoConflicts between a Rotcilfnoc and a Conflictor.
History
Date User Action Args
2019-06-24 15:30:49bfrkcreate
2019-06-24 19:56:37bfrksetmessages: + msg20872
2019-06-25 08:02:54bfrksetfiles: + patch-preview.txt, bugfix-in-v3_commutenoconflicts.dpatch, unnamed
messages: + msg20873
2019-06-25 09:29:11bfrksetfiles: + patch-preview.txt, bugfix-in-v3_commutenoconflicts.dpatch, unnamed
messages: + msg20874
2019-06-25 09:34:04bfrksetfiles: - bugfix-in-v3_commutenoconflicts.dpatch
2019-06-25 09:34:08bfrksetfiles: - bugfix-in-v3_commutenoconflicts.dpatch
2019-06-25 09:34:13bfrksetfiles: - patch-preview.txt
2019-06-25 09:34:16bfrksetfiles: - patch-preview.txt
2019-06-25 09:34:19bfrksetfiles: - unnamed
2019-06-25 09:34:20bfrksetfiles: - unnamed
2019-06-28 11:57:50bfrksetstatus: needs-screening -> needs-review
2019-07-28 13:58:27ganeshsetstatus: needs-review -> accepted-pending-tests
messages: + msg20988
2019-07-28 19:38:50ganeshsetstatus: accepted-pending-tests -> accepted
2019-07-29 09:59:20bfrksetmessages: + msg21000