Data Races and Static Analysis for InterruptDriven Kernels
Abstract
We consider a class of interruptdriven programs that model the kernel API libraries of some popular realtime embedded operating systems and the synchronization mechanisms they use. We define a natural notion of data races and a happensbefore ordering for such programs. The key insight is the notion of disjoint blocks to define the synchronizeswith relation. This notion also suggests an efficient and effective lockset based analysis for race detection. It also enables us to define efficient “syncCFG” based static analyses for such programs, which exploit data race freedom. We use this theory to carry out static analysis on the FreeRTOS kernel library to detect races and to infer simple relational invariants on key kernel variables and datastructures.
Keywords
Static analysis Interruptdriven programs Data races1 Introduction
Embedded software is widespread and increasingly employed in safetycritical applications in medical, automobile, and aerospace domains. These programs are typically multithreaded applications, running on uniprocessor systems, that are compiled along with a kernel library that provides prioritybased scheduling, and other task management and communication functionality. The applications themselves are similar to classical multithreaded programs (using lock, semaphore, or queue based synchronization) although they are distinguished by their prioritybased execution semantics. The kernel on the other hand typically makes use of nonstandard lowlevel synchronization mechanisms (like disablingenabling interrupts, suspending the scheduler, and flagbased synchronization) to ensure threadsafe access to its datastructures. In the literature such software (both applications and kernels) are referred to as interruptdriven programs. Our interest in this paper is in the subclass of interruptdriven programs corresponding to kernel libraries.
Efficient static analysis of concurrent programs is a challenging problem. One could carry out a precise analysis by considering the product of the control flow graphs (CFGs) of the threads, however this is prohibitively expensive due to the exponential number of program points in the product graph. A promising direction is to focus on the subclass of racefree programs. This is an important class of programs, as most developers aim to write racefree code, and one could try to exploit this property to give an efficient way of analyzing programs that fall in this class. In recent years there have been many techniques [7, 11, 12, 18, 21] that exploit the racefreedom property to perform sound and efficient static analysis. In particular [11, 21] create an appealing structure called a “syncCFG” which is the union of the control flow graphs of the threads augmented with possible “synchronization” edges, and essentially perform sequential analysis on this graph to obtain sound facts about the concurrent program. However these techniques are all for classical lockbased concurrent programs. A natural question asks if we can analyze interruptdriven programs in a similar way.
There are several challenges in doing this. Firstly one needs to define what constitutes a data race in a generalized setting that includes these programs. Secondly, how does one define the happensbefore order, and in particular the synchronizeswith relation that many of the racefree analysis techniques rely on, given the adhoc synchronization mechanisms used in these programs.
A natural route that suggests itself is to translate a given interruptdriven program into one that uses classical locks, and faithfully captures the interleaved executions of the original program. One could then use existing techniques for lockbased concurrency to analyze these programs. However, this route is fraught with many challenges. To begin with, it is not clear how one would handle flagbased synchronization which is one of the main synchronization mechanisms used in these programs. Even if one could handle this, such a translation may not preserve data races, in that the original program might have had a race but the translated program does not. Finally, some of the synchronizeswith edges in the translated program are clearly unnecessary, leading to imprecise dataflow facts in the analyses.
In this paper, we show that it is possible to take a more organic route and address these challenges in a principled way that could apply to other nonstandard classes of concurrent systems as well. Firstly, we propose a general definition of a data race that is not based on a happensbefore order, but on the operational semantics of the class of programs under consideration. The definition essentially says that two statements s and t can race, if two notional “blocks” around them can overlap in time during an execution. We believe that this definition accurately captures what it is that a programmer tries to avoid while dealing with shared variables whose values matter. Secondly we propose a way of defining the synchronizeswith relation, based on the notion of disjoint blocks. These are statically identifiable pairs of path segments in the CFGs of different threads that are guaranteed to never overlap (in time) during an execution of the program, much like blocks of code that lie between an acquire and release of the same lock. This relation now suggests a natural syncCFG structure on which we can perform analyses like valueset (including interval, nulldeference, and pointsto analysis), and regionbased relational invariant analysis, in a sound and efficient manner. We also use the notion of disjoint blocks to define an efficient and precise locksetbased analysis for detecting races in interruptdriven programs.
We implement some of these analyses on the FreeRTOS kernel library [3] which is one of the most widely used opensource realtime kernels for embedded systems, comprising about 3,500 lines of C code. Our racedetection analysis reports a total of 64 races in kernel methods, of which 18 turn out to be true positives. We also carry out a regionbased relational analysis using an implementation based on CIL [22]/Apron [15], to prove several relational invariants on the kernel variables and abstracted datastructures.
2 Overview
Our first contribution is a general notion of data races which is applicable to such programs. We say that two conflicting statements s and t in two different threads are involved in a data race if assuming s and t were enclosed in a notional “block” of skip statements, there is an execution in which the two blocks “overlap” in time. The given program can be seen to be free of races. However if we were to remove the disableint statement of line 10, then the statements accessing msgw in lines 12 and 42 would be racy, since soon after the access of msgw in qsend at line 12, there could be preemption by qrec_ISR which goes on to execute line 42.
Next we illustrate the notion of “disjoint blocks” which is the key to defining synchronizeswith edges, which we need in our syncCFG analysis as well as to define an appropriate happensbefore relation. Disjoint blocks are also used in our racedetection algorithm. A pair of blocks of code (for example any of the likeshaded blocks of code in the figure) are disjoint if they can never overlap during an execution. For example, the block comprising lines 11–14 in qsend and the whole of qrec_ISR, form a pair of disjoint blocks.
Next we give an analysis for checking racefreedom, by adapting the standard lockset analysis [24] for classical concurrent programs. We associate a unique lock with each pair of disjoint blocks, and add notional acquires and releases of this lock at the beginning and end (respectively) of these blocks. We now do the standard lockset analysis on this version of the program, and declare two accesses to be nonracy if they hold sets of locks with a nonempty intersection.
Finally, we show how to do dataflow analysis for such programs in a sound and efficient way. The basic idea is to construct a “syncCFG” for the program by unioning the controlflow graphs of the threads, and adding sync edges that capture the synchronizeswith edges (going from the end of a block to the beginning of its paired block), for example line 14 to line 41 and line 49 to line 11. The syncedges are shown by dashed arrows in the figure. We now do a standard “valueset” analysis (for example interval analysis) on this graph, keeping track of a set of values each variable can take. The resulting facts about a variable are guaranteed to be sound at points where the variable is accessed (or even “owned” in the sense that a notional read of the variable at that point is nonracy). For example an interval analysis on this program would give us that \(0 < \mathtt {msgw}\) at line 14. Finally, we could do a regionbased valueset analysis, by identifying regions of variables that are accessed as a unit – for example msgw and len could be in one region, while wtosend and wtorec could be in another. The figure shows some facts inferred by a polyhedral analysis based on these regions, for the given program.
3 InterruptDriven Programs
The programs we consider have a finite number of (static) threads, with a designated “main” thread in which execution begins. The threads access a set of shared global variables, some of which are used as “synchronization flags”, using a standard set of commands like assignment statements of the form x := e, conditional statements (ifthenelse), loop statements (while), etc. In addition, the threads can use commands like disableint, enableint (to disable and enable interrupts, respectively), suspendsch, resumesch (to suspend and resume the scheduler, respectively), while the main thread can also create a thread (enable it for execution). Table 1 shows the set of basic statements \( cmd _{V,T}\) over a set of variables \(V\) and a set of threads \(T\).
We allow standard integer and Boolean expressions over a set of variables \(V\). For an integer expression e over \(V\), and an environment \(\phi \) for \(V\), we denote by Open image in new window the integer value that e evaluates to in \(\phi \). Similarly for a Boolean expression b, we denote the Boolean value (\( true \) or \( false \)) that b evaluates to in \(\phi \) by Open image in new window . For a set of environments \(\varPhi \) for a set of variables V, we define the set of integer values that e can evaluate to in an environment in \(\varPhi \), by Open image in new window . Similarly, for a boolean expression b, we define the set of environments in \(\varPhi \) that satisfy b to be Open image in new window .
Each thread is of one of two types: “task” threads that are like standard threads, and “ISR” threads that represent threads that run as interrupt service routines. The main thread is a task thread, which is the only task thread enabled initially. The main thread can enable other threads (both task and ISR) for execution using the create command. Task threads can be preempted by other task threads (whenever interrupts are not disabled, and the scheduler is not suspended) or by ISR threads (whenever interrupts are not disabled). On the other hand ISR threads cannot be preempted and are assumed to run to completion.
Basic statements \( cmd _{V, T}\) over variables \(V\) and threads \(T\)
Command  Description 

