Kshitij Bansal

Stéphane Demri

Model-Checking Bounded Multi-Pushdown Systems

We provide complexity characterizations of model checking multi-pushdown systems. We consider three standard notions for boundedness: context boundedness, phase boundedness and stack ordering. The logical formalism is a linear-time temporal logic extending well-known logic CaRet but dedicated to multi-pushdown systems in which abstract operators are parameterized by stacks. We show that the problem is ExpTime-complete for context-bounded runs and unary encoding of the number of context switches; we also prove that the problem is 2ExpTimecomplete for phase-bounded runs and unary encoding of the number of phase switches. In both cases, the value k is given as an input, which makes a substantial difference in the complexity.

Introduction

Verification problems for pushdown systems, systems with a finite automaton and an unbounded stack, have been extensively studied and decidability can be obtained as in the case for finite-state systems. For instance, computing pre (X) (set of configurations reaching a regular set X), post (X) (correspondingly, configurations accessible from X), reachability and LTL model checking have been shown to be decidable [START_REF] Bouajjani | Reachability analysis of pushdown automata: application to model-checking[END_REF][START_REF] Schwoon | Model-checking pushdown systems[END_REF]. These have also been implemented, for instance in the model-checker Moped [START_REF] Schwoon | Model-checking pushdown systems[END_REF]. It can be argued that they are natural models for modeling recursive programs. Two limitations though of the model are the inability to model programs with infinite domains (like integers) and modeling concurrency. Having an infinite automaton to handle the former limitation leads to undecidability. An approach to tackle this has been to abstract infinite-state programs to Boolean programs using, for instance, predicate abstraction. The model is repeatedly refined, as needed, like in tools SLAM, SatAbs etc. For concurrency, a natural way to extend this model would be to consider pushdown automata with multiple stacks, which has seen significant interest in the recent past [START_REF] Atig | Global model checking of ordered multi-pushdown systems[END_REF][START_REF] Bollig | Temporal logics for concurrent recursive programs: Satisfiability and model checking[END_REF][START_REF] Cyriac | MSO decidability of multi-pushdown systems via split-width[END_REF][START_REF] Esparza | Complexity of pattern-based verification for multithreaded programs[END_REF]. This is the main object of study in this paper which we call multi-pushdown systems (MPDS).

The difficulty of model-checking MPDS is that a pushdown system with even two stacks and with a singleton stack alphabet is sufficient to model a Turing machine, hence making the problem of even testing reachability undecidable. This is not a unique situation and similar issues exists with other abstractions, like model-checking problems on counter systems; other models of multithreaded programs are also known to admit undecidable verification problems. That is why subclasses of runs have been introduced as well as problems related to the search for 'bounded runs' that may satisfy a desirable or undesirable property. For instance, context-bounded model-checking (bound on the number of context switches) [START_REF] Qaader | Context-bounded model checking of concurrent software[END_REF] allows to regain decidability.

This paper focuses on the study of model-checking problems for MPDS based on LTL-like dialects, naturally allowing to express liveness properties, when some bounds are fixed. Though decidability of these problems has been established in some recent works we aim to provide optimal computational complexity analysis for LTL-like properties. In particular, we consider a LTL-like specification language based on CaRet [START_REF] Alur | A temporal logic of nested calls and returns[END_REF], which strikes to us as fitting given the interest of the model in program verification. As in [START_REF] Torre | A temporal logic for multi-threaded programs[END_REF], CaRet generalized to multiple stacks and called Multi-CaRet is considered. Under this logic, we show modelchecking problem of MPDS restricted to k-context bounded runs is in Exp-Time, when k is encoded in unary. Since this problem is a generalization of LTL model checking pushdown systems which is known to be ExpTime-hard, this is an optimal result. Viewed as an extension of [START_REF] Bouajjani | Reachability analysis of pushdown automata: application to model-checking[END_REF], we consider both a more general model and a more general logic, while still preserving the complexity bounds. At a technical level, we focus on combining several approaches in order to achieve optimal complexity bounds. In particular, we combine the approach taken in CaRet model-checking of recursive state machines machines, ideas from reachability analysis of multi-pushdown systems [START_REF] Schwoon | Model-checking pushdown systems[END_REF] and the techniques introduced in [START_REF] Bouajjani | Reachability analysis of pushdown automata: application to model-checking[END_REF][START_REF] Schwoon | Model-checking pushdown systems[END_REF]. We also consider less restrictive notions, showing optimal 2-ExpTime for k-phase bounded runs [START_REF] La Torre | A robust class of context-sensitive languages[END_REF] when k is in unary. Note that in all restrictions we consider, k is given as an input and not as a parameter of the problem, which makes a substantial difference when complexity analysis is provided. When k is encoded in binary, the bounds are 2-ExpTime and 3-ExpTime for context and phase boundedness respectively. For a third notion of ordered multi-pushdown systems [START_REF] Atig | Emptiness of multi-pushdown automata is 2ETIME-complete[END_REF], model-checking is in 2ExpTime.

Related work.

In [START_REF] Madhusudan | The tree width of auxiliary storage[END_REF], decidability results are found for classes of automata with auxiliary storage based on MSO property, see also [START_REF] Torre | Scope-bounded multistack pushdown systems: fixedpoint, sequentialization and tree-width[END_REF]. This includes MPDS with bounded context and ordered MPDS. Unlike our ExpTime bound, the complexity is non-elementary in the size of the formula. This stems from the use of celebrated Courcelle's Theorem, which has parameterized complexity non-elementary, the parameter being the size of formula plus the tree-width.

More closely related to our approach of generalizing the automata-based approach for LTL are two recent works [START_REF] Atig | Linear-time model-cheking for multithreaded programs under scope-bounding[END_REF][START_REF] Torre | A temporal logic for multi-threaded programs[END_REF]; indeed model-checking of linear-time properties for MPDS under several boundedness hypothesis has been the subject of several recent studies. In [START_REF] Atig | Linear-time model-cheking for multithreaded programs under scope-bounding[END_REF], LTL model-checking on multi-pushdown systems when runs are k-scope-bounded is shown ExpTime-complete. Scopeboundedness strictly extends context-boundedness and therefore Corollary 7(I) and [START_REF] Atig | Linear-time model-cheking for multithreaded programs under scope-bounding[END_REF]Theorem 7] are closely related even though Corollary 7(I) deals with the richer Multi-CaRet and it takes into account specifically context-boundedness. By contrast, [START_REF] Torre | A temporal logic for multi-threaded programs[END_REF] introduces an extension of CaRet that is expressively identical to the variant we consider in our paper (models are multiply nested words). Again, it deals with scope-boundedness and Corollary 7(I) and [START_REF] Torre | A temporal logic for multi-threaded programs[END_REF]Theorem 6] are closely related even though Corollary 7(I) takes into account contextboundedness specifically, which leads to a slightly different result. Similarly, upper bounds [START_REF] Torre | A temporal logic for multi-threaded programs[END_REF]Theorem 7] about ordered multiply nested words, is related to upper bound we provide in Corollary 8 for OBMC. Nevertheless, as technical contributions, we first deal with context-boundedness, phase-boundedness and ordered MPDS uniformly independent of the notion of boundedness by following an automata-based approach reducing to the corresponding repeated reachability problem. In second step, we provide optimal complexity bounds by building on analysis for context-boundedness on [START_REF] Bouajjani | Reachability analysis of pushdown automata: application to model-checking[END_REF][START_REF] Schwoon | Model-checking pushdown systems[END_REF] whereas for ordered MPDS it relies on [START_REF] Atig | Global model checking of ordered multi-pushdown systems[END_REF]. Finally, our construction allows us to add regularity constraints on stack contents, extending notions from [START_REF] Esparza | Model-checking LTL with regular valuations for pushdown systems[END_REF], that are known to go beyond first-order language, by an adaptation of the case for Multi-CaRet.

Preliminaries

We write [N ] to denote the set {1, 2, . . . , N }. We also use a boldface as a shorthand for elements indexed by [N ], for e.g., a = {a i | i ∈ [N ]}. For a finite word w = a 1 . . . a k over the alphabet Σ, we write |w| to denote its length k. For 0 ≤ i < |w|, w(i) represents the (i + 1)-th letter of the word, here a i+1 .

Pushdown systems provide a natural execution model for programs with recursion. A generalization with multiple stacks allows us to model threads, formally defined next. A multi-pushdown system (MPDS) is a tuple of the form P = (G, N, Γ, ∆ 1 , . . . , ∆ N ), for some N ≥ 1 such that G is a non-empty finite set of global states, Γ is the finite stack alphabet containing the distinguished letter ⊥, for every s ∈ [N ], ∆ s is the transition relation acting on the s-th stack where ∆ s is a relation included in G × Γ × G × A(Γ ) with A(Γ ) defined as A(Γ ) def = a∈Γ {call(a), return(a), internal(a)}. Elements of the set A(Γ ) are to be thought of as actions modifying the stack with alphabet Γ . A configuration c of P is the global state along with contents of the N stacks, i.e. c belongs to G × (Γ * ) N . For every s ∈ [N ], we write -→ s to denote the one-step relation w.r.t. the s-th stack. Given two configurations c = (g, w 1 , . . . , w s a, . . . w N ) and c = (g , w 1 , . . . , w s , . . . , w N ), c -→ s c iff (g, a, g , a(b)) ∈ ∆ s where a(b) reflects the change in the stack enforcing one of the conditions below: w s = w s , a = return and a = b, or w s = w s b and a = internal, or w s = w s ab and a = call. The letter ⊥ from the stack alphabet plays a special role; indeed the initial content of each stack is precisely ⊥. Moreover, ⊥ cannot be pushed, popped or replaced by any other symbol. This is a standard way to constrain the transition relations and to check for 'emptiness' of the stack. We write -→ P to denote the relation

( s∈[N ] - → s ). Given a configuration c, there may exist c 1 , c 2 and i 1 = i 2 ∈ [N ] such that c - → i1 c 1 and c - → i2 c 2 ,
which is the fundamental property to consider such models as adequate for modeling concurrency. An infinite run is an ω-sequence of configurations c 0 , c 1 , c 2 , . . . s.t. for every i ≥ 0, we have c i -→ P c i+1 . If c i -→ s c i+1 , then we say that for that step, the s-th stack is active. Similar notions can be defined for finite runs. A standard problem on MPDS is the state reachability problem: given a MPDS P , a configuration c and a global state g, is there a run from c to some configuration c s.t. the state of c is g?

An enhanced multi-pushdown system is a multi-pushdown system of the form

P = (G × [N ] , N, Γ, ∆ 1 , . . . , ∆ N ) s.t. for every s ∈ [N ], ∆ s ⊆ (G × {s}) × Γ × (G × [N ]) × A(Γ ).
In such systems, the global state contains enough information to determine the next active stack. Observe that the way the one-step relation is defined, we do not necessarily need to carry this information as part of the finite control (see Lemma 1). We do that in order to enable us to assert about active stack in our logic (see Section 3), and for technical convenience.

