Objection! Undefined behavior!

The day-to-day life of a Solid Sands engineer working on our SuperGuard C/C++ standard library test suite looks vaguely like this:

• Take a class or group of functions from a library header.
• Consult the ISO standard for the language version(s) that introduced or amended the feature.
• Distill the semantic specifications into traceable requirements that can be individually tested.
• Write the tests.

This is the story of how I learned that this process is as much a lawyerly discipline as an engineering one.

Not too long after I started here, I thought things were going pretty well: I was getting to grips with the concept of functional safety, becoming familiar with our test framework, and receiving money in my bank account at regular intervals. Life was good.

As if on cue, fate decreed that I would be assigned to work on developing tests for the <mutex> header to supplement the 1.3 release of SuperGuard.

Now, it’s not that I expected this to be easy. I knew that conformance testing in a non-deterministic space was going to be a whole new paradigm. So I cracked open the C++11 standard and got reading. If developing the tests was likely to be somewhat onerous, at least writing the traceability requirements first would ease me into it.

Spoiler: it didn’t. What this task instead brought into sharp relief is the philosophy of the standard as a legal text, where precision is prioritized over readability; explication over implication; and everything over the happiness of test suite developers.

Consider, from C++11, the concept of mutex ownership, which the standard defines as extending “from the time [a thread] successfully calls one of the lock functions until it calls unlock”. One of these “lock functions” is…lock(), whose semantics are defined thus:

Requires: If [called on a non-recursive mutex], the calling thread does not own the mutex.

Effects: Blocks the calling thread until ownership of the mutex can be obtained for the calling thread.

Postcondition: The calling thread owns the mutex.

“Requires” is standard-ese for “violating this is undefined behavior”. So far, so intuitive: trying to acquire ownership of a mutex twice on the same thread is UB.

Unfortunately, just as laws comprise patches of amendments awkwardly sewn onto other patches, library features have a tendency to evolve between versions. Enter C++14, which splits the concept of ownership into exclusive (for read/write access) and shared (read-only), and introduces a shared_timed_mutex type which supports both. Now, suppose we have a shared_timed_mutex. We call lock_shared() on it to obtain shared ownership, and then immediately call lock(). Is that UB? The precondition doesn’t stipulate whether the prohibited ownership is exclusive or shared.

What’s that you say? Surely the addition of shared ownership in 14 would trigger a rewrite of the precondition to remove any ambiguity? That’s adorable. No, it stayed exactly the same.

At this point, anyone who wants a drama-free life has gone off to use Rust instead. So for the brave people who stuck around, let’s put on our lawyer’s wig and try to work out what the standard intends.

We know that in C++11, lock() conferred exclusive ownership, as no other kind existed. We also reason that for the function to suddenly change its behavior to confer shared ownership would wreak absolute havoc on existing code. And since it would seem insane for “own” to refer to one thing in the precondition and another in the postcondition, we assume that calling lock() in the described scenario is well-defined.

This is thinking like an engineer. Big mistake. The lawyer knows that insane things happen all the time, and does more digging. Eventually they find this, in the subsection on the shared_timed_mutex class itself:

The behavior of a program is undefined if:

• a thread attempts to recursively gain any ownership of a shared_timed_mutex.

Any ownership. Fitting all the pieces together, we get: the precondition forbids calling the function when the thread has exclusive or shared ownership, while “owns” in the postcondition refers only to exclusive ownership. That’s right, the concept of ownership has a different scope in each case!

Since my baptism in the fiery crucible of <mutex>, I’ve encountered this collision between engineering assumptions and the letter of the standard all over the place. Its prevalence is unrelated to the complexity of the feature under question, and is just as common in language features as in library ones. auto must be simple, right? Wrong. Or take explicitly typed enums. No, really, please take them.

Even where it seems obvious that a feature must work a certain way, our job is to search the statute…sorry, standard, for a justification. And once we find one, to dig into the fine print to make sure that justification isn’t contradicted anywhere. Because in the functional safety world as in the legal, due diligence is the enemy of assumption, and assumption is the mother of all disasters. I rest my case.