[darcs-users] Feedback please, Darcs subsystem for lightweight formal verification

[Iago Abal]

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 <iago.abal at gmail.com> 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 <dagitj at gmail.com> 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/>
>>   * 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.osuosl.org/pipermail/darcs-users/attachments/20101105/bebbc372/attachment.html>