Home » forums » LtU Forum

Neophyte question: detecting deadlock, livelock, races etc.

Since I've seen things like TyPiCal claim to perform static deadlock detection, I wonder why such presumably powerful tools don't seem to be more prevalent. There seem to be a few formal method languages and tools which help folks avoid deadlock etc., but then you have to convert that into the final language and hope it really does match the theory. And, most programmers don't know the theory or tools enough to use formal methods, or think they are in too much of a rush to afford them.

So I'm just wondering if there any less-formal programming language systems that have static deadlock, livelock, etc. detection? E.g. Erlang is great, but does it have any tools to help dis/prove such useful and important aspects of your final system? Might there be a relatively simple way to use TyPiCal with, say, occam-pi? Are there research-y programming systems that might address these bugaboos?

By raould at 2006-09-12 18:30 | LtU Forum | previous forum topic | next forum topic | other blogs | 7297 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Occam-pi

The classical formalism for designing occam programs is CSP. There are several tools out there (FDR2, Jeremy Martin's deadlock-checker) for doing checks on properties like deadlock and livelock on CSP process networks. The mapping from CSP to occam (or libraries that emulate occam in other languages) is pretty straightforward. So much so that there've been a few efforts towards performing automated code generation (see here or here for examples).

For those who don't want to mess with CSP directly, or have to deal in formalisms, probably the easiest thing to do is to make use of patterns of process network construction that have already been formally proved free of deadlock. Peter Welch did some excellent work a few ywars back on patterns of occam interprocess communication that were provably deadlock-free. If you construct certain kiinds of networks out of processes that obey IO-Seq or IO-Par patterns, you can avoid deadlock. Better yet, certain patterns of networks are provably equivalent to a single IO-Seq or IO-Par process, which makes it possible to design things in a hierarchical fashion. Other design rules can be found in Bill Roscoe's text on CSP, and Jeremy Martin's PhD thesis.

Of course, occam-pi adds pi-calculus-like constructs to the occam language, which makes it a little more difficult model in CSP. However, Peter Welch has done some preliminary work on a CSP semantics for occam-pi's mobile constructs (to which I've made a few minor contributions). There's probably a need for more work on design rules and patterns though. That work could presumably also be done in the pi-calculus, once a suitable mapping has been established to occam-pi.

More generally, static detection of things like deadlock directly from program code requires either tools to abstract the code into a formalism which supports deadlock-detection (for example, Gerard Holzmann has done some work on automatically abstracting C into Promela for checking with the SPIN model-checker), or a powerful type system ala TyPiCal. There's been some work in the direction of abstraction and model-checking for Erlang - see here or here. The most recent work along those lines that I'm aware of has been by Thomas Noll.

By Allan McInnes at Tue, 2006-09-12 20:24 | login or register to post comments

Thanks for the news

It is good to know that there are some choices, thanks for the detailed news. When I run my own company making hand-held devices that run on FPGAs, they will be running verified CSP code :-)

<ot rant>
While it is reassuring to know that folks are working on such issues, it sounds like they perhaps aren't quite what would be called commercial quality or mainstream. I think that's the fault of our entire industry that we don't take such advances and really incorporate and advance them.

It still irks and befuddles me that the software engineering world has not apparently gotten to the point where using systems that allow deadlock, livelock, races, starvation, whatever is considered gauche. Why aren't we all (in the most expansive sense possible) reaching for a higher standard? Maybe everybody really finds it interesting to spend time and energy tracking down deadlock bugs?! I just don't get it. I kinda think that, to paraphrase the Dead Milkmen, we should all have the attitude that if your software system ain't got {memory protection, automatic memory management, static type checking with automatic type inference, threading bug detection and prevention, etc.} then your software system could use some fixin'.
</ot rant>

By raould at Wed, 2006-09-13 18:09 | login or register to post comments

Obviously, I Can Only Say...

...hear, hear!

By Paul Snively at Fri, 2006-09-15 16:26 | login or register to post comments