Antoine Min
email: mine@di.ens.fr

STATIC ANALYSIS OF RUN-TIME ERRORS IN EMBEDDED REAL-TIME PARALLEL C PROGRAMS

Keywords: 1998 ACM Subject Classification: D.2.4, F.3.1, F.3.2 Abstract interpretation, parallel programs, run-time errors, static analysis

We present a static analysis by Abstract Interpretation to check for run-time errors in parallel and multi-threaded C programs. Following our work on Astrée, we focus on embedded critical programs without recursion nor dynamic memory allocation, but extend the analysis to a static set of threads communicating implicitly through a shared memory and explicitly using a finite set of mutual exclusion locks, and scheduled according to a real-time scheduling policy and fixed priorities. Our method is thread-modular. It is based on a slightly modified non-parallel analysis that, when analyzing a thread, applies and enriches an abstract set of thread interferences. An iterator then re-analyzes each thread in turn until interferences stabilize. We prove the soundness of our method with respect to the sequential consistency semantics, but also with respect to a reasonable weakly consistent memory semantics. We also show how to take into account mutual exclusion and thread priorities through a partitioning over an abstraction of the scheduler state. We present preliminary experimental results analyzing an industrial program with our prototype, Thésée, and demonstrate the scalability of our approach.

Introduction

Ensuring the safety of critical embedded software is important as a single "bug" can have catastrophic consequences. Previous work on the Astrée analyzer [START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF] demonstrated that static analysis by Abstract Interpretation could help, when specializing an analyzer to a class of properties and programs -namely in that case, the absence of run-time errors (such as arithmetic and memory errors) on synchronous control / command embedded avionic C software. In this article, we describe ongoing work to achieve similar results for multi-threaded and parallel embedded C software. Such an extension is demanded by the current trend in critical embedded systems to switch from large numbers of single-program processors communicating through a common bus to single-processor multi-threaded applications communicating through a shared memory -for instance, in the context of Integrated Modular Avionics [START_REF] Watkins | Transitioning from federated avionics architectures to integrated modular avionics[END_REF]. Analyzing each thread independently with a tool such as Astrée would not be sound and could miss bugs that only appear when threads interact. In this article, we focus on detecting the same kinds of run-time errors as Astrée does, while taking thread communications into account in a sound way, including accesses to the shared memory and synchronization primitives. In particular, we correctly handle the effect of concurrent threads accessing a common variable without enforcing mutual exclusion by synchronization primitives, and we report such accesses -these will be called data-races in the rest of the article. However, we ignore other concurrency hazards such as dead-locks, live-locks, and priority inversions, which are considered to be orthogonal issues.

Our method is based on Abstract Interpretation [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF], a general theory of the approximation of semantics which allows designing static analyzers that are fully automatic and sound by construction -i.e., consider a superset of all program behaviors. Such analyzers cannot miss any bug in the class of errors they analyze. However, they can cause spurious alarms due to over-approximations, an unfortunate effect we wish to minimize while keeping the analysis efficient.

To achieve scalability, our method is thread-modular and performs a rely-guarantee reasoning, where rely and guarantee conditions are inferred automatically. At its core, it performs a sequential analysis of each thread considering an abstraction of the effects of the other threads, called interferences. Each sequential analysis also collects a new set of interferences generated by the analyzed thread. It then serves as input when analyzing the other threads. Starting from an empty set of interferences, threads are re-analyzed in sequence until a fixpoint of interferences is reached for all threads. Using this scheme, few modifications are required to a sequential analyzer in order to analyze multi-threaded programs. Practical experiments suggest that few thread re-analyses are required in practice, resulting in a scalable analysis. The interferences are considered in a flow-insensitive and non-relational way: they store, for each variable, an abstraction of the set of all values it can hold at any program point of a given thread. Our method is however quite generic in the way individual threads are analyzed. They can be analyzed in a fully or partially flow-sensitive, context-sensitive, path-sensitive, and relational way (as is the case in our prototype).

As we target embedded software, we can safely assume that there is no recursion, dynamic allocation of memory, nor dynamic creation of threads nor locks, which makes the analysis easier. In return, we handle two subtle points. Firstly, we consider a weakly consistent memory model: memory accesses not protected by mutual exclusion (i.e., data-races) may cause behaviors that are not the result of any thread interleaving to appear. The reason is that arbitrary observation by concurrent threads can expose compiler and processor optimizations (such as instruction reordering) that are designed to be transparent on non-parallel programs only. We prove that our semantics is invariant by large classes of widespread program transformations, so that an analysis of the original program is also sound with respect to reasonably compiled and optimized versions. Secondly, we show how to take into account the effect of a real-time scheduler that schedules the threads on a single processor following strict, fixed priorities. According to this scheduling algorithm, which is quite common in the realm of embedded real-time software -e.g., in the real-time thread extension of the POSIX standard [START_REF]Portable operating system interface (POSIX) -Application program interface (API) amendment 2: Threads extension (C language). Technical report[END_REF], or in the ARINC 653 avionic operating system standard [3] -only the unblocked thread of highest priority may run. This ensures some lock-less mutual exclusion properties that are actually exploited in real-time embedded programs and relied on for their correctness (this includes the industrial application our prototype currently targets). We show how our analysis can take these properties into account, but we also present an analysis that assumes less properties on the scheduler and is thus sound for true multi-processors and non-real-time schedulers. We handle synchronization properties (enforced by either locks or priorities) through a partitioning with respect to an abstraction of the global scheduling state. The partitioning recovers some kind of inter-thread flow-sensitivity that would otherwise be completely abstracted away by the interference abstraction.

The approach presented in this article has been implemented and used at the core of a prototype analyzer named Thésée. It leverages the static analysis techniques developed in Astrée [START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF] for single-threaded programs, and adds the support for multiple threads. We used Thésée to analyze in 27 h a large (1.7 M lines) multi-threaded industrial embedded C avionic application, which illustrates the scalability of our approach.

Organisation. Our article is organized as follows. First, Sec. 2 presents a classic nonparallel semantics and its static analysis. Then, Sec. 3 extends them to several threads in a shared memory and discusses weakly consistent memory issues. A model of the scheduler and support for locks and priorities are introduced in Sec. 4. Our prototype analyzer, Thésée, is presented in Sec. 5, as well as some experimental results. Finally, Sec. 6 discusses related work, and Sec. 7 concludes and envisions future work.

This article defines many semantics. They are summarized in Fig. 1, using ⊆ to denote the "is less abstract than" relation. We alternate between two kinds of concrete semantics: semantics based on control paths (P π , P * , P H ), that can model precisely thread interleavings and are also useful to characterize weakly consistent memory models (P * , P H ), and semantics by structural induction on the syntax (P, P I , P C ), that give rise to effective abstract interpreters (P , P I , P C ). Each semantics is presented in its subsection and adds some features to the previous ones, so that the final abstract analysis P C presented in Sec. 4.5 should hopefully not appear as too complex nor artificial, but rather as the logical conclusion of a step-by-step construction.

Our analysis has been mentioned first, briefly and informally, in [START_REF] Bertrane | Static analysis and verification of aerospace software by abstract interpretation[END_REF]§ VI]. We offer here a formal, rigorous treatment by presenting all the semantics fully formally, albeit on an idealised language, and by studying their relationship. The present article is an extended version of [START_REF] Miné | Static analysis of run-time errors in embedded critical parallel C programs[END_REF] and includes a more comprehensive description of the semantics as well as the proof of all theorems, that were omitted in the conference proceedings due to lack of space.

Notations. In this article, we use the theory of complete lattices, denoting their partial order, join, and least element respectively as , , and ⊥, possibly with some subscript to indicate which lattice is considered. All the lattices we use are actually constructed by taking the Cartesian product of one or several powerset lattices -i.e., P(S) for some set S -, , and ⊥ are then respectively the set inclusion ⊆, the set union ∪, and the empty set ∅, applied independently to each component. Given a monotonic operator F in a complete lattice, we denote by lfp F its least fixpoint -i.e., F (lfp F ) = lfp F and ∀X : F (X) = X =⇒ lfp F X -which exists according to Tarski [START_REF] Tarski | A lattice theoretical fixpoint theorem and its applications[END_REF][START_REF] Cousot | Constructive versions of Tarski's fixed point theorems[END_REF]. We denote by A → B the set of functions from a set A to a set B, and by A -→ B the set of non-parallel semantics parallel semantics complete -morphisms from a complete lattice A to a complete lattice B, i.e., such that F ( A X) = B { F (x) | x ∈ X } for any finite or infinite set X ⊆ A. Additionally, such a function is monotonic. We use the theory of Abstract Interpretation by Cousot and Cousot and, more precisely, its concretization-based (γ) formalization [START_REF] Cousot | Abstract interpretation frameworks[END_REF]. We use widenings ( ) to ensure termination [START_REF] Cousot | Comparing the Galois connection and widening/narrowing approaches to abstract interpretation[END_REF]. The abstract version of a domain, operator, or function is denoted with a superscript. We use the lambda notation λx : f (x) to denote functions. If f is a function, then f [x → v] is the function with the same domain as f that maps x to v, and all other elements y = x to f (y). Likewise, f [∀x ∈ X : x → g(x)] denotes the function that maps any x ∈ X to g(x), and other elements y / ∈ X to f (y). Boldface fonts are used for syntactic elements, such as "while" in Fig. 2. Pairs and tuples are bracketed by parentheses, as in X = (A, B, C), and can be deconstructed (matched) with the notation "let (A, -, C) = X in • • • " where the "-" symbol denotes irrelevant tuple elements. The notation "let ∀x ∈ X :

