November 2, 2006
A while back I hacked up a quick and dirty concurrent queue data structure. There was a bizarre timing bug that resulted in random exceptions. The code looked OK to me, but concurrency bugs are sneaky. That’s why it’s important to use a modeling tool to statically check that your program doesn’t have any sneaky concurrency bugs in there. There are two major tools out there: TLA+ and SPIN. There are some other research tools out there, but these might be the most mature. I tinkered with both a long time ago, but I don’t know enough to make a sound judgment (but I found a review). From a non-technical standpoint, SPIN is appealing because it appears to have a larger user base and more documentation (books & papers). My goal is to embed the specifications into my code using XML comments. Then a simple preprocessor will extract the specs and run them through the model checker. That way I can see the spec while I write my code. So it’s important to choose a spec language that can support this development model. Managing separate spec and code files will become tedious. It would be easier if Spec# and Cω were further along, then Microsoft would do the integration for me.