Lemma 1. Given P = (G, N, Γ, ∆), one can construct in polynomial time an enhanced P = (G × [N ] , N, Γ, ∆ ) such that (I) for every infinite run of P of the form c 0 - → s0 c 1 - → s1 • • • c t - → st c t+1 • • • there is an infinite run c 0 - → s0 c 1 - → s1 • • • c t - → st c t+1 • • • of P such that ( ) for t ≥ 0, if c t = (g t , {w t s } s ), then c t = ((g t , s t ) , {w t s } s ) and (II) similarly, for every infinite run of P of the form c 0 - → s0 c 1 - → s1 • • • c t - → st c t+1 • • • there is an infinite run c 0 - → s0 c 1 - → s1 • • • c t - → st c t+1 • • • of P such that ( ).
The proof is by an easy verification. In the sequel, w.l.o.g., we consider enhanced MPDS only since all the properties that can be expressed in our logical languages are linear-time properties. For instance, there is a logspace reduction from the state reachability problem to its restriction to enhanced MPDS.

State reachability problem is known to be undecidable by a simple reduction from the non-emptiness problem for intersection of context-free grammars. This has motivated works on restrictions on runs so that decidability can be regained (for state reachability problem and for model-checking problems). We recall below standard notions for boundedness; other notions can be found in [START_REF] Torre | Reachability of multistack pushdown systems with scope-bounded matching relations[END_REF][START_REF] Cyriac | MSO decidability of multi-pushdown systems via split-width[END_REF]. Definitions are provided for infinite runs but they can be adapted to finite runs.

For the notion of k-boundedness, a phase is understood as a sub-run such that a single stack is active (see e.g. [START_REF] Qaader | Context-bounded model checking of concurrent software[END_REF]). Let

ρ = c 0 - → s0 c 1 - → s1 • • • c t - → st c t+1 • • • be an infinite run and k ≥ 0. We say that ρ is k-bounded if there exist positions i 1 ≤ i 2 ≤ . . . ≤ i k-1 such that s t = s t+1 for all t ∈ N \ {i 1 . . . i k-1 }.
In the notion of k-phase-boundednessdefined below, a phase is understood as a subrun such that return actions are performed on a single stack, see e.g. [START_REF] La Torre | A robust class of context-sensitive languages[END_REF]. Let

ρ = c 0 - → s0 c 1 - → s1 • • • c t - → st c t+1 • • • be an infinite run and k ≥ 0. We say that ρ is k-phase-bounded if there is a partition Y 1 , . . . , Y α of N with α ≤ k such that for every j ∈ [1, α] there is s ∈ [N ] s.t.
for every i ∈ Y j , if a return action is performed from c i to c i+1 , then it is done on the sth stack. Finally, in the notion of order-boundedness defined below, the stacks are linearly ordered and a return action on a stack can only be performed if the smallest stacks are empty, see e.g. [START_REF] Atig | Emptiness of multi-pushdown automata is 2ETIME-complete[END_REF]. Let P be a multi-pushdown system and = ([N ] , ≤) be a total ordering.

Let ρ = c 0 - → s0 c 1 - → s1 • • • c t - → st c t+1 • • • be an infinite run.
We say that ρ is -bounded if for every t ∈ N that a return is performed on the s-th stack, all the stacks strictly smaller than s w.r.t. are empty.

Specification Language Multi-CaRet

Below, we introduce Multi-CaRet, an extension of the logic CaRet proposed in [START_REF] Alur | A temporal logic of nested calls and returns[END_REF], and dedicated to runs of MPDS (instead of for runs of recursive state machines as done in [START_REF] Alur | A temporal logic of nested calls and returns[END_REF]). The logic below can be seen as a fragment of MSO and therefore the decidability results from [START_REF] Bollig | Temporal logics for concurrent recursive programs: Satisfiability and model checking[END_REF][START_REF] Madhusudan | The tree width of auxiliary storage[END_REF] apply to the forthcoming model-checking problems. However, our definition makes a compromise between a language of linear properties that extends the logic from [START_REF] Alur | A temporal logic of nested calls and returns[END_REF] and the most expressive logic for which our model-checking problems are known to be decidable. The logic below is expressively identical as well as syntactically and semantically similar to one in [START_REF] Torre | A temporal logic for multi-threaded programs[END_REF], except for the presence of regular constraints.

Models of Multi-CaRet are infinite runs of multi-pushdown systems. For each (enhanced) multi-pushdown system P = (G × [N ] , N, Γ, ∆ 1 , . . . , ∆ N ), the fragment Multi-CaRet(P ) of CaRet that uses syntactic resources from P (namely G and [N ]). Multi-CaRet is defined as the union of all the sub-languages Multi-CaRet(P ). The grammar φ :

= g | s | call | return | internal | φ ∨ φ | ¬φ | Xφ | φUφ | X a s φ | φU a s φ | X c s φ | φU c s φ, defines formulas of Multi-CaRet(P ), with s ∈ [N ], g ∈ G. Models of Multi-CaRet(P ) formulae are ω-sequences in G × [N ] × (Γ * ) N ω ,
which can be obviously understood as infinite runs of P .

Semantics. Given an infinite run ρ = c 0 c 1 . . . c t . . . with c t = (g t , s t , w t 1 , . . . , w t N ) for every position t ∈ N, the satisfaction relation ρ, t |= φ with φ in Multi-CaRet(P ) is defined inductively as follows (successor relations are defined just below and obvious clauses are omitted):

ρ, t
ρ, t |= X b s φ iff succ b,s ρ (t) is defined and ρ, succ b,s ρ (t) |= φ ρ, t |= φ 1 U a s φ 2 iff there exists a sequence of positions t ≤ i 0 < i 1 • • • < i k , where i 0 smallest such with s i0 = s, for j < k, i j+1 = succ a,s ρ (i j ), ρ, i j |= φ 1 and ρ, i k |= φ 2 ρ, t |= φ 1 U c s φ 2 iff there exists a sequence of positions t ≥ i 0 > i 1 • • • > i k
, where i 0 greatest such with s i0 = s, for Adding regularity constraints. We define Multi-CaRet reg as the extension of Multi-CaRet in which regularity constraints on stack contents can be expressed. Logic Multi-CaRet reg is defined from Multi-CaRet by adding atomic formulae of the form in(s, A) where s is a stack identifier and A is a finite-state automaton over the stack alphabet Γ . The satisfaction relation |= is extended accordingly: ρ, t |= in(s, A) iff w t s ∈ L(A) where L(A) is the set of finite words accepted by A. Note that regularity constraints can be expressed on each stack.

j < k, i j+1 = succ c,s ρ (i j ), ρ, i j |=
Let us introduce the model-checking problems considered herein. The modelchecking problem for MPDS (MC) is defined s.t. it takes as inputs a MPDS P , a configuration g, (⊥) N and a formula φ in Multi-CaRet(P ) and asks whether there is an infinite run ρ from g, (⊥) N such that ρ |= φ. We know that the model-checking problem for MPDS is undecidable whereas its restriction to a single stack is ExpTime-complete [START_REF] Alur | A temporal logic of nested calls and returns[END_REF]. Now, let us turn to bounded model-checking problems. Bounded model-checking problem for MPDS (BMC) is defined such that it takes as inputs P , a configuration g, (⊥) N , a formula φ in Multi-CaRet(P ) and a bound k ∈ N and it asks whether there is an infinite k-bounded run ρ from g, (⊥) N such that ρ |= φ. Note that k ∈ N is an input and not a parameter of BMC. This makes a significant difference for complexity since usually complexity can increase when passing from being a constant to being an input. Phase-bounded model-checking problem (PBMC) is defined similarly by replacing in the above definition 'k-bounded run' by 'k-phase-bounded run'. Similarly, we can obtain a definition with order-boundedness. Order-bounded modelchecking problem for multi-pushdown systems (OBMC) is defined such that it takes as inputs P , a configuration g, (⊥) N , a formula φ in Multi-CaRet(P ) and a total ordering = ([N ] , ≤) and it asks whether there is an infinite -bounded run ρ from g, (⊥) N such that ρ |= φ.

The problem of repeated reachability of MPDS, written REP, is defined in the expected way with a generalized Büchi acceptance condition related to states. We refer to the problem restricted to k-bounded runs by BREP. Obviously, the variants with other notions of boundedness can be defined too. Now, the simplified version of Multi-CaRet consists of the restriction of Multi-CaRet in which atomic formulae are of the form (g, s) when enhanced MPDS are involved. For every P in {MC,BMC,PBMC,OBMC}, there is a logspace reduction to P restricted to formulae from the simplified language. The proof idea consists in adding to global states information about the next active stack and about the type of action. In the sequel, w.l.o.g., we restrict ourselves to the simplified languages. By [START_REF] Madhusudan | The tree width of auxiliary storage[END_REF], we conclude that BMC, PBMC and OBMC are decidable (use of Courcelle's Theorem). However, it provides non-elementary upper bounds. As a main result of our paper, we show that BMC is ExpTime-complete when k is encoded in unary even in presence of regular constraints.

From Model-Checking to Repeated Reachability

Herein, we reduce the problem of model checking (MC) to the problem of repeated reachability (REP) while noting complexity features that are helpful later on (Theorem 4). This generalizes Vardi-Wolper reduction from LTL modelchecking into non-emptiness for generalized Büchi automata, similarly to the approach followed in [START_REF] Torre | A temporal logic for multi-threaded programs[END_REF]; not only we have to tailor the reduction to Multi-CaRet and to MPDS but also we aim at getting tight complexity bounds afterwards. The instance of MC that we have is a MPDS P , a formula φ and initial state (g 0 , i 0 ). For the instance of REP we will reduce to, we will denote the MPDS by P , the set of acceptance sets by F and the set of initial states by I 0 .

Augmented Runs. Let ρ be a run of the multi-pushdown system

P = (G × [N ] , N, Γ, ∆) with ρ ∈ (G × [N ] × (Γ * ) N ) ω .
The multi-pushdown system P is built in such a way that its runs correspond exactly to runs from P but augmented with pieces of information related to the satisfaction of subformulas (taken from the closure set Cl(φ) elaborated on shortly), whether a stack is dead or not (using a tag from {alive, dead}) and whether the current call will ever be returned or not (using a tag from {noreturn, willreturn}). These additional tags will suffice to reduce the existence of a run satisfying φ to the existence of a run satisfying a generalized Büchi condition. First, we define from ρ an "augmented run" γ(ρ) which is an infinite sequence from ( G × [N ] × ( Γ * ) N ) ω where G = G × P(Cl(φ)) N × {noreturn, willreturn} N × {alive, dead} N and Γ = Γ × P(Cl(φ)) × {noreturn, willreturn}. By definition, an augmented run is simply an ω-sequence but it remains to check that indeed, it will be also a run of the new system. We will see that G × [N ] is the set of global states of P and Γ is the stack alphabet of P . Before defining γ(•) which maps runs to augmented runs, let us introduce the standard notion for closure but slightly tailored to our needs. Each global state is partially made of sets of formulas that can be viewed as future obligations. This is similar to what is done for LTL and is just a variant of Fischer-Ladner closure. An obligation for a stack is a set of subformulas that is locally consistent; such consistent sets are called atoms and they are defined below as well as the notion of closure. Given a formula φ, its closure, denoted Cl(φ), is the smallest set that contains φ, the elements of G × [N ], and satisfies the following properties (b ∈ {a, c} and s ∈

[N ]): (i) if ¬φ ∈ Cl(φ) or Xφ ∈ Cl(φ) or X b s φ ∈ Cl(φ) then φ ∈ Cl(φ); (ii) if φ ∨ φ ∈ Cl(φ), then φ , φ ∈ Cl(φ); (iii) if φ Uφ ∈ Cl(φ), then φ , φ , and X(φ Uφ ) are in Cl(φ); (iv) if φ U b s φ ∈ Cl(φ), then φ , φ , and X b s (φ U b s φ ) are in Cl(φ); (v) if φ ∈ Cl(φ)
and φ in not of the form ¬φ , then ¬φ ∈ Cl(φ). The number of formulas in Cl(φ) is linear in the size of φ and P . An atom of φ, is a set A ⊆ Cl(φ) that satisfies the following properties: (a) for ¬φ ∈ Cl(φ),

φ ∈ A iff ¬φ / ∈ A; (b) or φ ∨ φ ∈ Cl(φ), φ ∨ φ ∈ A iff (φ ∈ A or φ ∈ A); (c) or φ Uφ ∈ Cl(φ), φ Uφ ∈ A iff φ ∈ A or (φ ∈ A and X(φ Uφ ) ∈ A); (d) A contains exactly one element from G × [N ].
Let Atoms(φ) denote the set of atoms of φ, along with empty set (used as special atom, use will become clear later). Note that there are 2 O(|φ|) atoms of φ.

We write ((g t , s t ), w t ) to denote the t-th configuration of ρ. We define the augmented run γ(ρ) so that its t-th configuration is of the form (( g t , s t ), w t ) with g t = (g t , A t , r t , d t ) and w t j = (w t j , v t j , u t j ) for every j in [N ]. We say that the stack j is active at time t if s t = j. Then, we define dead-alive tag to be dead if and only if the stack is not active at or after the corresponding position. The idea of the closure as we discussed is to maintain the set of subformulas that hold true at each step. We will expect it to be the empty set if the stack is dead. As for willreturn-noreturn tag, it reflects whether a call action has a "matching" return. This is similar to the {∞, ret} tags in [START_REF] Alur | A temporal logic of nested calls and returns[END_REF]. This may be done by defining tag to be noreturn if stack will never become smaller than what it is now. Finally, the formulas and willreturn-noreturn tag on the stack are defined to be what they were in the global state at the time when the corresponding letter was pushed.

∀t ≥ 0, j ∈ [N ] : (d t j = dead) def ⇔ (∀t ≥ t, s t = j). (1)
∀t ≥ 0, j ∈ [N ] with d t j = alive, ψ ∈ Cl(φ): ψ ∈ A t j def ⇔ ρ, t |= ψ where t is the least t ≥ t with s t = j. (2)
∀t ≥ 0, j ∈ [N ] with d t j = dead:

A t j def = ∅. (3
= k -1. (5)
Construction. We construct a system which simulates the original system with accepting runs having augmentations faithful to the semantics described above in (1)- [START_REF] Bansal | A note on the complexity of model-checking bounded multi-pushdown systems[END_REF]. We define the multi-pushdown system P as ( G × [N ] , N, Γ , ∆) with the states and alphabet as defined earlier, and each transition relation ∆ s is defined s.t. ( g, s, a, g , s , a( a )) is in ∆ s def ⇔ conditions from Fig. 1 are satisfied. The set F is defined by the following sets of accepting states:

(a) For each ψ = φ 1 Uφ 2 ∈ Cl(φ), we define F 1 ψ def = {( g, s) | φ 2 ∈ A s or ψ / ∈ A s }. (b) For each abstract-until formula ψ = φ 1 U a s φ 2 ∈ Cl(φ), we define F 2 ψ def = {( g, s) | r s = noreturn and (φ 2 ∈ A s or ψ / ∈ A s )}. (c) For each j ∈ [N ], we define F 3 j def = {( g, s) | j = s} ∪ {( g, s) | d j = dead}. (d) For each j ∈ [N ], F 4 j def = {( g, s) | d j = dead} ∪ {( g, s) | j = s, d s = noreturn}.
Lemma 2. Let ρ be a run of P . Then, γ(ρ) is a run of P such that for every F ∈ F, there is a global state in F that is repeated infinitely often. Lemma 3. Let ρ be a run of P satisfying the acceptance condition F. Then, ρ projected over states of P , denoted Π( ρ), is a run of P and γ(Π( ρ)) = ρ.

From Lemmas 2 and 3 the soundness and completeness of the reduction follow if we define the set of new initial states I 0 for the REP problem as states with initial state (g 0 , i 0 ) for the MC problem and φ present in the part tracking formulas that hold true: I 0 = {((g 0 , A, d, r), i 0 ) | φ ∈ A i0 }. This gives an exponentialtime reduction from MC to REP as well as their bounded variants. Theorem 4 below can be viewed as a counterpart of [14, Theorem 3].

Theorem 4. Let P be a MPDS with initial configuration (g, (⊥) N ) and φ be a Multi-CaRet formula. Let P be the system built from P , g and φ, I 0 be the associated set of initial states and F be the acceptance condition. (I) If ρ 1 is a run of P from (g, (⊥) N ) then ρ 2 = γ(ρ 1 ) is a run of P satisfying F and (A)-(C) hold true. (II) If ρ 2 is a run of P from some configuration with global state in I 0 and satisfying F, then Π(ρ 2 ) is a run of P and (A)-(C) hold true too.

Conditions (A)-(C) are defined as follows:

(A) ρ 1 is k-bounded iff ρ 2 is k- bounded, for all k ≥ 0; (B) ρ 1 is k-phase-bounded iff ρ 2 is k-phase-bounded, for all k ≥ 0; (C) ρ 1 is -bounded iff ρ 2 is -bounded, for all total orderings of the stacks = ([N ] , ≤).
Note that at each position, ρ 1 and ρ 2 work on the same stack and perform the same type of action (call, return, internal move), possibly with slightly different letters. This is sufficient to guarantee the satisfaction of the conditions (A)-(C).

Complexity Analysis with Bounded Runs

Bounded Repeated Global State Reachability Problem. We evaluate the complexity of BREP as well as its variant restricted to a single accepting global state, written BREP single . There is a logspace reduction from BREP to BREP single by copying the MPDS as many times as the cardinality of F (as done to reduce non-emptiness problem for generalized Büchi automata to nonemptiness problem for standard Büchi automata). This allows us to conclude about the complexity upper bound for BMC itself but it is worth noting that the MPDS obtained by synchronization has an exponential number of global states and therefore a refined complexity analysis is required to get optimal upper bounds. In order to analyze the complexity for BREP single , we take advantage of proof techniques that are introduced earlier and for which we provide a complexity analysis that will suit our final goal. Namely, existence of an infinite k-bounded run s.t. a final global state (g f , i f ) is repeated infinitely often is checked: (1) by first guessing a sequence of intermediate global states witnessing context switches of length at most k + 1, (2) by computing the (regular) set of reachable configurations following that sequence and then (3) by verifying whether there is a reachable configuration leading to an infinite run s.t. (g f , i f ) is repeated infinitely often and no stack switch is performed. The principle behind (2) is best explained in [START_REF] Qaader | Context-bounded model checking of concurrent software[END_REF] but we provide a complexity analysis using the computation of post (X) along the lines of [START_REF] Schwoon | Model-checking pushdown systems[END_REF]. Sets post (X) need to be computed at most k times, which might cause an exponential blow-up (for instance if at each step the number of states were multiplied by a constant). Actually, computing post adds an additive factor at each step, which is essential for our analysis. Let us define BREP single : it takes as inputs P , a configuration (g, i) , (⊥) N , a global state (g f , i f ) and k ∈ N and it asks whether there is an infinite k-bounded run ρ from (g, i) , (⊥) N s.t. (g f , i f ) is repeated infinitely often. The proof of Proposition 5 is at the heart of our complexity analysis and it relies on constructions from [START_REF] Bouajjani | Reachability analysis of pushdown automata: application to model-checking[END_REF][START_REF] Schwoon | Model-checking pushdown systems[END_REF]. We take advantage of it with the input system P . Note that [START_REF] Bollig | Temporal logics for concurrent recursive programs: Satisfiability and model checking[END_REF]Theorem 15] would lead to an ExpTime upper bound for BMC if k is not part of the input, see the ExpTime upper bound for the problem NESTED-TRACE-SAT(L -, k) from [START_REF] Bollig | Temporal logics for concurrent recursive programs: Satisfiability and model checking[END_REF]; in our case k is indeed part of the input and in that case, the developments in [START_REF] Bollig | Temporal logics for concurrent recursive programs: Satisfiability and model checking[END_REF] will lead to a 2ExpTime bound by using the method used for NESTED-TRACE-SAT(L -, k) even if k is encoded in unary. Indeed, somewhere in the proof, the path expression succ ≤k is exponential in the value k. Hence, Corollary 6(I) is the best we can hope for when k is part of the input of the model-checking problem. We write BMC reg to denote the extension of BMC in which Multi-CaRet is replaced by Multi-CaRet reg .

CaRet in which abstract temporal operators are related to calls and returns and parameterized by the stacks, and regularity constraints on stack contents are present too. A 2ExpTime upper bound is also established with ordered MPDS or with k-phase bounded runs.

  1. ((g, s), aS, (g , s ), a(a S )) ∈ ∆s 2. ds = alive 3. ∀j = s, dj = d j 4. If a = call, then rs = willreturn ⇒ r s = willreturn and a r = rs 5. If a = internal, then r s = rs and a r = ar 6. If a = return, then rs = willreturn and r s = ar 7. ∀j = s, rj = r j 8. (g, s) ∈ As 9. ∀j = s, Aj = A j 10. XAs ⊆ A s (= A s ) 11. If a = call, then a A = As 12. If a = internal, then X a s As ⊆ A s and a A = aA. 13. If a = return, then X a s aA ⊆ A s 14. Further, X a s As = ∅ if (a) a = call and rs = noreturn, or (b) a = return, or (c) d s = dead 15. If a = call, X c s A s = (X c s Atoms(φ)) ∩ As 16. If a = internal, then X c s A s = X c s As. 17. Let b ∈ {a, c}. Let ψ ∈ Cl(φ), ψ = φ1U b s φ2. Then, ψ ∈ As iff either φ2 ∈ As or (φ1 ∈ As and X a s ψ ∈ As). 18. Let b ∈ {a, c}. Let ψ ∈ Cl(φ), ψ = φ1U b j φ2 with j = s. Then ψ ∈ As iff ψ ∈ A s . 19. ∀j: If dj = dead, then Aj = ∅ and rj = noreturn.

Fig. 1 .

 1 Fig. 1. Conditions for ∆s. XA = {ψ | Xψ ∈ A}, X a 1 A = {ψ | X a 1 ψ ∈ A} and a = (aS, aA, ar) (similarly, a ).

Proposition 5 .

 5 BREP single can be solved in time O(|P | k+1 ×p(k, |P |)) for some polynomial p(•, •).

Corollary 6 .

 6 (I) BMC with k encoded with a unary representation is Exp-Time-complete. (II) BMC with k in binary encoding is in 2 ExpTime.

  φ 1 and ρ, i k |= φ 2 Definition for |= uses three successor relations: global successor relation, abstract successor relation that jumps to the first future position after a return action at the same level, if any, and the caller successor relation that jumps to the latest past position before a call action at the same level, if any. Here are the definitions: succ ρ (t) t s.t. s t = s and w t s = |w t s | -1. If such a t does not exist, then succ c,s ρ (t) is undefined; and succ a,s ρ (t) is defined when s is active at position t:

	1. If w t+1 s	= |w t s | + 1 (call), then succ a,s ρ (t) is the smallest t > t such that
	s t = s and w t s = |w t s |. If there is no such t then succ a,s ρ (t) is undefined.
	2. If w t+1 s	= |w t s | (internal), then succ a,s ρ (t) is the smallest t > t such that
	s t = s (first position when sth stack is active).
	3. If w t+1 s	= |w t s | -1 (return), then succ a,s ρ (t) is undefined.
	In the sequel, we write ρ |= φ whenever ρ, 0 |= φ.

def

= t + 1 for every t ∈ N; succ c,s ρ (t) (caller of s-th stack): largest t <

  in [l]: t k is largest t k ≤ t such that w t k

				)
	∀t ≥ 0, j ∈ [N ] : (r t j = noreturn)	def ⇔ (∀t ≥ t, w t j ≥ w t j ).	(4)
	∀t ≥ 0, j ∈ [N ] : v t j	def = A t1 j A t2 j . . . A t l j and u t j	def = d t1 j d t2 j . . . d t l j ,
	where for k j

