On Mon, Nov 17, 2008 at 4:04 AM, Silviu ANDRICA
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