Proof of a multi-threaded application

newer
Deploying a Binary Haskell Package

older
Re: [Haskell-cafe] implementing...

Silviu ANDRICA

17 Nov 2008 17 Nov '08

11:04 a.m.

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. Thank you and I hope you can help me, Silviu ANDRICA.

Show replies by date

Luke Palmer

17 Nov 17 Nov

12:52 p.m.

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

Ketil Malde

1:05 p.m.

"Luke Palmer" writes:

...

STM

My apologies for side-tracking, but does anybody have performance numbers for STM? I have an application waiting to be written using STM, boldly parallelizing where no man has parallelized before, but if it doesn't make it faster, the whole excercise gets a lot less convincing. Most material I find seems to be of the proof-of-concept kind. -k -- If I haven't seen further, it is by standing in the footprints of giants

Tim Docker

10:59 p.m.

Ketil Malde wrote:

...

My apologies for side-tracking, but does anybody have performance numbers for STM? I have an application waiting to be written using STM, boldly parallelizing where no man has parallelized before, but if it doesn't make it faster, the whole excercise gets a lot less convincing. Most material I find seems to be of the proof-of-concept kind.

Faster than what? I've used STM for a real application, and the main benefit I saw was in using a set of primitives that facilitate writing concurrent code that is clearer and more likely to be correct. Performance is fine - given it is IO bound, the time taken by STM is not an issue in this case. Are you considering using STM just to make otherwise pure code run in parallel on multiple cores? If so, then perhaps the pure parallelisation primitives are more appropriate. Tim

Ketil Malde

18 Nov 18 Nov

6:35 a.m.

"Tim Docker" writes:

...

...
My apologies for side-tracking, but does anybody have performance numbers for STM? I have an application waiting to be written using STM, boldly parallelizing where no man has parallelized before, but if it doesn't make it faster,

...

Faster than what?

Faster than an equivalent non-concurrent program. It'd also be nice if performance was comparable lock-based implementation.

...

Are you considering using STM just to make otherwise pure code run in parallel on multiple cores?

No, I have a complex structure that must be updated in non-predictable ways. That's what STM is for, no? -k -- If I haven't seen further, it is by standing in the footprints of giants

Ryan Ingram

7:14 a.m.

If you have multiple agents interacting with some structure and you want it to look like each of them is accessing it serialized, then STM is exactly what you want. The performance is always "in comparison to what"; you will likely get worse performance than the "best possible" implementation of your algorithm using locks, but that algorithm may be very difficult to write. My intuition is that if you spend put two programmers on a task, one using STM and one using locks, that the STM solution will perform better given the same amount of implementation time for any non-trivial problem. In addition, you can choose the level of "fine-grained-ness" in STM just as you can with locks, by choosing what things to make into TVars and what things to make pure. For example, this structure:

...

type STMMap a = TVar (Map k a)

will have much different performance than

...

type STMMap k a = TVar (STMNode a) data STMNode a = Tip | Branch !k a (STMMap k a) (STMMap k a)

and either one could be better depending on what you are doing. The former is like a "global lock" on the map, whereas the latter is analgous to "fine-grained" locks. But writing an algorithm using the "fine grained locks" version is a lot simpler to get right in STM than doing so with locks directly. In addition, STM's "optimistic concurrency" gives you the equivalent of multiple-reader single-writer locks for free; writing code with those directly is even more difficult to get right! -- ryan On Mon, Nov 17, 2008 at 10:35 PM, Ketil Malde wrote:

...

"Tim Docker" writes:

...
...
My apologies for side-tracking, but does anybody have performance numbers for STM? I have an application waiting to be written using STM, boldly parallelizing where no man has parallelized before, but if it doesn't make it faster,

...
Faster than what?

Faster than an equivalent non-concurrent program. It'd also be nice if performance was comparable lock-based implementation.

...
Are you considering using STM just to make otherwise pure code run in parallel on multiple cores?

No, I have a complex structure that must be updated in non-predictable ways. That's what STM is for, no?

-k -- If I haven't seen further, it is by standing in the footprints of giants _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Neil Davies

9:12 a.m.