Acknowledgments. We thank the reviewers for their time and helpful comments. K. Bansal also thanks LSV & ENS Cachan (France), and Clark Barrett in New York, for making the internship in Summer 2011 and hence, this work, possible.

 [START_REF] Alur | A temporal logic of nested calls and returns[END_REF]Work partially supported by projects ARCUS IdF/Inde and EU Seventh Framework Programme under grant agreement No. PIOF-GA-2011-301166 (DATAVERIF). 1 Omitted proofs and additional material can be found in the technical report [5].

Complexity Results for Other Boundedness Notions. We focus on the complexity analysis for OBMC and PBMC. Let OREP single be the variant of BREP single with ordered MPDS: it takes as inputs an ordered multi-pushdown system P , a configuration (g, i) , (⊥) N , a global state (g f , i f ) and it asks whether there is an infinite run ρ from (g, i) , (⊥) N such that (g f , i f ) is repeated infinitely often. According to [START_REF] Atig | Global model checking of ordered multi-pushdown systems[END_REF]Theorem 11], OREP single restricted to ordered multi-pushdown systems with k stacks can be checked in time O(|P |

where d is a constant. Our synchronized product P is exponential in the size of formulas (see Section 4), whence OBMC is in 2ExpTime too (k is linear in the size of our initial P ). Condition (C) from Theorem 4 needs to be used here.

Corollary 8. OBMC is in 2ExpTime.

The same complexity upper bound can be shown with regularity constraints. Now, let us consider k-bounded-phase runs. Let us define PBREP single in a similar way: it takes as inputs a MPDS P , a configuration (g, i) , (⊥) N , a global state (g f , i f ) and k ∈ N and it asks whether there is an infinite k-phase-bounded run ρ from (g, i) , (⊥) N such that (g f , i f ) is repeated infinitely often. In [3, Section 5], it is shown that non-emptiness for k-phase MPDS can be reduced to non-emptiness for ordered MPDS with 2k stacks. By inspecting the proof, we can conclude: a similar reduction can be performed for reducing the repeated reachability of a global state, and non-emptiness of k-phase P with N stacks is reduced to non-emptiness of one of N k instances of P with 2k stacks and each P is in polynomial-size in k + |P |. Therefore, PBREP single is in 2ExpTime. Indeed, there is an exponential number of instances and checking non-emptiness for one of them can be done in double exponential time. By combining the different complexity measures above, checking an instance of PBREP single with

) which is double-exponential in the size of P . Consequently, bounded model-checking with bounded-phase MPDS is in 2ExpTime too if the number of phases is encoded in unary. Again, the same complexity upper bounds apply when regularity constraints are added. Note that an alternative proof of Corollary 9(I) can be found in the recent paper [START_REF] Bollig | The complexity of model-checking multistack systems[END_REF] where fragments of MSO are taken into account.

Conclusion

We showed that model-checking over MPDS with k-bounded runs is ExpTimecomplete when k is an input bound encoded in unary, otherwise the problem is in 2ExpTime with a binary encoding. The logical language is a version of


Christian Haack

Marieke Huisman

Clément Hurlin

Reasoning about Java's Reentrant Locks

This paper presents a verification technique for a concurrent Java-like language with reentrant locks. The verification technique is based on permissionaccounting separation logic. As usual, each lock is associated with a resource invariant, i.e., when acquiring the lock the resources are obtained by the thread holding the lock, and when releasing the lock, the resources are released. To accommodate for reentrancy, the notion of lockset is introduced: a multiset of locks held by a thread. Keeping track of the lockset enables the logic to ensure that resources are not re-acquired upon reentrancy, thus avoiding the introduction of new resources in the system. To be able to express flexible locking policies, we combine the verification logic with value-parameterized classes. Verified programs satisfy the following properties: data race freedom, absence of null-dereferencing and partial correctness. The verification technique is illustrated on several examples, including a challenging lock-coupling algorithm.

Introduction

Writing correct concurrent programs, let alone verifying their correctness, is a highly complex task. The complexity is caused by potential thread interference at every program point, which makes this task inherently non-local. To reduce this complexity, concurrent programming languages provide high-level synchronization primitives. The main synchronization primitive of today's most popular modern object-oriented languages -Java and C# -are reentrant locks. While reentrant locks ease concurrent programming, using them correctly remains difficult and their incorrect usage can result in nasty concurrency errors like data races or deadlocks. Multithreaded Java-like languages do not offer enough support to prevent such errors, and are thus an important target for lightweight verification techniques.

An attractive verification technique, based on the regulation of heap space access, is O'Hearn's concurrent separation logic (CSL) [START_REF] O'hearn | Resources, concurrency and local reasoning[END_REF]. In CSL, the programmer formally associates locks with pieces of heap space, and the verification system ensures that a piece of heap space is only accessed when the associated lock is held. This, of course, is an old idea in verification of shared variable concurrent programs [START_REF] Andrews | Concurrent Programming: Principles and Practice[END_REF]. The novelty of CSL is that it generalizes these old ideas in an elegant way to languages with unstructured heaps, thus paving the way from textbook toy languages to realistic programming languages. This path has been further explored by Gotsman et al. [START_REF] Gotsman | Local reasoning for storable locks and threads[END_REF] and Hobor et al. [START_REF] Hobor | Oracle semantics for concurrent separation logic[END_REF], who adapt CSL from O'Hearn's simple concurrent language (with a static set of locks and threads) to languages with dynamic lock and thread creation and concurrency primitives that resemble POSIX threads. However, in these variants of CSL, locks are single-entrant; this paper adapts CSL to a Java-like language with reentrant locks.

Unfortunately, reentrant locks are inherently problematic for separation-logic reasoning, which tries to completely replace "negative" reasoning about the absence of aliasing by "positive" reasoning about the possession of access permissions. The problem is that a verification system for reentrant locks has to distinguish between initial lock entries and reentries, because only after initial entries is it sound to assume a lock's resource invariant. This means that initial lock entries need a precondition requiring that the current thread does not already hold the acquired lock. Establishing this precondition boils down to proving that the acquired lock does not alias a currently held lock, i.e., to proving absence of aliasing.

This does not mean, however, that permission-based reasoning has to be abandoned altogether for reentrant locks. It merely means that permission-based reasoning alone is insufficient. To illustrate this, we modularly specify and verify a finegrained lock-coupling list (where lock reentrancy complicates verification) that has previously been verified with separation logic rules for single-entrant locks [START_REF] Gotsman | Local reasoning for storable locks and threads[END_REF]. This example crucially uses that our verification system includes value-parameterized types. Value-parameterized types are generally useful for modularity, and are similar to typeparameterized types in Java Generics [START_REF] Naftalin | Java Generics[END_REF]. In the lock-coupling example, we use that value-parameterized types can express type-based ownership [START_REF] Clarke | Ownership types for flexible alias protection[END_REF][START_REF] Boyapati | Ownership types for safe programming: Preventing data races and deadlocks[END_REF], which is a common technique to relieve the aliasing problem in OO verification systems based on classical logic [START_REF] Müller | Modular Specification and Verification of Object-Oriented Programs[END_REF].

Another challenge for reasoning about Java-like languages is the handling of inheritance. In Java, each object has an associated reentrant lock, its object lock. Naturally, the resource invariant that is associated with an object lock is specified in the object's class. For subclassing, we need to provide a mechanism for extending resource invariants in subclasses in order to account for extended object state. To this end, we represent resource invariants as abstract predicates [START_REF] Parkinson | Separation logic and abstraction[END_REF]. We support modular verification of predicate extensions, by axiomatizing the so-called "stack of class frames" [START_REF] Deline | Typestates for objects[END_REF][START_REF] Barnett | Verification of object-oriented programs with invariants[END_REF] in separation logic, as described in our previous work [START_REF] Haack | Separation logic contracts for a Java-like language with fork/join[END_REF].

This paper is structured as follows. First, Section 2 describes the Java-like language that we use for our theoretical development. Next, Section 3 provides some background on separation logic and sketches the axiomatization of the stack of class frames. Section 4 presents Hoare rules for reentrant locking. The rules are illustrated by several examples in Section 5. Last, Section 6 sketches the soundness proof for the verification system, and Section 7 discusses related work and concludes.

A Java-like Language with Contracts

This section presents the Java-like language that is used to write programs and specifications. The language distinguishes between read-only variables ı, read-write variables ℓ, and logical variables α. The distinction between read-only and read-write variables is not essential, but often avoids the need for syntactical side conditions in the proof rules (see Section 4 and [12]). Method parameters (including this) are read-only; read-write variables can occur everywhere else, while logical variables can only occur in specifications and types. Apart from this distinction, the identifier domains are standard:

C, D ∈ ClassId I ∈ IntId s,t ∈ TypeId = ClassId ∪ IntId o, p, q, r ∈ ObjId f ∈ FieldId m ∈ MethId P ∈ PredId ı ∈ RdVar ℓ ∈ RdWrVar α ∈ LogVar x, y, z ∈ Var = RdVar ∪ RdWrVar ∪ LogVar
Values are integers, booleans, object identifiers and null. For convenience, readonly variables can be used as values directly. Read-only and read-write variables can only contain these basic values, while logical variables range over specification values that include both values and fractional permissions [START_REF] Boyland | Checking interference with fractional permissions[END_REF]. Fractional permissions are fractions 1 2 n in the interval (0, 1]. They are represented symbolically: 1 represents itself, and if symbolic fraction π represents concrete fraction fr then split(π) represents 1 2 • fr. The full fraction 1 grants read-write access right to an associated heap location, while split fractions grant read-only access rights. The verification system ensures that the sum of all fractional permissions for the same heap location is always at most 1. As a result, the system prevents read-write and write-write conflicts, while permitting concurrent reads. Formally, the syntactic domain of values is defined as follows:

n ∈ Int v, w ∈ Val ::= null | n | b | o | ı b ∈ Bool = {true, false} π ∈ SpecVal ::= α | v | 1 | split(π)
Now we define the types used in our language. Since interfaces and classes (defined next) can be parameterized with specification values, object types are of the form t< π>. Further, we define special types perm (for fractional permissions) and lockset (for sets of objects).

