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

Runtime Verification seeking a Senior Verification Engineer and a Full Stack Software Engineer

Runtime Verification, Inc is looking for two new software engineers to work on our family of products. We are a start-up based in Urbana, Illinois, less than 15 walk minutes away from the Computer Science Department at the University of Illinois in Urbana-Champaign (UIUC), which is in the top 5 schools in Computer Science in the United States and the top 1-2 schools in the domains of software engineering, formal methods and programming languages. Continue reading