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

[Luke Palmer]

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