C++ Annotations not so pointless? Plus some UMTS history.

Let me start this post with a retrospection: long long time ago I promised to write a blogpost about multithreaded testing, temporal logic and (even) the boundaries of knowledge. Pretty high claims, you'd say, and you'll be of course right, as I didn't write it despite of a few false starts. So though the wholesale treatment of this theme isn't possible now because I plain and simply forgotten much of the details, I'll try to catch the opportunity to pay off my "blogging debt" and use that stuff in a condensed form as intro for this post.

1. Past struggles

So then, long long ago I was writing an multithreading application (or rather a framework* for other programmers to use) under Linux/pthreads against an underspecified multithreading interface of a "General Telco Systems Programming Platform" ;) - let call it GTSPP;). It was underspecified because it was still being developed while we were writing production code to be deployed on backplane UMTS switches.

Well, what can I say, the regular multinational project's madness, alleged synergy, and all that stuff... But, perhaps surprisingly to you, I wanted to have that thing thoroughly tested! And I mean tested! After I found some unexpected behaviour of GTSPP;) and resulting deadlocks, I didn't want to allow it to happen again.

As at that time I was interested in logic, automatic theorem proving and generally in foundational speculations, I had that brilliant (or at least I thought that...) idea - why don't we just describe a multithrerading system in terms of modal logic, like that:

• []T (read: box T) meaning: T alway happens
• <>T (read: diamond T) meaning: T sometimes happens

 and then use automatic derivation do derive some theorems of thatt system? Like "Theorem 1: there will never be a deadlock here".  [In the originally planned post a lot of explanantions about Kripke, possible worlds, Buchi automata... and model checking would follow here... BUT this isn't the planned post, sorry!]

At last some sensible use of maths! Can't believe it, so these whole math classes weren't a total waste of time?

Well, yes and no. As I tried several open source products, none of them was able to read C++ code, annotate it with modal logic, and infer the needed theorems. You call me naive? But that's exactly what SPIN is doing! The only problem was that SPIN doesn't accept C or C++ code, but only it's own description language: Promela. So I had to recode my system in Promela. That was out of the question, as I didn't have so much time. Writing a general translator C++ to Promela translator was beyond question as well - Clang wasn't there yet!

SPIN's author did some interesting work for AT&T on translating C code to SPIN format and even open-sourced it, but as I tried to install it on my Linux machine I failed. Some package dependency was missing, and our sysadmin asserted that there's no no such package for the RedHat distribution... At that point I gave up** thinking: the real boundaries of knowledge are that of human laziness...

2. New hope?

You may remember that I wrote a post "Two C++ curiosities..." where I expressed my inability to grasp the reason for the introduction of attributes in C++ (apart from Microsoft's influence). Recently, the same Microsoft organized a C++ conference  with quite a good video coverage. As I happened to listen to the Clang presentation i noticed some interesting usage of that language feature. It looked roughly like that:

or in gcc's syntax:

Do you see that? Now you can add an attribute to multithreaded code and let the compiler check if it's deadlock and starvation free!

That's what I call a sensible vendor specific extension! Well, it could be, as at the present all this isn't available yet (it's a research project at Microsoft's) but at least now I learned one case where the attributes could do quite a good job!

PS: More information on that topic: the boost::thread and thread safety annotations post or LLVM docs.

--

* I know, programmers hate frameworks, we were hating GTSPP;) too, but we were merging an another telco framework used in the previous project with the hapless GTSPP;) as not to expose the application programmers to too much madness - you know, brains melting, people screaming, teams disintegrating... So it was a Good Thing in the end!

** You don't really think I gave up on this, do you? So what was my solution? Right! I wrote a Python test driver repeating testcases by 1000s and grepping the output for specified error messages. The classic and proven multithreading testing strategy. Maybe a little brute-force and old-fashioned, but you know what? It did the job!