skip  Do nothing 
x := e  Assign the value of expression e to variable \(x \in V\) 
\(\mathtt {assume(}b\mathtt {)}\)  Enabled only if expression b evaluates to \( true \), acts like skip 
create(t)  Enable thread \(t \in T\) for execution 
disableint  Disable interrupts and context switches 
enableint  Enable interrupts and context switches 
suspendsch  Suspend the scheduler (other task threads cannot preempt the current thread); Also sets \(\mathtt {ssflag}\) variable 
resumesch  Resume the scheduler (other task threads can now preempt the current thread); Also unsets \(\mathtt {ssflag}\) variable 
Formally we represent an interruptdriven program P as a tuple \((V,T)\) where \(V\) is a finite set of integer variables, and \(T\) is a finite set of named threads. Each thread \(t \in T\) has a type which is one of task or ISR, and an associated controlflow graph of the form \(G_t = (L_t, s _t, inst _t)\) where \(L_t\) is a finite set of locations of thread t, \( s _t \in L_t\) is the start location of thread t, \( inst _t \subseteq L_t \times cmd _{V,T} \times L_t\) is a finite set of instructions of thread t.
Some definitions related to threads will be useful going forward. We denote by \(L_P = \bigcup _{t \in T}L_t\) the disjoint union of the thread locations. Whenever P is clear from the context we will drop the subscript of P from \(L_P\) and its decorations. For a location \( l \in L\) we denote by \( tid ( l )\) the thread t which contains location \( l \). We denote the set of instructions of P by \( inst _P = \bigcup _{t\in T} inst _t\). For an instruction \(\iota \in inst _t\), we will also write \( tid (\iota )\) to mean the thread t. For an instruction \(\iota = \langle l ,c, l ' \rangle \), we call \( l \) the source location, and \( l '\) the target location of \(\iota \).

Q is a set of states of the form \(( pc , \phi , enab , rt, it, id , ss )\), where \( pc \in T\rightarrow L\) is the program counter giving the current location of each thread, \(\phi \in V\rightarrow \mathbb {Z}\) is a valuation for the variables, \( enab \subseteq T\) is the set of enabled threads, \(rt\in T\) is the currently running thread; \(it\in T\) is the task thread which is interrupted when the scheduler is suspended; and \( id \) and \( ss \) are Boolean values telling us whether interrupts are disabled (\( id = true \)) or not (\( id = false \)) and whether the scheduler is suspended (\( ss = true \)) or not (\( ss = false \)).

The set of labels \(\varSigma \) is the set of instructions \( inst _P\) of P.

The initial state s is \((\lambda t. s _t, \lambda x.0, \{ main \}, main , main , false , false )\). Thus all threads are at their entry locations, the initial environment sets all variables to 0, only the main thread is enabled and running, the interrupted task is set to \( main \) (this is a dummy value as it is used only when the scheduler is suspended), interrupts are enabled, and the scheduler is not suspended.
 For an instruction \(\iota = \langle l ,c, l ' \rangle \) in \( inst _P\), with \( tid (\iota ) = t\), we defineiff the following conditions are satisfied:$$ ( pc , \phi , enab , rt, it, id , ss ) \Rightarrow _{\iota } ( pc ', \phi ', enab ', rt', it', id ', ss ') $$

\(t \in enab \); \( pc (t) = l \); \( pc ' = pc [t\mapsto l ']\);

if \( id \) is true or \(rt\) is an ISR then \(t = rt\);

if \( ss \) is true, then either \(t = rt\) or t is an ISR thread;
 Based on the command c, the following conditions must be satisfied:

\(*\) If c is the skip command then \(\phi ' = \phi \), \( enab ' = enab \), \( id ' = id \), and \( ss ' = ss \).

\(*\) If c is an assignment statement of the form \(x := e\) then Open image in new window , \( enab ' = enab \), \( id ' = id \), and \( ss ' = ss \).

\(*\) If c is a command of the form \(\mathtt {assume(}b\mathtt {)}\) then Open image in new window , \(\phi ' = \phi \), \( enab ' = enab \), \( id ' = id \), and \( ss ' = ss \).

\(*\) If c is a \(\texttt {create}(u)\) command then \(t = main \), \(\phi ' = \phi \), \( enab ' = enab \cup \{u\}\), \( id ' = id \), and \( ss ' = ss \).

\(*\) If c is the \(\texttt {disableint}\) command then \(\phi ' = \phi \), \( enab ' = enab \), \( id ' = true \), and \( ss ' = ss \).

\(*\) If c is the \(\texttt {enableint}\) command then \(\phi ' = \phi \), \( enab ' = enab \), \( id ' = false \), and \( ss ' = ss \).

\(*\) If c is the \(\texttt {suspendsch}\) command then \(\phi ' = \phi [ssflag\mapsto 1]\), \( enab ' = enab \), \( id ' = id \), and \( ss ' = true \).

\(*\) If c is the \(\texttt {resumesch}\) command then \(\phi ' = \phi [ssflag\mapsto 0]\), \( enab ' = enab \), \( id ' = id \), and \( ss ' = false \).


In addition, the transitions set the new running thread \(rt'\) and interrupted task \(it'\) as follows. If t is an ISR thread, \( ss \) is true, and \(\iota \) is the first statement of t then \(it' = rt\), \(rt' = t\). If t is an ISR thread, \( ss \) is true, and \(\iota \) is the last statement of t then \(it' = it\), \(rt' = it\). In all other cases, \(rt' = t\) and \(it' = it\).

An execution \(\sigma \) of P is a finite sequence of transitions in \(\mathcal {T}_P\) from the initial state s: \(\sigma = \tau _0,\tau _1,\ldots ,\tau _n\) (\(n \ge 0\)) from \(\Rightarrow _{}\), such that there exists a sequence of states \(q_0, q_1, \ldots , q_{n+1}\) from Q, with \(q_0 = s\) and \(\tau _i = (q_i,\iota _i,q_{i+1})\) for each \(0 \le i \le n\). Wherever convenient we will also represent an execution like \(\sigma \) above as a sequence of the form \( q_0 \Rightarrow _{\iota _0} q_1 \Rightarrow _{\iota _1} \cdots \Rightarrow _{\iota _n} q_{n+1}. \) We say that a state \(q \in Q\) is reachable in program P if there is an execution of P leading to state q.
4 Data Races and HappensBefore Ordering
In this section we propose a definition of a data race which has general applicability, and also define a natural happensbefore order for interruptdriven programs.
4.1 Data Races
Data races have typically been defined in the literature in terms of a happensbefore order on program executions. In the classical setting of lockbased synchronization, the happensbefore relation is a partial order on the instructions in an execution, that is reflexivetransitive closure of the union of the programorder relation between two instructions in the same thread, and the synchronizeswith relation which relates a release of a lock in a thread to the next acquire of the same lock in another thread. Two instructions in an execution are then defined to be involved in a data race if they are conflicting accesses to a shared variable and are not ordered by the happensbefore relation.
We feel it is important to have a definition of a data race that is based on the operational semantics of the class of programs we are interested in, and not on a happensbefore relation. Such a definition would more tangibly capture what it is that a programmer typically tries to avoid when dealing with shared variables whose consistency she is worried about. Moreover, when coming up with a definition of the happensbefore order (the synchronizeswith relation in particular) for nonstandard concurrent programs like interruptdriven programs, it is useful to have a reference notion to relate to. For instance, one could show that a proposed happensbefore order is strong enough to ensure the absence of races.
The rationale for this definition is that the concerned statements s and t may be compiled down to a sequence of instructions (represented by the blocks with skip’s around s and t) depending on the underlying processor and compiler, and if these instructions interleave in an execution, it may lead to undesirable results.
To illustrate the definition, consider the program in Fig. 2a. The accesses to x in line 7 and line 11 can be seen to be racy, since there is an execution of the augmented program \(P'\) in which \( t1 \) performs the skip followed by the increment to x at line 7, followed by a context switch to thread \( t2 \) which goes on to execute lines 9 and 10 and then the read of x in line 11. On the other hand, the version of the program in which line 7 is enclosed in a disableintenableint block, does not contain a race.
We note that for classical concurrent programs, it might suffice to define a race as consecutive occurrences of conflicting accesses in an execution, as done in [4, 17]. However, this definition is not general enough to apply to interruptdriven programs. By this definition, the statements in lines 7 and 11 of the program in Fig. 2a are not racy, as there is no execution in which they happen consecutively. This is because the disableintenableint block containing the access in line 11 is “atomic” in that the statements in the block must happen contiguously in any execution, and hence the instructions corresponding to line 7 and line 11 can never happen immediately one after another.
4.2 Disjoint Blocks and the HappensBefore Relation
Now that we have a proposed definition of races, we can proceed to give a principled way to define the happensbefore relation for our class of interruptdriven programs. The main question is how does one define the synchronizeswith relation. Our insight here is that the key to defining the synchronizeswith relation lies in identifying what we call disjoint blocks for the class of programs. Disjoint blocks are statically identifiable pairs of path segments in the CFGs of different threads, which are guaranteed by the execution semantics of the class of programs never to overlap in an execution of the program. Disjoint block structures – for example in the form of blocks enclosed between locks/unlocks of the same lock – are the primary mechanism used by developers to ensure racefreedom. The synchronizeswith relation in an execution can then be defined as relating, for every pair (A, B) of disjoint blocks in the program, the end of block A to the beginning of the succeeding occurrence of block B in the execution. The happensbefore order for an execution can now be defined, as before, in terms of the program order and the synchronizeswith order, and is easily seen to be sufficient to ensure nonraciness.
We now focus on defining a happensbefore relation based on disjoint blocks for our class of interruptdriven programs. We have identified eight pairs of disjoint block patterns for this class of programs, which are depicted in Fig. 4. We use the following types of blocks to define the pairs. A block of type D is a path segment in a task thread that begins with a disableint and ends with an enableint with no intervening enableint in between. A block of type S is a path segment in a task thread that begins with a suspendsch and ends with a resumesch with no intervening resumesch. An I block is an initial and terminating path segment in an ISR thread (i.e. begins with the first instruction and ends with a terminating instruction). Similarly, for a task thread t, \(T_t\) is an initial and terminating path in t, while \(M_t\) is an initial segment of the main thread that ends with a \(\texttt {create}(t)\) command. A block of type \(C_{ssflag}\) is a path segment in an ISR thread corresponding to the then block of a conditional that checks if \(ssflag = 0\). For a synchronization flag f, \(C_f\) is the path segment in an ISR thread corresponding to the then block of a conditional that checks if \(f = 0\). Finally \(F_f\) is a segment between statements that set f to 1 and back to 0, in a task thread. We also require that an \(F_f\) segment be within the scope of a suspendsch command.
We can now describe the pairs of disjoint blocks depicted in Fig. 4. Case (a) says that two D blocks in different task threads are disjoint. Clearly two such blocks can never overlap in an execution, since once one of the blocks begins execution no contextswitch can occur until interrupts are enabled again. Case (b) says that D and I blocks are disjoint. Once again this is because once the D block begins execution no ISR can run until interrupts are enabled again, and once an ISR begins execution it runs to completion without any contextswitches. Case (e) says that S blocks in different task threads are disjoint, because once the scheduler is suspended no contextswitch to another task thread can occur. Case (f) says that \(M_t\) and \(T_t\) blocks are disjoint, since a thread cannot begin execution before it is created in main. Case (g) says that an S block is disjoint from a \(C_{\mathtt {ssflag}}\) block. This is because once the scheduler is suspended by the suspendsch command, and even if a contextswitch to an ISR occurs, the then block of the if statement will not execute. Conversely, if the ISR is running there can be no contextswitch to another thread. Finally, case (h) is similar to case (g). We note that the disjoint block pairs are not ordered (the relation is symmetric).
We can now define the synchronizeswith relation as follows. Let \(\sigma = q_0 \Rightarrow _{\iota _0} q_1 \Rightarrow _{\iota _1} \cdots \Rightarrow _{\iota _n} q_{n+1}\) be an execution of P. We say instruction \(\iota _i\) synchronizeswith an instruction \(\iota _j\) of P in \(\sigma \), if \(i < j\), \( tid (\iota _i) \ne tid (\iota _j)\), and there exists a pair of disjoint blocks A and B, with \(\iota _i\) ending block A and \(\iota _j\) beginning block B. As usual we say \(\iota _i\) is programorder related to \(\iota _j\) iff \(i < j\) and \( tid (\iota _i) = tid (\iota _j)\). We define the happensbefore relation on \(\sigma \) as the reflexivetransitive closure of the union of the programorder and synchronizeswith relations for \(\sigma \).
We can now define a HBrace in an execution \(\sigma \) of P as follows: we say that two instructions \(\iota _i\) and \(\iota _j\) in \(\sigma \) are involved in a HBrace if they are conflicting instructions that are not ordered by the happensbefore relation in \(\sigma \). We say that two instructions in P are HBracy if there is an execution of P in which they are involved in a HBrace. Finally, we say a program P is HBracefree if no two of its instructions are HBracy.
Once again, it is fairly immediate to see that if two statements of a program are not involved in a HBrace, they cannot be involved in a race. Further, if two statements belong to disjoint blocks, then they are clearly happensbefore ordered in every execution. Hence belonging to disjoint blocks is sufficient to ensure that the statements are happensbefore ordered, which in turn ensures that the statements cannot be involved in a race.
5 SyncCFG Analysis for InterruptDriven Programs
In this section we describe a way of lifting a sequential valueset analysis in a sound way for a HBrace free interruptdriven program, in a similar way to how it is done for lockbased concurrent programs in [11]. A valueset analysis keeps track of the set of values each variable can take at each program point. The basic idea is to create a “syncCFG” for a given interruptdriven program P, which is essentially the union of the CFGs of each thread of P, along with “maysynchronizewith” edges between statements that may be synchronizeswith related in an execution of P, and then perform the valueset analysis on the resulting graph. Whenever the given program is HBrace free, the result of the analysis is guaranteed to be sound, in a sense made clear in Theorem 1.
5.1 SyncCFG
We begin by defining the “syncCFG” for an interruptdriven program. It is on this structure that we will do the valueset analysis. Let \(P=(V,T)\) be an interruptdriven program, and let G be the disjoint union (over threads \(t \in T\)) of the CFGs \(G_t\). We define a set of maysynchronizewith edges in G, denoted \( MSW (G)\), as follows. The edges correspond to the pairs of disjoint blocks depicted in Fig. 4, in that they connect the ending of one block to the beginning of the other block in the pair. Consider two instructions \(\iota = \langle l ,c,m \rangle \in inst _t\) and \(\kappa = \langle l ',c',m' \rangle \in inst _{t'}\), with \(t \ne t'\). We add the edge \((m, l ')\) in \( MSW (G)\), iff for some pair of disjoint blocks (A, B), \(\iota \) ends a block of type A in thread t and \(\kappa \) begins a block of type B in thread \(t'\). For example, corresponding to a (D, D) pair of disjoint blocks, we add the edge \((m, l ')\) when c is an enableint command, and \(c'\) is a disableint command.
The syncCFG induced by P is the control flow graph given by G along with the additional edges in \( MSW \)(G). Figure 6 shows a program \(P_2\) and its induced syncCFG.
5.2 Value Set Analysis
We first spell out the particular form of abstract interpretation we will be using. It is similar to the standard formulation of [9], except that it is a little more general to accommodate nonstandard controlflow graphs like the syncCFG.

D is the set of abstract states.

\((D, \le )\) forms a complete lattice. We denote the join (least upper bound) in this lattice by \(\sqcup _{\le }\), or simply \(\sqcup \) when the ordering is clear from the context.

\(d_0 \in D\) is the initial abstract state.

\(F : inst _P \rightarrow (D \rightarrow D)\) associates a transfer function \(F(\iota )\) (or simply \(F_\iota \)) with each instruction \(\iota \) of P. We require each transfer function \(F_{\iota }\) to be monotonic, in that whenever \(d \le d'\) we have \(F_{\iota }(d) \le F_\iota (d')\).
An abstract interpretation \(\mathcal {A}= (D, \le , d_0, F)\) of P induces a “global” transfer function \(\mathcal {F}_\mathcal {A}: D \rightarrow D\), given by \( \mathcal {F}_{\mathcal {A}}(d) = d_0 \sqcup \bigsqcup _{\iota \in inst _P} F_\iota (d). \) This transfer function can also be seen to be monotonic. By the KnasterTarski theorem [28], \(\mathcal {F}_\mathcal {A}\) has a least fixed point (\( LFP \)) in D, which we denote by \( LFP (\mathcal {F}_\mathcal {A})\), and refer to as the resulting value of the analysis.
A value set for a set of variables \(V\) is a map \( vs : V\rightarrow 2^{\mathbb {Z}}\), associating a set of integer values with each variable in \(V\). A value set \( vs \) induces a set of environments \(\varPhi _{ vs }\) in a natural way: \(\varPhi _{ vs } = \{ \phi \  \ \mathrm {for \ all\ } x \in V,\ \phi (x) \in vs (x) \}\) (i.e. essentially the Cartesian product of the values sets). Conversely, a set of environments \(\varPhi \) for \(V\), induces a value set \( valset (\varPhi )\) given by \( valset (\varPhi )(x) = \{ v \in \mathbb {Z}\  \ \exists \phi \in \varPhi ,\ \phi (x) = v \}\), which is the “projection” of the environments to each variable \(x \in V\). Finally, we define a pointwise ordering on value sets as follows: \( vs \preceq vs '\) iff \( vs (x) \subseteq vs '(x)\) for each variable x in \(V\). We denote the least element in this ordering by \( vs _{\bot } = \lambda x. \emptyset \).

