Correct-by-construction Concurrency

I’ve been hacking merrily away in Idris over the last couple of weeks, seeing what I can make it do. One of the first things I wanted to try was an idea I had for a domain specific embedded language (DSEL) for concurrent programming. The result is written up in this draft paper.

I think one of the areas where dependently typed languages will become important, given appropriate and mature tools, will be the design and implementation of verified DSEL.
Here we use a DSEL to manage the lock state (i.e. number of times locked, type of the value stored in it) of each shared resource - it’s essentially a state monad parametrised over the type and lock status of the resources - which means that the lock state is statically known. As a result, the typechecker can verify that resources are locked before they are accessed, released before exit even in exceptional conditions, and even that they are requested in an order which guarantees deadlock freedom. Programs in the DSEL look (more or less) like monadic Haskell programs.

There is, as you would expect, an occasional need for an explicit proof term, especially to convince the typechecker that resource requests are ordered in a way which guarantees deadlock freedom. These proof terms can be computed dynamically if necessary, and we have found in practice that, when the ordering is safe, the proofs are reasonably simple. So assuming that you have put some thought into why your program is deadlock free, there should be no difficulty in proving it. I do think this is a situation where good tool support is necessary though - for the sake of the reader of the program, how do you hide the proof details so as not to obscure the algorithm, and for the sake of the programmer, how much can you automate? Can the DSEL author provide a library of lemmas and decision procedures to take the burden of proof away as far as possible? If you want complete static safety, as you probably do in a safety critical real-time system, you should expect to have to do some work to prove it, but we want to make this as painless as possible!

Any comments much appreciated!