ICFP presentation: Practical Proofs of Concurrent Programs by Marc Shapiro

I'm not especially interested in concurrency issues (read that: I'm not sufficiently knowledgeable in the field to be interested). They tend to be difficult, non-hackable problems. That is, you can't just start hacking away on the problem to see what works. You have to prove that your solution works; no amount of testing (much less a quick try through a few edge cases) can prove that it will work. That said, I'm all for people coming up with abstractions or frameworks that ease this problem for those of us who would rather not think about these problems so much. Hats off to them!

Everything before lunch today (Tuesday, the second day of the official conference, my third day day here since I attended this pre-conference Scheme workshop) is on the topic of concurrency so I'm not exactly on the edge of my seat. I wonder if I can catch a nap somehow...

Nevertheless I was interested by the first talk, by Marc Shapiro on using Rely-Guarantee analysis to prove correctness of concurrent programs. If I understand what he is doing, his work shows a new way to divide the concurrency issues of a given program into smaller pieces, each of which may be divided into smaller pieces using the same technique, until the pieces are small enough that the set of all the things that the pieces rely upon are guaranteed by the pieces. If you can do this, your program is proven to be safe with concurrency. I need to read the paper, except it looks like only the abstract is present in the Proceedings of the conference.