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!

In the C11 standard1, data races are conflicting actions between threads. Section 5.1.2.4 paragraph 25 says:

The execution of a program contains a data race if it contains two conflicting actions in different threads, at least one of which is not atomic, and neither happens before the other. Any such data race results in undefined behavior.

In the C standard, the closest thing to an ISR is an asynchronous signal handler. Nowhere does the standard speak of a data race between a asynchronous signal handler and the thread that it interrupts. Rather, the standard speaks of unspecified and undefined behavior by a signal handler. According to section 5.1.2.3 paragraph 5, the values of some objects are unspecified in a signal handler, other values are undefined, and with certain exceptions, modifying objects is undefined:

When the processing of the abstract machine is interrupted by receipt of a signal, the values of objects that are neither lock-free atomic objects nor of type volatile sig_atomic_t are unspecified, and the value of any object that is modified by the handler that is neither a lock-free atomic object nor of type volatile sig_atomic_t becomes undefined.

Curiously, the standard repeats itself about unspecified/undefined behavior in signal handlers, in section 7.14.1.1 paragraph 5, adding some qualifications about storage duration:

If the signal occurs other than as the result of calling the abort or raise function, the behavior is undefined if the signal handler refers to any object with static or thread storage duration that is not a lock-free atomic object other than by assigning a value to an object declared as volatile sig_atomic_t, or …

The storage-duration qualification is perplexing. If referring to objects of static or thread storage duration in a signal handler is undefined, then surely referring to objects of allocated storage or to objects of automatic storage (other than the handler’s own automatic storage), is undefined, too. §7.14.1.1 ¶ 5 probably just contains a typo.

Since the C11 standard provides no definition for data races between threads and interrupts, RV has let common sense and user needs guide us. Users are concerned with detecting accesses by both an interrupt and a thread when those accesses are both conflicting and asynchronous. Accesses by a thread and an interrupt conflict if both refer to the same object, and one access modifies the object. Every access by an interrupt is synchronous with respect to an access by a thread only if the interruption happens before the thread access, or the thread access happens before the interruption. Otherwise, the interrupt’s accesses are asynchronous. When we speak of a “data race” involving an interrupt, we mean just these asynchronous, conflicting accesses. Figure 1 shows a signal handler that aborts the program if a shared variable, shared.count, exceeds 25. The signal handler is established on the alarm signal, SIGALRM. Figure 2 is a fragment of code that shows how a conflicting access to the shared variable can be synchronized with signals:

	static struct {
		volatile int count;
	} shared = {
		  .count = ATOMIC_VAR_INIT(false)
	};

	static void
	alarm_handler(int signum __unused)
	{
		if (shared.count > 25)
			abort();
	}

Figure 1: alarm_handler shares a global variable with the application

	sigset_t blockingset, oldset;

	sigemptyset(&blockingset);
	sigaddset(&blockingset, SIGALRM);

	// save signal mask; block SIGALRM
	pthread_sigmask(SIG_BLOCK, &blockingset, &oldset);

	// modify shared variable
	shared.count++;

	// restore signal mask
	pthread_sigmask(SIG_SETMASK, &oldset, NULL);

Figure 2: synchronizing access between a thread and a signal

In recent work on RV-Predict/C, we have added new instrumentation and enhanced our causal model so that we can detect when programs that use interrupts or UNIX signals contain data races, according to our definition, above. In a future blog post, we will tell you more about this new development.

Notes

  1. Throughout this post I refer to the N1548 Committee Draft — December 2, 2010 ISO/IEC 9899:201x.

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

Experienced C Developers Can Still Misunderstand Simple Language Concepts

Not long ago, one of our customers came to us confused about an analysis report on a simple program their company used internally to assess knowledge of C. Among the code they sent us was something like the following three lines:

int32_t var = 0xffeeddcc;
int32_t var2 = 0x7f000000;
var2 <<= 8;

They assumed that this code should be free from defects, and thought that possibly the two defects we reported were incorrect. Let’s take a look at the error reports that result when we insert these lines into a simple program and execute them:
Continue reading

K Developer Interviewed in Illinois Paper

A local paper, the News-Gazette interviewed Cosmin Radoi. He has contributed to the K framework for  several years while studying at UIUC with Grigore Rosu. Cosmin’s latest project Kale uses the rewriting approach of the K framework to suggest program transformations and improvements, instead of using it to examine how programs execute according to a formal language semantics, as in RV-Match and much of the academic work with K. We wish Cosmin well in his own efforts to provide powerful software development tools.

wired_in_radoi

ASE 2001 paper that helped shape the Runtime Verification field got the Most Influential Paper Award

Klaus Havelund and I got the ASE 2016 most influential paper award for a paper we published 15 years ago, in ASE 2001.  That paper is important to me because it turned my interest to the field that we now call “runtime verification” (back then, we didn’t know exactly what it was).  Below is a link to an article that the CS Department at UIUC just published about this award.

 

capture
CS article

 

 

14% of SV-COMP’s “Correct Programs” are Undefined!

Capture

Last April (2016), I gave a tutorial on K at ETAPS’16 in Eindhoven, Netherlands, where I also demonstrated RV-Match.  During the week that I spent there, I heard several friends and colleagues who were involved with the Competition on Software Verification, SV-COMP, that some of the benchmark’s correct programs appear to be undefined.  What?  So some of the assumed-correct C programs that are used to evaluate the best program verifiers in the world are actually wrong programs? Continue reading

Runtime Verification seeking a Software Development Engineer

Runtime Verification, Inc is looking for a software engineer 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

RV Inc. to Give Tutorial at Runtime Verification ’16 Conference

Runtime Verification Inc. is going to be presenting an exciting tutorial at the RV’16 conference, featuring all of our current tools and technologies and their practical and creative uses and applications.

If you are new (or a veteran) to runtime verification technology, we invite you to join and learn about what RV Inc.’s tools can do for your codebase, today. We look forward to seeing you in sunny, beautiful Madrid!

2016-05-25--1464206820_1518x728_scrot