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
_______________________________________________
darcs-users mailing list
[email protected]
http://lists.osuosl.org/mailman/listinfo/darcs-users