T,U,V,W ∈ Type

::= void | int | bool | t< π> | perm | lockset
Next, class declarations are defined. Classes declare fields, abstract predicates (as introduced by Parkinson and Bierman [START_REF] Parkinson | Separation logic and abstraction[END_REF]), and methods. Following [START_REF] Parkinson | Separation logic and abstraction[END_REF], predicates are always implicitly parameterized by the receiver parameter this, and can explicitly list additional parameters. Methods have pre/postcondition specifications, parameterized by logical variables. The meaning of a specification is defined via a universal quantification over these parameters. In examples, we usually leave the parameterization implicit, but it is treated explicitly in the formal language.

F ∈ Formula specification formulas (see Sec. 3 and 4) spec ::= req F; ens F; pre/postconditions fd ::= T f ; field declarations pd ::= pred P< T ᾱ> = F; predicate definitions md ::

= < T ᾱ> spec U m( V ī){c} methods (scope of ᾱ, ī is T , spec,U, V , c) cl ∈ Class ::= classes class C< T ᾱ> ext U impl V {fd* pd* md*} (scope of ᾱ is T ,U, V , fd*, pd*, md*)
In a similar way, interfaces are defined formally as follows:

int ∈ Interface ::= interface I< T ᾱ> ext Ū {pt* mt*}
where pt* are predicate types and mt* are method types including specifications (see [START_REF] Haack | Reasoning about Java's reentrant locks[END_REF] for a formal definition). Class and interface declarations allow to define class tables: ct ⊆ Interface ∪ Class. We assume that class tables contain the classes Object and Thread. The Thread class declares a run() and a start() method. The run() method is meant to be overridden, whereas the start() method is implemented natively and must not be overridden. For thread objects o, calling o.start() forks a new thread (whose thread id is o) that will execute o.run(). The start()-method has no specification. Instead, our verification system uses run()'s precondition as start()'s precondition, and true as its postcondition.

We impose the following syntactic restrictions on interface and class declarations: (1) the types perm and lockset may only occur inside angle brackets or formulas;

(2) cyclic predicate definitions in ct must be positive. The first restriction ensures that permissions and locksets do not spill into the executable part of the language, while the second ensures that predicate definitions (which can be recursive) are well-founded.

Subtyping, denoted <:, is defined as usual. Commands are sequences of head commands hc and local variable declarations, terminated by a return value:

c ∈ Cmd ::= v | T ℓ; c | final T ı = ℓ; c | hc; c hc ∈ HeadCmd ::= ℓ = v | ℓ = op( v) | ℓ = v. f | v. f = v | ℓ = new C< π> | ℓ = v.m( v) | if (v){c}else{c} | v.lock() | v.unlock() | sc sc ∈ SpecCmd ::= assert(F) | π.commit
To simplify the proof rules, we assume that programs have been "normalized" prior to verification, so that every intermediate result is assigned to a local variable, and the right hand sides of assignments contain no read-write variables. Specification commands sc are used by the proof system, but are ignored at runtime. The specification command assert(F) makes the proof system check that F holds at this program point, while π.commit makes it check that π's resource invariant is initialized (see Section 4).

A Variant of Intuitionistic Separation Logic

We now sketch the version of intuitionistic separation logic that we use [START_REF] Haack | Separation logic contracts for a Java-like language with fork/join[END_REF]. Intuitionistic separation logic [START_REF] Ishtiaq | BI as an assertion language for mutable data structures[END_REF][START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF][START_REF] Parkinson | Separation logic and abstraction[END_REF]is suitable for reasoning about properties that are invariant under heap extensions, and is appropriate for garbage-collected languages.

Specification formulas are defined by the following grammar:

lop ∈ {*, -*, &, |} qt ∈ {ex, fa} κ ∈ Pred ::= P | P@C F ∈ Formula ::= e | PointsTo(e. f , π, e) | π.κ< π> | F lop F | (qt T α)(F)
We now briefly explain these formulas:

Expressions e are built from values and variables using arithmetic and logical operators, and the operators e instanceof T and C classof e. (The latter holds if C is e's dynamic class.) Expressions of type bool are included in the domain of formulas.

The points-to predicate

PointsTo(e. f , π, v) is ASCII for e. f π → v [4]
. Superscript π must be of type perm (i.e., a fraction). Points-to has a dual meaning: firstly, it asserts that field e. f contains value v, and, secondly, it represents access right π to e. f . As explained above, π = 1 grants write access, and any π grants read access.

The resource conjunction F * G expresses that resources F and G are independently available: using either of these resources leaves the other one intact. Resource conjunction is not idempotent: F does not imply F * F. Because Java is a garbage-collected language, we allow dropping assertions: F * G implies F.

The resource implication F -* G (a.k.a. separating implication or magic wand) means "consume F yielding G". Resource F -* G permits to trade resource F to receive resource G in return. Resource conjunction and implication are related by the modus ponens: F * (F -* G) implies G.

We remark that the logical consequence judgment of our Hoare logic is based on the natural deduction calculus of (affine) linear logic [START_REF] Wadler | A taste of linear logic[END_REF], which coincides with BI's natural deduction calculus [START_REF] O'hearn | The logic of bunched implications[END_REF] on our restricted set of logical operators. To avoid a proof theory with bunched contexts, we omit the ⇒-implication between heap formulas (and did not need it in our examples). However, this design decision is not essential.

The predicate application π.κ< π> applies abstract predicate κ to its receiver parameter π and the additional parameters π. As explained above, predicate definitions in classes map abstract predicates to concrete definitions. Predicate definitions can be extended in subclasses to account for extended object state. Semantically, P's predicate extension in class C gets *-conjoined with P's predicate extensions in C's superclasses. The qualified predicate π.P@C< π> represents the *-conjunction of P's predicate extensions in C's superclasses, up to and including C. The unqualified predicate π.P< π> is equivalent to π.P@C< π>, where C is π's dynamic class.

The following derived forms are convenient:

PointsTo(e. f , π, T ) ∆ = (ex T α)( PointsTo(e. f , π, α)) F *-* G ∆ = (F -* G) & (G -* F) F ispartof G ∆ = G -* (F * (F -* G))
Intuitively, F ispartof G says that F is a physical part of G: one can take G apart into F and its complement F -* G, and can put the two parts together to obtain G back.

The logical consequence of our Hoare logic is based on the standard natural deduction rules of (affine) linear logic. Sound axioms capture additional properties of our model. We now present some selected axioms 4 :

The following axiom regulates permission accounting ( π 2 abbreviates split(π)):

Γ ⊢ PointsTo(e. f , π, e ′ ) *-* ( PointsTo(e. f , π 2 , e ′ ) * PointsTo(e. f , π 2 , e ′ ))
The next axiom allows predicate receivers to toggle between predicate names and predicate definitions. The axiom has the following side conditions: Γ ⊢ this : C< π′′ >, the extension of P< π, π′ > in class C< π′′ > is F, and C< π′′ >'s direct supertype is D< >:

Γ ⊢ this.P@C< π, π′ > *-* (F * this.P@D< π>) (Open/Close)

Note that P@C may have more parameters than P@D: following Parkinson and Bierman [START_REF] Parkinson | Separation logic and abstraction[END_REF] we allow subclasses to extend predicate arities. Missing predicate parameters are existentially quantified, as expressed by the following axiom:

Γ ⊢ π.P< π> *-* (ex T ᾱ)(π.P< π, ᾱ>) (Missing Parameters)
Finally, the following axiom says that a predicate at a receiver's dynamic type (i.e., without @-selector) is stronger than the predicate at its static type. In combination with (Open/Close), this allows to open and close predicates at the receiver's static type:

Γ ⊢ π.P@C< π> ispartof π.P< π> (Dynamic Type)
We note that our axioms for abstract predicates formalize the so-called "stack of class frames" [9,3] using separation logic. Our Hoare rules combine typing judgment with Hoare triples. In a Java-like language, such a combination is needed because method specifications are looked up based on receiver types. As common in separation logic, we use local Hoare rules combined with a frame rule [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF]. Except from the rules for reentrant locks, the Hoare rules are pretty standard and we omit them. We point out that we do not admit the structural rule of conjunction. As a result, we do not need to require that resource invariants associated with locks (as presented in Section 4) are precise or supported formulas 5 .

Proof Rules for Reentrant Locks

We now present the proof rules for reentrant locks: as usual [START_REF] O'hearn | Resources, concurrency and local reasoning[END_REF], we assign to each lock a resource invariant. In our system, resource invariants are distinguished abstract predicates named inv. They have a default definition in the Object class and are meant to be extended in subclasses: class Object { ... pred inv = true; ... }

The resource invariant o.inv can be assumed when o's lock is acquired non-reentrantly and must be established when o's lock is released with its reentrancy level dropping to 0. Regarding the interaction with subclassing, there is nothing special about inv. It is treated just like other abstract predicates.

In CSL for single-entrant locks [START_REF] O'hearn | Resources, concurrency and local reasoning[END_REF], locks can be acquired without precondition. For reentrant locks, on the other hand, it seems unavoidable that the proof rule for acquiring a lock distinguishes between initial acquires and re-acquires. This is needed because it is quite obviously unsound to simply assume the resource invariant after a re-acquire. Thus, a proof system for reentrant locks must keep track of the locks that the current thread holds. To this end, we enrich our specification language:

π ∈ SpecVal ::= . . . | nil | π • π F ∈ Formula ::= . . . | Lockset(π) | π contains e
Here is the informal semantics of the new expressions and formulas:

nil: the empty multiset.

π • π ′ : the multiset union of multisets π and π ′ .

-Lockset(π): π is the multiset of locks held by the current thread. Multiplicities record the current reentrancy level. (non-copyable) π contains e: multiset π contains object e. (copyable)

We classify the new formulas (of which there will be two more) into copyable and noncopyable ones. Copyable formulas represent persistent state properties (i.e., properties that hold forever, once established), whereas non-copyable formulas represent transient state properties (i.e., properties that hold temporarily). For copyable F, we postulate the axiom (G & F) -* (G * F), whereas for non-copyable formulas we postulate no such axiom. Note that this axiom implies F -* (F * F), hence the term "copyable". As indicated above, π contains e is copyable, whereas Lockset(π) is not. Initial locksets. When verifying the body of Thread.run(), we assume Lockset(nil) as a precondition.

Initializing resource invariants. Like class invariants must be initialized before method calls, resource invariants must be initialized before the associated locks can be acquired. In O'Hearn's simple concurrent language [START_REF] O'hearn | Resources, concurrency and local reasoning[END_REF], the set of locks is static and initialization of resource invariants is achieved in a global initialization phase. This is not possible when locks are created dynamically. Conceivably, we could tie the initialization of resource invariants to the end of object constructors. However, this is problematic because Java's object constructors are free to leak references to partially constructed objects (e.g., by passing this to other methods). Thus, in practice we have to distinguish between initialized and uninitialized objects semantically. Furthermore, a semantic distinction enables late initialization of resource invariants, which can be useful for objects that remain thread-local for some time before getting shared among threads. To support flexible initialization of resource invariants, we introduce two more formulas: F ∈ Formula ::= . . . | e.fresh | e.initialized Restriction: e.initialized must not occur in negative positions.

e.fresh: e's resource invariant is not yet initialized. (non-copyable) e.initialized: e's resource invariant has been initialized. (copyable)

The fresh-predicate is introduced as a postcondition of new:

C< T ᾱ> ∈ ct Γ ⊢ π : T [ π/α] C< π> <: Γ (ℓ) (New) Γ ⊢ {true}ℓ = new C< π>{ℓ.init * C classof ℓ * Γ (u)<:Object ℓ != u * ℓ.fresh}
In addition, the postcondition grants access to all fields of the newly created object ℓ (by the special abstract predicate ℓ.init), and records that ℓ's dynamic class is known to be C. Furthermore, the postcondition records that the newly created object is distinct from all other objects that are in scope. This postcondition is usually omitted in separation logic, because separation logic gets around explicit reasoning about the absence of aliasing. Unfortunately, we cannot entirely avoid this kind of reasoning when establishing the precondition for the rule (Lock) below, which requires that the lock is not already held by the current thread.

The specification command π.commit triggers π's transition from the fresh to the initialized state, provided π's resource invariant is established:

Γ ⊢ π : Object Γ ⊢ π ′ : lockset (Commit) Γ ⊢ {Lockset(π ′ ) * π.inv * π.fresh} π.commit {Lockset(π ′ ) * !(π ′ contains π) * π.initialized}
Locking and unlocking. There are two rules each for locking and unlocking, depending on whether or not the lock/unlock is associated with an initial entry or a reentry:

Γ ⊢ v : Object Γ ⊢ π : lockset (Lock) Γ ⊢ {Lockset(π) * !(π contains v) * v.initialized} v.lock() {Lockset(v • π) * v.inv} Γ ⊢ v : Object Γ ⊢ π : lockset (Re-Lock) Γ ⊢ {Lockset(v • π)}v.lock(){Lockset(v • v • π)}
The rule (Lock) applies when lock v is acquired non-reentrantly, as expressed by the precondition Lockset(π) * !(π contains v). The precondition v.initialized makes sure that (1) threads only acquire locks whose resource invariant is initialized, and (2) no null-error can happen (because initialized values are non-null). The postcondition adds v to the current thread's lockset, and assumes v's resource invariant. The rule (Re-Lock) applies when a lock is acquired reentrantly.

Γ ⊢ v : Object Γ ⊢ π : lockset (Re-Unlock) Γ ⊢ {Lockset(v • v • π)}v.unlock(){Lockset(v • π)} Γ ⊢ v : Object Γ ⊢ π : lockset (Unlock) Γ ⊢ {Lockset(v • π) * v.inv}v.unlock(){Lockset(π)}
The rule (Re-Unlock) applies when v's current reentrancy level is at least 2, and (Unlock) applies when v's resource invariant gets established in the precondition. Some non-solutions. One might wish to avoid the disequalities in (New)'s postcondition. Several approaches for this come to mind. First, one could drop the disequalities in (New)'s postcondition, and rely on (Commit)'s postcondition !(π ′ contains π) to establish (Lock)'s precondition. While this would be sound, in general it is too weak, as we are not be able to lock π if we first lock some other object x (because from !(π ′ contains π) we cannot derive !(x•π ′ contains π) unless we know π != x). Second, the Lockset predicate could be abandoned altogether, using a predicate π.Held(n) instead, that says that the current thread holds lock π with reentrancy level n. In particular, π.Held(0) means that the current thread does not hold π's lock at all. We could reformulate the rules for locking and unlocking using the Held-predicate, and introduce ℓ.Held(0) as the postcondition of (New), replacing the disequalities. However, this approach does not work, because it grants only the object creator permission to lock the created object! While it is conceivable that a clever program logic could somehow introduce π.Held(0)-predicates in other ways (besides introducing it in the postcondition of (New)), we have not been able to come up with a workable solution along these lines.

Examples

In this section, we illustrate our proof rules by several examples. We use the following convenient abbreviations:

π.locked(π ′ ) ∆ = Lockset(π • π ′ ) π.unlocked(π ′ ) ∆ = Lockset(π ′ ) * !(π ′ contains π)
The formula π.locked(π ′ ) says that the current thread's lockset π • π ′ contains lock π, and π.unlocked(π ′ ) that the current thread's lockset π ′ does not contain lock π.

Example 1: A Method with Callee-side Locking. We begin with a very simple example of a race free implementation of a bank account. The account lock guards access to the account balance, as expressed by inv's definition below. The precondition of deposit() requires that prior to calling acc.deposit() the account's resource invariant must be initialized and the current thread must not hold the account lock already. The postcondition ensures that the current thread's lockset after the call equals its lockset before the call. We have annotated deposit()'s body with a proof outline and invite the reader to match the outline to our proof rules. Note that when opening inv, we use the axioms (Dynamic Type) and (Open/Close). When closing inv, we use (Open/Close) and the modus ponens.

Example 2: A Method with Caller-side Locking. In the previous example, deposit()'s contract does not say that this method updates the account balance. In fact, because our program logic ties the balance field to the account's resource invariant, it prohibits the contract to refer to this field unless the account lock is held before and after calling deposit(). Note that this is not a shortcoming of our program logic but, on the contrary, is exactly what is needed to ensure sound method contracts: pre/postconditions that refer to the balance field when the account object is unlocked are subject to thread interference and thus lead to unsoundness. However, we can also express a contract for a deposit()-method that enforces that callers have acquired the lock prior to calling deposit(), and furthermore expresses that deposit() updates the balance field. To this end, we make use of the feature that the arity of abstract predicates can be extended in subclasses. Thus, we can extend the arity of the inv-predicate (which has arity 0 in the Object class) to have an additional integer parameter in the Account class: Here, deposit()'s contract is implicitly quantified by the variable balance. When a caller establishes the precondition, the balance variable gets bound to a concrete integer, namely the current content of the balance field. Note that acc.deposit() can only be called when acc is locked (as locking acc is the only way to establish the precondition acc.inv< >). Furthermore, deposit()'s contract forces deposit()'s implementation to hold the receiver lock on method exit. This example makes use of contract conjunction. Intuitively, a method with two contracts joined by "also" satisfies both these contracts. Technically, contract conjunction is a derived form [START_REF] Parkinson | Local Reasoning for Java[END_REF]:

req F 1 ; ens G 1 ; also req F 2 ; ens G 2 ; ∆ = req (F 1 & α == 1) | (F 2 & α == 2); ens (G 1 & α == 1) | (G 2 & α == 2);
In the example, the first clause of the contract conjunction applies when the caller does not yet hold the object lock, and the second clause applies when he already holds it.

The precondition locked(s) in the second clause is needed as a pre-condition for reacquiring the lock, see the rule (Re-Lock). In Example 2, this precondition was not needed because there deposit()'s implementation does not acquire the account lock. Example 4: A Fine-grained Locking Policy. To illustrate that our solution also supports fine-grained locking policies, we show how we can implement lock coupling. Suppose we want to implement a sorted linked list with repetitions. For simplicity, assume that the list has only two methods: insert() and size(). The former inserts an integer into the list, and the latter returns the current size of the list. To support a constant-time size()-method, each node stores the size of its tail in a count-field.

In order to allow multiple threads inserting simultaneously, we want to avoid using a single lock for the whole list. We have to be careful, though: a naive locking policy that simply locks one node at a time would be unsafe, because several threads trying to simultaneously insert the same integer can cause a semantic data race, so that some integers get lost and the count-fields get out of sync with the list size. The lock coupling technique avoids this by simultaneously holding locks of two neighboring nodes at critical times.

Lock coupling has been used as an example by Gotsman et al. [START_REF] Gotsman | Local reasoning for storable locks and threads[END_REF] for single-entrant locks. The additional problem with reentrant locks is that insert()'s precondition must require that none of the list nodes is in the lockset of the current thread. This is necessary to ensure that on method entry the current thread is capable of acquiring all nodes's resource invariants: req this.unlocked(s) * no list node is in s ; ens Lockset(s); void insert(int x);

The question is how to formally represent the informal condition. Our solution makes use of class parameters. We require that nodes of a lock-coupled list are statically owned by the list object, i.e., they have type Node<o>, where o is the list object. Then we can approximate the above contract as follows:

Note that in our definition of π.traversable(π ′ ), we quantify over a type parameter (namely the owner-parameter of the Owned-type). Here we are taking advantage of the fact that program logic and type system are inter-dependent. Now, we can formally define an interface for sorted integer lists: But how can clients of lock-coupling lists establish insert()'s precondition? The answer is that client code needs to track the types of locks held by the current thread. For instance, if C is not a subclass of Owned, then list.insert()'s precondition is implied by the following assertion, which is satisfied when the current thread has locked only objects of types C and Owned<ℓ>.

interface SortedIntList { pred inv<int c>; // c
list.unlocked(s) * ℓ!=list * (fa Object z)(!(s contains z) | z instanceof C | z instanceof Owned<ℓ>)
6 Semantics and Soundness

Runtime Structures

We model dynamics by a small-step operational semantics that operates on states, consisting of a heap, a lock table and a thread pool. As usual, heaps map each object identifier to its dynamic type and to a mapping from fields to closed values:

h ∈ Heap = ObjId ⇀ Type × (FieldId ⇀ ClVal) ClVal = Val \ RdVar
Stacks map read/write variables to closed values. Their domains do not include readonly variables, because our operational semantics instantiates those by substitution:

s ∈ Stack = RdWrVar ⇀ ClVal
A thread is a pair of a stack and a command. A thread pool maps object identifiers (representing Thread objects) to threads. For better readability, we use syntax-like notation and write "s in c" for threads t = (s, c), and "o 1 is

t 1 | • • • | o n is t n " for thread pools ts = {o 1 → t 1 , . . . , o n → t n }: t ∈ Thread = Stack × Cmd ::= s in c ts ∈ ThreadPool = ObjId ⇀ Thread ::= o 1 is t 1 | • • • | o n is t n
Lock tables map objects o to either the symbol free, or to the thread object that currently holds o's lock and a number that counts how often it currently holds this lock:

l ∈ LockTable = ObjId ⇀ {free} ⊎ (ObjId × N)
Finally, a state consists of a heap, a lock table, and a thread pool:

st ∈ State = Heap × LockTable × ThreadPool
We omit the (pretty standard) rules for our small-step relation st → ct st ′ . The relation depends on the underlying class table (for looking up methods), hence the subscript ct.

Kripke Resource Semantics

We define a forcing relation of the form Γ ⊢ E ; R; s |= F, where Γ is a type environment, E is a predicate environment, R is a resource, and s is a stack. We assume that the stack s, the formula F, and the resource R are well-typed in Γ , i.e., the semantic relation is defined on well-typed tuples. The predicate environment E maps predicate identifiers to concrete heap predicates that satisfy the predicate definitions from the class table. Our well-foundedness restriction on predicate definitions ensures that such a predicate environment exists.

Resources R range over the set Resource with a binary relation # ⊆ Resource × Resource (the compatibility relation) and a partial binary operator * : # → Resource (the resource joining operator) that is associative and commutative. Concretely, resources are 5-tuples R = (h, P, L , F , I ): a heap h, a permission table 7 , a fresh set F ⊆ ObjId, and an initialized set I ⊆ ObjId. We require that resources satisfy the following axioms:

P ∈ ObjId × FieldId → [0, 1], an abstract lock table L ∈ ObjId ⇀ Bag(ObjId)
(1) P(o, f ) > 0 iff o ∈ dom(h) and f ∈ dom(h(o) 2 ), (2) F ∩ I = / 0, and (3)
if o ∈ L (p) then o ∈ I . Each of the five resource components carries itself a resource structure (#, *). These structures are lifted to 5-tuples componentwise. We now define # and * for the five components.

Heaps are compatible if they agree on object types and memory content:

h#h ′ iff (∀o ∈ dom(h) ∩ dom(h ′ ))( h(o) 1 = h ′ (o) 1 and (∀ f ∈ dom(h(o) 2 ) ∩ dom(h ′ (o) 2 ))( h(o) 2 ( f ) = h ′ (o) 2 ( f ) ) )
To define heap joining, we lift set union to deal with undefinedness:

f ∨ g = f ∪ g, f ∨ undef = undef ∨ f = f . Similarly for types: T ∨ undef = undef ∨ T = T ∨ T = T . (h * h ′ )(o) 1 ∆ = h(o) 1 ∨ h ′ (o) 1 (h * h ′ )(o) 2 ∆ = h(o) 2 ∨ h ′ (o) 2
Joining permission tables is pointwise addition:

P#P ′ iff (∀o)(P(o) + P ′ (o) ≤ 1) (P * P ′ )(o) ∆ = P(o) + P ′ (o)
Abstract lock tables map thread identifiers to locksets. The compatibility relation captures that distinct threads cannot hold the same lock.

L #L ′ iff dom(L ) ∩ dom(L ′ ) = / 0 (∀o ∈ dom(L ), p ∈ dom(L ′ ))(L (o) ⊓ L ′ (p) = [ ]) L * L ′ ∆ = L ∪ L ′
Fresh sets F keep track of allocated but not yet initialized objects, while initialized sets I keep track of initialized objects. We define # for fresh sets as disjointness in order to mirror that o.fresh is non-copyable, and for initialized sets as equality in order to mirror that o.initialized is copyable:

F #F ′ iff F ∩ F ′ = / 0 F * F ′ ∆ = F ∪ F ′ I #I ′ iff I = I ′ I * I ′ ∆ = I (= I ′ )
This completes the description of the semantic domains. We continue with the formal semantics of expressions and formulas. Expressions of type lockset are interpreted as multisets in the obvious way:

[[nil]] h s = [ ] and [[e • e ′ ]] h s = [[e]] h s ⊔ [[e ′ ]] h s .
Here are the semantic clauses for our new formulas for reentrant locking:

Γ ⊢ E ; (h, P, L , F , I ); s |= Lockset(π) iff L (o) = [[π]] for some o Γ ⊢ E ; (h, P, L , F , I ); s |= π contains e iff [[e]] h s ∈ [[π]] Γ ⊢ E ; (h, P, L , F , I ); s |= e.fresh iff [[e]] h s ∈ F Γ ⊢ E ; (h, P, L , F , I ); s |= e.initialized iff [[e]] h s ∈ I
These clauses are self-explanatory, except perhaps the existential quantification in the clause for Lockset(π). Intuitively, this clause says that there exists a thread identifier o in the domain of L such that π denotes the current lockset associated with o. We omit the (standard) clauses for the other logical operators, see e.g., [START_REF] Haack | Reasoning about Java's reentrant locks[END_REF].

Soundness

In this section, we extend our verification rules to runtime states. The extended rules are never used in verification, but instead define a global state invariant, st : ⋄, that is preserved by the small-step rules of our operational semantics. We need a few definitions: For R = (h, P, L , F , I ), let R hp = h, R perm = P, R lock = L , R fresh = F and R init = I . Our forcing relation |= from the last section assumes formulas without logical variables: we deal with those by substitution, ranged over by σ ∈ LogVar ⇀ SpecVal. We state (Γ ⊢ σ : Γ ′ ) whenever dom(σ ) = dom(Γ ′ ) and (Γ [σ ] ⊢ σ (α) : Γ ′ (α)[σ ]) for all α in dom(σ ). Furthermore, we define cfv(c) = {x ∈ fv(c) | x occurs in an object creation command ℓ = new C< π> }. Now, we extend the Hoare triple judgment to threads:

Γ hp = fst • R hp Γ ⊢ σ : Γ ′ dom(Γ ′ ) ∩ cfv(c) = / 0 Γ ,Γ ′ ⊢ s : ⋄ dom(R lock ) ⊆ {o} Γ [σ ] ⊢ E ; R; s |= F[σ ] Γ ,Γ ′ ; r ⊢ {F}c : void{G} (Thread) R ⊢ o is (s in c) : ⋄
The object identifier r in the Hoare triple (last premise) is the current receiver, needed to determine the scope of abstract predicates. We have omitted the receiver parameter from our Hoare rules in Section 4, because for source code verification the receiver parameter is always this.

We straightforwardly extend this judgment to thread pools:

(Empty Pool) R ⊢ / 0 : ⋄ R ⊢ t : ⋄ R ′ ⊢ ts : ⋄ (Cons Pool) R * R ′ ⊢ t | ts : ⋄
To further extend the judgment to states, we define the set ready(R) of all initialized objects whose locks are not held, and the function conc that maps abstract lock tables to concrete lock tables:

ready(R) ∆ = R init \ { o | (∃p)(o ∈ L (p)) } conc(L )(o) ∆ = (p, L (p)(o)), if o ∈ L (p) conc(L )(o) ∆ = free, otherwise
In conc's definition, we let L (p)(o) stand for the multiplicity of o in L (p). Note that conc is well-defined, by axiom (2) for resources. The rule for states ensures that there exists a resource R to satisfy the thread pool ts, and a resource R ′ to satisfy the resource invariants of the locks that are ready to be acquired:

h = (R * R ′ ) hp l = conc(R lock ) R ⊢ ts : ⋄ R#R ′ R ′ lock = / 0 fst • R ′ hp ⊆ fst • h = Γ Γ ⊢ E ; R ′ ; / 0 |= o∈ready(R) o.inv (State) h, l, ts : ⋄
The judgment (ct : ⋄) is the top-level judgment of our source code verification system, to be read as "class table ct is verified". We have shown the following theorem: Theorem 1 (Preservation). If (ct : ⋄), (st : ⋄) and st → ct st ′ , then (st ′ : ⋄).

From the preservation theorem, we can draw the following corollaries: verified programs are data race free, verified programs never dereference null, and if a verified program contains assert(F), then F holds whenever the assertion is reached.

Comparison to Related Work and Conclusion

Related work. There are a number of similarities between our work and Gotsman et al. [START_REF] Gotsman | Local reasoning for storable locks and threads[END_REF], for instance the treatment of initialization of dynamically created locks. Our initialized predicate corresponds to what Gotsman calls lock handles (with his lock handle parameters corresponding to our class parameters). Since Gotsman's language supports deallocation of locks, he scales lock handles by fractional permissions in order to keep track of sharing. This is not necessary in a garbage-collected language. In addition to single-entrant locks, Gotsman also treats thread joining. We have covered joining in a recent paper [START_REF] Haack | Separation logic contracts for a Java-like language with fork/join[END_REF] for Java threads (joining Java threads has a slightly different operational semantics than joining POSIX threads as modeled in [START_REF] Gotsman | Local reasoning for storable locks and threads[END_REF]). The essential differences between Gotsman's and our paper are (1) that we treat reentrant locks, which are a different synchronization primitive than single-entrant locks, and (2) that we treat subclassing and extension of resource invariants in subclasses. Hobor et al.'s work [START_REF] Hobor | Oracle semantics for concurrent separation logic[END_REF] is very similar to [START_REF] Gotsman | Local reasoning for storable locks and threads[END_REF].

Another related line of work is by Jacobs et al. [START_REF] Jacobs | A statically verifiable programming model for concurrent object-oriented programs[END_REF] who extend the Boogie methodology for reasoning about object invariants [START_REF] Barnett | Verification of object-oriented programs with invariants[END_REF] to a multithreaded Java-like language. While their system is based on classical logic (without operators like * and -*), it includes built-in notions of ownership and access control. Their system deliberately enforces a certain programming discipline (like CSL and our variant of it also do) rather than aiming for a complete program logic. The object life cycle imposed by their discipline is essentially identical to ours. For instance, their shared objects (objects that are shared between threads) directly correspond to our initialized objects (objects whose resource invariants are initialized). Their system prevents deadlocks, which our system does not. They achieve deadlock prevention by imposing a partial order on locks. As a consequence of their order-based deadlock prevention, their programming discipline statically prevents reentrancy, although it may not be too hard to relax this at the cost of additional complexity.

In a more traditional approach, Ábráham, De Boer et al. [START_REF] Ábrahám | Tool-supported proof system for multithreaded Java[END_REF][START_REF] De Boer | A sound and complete shared-variable concurrency model for multi-threaded Java programs[END_REF] apply assume-guarantee reasoning to a multithreaded Java-like language.

Conclusion. We have adapted concurrent separation logic to a Java-like language. Resource invariants are specified as abstract predicates in classes, and can be modularly extended in subclasses by a separation-logic axiomatization of the "stack of class frames" [START_REF] Deline | Typestates for objects[END_REF][START_REF] Barnett | Verification of object-oriented programs with invariants[END_REF]. The main difficulty was dealing with reentrant locks. These complicate the proof rules, and some reasoning about the absence of aliasing is needed. However, permission-based reasoning is still largely applicable, as illustrated by a verification of a lock-coupling list in spite of reentrancy. In this example, a rich dependent type system with value-parameterized classes proved useful. Because we needed to extend CSL's proof rules to support reasoning about the absence of aliasing (e.g., by adding an additional postcondition to the object creation rule), it does not seem possible to derive our proof rules from CSL's standard proof rules through an encoding of reentrant locks in terms of single-entrant locks. We have omitted wait/notify (conditional synchronization) in this paper, but we have treated it in our technical report [START_REF] Haack | Reasoning about Java's reentrant locks[END_REF]. Whereas reentrancy slightly complicates the operational semantics of wait/notify (because the runtime has to remember the reentrancy level of a waiting thread), the proof rules for wait/notify are unproblematic.

class

  Account extends Object { private int balance; pred inv = PointsTo(this.balance, 1, int); req this.initialized * this.unlocked(s); ens Lockset(s); int deposit(int x) { { this.initialized * this.unlocked(s) } (expanding unlocked) { this.initialized * Lockset(s) * !(s contains this) } lock(); { Lockset(this•s) * this.inv } (opening inv) { Lockset(this•s) * PointsTo(this.balance, 1, int) * (this.inv@Account -* this.inv) } balance = balance + x; { Lockset(this•s) * PointsTo(this.balance, 1, int) * (this.inv@Account -* this.inv) } (closing inv) { Lockset(this•s) * this.inv } unlock(); { Lockset(s) } } }

class

  Account extends Object { private int balance; pred inv<int balance> = PointsTo(this.balance, 1, balance); req inv<balance>; ens inv<balance + x>; void deposit(int x){ balance = balance + x; } }

  Example 3: A Method Designed for Reentry. The implementations of the deposit() method in the previous examples differ. Because Java's locks are reentrant, a single implementation of deposit() actually satisfies both contracts:

	class Account extends Object {
	private int balance;
	pred inv<int balance> = PointsTo(this.balance, 1, balance);
	req unlocked(s) * initialized; ens Lockset(s);
	also
	req locked(s) * inv<balance>; ens locked(s) * inv<balance + x>;
	void deposit(int x) { lock(); balance = balance + x; unlock(); } }

  Figure1shows a tail-recursive lock-coupling implementation of SortedIntList. It makes use of the predicate modifier spec public, which exports the predicate definition to object clients6 . The auxiliary predicate n.couple<c, c ′ >, as defined in the Node class, holds in states where n.count == c and n.next.count == c ′ .

	is the number of list nodes
	req this.inv<c>; ens this.inv<c> * result==c;
	int size();
	req this.unlocked(s) * this.traversable(s); ens Lockset(s);
	void insert(int x); }

Throughout this paper, Γ ranges over type environments assigning types to free variables and object identifiers.

See O'Hearn[START_REF] O'hearn | Resources, concurrency and local reasoning[END_REF] for definitions of precise and supported formulas, and why they are needed.

spec public can be defined in terms of class axioms, see[START_REF] Haack | Separation logic contracts for a Java-like language with fork/join[END_REF].

Where we use ⊓ to denote bag intersection, ⊔ for bag union, and [ ] for the empty bag.

⋆ Supported in part by IST-FET-2005-015905 Mobius project. † Supported in part by ANR-06-SETIN-010 ParSec project. ‡ Research done while at INRIA Sophia Antipolis -Méditerranée.

To express this formally, we define a marker interface for owned objects:

interface Owned<Object owner> { /* a marker interface */ } Next we define an auxiliary predicate π.traversable(π ′ ) (read as "if the current thread's lockset is π ′ , then the aggregate owned by object π is traversable"). Concretely, this predicate says that no object owned by π is contained in π ′ :


Andreea Gruev-Vintila

Nikos Kalampalikis

Alexandra Laignel-Lavastine

Chronique des années retrouvées (2019)

Keywords: Serge Moscovici, autobiography, social psychology, antisemitism, trauma

The manuscript was edited in French from handwritten notes in seven or eight languages found posthumously and is illustrated with superb photos from the family's personal archives. It won the "Influences" Ideas Prize 2019. Who is this young foreigner, 'person-less' (sanspersonne), who arrived in Paris at 22 years old, carrying 'a legacy of 6 million dead'? How did he transform a traumatic life-course into a legacy of innovation, creativity and change? How did his gaze, coupled with a particular sensitivity that he called his radar, change the trajectory of social psychology, renovate its questions, lead to new scientific paradigms? How does his heritage touch us today, in the European and global context marked by extreme crises and threats? The story is captivating.

A POSTHUMOUS WORK

x.2 historian Alexandra Laignel-Lavastine, with the support of the Mémorial de la Shoah (Shoah Memorial), and published by the Éditions Grasset thanks to the perseverance of his sons, Denis and Pierre Moscovici. The manuscript was edited in French from handwritten notes in seven or eight languages found posthumously and is illustrated with superb photos from the family's personal archives. It won the "Influences" Ideas Prize 2019.

Serge Moscovici writes about his arrival in Paris in as a young Jewish immigrant.

He recounts the first years of his human and intellectual journey in post-war France, a society whose analyst he would become, as a founder of modern social psychology and a precursor of political ecology. The book is written with the voice, the questions and the humour of this man whose psychosocial, Proustian gaze still questions contemporary societies.

Who is this young foreigner, 'person-less' (sans-personne), who arrived in Paris at 22 years old, carrying 'a legacy of 6 million dead'? 1 How did he transform a traumatic life-course into a legacy of innovation, creativity and change? How did his gaze, coupled with a particular sensitivity that he called his radar, change the trajectory of social psychology, renovate its questions, lead to new scientific paradigms? How does his heritage touch us today, in the European and global context marked by extreme crises and threats? The story is captivating.

This second autobiographical volume is easy and quick to read. Moscovici's regular readers discover once again their influential author and scientist, five years after his death, his very personal writing style, his experience of History. New readers discover the story of a man who observed post-war life in Paris while experiencing its significant incidents and encounters. The book includes a number of intimate insights, something that was rare even for those who knew Moscovici personally.

TRAUMA

As a survivor of the horrific pogroms and of anti-Semitism in Romania, he describes the psycho-traumatic explosion that occurred a few years later, once he became safe in Paris:

"My life was in perpetual imbalance, and in my eyes, this meant an unfair punishment which translated into all kinds of phobias and anxieties. But I had understood one thing: I should especially not sink into melancholy or else I would collapse" (p. 92).

1 All translations in English are the work of the author of the book review.

Papers on Social Representations, xx (x), x.1-x.6 (2021) [http://psr.iscte-iul.pt/index.php/PSR/index]

x.3

His survival resources came from other victims. A few months earlier 'the survivors in the DP camps had taught me that there is one thing that we must abhor more passionately than misery itself: resignation to misery'. A commandment to resist out of the duty towards those who had resisted. 'The psyche is an extraordinary entity: I had resigned to die, I resigned to live' he writes. To connect to life, seeking to restore a feminine face of love to repair the wrong, while doubting and The face and name of love was Marie Bromberg-Moscovici, the mother of his two sons, a psychoanalyst herself. 'I would have liked so much to be a man on the side of women' writes Moscovici, whose reflection on the active minorities' influence drew on his observations of feminism. 'Unfortunately, I have become a man on the side of men'.

TRANSFORMATION

Moscovici scrutinizes the mystery of post-war France's sophisticated social scene through the particular gaze of a young broken refugee. He writes about the meaning of being Jewish: 'My way of being Jewish? I would say a gift for stubbornness and a penchant for disobedience. And x.4

This 'trio of aliens' was a luminous, indestructible link in those years of cold, hunger, loneliness and labour. Laughing through tears, Moscovici notes with his unique bitterer gelekhter (bitter laughter), a leitmotif of the book: "I could now count on Paul and Chiva. But they themselves struggled with their own difficulties: Paul's hotel room had just been repainted in yellow with a flower wallpaper that was driving him nuts, and Chiva had relapsed from his primary infection. As for me, it must be admitted that nothing is more monotonous, poorer, nor more repetitive than a depressed person's complaint" (p. 183).

These 'three Romanian Jewish refugees with no return, no family and no money', 'educated by the terror of history', who 'had just understood that they were the last Jews in Europe', formed a community of destiny and sorrow, an active minority in Moscovici's scientific terms. They began to work (sewing machine, shoe manufacturer counter...), and decided to get out of it together at all costs. In the summer of 1948, they enrolled at the Sorbonne.

For the young Moscovici there were 'on one side the hard sciences, on the other, philosophy. All the rest, humanities and social sciences, were a terra incognita'. At a time when it had lost its early twentieth century appeal, psychology appeared as a new territory to him, and the recent Bachelor created at the Sorbonne in 1947 became a solution for his resident papers in France. 'Everything would be invented' he wrote. Moscovici fondly remembers his first paper published in 1953 in the Bulletin de Psychologie, 'a forum open to young researchers', alongside Claude Lévi-Strauss and Daniel Lagache, the only professor who taught social psychology, and later his supervisor.

He writes that he chose to study psychology because of the discrepancy between "society as Marx saw it with his telescope and that which Proust described through his microscope" (p. 116). He recalls the role played in his choice by what he calls: 'the events through which I had just gone in Romania', which commanded him to 'to unravel the mystery of such collective hysteria, which also had me taught that an individual or a group could resist the deadliest ideologies, hence the interest, in my eyes, of working on social representations'.

If trauma is a loss of meaning, then the book is perhaps a contribution to one of the most important functions of psychology, restoring meaning [START_REF] Johnstone | The power threat meaning framework: an alternative nondiagnostic conceptual system[END_REF] x.5 Zionism and Communism, the attraction for the few and the fascination for the many. The communist experience served as a sting for The Age of Crowds (1981); for the Psychology of active minorities (1979), it was the Zionist movement. In fact, my past never ceased to secretly labour in my work" (p. 59).

TRANSMISSION

Serge Moscovici has repeatedly stressed social psychology's strategic position to answer the political and social questions of contemporary societies. The book reveals his mature retrospective gaze on the young man who had crossed the great History in the mid-twentieth century with his singular and own traumatic history, both of which nourished his thinking, transformed psychosocial paradigms, and opened transdisciplinary borders.

His sons, in their beautiful afterword, mention their wish to find their father's handwritten notes in the years that followed those recalled in the book, in which he became worldwide known through his research, personality, ideas, and teaching. May their wish come true to cultivate Serge Moscovici's unique and precious, charismatic and founding legacy, which continues to inspire generations of humanities and social sciences researchers around the world. Flaubert, to whom Moscovici was attached, wrote: 'The man is nothing, the work everything'.

  Mon après-guerre à Paris. Chronique des années retrouvées (My post-war in Paris. Chronicle of the years found) is Serge Moscovici's second autobiographical volume. It follows the first volume, Chronique des années égarées: récit autobiographique (Chronicle of lost years: autobiographical story) published in 1997. It was edited and annotated by philosopher and Papers on Social Representations, xx (x), x.1-x.6 (2021) [http://psr.iscte-iul.pt/index.php/PSR/index]

I

  never lived without a religious presence, or rather without the impetus of the believer, no matter if I became an atheist'. It combined with his status as a foreigner and stateless person, which he kept until 1958. 'There is yet another difference between an ordinary foreigner and a Jewish foreigner. The former faces xenophobia, contempt, humiliation, but rarely hatred. The Jews, however, face hatred and jealousy as passions. (…) What irresistible envy can Jews stir in the souls of others?' His anchor became the small group of outsiders formed with Isac Chiva and Paul Celan, a trio cemented by 'a rage to live and a need to take revenge on death'. Isac Chiva, born in 1925 in Romania, who later became Claude Lévi-Strauss' right-hand, remained one of Moscovici's most loyal, lifetime friends. Paul Celan, the 'heartwounded poet', born in 1920 in Romania, a witness and survivor of Nazism, killed himself in Paris in 1970. He is considered one of the greatest German language poets in post-war Europe. According to Moscovici, their subversive marginality came from their propensity 'to change the questions and make connections that could seem academically unusual in the eyes of the French'. How those questions changed the social psychology paradigm and especially at what cost and with what tumult, is what we learn in the book. Papers on Social Representations, xx (x), x.1-x.6 (2021) [http://psr.iscte-iul.pt/index.php/PSR/index]

  . It sheds a light on the deeper significance of Moscovici's contributions to social psychology: "In retrospect, I think that I imported into my later reflection those two collective experiences, Papers on Social Representations, xx (x), x.1-x.6 (2021) [http://psr.iscte-iul.pt/index.php/PSR/index]

x.6 ANDREEA GRUEV-VINTILA is Associate Professor of Social Psychology at the University of Paris-Nanterre (LAPPS) (France). She conducts research on sense making under extreme circumstances and on the social psychological foundations of power, resistance and violence, using a social representational, trauma informed approach. She is the first social psychologist E-mail: nikos.kalampalikis@univ-lyon2.fr