P ( §2.
y x = • • • in • • • " is
used to bind a collection of variables (y x ) x∈X at once. Semantic functions are denoted with double brackets, as in X y , where y is an (optional) syntactic object, and X denotes the kind of objects (S for statements, E for expressions, P for programs, Π for control paths). The kind of semantics considered (parallel, non-parallel, abstract, etc.) is denoted by subscripts and superscripts over X, as exemplified in Fig. 1. Finally, we use finite words over arbitrary sets, using and • to denote, respectively, the empty word and word concatenation. The concatenation • is naturally extended to sets of words:

A • B def = { a • b | a ∈ A, b ∈ B }.

Non-parallel Programs

This section recalls a classic static analysis by Abstract Interpretation of the run-time errors of non-parallel programs, as performed for instance by Astrée [START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF]. The formalization introduced here will be extended later to parallel programs, and it will be apparent that an analyzer for parallel programs can be constructed by extending an analyzer for non-parallel programs with few changes. 2.1. Syntax. For the sake of exposition, we reason on a vastly simplified programming language. However, the results extend naturally to a realistic language, such as the subset of C excluding recursion and dynamic memory allocation considered in our practical experiments (Sec. 5). We assume a fixed, finite set of variable names V. A program is a single structured statement, denoted body ∈ stat. The syntax of statements stat and of expressions expr is depicted in Fig. 2. Constants are actually constant intervals [c 1 , c 2 ], which return a new arbitrary value between c 1 and c 2 every time the expression is evaluated. This allows modeling non-deterministic expressions, such as inputs from the environment, or stubs for expressions that need not be handled precisely, e.g., sin(x) could be replaced with [-1, 1]. Each unary and binary operator is tagged with a syntactic location ∈ L and we denote by L the finite set of all syntactic locations. The output of an analyzer will be the set of locations with errors -or rather, a superset of them, due to approximations.

For the sake of simplicity, we do not handle procedures. These are handled by inlining in our prototype. We also focus on a single data-type (real numbers in R) and numeric expressions, which are sufficient to provide interesting properties to express, e.g., variable bounds, although in the following we will only discuss proving the absence of division by zero. Handling of realistic data-types (machine integers, floats arrays, structures, pointers, etc.) and more complex properties (such as the absence of numeric and pointer overflow) as done in our prototype is orthogonal, and existing methods apply directly -for instance [START_REF] Bertrane | Static analysis and verification of aerospace software by abstract interpretation[END_REF].

Concrete Structured Semantics P.

As usual in Abstract Interpretation, we start by providing a concrete semantics, that is, the most precise mathematical expression of program semantics we consider. It should be able to express the properties of interest to us, i.e., which run-time errors can occur -only divisions by zero for the simplified language of Fig. 2. For this, it is sufficient that our concrete semantics tracks numerical invariants. As this problem is undecidable, it will be abstracted in the next section to obtain a sound static analysis.

A program environment ρ ∈ E maps each variable to a value, i.e., E def = V → R. The semantics E e of an expression e ∈ expr takes as input a single environment ρ, and outputs a set of values, in P(R), and a set of locations of run-time errors, in P(L). It is defined by structural induction in Fig. 3. Note that an expression can evaluate to one value, several values (due to non-determinism in [c 1 , c 2 ]) or no value at all (in the case of a division by zero).

E e : E → (P(R) × P(L)) E X ρ def = ({ ρ(X) }, ∅) E [c 1 , c 2 ] ρ def = ({ c ∈ R | c 1 ≤ c ≤ c 2 }, ∅) E -e ρ def = let (V, Ω) = E e ρ in ({ -x | x ∈ V }, Ω) E e 1 e 2 ρ def = let (V 1 , Ω 1 ) = E e 1 ρ in let (V 2 , Ω 2 ) = E e 2 ρ in ({ x 1 x 2 | x 1 ∈ V 1 , x 2 ∈ V 2 , = / ∨ x 2 = 0 }, Ω 1 ∪ Ω 2 ∪ { | = / ∧ 0 ∈ V 2 }) where ∈ { +, -, ×, / }
To define the semantics of statements, we consider as semantic domain the complete lattice:

D def = P(E) × P(L) (2.1)
with partial order defined as the pairwise set inclusion: (A, B)

(A , B ) def ⇐⇒ A ⊆ A ∧ B ⊆ B .
We denote by the associated join, i.e., pairwise set union. The structured semantics S s of a statement s is a morphism in D that, given a set of environments R and errors Ω before a statement s, returns the reachable environments after s, as well as Ω enriched with the errors encountered during the execution of s. It is defined by structural induction in Fig. 4. We introduce the new statements e 0? (where ∈ { =, =, <, >, ≤, ≥ } is a comparison operator) which we call "guards." These statements do not appear standalone in programs, but are useful to factor the semantic definition of conditionals and loops (they are similar to the guards used in Dijkstra's Guarded Commands [START_REF] Dijkstra | Guarded commands, non-determinacy and formal derivation of programs[END_REF]). Guards will also prove useful to define control paths in Sec. 2.4. Guards filter their argument and keep only those environments where the expression e evaluates to a set containing a value v satisfying v 0. The symbol denotes the negation of , i.e., the negation of =, =, <, >, ≤, ≥ is, respectively, =, =, ≥, ≤, >, <. Finally, the semantics of loops computes a loop invariant using the least fixpoint operator lfp. The fact that such fixpoints exist, and the related fact that the semantic functions are complete -morphisms, i.e., S s ( i∈I X i ) = i∈I S s X i , is stated in the following theorem: Theorem 2.1. ∀s ∈ stat : S s is well defined and a complete -morphism.

Proof. In Appendix A.1.

We can now define the concrete structured semantics of the program as follows:

P def = Ω, where (-, Ω) = S body (E 0 , ∅) (2.2)
where E 0 ⊆ E is a set of initial environments. We can choose, for instance,

E 0 = E or E 0 def = { λX ∈ V : 0 }.
Note that all run-time errors are collected while traversing the program structure; they are never discarded and all of them eventually reach the end of body, and so, appear in P, even if S body (E 0 , ∅) outputs an empty set of environments. Our program semantics thus observes the set of run-time errors that can appear in any execution starting at the beginning of body in an initial environment. This includes errors occurring in executions that loop forever (such as infinite reactive loops in control / command software) or that halt before the end of body.

S s : D -→ D S X ← e (R, Ω) def = (∅, Ω) ρ∈R let (V, Ω ) = E e ρ in ({ ρ[X → v] | v ∈ V }, Ω ) S e 0? (R, Ω) def = (∅, Ω) ρ∈R let (V, Ω ) = E e ρ in ({ ρ | ∃v ∈ V : v 0 }, Ω ) S s 1 ; s 2 (R, Ω) def = (S s 2 • S s 1 )(R, Ω) S if e 0 then s (R, Ω) def = (S

2.3.

Abstract Structured Semantics P . The semantics P is not computable as it involves least fixpoints in an infinite-height domain D, and not all elements in D are representable in a computer as D is uncountable. Even if we restricted variable values to a more realistic, large but finite, subset -such as machine integers or floats -naive computation in D would be unpractical. An effective analysis will instead compute an abstract semantics over-approximating the concrete one.

The abstract semantics is parametrized by the choice of an abstract domain of environments obeying the signature presented in Fig. 5. It comprises a set E of computerrepresentable abstract environments, with a partial order ⊆ E (denoting abstract entailment) and an abstract environment E 0 ∈ E representing initial environments. Each abstract environment represents a set of concrete environments through a monotonic concretization function γ E : E → P(E). We also require an effective abstract version ∪ E of the set union ∪, as well as effective abstract versions S s of the semantic operators S s for assignment and guard statements. Only environment sets are abstracted, while error sets are represented explicitly, so that the actual abstract semantic domain for S s is D def = E × P(L), with concretization γ defined in Fig. 5. Figure 5 also presents the soundness conditions that state that an abstract operator outputs a superset of the environments and error locations returned by its concrete version. Finally, when E has infinite strictly increasing chains, we require a widening operator E , i.e., a sound abstraction of the join ∪ with a termination guarantee to ensure the convergence of abstract fixpoint computations in finite time. There exist many abstract domains E , for instance the interval domain [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF], where an abstract environment in E associates an interval to each variable, the octagon domain [START_REF] Miné | The octagon abstract domain[END_REF], where an abstract environment in E is a conjunction of constraints of the form ±X ± Y ≤ c with X, Y ∈ V, c ∈ R, or the polyhedra domain [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF], where an abstract environment in E is a convex, closed (possibly unbounded) polyhedron.

In the following, we will refer to assignments and guards collectively as primitive statements. Their abstract semantics S s in D depends on the choice of abstract domain; we assume it is provided as part of the abstract domain definition and do not discuss it. By contrast, the semantics of non-primitive statements can be derived in a generic way,

E (set of abstract environments) γ E : E → P(E) (concretization) ⊥ E ∈ E (empty abstract environment) s.t. γ E (⊥ E ) = ∅ E 0 ∈ E (initial abstract environment) s.t. γ E (E 0 ) ⊇ E 0 ⊆ E : (E × E ) → { true, false } (abstract entailment) s.t. X ⊆ E Y =⇒ γ E (X ) ⊆ γ E (Y ) ∪ E : (E × E ) → E (abstract join) s.t. γ E (X ∪ E Y ) ⊇ γ E (X ) ∪ γ E (Y ) E : (E × E ) → E (widening) s.t. γ E (X E Y ) ⊇ γ E (X ) ∪ γ E (Y ) and ∀(Y i ) i∈N : the sequence X 0 = Y 0 , X i+1 = X i E Y i+1 reaches a fixpoint X k = X k+1 for some k ∈ N D def = E × P(L) (abstraction of D) γ : D → D (concretization for D ) s.t. γ(R , Ω) def = (γ E (R ), Ω) S s : D → D s.t. ∀s ∈ { X ← e, e 0? } : (S s • γ)(R , Ω) (γ • S s )(R , Ω)
Figure 5: Abstract domain signature, and soundness and termination conditions.

as presented in Fig. 6. Note the similarity between these definitions and the concrete semantics of Fig. 4, except for the semantics of loops that uses additionally a widening operator derived from E . The termination guarantee of the widening ensures that, given any (not necessarily monotonic) function

F : D → D , the sequence X 0 def = (⊥ E , ∅), X i+1 def = X i F (X i ) reaches a fixpoint X k = X k+1 in finite time k ∈ N.
We denote this limit by lim λX : X F (X ). Note that, due to widening, the semantics of a loop is generally not a join morphism, and even not monotonic [START_REF] Cousot | Comparing the Galois connection and widening/narrowing approaches to abstract interpretation[END_REF], even if the semantics of the loop body is. Hence, there would be little benefit in imposing that the semantics of primitive statements provided with D is monotonic, and we do not impose it in Fig. 5. Note also that lim F may not be the least fixpoint of F (in fact, such a least fixpoint may not even exist).

The abstract semantics of a program can then be defined, similarly to (2.2), as:

P def = Ω, where (-, Ω) = S body (E 0 , ∅) .
The following theorem states the soundness of the abstract semantics: Theorem 2.2. P ⊆ P .

Proof. In Appendix A.2.

The resulting analysis is flow-sensitive. It is relational whenever E is -e.g., with octagons [START_REF] Miné | The octagon abstract domain[END_REF]. The iterator follows, in the terminology of [START_REF] Bourdoncle | Efficient chaotic iteration strategies with widenings[END_REF], a recursive iteration strategy.

S s : D → D S s 1 ; s 2 (R , Ω) def = (S s 2 • S s 1 )(R , Ω) S if e 0 then s (R , Ω) def = (S s • S e 0? )(R , Ω) ∪ S e 0? (R , Ω) S while e 0 do s (R , Ω) def = S e 0? (lim λX : X ((R , Ω) ∪ (S s • S e 0? )X )) where: (R 1 , Ω 1 ) ∪ (R 2 , Ω 2 ) def = (R 1 ∪ E R 2 , Ω 1 ∪ Ω 2 ) (R 1 , Ω 1 ) (R 2 , Ω 2 ) def = (R 1 E R 2 , Ω 1 ∪ Ω 2 )
Figure 6: Derived abstract functions for non-primitive statements.

The advantage of this strategy is its efficient use of memory: few abstract elements need to be kept in memory during the analysis. Indeed, apart from the current abstract environment, a clever implementation of Fig. 6 exploiting tail recursion would only need to keep one extra environment per if e 0 then s statement -to remember the (R , Ω) argument while evaluating s -and two environments per while e 0 do s statement -one for (R , Ω) and one for the accumulator X -in the call stack of the abstract interpreter function S . Thus, the maximum memory consumption is a function of the maximum nesting of conditionals and loops in the analyzed program, which is generally low. This efficiency is key to analyze large programs, as demonstrated by Astrée [START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF].

2.4. Concrete Path-Based Semantics P π . The structured semantics of Sec. 2.2 is defined as an interpretation of the program by induction on its syntactic structure, which can be conveniently transformed into a static analyzer, as shown in Sec. 2.3. Unfortunately, the execution of a parallel program does not follow such a simple syntactic structure; it is rather defined as an interleaving of control paths from distinct threads (Sec. 3.1). Before considering parallel programs, we start by proposing in this section an alternate concrete semantics of non-parallel programs based on control paths. While its definition is different from the structured semantics of Sec. 2.2, its output is equivalent.

A control path p is any finite sequence of primitive statements, among X ← e, e 0?. We denote by Π the set of all control paths. Given a statement s, the set of control paths it spawns π(s) ⊆ Π is defined by structural induction as follows:

π(X ← e) def = { X ← e } π(s 1 ; s 2 ) def = π(s 1 ) • π(s 2 ) π(if e 0 then s) def = ({ e 0? } • π(s)) ∪ { e 0? } π(while e 0 do s) def = (lfp λX : { } ∪ (X • { e 0? } • π(s))) • { e 0? } (2.3)
where denotes then empty path, and • denotes path concatenation, naturally extended to sets of paths. A primitive statement spawns a singleton path of length one, while a conditional spawns two sets of paths -one set where the then branch is taken, and one where it is not taken -and loops spawn an infinite number of paths -corresponding to all possible unrollings. Although π(s) is infinite whenever s contains a loop, it is possible that many control paths in π(s) are actually infeasible, i.e., have no corresponding execution. In particular, even if a loop s is always bounded, π(s) contains unrollings of arbitrary length.

We can now define the semantics Π P ∈ D -→ D of a set of paths P ⊆ Π as follows, reusing the semantics of primitive statements from Fig. 4 and the pairwise join on sets of environments and errors:

Π P (R, Ω) def = { (S s n • • • • • S s 1 )(R, Ω) | s 1 • . . . • s n ∈ P } . (2.4)
The path-based semantics of a program is then:

P π def = Ω, where (-, Ω) = Π π(body) (E 0 , ∅) . (2.5)
Note that this semantics is similar to the standard meet over all paths solution 1 of data-flow problems -see, e.g., [48, § 2] -but for concrete executions in the infinite-height lattice D.

The meet over all paths and maximum fixpoint solutions of data-flow problems are equal for distributive frameworks; similarly, our structured and path-based concrete semantics (based on complete -morphisms) are equal:

Theorem 2.3. ∀s ∈ stat : Π π(s) = S s .
Proof. In Appendix A.3.

An immediate consequence of this theorem is that P = P π , hence the two semantics compute, in different ways, the same set of errors.

Parallel Programs in a Shared Memory

In this section, we consider several threads that communicate through a shared memory, without any synchronization primitive yet -they will be introduced in Sec. 4. We also discuss here the memory consistency model, and its effect on the semantics and the static analysis.

A program has now a fixed, finite set T of threads. To each thread t ∈ T is associated a statement body body t ∈ stat. All the variables in V are shared and can be accessed by all threads.

3.1. Concrete Interleaving Semantics P * . The simplest and most natural model of parallel program execution considers all possible interleavings of control paths from all threads. These correspond to sequentially consistent executions, as coined by Lamport [START_REF] Lamport | How to make a multiprocessor computer that correctly executes multiprocess programs[END_REF].

A parallel control path p is a finite sequence of pairs (s, t), where s is a primitive statement (assignment or guard) and t ∈ T is a thread that executes it. We denote by Π * the set of all parallel control paths. The semantics Π * P ∈ D -→ D of a set of parallel control paths P ⊆ Π * is defined as in the case of regular control paths (2.4), ignoring thread identifiers:

Π * P (R, Ω) def = { (S s n • • • • • S s 1 )(R, Ω) | (s 1 , -) • . . . • (s n , -) ∈ P } . (3.1)
1 The lattices used in data-flow analysis and in abstract interpretation are dual: the former use a meet to join paths -hence the expression "meet over all paths" -while we employ a join . Likewise, the greatest fixpoint solution of a data-flow analysis corresponds to our least fixpoint.

We now denote by π * ⊆ Π * the set of parallel control paths spawned by the whole program. It is defined as:

π * def = { p ∈ Π * | ∀t ∈ T : proj t (p) ∈ π(body t ) } (3.2)
where the set π(body t ) of regular control paths of a thread is defined in (2.3), and proj t (p) extracts the maximal sub-path of p on thread t as follows:

proj t ((s 1 , t 1 ) • . . . • (s n , t n )) def = s i 1 • . . . • s im such that ∀j : 1 ≤ i j < i j+1 ≤ n ∧ t i j = t ∧ ∀k : (k < i 1 ∨ k > i m ∨ i j < k < i j+1 ) =⇒ t k = t .
The semantics P * of a parallel program becomes, similarly to (2.5):

P * def = Ω, where (-, Ω) = Π * π * (E 0 , ∅) (3.3)
i.e., we collect the errors that can appear in any interleaved execution of all the threads, starting in an initial environment.

Because we interleave primitive statements, a thread can only interrupt another one between two primitive statements, and not in the middle of a primitive statement. For instance, in a statement such as X ← Y + Y , no thread can interrupt the current one and change the value of Y between the evaluation of the first and the second Y sub-expression, while it can if the assignment is split into X ← Y ; X ← X + Y . Primitive statements are thus atomic in P * . By contrast, we will present a semantics where primitive statements are not atomic in Sec. 3.4.

3.2. Concrete Interference Semantics P I . Because it reasons on infinite sets of paths, the concrete interleaving semantics from the previous section is not easily amenable to abstraction. In particular, replacing the concrete domain D in P * with an abstract one D (as defined in Sec. 2.3) is not sufficient to obtain an effective and efficient static analyzer as we still have a large or infinite number of paths to analyze separately and join. By contrast, we propose here a (more abstract) concrete semantics that can be expressed by induction on the syntax. It will lead naturally, after further abstraction in Sec. 3.3, to an effective static analysis.

3.2.1. Thread semantics. We start by enriching the non-parallel structured semantics of Sec. 2.2 with a notion of interference. We call interference a triple (t, X, v) ∈ I, where I def = T × V × R, indicating that the thread t can set the variable X to the value v. However, it does not say at which program point the assignment is performed, so, it is a flow-insensitive information.

The new semantics of an expression e, denoted E I e , takes as argument the current thread t ∈ T and an interference set I ⊆ I in addition to an environment ρ ∈ E. It is defined in Fig. 7. The main change with respect to the interference-free semantics E e of Fig. 3 is that, when fetching a variable X ∈ V, each interference (t , v, X) ∈ I on X from any other thread t = t is applied. The semantics of constants and operators is not changed, apart from propagating t and I recursively. Note that the choice of evaluating E I X (t, ρ, I) to ρ(X) or to some interference in I, as well as the choice of the interference in I, is non-deterministic. Thus, distinct occurrences of the same variable in an expression may evaluate, in the same environment, to different values.

E I e : (T × E × P(I)) → (P(R) × P(L))

E I X (t, ρ, I) def = ({ ρ(X) } ∪ { v | ∃t = t : (t , X, v) ∈ I }, ∅) E I [c 1 , c 2 ] (t, ρ, I) def = ({ c ∈ R | c 1 ≤ c ≤ c 2 }, ∅) E I -e (t, ρ, I) def = let (V, Ω) = E I e (t, ρ, I) in ({ -x | x ∈ V }, Ω) E I e 1 e 2 (t, ρ, I) def = let (V 1 , Ω 1 ) = E I e 1 (t, ρ, I) in let (V 2 , Ω 2 ) = E I e 2 (t, ρ, I) in ({ x 1 x 2 | x 1 ∈ V 1 , x 2 ∈ V 2 , = / ∨ x 2 = 0 }, Ω 1 ∪ Ω 2 ∪ { | = / ∧ 0 ∈ V 2 }) where ∈ { +, -, ×, / }
S I s, t : D I I -→ D I S I X ← e, t (R, Ω, I) def = (∅, Ω, I) I I ρ∈R let (V, Ω ) = E I e (t, ρ, I) in ({ ρ[X → v] | v ∈ V }, Ω , { (t, X, v) | v ∈ V })
S I e 0?, t (R, Ω, I) The semantics of a statement s executed by a thread t ∈ T is denoted S I s, t . It is presented in Fig. 8. This semantics is enriched with interferences and is thus a complete I -morphism in the complete lattice:

S I s 1 ; s 2 , t (R, Ω, I) def = (S I s 2 , t • S I s 1 , t )(R, Ω, I)
D I def = P(E) × P(L) × P(I)
where the join I is the pairwise set union. The main point of note is the semantics of assignments X ← e. It both uses its interference set argument, passing it to E I e , and enriches it with the interferences generated on the assigned variable X. The semantics of guards simply uses the interference set, while the semantics of conditionals, loops, and sequences is identical to the non-interference one from Fig. 4. The structured semantics of a thread t with interferences I is then S I body t , t (E 0 , ∅, I).

Program semantics.

The semantics S I body t , t still only analyzes the effect of a single thread t. It assumes a priori knowledge of the other threads, through I, and contributes to this knowledge, by enriching I. To solve this dependency and take into account multiple threads, we iterate the analysis of all threads until interferences stabilize. Thus, the semantics of a multi-threaded program is:

P I def = Ω, where (Ω, -) def = lfp λ(Ω, I) : t∈T let (-, Ω , I ) = S I body t , t (E 0 , Ω, I) in (Ω , I ) (3.4)
where the join is the componentwise set union in the complete lattice P(L) × P(I).

3.

Π I P, t (R, Ω, I) def = I { (S I s n , t • • • • • S I s 1 , t )(R, Ω, I) | s 1 • . . . • s n ∈ P } .
(3.5) These two forms are equivalent, and Thm. 2.3 naturally becomes:

Theorem 3.1. ∀t ∈ T , s ∈ stat : Π I π(s), t = S I s, t .
Proof. In Appendix A.4.

The following theorem then states that the semantics P I computed with an interference fixpoint is indeed sound with respect to the interleaving semantics P * that interleaves paths from all threads: Theorem 3.2. P * ⊆ P I .

Proof. In Appendix A.5.

The equality does not hold in general. Consider, for instance, the program fragment in Fig. 9(a) inspired from Dekker's mutual exclusion algorithm [START_REF] Dijkstra | Cooperating sequential processes[END_REF]. According to the interleaving semantics, both threads can never be in their critical section simultaneously. The interference semantics, however, does not ensure mutual exclusion. Indeed, it computes the following set of interferences: { (t 1 , flag1, 1), (t 2 , flag2, 1) }. Thus, in thread t 1 , flag2 evaluates to {0, 1}. The value 0 comes from the initial state E 0 and the value 1 comes from the interference (t 2 , flag2, 1). Likewise, flag1 evaluates to {0, 1} in thread t 2 . Thus, both conditions flag1 = 0 and flag2 = 0 can be simultaneously true. This imprecision is due to the flow-insensitive treatment of interferences. We now present a second example of incompleteness where the loss of precision is amplified by the interference fixpoint. Consider the program in Fig. 9(b) where two threads increment the same zero-initialized variable x. According to the interleaving semantics, either the value 1 or 2 is stored into y. However, in the interference semantics, the interference fixpoint builds a growing set of interferences, up to { (t, x, i) | t ∈ {t 1 , t 2 }, i ≥ 1 }, as each thread increments the possible values written by the other thread. Note that the program features no loop and x can thus be incremented only finitely many times (twice), but the interference abstraction is flow-insensitive and forgets how many times an action can be performed. As a consequence, any positive value can be stored into y, instead of only 1 or 2.

Our interference semantics is based on a decomposition of the invariant properties of parallel programs into a local invariant at each thread program point and a global interference invariant. This idea is not new, and complete methods to do so have already been

E 0 : flag1 = flag2 = 0 thread t 1 thread t 2 flag1 ← 1;
flag2 ← 1; if flag2 = 0 then if flag1 = 0 then critical section critical section (a) Mutual exclusion algorithm. proposed. Such methods date back to the works of Owicki, Gries, and Lamport [START_REF] Owicki | An axiomatic proof technique for parallel programs I[END_REF][START_REF] Lamport | Proving the correctness of multiprocess programs[END_REF][START_REF] Lamport | The "Hoare logic" of concurrent programs[END_REF] and have been formalized in the framework of Abstract Interpretation by Cousot and Cousot [START_REF] Cousot | Invariance proof methods and analysis techniques for parallel programs[END_REF]. We would say informally that our interference semantics is an incomplete abstraction of such complete methods, where interferences are abstracted in a flow-insensitive and nonrelational way. Our choice to abstract away these information is a deliberate move that eases considerably the construction of an effective and efficient static analyzer, as shown in Sec. 3.3. Another strong incentive is that the interference semantics is compatible with the use of weakly consistent memory models, as shown in Sec. 3.4. Note finally that Sec. 4.4 will present a method to recover a weak form of flow-sensitivity (i.e., mutual exclusion) on interferences, without loosing the efficiency nor the correctness with respect to weak memory models.

E 0 : x = y = 0 thread t 1 thread t 2 x ← x + 1; x ← x + 1 y ← x (b) Parallel incrementation.
3.3. Abstract Interference Semantics P I . The concrete interference semantics P I introduced in the previous section is defined by structural induction. It can thus be easily abstracted to provide an effective, always-terminating, and sound static analysis.

We assume, as in Sec. 2.3, the existence of an abstract domain E abstracting sets of environments -see Fig. 5. Additionally, we assume the existence of an abstract domain N that abstracts sets of reals, which will be useful to abstract interferences. Its signature is presented in Fig. 10. It is equipped with a concretization γ N : N → P(R), a least element ⊥ N , an abstract join ∪ N and, if it has strictly increasing infinite chains, a widening N . We also require two additional functions that will be necessary to communicate information between E and N . Firstly, a function get(X, R ) that extracts from an abstract environment R ∈ E the set of values a variable X ∈ V can take, and abstracts this set in N . Secondly, a function as-expr (V ) able to synthesize a (constant) expression approximating any non-empty abstract value V ∈ N \ {⊥ N }. This provides a simple way to use an abstract value from N in functions on abstract environments in E . For instance, S X ← as-expr (V ) (R , Ω) non-deterministically sets the variable X in the environments γ E (R ) to any value in γ N (V ).

Any non-relational domain on a single variable can be used as N . One useful example is the interval domain [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]. In this case, an element in N is either ⊥ N , or a pair consisting of a lower and an upper bound. The function as-expr is then straightforward because intervals can be directly and exactly represented in the syntax of expressions. Moreover, the function get consists in extracting the range of a variable from an abstract environment R ∈ E , an operation which is generally available in the implementations of numerical abstract domains, e.g., in the Apron library [START_REF] Jeannet | Apron: A library of numerical abstract domains for static analysis[END_REF]. We now show how, given these domains, we can construct an abstraction P I of P I . We first construct, using N , an abstraction I of interference sets from P(I), as presented in Fig. 11. It is simply a partitioning of abstract sets of real values with respect to threads and variables: I def = (T × V) → N , together with pointwise concretization γ I , join ∪ I , and widening I . Note that I is not isomorphic to a non-relational domain on a set T × V of variables. Indeed, the former abstracts (T × V) → P(R) P(T × V × R) = P(I), while the latter would abstract P((T × V) → R). In particular, the former can express abstract states where the value set of some but not all variables is empty, while ⊥ N elements in the later coalesce to a single element representing ∅. We then construct an abstraction D I of the semantic domain D I , as presented in Fig. 12. An element of D I is a triple (R , Ω, I ) composed of an abstraction R ∈ E of environments, a set Ω ⊆ L of errors, and an abstraction I ∈ I of interferences. The concretization γ, join ∪ , and widening are defined pointwise.

N (abstract sets of reals) γ N : N → P(R) (concretization function) ⊥ N ∈ N (abstract empty set) s.t. γ N (⊥ N ) = ∅ ∪ N : (N × N ) → N (abstract join) s.t. γ N (V ∪ N W ) ⊇ γ N (V ) ∪ γ N (W ) N : (N × N ) → N (widening) s.t. γ N (V N W ) ⊇ γ N (V ) ∪ γ N (W ) and ∀(W i ) i∈N : the sequence V 0 = W 0 , V i+1 = V i N W i+1 reaches a fixpoint V k = V k+1 for some k ∈ N get : (V × E ) → N (variable extraction) s.t. γ N (get(X, R )) ⊇ { ρ(X) | ρ ∈ γ E (R ) } as-expr : (N \ {⊥ N }) → expr (conversion to expression) s.t. ∀ρ : let (V, -) = E as-expr (V ) ρ in V ⊇ γ N (V )
I def = (T × V) → N γ I : I → P(I) s.t. γ I (I ) def = { (t, X, v) | t ∈ T , X ∈ V, v ∈ γ N (I (t, X)) } ⊥ I def = λ(t, X) : ⊥ N I 1 ∪ I I 2 def = λ(t, X) : I 1 (t, X) ∪ N I 2 (t, X) I 1 I I 2 def = λ(t, X) : I 1 (t, X) N I 2 (t, X)
D I def = E × P(L) × I γ : D I → D I s.t. γ(R , Ω, I ) def = (γ E (R ), Ω, γ I (I )) (R 1 , Ω 1 , I 1 ) ∪ (R 2 , Ω 2 , I 2 ) def = (R 1 ∪ E R 2 , Ω 1 ∪ Ω 2 , I 1 ∪ I I 2 ) (R 1 , Ω 1 , I 1 ) (R 2 , Ω 2 , I 2 ) def = (R 1 E R 2 , Ω 1 ∪ Ω 2 , I 1 I I 2 )
Figure 12: Abstract semantic domain D I , derived from E and I .

The abstract semantics S I s, t of a statement s executed in a thread t ∈ T should be a function from D I to D I obeying the soundness condition:

(S I s, t • γ)(R , Ω, I ) I (γ • S I s, t )(R , Ω, I )
i.e., the abstract function over-approximates the sets of environments, errors, and interferences. Such a function is defined in a generic way in Fig. 13. The semantics of assignments and guards with interference is defined based on their non-interference semantics S s , provided as part of the abstract domain E . In both cases, the expression e to assign or test is first modified to take interferences into account, using the apply function. This function takes as arguments a thread t ∈ T , an abstract environment R ∈ E , an abstract interference I ∈ I , and an expression e. It first collects, for each variable Y ∈ V, the relevant interferences V Y ∈ N from I , i.e., concerning the variable Y and threads t = t. If the interference for Y is empty, ⊥ N , the occurrences of Y in e are kept unmodified. If it is not empty, then the occurrences of Y are replaced with a constant expression encompassing all the possible values that can be read from Y , from either the interferences or the environments γ E (R ). Additionally, the semantics of an assignment X ← e enriches I with new interferences corresponding to the values of X after the assignment. The semantics of non-primitive statements is identical to the interference-free case of Fig. 6.

Finally, an abstraction of the interference fixpoint (3.4) is computed by iteration on abstract interferences, using the widening I to ensure termination, which provides the abstract semantics P I of our program:

P I def = Ω, where (Ω, -) def = lim λ(Ω, I ) : let ∀t ∈ T : (-, Ω t , I t ) = S I body t , t (E 0 , Ω, I ) in ( { Ω t | t ∈ T }, I I I { I t | t ∈ T }) (3.6)
where lim F denotes the limit of the iterates of F starting from (∅, ⊥ I ). The following theorem states the soundness of the analysis:

Theorem 3.3. P I ⊆ P I .

Proof. In Appendix A.6.

The obtained analysis remains flow-sensitive and can be relational within each thread, provided that E is relational. However, interferences are abstracted in a flow-insensitive and non-relational way. This was already the case for the concrete interferences in P I and it is not related to the choice of abstract domains. The analysis is expressed as an outer iteration that completely re-analyzes each thread until the abstract interferences stabilize. Thus, it can be implemented easily on top of an existing non-parallel analyzer. Compared

S I s, t : D I → D I S I X ← e, t (R , Ω, I ) def = let (R , Ω ) = S X ← apply(t, R , I , e) (R , Ω) in (R , Ω , I [(t, X) → I (t, X) ∪ N get(X, R )]) S I e 0?, t (R , Ω, I ) def = let (R , Ω ) = S apply(t, R , I , e) 0? (R , Ω) in (R , Ω , I ) S I if e 0 then s, t (R , Ω, I ) def = (S I s, t • S I e 0?, t )(R , Ω, I ) ∪ S I e 0?, t (R , Ω, I ) S I while e 0 do s, t (R , Ω, I ) def = S I e 0?, t (lim λX : X ((R , Ω, I ) ∪ (S I s, t • S I e 0?, t )X )) S I s 1 ; s 2 , t (R , Ω, I ) def = (S I s 2 , t • S I s 1 , t )(R , Ω, I )
where:

apply(t, R , I , e) def = let ∀Y ∈ V : V Y = ∪ N { I (t , Y ) | t = t } in let ∀Y ∈ V : e Y = Y if V Y = ⊥ N as-expr (V Y ∪ N get(Y, R )) if V Y = ⊥ N in e[∀Y ∈ V : Y → e Y ]
Figure 13: Abstract semantics of statements with interference.

to a non-parallel program analysis, the cost is multiplied by the number of outer iterations required to stabilize interferences. Thankfully, our preliminary experimental results suggest that this number remains very low in practice -5 for our benchmark in Sec. 5. In any case, the overall cost is not related to the (combinatorial) number of possible interleavings, but rather to the amount of abstract interferences I , i.e., of actual communications between the threads. It is thus always possible to speed up the convergence of interferences or, conversely, improve the precision at the expense of speed, by adapting the widening N .

In this article, we focus on analyzing systems composed of a fixed, finite number of threads. The finiteness of T is necessary for the computation of P I in (3.6) to be effective. However, it is actually possible to relax this hypothesis and allow an unbounded number of instances of some threads to run in parallel. For this, it is sufficient to consider selfinterferences, i.e., replace the condition t = t in the definition E I X (t, ρ, I) in Fig. 7 (for the concrete semantics) and apply(t, R , I , e) in Fig. 13 (for the abstract semantics) with t = t ∨ t ∈ T , where T ⊆ T denotes the subset of threads that can have several instances. The resulting analysis is necessarily uniform, i.e., it cannot distinguish different instances of the same thread nor express properties about the number of running instances -it is abstracted statically in a domain of two values: "one" (t / ∈ T ) and "two or more" (t ∈ T ). In order to analyze actual programs spawning an unbounded number of threads, a non-uniform analysis (such as performed by Feret [START_REF] Feret | Occurrence counting analysis for the pi-calculus[END_REF] in the context of the π-calculus) may be necessary to achieve a sufficient precision, but this is not the purpose of the present article.

3.4. Weakly Consistent Memory Semantics P * . We now review the various parallel semantics we proposed in the preceding sections and discuss their adequacy to describe actual models of parallel executions.

It appears that our first semantics, the concrete interleaving semantics P * of Sec. 3.1, while simple, is not realistic. A first issue is that, as noted by Reynolds in [START_REF] Reynolds | Toward a grainless semantics for shared-variable concurrency[END_REF], such a semantics requires choosing a level of granularity, i.e., some basic set of operations that are assumed to be atomic and cannot be interrupted by another thread. In our case, we assumed assignments and guards (i.e., primitive statements) to be atomic. In contrast, an actual system may schedule a thread within an assignment and cause, for instance, x to be 1 at the end of the program in Fig. 9(b) instead of the expected value 2. A second issue, noted by Lamport in [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF], is that the latency of loads and stores in a shared memory may break the sequential consistency in true multiprocessor systems: threads running on different processors may not always agree on the value of a shared variable. For instance, in the mutual exclusion algorithm of Fig. 9(a), the thread t 2 may still see the value 0 in flag1 even after the thread t 1 has entered its critical section, causing t 2 to also enter its critical section, as the effect of the assignment flag1 ← 1 is propagated asynchronously and takes some time to be acknowledged by t 2 . Moreover, Lamport noted in [START_REF] Lamport | How to make a multiprocessor computer that correctly executes multiprocess programs[END_REF] that reordering of independent loads and stores in one thread by the processor can also break sequential consistencyfor instance performing the load from flag2 before the store into flag1, instead of after, in the thread t 1 in Fig. 9(a). More recently, it has been observed by Manson et al. [START_REF] Manson | The Java memory model[END_REF] that optimizations in modern compilers have the same ill-effect, even on mono-processor systems: program transformations that are perfectly safe on a thread considered in isolation (for instance, reordering the independent assignment flag1 ← 1 and test flag2 = 0 in t 1 ) can cause non-sequentially-consistent behaviors to appear. In this section, we show that the interference semantics correctly handles these issues by proving that it is invariant under a "reasonable" class of program transformations. This is a consequence of its coarse, flow-insensitive and non-relational modeling of thread communications.

Acceptable program transformations of a thread are defined with respect to the pathbased semantics Π of Sec. 2.4. A transformation of a thread t is acceptable if it gives rise to a set π (t) ⊆ Π of control paths such that every path p ∈ π (t) can be obtained from a path p ∈ π(body t ) by a sequence of elementary transformations described below in Def. 3.4. Elementary transformations are denoted q q , where q and q are sequences of primitive statements. This notation indicates that any occurrence of q in a path of a thread can be replaced with q , whatever the context appearing before and after q. The transformations in Def. 3.4 try to account for widespread compiler and hardware optimizations, but are restricted to transformations that do not generate new errors nor new interferences. 2 This ensures that an interference-based analysis of the original program is sound with respect to the transformed one, which is formalized below in Thm. 3.5.

The elementary transformations of Def. 3.4 require some side-conditions to hold in order to be acceptable. They use the following notions. We say that a variable X ∈ V is fresh if it does not occur in any thread, and local if it occurs only in the currently transformed thread. We denote by s[e /e] the statement s where some, but not necessarily all, occurrences of the expression e may be changed into e . The set of variables appearing in the expression e is denoted var (e), while the set of variables modified by the statement s is 2 The environments at the end of the thread after transformations may be different, but this does not pose a problem as environments are not observable in our semantics: P * ⊆ L (3.3). lval (s). Thus, lval (X ← e) = {X} while lval (e 0?) = ∅. The predicate nonblock (e) holds if evaluating the expression e cannot block the program -as would, e.g., an expression with a definite run-time error, such as 1/0 -i.e., nonblock (e) def ⇐⇒ ∀ρ ∈ E : V ρ = ∅ where (V ρ , -) = E e ρ. We say that e is deterministic if, moreover, ∀ρ ∈ E : |V ρ | = 1. Finally, noerror (e) holds if evaluating e is always error-free, i.e., noerror (e) def ⇐⇒ ∀ρ ∈ E : Ω ρ = ∅ where (-, Ω ρ ) = E e ρ. We are now ready to state our transformations: Definition 3.4 (Elementary path transformations).

(1) Redundant store elimination: X ← e 1 • X ← e 2 X ← e 2 , when X / ∈ var (e 2 ) and nonblock (e 1 ).

(2) Identity store elimination: X ← X . (3) Reordering assignments: These simple rules, used in combination, allow modeling large classes of classic program transformations as well as distributed memories. Store latency can be simulated using rules 7 and 3. Breaking a statement into several ones is possible with rules 7 and 8. As a consequence, the rules can expose preemption points within statements, which makes primitive statements no longer atomic. Global optimizations, such as constant propagation and folding, can be achieved using rules 7 and 9. Rules 1-6 allow peephole optimizations. Additionally, transformations that do not change the set of control paths, such as loop unrolling, are naturally supported.

X 1 ← e 1 • X 2 ← e 2 X 2 ← e 2 • X 1 ← e 1 , when X 1 / ∈ var (e 2 ), X 2 / ∈ var (e 1 ), X 1 = X 2 ,
Given the set of transformed control paths π (t) for each thread t ∈ T , the set of transformed parallel control paths π * is defined, similarly to (3.2), as:

π * def = { p ∈ Π * | ∀t ∈ T : proj t (p) ∈ π (t) } (3.7)
and the semantics P * of the parallel program is, similarly to (3.3):

P * def = Ω, where (-, Ω) = Π * π * (E 0 , ∅) . (3.8)
Any original thread π(body t ) being a special case of transformed thread π (t) (considering the identity transformation), we have P * ⊆ P * . The following theorem extends Thm. 3.2 to transformed programs: Theorem 3.5. P * ⊆ P I .

3 The original expression simplification rule from [START_REF] Miné | Static analysis of run-time errors in embedded critical parallel C programs[END_REF] required a much stronger side-condition: EI e (t, ρ, I) EI e (t, ρ, I) for all ρ and I, which actually implied that e and e were variable-free. We propose here a more permissive side-condition allowing local variables to appear in e and e .

Proof. In Appendix A.7.

An immediate consequence of Thms. 3.3 and 3.5 is the soundness of the abstract semantics P I with respect to the concrete semantics of the transformed program P * , i.e., P * ⊆ P I . Note that, in general, P * = P I . The two semantics may coincide, as for instance in the program of Fig. 9(a). In that case: P * P * = P I . However, in the case of Fig. 9(b), y can take any positive value according to the interference semantics P I (as explained in Sec. 3.2), while the interleaving semantics after program transformation P * only allows the values 1 and 2; we have P * = P * P I . Theorem 3.5 holds for our "reasonable" collection of program transformations, but may not hold when considering other, "unreasonable" ones. For instance, in Fig. 9(a), flag1 ← 1 should not be replaced by a misguided prefetching optimizer with flag1 ← 42; flag1 ← 1 in thread t 1 . This would create a spurious interference causing the value 42 to be possibly seen by thread t 2 . If there is no other reason for t 2 to see the value 42, such as a previous or future assignment of 42 into flag1 by t 1 , it would create an execution outside those considered by the interference semantics and invalidate Thm. 3.5. Such "out-of-thin-air" values are explicitly forbidden by the Java semantics as described by Manson et al. [START_REF] Manson | The Java memory model[END_REF]. See also [START_REF] Saraswat | A theory of memory models[END_REF] for an in-depth discussion of out-of-thin-air values. Another example of invalid transformation is the reordering of assignments

X 1 ← e 1 • X 2 ← e 2
X 2 ← e 2 • X 1 ← e 1 when e 1 may block the program, e.g., due to a division by zero X 1 ← 1/0. Indeed, the transformed program could expose errors in e 2 that cannot occur in the original program because they are masked by the previous error in X 1 ← e 1 . This case is explicitly forbidden by the nonblock (e 1 ) side condition in Def. 3.4.(3). The proof in Appendix A.7 contains more examples of transformations that become invalid when side-conditions are not respected.

Definition 3.4 is not exhaustive. It could be extended with other "reasonable" transformations, and some restrictive side-conditions might be relaxed in future work without breaking Thm. 3.5. It is also possible to enrich Def. 3.4 with new transformations that do not respect Thm. 3.5 as is, and then adapt the interference semantics to retrieve a similar theorem. For instance, we could allow speculative stores of some special value, such as zero, which only requires adding an interference (t, X, 0) for each thread t and each variable X modified by t. As another example, we could consider some memory writes to be non-atomic, such as 64-bit writes on 32-bit computers, which requires adding interferences that expose partially assigned values.

Finally, it would be tempting to, dually, reduce the number of allowed program transformations, and enforce a stronger memory consistency. For instance, we could replace Def. 3.4 with a model of an actual multiprocessor, such as the intel x86 architecture model proposed by Sewell et al. in [START_REF] Sewell | x86-TSO: A rigorous and usable programmer's model for x86 multiprocessors[END_REF], which is far less permissive and thus ensures many more properties. We would obtain a more precise interleaving semantics P * , closer to the sequentially consistent one P * . However, this would not mechanically improve the result of our static analysis P I , as it is actually an abstraction of the concrete interference semantics P I , itself an incomplete abstraction of P * . Our choice of an interference semantics was not initially motivated by the modeling of weakly consistent memories (although this is an important side effect), but rather by the construction of an effective and efficient static analyzer. Effectively translating a refinement of the memory model at the level of an interference-based analysis without sacrificing the efficiency remains a challenging future work.

Multi-threaded Programs With a Real-Time Scheduler

We now extend the language and semantics of the preceding section with explicit synchronization primitives. These can be used to enforce mutual exclusion and construct critical sections, avoiding the pitfalls of weakly consistent memories. We also extend the semantics with a real-time scheduler taking thread priorities into account, which provides an alternate way of implementing synchronization. 4.1. Priorities and Synchronization Primitives. We first describe the syntactic additions to our language and introduce informally the change in semantics.

We denote by M a finite, fixed set of mutual exclusion locks, so-called mutexes. The original language of Fig. 2 is enriched with primitives to control mutexes and scheduling as follows:

stat ::= lock(m)

(mutex locking, m ∈ M) | unlock(m) (mutex unlocking, m ∈ M) | X ← islocked(m) (mutex testing, X ∈ V, m ∈ M) | yield (thread pause) (4.1)
The primitives lock(m) and unlock(m) respectively acquire and release the mutex m ∈ M. The primitive X ← islocked(m) is used to test the status of the mutex m: it stores 1 into X if m is acquired by some thread, and 0 if it is free. The primitive yield is used to voluntarily relinquish the control to the scheduler. The definition of control paths π(s) from (2.3) is extended by stating that π(s) def = {s} for these statements, i.e., they are primitive statements. We also assume that threads have fixed, distinct priorities. As only the ordering of priorities is significant, we denote threads in T simply by integers ranging from 1 to |T |, being understood that thread t has a strictly higher priority than thread t when t > t .

To keep our semantics simple, we assume that acquiring a mutex for a thread already owning it is a no-op, as well as releasing a mutex it does not hold. Our primitive mutexes can serve as the basis to implement more complex ones found in actual implementations. For instance, mutexes that generate a run-time error or return an error code when locked twice by the same thread can be implemented using an extra program variable for each mutex / thread pair that stores whether the thread has already locked that mutex. Likewise, recursive mutexes can be implemented by making these variables count the number of times each thread has locked each mutex. Finally, locking with a timeout can be modeled as a non-deterministic conditional that either locks the mutex, or yields and returns an error code.

Our scheduling model is that of real-time processes, used noticeably in embedded systems. Example operating systems using this model include those obeying the ARINC 653 standard [3] (used in avionics), as well as the real-time extension of the POSIX threads standard [START_REF]Portable operating system interface (POSIX) -Application program interface (API) amendment 2: Threads extension (C language). Technical report[END_REF]. Hard guarantees about the execution time of services, although an important feature of real-time systems, are not the purpose of this article as we abstract physical time away. We are interested in another feature: the strict interpretation of thread priorities when deciding which thread to schedule. More precisely: a thread that is not blocked waiting for some resource can never be preempted by a lower priority thread. This is unlike schedulers found in desktop computers (for instance, vanilla POSIX threads [START_REF]Portable operating system interface (POSIX) -Application program interface (API) amendment 2: Threads extension (C language). Technical report[END_REF] without the real-time extension) where even lower priority threads always get to run, preempting low priority high priority lock(m); higher priority ones if necessary. Moreover, we consider in this section that only a single thread can execute at a given time -this was not required in Sec. 3. This is the case, for instance, when all the threads share a single processor. In this model, the unblocked thread with the highest priority is always the only one to run. All threads start unblocked and may block, either by locking a mutex that is already locked by another thread, or by yielding voluntarily, which allows lower priority threads to run. Yielding denotes blocking for a non-deterministic amount of time, which is useful to model timers of arbitrary duration and waiting for external resources. A lower priority thread can be preempted when unlocking a mutex if a higher priority thread is waiting for this mutex. It can also be preempted at any point by a yielding higher priority thread that wakes up non-deterministically. Thus, a preempted thread can be made to wait at an arbitrary program point, and not necessarily at a synchronization statement. The scheduling is dynamic and the number of possible thread interleavings authorized by the scheduler remains very large, despite being controlled by strict priorities. This scheduling model is precise enough to take into account fine mutual exclusion properties that would not hold if we considered arbitrary preemption or true parallel executions on concurrent processors. For instance, in Fig. 14, the high priority thread avoids a call to lock by testing with islocked whether the low priority thread acquired the lock and, if not, executes its critical section and modifies Y and Z, confident that the low priority thread cannot execute and enter its critical section before the high priority thread explicitly yields.

X ← islocked(m); Y ← 1; if X = 0 then Z ← 1; Z ← 2; T ← Y -Z; Y ← 2; unlock(m) yield

Concrete Scheduled Interleaving

Semantics P H . We now refine the various semantics of Sec. 3 to take scheduling into account, starting with the concrete interleaving semantics P * of Sec. 3.1. In this case, it is sufficient to redefine the semantics of primitive statements. This new semantics will, in particular, exclude interleavings that do not respect mutual exclusion or priorities, and thus, we observe fewer behaviors. This is materialized by the dotted ⊆ arrow in Fig. 1 between P * and the refined semantics P H we are about to present. 4We define a domain of scheduler states H as follows:

H def = (T → { ready, yield , wait(m) | m ∈ M }) × (T → P(M)) . (4.2)
A scheduler state (b, l) ∈ H is a pair, where the function b associates to each thread whether it is ready (i.e., it is not blocked, and runs if no higher priority thread is also ready), yielding (i.e., it is blocked at a yield statement), or waiting for some mutex m (i.e., it is blocked at a lock(m) statement). The function l associates to each thread the set of all the mutexes it holds. A program state is now a pair ((b, l), ρ) composed of a scheduler state (b, l) ∈ H and an environment ρ ∈ E. The semantic domain D def = P(E) × P(L) from (2.1) is thus replaced with D H defined as:

D H def = P(H × E) × P(L) (4.3)
with the associated pairwise join H .

The semantics S H s, t of a primitive statement s executed by a thread t ∈ T is described in Fig. 15. It is decomposed into three steps: enabled t , S † H s, t , and sched , the first and the last steps being independent from the choice of statement s. Firstly, the function enabled t filters states to keep only those where the thread t can actually run, i.e., t is the highest priority thread which is ready. Secondly, the function S † H s, t handles the statement-specific semantics. For yield, lock, and unlock statements, this consists in updating the scheduler part of each state. For lock statements, the thread enters a wait state until the mutex is available. Actually acquiring the mutex is performed by the following sched step if the mutex is immediately available, and by a later sched step following the unlocking of the mutex by its owner thread otherwise. The islocked statement updates each environment according to its paired scheduler state. The other primitive statements, assignments and guards, are not related to scheduling; their semantics is defined by applying the regular, mono-threaded semantics S s from Fig. 4 to the environment part, leaving the scheduler state unchanged. Thirdly, the function sched updates the scheduler state by waking up yielding threads non-deterministically, and giving any newly available mutex to the highest priority thread waiting for it, if any.

The semantics Π H P ∈ D H H -→ D H of a set P ⊆ Π * of parallel control paths then becomes, similarly to (3.1):

Π H P (R, Ω) def = H { (S H s n , t n • • • • • S H s 1 , t 1 )(R, Ω) | (s 1 , t 1 ) • . . . • (s n , t n ) ∈ P } (4.4)
and the semantics P H of the program is, similarly to (3.3):

P H def = Ω, where (-, Ω) = Π H π * ({h 0 } × E 0 , ∅) (4.5)
where π * is the set of parallel control paths of the program, defined in (3.2), and h 0 def = (λt : ready, λt : ∅) denotes the initial scheduler state (all the threads are ready and hold no mutex). As in Sec. 3.1, many parallel control paths in π * are unfeasible, i.e., return an empty set of environments, some of which are now ruled out by the enabled t function because they do not obey the real-time scheduling policy or do not ensure the mutual exclusion enforced by locks. Nevertheless, errors from a feasible prefix of an unfeasible path are still taken into account. This includes, in particular, the errors that occur before a dead-lock. 4.3. Scheduled Weakly Consistent Memory Semantics P H . As was the case for the interleaving semantics without a scheduler (Sec. 3.1), the scheduled interleaving semantics does not take into account the effect of a weakly consistent memory. Recall that a lack of memory consistency can be caused by the underlying hardware memory model of a multiprocessor, by compiler optimisations, or by non-atomic primitive statements. While we can disregard the hardware issues when considering mono-processor systems (i.e., everywhere in

S H s, t : D H H -→ D H S H s, t def = sched • S †
H s, t • enabled t where:

enabled t (R, Ω) def = ({ ((b, l), ρ) ∈ R | b(t) = ready ∧∀t > t : b(t ) = ready }, Ω) S † H yield, t (R, Ω) def = ({ ((b[t → yield ], l), ρ) | ((b, l), ρ) ∈ R }, Ω) S † H lock(m), t (R, Ω) def = ({ ((b[t → wait(m)], l), ρ) | ((b, l), ρ) ∈ R }, Ω) S † H unlock(m), t (R, Ω) def = ({ ((b, l[t → l(t) \ {m}]), ρ) | ((b, l), ρ) ∈ R }, Ω) S † H X ← islocked(m), t (R, Ω) def = ({ ((b, l), ρ[X → 0]) | ((b, l), ρ) ∈ R, ∀t ∈ T : m / ∈ l(t ) } ∪ { ((b, l), ρ[X → 1]) | ((b, l), ρ) ∈ R, ∃t ∈ T : m ∈ l(t ) }, Ω)
for all other primitive statements s ∈ { X ← e, e 0? } :

S † H s, t (R, Ω) def = ({ ((b, l), ρ ) | ∃ρ : ((b, l), ρ) ∈ R, (R , -) = S s ({ρ}, Ω), ρ ∈ R }, Ω ) where (-, Ω ) = S s ({ ρ | (-, ρ) ∈ R }, Ω) sched (R, Ω) def = ({ ((b , l ), ρ) | ((b, l), ρ) ∈ R }, Ω) s.t. ∀t : if b(t) = wait(m) ∧ (m ∈ l(t) ∨ (∀t : m / ∈ l(t ) ∧ ∀t > t : b(t ) = wait(m))) then b (t) = ready ∧ l (t) = l(t) ∪ {m} else l (t) = l(t) ∧ (b (t) = b(t) ∨ (b (t) = ready ∧ b(t) = yield ))
Figure 15: Concrete semantics of primitive statements with a scheduler.

Sec. 4 except Sec. 4.4.5) the other issues remain, and so, we must consider their interaction with the scheduler. Thus, we now briefly present a weakly consistent memory semantics for programs with a scheduler. The interference semantics designed in Secs. 4.4 and 4.5 will be sound with respect to this semantics.

In addition to restricting the interleaving of threads, synchronization primitives also have an effect when considering weakly consistent memory semantics: they enforce some form of sequential consistency at a coarse granularity level. More precisely, the compiler and processor handle synchronization statements specially, introducing the necessary flushes into memory and register reloads, and refraining from optimizing across them.

Recall that the weakly consistent semantics P * of Sec. 3.4 is based on the interleaving semantics P * of Sec. 3.1 applied to transformed threads π (t), which are obtained by transforming the paths in π(body t ) using elementary path transformations q q from Def. 3.4. To take synchronization into account, we use the same definition of transformed threads π (t), but restrict it to transformations q q that do not contain any synchronization primitive. For instance, we forbid the application of sub-expression elimination (Def. 3.4.( 8)) on the following path: lock(m) • Y ← e X ← e • lock(m) • Y ← X. However, if q and q do not contain any synchronization primitive, and q q , then it is legal to replace q with q in a path containing synchronization primitives before and after q. For instance, the transformation lock(m) acceptable. The scheduled weakly consistent memory semantics is then, based on (4.5):

• Y ← e lock(m) • X ← e • Y ← X is unlock(m) lock(m) unlock(m) lock(m) W W R W R thread 1 thread 2 (a) Well synchronized communication. W W lock(m) unlock(m) lock(m) unlock(m) R W R R W thread 2 thread 1 (b) Weakly consistent communications.
P H def = Ω, where (-, Ω) = Π H π * ({h 0 } × E 0 , ∅) (4.6)
where π * is defined, as before (3.7), as the interleavings of control paths from all π (t), t ∈ T .

4.4. Concrete Scheduled Interference Semantics P C . We now provide a structured version P C of the scheduled interleaving semantics P H . Similarly to the interference abstraction P I from Sec. 3.2 of the non-scheduled interleaving semantics P * , it is based on a notion of interference, it is sound with respect to both the interleaving semantics P H and its weakly consistent version P H , but it is not complete with respect to either of them. The main changes with respect to the interference abstraction P I are: a notion of scheduler configuration (recording some information about the state of mutexes), a partitioning of interferences and environments with respect to configurations, and a distinction between well synchronized thread communications and data-races. As our semantics is rather complex, we first present it graphically on examples before describing it in formal terms.

4.4.1. Interferences. In the non-scheduled semantics P I (Sec. 3.2), any interference (t, X, v), i.e., any write by a thread t of a value v into a variable X, could influence any read from the same variable X in another thread t = t. While this is also a sound abstraction of the semantics with a scheduler, the precision can be improved by refining our notion of interference and exploiting mutual exclusion properties enforced by the scheduler.

Good programming practice dictates that all read and write accesses to a given shared variable should be protected by a common mutex. This is exemplified in Fig. 16.(a) where W and R denote respectively a write to and a read from a variable X, and all reads and writes are protected by a mutex m. In this example, thread 1 writes twice to X while holding m. Thus, when thread 2 locks m and reads X, it can see the second value written by thread 1, but never the first one, which is necessarily overwritten before thread 2 acquires m. Likewise, after thread 2 locks m and overwrites X, while it still holds m it can only read back the value it has written and not any value written by thread 1. Thus, a single interference from thread 1 can effect thread 2, and at only one read position; we call this read / write pair a "well synchronized communication." Well synchronized communications are flow-sensitive (the order of writes and reads matters), and so, differ significantly from the interferences of Sec. 3.2. In practice, we model such communications by recording at the point unlock(m) in thread 1 the current value of all the variables that are modified while m is locked, and import these values in the environments at the point lock(m) in thread 2.

Accesses are not always protected by mutexes, though. Consider, for instance, the example in Fig. 16.(b), where X may additionally be modified by thread 1 and read by thread 2 outside the critical sections defined by mutex m. In addition to the well synchronized communication of Fig. 16.(a), which is omitted for clarity in Fig. 16.(b), we consider that a write from thread 1 effects a read from thread 2 if either operation is performed while m is not locked. These read / write pairs correspond to data-races, and neither the compiler nor the hardware is required to enforce memory consistency. We call these pairs "weakly consistent communications." In practice, these are handled in a way similar to the interferences in Sec. 3.2: the values thread 1 can write into X are remembered in a flow-insensitive interference set, and the semantics of expressions is modified so that, when reading X in thread 2, either the thread's value for X or a value from the interference set is used. We also remember the set of mutexes that threads hold during each read and each write, so that we can discard communications that cannot occur due to mutual exclusion. For instance, in Fig. 16.(b), there is no communication of any kind between the first write in thread 1 and the second read in thread 2. The example also shows that well synchronized and weakly consistent communications can mix freely: there is no weakly consistent communication between the second write in thread 1 and the second read in thread 2 due to mutual exclusion (both threads hold the mutex m); however, there is a well synchronized communication -shown in Fig. 16.(a).

Figure 17 illustrates the communications in the case of several mutexes: m1 and m2. In Fig. 17.(a), weakly consistent communications only occur between write / read pairs when the involved threads have not locked a common mutex. For instance, the first write by thread 1 is tagged with the set of locked mutexes {m1}, and so, can only influence the first read by thread 2 (tagged with ∅) and not the following two (tagged respectively with {m1} and {m1, m2}). Likewise, the second write, tagged with {m1, m2}, only influences the first read. However, the third write, tagged with only {m2}, influences the two first reads (thread 2 does not hold the mutex m2 there). In Fig. 17.(b), well synchronized communications import, as before, at a lock of mutex m1 (resp. m2) in thread 2, the last value written by thread 1 before unlocking the same mutex m1 (resp. m2). The well synchronized communication in Fig. 17.(c) is more interesting. In that case, thread 1 unlocks m2 before m1, instead of after. As expected, when thread 2 locks m1, it imports the last (third) value written by thread 1, just before unlocking m1. We note, however, that the second write in thread 1 does not influence thread 2 while thread 2 holds mutex m1, as the value is always over-written by thread 1 before unlocking m1. We model this by importing, when locking a mutex m in thread 2, only the values written by thread 1 while it does not hold a common mutex (in addition to m) with thread 2. Thus, when locking m2 while still holding the mutex m1, thread 2 does not import the second value written by thread 1 because thread 1 also holds m1 during this write. 4.4.2. Interference partitioning. To differentiate between well synchronized and weakly consistent communications, and to avoid considering communications between parts of threads that are in mutual exclusion, we partition interferences with respect to a thread-local view of scheduler configurations. The (finite) set C of configurations is defined as:

C def = P(M) × P(M) × { weak , sync(m) | m ∈ M } . (4.7)
In a configuration (l, u, s) ∈ C, the first component l ⊆ M denotes the exact set of mutexes locked by the thread creating the interference, which is useful to decide which reads will be affected by the interference. The second component u ⊆ M denotes a set of mutexes that are known to be locked by no thread (either current or not). This information is inferred by the semantics of islocked statements and can be exploited to detect extra mutual exclusion properties that further limit the set of reads affected by an interference (as in the example in Fig. 14). The last component, s, allows distinguishing between weakly consistent and well synchronized communications: weak denotes an interference that generates weakly consistent communications, while sync(m) denotes an interference that generates well synchronized communications for critical sections protected by the mutex m. These two kinds of interferences are naturally called, respectively, weakly consistent and well synchronized interferences. The partitioned domain of interferences is then:

I def = T × C × V × R (4.8)
which enriches the definition of I from Sec. 3.2 with a scheduler configuration in C. The interference (t, c, X, v) ∈ I indicates that the thread t ∈ T can write the value v ∈ R into the variable X ∈ V and the scheduler is in the configuration c ∈ C at the time of the write.

4.4.3. Environment partitioning. When computing program states in our semantics, environments are also partitioned with respect to scheduler configurations in order to track some information on the current state of mutexes. Thus, our program states associate an environment ρ ∈ E and a configuration in (l, u, s) ∈ C, where the configuration (l, u, s) indicates the set of mutexes l held by the thread in that state, as well as the set of mutexes u that are known to be held by no thread; the s component is not used and always set by convention to weak . The semantic domain is now:

D C def = P(C × E) × P(L) × P(I) (4.9)
partially ordered by pointwise set inclusion. We denote by C the associated pointwise join.

While regular statements (such as assignments and tests) update the environment part of each state, synchronization primitives update the scheduler part of the state. The use of pairs of environments and scheduler configurations allows representing relationships between the value of a variable and the state of a mutex, which is important for the precise modeling of the islocked primitive in code similar to that of Fig. 14. For instance, after the statement X ← islocked(m), all states ((l, u, s), ρ) satisfy ρ(X) = 0 =⇒ m ∈ u. Thus, when the high thread enters the "then" branch of the subsequent X = 0 test, we know that m is not locked by any thread and we can disregard the interferences generated by the low thread while holding m. The semantics E C e (t, c, ρ, I) of an expression e is presented in Fig. 18. It is similar to the non-scheduled semantics E I e (t, ρ, I) of Fig. 7, except that it has an extra argument: the current configuration c ∈ C (4.7) of the thread evaluating the expression. The other arguments are: the thread t ∈ T evaluating the expression, the environment ρ ∈ E in which it is evaluated, and a set I ⊆ I (4.8) of interferences from the whole program. Interferences are applied when reading a variable E C X . Only weakly consistent interferences are handled in expressions -well synchronized interferences are handled in the semantics of synchronization primitives, presented below. Moreover, we consider only interferences with configurations that are not in mutual exclusion with the current configuration c. Mutual exclusion is enforced by the predicate intf , which states that, in two scheduler configurations (l, u, weak ) and (l , u , weak ) for distinct threads, no mutex can be locked by both threads (l ∩ l = ∅), and no thread can lock a mutex which is assumed to be free by the other one (l ∩ u = l ∩ u = ∅). The semantics of other expression constructs remains the same, passing recursively the arguments t, c, and I unused and unchanged.

E C e : (T × C × E × P(I)) → (P(R) × P(L)) E C X (t, c, ρ, I) def = ({ ρ(X) } ∪ { v | ∃(t , c , X, v) ∈ I : t = t ∧ intf (c, c ) }, ∅) E C [c 1 , c 2 ] (t, c, ρ, I) def = ({ c ∈ R | c 1 ≤ c ≤ c 2 }, ∅) E C -e (t, c, ρ, I) def = let (V, Ω) = E C e (t, c, ρ, I) in ({ -x | x ∈ V }, Ω) E C e 1 e 2 (t, c, ρ, I) def = let (V 1 , Ω 1 ) = E C e 1 (t, c, ρ, I) in let (V 2 , Ω 2 ) = E C e 2 (t, c, ρ, I) in ({ x 1 x 2 | x 1 ∈ V 1 , x 2 ∈ V 2 , = / ∨ x 2 = 0 }, Ω 1 ∪ Ω 2 ∪ { | = / ∧ 0 ∈ V 2 }) where ∈ { +, -, ×, / } where: intf ((l, u, s), (l , u , s )) def ⇐⇒ l ∩ l = u ∩ l = u ∩ l = ∅ ∧ s = s = weak
We now turn to the semantics S C s, t (R, Ω, I) of a statement s executed by a thread t, which is defined in Fig. 19. It takes as first argument a set R of states which are now pairs consisting of an environment ρ ∈ E and a scheduler configuration c ∈ C, i.e., R ⊆ C × E. The other arguments are, as in the non-scheduled semantics of Fig. 8, a set of run-time errors Ω ⊆ L to enrich, and a set of interferences I ⊆ I to use and enrich. The semantics of assignments and tests in Fig. 19 is similar to the non-scheduled case (Fig. 8). The scheduler configuration associated with each input environment is simply passed as argument to the expression semantics E C in order to select precisely which weakly relational interferences to apply (through intf ), but it is otherwise left unmodified in the output. Additionally, assignments X ← e generate weakly consistent interferences, which store in I the current thread t and the scheduler configuration c of its state, in addition to the modified variable X and its new value.

S C s, t : D C C -→ D C S C X ← e, t (R, Ω, I) def = (∅, Ω, I) C C (c,ρ)∈R let (V, Ω ) = E C e (t, c, ρ, I) in ({ (c, ρ[X → v]) | v ∈ V }, Ω , { (t, c, X, v) | v ∈ V }) S C e 0?, t (R, Ω, I) def = (∅, Ω, I) C C (c,ρ)∈R let (V, Ω ) = E C e (t, c, ρ, I) in ({ (c, ρ) | ∃v ∈ V : v 0 }, Ω , ∅) S C if e 0 then s, t (R, Ω, I) def = (S C s, t • S C e 0?, t )(R, Ω, I) C S C e 0?, t (R, Ω, I) S C while e 0 do s, t (R, Ω, I) def = S C e 0?, t (lfp λX : (R, Ω, I) C (S C s, t • S C e 0?, t )X) S C s 1 ; s 2 , t (R, Ω, I) def = (S C s 2 , t • S C s 1 , t )(R, Ω, I) S C lock(m), t (R, Ω, I) def = ({ ((l ∪ {m}, ∅, s), ρ ) | ((l, -, s), ρ) ∈ R, ρ ∈ in(t, l, ∅, m, ρ, I) }, Ω, I ∪ { out(t, l, ∅, m , ρ, I) | ∃u : ((l, u, -), ρ) ∈ R ∧ m ∈ u }) S C unlock(m), t (R, Ω, I) def = ({ ((l \ {m}, u, s), ρ) | ((l, u, s), ρ) ∈ R }, Ω, I ∪ { out(t, l \ {m}, u, m, ρ, I) | ((l, u, -), ρ) ∈ R }) S C yield, t (R, Ω, I) def = ({ ((l, ∅, s), ρ) | ((l, -, s), ρ) ∈ R }, Ω, I ∪ { out(t, l, ∅, m , ρ, I) | ∃u : ((l, u, -), ρ) ∈ R ∧ m ∈ u }) S C X ← islocked(m), t (R, Ω, I) def = if no thread t > t locks m, then: ({ ((l, u ∪ {m}, s), ρ [X → 0]) | ((l, u, s), ρ) ∈ R, ρ ∈ in(t, l, u, m, ρ, I) } ∪ { ((l, u \ {m}, s), ρ[X → 1]) | ((l, u, s), ρ) ∈ R }, Ω, I ∪ { (t, c, X, v) | v ∈ {0, 1}, (c, -) ∈ R }) otherwise: S C X ← [0, 1], t (R, Ω, I)
where: in(t, l, u, m, ρ, I) The semantics of non-primitive statements remains the same as in previous semantics by structural induction on the syntax of statements (e.g., Fig. 8).

def = { ρ | ∀X ∈ V : ρ (X) = ρ(X) ∨ (∃t , l , u : (t , (l , u , sync(m)), X, ρ (X)) ∈ I ∧ t = t ∧ l ∩ l = l ∩ u = l ∩ u = ∅) } out(t, l, u, m, ρ, I) def = { (t, (l, u, sync(m)), X, ρ(X)) | ∃l : (t, (l , -, weak ), X, -) ∈ I ∧ m ∈ l }
The main point of note is thus the semantics of synchronization primitives. It updates the scheduler configuration and takes care of well synchronized interferences.

Let us explain first how the scheduler part (l, u, s) ∈ C of a state ((l, u, s), ρ) ∈ R is updated. Firstly, the set l of mutexes held by the current thread is updated by the primitives lock(m) and unlock(m) by respectively adding m to and removing m from l. Secondly, the set of mutexes u that are known to be free in the system is updated by X ← islocked(m). Generally, no information on the state of the mutex is known a priori. Each input state thus spawns two output states: one where m is free (m ∈ u), and one where m is not free (m / ∈ u). In the first state, X is set to 0 while, in the second state, it is set to 1. As a consequence, although the primitive cannot actually infer whether the mutex is free or not, it nevertheless keeps the relationship between the value of X and the fact that m is free. Inferring this relation is sufficient to analyze precisely the code in Fig. 14. It is important to note that the information in m ∈ u is transient as, when a context switch occurs, another thread t can run and lock m, thus invaliding the assumption by thread t that no thread has locked m. We distinguish two scenarios, depending on whether t has higher priority than t or not. When t < t, the thread t has lower priority and cannot preempt t at an arbitrary point due to the real-time nature of the scheduler. Instead, t must wait until t performs a blocking operation (i.e., calls a lock or yield primitive) to get the opportunity to lock m. This case is handled by having all our blocking primitives reset the u component to ∅. When t > t, the thread t can preempt t at arbitrary points, including just after the islocked primitive, and so, we can never safely assume that m ∈ u. If this scenario is possible, X ← islocked(m) is modeled as X ← [0, 1], without updating u. To decide which transfer function to use for islocked, we need to know the set of all mutexes than can be locked by each thread. It is quite easy to enrich our semantics to track this information but, as it is cumbersome, we did not include this in Fig. 19 -one way is to add a new component M : T → P(M) to the domain I of interferences, in which we remember the set of arguments m of each lock(m) encountered by each thread; then, we check that ∃t > t : m ∈ M (t ) before applying the precise transfer function for X ← islocked(m) in thread t.

We now discuss how synchronization primitives handle well synchronized interferences. We use two auxiliary functions, in(t, l, u, m, ρ, I) and out(t, l, u, m, ρ, I), that model respectively entering and exiting a critical section protected by a mutex m ∈ M in a thread t ∈ T . The arguments l, u ⊆ M reflect the scheduler configuration when the primitive is called, i.e., they are respectively the set of mutexes held by thread t and those assumed to be free in the system. The function out(t, l, u, m, ρ, I) collects a set of well synchronized interferences from an environment ρ ∈ E. These are constructed from the current value ρ(X) of the variables X that have been modified while the mutex m was held. Such information can be tracked precisely in the semantics by adding another component in C → P(V) to our program states R but, for the sake of simplicity, the semantics we present simply extracts this information from the interferences in I: we consider all the variables that have some weakly consistent interference by thread t in a configuration where it holds m (m ∈ l). This may actually over-approximate the set of variables we seek as it includes variables that have been modified in previous critical sections protected by the same mutex m, but not in the current critical section. 5 Given a variable X, the interference we store is then (t, (l, u, sync(m)), X, ρ(X)). The function in(t, l, u, m, ρ, I) applies well synchronized interferences from I to an environment ρ: it returns all the environments ρ that can be obtained 5 Our prototype performs the same over-approximation for the sake of keeping the analysis simple, and we did not find any practical occurrence where this resulted in a loss of precision. We explain this by remaking that critical sections delimited by the same mutex tend to protect the same set of modified variables.

from ρ by setting one or several variables to their interference value. It only considers well synchronized interferences with configuration sync(m) and from threads t = t. Moreover, it uses a test similar to that of intf to avoid applying interferences that cannot occur due to mutual exclusion, by comparing the current state of mutexes (l and u) to their state when the interference was stored.

The function pair in / out is actually used to implement two kinds of critical sections. A first kind stems from the use of lock(m) and unlock(m) statements, which naturally delimit a critical section protected by m. Additionally, whenever a mutex m is added to the u scheduler component by a primitive X ← islocked(m), we also enter a critical section protected by m. Thus, in is called for mutex m, and intf ensures that weakly consistent interferences where m is locked are no longer applied. Such critical sections end when m leaves u, that is, whenever the thread executes a blocking primitive: lock or yield. These primitives call out for every mutex currently in u, and reset u to ∅ in the program state. Proof. In Appendix A.8. 4.4.5. Multiprocessors and non-real-time systems. The only part of our semantics that exploits the fact that only one thread can execute at a given time is the semantics of X ← islocked(m). It assumes that, after the current thread has performed the test, the state of the mutex m cannot change until the current thread calls a blocking primitive (lock or yield) -unless some higher priority thread can also lock the mutex m. Thus, in order to obtain a semantics that is also sound for truly parallel or non-real-time systems, it is sufficient to interpret all statements X ← islocked(m) as X ← [0, 1].

While more general, this semantics is less precise when analyzing a system that is known to be mono-processor and real-time. For instance, this semantics cannot prove that the two threads in Fig. 14 are in mutual exclusion and that, as a result, T = 0 at the end of the program. It finds instead T ∈ { -1, 0, 1 }, which is less precise. As our target application (Sec. 5) is mono-processor and real-time, we will not discuss this more general but less precise semantics further. 4.4.6. Detecting data-races. In our semantics, data-races silently cause weakly consistent interferences but are otherwise not reported. It is easy to modify the semantics to output them. Write / write data-races can be directly extracted from the computed set of interferences I gathered by the least fixpoint in (4.10) as follows:

{ (t, t , X) ∈ T × T × V | ∃c, c : (t, c, X, -) ∈ I ∧ (t , c , X, -) ∈ I ∧ t = t ∧ intf (c, c ) }
is a set where each element (t, t , X) indicates that threads t and t may both write into X at the same time. Read / write data-races cannot be similarly extracted from I as the set of interferences does not remember which variables are read from, only which ones are written to. A simple solution is to instrument the semantics of expressions so that, during expression evaluation, it gathers the set of read variables that are affected by an interference. This is performed, for instance, by E CR presented in Fig. 20. This function has the same arguments as E C , except that no environment ρ is needed, and it outputs a set of data-races (t, t , X) instead of environments and errors.

E CR e : (T × C × P(I)) → P(T × T × V) E CR X (t, c, I) def = { (t, t , X) | ∃c : (t , c , X, -) ∈ I ∧ t = t ∧ intf (c, c ) } E CR [c 1 , c 2 ] (t, c, I) def = ∅ E CR -e (t,
E 0 : X = Y = 5 thread t 1 thread t 2 while 0 = 0 do while 0 = 0 do lock(m); lock(m); if X > 0 then if X < 10 then X ← X -1; X ← X + 1; Y ← Y -1; Y ← Y + 1; unlock(m) unlock(m)
4.4.7. Precision. The interference abstraction we use in P C is sound be not complete with respect to the interleaving-based semantics P H . In addition to the incompleteness already discussed in Sec. 3.2, some loss of precision comes from the handling of well synchronized accesses. A main limitation is that such accesses are handled in a non-relational way, hence P C cannot represent relations enforced at the boundary of critical sections but broken within, while P H can. For instance, in Fig. 14, we cannot prove that Y = Z holds outside critical sections, but only that Y, Z ∈ {1, 2}. This shows in particular that even programs without data-races have behaviors in P C outside the sequentially consistent ones. However, we can prove that the assignment into T is free from interference, and so, that T = 0. By contrast, the interference semantics P I of Sec. 3.2 ignores synchronization and would output T ∈ { -1, 0, 1 }, which is less precise. Figure 21 presents another example where the lack of relational interference results in a loss of precision. This example implements an abstract producer / consumer system, where a variable X counts the number of resources, thread t 1 consumes resources (X ← X -1) if available (X > 0), and thread t 2 generates resources (X ← X + 1) if there is still room for resources (X < 10). Our interference semantics can prove that X is always bounded in [0, 10]. However, it cannot provide an upper bound on the variable Y . Actually, Y is also c,X) bounded by [0, 10] as it mirrors X. Proving this would require inferring a relational lock invariant: X = Y . Finally, Fig. 22 presents an example where the lack of inter-thread flow sensitivity results in a loss of precision. In this example, the high priority thread always executes first, until it reaches yield, at which point it allows the lower priority thread to execute. To prove that the expression 1/(Y -1) does not perform an error, it is necessary to prove that it is executed before the low thread stores 1 into Y . Likewise, to prove that the expression 1/X does not perform an error in the low thread, it is necessary to prove that it is executed after the high thread stores 1 into X. With respect to flow sensitivity, our semantics is only able to express that an event is performed before another one within the same thread (intra-thread flow sensitivity) and that a thread communication between a pair of locations cannot occur (mutual exclusion), but it is not able to express that an event in a thread is performed before another one in another thread (inter-thread flow sensitivity). 4.5. Abstract Scheduled Interference Semantics P C . We now abstract the interference semantics with scheduler P C from the preceding section in order to construct an effective static analyzer. We reuse the ideas from the abstraction P I of P I in Sec. 3.3. The main difference is that we track precisely scheduler configurations in C (4.7), and we partition abstract environments and interferences with respect to them. As in Sec. 3.3, we assume that an abstract domain E of environment sets P(E) is given (with signature in Fig. 5), as well as an abstract domain N of real sets P(R) (with signature in Fig. 10). The abstract domain of interferences I , abstracting I (4.8), is obtained by partitioning N with respect to T and V, similarly to the interference domain of Fig. 11, but also C, as shown in Fig. 23. As V, T , and C are all finite, a map from T × C × V to N can indeed be represented in memory, and the join ∪ I and widening I can be computed pointwise. Moreover, abstract environments E are also partitioned with respect

E 0 : X = Y = 0 high thread low thread X ← 1; B ← 1/X; A ← 1/(Y -1); Y ← 1 yield
I def = (T × C × V) → N γ I : I → P(I) s.t. γ I (I ) def = { (t, c, X, v) | t ∈ T , c ∈ C, X ∈ V, v ∈ γ N (I (t, c, X)) } ⊥ I def = λ(t, c, X) : ⊥ N I 1 ∪ I I 2 def = λ(t, c, X) : I 1 (t, c, X) ∪ N I 2 (t,
I 1 I I 2 def = λ(t, c, X) : I 1 (t, c, X) N I 2 (t, c, X)
D C def = (C → E ) × P(L) × I γ : D C → D C s.t. γ(R , Ω, I ) def = ({ (c, ρ) | c ∈ C, ρ ∈ γ E (R (c)) }, Ω, γ I (I )) (R 1 , Ω 1 , I 1 ) ∪ (R 2 , Ω 2 , I 2 ) def = (λc : R 1 (c) ∪ E R 2 (c), Ω 1 ∪ Ω 2 , I 1 ∪ I I 2 ) (R 1 , Ω 1 , I 1 ) (R 2 , Ω 2 , I 2 ) def = (λc : R 1 (c) E R 2 (c), Ω 1 ∪ Ω 2 , I 1 I I 2 )
Figure 24: Abstract domain of statements D C , derived from E and I .

S C s, t : D C → D C S C X ← e, t (R , Ω, I ) def = let ∀c ∈ C : (R c , Ω c ) = S X ← apply(t, c, R , I , e) (R (c), Ω) in (λc : R c , c∈C Ω c , I [∀c ∈ C : (t, c, X) → I (t, c, X) ∪ N get(X, R c )]) S C e 0?, t (R , Ω, I ) def = let ∀c ∈ C : (R c , Ω c ) = S apply(t, c, R , I , e) 0? (R (c), Ω) in (λc : R c , c∈C Ω c , I ) S C if e 0 then s, t (R , Ω, I ) def = (S C s, t • S C e 0?, t )(R , Ω, I ) ∪ S C e 0?, t (R , Ω, I ) S C while e 0 do s, t (R , Ω, I ) def = S C e 0?, t (lim λX : X ((R , Ω, I ) ∪ (S C s, t • S C e 0?, t )X )) S C s 1 ; s 2 , t (R , Ω, I ) def = (S C s 2 , t • S C s 1 , t )(R , Ω, I )
where:

apply(t, c, R , I , e) def = let ∀Y ∈ V : V Y = ∪ N { I (t , c , Y ) | t = t ∧ intf (c, c ) } in let ∀Y ∈ V : e Y = Y if V Y = ⊥ N as-expr (V Y ∪ N get(Y, R (c))) if V Y = ⊥ N in e[∀Y ∈ V : Y → e Y ]
Figure 25: Abstract scheduled semantics of statements with interference.

to C. Hence, the abstract semantic domain D C abstracting D C (4.9) becomes:

D C def = (C → E ) × P(L) × I . (4.11)
It is presented in Fig. 24. Sound abstract transfer functions S C , derived from those in E (S ), are presented in Figs. 25-26. Assignments and tests in Fig. 25 are very similar to the non-scheduled case S I (Fig. 13) with two differences. Firstly, S is applied pointwise to each abstract environment R (c) ∈ E , c ∈ C. New interferences due to assignments are also considered pointwise. Secondly, the apply function now takes as extra argument a configuration c, and then only considers interferences from configurations c not in mutual exclusion with c. This is defined through

S C lock(m), t (R , Ω, I ) def = (λ(l, u, s) : E { in (t, l , ∅, m, R (l , u , s), I ) | l = l ∪ {m} ∧ u = ∅ ∧ u ⊆ M ∧ s = weak }, Ω, I ∪ I I { out (t, l, ∅, m , R (l, u, s), I ) | l, u ⊆ M ∧ m ∈ u ∧ s = weak }) S C unlock(m), t (R , Ω, I ) def = (λ(l, u, s) : E { R (l , u , s) | l = l \ {m} ∧ u = u ∧ s = weak }, Ω, I ∪ I I { out (t, l \ {m}, u, m, R (l, u, s), I ) | l, u ⊆ M ∧ s = weak }) S C yield, t (R , Ω, I ) def = (λ(l, u, s) : E { R (l , u , s) | l = l ∧ u = ∅ ∧ u ⊆ M ∧ s = weak }, Ω, I ∪ I I { out (t, l, ∅, m , R (l, u, s), I ) | l, u ⊆ M ∧ m ∈ u ∧ s = weak }) S C X ← islocked(m), t (R , Ω, I ) def = let (R , -, I ) = S C X ← [0, 1], t (R , Ω, I ) in if no thread t > t locks m, then: (λ(l, u, s) : E { let (V , -) = S X ← 0 (in (t, l , u , m, R (l , u , s), I ), ∅) if m ∈ u S X ← 1 (R (l , u , s), ∅) if m / ∈ u in V | l = l ∧ u \ {m} = u \ {m} ∧ s = weak }, Ω, I ) otherwise: (R , Ω, I )
where: the same function intf we used in the concrete semantics (Fig. 18). The semantics of nonprimitive statements is the same as for previous semantics, by structural induction on the syntax of statements. The semantics of synchronization primitives is presented in Fig. 26. It uses the functions in and out which abstract, respectively, the functions in and out presented in Fig. 19. As their concrete versions, in and out take as arguments a current thread t ∈ T , a mutex m ∈ M protecting a critical section, and sets of mutexes l, u ⊆ M describing the current scheduling configuration. Moreover, they take as arguments an abstract set of interferences I ∈ I instead of a concrete set, and an abstract set of environments V ∈ E instead of a single concrete one. The function out uses get (Fig. 10) to extract abstract sets of variable values from abstract environments and construct new abstract well synchronized interferences. The function in applies these interferences to an abstract environment by converting them to an expression (using as-expr ) and updating the value of variables (using an assignment in S ). Additionally, the semantics of synchronization primitives models updating the scheduler configuration from c = (l , u , weak ) to c = (l, u, weak ) by moving abstract environments from R (c ) into R (c); when partitions are collapsed, all the abstract environments mapped to the same configuration c are merged into R (c) using ∪ E . Finally, the abstract analysis P C computes a fixpoint with widening over abstract interferences, which is similar to (3.6):

in (t, l, u, m, V , I ) def = V ∪ E E { let X = I (t , (l , u , sync(m)), X) in let (V , -) = S X ← as-expr (X ) (V , ∅) in V | X ∈ V ∧ t = t ∧ l ∩ l = l ∩ u = l ∩ u = ∅ } out (t, l, u, m, V , I ) def = λ(t , c, X) :      get(X, V ) if t = t ∧ c = (l, u, sync(m)), ∃c = (l , -, weak ) : m ∈ l ∧ I (t, c , X) = ⊥ N ⊥ N otherwise
P C def = Ω, where (Ω, -) def = lim λ(Ω, I ) : let ∀t ∈ T : (-, Ω t , I t ) = S C body t , t (R 0 , Ω, I ) in ( { Ω t | t ∈ T }, I I I { I t | t ∈ T }) (4.12)
where the partitioned initial abstract environment R 0 ∈ C → E is defined as:

R 0 def = λc : E 0 if c = (∅, ∅, weak ) ⊥ E otherwise
The resulting analysis is sound:

Theorem 4.2. P C ⊆ P C .
Proof. In Appendix A.9.

Due to partitioning, P C is less efficient than P I . The abstract semantic functions for primitive statements, as well as the join ∪ and widening , are performed pointwise on all configurations c ∈ C. However, a clever implementation need not represent explicitly nor iterate over partitions mapping a configuration to an empty environment ⊥ E or an empty interference ⊥ N . The extra cost with respect to a non-scheduled analysis has thus a component that is linear in the number of non-⊥ E environment partitions and a component linear in the number of non-⊥ N interferences. Thankfully, partitioned environments are extremely sparse: Sec. 5 shows that, in practice, at most program points, R (c) = ⊥ E except for a few configurations (at most 4 in our benchmark). Partitioned interferences are less sparse (52 in our benchmark) because, being flow-insensitive, they accumulate information for configurations reachable from any program point. However, this is not problematic: as interferences are non-relational, a larger number of partitions can be stored and manipulated efficiently.

Thanks to partitioning, the precision of P C is much better than that of P I in the presence of locks and priorities. For instance, P C using the interval domain discovers that T = 0 in Fig. 14, while the analysis of Sec. 3.3 would only discover that T ∈ [-1, 1] due to spurious interferences from the high priority thread.

Experimental Results

We implemented the abstract analysis of Sec. 4.5 in Thésée, our prototype analyzer based on the Astrée static analyzer [START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF]. We first describe succinctly Astrée, then Thésée, and finally our target application and its analysis by Thésée.

5.1. The Astrée Analyzer. Astrée is a static analyzer that checks for run-time errors in embedded C programs. Astrée accepts a fairly large subset of C, excluding notably dynamic memory allocation and recursion, that are generally unused (or even forbidden) in embedded code. Moreover, Astrée does not analyze multi-threaded programs, which is the very issue we address in the present article.

The syntax and semantics assumed by Astrée are based on the C99 norm [START_REF]working group. C standard[END_REF], supplemented with the IEEE 754-1985 norm for floating-point arithmetics [START_REF]Standard for binary floating-point arithmetic[END_REF]. The C99 norm underspecifies many aspects of the semantics, leaving much leeway to compiler implementations, including random undocumented and unpredictable behaviors in case of an error such as an integer overflow. A strictly conforming program would rely only on the semantics defined in the norm. Few programs are strictly conforming; they rely instead on additional, platform-specific semantic hypotheses. This is especially true in the embedded software industry, where programs are designed for a specific, well-controlled platform, and not for portability. Thus, Astrée provides options to set platform-specific semantic features, such as the bit-size and byte-ordering of data-types, and the subsequent analysis is only sound with respect to these hypotheses. The run-time errors checked by Astrée are: overflows in integer arithmetics and casts, integer divisions by zero, invalid bit-shifts, infinities and Not a Number floating-point values (caused by overflows, divisions by zero, or invalid operations), out-of-bound array accesses, invalid pointer arithmetics or dereferences (including null, dangling, and misaligned pointers), and failure of user-defined assertions (specified in a syntax similar to the standard assert function).

Astrée takes as input the C source after preprocessing by a standard preprocessor and a configuration file describing the ranges of the program inputs (such as memorymapped sensors) if any. It then runs fully automatically and outputs a list of alarms corresponding to potential errors, and optionally program invariants for selected program points and variables. Astrée is sound in that it computes an over-approximation of all program traces, for all input scenarios. Moreover, the analysis continues even for erroneous program traces if the behavior after the error has a reasonable semantics. This is the case after integer overflows, for instance, using a wrap-around semantics, but it is not the case after dereferencing a dangling pointer, which has truly unpredictable results. In all cases, when there is no alarm, or when all the alarms can be proved by other means to be spurious, then the program is indeed proved free of run-time error.

Although Astrée accepts a large class of C programs, it cannot analyze most of them precisely and efficiently. It is specialized, by its choice of abstractions, towards control / command aerospace code, for which it gives good results. Thanks to a modular design, it can be adapted to other application domains by adding new abstractions. Actually, the initial specialization towards control / command avionic software [START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF] was achieved by incrementally adding new domains and refining existing ones until all false alarms could be removed on a target family of large control software from Airbus (up to 1 M lines) [START_REF] Delmas | Astrée: from research to industry[END_REF]. The resulting analyzer achieved the zero false alarm goal in a few hours of computation on a standard 2.66 GHz 64-bit intel server, and could be deployed in an industrial context [START_REF] Delmas | Astrée: from research to industry[END_REF]. This specialization can be continued with limited effort, at least for related application domains, as shown by our case study on space software [START_REF] Bouissou | Space software validation using abstract interpretation[END_REF]. Astrée is now a mature tool industrialized by AbsInt [START_REF] Absint | Angewandte Informatik. Astrée run-time error analyzer[END_REF].

Figure 27 presents the design of Astrée as a hierarchy of abstract domains -we ignore for now boldface domains, which are specific to Thésée. Actually, Astrée does not contain a single "super-domain" but rather many small or medium-sized domains that focus on a specific kind of properties each, possess a specific encoding of these properties and algorithms to manipulate them, and can be easily plugged in and out. One of the first domain included in Astrée was the simple interval domain [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] that expresses properties of the form X ∈ [a, b] for every machine integer and floating-point variable X ∈ V. The interval domain is key as it is scalable, hence it can be applied to all variables at all program points. Moreover, it is able to express sufficient conditions for the absence of many kinds of errors, e.g., overflows. Astrée also includes relational domains, such as the octagon domain [START_REF] Miné | The octagon abstract domain[END_REF] able to infer relations of the form ±X ± Y ≤ c. Such relations are necessary at a few locations, for instance to infer precise loop invariants, which then lead to tighter variable bounds. However, as the octagon domain is less scalable, it is used only on a few variables, selected automatically by a syntactic heuristic. Astrée also includes abstract domains specific to the target application domain, such as a domain to handle digital filtering featured in many control / command applications [START_REF] Feret | Static analysis of digital filters[END_REF]. The computations are performed in all the domains in parallel, and the domains communicate information through a partially reduced product [START_REF] Cousot | Combination of abstractions in the Astrée static analyzer[END_REF], so that they can improve each other in a controlled way -a fully reduced product, where all domains communicate all their finds, would not scale up. Additionally to numeric variables, the C language features pointers. Pointer values are modeled in the concrete semantics of Astrée as semi-symbolic pairs containing a variable name and an integer byteoffset. The pointer abstract domain is actually a functor that adds support for pointers to any (reduced product of) numerical abstract domain(s) by maintaining internally for each pointer a set of pointed-to variables, and delegating the abstraction of the offset to the underlying numerical domain(s) (associating a synthetic integer variable to each offset). Another functor, the memory domain, handles the decomposition of aggregate variables (such as arrays and structures) into simpler scalar variables. The decomposition is dynamic to account for the weak type system of C and the frequent reinterpretation of the same memory portions as values of different types (due to union types and to type-punning). Both functors are described in [START_REF] Miné | Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics[END_REF]. Finally, a trace partitioning domain [START_REF] Mauborgne | Trace partitioning in abstract interpretation based static analyzer[END_REF] adds a limited amount (for efficiency) of path-sensitivity by maintaining at the current control point several abstract states coming from execution traces with a different history (such as which branches of if statements were taken in the past). The computation in these domains is driven by an iterator that traverses the code by structural induction on its syntax, iterating loops with widening and stepping into functions to achieve a fully flow-and context-sensitive analysis.

More information and pointers about Astrée can be found in [START_REF] Bertrane | Static analysis and verification of aerospace software by abstract interpretation[END_REF]. 5.2. The Thésée Analyzer. Thésée is a prototype extension of Astrée that uses the abstract scheduled interference semantics of Sec. 4.5 to support the analysis of multi-threaded programs. Thésée checks for the same classes of run-time errors as Astrée. Additionally, it reports data-races, but ignores other parallel-related hazards, such as dead-locks and priority inversions, that are not described in our concrete semantics.

Thésée benefited directly from Astrée's numerous abstract domains and iteration strategies targeting embedded C code. Figure 27 presents the design of Thésée, where nonboldface domains are inherited from Astrée and boldface ones have been added.

Firstly, the memory domain has been modified to compute the abstract interferences generated by the currently analyzed thread and apply the interferences from other threads. We use the method of Fig. 25: the memory domain dynamically modifies expressions to include interferences explicitly (e.g., replacing variables with intervals) before passing the expressions to a stack of domains that are unaware of interferences. Interferences are themselves stored and manipulated by a specific domain which maintains abstract sets of values. Non-relational abstractions from Astrée, such as intervals but also abstract pointer values, are directly exploited to represent abstract interferences.

Secondly, a scheduler partitioning domain has been added. It maintains an abstraction of environments and of interferences for each abstract scheduled configuration live at the current program point. Then, for each configuration, it calls the underlying domain with the abstract environment associated to this configuration, as well as the abstract interferences that can effect this environment (i.e., a join of interferences from all configurations not in mutual exclusion with the current one). Additionally, the scheduler domain interprets directly all the instructions related to synchronization, which involves copying and joining abstract environments from different configurations, as described in Fig. 26.

Finally, we introduced an additional, parallel iterator driving the whole analysis. Following the execution model of the ARINC 653 specification, the parallel iterator first executes the main function as a regular single-threaded program and collects the set of resources (threads, synchronization objects) it creates. Then, as the program enters parallel mode, the iterator analyzes each thread in sequence, and keeps re-analyzing them until their interferences are stable (in parallel mode, no new thread may be created).

All these changes add up to approximately 10 K lines of code in the 100 K lines analyzer and did not require much structural change.

5.3. Analyzed Application. Thésée has been applied to the analysis of a large industrial program consisting of 1.7 M lines of unpreprocessed C code 6 and 15 threads, and running under an ARINC 653 real-time OS [3]. The analyzed program is quite complex as it mixes string formatting, list sorting, network protocols (e.g., TFTP), and automatically generated synchronous logic.

The application performs system calls that must be properly modeled by the analyzer. To keep the analyzer simple, Thésée implements natively only low-level primitives to declare and manipulate threads as well as simple mutexes having the semantics described in Sec. 4.1. However, ARINC 653 objects have a more complex semantics. The analyzed program is thus completed with a 2,500-line hand-written model of the ARINC 653 standard, designed specifically for the analysis with Thésée. It implements all the system calls in C extended with Thésée primitives. The model maps high-level ARINC 653 objects to lower-level Thésée ones. For instance, ARINC processes 7 have a name while Thésée threads only have an integer identifier, so, the model keeps track of the correspondence between names and identifiers in C arrays and implements system calls to look up names and identifiers. It also emulates the ARINC semantics using Thésée primitives. For instance, a lock with a timeout is modeled as a non-deterministic test that either actually locks the mutex, or yields and returns an error code without locking the mutex. An important feature of the program we analyze is that all potentially blocking calls have a finite timeout, so, by construction, no dead-lock nor unbounded priority inversion can occur. This explains why we did not focus on detecting statically these issues in the present article. 5.4. Analysis Results. At the time of writing, the analysis with Thésée of this application takes 27 h on our 2.66 GHz 64-bit intel server. An important result is that only 5 iterations are required to stabilize abstract interferences. Moreover, there is a maximum of 52 partitions for abstract interferences and 4 partitions at most for abstract environments, so that the analysis fits in the 32 GB of memory of our server. The analysis currently generates 2,136 alarms (slightly less than one alarm per 800 lines of unpreprocessed code).

These figures have evolved before and during the writing of this article, as we improved the analysis. Figure 28 presents the evolution of the number of alarms on a period of 18 months. As our improvement effort focuses on optimizing the analysis precision, we do not present the detailed evolution of the analysis time (it oscillates between 14 h and 28 h, 8 with a number of iterations between 4 and 7) nor the memory consumption (stable at a little under 30 GB). The number of alarms started at 12,257 alarms mid-2010, as reported in [7, § VI]. This high initial number can be explained by the lack of specialization of the analyzer: 6 After preprocessing and removal of comments, empty lines, and multiple definitions, the code is 2.1 M lines. The increase in size is due to the use of macros. 7 In the ARINC 653 [3] terminology, execution units in shared memory are called "processes"; they correspond to POSIX threads and not to POSIX processes [START_REF]Portable operating system interface (POSIX) -Application program interface (API) amendment 2: Threads extension (C language). Technical report[END_REF]. 8 Intuitively, adding domains and refining their precision degrades the efficiency. However, inferring tighter invariants can also reduce the number of loop iterations to reach a fixpoint, and so, improving the precision may actually lower the overall analysis time.

accumulates, in acc, elapsed time as counted by a clock variable (updated elsewhere), and we need to discover the invariant acc ≤ clock. This requires analyzing precisely the incrementation of acc in a relational domain. As the octagon domain we use [START_REF] Miné | The octagon abstract domain[END_REF] only supported precisely assignments involving two variables, we added new transfer functions for three-variable assignments (another solution, using the more powerful polyhedron domain [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF], did not prove scalable enough). A second example is an improvement of the pointer domain to precisely track pointers traversing nested arrays and structures, as in Fig. 29.(b) where the precise location of the pointer m+i needs to be returned. Our target application features similar complex data-structures and their traversal extensively. We thus added a non-relational integer domain for offsets of the form

α 0 + i α i [ i , h i ],
where the values of α i , i , and h i are inferred dynamically. Note that all these improvements concern only the abstract domain parameters; neither the interference iterator nor the scheduler partitioning were refined.

Following the design-by-refinement used in Astrée [START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF], we have focused on the analysis of a single (albeit large and complex) industrial software and started refining the analyzer to lower the number of alarms, instead of multiplying shallower case studies. We plan to further improve the analysis precision in order to approach the zero false alarm goal. This is the objective of the AstréeA project [START_REF] Cousot | The AstréeA static analyzer[END_REF], successor to Thésée. The remaining 2,136 alarms can be categorized into three kinds. Firstly, some alarms are, similarly to the ones described in Fig. 29, not related to parallelism but to the imprecision of the parameter abstract domains. An important class of properties currently not supported by Astrée nor Thésée is that of memory shape properties [START_REF] Chang | Relational inductive shape analysis[END_REF]. In the context of embedded software, dynamic memory allocation is disabled; nevertheless, our target code features dynamic linked lists allocated in large static arrays. Another class of properties concerns the correct manipulation of zero-terminated C strings. A significant part of the remaining alarms may be removed by designing new memory domains for these properties. Secondly, some alarms can be explained by an imprecise abstraction of thread interferences, similar to the imprecision observed in Figs. [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF][START_REF] De Roever | Concurrency Verification: Introduction to Compositional and Noncompositional Methods[END_REF] (these examples were inspired from our target code). Hence the need to extend our framework to support relational and flow-sensitive abstractions of interferences. Thirdly, some alarms have simply not yet been fully investigated. Although Thésée provides verbose information on the context of each alarm as well as the thread-local and interference invariants, discovering the origin of alarms is a challenging task on such a large code: it often requires tracking the imprecision upstream and understanding the interplay of thread interferences.

Related Work

There are far too many works on the semantics and analysis of parallel programs to provide a fair survey and comparison here. Instead, we focus on a few works that are either recent or provide a fruitful comparison with ours. 6.1. Interferences. The idea of attaching to each thread location a local invariant and handling proofs of parallel programs similarly to that of sequential programs dates back to the Hoare-style logic of Owicki and Gries [START_REF] Owicki | An axiomatic proof technique for parallel programs I[END_REF] and the inductive assertion method of Lamport [START_REF] Lamport | Proving the correctness of multiprocess programs[END_REF][START_REF] Lamport | The "Hoare logic" of concurrent programs[END_REF]. It has been well studied since; see [START_REF] De Roever | Concurrency Verification: Introduction to Compositional and Noncompositional Methods[END_REF] for a recent account and survey. The difference between the proofs of sequential programs and that of parallel programs in this framework is that the local invariants of each thread must be proved invariant by the execution of all other threads -i.e., a non-interference check. These proof methods are studied from an Abstract Interpretation theoretical point of view by Cousot and Cousot [START_REF] Cousot | Invariance proof methods and analysis techniques for parallel programs[END_REF], which leads to two results: an expression of each method as a decomposition of the global invariant into thread-local invariants, and a framework to apply abstractions and derive effective and sound static analyzers. When shifting from proof methods to inference methods, the non-interference check naturally becomes an inference of interferences. Our work is thus strongly inspired from [START_REF] Cousot | Invariance proof methods and analysis techniques for parallel programs[END_REF]: it is based on an Owicki-Gries style decomposition of the global invariant (although it is not only based on the control points of threads, but also on a more complex scheduler state). The thread-local and interference parts are then abstracted separately, using a relational flow-sensitive analysis for the former and a coarser non-relational flow-insensitive analysis for the later. Our work is also similar to the recent static analysis of C programs with POSIX threads by Carré and Hymans [START_REF] Carré | From single-thread to multithreaded: An efficient static analysis algorithm[END_REF]: both are based on Abstract Interpretation and interference computation, and both are implemented by modifying existing static analyses of sequential programs. Their analysis is more powerful than ours in that it handles dynamic thread creation and the concrete semantics models interferences as relations (instead of actions), but the subsequent abstraction leads to a non-relational analysis; moreover, real-time scheduling is not considered. 6.2. Data-Flow Analysis. Fully flow-insensitive analyses, such as Steensgaard's pointsto analysis [START_REF] Steensgaard | Points-to analysis in almost linear time[END_REF], naturally handle parallel programs. To our knowledge, all such analyses are also non-relational. These fast analyses are adequate for compiler optimization but, unfortunately, the level of accuracy required to prove safety properties demands the use of (at least partially) flow-sensitive and relational methods, which we do. By contrast, Sȃlcianu and Rinard [START_REF] Sȃlcianu | Pointer and escape analysis for multithreaded programs[END_REF] proposed a flow-sensitive pointer and escape analysis for parallel programs which is more precise (and more costly), although it still targets program optimisation. It uses a notion of interference to model the effect of threads and method calls. 6.3. Model Checking. Model-checking also has a long history of verifying parallel systems, including recently weak memory models [START_REF] Atig | On the verification problem for weak memory models[END_REF]. To prevent state explosion, Godefroid [START_REF] Godefroid | Partial-Order Methods for the Verification of Concurrent Systems -An Approach to the State-Explosion Problem[END_REF] introduced partial order reduction methods. They limit the number of interleavings to consider, with no impact on soundness nor completeness. Due to the emphasis on completeness, the remaining set of interleavings can still be high. By contrast, we abstract the problem sufficiently so that no interleaving need to be considered at all, at the cost of completeness. Another way to reduce the complexity of model checking is the context bound approach, as proposed by Qadeer et al. [START_REF] Qadeer | Context-bounded model checking of concurrent software[END_REF]. As it is unsound, it may fail to find some run-time errors. By contrast, our method takes into account all executions until completion. In his PhD, Malkis [START_REF] Malkis | Cartesian Abstraction and Verification of Multithreaded Programs[END_REF] used abstract interpretation to prove the equivalence of Owicki and Gries's proof method and the more recent model-checking algorithm by Flanagan and Qadeer [START_REF] Flanagan | Thread-modular model checking[END_REF], and presented an improvement based on counterexample-guided abstract refinement, a method which, unlike ours, is not guaranteed to converge in finite time.

6.4. Weakly Consistent Memories. Weakly consistent memory models have been studied originally for hardware -see [START_REF] Adve | Shared memory consistency models: A tutorial[END_REF] for a tutorial. Precise formal models are now available for popular architectures, such as the intel x86 model by Sewell et al. [START_REF] Sewell | x86-TSO: A rigorous and usable programmer's model for x86 multiprocessors[END_REF], either inferred from informal processor documentations or reverse-engineered through "black-box" testing [START_REF] Alglave | Litmus: Running tests against hardware[END_REF]. Pugh [START_REF] Pugh | Fixing the Java memory model[END_REF] pioneered the use of weakly consistent memory models in programming language semantics in order to take into account hardware and compiler optimizations. This culminated in the Java memory model of Manson et al. [START_REF] Manson | The Java memory model[END_REF][START_REF] Gosling | The Java Language Specification[END_REF].

Weakly consistent memory models are now recognised as an important part of language semantics and are increasingly supported by verification methods. An example in modelchecking is the work of Atig et al. [START_REF] Atig | On the verification problem for weak memory models[END_REF]. An example in theorem proving is the extension by Ševčík et al. [START_REF] Ševčík | Relaxed-memory concurrency and verified compilation[END_REF] of Leroy's formally proved C compiler [START_REF] Leroy | Formal certification of a compiler back-end or: Programming a compiler with a proof assistant[END_REF]. Testing methods have also been proposed, such as that of Alglave et al. [START_REF] Alglave | Litmus: Running tests against hardware[END_REF]. In the realm of static analysis, we can cite the static analysis by Abstract Interpretation of the happens-before memory model (at the core of the Java model) designed by Ferrara [START_REF] Ferrara | Static analysis via abstract interpretation of the happens-before memory model[END_REF]. Recently, Alglave and al. proposed in [START_REF] Alglave | Soundness of data flow analyses for weak memory models[END_REF] to lift analyses that are only sound with respect to sequential consistency, to analyses that are also sound in weak memory models. Their method is generic and uses a "repair loop" similar to our fixpoint of flow-insensitive interferences.

Memory models are often defined implicitly, by restricting execution traces using global conditions, following the approach chosen by the Java memory model [START_REF] Gosling | The Java Language Specification[END_REF]. We chose instead a generative model based on local control path transformations, which is reminiscent of the approach by Saraswat et al. [START_REF] Saraswat | A theory of memory models[END_REF]. We believe that it matches more closely classic software and hardware optimizations. Note that we focus on models that are not only realistic, but also amenable to abstraction into an interference semantics. The first condition ensures the soundness of the static analysis, while the second one ensures its efficiency. 6.5. Real-Time Scheduling. Many analyses of parallel programs assume arbitrary preemption, either implicitly at all program points (as in flow-insensitive analyses), or explicitly at specified program points (as in context-bounded approaches [START_REF] Qadeer | Context-bounded model checking of concurrent software[END_REF]), but few analyses model and exploit the strict scheduling policy of real-time schedulers. A notable exception is the work of Gamatié et al. [START_REF] Gamatié | Synchronous modeling of avionics applications using the SIGNAL language[END_REF] on the modeling of systems under an ARINC 653 operating system. As the considered systems are written in the SIGNAL language, their ARINC 653 model is naturally also written in SIGNAL, while ours in written in C (extended with low-level primitives for parallelism, which were not necessary when modeling in SIGNAL as the language can naturally express parallelism). 6.6. Further Comparison. A detailed comparison between domain-aware static analyzers, such as Astrée, and other verification methods, such as theorem proving and model checking, is presented in [START_REF] Cousot | Varieties of static analyzers: A comparison with Astrée, invited paper[END_REF]. These arguments are still valid in the context of a parallel program analysis and not repeated here. On the more specific topic of parallel program analysis, we refer the reader to the comprehensive survey by Rinard [START_REF] Rinard | Analysis of multithreaded programs[END_REF].

Conclusion

We presented a static analysis by Abstract Interpretation to detect in a sound way run-time errors in embedded C software featuring several threads, a shared memory with weak consistency, mutual exclusion locks, thread priorities, and a real-time scheduler. Our method is based on a notion of interferences and a partitioning with respect to an abstraction of the scheduler state. It can be implemented on top of existing analyzers for sequential programs, leveraging a growing library of abstract domains. Promising early experimental results on an industrial code demonstrate the scalability of our approach.

A broad avenue for future work is to bridge the gap between the interleaving semantics and its incomplete abstraction using interferences. In particular, it seems important to abstract interferences due to well synchronized accesses in a relational way (this is in particular needed to remove some alarms remaining in our target application). We also wish to add some support for abstractions that are (at least partially) sensitive to the history of thread interleavings. This would be useful to exploit more properties of real-time schedulers, related for instance to the guaranteed ordering of some computations (by contrast, we focused in this article mainly on properties related to mutual exclusion).

Moreover, we wish to extend our framework to include more models of parallel computations. This includes support for alternate real-time operating systems with similar scheduling policies but manipulating different synchronization objects, for instance the condition variables in real-time POSIX systems [START_REF]Portable operating system interface (POSIX) -Application program interface (API) amendment 2: Threads extension (C language). Technical report[END_REF], or alternate priority schemes, such as the priority ceiling protocol for mutexes. Another example is the support for the OSEK/VDX and Autosar real-time embedded platforms widely used in the automotive industry. We also wish to study more closely weak memory consistency semantics and, in particular, how to design more precise or more general interference semantics, and abstract them efficiently. Supporting atomic variables, recently included in the C and C++ languages, may also trigger the need for a finer, field-sensitive handling of weak memory consistency.

A long term goal is the analysis of other errors specifically related to parallelism, such as dead-locks, live-locks, and priority inversions. In a real-time system, all system calls generally have a timeout in order to respect hard deadlines. Thus, interesting properties are actually quantitative: by construction, unbounded priority inversions cannot occur, so, we wish to detect bounded priority inversions.

On the practical side, we wish to improve our prototype analyzer to reduce the number of false alarms on our target industrial code. This requires some of the improvements to the parallel analysis framework proposed above (such as relational and flow-sensitive abstractions for interferences), but also the design of new numerical, pointer, and memory domains which are not specific to parallel programs.

i∈N G i (∅, ∅). We now prove by induction on i that G ,Ω). Note that, ∀i ∈ N : F i is a complete -morphism. Thus, the function (R, Ω) → lfp G is also a complete -morphism, and so is S while e 0 do s . A.2. Proof of Theorem 2.2. P ⊆ P .

i (∅, ∅) = k<i F k (R, Ω). Indeed: G 1 (∅, ∅) = (R, Ω) F (∅, ∅) = (R, Ω) = F 0 (R, Ω) and G i+1 (∅, ∅) = G k<i F k (R, Ω) = (R, Ω) F k<i F k (R, Ω) = (R, Ω) k<i F k+1 (R, Ω) = k<i+1 F k (R, Ω) because F is a -morphism. As a consequence, lfp G = i∈N F i (R
Proof. We prove by structural induction on s that:

∀s, R , Ω : (S s • γ)(R , Ω) (γ • S s )(R , Ω) .
• The case of primitive statements X ← e and e 0? holds by hypothesis: the primitive abstract functions provided by the abstract domain are assumed to be sound.

• The case of sequences s 1 ; s 2 is settled by noting that the composition of sound abstractions is a sound abstraction. • The case of conditionals if e 0 then s is settled by noting additionally that ∪ is a sound abstraction of , as ∪ E is a sound abstraction of ∪. • We now treat the case of loops. By defining:

F (X) def = (R , Ω) ∪ (S s • S e 0? )(X) F (X) def = (R, Ω) (S s • S e 0? )(X)
we have S while e 0 do s (R , Ω) = S e 0? (lim λX : X F (X )) S while e 0 do s (R, Ω)

= S e 0? (lfp F ) .

By induction hypothesis, soundness of ∪ and composition of sound functions, F is a sound abstraction of F . Assume now that (R , Ω ) is the limit of iterating λX : X F (X) from (⊥ E , ∅). Then, it is a fixpoint of λX : X F (X ), hence (R , Ω ) = (R , Ω ) F (R , Ω ). Applying γ and the soundness of and F , we get:

γ(R , Ω ) = γ((R , Ω ) F (R , Ω )) γ(F (R , Ω )) F (γ(R , Ω )) .
Thus, γ(R , Ω ) is a post-fixpoint of F . As a consequence, it over-approximates lfp F , which implies the soundness of the semantics of loops. We now apply the property we proved to s = body, R = E 0 and Ω = ∅, and use the monotony of S s and the fact that γ(E 0 ) ⊇ E 0 to get:

γ(S body (E 0 , ∅)) S body (γ(E 0 , ∅)) S body (E 0 , ∅) which implies P ⊇ P. A.3. Proof of Theorem 2.3. ∀s ∈ stat : Π π(s) = S s .
Proof. The proof is by structural induction on s.

• The case of primitive statements is straightforward as π(s) = { s }.

• For sequences, we use the induction hypothesis and the fact that Π is a morphism for path concatenation to get:

S s 1 ; s 2 = S s 2 • S s 1 = Π π(s 2 ) • Π π(s 1 ) = Π π(s 1 ) • π(s 2 ) = Π π(s 1 ; s 2 ) .
• For conditionals, we also use the fact that Π is a morphism for ∪:

S if e 0 then s (R, Ω) = (S s • S e 0? )(R, Ω) S e 0? (R, Ω) = (Π π(s) • Π { e 0? } )(R, Ω) Π { e 0? } (R, Ω) = Π ((e 0?) • π(s)) ∪ { e 0? } (R, Ω) = Π π(if e 0 then s) (R, Ω) .
• For loops while e 0 do s, we define F and G as in proof A.1, i.e., F (X)

def = (S s • S e 0? )X and G(X) def = (R, Ω) F (X). Recall then that lfp G = i∈N F i (R, Ω).
By induction hypothesis and •-morphism, we have:

F i = (S s • S e 0? ) i = (Π {e 0?} • π(s) ) i = Π ({e 0?} • π(s)) i .
Let us now define the set of paths

P def = lfp λX : { } ∪ (X • {e 0?} • π(s))
. By [START_REF] Cousot | Constructive versions of Tarski's fixed point theorems[END_REF], P = i∈N ({e 0?} • π(s)) i . As a consequence:

Π P = i∈N Π ({e 0?} • π(s)) i = i∈N F i and Π P (R, Ω) = i∈N F i (R, Ω) = lfp G.
consider first the case of variables e = X ∈ V, which is the interesting case. When γ E (R ) has no interference for X, then apply(t, R , I , X) = X and:

E apply(t, R , I , X) ρ = E X ρ = {ρ(X)} = E I X (t, ρ, γ I (I )) .
In case of interferences on X, we have apply(t, R , I , X) = as-expr (V X ∪ N get(X, R )), which is an interval [l, h] containing, by definition of as-expr and soundness of get, both ρ(X) and { v | ∃t = t : (t , X, v) ∈ γ I (I ) }. Thus, E apply(t, R , I , X) ρ = [l, h] ⊆ E X ρ. For other expressions, we note that E I and E are defined in similar way, and so, the proof stems from the induction hypothesis and the monotony of E I and E.

To prove the soundness of primitive statements S I s , we combine the above result with the soundness of S with respect to S. We immediately get that R((S I s • γ)(R , Ω, I )) ⊆ R((γ •S I s )(R , Ω, I )) for an assignment or test s, and likewise for the Ω component. (We reuse the notations R(X), Ω(X), I(X) from the proof A.5.) The I component is unchanged by S I s and S I s when s is a test. For the I component after an assignment, we remark that I((S I X ← e • γ)(R , Ω, I)) can be written as γ I (I) ∪ { (t, X, ρ(X)) | ρ ∈ R((S I X ← e • γ)(R , Ω, I)) } .

We then reuse the fact that R((S I s •γ)(R , Ω, I )) ⊆ R((γ •S I s )(R , Ω, I )) to conclude the proof of primitive statements.

The case of non-primitive statements is easier as it is mostly unchanged between S and S I (hence, between S and S I ). Hence, the proof in A.2 of Thm. 2.2 still applies.

As a consequence, we have: By soundness of ∪ I , I , S I , and E 0 , we get that F is a sound abstraction of F . The same fixpoint transfer property that was used for loops in proof A.2 can be used here to prove that lim F is a sound abstraction of lfp F . As a consequence, we have Ω I ⊇ Ω I , and so, P I ⊇ P I .

-(R i , Ω i , I i ) = Π I X i ← e i , t (R, Ω, I) for i = 1, 2, and -(R 1;2 , Ω 1;2 , I 1;2 ) = Π I X 1 ← e 1 • X 2 ← e 2 , t (R, Ω, I), and -(R 2;1 , Ω 2;1 , I 2;1 ) = Π I X 2 ← e 2 • X 1 ← e 1 , t (R, Ω, I). As X 2 / ∈ var (e 1 ), X 1 / ∈ var (e 2 ), and X 1 = X 2 , we have This implies R 1;2 = R 2;1 , and so, (iii).

As nonblock (e 1 ), we have ∀ρ ∈ R : ∃v : ρ[X 1 → v] ∈ R 1 . This implies Ω 2 = Ω(Π I X 2 ← e 2 , t (R 1 , Ω, I)), and so Ω 1;2 = Ω 1 ∪ Ω 2 . Likewise, I 1;2 = I 1 ∪ I 2 . Moreover, Ω 2;1 ⊆ Ω 1 ∪ Ω 2 = Ω 1;2 and I 2;1 ⊆ I 1 ∪ I 2 = I 1;2 . Thus (i) and (ii) hold.

As in (1), the nonblock (e 1 ) hypothesis is important so that errors in e 2 masked by X 1 ← e 1 in the original program do not appear in the transformed program.

(4) Reordering guards: e 1 0? • e 2 0? e 2 0? • e 1 0?, where noerror (e 2 ). We use the same notations as in the preceding proof. We have I 2;1 = I 1;2 = I, which proves (ii). Consider ρ ∈ R, then either ρ ∈ R 1 ∩ R 2 , in which case ρ ∈ R 1;2 and ρ ∈ R 2;1 , or ρ / ∈ R 1 ∩ R 2 , in which case ρ / ∈ R 1;2 and ρ / ∈ R 2;1 . In both cases, R 1;2 = R 2;1 , which proves (iii). We have Ω 2 ⊆ Ω 2;1 ⊆ Ω 1 ∪ Ω 2 and Ω 1 ⊆ Ω 1;2 ⊆ Ω 1 ∪ Ω 2 . But, as noerror (e 2 ), Ω 2 = ∅, which implies Ω 2;1 ⊆ Ω 1 ⊆ Ω 1;2 , and so, (i).

The property noerror (e 2 ) is important. Consider otherwise the case where e 1 0? filters out an environment leading to an error in e 2 . The error would appear in the transformed program but not in the original one.

(5) Reordering guards before assignments: X 1 ← e 1 • e 2 0? e 2 0? • X 1 ← e 1 , where X 1 / ∈ var (e 2 ) and either nonblock (e 1 ) or noerror (e 2 ). We use the same notations as in the preceding proofs. As X 1 / ∈ var (e 2 ), we have ∀ρ, v : E I e 2 (t, ρ, I) = E I e 2 (t, ρ[X 1 → v], I) .

This implies R 1;2 = R 2;1 , and so, (iii). Moreover, we have I 1;2 = I 1 and I 2;1 ⊆ I 1 , thus (ii) holds. For (i), consider first the case nonblock (e 1 ). We have ∀ρ ∈ R : ∃v : ρ[X 1 → v] ∈ R 1 . This implies Ω 2 = Ω(Π I e 2 0?, t (R 1 , Ω, I)), and so Ω 1;2 = Ω 1 ∪ Ω 2 .

As Ω 2 ⊆ Ω 2;1 ⊆ Ω 1 ∪ Ω 2 , (i) holds. Consider now the case noerror (e 2 ). We have Ω 1;2 = Ω 1 and Ω 2;1 ⊆ Ω 1 , and so, (i) holds. [START_REF] Atig | On the verification problem for weak memory models[END_REF] Reordering assignments before guards: e 1 0? • X 2 ← e 2 X 2 ← e 2 • e 1 0?, where X 2 / ∈ var (e 1 ), X 2 ∈ V l (t), and noerror (e 2 ). As X 2 / ∈ var (e 1 ), we have ∀ρ, v : E I e 1 (t, ρ, I) = E I e 1 (t, ρ[X 2 → v], I) and thus, using the same notations as before, R 1;2 = R 2;1 , and so, (iii). Because, noerror (e 2 ), we have Ω 2;1 ⊆ Ω 1 ∪ Ω 2 = Ω 1 and Ω 1;2 = Ω 1 , and so Ω 2;1 ⊆ Ω 1;2 (i).

Unlike the preceding proofs, we now have I 1;2 ⊆ I 2;1 = I 2 and generally I 1;2 ⊇ I 2;1 . However, as X 2 ∈ V l (t), we have I 2;1 \I 1;2 ⊆ {t}×V l (t)×R, i.e., the only interferences added by the transformation concern the variable X 2 , local to t. This is sufficient to ensure (ii). As var (e) ⊆ V l (t), there is no interference in I for variables in e from other threads. We deduce that E I e (t, ρ, I) = E e ρ. Likewise, E I e (t, ρ, I) = E e ρ, and so, E I e (t, ρ, I) E I e (t, ρ, I). By monotony of S I , we get: Π I s, t (R, Ω, I) Π I s[e /e], t (R, Ω, I) which implies (i)-(iii). We now prove that, if the pair p, p satisfies (i)-(iii), then so does the pair p•s, p •s for any primitive statement s executed by t. We consider a triple (R 0 , Ω 0 , I 0 ) and note (R , Ω , I ) = Π I p , t (R 0 , Ω 0 , I 0 ) and (R, Ω, I) = Π I p, t (R 0 , Ω 0 , I 0 ). Take any ρ ∈ R . By (iii) on the pair p, p , there is some ρ ∈ R that equals ρ except maybe for some variables that are free, and so, cannot occur in s. Moreover, by (ii) on p, p , I contains I except maybe for some interferences that are from t, and so, cannot influence the expression in s. So, by noting e the expression appearing in s, E I e (t, ρ , I ) I E I e (t, ρ, I). As a consequence, (i) and (ii) hold for the pair p•s, p •s. Consider now ρ ∈ R(Π I p • s, t (R 0 , Ω 0 , I 0 )). If s is a guard e = 0? (the other guards e 0? being similar), then ρ ∈ R and, by (iii) for p, p , ∃ρ ∈ R equal to ρ except for some free variables. As, 0 ∈ V (E I e (t, ρ , I )) ⊆ V (E I e (t, ρ, I)), ρ proves the property (iii) for p • s, p • s. If s is an assignment X ← e then ρ = ρ 0 [X → ρ (X)] for some ρ 0 ∈ R and ρ (X) ∈ V (E I e (t, ρ 0 , I )). By (iii) for p, p , ∃ρ 0 ∈ R equal to ρ 0 except for some free variables. So, ρ (X) ∈ V (E I e (t, ρ 0 , I )) ⊆ V (E I e (t, ρ 0 , I)). Thus, ρ 0 [X → ρ (X)] proves the property (iii) for p • s, p • s.

The following two properties are much easier to prove. Firstly, if the pair p, p satisfies (i)-(iii), so does the pair q • p, q • p for any path q. This holds because (i)-(iii) are stated for all R, Ω and I. Secondly, if both pairs p, p and p , p satisfy (i)-(iii), then so does the pair p, p . This completes the proof that elementary path transformations can be applied in a context with an arbitrary prefix and suffix, and that several transformations can be applied sequentially.

We are now ready to prove the theorem. Consider the least fixpoint computed by the interference semantics (3.4):

(Ω I , I I ) = lfp F where F (Ω, I) = ( t∈T Ω t , t∈T I t ) and (-, Ω t , I t ) = S I body t , t (E 0 , Ω, I) .

By Thm. 3.1, we have (-, Ω t , I t ) = Π I π(body t ), t (E 0 , Ω, I). Given transformed threads π (t), consider also the fixpoint:

(Ω I , I I ) = lfp F where F (Ω , I ) = ( t∈T Ω t , t∈T I t \ I l ) and (-, Ω t , I t ) = Π I π (t), t (E 0 , Ω , I ) and I l is a set of interferences we can ignore as they only affect local or fresh variables:

I l = { (t, X, v) | t ∈ T , v ∈ R, X ∈ V f ∪ V l (t) } .
Then, given each path in p ∈ π (t), we can apply properties (i) and (ii) to the pair p, p , where p is the path in π(body t ) that gives p after transformation. We get that F (X) I F (X). As a consequence, lfp F I lfp F . The transformed semantics, however, is not prove:

(i) Ω(Π C p , t (R, Ω, I)) ⊆ Ω(Π C p, t (R, Ω, I)) Note, in particular, that in (ii) and (iii), the configuration c is the same for the original path p and the transformed path p . We first consider the case of acceptable elementary operations from Def. 3.4. As they involve guards and assignments only, not synchronization primitives, and because S C X ← e, t and S C e 0?, t never change the partitioning, the proof of (i)-(iii) for all elementary transformations is identical to that of proof A.7.

We now prove that, if (i)-(iii) hold for a pair p, p , then they also hold for a pair p•s, p •s for any statement s. The case where s is an assignment or guard is also identical to that of proof A.7, for the same reason. We now consider the case of synchronization primitives. (i) holds because synchronization primitives do not change the set of errors. The proof that (ii) holds is similar to the case of an assignment. Indeed, any interference added by s after p has the form (t, c, X, ρ (X)) for some state (c, ρ ) ∈ R(Π C p , t (R, Ω, I)). Due to (iii), there is some (c, ρ) ∈ R(Π C p, t (R, Ω, I)) where, either X ∈ V f or ρ(X) = ρ (X). When X / ∈ V f , we note that any (t, c, X, ρ (X)) added by s after p is also added by s after p. Thus, the extra interferences in p do not violate (ii). For the proof of (iii), take (c, ρ ) ∈ R(Π C p • s, t (R, Ω, I)). There exists some (c, ρ 1 ) ∈ R(Π C p , t (R, Ω, I)) where, for all X ∈ V, either ρ (X) = ρ 1 (X), or there is a well synchronized interference (t , c , X, ρ (X)) with t = t . By applying (ii) to the pair p, p , all these interferences are also in I(Π C p, t (R, Ω, I)). Thus, by applying (iii) to the pair p, p , we get a state (c, ρ 1 ) ∈ R(Π C p, t (R, Ω, I)) that also satisfies (iii) for the pair p • s, p • s.

As in proof A.7, the fact that, for any p, p , p , q, if the pairs p, p and p , p satisfy (i)-(iii), then so do the pair p, p and the pair q • p, q • p is straightforward. This completes the proof that elementary path transformations can be applied in sequence and applied in a context containing any primitive statements (even synchronization ones) before and after the transformed part.

The end of the proof is identical to that of proof A.7. We compare the fixpoints lfp F and lfp F that compute respectively the semantics of the original program S C body t , t = Π C π(body t ), t and the transformed program Π C π (t), t . Then, (i) and (ii) imply that F (X) C F (X), and so, lfp F C lfp F , except for interferences on local or free variables. In particular, Ω(lfp F ) ⊆ Ω(lfp F ). The interference semantics of the original program contains all the errors that can occur in any program obtained by acceptable thread transformations. As a consequence, P H ⊆ P C . A.9. Proof of Theorem 4.2. P C ⊆ P C .

Proof. We remark that P C and P I , and so, P C and P I , are similar. In particular, the definitions for non-primitive statements and the fixpoint computation of interferences have the exact same structure. Hence, the proof A.6 applies directly to prove the soundness of non-primitive statements as a consequence of the soundness of primitive statements. Moreover, for assignments and tests, the proof of soundness is identical to the proof A.6, but componentwise for each c ∈ C. To prove the soundness of synchronization statements, we first observe the soundness of in and out in that: ∀t ∈ T , l, u ⊆ M, m ∈ M, V ∈ E , I ∈ I : ∀ρ ∈ γ E (V ) : in(t, l, u, m, ρ, γ I (I )) ⊆ γ E (in (t, l, u, m, V , I )) out(t, l, u, m, ρ, γ I (I )) ⊆ γ I (out (t, l, u, m, V , I )) .

2 )Figure 1 :

 21 Figure 1: Semantics defined in the article.

Figure 2 :

 2 Figure 2: Syntax of programs.

Figure 3 :

 3 Figure 3: Concrete semantics of expressions.

Figure 4 :

 4 Figure 4: Structured concrete semantics of statements.

Figure 7 :

 7 Figure 7: Concrete semantics of expressions with interference.

  , Ω ) = E I e (t, ρ, I) in ({ ρ | ∃v ∈ V : v 0 }, Ω , ∅) S I if e 0 then s, t (R, Ω, I) def = (S I s, t • S I e 0?, t )(R, Ω, I) I S I e 0?, t (R, Ω, I) S I while e 0 do s, t (R, Ω, I) def = S I e 0?, t (lfp λX : (R, Ω, I) I (S I s, t • S I e 0?, t )X)

Figure 8 :

 8 Figure 8: Concrete semantics of statements with interference.

Figure 9 :

 9 Figure 9: Incompleteness examples for the concrete interference semantics.

Figure 10 :

 10 Figure 10: Signature, soundness and termination conditions for a domain N abstracting sets of reals.

Figure 11 :

 11 Figure 11: Abstract domain I of interferences, derived from N .

Figure 14 :

 14 Figure 14: Using priorities to ensure mutual exclusion.

Figure 16 :

 16 Figure 16: Well synchronized versus weakly consistent communications.

Figure 17 :

 17 Figure 17: Well synchronized and weakly consistent communications with two locks.

Figure 18 :

 18 Figure 18: Concrete scheduled semantics of expressions with interference.

Figure 19 :

 19 Figure 19: Concrete scheduled semantics of statements with interference.

Finally

  , we turn to the semantics P C of a program, which has the same fixpoint form as P I (3.4):P C def = Ω, where (Ω, -) def = lfp λ(Ω, I) : t∈T let (-, Ω , I ) = S C body t , t ({c 0 } × E 0 , Ω, I) in (Ω , I ) (4.10)where the initial configuration is c0 def = (∅, ∅, weak ) ∈ C.This semantics is sound with respect to that of Secs. 4.2-4.3: Theorem 4.1. P H ⊆ P C and P H ⊆ P C .

Figure 20 :

 20 Figure 20: Read / write data-race detection.

Figure 21 :

 21 Figure 21: Imprecisely analyzed program due to the lack of relational lock invariant.

Figure 22 :

 22 Figure 22: Imprecisely analyzed program due to the lack of inter-thread flow-sensitivity.

Figure 23 :

 23 Figure 23: Abstract domain of scheduled interferences I , derived from N .

Figure 26 :

 26 Figure 26: Abstract scheduled semantics with interference of synchronization primitives.

Figure 27 :

 27 Figure 27: Hierarchy of abstractions in Astrée and Thésée. Domains in boldface are specific to Thésée and not included in Astrée.

  ∀t ∈ T : (S I body t , t • γ)(R , Ω, I ) I (γ • S I body t , t )(R , Ω, I ) .Consider now the solutions (Ω I , I I ) and (Ω I , I I ) of the fixpoints (3.4) and (3.6). We have:(Ω I , I I ) = lfp F where F (Ω, I) = t∈T (Ω t , I t ) and (-, Ω t , I t ) = S I body t , t (E 0 , Ω, I) Likewise:(Ω I , I I ) = lim F where F (Ω , I ) = (Ω , I ) t∈T (Ω t , I t ) and (-, Ω t , I t ) = S I body t , t (E 0 , Ω , I ) defining (Ω 1 , I 1 ) (Ω 2 , I 2 ) def = (Ω 1 ∪ Ω 2 , I 1 ∪ I I 2 ) and (Ω 1 , I 1 ) (Ω 2 , I 2 ) def = (Ω 2 , I 1 I I 2 )

  ∀ρ, v : E I e 1 (t, ρ, I) = E I e 1 (t, ρ[X 2 → v], I) and ∀ρ, v : E I e 2 (t, ρ, I) = E I e 2 (t, ρ[X 1 → v], I) .

( 9 )

 9 Expression simplification: s s[e /e], when ∀ρ : E e ρ E e ρ and var (e) ∪ var (e ) ⊆ V l (t).

(

  ii) ∀(t , c, X, v) ∈ I(Π C p , t (R, Ω, I)) : (t , c, X, v) ∈ I(Π C p, t (R, Ω, I)) or t = t ∧ X ∈ V l (t) (iii) ∀(c, ρ ) ∈ R(Π C p , t (R, Ω, I)) : ∃ρ ∈ E : (c, ρ) ∈ R(Π C p, t (R, Ω, I)), ∀X ∈ V : ρ(X) = ρ (X) or X ∈ V f

  Secondly, we observe that S C first reorganizes (without loss of information) the sets of environment tuples R ⊆ C × E and interference tuplesI ⊆ T × C × V × R appearing in S C as functions R def = λc : { ρ | (c, ρ) ∈ R } and I def = λt, c, X : { v | (t, c, X, v) ∈ I }.Then, it applies an abstraction in, respectively, E and N by replacing the set union ∪ by its abstract counterparts ∪ E and ∪ I .

  2.3. Soundness and completeness. Before linking our interference semantics P I (by structural induction) to the interleaving semantics P * of Sec. 3.1 (which is path-based), we remark that we can restate the structured interference semantics S I body t , t of a single thread t in a path-based form, as we did in Sec. 2.4 for non-parallel programs. Indeed, we can replace S with S I in (2.4) and derive a path-based semantics with interference Π I P, t ∈ D I

	I -→ D I
	of a set of (non-parallel) control paths P ⊆ Π in a thread t as follows:

Note that Fig.1states that each concrete semantics without scheduler abstracts the corresponding concrete semantics with scheduler, but states nothing about abstract semantics. Abstract semantics are generally incomparable due to the use of non-monotonic abstractions and widenings.

Acknowledgement

We wish to thank the ESOP'11 and LMCS anonymous reviewers as well as David Pichardie for their helpful comments on several versions of this article.

This work was partially supported by the INRIA project "Abstraction" common to CNRS and ENS in France, and by the project ANR-11-INSE-014 from the French Agence nationale de la recherche.

Analysis result

Figure 28: Evolution of the number of alarms in the analysis of our target application as we improved our prototype analyzer. the first versions of Thésée were naturally tuned for avionic control / command software as they inherited abstract domains E and N from Astrée, but our target application for Thésée is not limited to control / command processing. To achieve our current results, we improved the numerical, pointer, and memory domains in Thésée, and designed new ones.

We illustrate two of these improvements in Fig. 29. A first example is the improvement of transfer functions of existing domains. For instance, the function accum from Fig. 29.(a)

Appendix A. Proof of Theorems A.1. Proof of Theorem 2.1. ∀s ∈ stat : S s is well defined and a complete -morphism.

Proof. We prove both properties at the same time by structural induction on s.

• The case of assignments X ← e and guards e 0? is straightforward.

• The semantics of conditionals and sequences is well-defined as its components are well-defined by induction hypothesis. It is a complete -morphism, by induction hypothesis and the fact that the composition and the join of complete -morphisms are complete -morphisms. • For a loop while e 0 do s, consider F and G defined as:

By induction hypothesis, F , and so G, are complete -morphisms. Thus, G has a least fixpoint [START_REF] Cousot | Constructive versions of Tarski's fixed point theorems[END_REF]. We note that:

S while e 0 do s (R, Ω) = S e 0? (lfp G) which proves that the semantics of loops is well-defined. Moreover, according to [START_REF] Cousot | Constructive versions of Tarski's fixed point theorems[END_REF] again, the least fixpoint can be computed by countable Kleene iterations: lfp G = Finally:

S while e 0 do s (R, Ω) = S e 0? (lfp G)

Proof. The proof A.3 of Thm. 2.3 only relies on the fact that the semantic functions S s are complete -morphisms. As the functions S I s, t are complete I -morphisms, the same proof holds.

A.5. Proof of Theorem 3.2. P * ⊆ P I .

Proof. To ease the proof, we will use the notations R(X), Ω(X), I(X) to denote the various components of a triplet X = (R(X), Ω(X), I(X)) in the concrete domain D I = P(E) × P(L) × P(I), and V (X), Ω(X) for pairs X = (V (X), Ω(X)) in P(R) × P(L) output by the semantics of expressions.

Let (Ω I , I I ) be the fixpoint computed in (3.4), i.e., (Ω I , I I ) = t∈T (Ω t , I t ) where (-, Ω t , I t ) = S I body t , t (E 0 , Ω I , I I ). Then, by definition, P I = Ω I . We first prove the following properties that compare respectively the set of errors and environments output by the interleaving semantics and the interference semantics of any path p ∈ π * :

The proof is by induction on the length of p. The case p = is straightforward: the Ω component is ∅ on both sides of (i), and we can take ρ = ρ in (ii) as the R component is E 0 on both sides. Consider now p = p • (s , t ), i.e., p is a path p followed by an assignment or guard s from thread t . Consider some ρ ∈ R(Π * p (E 0 , ∅)) and the expression e appearing in s . We can apply the (ii) recurrence hypothesis to p and t which returns some ρ ∈ R(Π I proj t (p ), t (E 0 , ∅, I I )). The fact that, for any X ∈ V, either ρ(X) = ρ (X) or ∃t = t : (t , X, ρ(X)) ∈ I I implies, given the definition of E I e (Fig. 7), that:

(iii) E e ρ E I e (t , ρ , I I ) When considering, in particular, the error component Ω(E e ρ), (iii) allows extending the recurrence hypothesis (i) on p to also hold on p, i.e., executing s adds more errors on the right-hand side of (i) than on the left-hand side.

To prove (ii) on p, we consider two cases, depending on the kind of statement s : • Assume that s is a guard, say e = 0? (the proof is identical for other guards e 0?). Take any t ∈ T and ρ ∈ R(Π * p (E 0 , ∅)). By definition of S e = 0? , we have ρ ∈ R(Π * p (E 0 , ∅)) and 0 ∈ V (E e ρ). Take any ρ that satisfies the recurrence hypothesis (ii) on p for t and ρ. We prove that it also satisfies (ii) on p for t and ρ.

The case t = t is straightforward as, in this case, proj t (p) = proj t (p ). When t = t , then proj t (p) = proj t (p ) • (e = 0?). Recall property (iii): E e ρ E I e (t , ρ , I I ), which implies that 0 ∈ V (E I e (t , ρ , I I )), and so, we have ρ ∈ R(Π I proj t (p), t (E 0 , ∅, I I )).

• Assume that s is an assignment X ← e . Take any ρ ∈ R(Π * p (E 0 , ∅)) and t ∈ T . Then ρ has the form ρ 0 [X → ρ(X)] for some ρ 0 ∈ R(Π * p (E 0 , ∅)) and ρ(X) ∈ V (E e ρ 0 ). We first prove that (t , X, ρ(X)) ∈ I I . Take ρ 0 as defined by the recurrence hypothesis (ii) for t , p and ρ 0 . Then ρ(X) ∈ V (E e ρ 0 ) ⊆ V (E I e (t , ρ 0 , I I )) by property (iii). By definition of S I X ← e , t (Fig. 8), we have (t , X, ρ(X)) ∈ I(S I X ← e , t ({ρ 0 }, ∅, I I )). We have

To prove (ii), we consider first the case where t = t . Take ρ 0 as defined by the recurrence hypothesis (ii) for t, p and ρ 0 . As t = t , proj t (p) = proj t (p ), and ρ 0 ∈ R(Π I proj t (p), t (E 0 , ∅, I I )). As ρ and ρ 0 are equal except maybe on X, and we have (t , X , ρ(X)) ∈ I I , then ρ 0 satisfies (ii) for t, p, and ρ.

We now consider the case where t = t . Take ρ 0 as defined by the recurrence hypothesis (ii) for t, p and ρ 0 . We define ρ = ρ 0 [X → ρ(X)]. The property (iii) implies V (E e ρ 0 ) ⊆ V (E I e (t , ρ 0 , I I )). We get ρ ∈ R(Π I proj t (p ) • (X ← e ), t (E 0 , ∅, I I )) = R(Π I proj t (p), t (E 0 , ∅, I I )). As ρ and ρ 0 are equal except maybe on X, and ρ and ρ 0 are also equal except maybe on X, and on X we have ρ(X) = ρ (X), then ρ satisfies (ii) for t, p and ρ. The theorem then stems from applying property (i) to all p ∈ π * and using Thm. 3.1:

A.6. Proof of Theorem 3.3. P I ⊆ P I .

Proof. We start by considering the semantics of expressions. We first note that, for any abstract environment R ∈ E , abstract interference I ∈ I , thread t, and expression e, if ρ ∈ γ E (R ), then E I e (t, ρ, γ I (I )) ⊆ E apply(t, R , I , e) ρ, i.e., apply can be used to over-approximate the semantics with interference E I using the non-interfering semantics E in the concrete. We prove this by structural induction on the syntax of expressions e. We A.7. Proof of Theorem 3.5. P * ⊆ P I .

Proof. We reuse the notations R(X), Ω(X), I(X), V (X) from proof A.5. Consider a path p from a thread t that gives, under an elementary transformation from Def. 3.4, a path p . Let us denote by V f the subset of fresh variables (i..e, that do not appear anywhere in the program, except maybe in p ), and by V l (t) the subset of variables that are local to t (i.e., that do not appear anywhere, except maybe in thread t).

We consider triples (R, Ω, I) such that the interferences I are consistent with the fresh and local variables, i.e., if (t, X, v) ∈ I, then X / ∈ V f and X ∈ V l (t ) =⇒ t = t . We prove that, for such triples, the following holds:

i.e., the transformation does not add any error (i), it can only add interferences on local variables (ii), and change environments on fresh variables (iii). We now prove (i)-(iii) for each case in Def. 3.4.

(1) Redundant store elimination: X ← e 1 • X ← e 2 X ← e 2 , where X / ∈ var (e 2 ) and nonblock (e 1 ). We note:

-

∈ var (e 2 ), E I e 2 (t, ρ, I) = E I e 2 (t, ρ[X → v], I) for any ρ and v. Moreover, as nonblock (e 1 ):

This implies R 1;2 = R 2 , and so, (iii). Moreover, Ω 1;2 = Ω 1 ∪ Ω 2 ⊇ Ω 2 , and so, (i). Likewise, I 1;2 = I 1 ∪ I 2 ⊇ I 2 , and so, (ii).

Note that the hypothesis nonblock (e 1 ) is important. Otherwise we could allow

, where the error is in the transformed program but not in the original one (here, Ω 1;2 = Ω 1 ⊇ Ω 2 ).

(2) Identity store elimination X ← X . We have:

In the two last inequalities, the converse inequality does not necessarily hold. Indeed, X ← X creates interferences that may be observed by other thread. Moreover V (E I X (t, ρ, I)) is not necessarily { ρ(X) }, but may contain interferences from other threads. This shows in particular that the converse transformation, identity insertion, is not acceptable as it introduces interferences.

(3) Reordering assignments:

∈ var (e 2 ), X 2 / ∈ var (e 1 ), X 1 = X 2 , and nonblock (e 1 ). We note:

, where X / ∈ var (e), var (e) ⊆ V l (t), and e is deterministic. Let us note :

-

. As e is deterministic and X / ∈ var (e), V (E X ρ 1 ) = V (E e ρ) = {ρ 1 (X)}. Additionally, as var (e) ⊆ V l (t), there is no interference in I for variables in e from other threads, and so, V (E I X (t, ρ 1 , I 1 )) = V (E I e (t, ρ, I)) = {ρ 1 (X)}. As a consequence, R 1;2 = R 1;2 , which proves (iii). Moreover, I 1;2 = I 1;2 , hence (ii) holds. Finally, we have { Ω(E I e (t, ρ, I)

, any error from the evaluation of e while executing s[e/X] in R 1 was already present during the evaluation of e while executing X ← e in R. Thus, Ω 1;2 = Ω 1;2 , and (i) holds.

The fact that e is deterministic is important. Otherwise, consider

. Then Y ∈ {0, 2} on the left of while Y ∈ {0, 1, 2} on the right of : the transformed program has more behaviors than the original one. Likewise, var (e) ⊆ V l (t) ensures that e may not evaluate to a different value due to interferences from other threads.

(8) Sub-expression elimination:

where X ∈ V f , var (e) ∩ lval (s i ) = ∅, and noerror (e). Let us note:

(R , Ω , I ) = Π I X ← e, t (R, Ω, I) . Consider ρ ∈ R . Then ρ = ρ[X → ρ (X)] for some ρ ∈ R and ρ (X) ∈ V (E I e (t, ρ, I)). As X does not appear in s i (being fresh), and noting:

X)} and, as X ∈ V f , there is no interference on X, and

As var (e) ∩ lval (s i ) = ∅, and noting

As X ∈ V f , this implies (ii) when i = n. Moreover, as noerror (e), Ω = Ω. Note that:

exactly lfp F , but rather:

(Ω t , I t ) = lfp F where F (Ω , I ) = ( t∈T Ω t , t∈T I t ) and (Ω t , I t ) defined as before

The difference lies in the extra interferences generated by the transformed program, which are all in I l . Such interferences, however, have no influence on the semantics of threads, as we have:

. Indeed, any interference (t , X, v) ∈ I l is either from thread t and then ignored for the thread t itself, or it is from another thread t = t in which case X is a local variable of t or a free variable, which does not occur in t . As a consequence, I t = I t and Ω t = Ω t , and so, Ω = Ω ⊆ Ω. Hence, the interference semantics of the original program contains all the errors that can occur in any program obtained by acceptable thread transformations.

A.8. Proof of Theorem 4.1. P H ⊆ P C and P H ⊆ P C .

Proof. We first prove P H ⊆ P C .

In order to do so, we need to consider a path-based interference semantics Π C P, t that, given a set of paths P ⊆ π(body t ) in a thread t, computes:

Similarly to Thms. 2.3, 3.1, the two semantics are equal:

The proof is identical to that in A.3 as the S C functions are complete -morphisms, and so, we do not repeat it here.

The rest of the proof that P H ⊆ P C follows a similar structure as A.5. Let (Ω C , I C ) be the fixpoint computed in (4.10), i.e.,

We denote initial states for P H and P C as respectively E 0h def = {h 0 }×E 0 and E 0c def = {c 0 }×E 0 . Furthermore, we link scheduler states h ∈ H and partitioning configurations c ∈ C in a thread t with the following abstraction α t : H → P(C):

i.e., a configuration forgets the ready state b(t) of the thread (ready, yield ing, or waiting for some mutex), but remembers the exact set of mutexes l(t) held by the current thread, and optionally remembers the mutexes not held by any thread u. We prove the following properties by induction on the length of the path p ∈ π * :

The properties hold for p = as ∀t ∈ T :

Assume that the properties hold for p and consider p = p • (s , t ), i.e., p followed by a primitive statement s executed by a thread t . The case where s is an assignment or a guard is very similar to that of proof A.5: we took care to update (ii) to reflect the change in the evaluation of variables in expressions E C X (in particular, the use of intf to determine which interferences from other threads can influence the current one, given their respective configuration). The effect of enabled t in S H s , t is to remove states from R(Π H p (E 0h , ∅)), and so, it does not invalidate (ii). Moreover, as assignments and guards do not modify the scheduler state, the subsequent sched application has no effect. Consider now the case where s is a synchronization primitive. Then (i) holds as these primitives do not modify the error set. We now prove (ii). Given

Given t ∈ T , we apply (ii) on (h 1 , ρ 1 ) and p , and get a state (c 1 , ρ 1 ) ∈ R(Π C proj t (p ), t (E 0c , ∅, I C )) with c 1 ∈ α t (h 1 ). We will note (l 1 , u 1 , -) the components of c 1 . We construct a state in C × E satisfying (ii) for p. We first study the case where t = t and consider several sub-cases depending on s :

• Case s = yield. We have ρ 1 = ρ and α t (h 1 ) = α t (h). We choose c = (l 1 , ∅, weak ). Then (c, ρ 1 ) ∈ R(S C s , t ({ (c 1 , ρ 1 ) }, Ω, I C )). Moreover, c ∈ α t (h). We also have, ∀c ∈ C : intf (c 1 , c ) =⇒ intf (c, c ). Hence, ∀X ∈ V : either ρ(X) = ρ 1 (X), or ρ 1 (X) comes from some weakly consistent interference not in exclusion with c 1 , and so, not in exclusion with c. As a consequence, (c, ρ 1 ) satisfies (ii) for p .

• Case s = lock(m). We choose c = (l 1 ∪ {m}, ∅, weak ). This ensures as before that c ∈ α t (h). Moreover, ρ 1 = ρ. We now construct ρ such that

and

-Otherwise, we know that ρ(X) = ρ 1 (X) comes from a weakly consistent interference compatible with c 1 : ∃t , c :

If intf (c, c ) as well, then the same weakly consistent interference is compatible with c and can be applied to ρ . We can thus set ρ (X) = ρ 1 (X). -Otherwise, as intf (c, c ) does not hold, then either m ∈ l or m ∈ u , where (l , u , -) = c . Assume that m ∈ l , i.e., ρ 1 (X) was written to X by thread t while holding the mutex m. Because R(Π H p (E 0h , ∅)) = ∅, the mutex m is unlocked before t executes s = lock(m), so, t executes unlock(m) at some point in an environment mapping X to ρ 1 (X). Note that S C unlock(m), t calls out to convert the weakly consistent interference (t , c , X, ρ 1 (X)) ∈ I C to a well synchronized interference (t , (l \{m}, u , sync(m)), X, ρ 1 (X)) ∈ I C . This interference is then imported by S C lock(m), t through in. Thus:

and we can set ρ (X) = ρ 1 (X) = ρ(X).

The case where m ∈ u is similar, except that the weakly consistent interference is converted to a well synchronized one by a statement S C yield, t or S C unlock(m ), t for an arbitrary mutex m , in an environment where X maps to ρ 1 (X). In all three cases, (c, ρ ) satisfies (ii) for p .

• Case s = unlock(m). We have ρ 1 = ρ. We choose c = (l 1 \ {m}, u 1 , weak ), which implies c ∈ α t (h). Moreover, as in the case of yield, ∀c : intf (c 1 , c ) =⇒ intf (c, c ). Similarly, (c, ρ 1 ) satisfies (ii) for p .

Otherwise, if ρ(X) = 0, we set c = (l 1 , u 1 ∪ {m}, weak ) and, if ρ(X) = 1, we set c = (l 1 , u 1 \ {m}, weak ), so that c ∈ α t (h). Moreover, when ρ(X) = 0, then ρ is constructed as in the case of lock(m), except that ρ (X) is set to 0. Likewise, the case ρ(X) = 1 is similar to that of yield and unlock(m), except that we also set ρ = ρ 1 [X → 1]. In all cases (c, ρ ) satisfies (ii) for p .

We now study the case t = t , which implies proj t (p) = proj t (p ). We prove that, in each case, (c 1 , ρ 1 ) satisfies (ii) for p:

• Case s = yield. We have ρ 1 = ρ and α t (h 1 ) = α t (h).

• Case s = lock(m). We have ρ 1 = ρ. In order ensure that c 1 ∈ α t (h), we need to ensure that m / ∈ u 1 . We note that, by definition of S C , a configuration with m ∈ u 1 can only be reached if the control path proj t (p ) executed by the thread t contains some X ← islocked(m) statement not followed by any lock(m) nor yield statement, and no thread t > t locks m. We deduce that t < t. Hence, the interleaved control path p preempts the thread t after a non-blocking operation to schedule a lower-priority thread t . This is forbidden by the enabled function: we have R(enabled t (Π H p (E 0h , ∅))) = ∅, hence R(Π H p (E 0h , ∅)) = ∅.

• Case s = unlock(m). We have ρ 1 = ρ and α t (h 1 ) ⊆ α t (h).

• Case s = X ← islocked(m). We have α t (h 1 ) = α t (h). Moreover, ∀Y = X : ρ 1 (Y ) = ρ(Y ) and ρ(X) ∈ {0, 1}. To prove that (ii) holds, it is sufficient to prove that ∃t , c : t = t , (t , c , X, ρ(X)) ∈ I C and intf (c 1 , c ), so that the value of ρ(X) can be seen as an interference from some t in t. We choose t = t . Moreover, as c , we choose the configuration obtained by applying the recurrence hypothesis (ii) to p on (h 1 , ρ 1 ), but t instead of t. We deduce then by, definition of S C X ← islocked(m), t on the configuration c , that there exist interferences (t , c , X, 0), (t , c , X, 1) ∈ I C .

This ends the proof that P H ⊆ P C .

We now prove that P H ⊆ P C . The proof is similar to A.7. Given an original path p and the transformed path p of a thread t, given any (R, Ω, I) such that I is consistent with fresh and local variables, we