C11 Fails to Define Data Races Involving Interrupts

Users of our data-race detector for C/C++ programs, RV-Predict/C, frequently tell us at Runtime Verification, Inc., (RV) that they would like to see a variant that detects data races between threads and interrupts in embedded systems. A solitary application thread may share data locations with one or more interrupt service routines (ISRs). Data accesses by the ISRs and the application thread may conflict. The conflicting accesses can lead to unexpected behavior in safety-critical software. Users hope to detect conflicting accesses using runtime verification, and fix their software to avoid the conflicts.

What does it mean to have a “data race” between a thread and an interrupt? We quickly realized at RV that we resorted to a vague analogy between threads and interrupts to define a data race. It was important to produce a formal definition. We are concerned with interrupts only in C programs, so we sought an authoritative definition in the C11 standard. We were surprised when we could not find one!
Continue reading

“restrict” keyword in header files

It would appear that Mac OS X’s copy of string.h is invalid.

It declares strcpy as

char *strcpy(char *, const char *);

But the C standard declares it as

char *strcpy(char * restrict, const char * restrict);

These two types are actually incompatible with each other according to the C standard, and a function that is declared  more than once in different translation units with different declarations is considered undefined behavior. Thus, any correctly conforming C library will cause any code that includes string.h to be undefined.


Undefined C: Common mistakes

This blog post is the beginning of an intended series of blog posts detailing undefined and unspecified behavior in the ISO C standard, and its impact on development. To start with, we will summarize the domain and provide information about some of the undefined behaviors which we have found to be most widespread in production-deployed C code of the open source projects we have tested.

Continue reading