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!

Coding styles.

As I was looking at my mate's C++ code I spotted the following curious lines:

  TreeDataCIterator it  ( m_treeDataList.begin() ), 
                    end ( m_treeDataList.end() );

Don't you think it's rather unusual for C++? Myself would rather writhe something more mundane like:

  TreeDataCIterator it = m_treeDataList.begin(); 
  TreeDataCIterator end = m_treeDataList.end();

complying with some old coding guidelines of the dark ages (aka 90-ties) which were imposed on the unhappy programmers in some big, iternational, waterfall project. But, you know, habit is the second nature... So I was somehow perplexed by the originality of the code, as I'd rather expected more dull style (like mine) considered C++'s strong C-legacy. But then I rememebred that my mate was originally a LISP programmer (but then his LISP-based company didn't really take off) and everything became clear! Look at this snippet uf LISP code from the SICP book:

  (define (count-leaves x)
      (cond ((null? x) 0)
            ((not (pair? x)) 1)
            (else (+ (count-leaves (car x))
                     (count-leaves (cdr x))))))

isn't it similiar? The love of parenthesis cannot be cured of easily ;-).

On the other hand, this could be as well an exmple if the C++ initalization syntax, and in C++11 we could write as well:

  TreeDataCIterator it  { m_treeDataList.begin() }, 
                    end { m_treeDataList.end() };

Not that LISPy at all (instead maybe a little confusing)! But seriously, don't you think arguing about this is a loss of time? Well, not really, good code should be readable, and if we care about our code, it's does matter. But then I find myself increasingly obsessed with code formatting and visual appeal of my code. It's certainly not wrong, but it robs my brain of its preciuos ressources. Remember? Your brain can hold in memory only 6-7 items at the same time, so decreasing mental load is a blessing for it. Not mentioning that formatting and reformatting your code takes time.

And the worst is, that your favourite formatting style at the moment won't be that in the next year. Myself, I was in projects where the coding styles looken at first insane to me! And I arguend and ranted but complied to them for the greater (i.e. project's) good. An guess what, now I'm using elements of these coding styles in my own code! Ok, not everything, but some parts weren't so nutty at all. What does that mean? Yes, you guessed it: coding styles doen't matter at all. But switching between them does!

So why we just don't stop doing this? Why don't let wo the computer do this and concertrate on more important aspects oif code? There are so many of them! As I first read about Go's policy about code formatting I wasn't too enthusiastic about it. But meanwhile I find it a good idea: only one prescribed layout style automatically imposed on your source code! Let's forget about coding standards and concentrate on problem solving!