[Haskell-cafe] Proof of a multi-threaded application

[Hans van Thiel]

On Mon, 2008-11-17 at 05:52 -0700, Luke Palmer wrote:
> On Mon, Nov 17, 2008 at 4:04 AM, Silviu ANDRICA <silviu.andrica at epfl.ch> wrote:
> > Hello,
> >   I am very new to Haskell, this is my first day, and I wanted to know if it
> > is possible to prove correctness of a multi-threaded application written in
> > Haskell.
> > Basically, I want to check that a multi-threaded implementation of an
> > algorithm that detects cycles in a dynamically changing graph, actually
> > detects the cycles. Also, the algorithm prevents previously detected cycles
> > from happening by not allowing certain edges to be added. And I want to
> > check that this property also holds.
> 
> This is going to be difficult -- no matter what language you try to
> prove it in.  In Haskell you have a decent shot, I suppose, since you
> could at least prove the pure bits correct without much fuss.
> 
> The way I might try to approach this is to model your algorithm and
> the dynamically changing graph together as a nondeterministic state
> machine: a function of type State -> [State]  (returning all the
> possible "next steps" of the system).  Then I would look for some
> invariant that is preserved at each step, and prove its preservation.
> 
> That is how you could prove your *algorithm* correct.  But I suspect
> there will be many difficulties proving that your implementation
> corresponds to your algorithm.  This is mostly because in the IO
> monad, "anything goes"; i.e. the semantics are complex and mostly
> unknown.  You might make some progress by isolating a small portion of
> the IO monad and assuming that it obeys some particular reasonable
> nondeterministic semantics.  But that will be a large, intuitive
> assumption which will decrease the degree of certainty of your proof.
> 
> If you implement your algorithm in terms of STM (one of Haskell's
> flaunting points :-) rather than more traditional primitives (eg.
> locks) you will have a better shot, since you can more easily show
> that an invariant is kept before and after a transaction, without
> having to fuss with the concurrency details inside where the invariant
> is briefly broken.
> 
> Concurrency is quite hard to reason about formally (no matter what
> language it is in).  Good luck!
> 
> Luke
> 
Yes, but if it's worth the effort you could do a formal verification,
not of the code, but of a model with the Spin model checker.

http://spinroot.com/spin/whatispin.html

First you write a model in Promela (Process meta language) which looks a
lot like C, but abstracts from (most of) the computations and instead
concentrates on communication and coordination of non-deterministic
processes. With Spin and the graphical interface XSpin (or the
alternative JSpin) you can both simulate and verify your model.
It finds deadlocks, you can write asserts, test liveness and you can
even check claims in LTL (linear temporal logic) about execution paths.
It's all open source and free. 'The Spin Model Checker', by Gerard
Holzmann, is the reference, but there are several other books about Spin
and its principles. 

Best Regards,

Hans van Thiel