Well, just for playing I made the following:
First I defined a relation Effect2 which given two patches p, q relates a
tree t with another tree t' if t' = q (p t).
*fun Effect2[p, q : Patch] : Tree -> lone Tree =def { t1, t3 : Tree | exists
t2 : Tree, t2 = p t1 /\ t3 = q t2 }*
*Note about notation*: Effect2 is a simple relation (a partial function) so
given a tree exists at most one related tree, but it isn't a entire relation
(so it is not a function).
So I was able to prove a more interesting weaker version of
effect-preserving:
* forall h1,h2,h2',h1' : Hunk,
h1,h2 <-> h2' h1' ==> Effect2[h1,h2] in Effect2[h2',h1'] \/
Effect2[h2',h1'] in Effect2[h1,h2]*
which is *true*.
Well, I think this results are interesting and have some (maybe small) value
:) As far as I know, the Coq formalization done by Ian provides proofs about
this things, but if I'm not wrong the definition of commuteHunk is not a
copy of Darcs (but a restriction) implementation as it is in our case.
On Sat, Nov 6, 2010 at 2:47 PM, Iago Abal <[email protected]> wrote:
> Hi Ganesh,
>
> (And thanks again for your interest!)
>
> Int overflow is "under control". As I said you we have seen that
> commuteHunk is not sound when an Int overflow occurs. The idea is simple, we
> defined an invariant over Hunks and we saw that commuteHunk does not
> preserve that invariant (it is not safe). The counterexample is trivial,
> since commuteHunk performs additions/substractions an overflow may cause a
> Hunk to point to a negative line number.
>
> This is the last I comment to you in the IRC (surely better explained), but
> this is solved. In fact, we not only check if an Int overflow occurs, but we
> also check if a Hunk respect FS limits (i.e. we guarantee that every hunk is
> applicable to some tree). The next step was, as you said, to add
> pre-conditions that make commuteHunk safe, and then we have check four
> properties of hunk commutation (of commmutation in general, but we were
> interested in Hunks problems), three of them stated in page 5 of Jacobson's
> paper:
>
> In the following *false* means *false*, but *true* means "*true* in a
> finite universe of 1 file, 2 different lines, and a maximum of 3 lines per
> file".
>
> 1. if p q are sequential, and p q <-> r s, then r s are sequential too.
> This is *true*.
> 2. Commutation is effect preserving: i.e. p q <-> r s, then effect(r s)
> = effect(p q). This is *false*. In a infinite universe may be true, and
> in fact I do not find a counterexample that is not true in a infinite
> universe... To understand the problem consider the "expanded" formula:
> *forall p q r s : Hunk, t1 t2 t3 : Tree, t2 = p t1 /\ t3 = q t2 /\ p q
> <-> r s ==> exists t2' : Tree, t2' = r t1 /\ t3 = s t2'*. Such t2' is
> not guaranteed to exists because it may be a tree with a file with 4 lines
> (the imposed limit was three).
> - This only states that "effect(r s) is in effect(p q)", but
> symmetric property would complete the equality.
> - We have defined "be-applicable-to": p (Patch) isApplicableTo t (Tree)
> =def exists t' : Tree, t' = p t. And a "weak" effect-preserving property
> saying: *forall p q r s : Hunk, t1 t2 t3 : Tree, t2 = p t1 /\ t3 = q
> t2 /\ p q <-> r s /\ r isApplicableTo t1 ==> exists t2' : Tree, t2' = r
> t1
> /\ t3 = s t2'*. This is *true*.
> 3. Commutation is symmetric: p q <-> r s, then r s <-> p q. This is
> *true*.
> 4. Rotating: p q <-> r s, then inv(r) p <-> s inv(q). This is *true*.
>
>
>
> On Sat, Nov 6, 2010 at 12:56 PM, Ganesh Sittampalam <[email protected]>wrote:
>
>> Hi Iago,
>>
>> My feeling is that the Int limits are indeed effectively irrelevant, but
>> it is good to at least be aware of them.
>>
>> Are there some preconditions you can put on your checks and then prove
>> that things work ok with those preconditions? (e.g. that hunk position +
>> length of new contents is never out of range). That would provide valuable
>> confidence that we really understand the effects of the limits.
>>
>> Cheers,
>>
>> Ganesh
>>
>>
>> On Fri, 5 Nov 2010, Iago Abal wrote:
>>
>> Just for who is interested in this experiment, or for who is interested
>>> in
>>> Darcs correctness.
>>>
>>> After some weeks of work, we are starting to get some results. We are
>>> modeling a filesystem that offers an API as expected by Darcs (a very
>>> simple
>>> version of {Readable/Writable}Repository) and modeling patches over it.
>>>
>>> Model-check Darcs is quite tricky! We have had to construct a complete
>>> universe of all possible trees up to some limits (number of files, lines
>>> per
>>> file, etc)... which makes the process a bit slow (but automatic anyway
>>> :),
>>> and check an assertion could take arround 10 minutes (even with a very
>>> small
>>> universe of 63 trees...).
>>> Maybe you won't care about this, but we are getting many counterexamples
>>> due
>>> to a fact that is not considered in the theory but it is the main source
>>> of
>>> obscure bugs in the real world... «there are limits: machine integers can
>>> overflow, files can't be arbitrary big, etc», so for instance, it is not
>>> true the effect-preserving property of patch commutation. To be honest
>>> I'm
>>> not completely sure if this matters due to the actual limits of
>>> filesystems
>>> (etc), maybe it is a bit irrelevant in practice, depends if you care
>>> Darcs
>>> could be a piece of software used in NASA missions ;)
>>>
>>> On Sat, Oct 9, 2010 at 8:23 PM, Iago Abal <[email protected]> wrote:
>>>
>>> Thanks for your (really quick) replies, I'm very pleased to see that
>>>> this
>>>> project is of interest for some of you.
>>>>
>>>> On Sat, Oct 9, 2010 at 6:52 PM, Jason Dagit <[email protected]> wrote:
>>>>
>>>> Iago,
>>>>>
>>>>> Thanks for your interest. I think this sounds like a really exciting
>>>>> project. It's exciting that you're interested in using model checking
>>>>> on
>>>>> darcs! I hope you pick this project and make progress.
>>>>>
>>>>>
>>>>> Hi Iago,
>>>>>>
>>>>>
>>>>>
>>>>> On Sat, 9 Oct 2010, Iago Abal wrote:
>>>>>>
>>>>>
>>>>>
>>>>> I will try to be brief but concise. I'm a MSc student doing a
>>>>>>>
>>>>>> formal-methods
>>>>>>
>>>>>
>>>>> course about "analysis, modeling and testing". This course has a
>>>>>> project
>>>>>>
>>>>>
>>>>> component which consists on modeling a problem using Alloy[1], verify
>>>>>>
>>>>>
>>>>> (lightweight approach) properties about the problem using that model,
>>>>>> code
>>>>>>
>>>>>
>>>>> the problem (if there is no available code) annotating the code with
>>>>>>
>>>>>
>>>>> contracts and, finally, test it. Of course, the final goal is to
>>>>>> ensure
>>>>>> that
>>>>>>
>>>>>
>>>>> the real code actually meets its specification.
>>>>>>
>>>>>
>>>>>
>>>>> One thing I'm confused about here - can Alloy actually model check
>>>>>>
>>>>>
>>>>> Haskell? If not, how would you be able to ensure anything about the
>>>>> real
>>>>>
>>>>> code?
>>>>>
>>>>>
>>>>> If I understand Iago correctly, the goal is to check the specification
>>>>> abstractly and then later check the code against tests derived from the
>>>>> specification / model checking.
>>>>>
>>>>> Exactly. As I said, Alloy is a lightweight approach, so we will prove
>>>> things about a *model* of the real system and not about the real system
>>>> itself. But contracts and testing will let us to *believe* that the real
>>>> system corresponds to our model and satisfies its properties (produce
>>>> code
>>>> refining specification is not part of the project goals).
>>>>
>>>> One of our "problems" is the lack of good support for design-by-contract
>>>> in
>>>> Haskell. The "standard way" will be ".NET + Contracts" though
>>>> course-teacher
>>>> said to be interested on modeling Darcs and he accepts to work with
>>>> Haskell
>>>> using "something" for contracts, and QuickCheck/SmallCheck for testing.
>>>>
>>>>
>>>>>
>>>>>
>>>>>> Ok so... the project is done by groups and we are collecting
>>>>>>> proposals
>>>>>>>
>>>>>> for
>>>>>>
>>>>>
>>>>> this project, and, I was thinking in something related to Darcs. I
>>>>>> have
>>>>>> to
>>>>>>
>>>>>
>>>>> take more serious look for this, but currently I think that model
>>>>>>
>>>>>
>>>>> patch-theory and test Darcs.Patch.* code could be a choice. My
>>>>>> question
>>>>>> is,
>>>>>>
>>>>>
>>>>> if someone could propose Darcs subsystems that 1) have a
>>>>>> well-documented
>>>>>>
>>>>>
>>>>> specification complex enough to be of interest modeling and verifying
>>>>>> it, 2)
>>>>>>
>>>>>
>>>>> have small/medium-size implementation understandable just with few
>>>>>> weeks
>>>>>> of
>>>>>>
>>>>>
>>>>> work 3) it is of interest for the Darcs community (I think this point
>>>>>> is
>>>>>>
>>>>>
>>>>> important if we want to get some help from you like answering "boring
>>>>>>
>>>>>
>>>>> questions").
>>>>>>
>>>>>
>>>>>
>>>>> I think that some of the internals of Darcs.Patch would be a
>>>>>> reasonable
>>>>>>
>>>>>
>>>>> candidate, if you start small and work your way up as time permits.
>>>>>
>>>>>
>>>>> I'm not entirely sure what kind of specification you want, but darcs
>>>>>>
>>>>>
>>>>> patches satisfy various equational laws, and also have the higher-level
>>>>>
>>>>> property that commuting two patches in a sequence doesn't affect the
>>>>>
>>>>>> final
>>>>>>
>>>>>
>>>>> result of that sequence.
>>>>>
>>>>>
>>>>> Resources to help you get started with this include:
>>>>> * My MS thesis about darcs: http://files.codersbase.com/thesis.pdf
>>>>> * My thesis talk slides: http://files.codersbase.com/thesistalk.pdf
>>>>> * Judah Jacobson's formalized patch theory:
>>>>> http://www.math.ucla.edu/~jjacobson/patch-theory/<http://www.math.ucla.edu/%7Ejjacobson/patch-theory/>
>>>>> <http://www.math.ucla.edu/%7Ejjacobson/patch-theory/>
>>>>>
>>>>> * Ian Lynagh's Camp: http://projects.haskell.org/camp/
>>>>>
>>>>> Camp is interesting as it has almost the same underlying theory as
>>>>> darcs
>>>>> but there have been more efforts to formalize it. In this case, using
>>>>> the
>>>>> theorem proving language Coq. Just check around on the camp site and
>>>>> you
>>>>> should find links to the proofs.
>>>>>
>>>>>
>>>>> Thanks for the resources links! I will take a look this days to get
>>>> the big
>>>> picture and have some idea of the complexity of formalizing all the
>>>> patch
>>>> stuff.
>>>>
>>>> Answering Ganesh:
>>>>
>>>> I'm not entirely sure what kind of specification you want
>>>>
>>>>>
>>>>> A Darcs repository is consistent iff P holds, commuting patches A and
>>>> B
>>>> under conditions C is a valid operation, etc. I don't know a lot about
>>>> Darcs
>>>> theory, but I think that patch commutation is an important thing and it
>>>> could be the center of the verification effort.
>>>>
>>>>
>>>>
>>>>> I think if you started with "hunk" patches on a single file, then you
>>>>>>
>>>>>
>>>>> would have a tractable problem to begin with which you could then build
>>>>>
>>>>> on. I'd be happy to help with understanding the code and how it's meant
>>>>>
>>>>>> to
>>>>>>
>>>>>
>>>>> behave.
>>>>>
>>>>>
>>>>> Some things of interest that you might be able to check:
>>>>> * Are token replace patches well behaved when commuting with hunk
>>>>> patches?
>>>>> * Are there cases where darcs algorithms go exponential in run-time?
>>>>> * Interaction between setpref patches and normal patches
>>>>> * Not patch theory related: Exception handling, cleaning up, and
>>>>> transactional properties
>>>>>
>>>>> I think Ganesh is right about starting small. For example start with
>>>>> hunk-hunk commutes and see what you get. Even simpler might be file
>>>>> add/remove patches. I noticed that the Alloy tutorial models a unix
>>>>> file
>>>>> system. That may actually be a great place to start with your work.
>>>>> Then
>>>>> build up to transformations on the file system objects, and so on.
>>>>> I've
>>>>> been thinking about starting from that point in a language such as
>>>>> Agda. If
>>>>> only I had more spare time.
>>>>>
>>>>> Yes, right, the idea is to start small and work, at least, until get a
>>>>>
>>>> model with enough complexity for the course goals. I hope to be able to
>>>> get
>>>> something interesting for Darcs too -- I know last year there was a
>>>> project
>>>> related to model Subversion but it was not completed (so, it was
>>>> something-like-subversion).
>>>>
>>>>
>>>> You should not feel shy about asking us questions on the list.
>>>>> Rigorously
>>>>> verifying darcs is of great interest to quite a few of us and the
>>>>> discussions are very helpful to everyone.
>>>>>
>>>>>
>>>>
>>>>> I hope that helps.
>>>>
>>>>> Jason
>>>>>
>>>>> Yeah, that helps, thanks!
>>>>
>>>>
>>>> --
>>>> Iago Abal Rivas
>>>>
>>>>
>>>
>>>
>>>
>
>
> --
> Iago Abal Rivas
>
--
Iago Abal Rivas
_______________________________________________
darcs-users mailing list
[email protected]
http://lists.osuosl.org/mailman/listinfo/darcs-users