Ketil You may not be asking the right question here. Your final system's performance is going to be influenced far more by your algorithm for updating than by STM (or any other concurrency primitive's) performance. Others have already mentioned the granularity of locking - but that one of the performance design decisions that you need to quantify. The relative merits of various approaches are going to come down to issues such as * given that you have a lock what is the cost of locking (in term of the lack of forward progress) * how often will you have to pay this cost (that will be application / data dependent) * given you use STM, what is the (differential) cost of the underlying housekeeping (depends what processing is with the 'atomically') * what is the likelihood that you will have to undo stuff (represents the same cost as the lack of forward progress). So the answer which is better, as it always is, will be - it depends Welcome to the wonderful world of performance engineering. The answer you seek is tractable - but will require more analysis. Neil On 18 Nov 2008, at 06:35, Ketil Malde wrote:

...

"Tim Docker" writes:

...
...
My apologies for side-tracking, but does anybody have performance numbers for STM? I have an application waiting to be written using STM, boldly parallelizing where no man has parallelized before, but if it doesn't make it faster,

...
Faster than what?

Faster than an equivalent non-concurrent program. It'd also be nice if performance was comparable lock-based implementation.

...
Are you considering using STM just to make otherwise pure code run in parallel on multiple cores?

No, I have a complex structure that must be updated in non-predictable ways. That's what STM is for, no?

-k -- If I haven't seen further, it is by standing in the footprints of giants _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Ketil Malde

10:04 a.m.

Neil Davies writes:

...

You may not be asking the right question here. Your final system's performance is going to be influenced far more by your algorithm for updating than by STM (or any other concurrency primitive's) performance.

I may not be asking the right question, but I am happy about the answer, including yours :-) I think STM is semantically the right tool for the (my) job, but for it to be useful, the implementation must not be the limiting factor. I.e running on n+1 CPUs should be measurably faster than running on n, at least up to n=8, and preferably more. With the assuming I can get enough parallelism and avoiding too many rollbacks, of course.

...

Others have already mentioned the granularity of locking - but that one of the performance design decisions that you need to quantify.

Yes. Fine grained - I'm thinking a large Array of TVars. (If you only have a single TVar, it might as well be an MVar, no?) -k -- If I haven't seen further, it is by standing in the footprints of giants

Neil Davies

12:13 p.m.

On 18 Nov 2008, at 10:04, Ketil Malde wrote:

...

Neil Davies writes:

...
You may not be asking the right question here. Your final system's performance is going to be influenced far more by your algorithm for updating than by STM (or any other concurrency primitive's) performance.

I may not be asking the right question, but I am happy about the answer, including yours :-)

I think STM is semantically the right tool for the (my) job, but for it to be useful, the implementation must not be the limiting factor. I.e running on n+1 CPUs should be measurably faster than running on n, at least up to n=8, and preferably more.

More detailed questions: how complex is the mutual exclusion block? If it is well known now and not likely to change you can implement several ways and work out any extra overhead (run it lot) against the other approaches. Nothing like a quick benchmark. Otherwise stick with STM (its composable after all).

...

With the assuming I can get enough parallelism and avoiding too many rollbacks, of course.

Its not the parallelism that is the issue here, it is the locality of reference. If you have data that is likely to be widely spread amongst all the possible mutual exclusion blocks then you are on to a winner. If your data is clustered and likely to hit the same 'block' then, whatever you do, your scalability is scuppered. Also, consider how much concurrency you've got, not just the parallelism. You need enough concurrency to exploit the parallelism but not too much more - too much more can start creating contention for the mutual exclusion blocks that would not have existed at less concurrency.

...

...
Others have already mentioned the granularity of locking - but that one of the performance design decisions that you need to quantify.

Yes. Fine grained - I'm thinking a large Array of TVars. (If you only have a single TVar, it might as well be an MVar, no?)

What do those TVars contain? how many of them are being updated atomically?

...

-k -- If I haven't seen further, it is by standing in the footprints of giants

Neil

Ryan Ingram

12:27 p.m.

On Tue, Nov 18, 2008 at 2:04 AM, Ketil Malde wrote:

...

Yes. Fine grained - I'm thinking a large Array of TVars. (If you only have a single TVar, it might as well be an MVar, no?)

With only one I think that IORef + atomicModifyIORef might even be better! :) -- ryan

Hans van Thiel

3:03 p.m.

On Mon, 2008-11-17 at 05:52 -0700, Luke Palmer wrote:

...

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

6076

Age (days ago)

6077

Last active (days ago)

List overview

Download

10 comments

7 participants

participants (7)

Hans van Thiel
Ketil Malde
Luke Palmer
Neil Davies
Ryan Ingram
Silviu ANDRICA
Tim Docker