Template metaprogramming to auto-detect race conditions

[KishoreG]

I read a GitHub project description about using template metaprogramming to auto-detect race conditions, and I wanted to learn more about it and how it can be implemented. Could anyone point me in the right direction of how this is possible using C++ templates or give a small example?

[mbozzi]

I read a GitHub project description about using template metaprogramming to auto-detect race conditions

Can you link the project?

A meta-program is a program whose output is source code. In this case the meta-program is written in C++ and outputs C++, but the language in which the meta-program is written doesn't really matter.

There are at least two options:
a.) monitor the executing program and wait for a race to occur;
b.) analyze a controlled subset of the program's source code and prove that no races occur.

Option a is conceptually easy: it involves adding code into the system that detects race conditions. This is typically done with the C++ compiler's help (e.g., with Clang's ThreadSanitizer module), but at least in principle any capable metaprogram could do it too. The compiler (and ThreadSanitizer) is just a metaprogram that eats your source code and outputs it in another form.

Option b is conceptually harder: there are some rules which, if obeyed, guarantee the absence of race conditions. A metaprogram could be constructed to implement a language that makes race conditions impossible by definition.

For example,
- Robert Ramey's Safe Numerics is a template library which implements a compiler for a language which does arithmetic safely. If arithmetic is expressed using the library's language, it is guaranteed to either be free of integer overflow or to result in a compiler error.

- Hana Dusikova's compile time regular expression library (CTRE) is a template library which implements a compiler for the language of regular expressions. If a regular expression is written in the library's language, it is guaranteed to compile into a valid regular expression matcher, or to result in a compiler error.

- Boost Spirit is a (much older) template library which implements a parser generator - a compiler for the language of attribute grammars. If a grammar is written in the library's language, it is guaranteed to either compile to a working parser or to result in a compiler error.

Actually in the case of Spirit or CTRE, correctness isn't the primary focus, so there may be certain invalid sentences that type-check, but the nature of the implementation will probably disallow most of them. Ramey's library is the best example, it is designed specifically to prove the absence of a particular kind of error, exactly what the question is looking for. It is also the simplest internally.

[jonnin]

B does not seem like detection, but prevention. I don't see how, if you have code with a race condition, B would detect it (?). Are you saying that the code would fail to compile in the new language due to the RC and that would be your 'detection'?

[mbozzi]

B does not seem like detection, but prevention

Yes it's just prevention.

Although in my opinion prevention is more interesting. Nothing beats a guarantee that your code will never encounter a race condition.

Formal methods can help do this now, see TLA+ for example
https://lamport.azurewebsites.net/tla/tla.html

[jonnin]

that is a neat link, thx. I am going to have to go over that a few times.
I agree, prevention is better, but I was trying to fit the answer to the problem. The problem, by the way, sounds like (a subset of) one I was told is NP .. "can a program determine if another program will always execute correctly for any input".

[mbozzi]

I am going to have to go over that a few times.

Yeah it's pretty neat stuff, but a lot of it is over my head. This stuff is still so niche, I wish the entry barrier was a bit lower.

"Can a program determine if another program will always execute correctly for any input?"

The answer to that is "no":

For argument's sake, assume "will always execute correctly" means "never dereferences a null pointer". We can prove that we can't decide by modifying the program being analyzed:
- Step 1 is to change all the places where the program quits into infinite loops. So after step 1 the program will never quit.
- Step 2 is to add if (! pointer) quit(); before every dereference. So after step 2 the program quits if and only if it would dereference a null pointer.

So if we can decide about null pointers, we can also decide whether our program will eventually quit, or vice versa. This is called the "halting problem", it's the same question where "will execute correctly" means "will eventually quit".

Assume there's a program which solves the halting problem correctly, called h.exe. We can write another program called g.exe with this source code:

if h.exe says g.exe would eventually quit: enter an infinite loop; else quit.

Which highlights a contradiction because g.exe enters an infinite loop if h.exe claims g.exe eventually quits, or vice versa. Therefore a solution to the halting problem h.exe can't exist, and since the question about null pointers is equivalent, a solution to that can't exist either.

So this analysis is impossible, but a program that only answers correctly on some inputs, occasionally flags false positives, or sometimes says "I don't know" is still okay. For example, C++ has type casts (partly) to get around the type checker's false-positive rejection of correct code. My understanding is that the "subset of programs" thing is really helpful.