An Introduction to separation Logic (Preliminary Draft) John C.Reynolds Computer Science Department Carnegie Mellon University ©，John C.Reynolds2008 ITU University,Copenhagen October 20-22.2008,corrected October 23
An Introduction to Separation Logic (Preliminary Draft) John C. Reynolds Computer Science Department Carnegie Mellon University c John C. Reynolds 2008 ITU University, Copenhagen October 20–22, 2008, corrected October 23
An Introduction to Separation Logic 2008 John C.Reynolds October 23.2008 Chapter 1 An Overview Separation logic is a novel system for reasoning about imperative programs. It extends Hoare logic with enriched assertions that can describe the separa- tion of stor ources concisely.The original goal of the logic ed mutable data struct res,i.e.,stru tuere upatablebe rfren from more th one po! More recently,the logic has been extended to deal with shared-variable con- currency and information hiding,and the notion of separation has proven applicable to a wider conceptual range,where access to memory is replaced by permission to exercise capabilities,or by knowledge of structure.In a research area,with a growing 1.1 An Example of the Problem The use of shared mutable data structures is widespread in areas as diverse as systems programming and artificial intelligence.Approaches to reasoning about this technique have been studied for three decades,but the result has been methods that suffer from either limited applicability or extreme complexity,and scale poorly to programs of even moderate size. For co onventional logics,the problem with sharing is that it is the default in the logic hile nonsharing is the default in programming,so that decaring all of the instances where sharing does not occur-or at least those instances necessary for correctness-can be extremely tedious. For example,consider the following program,which performs an in-place 3
Chapter 1 An Overview An Introduction to Separation Logic c 2008 John C. Reynolds October 23, 2008 Separation logic is a novel system for reasoning about imperative programs. It extends Hoare logic with enriched assertions that can describe the separation of storage and other resources concisely. The original goal of the logic was to facilitate reasoning about shared mutable data structures, i.e., structures where updatable fields can be referenced from more than one point. More recently, the logic has been extended to deal with shared-variable concurrency and information hiding, and the notion of separation has proven applicable to a wider conceptual range, where access to memory is replaced by permission to exercise capabilities, or by knowledge of structure. In a few years, the logic has become a significant research area, with a growing literature produced by a variety of researchers. 1.1 An Example of the Problem The use of shared mutable data structures is widespread in areas as diverse as systems programming and artificial intelligence. Approaches to reasoning about this technique have been studied for three decades, but the result has been methods that suffer from either limited applicability or extreme complexity, and scale poorly to programs of even moderate size. For conventional logics, the problem with sharing is that it is the default in the logic, while nonsharing is the default in programming, so that declaring all of the instances where sharing does not occur — or at least those instances necessary for correctness — can be extremely tedious. For example, consider the following program, which performs an in-place 3
4 CHAPTER 1.AN OVERVIEW reversal of a list LREVj:=nil while i nil do (k:=i+1];i+]:=j;j:=i;i:=k) (Here the notation [e]denotes the contents of the storage at address e.) The invariant of this program must state that i and j are lists representing two sequences a and B such that the reflection of the initial value ao can be obtained by concatenating the reflection of a onto B: 3a,B.list a in list B ja a!.B, where the predicate list i is defined by induction on the length of list eiei=nil list(a-a)ij.ia,jA list aj (and-can be read as“"points to”)- Unfortunately,however,this is not enough,since the program will mal- function if there is any sharing between the lists i and j.To prohibit this we must extend the invariant to assert that only nil is reachable from both and j: (3a,B.list a in list B jan=at.B) A(Vk.reachable(i,k)A reachable(j,k)=k=nil), (1.1 where reachable(i,j)n20.reachable(i,j) reachableo(i,j)i=j reachable+(i,j)a,k.ia,k A reachable(k,j). Even worse, that is not supposed ose there is some other list representing 00 aftected by th of our program.Then it must not share with either i or j,so that the invariant becomes (a,3.1 listi list=a.) ∧(k.reachable(i,k)A reachable(j,k)→k=nil) A list x (1.2) A(Vk.reachable(x,k) A (reachable(i,k)Vreachable(j,k))=k nil)
4 CHAPTER 1. AN OVERVIEW reversal of a list: LREV def = j := nil ; while i 6= nil do (k := [i + 1] ; [i + 1] := j ; j := i ; i := k). (Here the notation [e] denotes the contents of the storage at address e.) The invariant of this program must state that i and j are lists representing two sequences α and β such that the reflection of the initial value α0 can be obtained by concatenating the reflection of α onto β: ∃α, β. list α i ∧ list β j ∧ α † 0 = α † ·β, where the predicate list α i is defined by induction on the length of α: list i def = i = nil list(a·α)i def = ∃j. i ,→ a, j ∧ list α j (and ,→ can be read as “points to”). Unfortunately, however, this is not enough, since the program will malfunction if there is any sharing between the lists i and j. To prohibit this we must extend the invariant to assert that only nil is reachable from both i and j: (∃α, β. list α i ∧ list β j ∧ α † 0 = α † ·β) ∧ (∀k. reachable(i, k) ∧ reachable(j, k) ⇒ k = nil), (1.1) where reachable(i, j) def = ∃n ≥ 0. reachablen(i, j) reachable0(i, j) def = i = j reachablen+1(i, j) def = ∃a, k. i ,→ a, k ∧ reachablen(k, j). Even worse, suppose there is some other list x, representing a sequence γ, that is not supposed to be affected by the execution of our program. Then it must not share with either i or j, so that the invariant becomes (∃α, β. list α i ∧ list β j ∧ α † 0 = α † ·β) ∧ (∀k. reachable(i, k) ∧ reachable(j, k) ⇒ k = nil) ∧ list γ x ∧ (∀k. reachable(x, k) ∧ (reachable(i, k) ∨ reachable(j, k)) ⇒ k = nil). (1.2)
1.1.AN EXAMPLE OF THE PROBLEM Even in this trivial situation,where all sharing is prohibited,it is evident that this form of reasoning scales poorly. In separation logic,however,this kind of difficulty can be avoided by using a novel logical operation P*Q,called the separating conjunction,that that P and Q hold for disjoint portions of the addre ssable storag ing is built into this operation,Invariant(1.1) can be written more succinctly as (3a,B.list a i list Bj)A ad =at.B, (1.3) and Invariant (1.2)as (3a,B.list a i list Bj list x)A ao=at.B. (1.4) A more general advantage is the support that separation logic gives to local reasoning,which underlies the scalability of the logic.For example,one can use (1.3)to prove a local specification: {list a i}LREV {list at j). In separation logic,this specification implies,not only that the program expects to find a list at i representing a,but also that this list is the only addressable storage touched by the execution of LREV(often called the foot- print of LREV).If LREV is a part of a larger program that also manipulates some separate storage,say containing the list k.then one can use an infer- ence rule due to O'Hear called the frame rule,to infer directly that the additional storage is unaffected byLR {list a i list yk}LREV {list at j list k}, thereby avoiding the extra complexity of Invariant(1.4). In a realistic situation,of course,LREV might be a substantial subpro- n.and the description n of the s eparate sto might also be volumine reaso locally about】 REV,i.e.,while ignoring the separate storage,and then scale up to the combined storage by using the frame rule. There is little need for local reasoning in proving toy examples.But it provides scalability that is critical for more complex programs
1.1. AN EXAMPLE OF THE PROBLEM 5 Even in this trivial situation, where all sharing is prohibited, it is evident that this form of reasoning scales poorly. In separation logic, however, this kind of difficulty can be avoided by using a novel logical operation P ∗ Q, called the separating conjunction, that asserts that P and Q hold for disjoint portions of the addressable storage. Since the prohibition of sharing is built into this operation, Invariant (1.1) can be written more succinctly as (∃α, β. list α i ∗ list β j) ∧ α † 0 = α † ·β, (1.3) and Invariant (1.2) as (∃α, β. list α i ∗ list β j ∗ list γ x) ∧ α † 0 = α † ·β. (1.4) A more general advantage is the support that separation logic gives to local reasoning, which underlies the scalability of the logic. For example, one can use (1.3) to prove a local specification: {list α i} LREV {list α † j}. In separation logic, this specification implies, not only that the program expects to find a list at i representing α, but also that this list is the only addressable storage touched by the execution of LREV (often called the footprint of LREV ). If LREV is a part of a larger program that also manipulates some separate storage, say containing the list k, then one can use an inference rule due to O’Hearn, called the frame rule, to infer directly that the additional storage is unaffected by LREV: {list α i ∗ list γ k} LREV {list α † j ∗ list γ k}, thereby avoiding the extra complexity of Invariant (1.4). In a realistic situation, of course, LREV might be a substantial subprogram, and the description of the separate storage might also be voluminous. Nevertheless, one can still reason locally about LREV, i.e., while ignoring the separate storage, and then scale up to the combined storage by using the frame rule. There is little need for local reasoning in proving toy examples. But it provides scalability that is critical for more complex programs
6 CHAPTER 1.AN OVERVIEW 1.2 Background A partial bibliography of early work on reasoning about shared mutable data structure is given in Reference [1]. The central concept of separating conjunction is implicit in Burstall's early idea of a "distinct nonrepeating tree system"[2.In lectures in the fall of 1999,the author described the concept explicitly,and embedded it in a flawed extension of Hoare logic 3,4.Soon thereafter,a sound intuitionistic version of the logic was discovered independently by Ishtiag and O'Hearn 5]and by the author [1].Realizing that this logic was an instance of the separating implication PQ. The intuitionistic character of this logic implied a monotonicity property that an assertion true for some portion of the addressable storage would extension of that portion,such as might be created by in their paper.however.Ishtiaa and o'Hearn also presented a classical version of the logic that does not impose this monotonicity property,and can therefore be used to reason about explicit storage deallocation:they showed that this version is than the intuitionistic logic. since the latter can be translated into the classical logic O'Hearn also went on to devise the frame rule and illustrate its importance [8,9,10,5 Originally,in both the intuitionistic and classical version of the logic addresses were assumed to be disjoint from integers,and to refer to entire records rather than particular fields,so that address arithmetic was pre- cluded.Later,the author generalized the logic to permit reasoning about unrestricted address arithmetic,by regarding addresses as integers which re- fer to individual fields 8,11].It is this form of the logic that will be described and used in most of these note Since these logics are based on the idea that the structure of an assertion can describe the separation of storage into disjoint components,we have come to use the term separation logic,both for the extension of predicate calculus with the separation operators and for the resulting extension of Hoare logic At present,separation logic has been used to manually verify a variety of small programs,as well as a few that are large enough to demonstrate the potential of local reasoning for scalability [12,10,13,14,15].In addition:
6 CHAPTER 1. AN OVERVIEW 1.2 Background A partial bibliography of early work on reasoning about shared mutable data structure is given in Reference [1]. The central concept of separating conjunction is implicit in Burstall’s early idea of a “distinct nonrepeating tree system” [2]. In lectures in the fall of 1999, the author described the concept explicitly, and embedded it in a flawed extension of Hoare logic [3, 4]. Soon thereafter, a sound intuitionistic version of the logic was discovered independently by Ishtiaq and O’Hearn [5] and by the author [1]. Realizing that this logic was an instance of the logic of bunched implications [6, 7], Ishtiaq and O’Hearn also introduced a separating implication P −∗ Q. The intuitionistic character of this logic implied a monotonicity property: that an assertion true for some portion of the addressable storage would remain true for any extension of that portion, such as might be created by later storage allocation. In their paper, however, Ishtiaq and O’Hearn also presented a classical version of the logic that does not impose this monotonicity property, and can therefore be used to reason about explicit storage deallocation; they showed that this version is more expressive than the intuitionistic logic, since the latter can be translated into the classical logic. O’Hearn also went on to devise the frame rule and illustrate its importance [8, 9, 10, 5]. Originally, in both the intuitionistic and classical version of the logic, addresses were assumed to be disjoint from integers, and to refer to entire records rather than particular fields, so that address arithmetic was precluded. Later, the author generalized the logic to permit reasoning about unrestricted address arithmetic, by regarding addresses as integers which refer to individual fields [8, 11]. It is this form of the logic that will be described and used in most of these notes. Since these logics are based on the idea that the structure of an assertion can describe the separation of storage into disjoint components, we have come to use the term separation logic, both for the extension of predicate calculus with the separation operators and for the resulting extension of Hoare logic. At present, separation logic has been used to manually verify a variety of small programs, as well as a few that are large enough to demonstrate the potential of local reasoning for scalability [12, 10, 13, 14, 15]. In addition: