darcs

Issue 2047 Falsifiable Darcs.Test.Patch.Properties.recommute

Title Falsifiable Darcs.Test.Patch.Properties.recommute
Priority bug Status needs-diagnosis/design
Milestone Resolved in
Superseder Nosy List Serware, ganesh, iago
Assigned To
Topics Conflicts, Darcs2

Created on 2011-02-22.13:11:57 by iago, last changed 2014-06-03.22:47:21 by bf.

Files
File name Uploaded Type Edit Remove
falsifiable_recommute iago, 2011-02-22.13:11:56 application/octet-stream
falsifiable_recommute2 iago, 2011-02-24.17:58:14 application/octet-stream
unnamed iago, 2011-02-24.17:58:14 text/html
Messages
msg13725 (view) Author: iago Date: 2011-02-22.13:11:56
Running QuickCheck tests I have found a possible bug (I guess in 
commutation/merging of V2 patches) which breaks recommute property.
I have found the same bug twice, in both cases the problem looks related 
with a conflictor between "move a file into a directory" and "remove that 
directory".
Attachments
msg13755 (view) Author: kowey Date: 2011-02-24.13:46:35
I think we need somebody to study this log and figure out if it's an 
actual bug, turn it into English, and can it.
msg13756 (view) Author: iago Date: 2011-02-24.17:58:14
Another counter-example, may help. In this case the problem appears due to a
conflictor between "edit/remove a file inside a directory" and "remove that
directory".

On Thu, Feb 24, 2011 at 1:46 PM, Eric Kow <bugs@darcs.net> wrote:

>
> Eric Kow <kowey@darcs.net> added the comment:
>
> I think we need somebody to study this log and figure out if it's an
> actual bug, turn it into English, and can it.
>
> ----------
> nosy: +Serware
> priority:  -> bug
> status: unknown -> need-action
> topic: +Conflicts, Darcs2
>
> __________________________________
> Darcs bug tracker <bugs@darcs.net>
> <http://bugs.darcs.net/issue2047>
> __________________________________
>



-- 
Iago Abal Rivas
Attachments
msg15432 (view) Author: owst Date: 2012-03-30.18:26:09
Ok, so I've spent today finally figuring out this bug. Basically, it's
due to the interaction of Duplicates/Conflictors. In this particular
case, we commute a Conflictor past a Duplicate's context, but throw away
the resulting Conflictor, such that we can't do a reverse commute to
obtain the original patches.

Here's a dump of the whiteboard that Igloo and I twiddled with to
determine the problem:

We have an original context of "adddir ./dir1; addfile ./file1.txt"

Then we have two parallel branches, AB and CD:

A: rmdir ./dir1
B: conflictor [
   rmdir ./dir1
   ]
   |:
   move ./file1.txt ./dir1/file3.txt

C: rmdir ./dir1
D: move ./file1.txt ./file2.txt
  
We merge AB :\/: CD to obtain:
  
  A: rmdir ./dir1
  B: conflictor [
     rmdir ./dir1
     ]
     |:
     move ./file1.txt ./dir1/file3.txt
C'': duplicate
     |rotcilfnoc [
     |rmdir ./dir1
     |]
     ||:
     |move ./file1.txt ./dir1/file3.txt
     |adddir ./dir1
     |:
     rmdir ./dir1
D'': conflictor {{
     :
     move ./file1.txt ./dir1/file3.txt
     :
     rmdir ./dir1
     }} []
     :
     move ./file1.txt ./file2.txt

And now we try to commute (C'' :> D'') which results in:

D''':
conflictor {{
|:
move ./file1.txt ./dir1/file3.txt
|:
rmdir ./dir1
}} []
|:
move ./file1.txt ./file2.txt

C''':
duplicate
|rotcilfnoc [
|rmdir ./dir1
|move ./file1.txt ./file2.txt
|]
||:
|move ./file1.txt ./dir1/file3.txt
|adddir ./dir1
|:
rmdir ./dir1

By the definition of Commute (p :> Duplicate), we did a commute of (inv
p) and the "context" of the Duplicate's Non.

So, that is a commute of:

rotcilfnoc {{
|:
move ./file1.txt ./dir1/file3.txt
|:
rmdir ./dir1
}} []
|:
move ./file1.txt ./file2.txt

And:
rotcilfnoc {} [
    rmdir ./dir1
]
|:
move ./file1.txt ./dir1/file3.txt

We do this commute by first inverting, swithching order, then commuting,
then switching order, then inverting.
So, the commute we do is:

conflictor {} [
    rmdir ./dir1
]
|:
move ./file1.txt ./dir1/file3.txt

and

conflictor {{
    |:
    move ./file1.txt ./dir1/file3.txt
    |:
    rmdir ./dir1
}} []
|:
move ./file1.txt ./file2.txt

which (working out by hand) gives us:

move ./file1.txt ./file2.txt

and

conflictor {} [
    move ./file1.txt ./file2.txt
    rmdir ./dir1
]
|:
move ./file1.txt ./dir1/file3.txt

the second of which you can see in the resulting C'''.



However!! the only way of obtaining the original conflictor, is to
commute it back with 'move ./file1.txt ./file2.txt' - but we've thrown
that away, and can't get it back!
msg17504 (view) Author: bf Date: 2014-06-01.16:21:33
OMG. I would have searched the tracker for a duplicate, except I never
expected Darcs to contain a bug like that for over three years and
apparently nobody knows how to fix it. It makes me feel I am wasting my
time fiddling with UI issues.

I am changing the status of this ticket, as this is obviously
reproducible, in fact we have a number of documented cases of failure.
msg17511 (view) Author: ganesh Date: 2014-06-03.05:22:25
We do sort of know how to fix this; Ian Lynagh has formalised and cleaned up the Darcs 2 patch 
algorithm in Camp (http://projects.haskell.org/camp/) and it's likely that by reimplementing 
it in terms of his cleanup that we'd fix the problems in the current implementation.

However, it would require migrating all existing repos to a new patch format (like the darcs-1 
-> darcs-2 transition) so we'd need to be sure it was worth it. I'm not sure that sticking 
with this algorithm at all is actually the right way to go; it's a significant improvement on 
the darcs-1 merge algorithm but it still has some nasty quadratic blowup cases. I've been 
thinking about an alternative off and on for a while but haven't got as far as trying it for 
real: http://darcs.net/Ideas/Graphictors (this page is just a skeleton so far)

Although it's not exactly great that our merge algorithm can go wrong like this, in practice 
people hit it very rarely, and they can work around it by amending out the conflict.

In the meantime we should disable the failing test as it's not telling us anything useful.
msg17519 (view) Author: bf Date: 2014-06-03.22:47:20
Two comments:

* It was my impression that Camp and the corresponding V3 theory is work
in progress and the proofs not yet complete. I'd love to be proven
wrong, of course.

* If it is technically possible at all, however difficult, we should
strive to make conversion V1/V2 -> V3 as painless as possible. Doing it
like with the V1 -> V2 switch, i.e. forcing users to join all existing
branches into a one large repo, then convert, then split up again is
just horrible and completely contrary to Darcs' nature as a distributed
VCS. The new repo/patch format must be designed in such a way that we
can seamlessly integrate the old formats. For instance, pulling form a
V1/V2 repo automatically converts the patches, and the conversion should
not change the hash i.e. the patch identity. I don't care how many dirty
tricks it needs to implement that, but if we don't do it, we'll
certainly loose the rest of our user base.
History
Date User Action Args
2011-02-22 13:11:57iagocreate
2011-02-24 13:46:37koweysetpriority: bug
status: unknown -> needs-reproduction
topic: + Conflicts, Darcs2
messages: + msg13755
nosy: + Serware
2011-02-24 17:58:14iagosetfiles: + unnamed, falsifiable_recommute2
messages: + msg13756
2012-03-30 18:26:10owstsetmessages: + msg15432
2014-06-01 14:33:18owstlinkissue2399 superseder
2014-06-01 16:21:34bfsetstatus: needs-reproduction -> needs-diagnosis/design
messages: + msg17504
2014-06-03 05:22:27ganeshsetmessages: + msg17511
2014-06-03 22:47:21bfsetmessages: + msg17519