D is the set \(L_P \rightarrow (V \rightarrow 2^\mathbb {Z})\) (thus an element of D associates a valueset with each program location)

The ordering \(d \le d'\) holds iff \(d(l) \preceq d'(l)\) for each \(l \in L_P\)
 The initial abstract value \(d_0\) is given by:

The transfer functions are given as follows. Given an abstract value d, and a location \(l \in L_P\), we define \( vs _l^d\) to be the join of the valueset at l, and the valueset at all maysynchronizeswith edges coming into l. Thus \( vs _l^d = d(l) \sqcup _{\preceq } \bigsqcup _{(n,l) \in MSW (G)} d(n)\). Below we will use \(\varPhi \) as an abbreviation of the set \(\varPhi _{ vs _l^d}\) of environments induced by \( vs _l^d\). Let \(\iota = \langle l ,c, l ' \rangle \) be an instruction in P.
 If c is the command \(\mathtt {assume(}b\mathtt {)}\), then \(F_\iota (d) = d'\) where
 If c is any other command (skip, disableint, enableint, suspendsch, resumesch, or create) then \(F_\iota (d) = d'\) where
Figure 6 shows the results of a valueset analysis on the syncCFG of program \(P_2\). The dataflow facts are shown just before a statement, at selected points in the program.
Soundness. The valueset analysis is sound in the following sense: if P is a HBrace free program, and we have a reachable state of P at a location l in a thread where a variable x is read; then the value of x in this state is contained in the valueset for x, obtained by the analysis at point l. More formally:
Theorem 1
Let \(P=(V,T)\) be an HBrace free interruptdriven program, and let \(d^*\) be the result of the analysis \(\mathcal {A}_{ vset }\) on P. Let l be a location in a thread \(t \in T\) where a variable x is read (i.e. P contains an instruction of the form \(\langle l ,c, l ' \rangle \) where c is a read access of x). Let \(\phi \) be an environment at l reachable via some execution of P. Then \(\phi (x) \in d^*(l)(x)\).
The proof of this theorem is similar to the one for classical concurrent programs in [11] (see [10] for a more accurate proof). The soundness claim can be extended to locations where a variable is “owned” (which includes locations where it is read). We say a variable x is owned by a thread t at location l, if an inserted read of x at this point is nonHBracy in the resulting program.
RegionBased Analysis. One problem with the valueset analysis is that it may not be able to prove relational invariants (like \(x \le y\)) for a program. One way to remedy this is to exploit the fact that concurrent programs often ensure racefree access to a region of variables, and to essentially do a regionbased valueset analysis, as originally done in [21]. More precisely, let us say we have a partition of the set of variables \(V\) of a program P into a set of regions \(R_1, \ldots , R_n\). We classify each read (write) access to a variable x in a region R, as an read (write) access to region R. We say that two instructions in an execution of P are involved in a HBregionrace, if the two instructions are conflicting accesses to the same region R, and are not happensbefore ordered in the execution. A program is HBregionrace free if none of its executions contain a HBregionrace.
We can now define a regionbased version of the valueset analysis for a program P, which we call \(\mathcal {A}_{ rvset }\). The valueset for a region R is a set of valuations (or subenvironments) for the variables in R. The transfer functions are defined in an analogous way to the valueset analysis. The analogue of Theorem 1 for regions gives us that for a HBregionrace free program, at any location where a region R is accessed, the regionvalueset computed by the analysis at that point will contain every subenvironment of R reachable at that point.
6 Translation to Classical LockBased Programs
In this section we address the question of why an executionpreserving translation to a classical lockbased program is not a fruitful route to take. In a nutshell, such a translation would not preserve races and would induce a syncCFG with many unnecessary MSW edges, leading to much more imprecise facts than the analysis on the native syncCFG described in the previous section. We also describe how our approach can be viewed as a lightweight translation of an interruptdriven program to a classical lockbased one. The translation is “lightweight” in the sense that it does not attempt to preserve the execution semantics of the given interruptdriven program, but instead preserves races and the syncCFG structure of the original program.
6.1 ExecutionPreserving Lock Translation
One could try to translate a given interruptdriven program P into a classical lockbased program \(P^L\) in a way that preserves the interleaved execution semantics of P. By this we mean that every execution of P has a corresponding execution in \(P^L\) that follows essentially the same sequence of interleaved instructions from the different threads (modulo of course the synchronization statements which may differ); and viceversa. For example, to capture the semantics of disableintenableint, one could introduce an “execution” lock E which is acquired in place of disabling interrupts, and released in place of enabling interrupts. Every instruction in a task thread outside a disableintenableint block must also acquire and release E immediately before and after the instruction. Note that the latter step is necessary if we want to capture the fact that once a thread disables interrupts it cannot be preempted by any thread. Figure 5a shows an interruptdriven program \(P_1\) and its lock translation \(P^L_1\) in Fig. 5b. There are still issues with the translation related to reentrancy of locks and it is not immediately clear how one would handle flagbased synchronization – but let us keep this aside for now.
The second problem with a precise lock translation is that the syncCFG of the translated program has many unnecessary MSWedges, leading to imprecision in the ensuing analysis. Consider the program \(P_2\) in Fig. 6, and its lock translation \(P_2^L\) in Fig. 7. \(P_2\) is similar to \(P_1\) except that line 4 is now an increment of y instead of x, and the resulting program is racefree (in fact HBracefree). Notice that the maysyncwith edges from line 13 to 4, and line 6 to 10 in the syncCFG of \(P_2^L\) in Fig. 7 are unnecessary (they are not present in the native syncCFG) and lead to imprecise facts in an interval analysis on this graph. Some of the final facts in an interval analysis on these graphs are shown alongside the programs in Figs. 6 and 7. In particular the analysis on \(P_2^L\) is unable to prove the assertion in line 10 of the original program.
6.2 A Lightweight LockTranslation
Let us first spell out the translation. Let us fix an interruptdriven program \(P=(V,T)\). The idea is simply to introduce a lock corresponding to each pattern of disjoint block pairs listed in Fig. 4, and to insert at the entry and exit to these blocks an acquire and release (respectively) of the corresponding lock. For each of the cases (a) through (h) we introduce locks named A through H, with some exceptions. Firstly, for case (f) regarding the create of a thread t, we simply translate these as a \(\texttt {spawn}(t)\) command in a classical lockbased programming language, which has a standard acquirerelease semantics. Secondly, for case (h), we need a copy of H for each thread t, which we call \(H_t\). This is because the concerned blocks (say between a set and unset of the flag f) are not disjoint across task threads, but only with the “then” block of an ISR thread statement that checks if \(f = 0\). The ISR thread now acquires the set of locks \(\{H_t \  \ t \in T\}\) at the beginning of the “then” block of the if statement, and releases them at the end of that block. We call the resulting classical lockbased program \(P^W\). Figure 5c shows this translation for the program \(P_1\).
Figure 8 shows this translation along with the syncCFG edges and some of the final facts in an interval analysis for the program \(P_2\).
It is not difficult to see that \(P^W\) allows all executions that are possible in P. However it also allows more: for example the execution of \(P_1^W\) (Fig. 5c) in which thread t1 preempts t2 at line 9 to execute the statement at line 4, is not allowed in \(P_1\). Thus it only weakly captures the execution semantics of P. However, every race in P is also a race in \(P^W\). To see this, suppose we have a race on statements s and t in P. This means there is a highlevel race on the two skip blocks around s and t in the augmented program \(P'\). Since an execution exhibiting the highlevel race on these blocks would also be present in \((P')^W\) which is identical to \((P^W)'\), it follows that the corresponding statements are racy in \(P^W\) as well.
Further, since our translation preserves disjoint blocks by construction, if s and t are in disjoint blocks in P, the corresponding statements will be in disjoint blocks in \(P^W\); and viceversa. It follows that the syncCFGs induced by P and \(P^W\) are essentially isomorphic (modulo the synchronization statements). As a result, any valuesetbased analysis will produce identical results on the two graphs.
Finally, if statements s and t are HBracy in P, they must also be HBracy in \(P^W\). This is because disjoint blocks are preserved and the synchronizeswith relation is inherited from the disjoint blocks. Hence the execution witnessing the HBrace in P would also be present in \(P^W\), and would also witness a HBrace on the corresponding statements.
We summarize these observations below:
Proposition 1
 1.
If statements s and t are racy in P, the corresponding statements are racy in \(P^W\) as well.
 2.
If statements s and t are HBracy in P, the corresponding statements are HBracy in \(P^W\) as well.
 3.
The syncCFGs induced by P and \(P^W\) are essentially isomorphic. As a result the final facts in a valuesetbased analysis on these graphs will be identical.
6.3 Lockset Analysis for Race Detection
For classical lockbased programs, the lockset analysis [24] essentially tracks whether two statements are in disjoint blocks. Here two blocks are disjoint if they hold the same lock for the duration of the block. When two statements are in disjoint blocks, they are necessarily happensbefore ordered, and hence this gives us a way to declare pairs of statements to be nonHBracy.
A lockset analysis computes the set of locks held at each program point as follows: at program entry it is assumed that no locks are held. When a call to acquire(l) is encountered, the analysis adds the lock l at the out point of the call. When a call to release(l) is encountered the lockset at the out point of the call is the lockset computed at the in point with the lock l removed. For any other statement, the lockset from the in point of the statement is copied to its out point. The join operation is the simple intersection of the input locksets. Once locksets are computed at each point, a pair of conflicting statements s and t in different threads are declared to may HBrace if the locksets held at these points have no lock in common.
Using our lock translation above, we can detect races as follows. Given an interruptdriven program P, we first translate it to the lockbased program \(P^W\), and do a lockset analysis on \(P^W\). If any pair of conflicting statements s and t are found to be mayHBracy in \(P^W\), we declare them to be mayHBracy in P. By Proposition 1(2), it follows that this is a sound analysis for interruptdriven programs.
7 Analyzing the FreeRTOS Kernel Library
We now perform an experimental evaluation of the proposed race detection algorithm and syncCFGbased relational analysis for interruptdriven programs. We use the FreeRTOS kernel library [3], on which our interruptdriven program semantics are based, to perform our evaluation. FreeRTOS is a collection of functions mostly written in C, that an application developer compiles with and invokes in the application code. We view the FreeRTOS kernel library as an interruptdriven program as follows: we build an interruptdriven program out of the FreeRTOS kernel as shown in the figure alongside. The main thread is responsible for initializing the kernel data structures and then creating two threads: a task thread which branches out calling each task kernel API function, and loops on this; and an ISR thread which similarly branches and loops on the ISR kernel API functions. FreeRTOS provides versions of API functions that can be called from interrupt service routines. These functions have “FromISR” appended to their name. While it is sufficient to have one ISR thread, we assume (in the analysis) that there could be any number of task threads running. To achieve this we simply add syncedges within each task kernel function, in addition to the usual syncedges between task functions. We used FreeRTOS version 10.0.0 for our experiments. We conducted these experiments on an Intel Core i7 machine with 32 GB RAM running Ubuntu 16.04.
7.1 Race Detection
We consider 49 task and queue API functions that can be called from an application (termed toplevel functions) for race detection. The functions operating on semaphores and mutexes were not considered.
We prepared the API functions for analysis, in two steps: (1) inlining and (2) lock insertion, as follows: The function vTaskStartScheduler and the queue initialization code in the function xQueueGenericCreate were treated as part of the main thread, which initializes kernel data structures. All the helper function calls made inside the toplevel functions were inlined. After inlining, the functions are modified to acquire and release locks using the strategy explained in Sect. 6.2. We consider each pair of disjoint blocks as taking the same distinct lock. For example, the pair of disjoint blocks protected by disableintenableint take lock A. That is disableint is replaced with acquire(A) and enableint is replaced with release(A). A total of 9 locks corresponding to disjoint blocks were employed in the modification of the FreeRTOS code. The two steps outlined above are automated. Inlining is achieved using the inline pass in the CIL framework [22]. Lock insertion is accomplished using a script.
The modified code, which has over 3.5K lines of code, is used for race detection. We tracked 24 variables and check whether the statements accessing them are racy. These variables include fields in the queue datastructure, task control block, and queue registry, as well as variables related to tasks. FreeRTOS maintains lists for the states of the tasks like “ready”, “suspended”, “waiting to send”, etc. The pointers to these lists are also analysed. Access to any portion of a list (like the delayed list) is treated as an access of a corresponding variable of the same name.
Races are detected in this modified FreeRTOS code in three steps  (1) compute locks held, (2) identify whether access of a variable is a read or write, and (3) report potential races. First a lockset analysis, as explained in Sect. 6.3, to compute locks held at each access to variables, is implemented as a pass in CIL. The modified FreeRTOS code is analyzed using this new pass and the lockset at each access to the 24 variables of interest is computed. Then, a writes pass to identify whether accesses to variables are “read” or “write”, also implemented in CIL, is run on the modified FreeRTOS code. Finally, a shell script to interpret both the results in the previous steps and report potential races is employed. The script identifies the conflicting access pairs (using the writes pass) and the locks held by the conflicting accesses (using lockset pass).
Our analysis reports 64 pairs of conflicting accesses as being potentially racy. On manual inspection we classified 18 of them are real races and the rest as false positives. Table 2 summarizes our findings. The second column in the table lists the variables of interest involved in the race, like various task list pointers, queue registry fields pcQueueName and xHandle, task variable uxCurrentNumberOfTasks, tick count xTickCount, etc. The third column lists the functions in which the conflicting accesses are made and the fourth gives the number of racing pairs. The fifth column assesses the potential races based on our manual inspection of the code. The analysis took 3.91 s.
The false positives were typically due to the fact that we had abstracted datastructures (like the delayed list which is a linkedlist) by a synonymous variable. Thus even if the accesses were to different parts of the structure (like the container field of a list item and the next pointer of a different list item) our analysis flagged them as races.
We were in touch with the developers of FreeRTOS regarding the 18 pairs we classified as true positives. The 14 races on the queue registry were deemed to be nonissues as the queue delete function is usually invoked only once the application is about to terminate. The 2 races on uxCurrentNumberOfTasks are known (going by comments in the code) but are considered benign as the variable is of “base type”. The remaining couple of races on the delayed task lists appear to be real issues as they have been fixed (independent of our work) in v10.1.1.
7.2 RegionBased Relational Analysis
Our aim here is to do a regionbased interval and polyhedral analysis of a regionracefree subset of the FreeRTOS kernel APIs, and to prove some simple assertions about the kernel variables in each region.
Potential races
Variables  Functions  \(\#\)Race pairs  Remark 

pxDelayedTaskList  eTaskGetState xTaskIncrementTick  1  Real race. Read of pxDelayedTaskList in eTaskGetState while it is written to in xTaskIncrementTick 
pxOverflowDelayedTaskList  eTaskGetState xTaskIncrementTick  1  Real race. (similar as above) 
uxCurrentNumberOfTasks  xTaskCreate uxTaskGetNumberOfTasks  2  Real race. Unprotected read in uxTaskGetNumberOfTasks while it is written to in xTaskCreate 
pcQueueName xHandle  vQueueDelete pcQueueGetName vQueueAddToRegistry  14  Real race. Unprotected accesses in queue registry functions 
xTasksWaitingToSend xTasksWaitingToReceive  eTaskGetState xQueueGenericReset  2  False positive. Initialization of vars when queue is created 
pxDelayedTaskList pxOverflowDelayedTaskList xSuspendedTaskList pxCurrentTCB  9 functions like xTaskCreate, eTaskGetState, etc.  11  False positive. Initialization of vars when the first task is created 
pxDelayedTaskList pxOverflowDelayedTaskList xSuspendedTaskList xTasksWaitingToSend xTasksWaitingToReceive  13 functions like vTaskDelay, eTaskGetState, etc.  33  False positive. The accesses are to disjoint portions of the lists 
The FreeRTOS code was modified further to reflect access to regions. For this new variables \(R_1,\ldots , R_6\), are declared. Wherever there is a write (or read) access to a variable in region i an assignment statement that defines (or reads from) variable \(R_i\) is inserted just before the access. This is done using a script which takes the result of the writes pass to find where in the source code an appropriate assignment statement has to be inserted. We selected 15 APIs that did not contain any region races.
Next, we prepared the API functions for the analysis in two steps. They are described below:
Abstraction of FreeRTOS API Functions. We abstracted the FreeRTOS source code to prepare it for the relational analysis. In this abstraction, we basically model the various lists (ready list, delayed list) by their lengths and the value at the head of the list (if required). Using this abstraction, we are able to convert list operations to operations on integers.
Similarly, to model insertion into a list, we abstract it by incrementing the variable which represents the length of the list. We abstracted all the API functions in a similar fashion.
Creation of the SyncCFG. The next step is to create a syncCFG out of the abstracted program. For doing this, we used the abstracted version of the FreeRTOS code (along with acquirerelease added as explained in Sect. 7.1).
Next, we used a script to insert nondeterministic gotos from the point of release of a lock to the acquire of the same lock. Since we are using gotos for creation of syncCFG, we keep all the API functions in main itself and evaluate a nondeterministic “if” condition before entering the code for an API function.
Results. For the purpose of analysis we listed out some numerical relations between kernel variables in the same region, which we believed should hold. We identified a total of 15 invariants including 4 invariants which involve relations between kernel variables. We then inserted assertions for these invariants at the key points in our source code like the exit of a block protecting a region.
We have implemented an intervalbased valueset analysis and a regionbased octagon and polyhedral analysis for C programs using CIL [22] as the frontend and the Apron library (version 0.9.11) [16]. We represent the syncwith edges of the syncCFG of a program using goto statements from the source (release) to the target (acquire) of the maysynchronizeswith (MSW) edges.
We ran our implementation on the abstracted version of the FreeRTOS kernel library, with the aim of checking how many of the invariants it was able to prove. The abstracted code along with addition of gotos is about 1500 lines of code. We did a preliminary interval analysis on this abstracted syncCFG and were able to prove 11 out of these 15 invariants. With a widening threshold of 30, the interval analysis takes under 5 min to run. As expected, the interval analysis could not prove the relational invariants.
We then did a regionbased polyhedral analysis using the six regions identified above. For the regionbased analysis, we used convex polyhedra domain with a widening threshold of 30. It is able to prove all the assertions we believed to be true. The analysis takes about 30 min to complete with the convex polyhedra domain and about 20 min with the octagon domain.
Relational analysis results
Assertion  Interval Anal  Region Anal (Oct/Polyhedral) 

xTickCount \(\le \) xNextTaskUnblockTime  No  Yes 
head(pxDelayedTaskList) = xNextTaskUnblockTime  No  Yes 
head(pxDelayedTaskList) \(\ge \) TickCount  No  Yes 
uxMessagesWaiting \(\le \) uxLength  No  Yes 
uxMessagesWaiting \(\ge \) 0  Yes  Yes 
uxCurrentNumberOfTasks \(\ge \) 0  Yes  Yes 
lenpxReadyTasksLists \(\ge \) 0  Yes  Yes 
uxTopReadyPriority \(\ge \) 0  Yes  Yes 
lenpxDelayedTaskList \(\ge \) 0  Yes  Yes 
lenxPendingReadyList \(\ge \) 0  Yes  Yes 
lenxSuspendedTaskList \(\ge \) 0  Yes  Yes 
cRxLock \(\ge \) −1  Yes  Yes 
cTxLock \(\ge \) −1  Yes  Yes 
lenxTasksWaitingToSend \(\ge \) 0  Yes  Yes 
lenxTasksWaitingToReceive \(\ge \) 0  Yes  Yes 
8 Related Work
We classify related work based on the main topics touched upon in this paper.
Data Races. Adve and Hill [1] introduce the notion of a data race using a happensbefore relation, and identify instructions that form releaseacquire pairs, for lowlevel concurrent programs. Boehm and Adve [4] define races in terms of consecutive occurrences in a sequentially consistent execution, as well as using a happensbefore order, in the context of the C++ semantics. They show their notions are equivalent as far as racefree programs go. As pointed out earlier, the definition of races as consecutive occurrences is inadequate in our setting. Schwarz et al. [26] define a notion of data race for prioritybased interruptdriven programs, where there is a single main task and multiple ISRs. A race occurs when the main thread is accessing a variable at a certain dynamic priority, and an ISR thread with higher priority also accesses the variable. Our definition can be seen to be stronger and more accurately captures racy situations. In particular, if the ISR thread with higher priority does not actually execute the conflicting access, due to say a condition not being enabled, then we would not call it a race. The term “highlevel” race was coined by Artho et al. [2]. Our definition of a highlevel race follows that of [20].
Analysis of InterruptDriven Programs. Regehr and Cooprider [23] describe a sourcetosource translation of an interruptdriven program to a standard multithreaded program, and analyze the translated program for races. Their translation is inadequate for our setting in many ways: in particular, disableenable of interrupts is translated by acquiring and releasing all ISRspecific locks; however this does not prevent interaction with another task while one task has disabled interrupts. In [8] they also describe an analysis framework for constantpropagation analysis on TinyOS applications. They use a similar idea of adding “controlflow” edges between disableenable blocks and ISRs. However no soundness argument is given, and other kinds of blocks (suspend/resume, flagbased synchronization) are not handled. The works in [5, 6, 13] analyze timing properties, interruptlatency, and stack sizes for interruptdriven programs, using modelchecking, algebraic, and algorithmic approaches. Schwarz et al. [25, 26] give analyses for racedetection and invariants based on linearequalities for their aforementioned class of prioritybased interruptdriven programs. Our work differs in several ways: Their analysis is directed towards applications (we target libraries where task priorities do not matter), their analyses are specific (we provide a basis for carrying out a variety of valueset and relational analyses, targeting racefree programs), they consider priority and flagbased synchronization (but not disableenable and suspendresume based synchronization). Sung and others [27] consider interruptdriven applications in the form of ISRs with different priorities, and perform intervalbased static analysis for checking assertions. They do not handle libraries and do not leverage racefreedom. Finally, [20] uses a modelchecking approach to find all highlevel races in FreeRTOS with a completeness guarantee.
Analysis of RaceFree Programs. Chugh et al. [7] use race information to do threadmodular nulldereference analysis, by killing facts at a point whenever a notional read of a variable is found to be racy. De et al. [11] propose the syncCFG and valueset analysis for racefree programs, while Mukherjee et al. [21] extend the framework to region and relational analyses. Gotsman et al. [12] and Miné et al. [18, 19] define relational shape/value analyses for concurrent programs that exploit racefreedom and lock invariants respectively. All these works are for classical lockbased synchronization while we target interruptdriven programs.
9 Conclusion
In this paper our aim has been to give efficient static analyses for classes of nonstandard concurrent programs like interruptdriven kernels, that exploit the property of racefreedom. Towards this goal, we have proposed a definition of data races which we feel is applicable to general concurrent programs. We have also proposed a general principle for defining synchronizeswith edges, which is the key ingredient of a happensbefore relation, based on the notion of disjoint blocks. We have implemented our theory to perform sound and effective static analysis for racedetection and invariant inference, on the popular realtime kernel FreeRTOS.
We feel this framework should be applicable to other kinds of concurrent systems, like other embedded kernels (for example TIRTOS [14]) and application programs, and eventdriven programs. There are additional challenges in these systems like prioritybased preemption and priority inheritance conventions which need to be addressed. Apart from investigating these systems we would like to apply this theory to perform other static analyses like nulldereference, pointsto, and shape analysis, for these nonstandard classes of concurrent programs.
References
 1.Adve, S.V., Hill, M.D.: A unified formalization of four sharedmemory models. IEEE Trans. Parallel Distrib. Syst. 4(6), 613–624 (1993)CrossRefGoogle Scholar
 2.Artho, C., Havelund, K., Biere, A.: Highlevel data races. J. Softw. Test. Verif. Reliab. 13, 207–227 (2003)CrossRefGoogle Scholar
 3.Barry, R.: The FreeRTOS kernel, v10.0.0 (2017). https://freertos.org
 4.Boehm, H., Adve, S.V.: Foundations of the C++ concurrency memory model. In: Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, USA, pp. 68–78. ACM (2008)Google Scholar
 5.Brylow, D., Damgaard, N., Palsberg, J.: Static checking of interruptdriven software. In: Proceedings of the 23rd International Conference on Software Engineering, ICSE 2001, Toronto, Ontario, Canada, 12–19 May 2001, pp. 47–56 (2001)Google Scholar
 6.Chatterjee, K., Ma, D., Majumdar, R., Zhao, T., Henzinger, T.A., Palsberg, J.: Stack size analysis for interruptdriven programs. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 109–126. Springer, Heidelberg (2003). https://doi.org/10.1007/3540448985_7CrossRefzbMATHGoogle Scholar
 7.Chugh, R., Voung, J.W., Jhala, R., Lerner, S.: Dataflow analysis for concurrent programs using data race detection. In: Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, 7–13 June 2008, pp. 316–326 (2008)Google Scholar
 8.Cooprider, N., Regehr, J.: Pluggable abstract domains for analyzing embedded software. In: Proceedings of the ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2006), Ottawa, Canada, 14–16 June 2006, pp. 44–53 (2006)Google Scholar
 9.Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the ACM SIGACTSIGPLAN Symposium on Principles of Programming Languages, pp. 238–252. ACM (1977)Google Scholar
 10.De, A.: Access path based dataflow analysis for sequential and concurrent programs. Ph.D. thesis, Indian Institute of Science, Bangalore, December 2012Google Scholar
 11.De, A., D’Souza, D., Nasre, R.: Dataflow analysis for data racefree programs. In: Proceedings of the 20th European Symposium on Programming ESOP 2011, Saarbrücken, Germany, 26 March – 3 April 2011, pp. 196–215 (2011)Google Scholar
 12.Gotsman, A., Berdine, J., Cook, B., Sagiv, M.: Threadmodular shape analysis. In: Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, San Diego, California, USA, 10–13 June 2007, pp. 266–277 (2007)Google Scholar
 13.Huang, Y., Zhao, Y., Shi, J., Zhu, H., Qin, S.: Investigating time properties of interruptdriven programs. In: Gheyi, R., Naumann, D. (eds.) SBMF 2012. LNCS, vol. 7498, pp. 131–146. Springer, Heidelberg (2012). https://doi.org/10.1007/9783642332968_11CrossRefGoogle Scholar
 14.Texas Instruments: TIRTOS: A RealTime Operating System for Microcontrollers (2017). http://www.ti.com/tool/tirtos
 15.Jeannet, B., Miné, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661–667. Springer, Heidelberg (2009). https://doi.org/10.1007/9783642026584_52CrossRefGoogle Scholar
 16.Jeannet Bertrand, M.A.: Apron numerical abstract domain library (2009). http://apron.cri.ensmp.fr/library/
 17.Kini, D., Mathur, U., Viswanathan, M.: Dynamic race prediction in linear time. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, pp. 157–170. ACM, New York (2017)Google Scholar
 18.Miné, A.: Relational threadmodular static value analysis by abstract interpretation. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 39–58. Springer, Heidelberg (2014). https://doi.org/10.1007/9783642540134_3CrossRefzbMATHGoogle Scholar
 19.Monat, R., Miné, A.: Precise threadmodular abstract interpretation of concurrent programs using relational interference abstractions. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 386–404. Springer, Cham (2017). https://doi.org/10.1007/9783319522340_21CrossRefzbMATHGoogle Scholar
 20.Mukherjee, S., Kumar, A., D’Souza, D.: Detecting all highlevel dataraces in an RTOS kernel. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 405–423. Springer, Cham (2017). https://doi.org/10.1007/9783319522340_22CrossRefGoogle Scholar
 21.Mukherjee, S., Padon, O., Shoham, S., D’Souza, D., Rinetzky, N.: Threadlocal semantics and its efficient sequential abstractions for racefree programs. In: Ranzato, F. (ed.) SAS 2017. LNCS, vol. 10422, pp. 253–276. Springer, Cham (2017). https://doi.org/10.1007/9783319667065_13CrossRefGoogle Scholar
 22.Necula, G.: CIL – infrastructure for c program analysis and transformation (v. 1.3.7) (2002). http://people.eecs.berkeley.edu/~necula/cil/
 23.Regehr, J., Cooprider, N.: Interrupt verification via thread verification. Electr. Notes Theor. Comput. Sci. 174(9), 139–150 (2007)CrossRefGoogle Scholar
 24.Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.E.: Eraser: a dynamic data race detector for multithreaded programs. ACM Trans. Comput. Syst. 15(4), 391–411 (1997)CrossRefGoogle Scholar
 25.Schwarz, M.D., Seidl, H., Vojdani, V., Apinis, K.: Precise analysis of valuedependent synchronization in priority scheduled programs. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 21–38. Springer, Heidelberg (2014). https://doi.org/10.1007/9783642540134_2CrossRefGoogle Scholar
 26.Schwarz, M.D., Seidl, H., Vojdani, V., Lammich, P., MüllerOlm, M.: Static analysis of interruptdriven programs synchronized via the priority ceiling protocol. In: Proceedings of the ACM SIGPLANSIGACT Principles of Programming Languages (POPL), pp. 93–104 (2011)Google Scholar
 27.Sung, C., Kusano, M., Wang, C.: Modular verification of interruptdriven software. In: Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, ASE 2017, Urbana, IL, USA, 30 October – 3 November 2017, pp. 206–216 (2017)Google Scholar
 28.Tarski, A., et al.: A latticetheoretical fixpoint theorem and its applications. Pac. J. Math. 5, 285–309 (1955)MathSciNetCrossRefGoogle Scholar
Copyright information
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.