On Apr 10, 8:58 am, "Edward K. Ream" <[email protected]> wrote:
> In this thread, I will attempt to state and prove one or more @shadow
> theorems, which generally state that any group of people can use
> @shadow files in cooperative (bzr) environments.
After studying the @shadow code, it appears that the the proof of the
various @shadow theorems may be easier than I thought. BTW, the heart
of the @shadow update algorithm is in propagate_changed_lines. There
are lots of administrative details handled elsewhere, but except as
discussed in the conclusion we can completely ignore those details.
The present @shadow code does *not* check file modification dates of
the public and private files (A and A'). When reading an @shadow
node, the @shadow update algorithm *always* use he contents of the
public file A. Since node structure can only come from the private
file A', we have the following aphorism:
@shadow takes content from the public file and structure from the
private file.
Let's look at the four cases:
Case 1: Alice doesn't use Leo, and pushes only A. Bob pulls A.
Case 2: Alice pushes A. Bob pulls A. Alice pushes A'. Bob pulls A'.
Case 3: Alice pushes A'. Bob pulls A'. Alice pushes A. Bob pulls A.
Case 4: Alice pushes both A and A' before Bob pulls either. Bob then
pulls A and A'.
Actually, these cases are a bit misnamed. By "pulling" I mean that
Bob not only pulls a file, but then uses Leo to open the pulled file
and saves the result. That is,it doesn't matter what happens with
respect to bzr until Bob actually uses the pulled file.
Case 1: Alice doesn't use Leo, and pushes only A. Bob pulls A.
The structure will never change, and Bob gets the new content when Bob
pulls A, that is, pulls A and opens the .leo file containing @shadow
A.
Case 2: Alice pushes A. Bob pulls A. Alice pushes A'. Bob pulls A'.
Bob gets the new content after pulling A, and gets the new structure
after pulling A'. Pulling A' **retains the content of A**.
Case 3: Alice pushes A'. Bob pulls A'. Alice pushes A. Bob pulls A.
Pulling A' changes the structure of the @shadow tree, but leaves the
content unchanged. Pulling A updates the content of A, while leaving
the structure unchanged.
Case 4: Alice pushes both A and A' before Bob pulls either. Bob then
pulls A and A'.
Pulling A and A' simultaneously updates the content from A and the
structure from A', just as with either Case 2 or Case 3.
So it would appear that the theorem has been proved. In fact, there
are some details to make explicit:
1. Recall that the original proof (July 2008) that @shadow was safe
was the Aha that boundary cases in inserting or deleting lines do
*not* affect the corresponding public file. See
http://groups.google.com/group/leo-editor/browse_thread/thread/4c2fcd3d26bc546d/023be7e2812eb7c0
This same Aha makes the assertions about Cases 2, 3 and 4 correct.
That is, the resulting public file will be the same **no matter how
the @shadow update algorithm assigns lines to nodes**. Thus, it
doesn't matter what nodes exists (what the structure of the @shadow
tree is) when the @shadow update algorithm runs.
2. In the more general situation, in which Alice,Carol,Doug, etc. are
all merrily committing away without regard to the order in which they
push A and A', seems to be essentially the same. No matter how many
people are committing, content always comes from A, node structure
comes from A', and the resulting public file will always be determined
solely by the latest version of A that has been pulled.
3. Bzr conflicts involving A and A' can, of course, occur. In some
sense, they will be resolved as usual. However, because programmers
can wait a long time between committing A and A', these conflicts can
be delayed as well. I don't believe that this is likely to be a
significant problem in practice.
Conclusions
1. Imo, we are now in a position to start experimenting with using
@shadow to manage files in bzr repositories. I plan to begin by
experimenting on local repositories. I would be hasty, imo, simply to
convert Leo's sources to @shadow files.
2. At present, the @shadow update algorithm is "stateless" in the
sense that it works the same regardless of the file modification dates
of A and A'. This is mostly a happy accident.
3. Naturally, Leo invokes the @shadow update algorithm only when A and
A' both exist. If only A' exists, we want to use it. If only A
exists, we want to use Leo's import code. These are the
"administrative details" mentioned at the start of this reply. I'll
change how @shadow works in this regard as needed.
In short, it seems that the various @shadow theorems have been proven
well enough for now. I have included all my reasoning here in the
hopes that:
a) Everyone can see why using @shadow in bzr repositories might work,
b) Someone will correct me if there are problems with the proofs.
All comments and suggestions are welcome.
Edward
--~--~---------~--~----~------------~-------~--~----~
You received this message because you are subscribed to the Google Groups
"leo-editor" group.
To post to this group, send email to [email protected]
To unsubscribe from this group, send email to
[email protected]
For more options, visit this group at
http://groups.google.com/group/leo-editor?hl=en
-~----------~----~----~----~------~----~------~--~---
