1.2.BACKGROUND 1.It has been shown that deciding the validity of an assertion in separa- tion logic is not recursively enumerable,even when address arithmetic and the characteristic operation emp,,*,and-*,but not are oo ited,ther the valid of as s is algorithmically decidable within the complexity class PSPACE [16]. 2.An iterated form of separating conjunction has been introduced to rea- son about arrays [17]. 3.The logic has been extended to procedures with global variables,where a"hypothetical frame rule"permits reasoning with information hiding [18,19].Recently,a further extension to higher-order procedures (in the sense of Algol-like languages)has been developed [20]. 4.The logic has been integrated with data refin nt and with object-oriented programming(i.e.,with a subset o t,24 5.The logic has been extended to shared-variable concurrency with condi tional critical regions,where one can reason about the transfer of owner- ship of storage from one process to another [25,26].Further extensions have been made to nonblocking algorithms [27]and to rely/guarantee reasoning 28 6.In the context of proof-carryi aration logic has inspired work ocedure has been dev d for restricted form of the logic 8.Fractional permissions(in the sense of Boyland (31])and counting per- missions have been introduced so that one can permit several concur- rent processes to have read-only access to an area of the heap [32].This approach has also been applied to program variables [33]. 9.Separation logic itself has been extended to a higher-order logic [341. 10.Separation logic has been implemented in Isabelle/HOL [15]
1.2. BACKGROUND 7 1. It has been shown that deciding the validity of an assertion in separation logic is not recursively enumerable, even when address arithmetic and the characteristic operation emp, 7→, ∗ , and −∗, but not ,→ are prohibited [16, 10]. On the other hand, it has also been shown that, if the characteristic operations are permitted but quantifiers are prohibited, then the validity of assertions is algorithmically decidable within the complexity class PSPACE [16]. 2. An iterated form of separating conjunction has been introduced to reason about arrays [17]. 3. The logic has been extended to procedures with global variables, where a “hypothetical frame rule” permits reasoning with information hiding [18, 19]. Recently, a further extension to higher-order procedures (in the sense of Algol-like languages) has been developed [20]. 4. The logic has been integrated with data refinement [21, 22], and with object-oriented programming (i.e., with a subset of Java) [23, 24]. 5. The logic has been extended to shared-variable concurrency with conditional critical regions, where one can reason about the transfer of ownership of storage from one process to another [25, 26]. Further extensions have been made to nonblocking algorithms [27] and to rely/guarantee reasoning [28]. 6. In the context of proof-carrying code, separation logic has inspired work on proving run-time library code for dynamic allocation [29]. 7. A decision procedure has been devised for a restricted form of the logic that is capable of shape analysis of lists [30]. 8. Fractional permissions (in the sense of Boyland [31]) and counting permissions have been introduced so that one can permit several concurrent processes to have read-only access to an area of the heap [32]. This approach has also been applied to program variables [33]. 9. Separation logic itself has been extended to a higher-order logic [34]. 10. Separation logic has been implemented in Isabelle/HOL [15]
8 CHAPTER 1.AN OVERVIEW It should also be mentioned that separation logic is related to other recent logics that embody a notion of separation,such as spatial logics or ambient 1ogic35,36,37,38,39,40. 1.3 The Programming Language The programming language we will use is a low-level imperative language- specifically,the simple imperative language originally axiomatized by Hoare (3,4],extended with new commands for the manipulation of mutable shared data structures: (comm):=… |(var）:=cons(exp〉，.，(exp) allocation I(war〉：=[(expl lookup I[(exp】:=(exp mutation dispose(exp) deallocation Memory managenent is explicit;there is no garbage collection.As we will dereferencing of dangling addresses will cs mantically we extend computational states tocontain two components a store (son mes called stack mapping variables into values(as in the semantics of the unextended simple imperative language),and a heap,map- ping addresses into values(and representing the mutable structures). In the early versions of separation logic,integers,atoms,and addresses were regarded as distinct kinds of value,and heaps were mappings from finite sets of addresses to nonempty tuples of values: Values Integers U Atoms U Addresses where Integers,Atoms,and Addresses are disjoint nil e Atoms Storesy=V→Values Henp --Valae) Statesv =Storesv x Heaps where V is a finite set of variables
8 CHAPTER 1. AN OVERVIEW It should also be mentioned that separation logic is related to other recent logics that embody a notion of separation, such as spatial logics or ambient logic [35, 36, 37, 38, 39, 40]. 1.3 The Programming Language The programming language we will use is a low-level imperative language — specifically, the simple imperative language originally axiomatized by Hoare [3, 4], extended with new commands for the manipulation of mutable shared data structures: hcommi ::= · · · | hvari := cons(hexpi, . . . ,hexpi) allocation | hvari := [hexpi] lookup | [hexpi] := hexpi mutation | dispose hexpi deallocation Memory managenent is explicit; there is no garbage collection. As we will see, any dereferencing of dangling addresses will cause a fault. Semantically, we extend computational states to contain two components: a store (sometimes called a stack), mapping variables into values (as in the semantics of the unextended simple imperative language), and a heap, mapping addresses into values (and representing the mutable structures). In the early versions of separation logic, integers, atoms, and addresses were regarded as distinct kinds of value, and heaps were mappings from finite sets of addresses to nonempty tuples of values: Values = Integers ∪ Atoms ∪ Addresses where Integers, Atoms, and Addresses are disjoint nil ∈ Atoms StoresV = V → Values Heaps = S A fin ⊆Addresses (A → Values+ ) StatesV = StoresV × Heaps where V is a finite set of variables
1.3.THE PROGRAMMING LANGUAGE (Actually,in most work using this kind of state,authors have imposed re- stricted formats on the records in the heap,to reflect the specific usage of the program they are specifying.) To permit unrestricted address arithmetic,however,in the version of the logic used in most of this paper wewill assume that all vales are integers. an infinite number of which are addr we also assume that atoms ar integers that are not addresses,and that heaps map addresses into single values: Values=Integers Atoms U Addresses C Integers where Atoms and Addresses are disjoint nil e Atoms Storesv=V→Values Henps=U(A-Valucs) Statesy =Storesy x Heaps where V is a finite set of variables (To permit unlimited allocation of records of arbitrary size,we require that, for all n >0,the set of addresses must contain infinitely many consecutive sequences of length n.For instance,this will occur if only a finite number of positive integers are not addresses.) Our inte is to apture the low-level character of machine lan uage.One estore as describing the ontents of reg the contents of n addresbe 41 ters,and the heap by assumin g that each address is equipped with an "activity bit";then the domain of the heap is the finite set of active addresses. The semantics of ordinary and boolean expressions is the same as in the simple imperative language: l (exp)Uv)Storesv)-Vales [be(boolexp)lbep∈ Storesv)(true,false) (where FV(p)is the set of variables occurring free in the phrase p).In
1.3. THE PROGRAMMING LANGUAGE 9 (Actually, in most work using this kind of state, authors have imposed restricted formats on the records in the heap, to reflect the specific usage of the program they are specifying.) To permit unrestricted address arithmetic, however, in the version of the logic used in most of this paper we will assume that all values are integers, an infinite number of which are addresses; we also assume that atoms are integers that are not addresses, and that heaps map addresses into single values: Values = Integers Atoms ∪ Addresses ⊆ Integers where Atoms and Addresses are disjoint nil ∈ Atoms StoresV = V → Values Heaps = S A fin ⊆Addresses (A → Values) StatesV = StoresV × Heaps where V is a finite set of variables. (To permit unlimited allocation of records of arbitrary size, we require that, for all n ≥ 0, the set of addresses must contain infinitely many consecutive sequences of length n. For instance, this will occur if only a finite number of positive integers are not addresses.) Our intent is to capture the low-level character of machine language. One can think of the store as describing the contents of registers, and the heap as describing the contents of an addressable memory. This view is enhanced by assuming that each address is equipped with an “activity bit”; then the domain of the heap is the finite set of active addresses. The semantics of ordinary and boolean expressions is the same as in the simple imperative language: [[e ∈ hexpi]]exp ∈ ( S V fin ⊇FV(e) StoresV ) → Values [[b ∈ hboolexpi]]bexp ∈ ( S V fin ⊇FV(b) StoresV ) → {true,false} (where FV(p) is the set of variables occurring free in the phrase p). In
CHAPTER 1.AN OVERVIEW particular,do not depend upon the heap,so that they are always well-defined and never cause side-effects. Thus expressions do not contain notations,such as cons or [-that refer to the heap;instead these notations are part of the structure of com- mands (and thus cannot be nested).It follows that none of the new heap- manipulating commands are instances of the simple assignment command (var):=(exp e h we w ite the allo lookup, and mutation ands with the familiar operator:=).In act,these com vill n obey Hoare's inference rule for assignment.However,since they alter the store at the variable v,we will say that the commands v:=cons(.)and v:=[el,as well as v:=e (but not [u]:=e or dispose v)modify v. Our strict avoidance of side-effects in expressions will allow us to use them in assertions with the same freedom as in ordinary mathematics.This will substantially simplify the logic,at the expense occasional co mplications in programs. The semantics of the new commands is simple enough to be conveyed by example.If we begin with a state where the store maps the variables x and y into three and four,and the heap is empty,then the typical effect of each kind of heap-manipulating command is: Store:x:3,y:4 Heap:empty Allocation ×:=cons(1,2); Store:x:37,y:4 Heap:37:1,38:2 Lookup y:=[x]; Store:x:37.y:1 Heap:37:1,38:2 Mutation x+1刂=3； Store:x:37,y:1 Heap:37:1,38:3 Deallocation dispose(x+1) Store:x:37,y:1 Heap:37:1 The allocation operation cons(ei,. .en)activates and initializes n cells in the heap.It is important to notice that,aside from the requirement that the addresses of these cells be consecutive and previously inactive,the choice of addresses is indeterminate
10 CHAPTER 1. AN OVERVIEW particular, expressions do not depend upon the heap, so that they are always well-defined and never cause side-effects. Thus expressions do not contain notations, such as cons or [−], that refer to the heap; instead these notations are part of the structure of commands (and thus cannot be nested). It follows that none of the new heapmanipulating commands are instances of the simple assignment command hvari := hexpi (even though we write the allocation, lookup, and mutation commands with the familiar operator :=). In fact, these commands will not obey Hoare’s inference rule for assignment. However, since they alter the store at the variable v, we will say that the commands v := cons(· · ·) and v := [e], as well as v := e (but not [v] := e or dispose v) modify v. Our strict avoidance of side-effects in expressions will allow us to use them in assertions with the same freedom as in ordinary mathematics. This will substantially simplify the logic, at the expense of occasional complications in programs. The semantics of the new commands is simple enough to be conveyed by example. If we begin with a state where the store maps the variables x and y into three and four, and the heap is empty, then the typical effect of each kind of heap-manipulating command is: Store : x: 3, y: 4 Heap : empty Allocation x := cons(1, 2) ; ⇓ Store : x: 37, y: 4 Heap : 37: 1, 38: 2 Lookup y := [x] ; ⇓ Store : x: 37, y: 1 Heap : 37: 1, 38: 2 Mutation [x + 1] := 3 ; ⇓ Store : x: 37, y: 1 Heap : 37: 1, 38: 3 Deallocation dispose(x + 1) ⇓ Store : x: 37, y: 1 Heap : 37: 1 The allocation operation cons(e1, . . . , en) activates and initializes n cells in the heap. It is important to notice that, aside from the requirement that the addresses of these cells be consecutive and previously inactive, the choice of addresses is indeterminate
1.4.ASSERTIONS 之 The remaining operations,for mutation,lookup,and deallocation,all cause memory faults (denoted by the terminal configuration abort)if an inactive address is dereferenced or deallocated.For example: Store x:3,y:4 Heap:empty Allocation x:=cons(1,2); Store:: Lookup y=X☒： Store x:37,y:1 Heap:37:1,38:2 Mutation+]:=3; abort 1.4 Assertions As in Hoare logic,assertions describe states,but now states contain heaps as Thus,in addition to the sual operati 兰e four ner ·emp (empty heap The heap is empty. ·e-e (singleton heap) The heap contains one cell,at address e with contents e'. D1*D2 (separating conjunction) The heap can be split into two disjoint parts such that p holds for one part and pa holds for the other. (se parating implication) If the heapis extended witha disjont part in then holds for the extended heap. It is also useful to introduce abbreviations for asserting that an address e is active: edf 3r'er'where r'not free in e
1.4. ASSERTIONS 11 The remaining operations, for mutation, lookup, and deallocation, all cause memory faults (denoted by the terminal configuration abort) if an inactive address is dereferenced or deallocated. For example: Store : x: 3, y: 4 Heap : empty Allocation x := cons(1, 2) ; ⇓ Store : x: 37, y: 4 Heap : 37: 1, 38: 2 Lookup y := [x] ; ⇓ Store : x: 37, y: 1 Heap : 37: 1, 38: 2 Mutation [x + 2] := 3 ; ⇓ abort 1.4 Assertions As in Hoare logic, assertions describe states, but now states contain heaps as well as stores. Thus, in addition to the usual operations and quantifiers of predicate logic, we have four new forms of assertion that describe the heap: • emp (empty heap) The heap is empty. • e 7→ e 0 (singleton heap) The heap contains one cell, at address e with contents e 0 . • p1 ∗ p2 (separating conjunction) The heap can be split into two disjoint parts such that p1 holds for one part and p2 holds for the other. • p1 −∗ p2 (separating implication) If the heap is extended with a disjoint part in which p1 holds, then p2 holds for the extended heap. It is also useful to introduce abbreviations for asserting that an address e is active: e 7→ − def = ∃x 0 . e 7→ x 0 where x 0 not free in e