Modeling tools

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 were further along, then Microsoft would do the integration for me.


Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s

%d bloggers like this: