Specifying Compatible Sharing in Data Structures
Contents
1. 5 h H K1AK2A S1 L XMem k 1 A S2 L2 XMem Ke2 4 gt s hE KiAs hE kA Compatible K A K2 As H S S2 h definition 1 case SPLIT COMBINE FA 4 gt h s _ hr Ar c fous _ A h s _ hr Ar cl foeas Ah ChA Compatible K AK2 As H S1 S2 lt gt s h EK As8 h k2Ah Ch AS S1 8S2 Compatiblepa gt s hE k1 k2AS1 S2 definition 1 case SPLIT READ FA 4 gt h s gt r Ar c fFars h s _ gt 4r Ar c frrars _ Ah ChA Compatible K1 A k2 As8 S1 8S2 lt gt s h E Ki As h K2Ah Ch AS Si S2 gt S h Ky AK2AS1 S2 Thus K1A k2 K1A k2 A S1 S2 Compatiblera definition 1 There are two ways of splitting the overlaid heaps in the first case we use the SPLIT COMBINE FA to combine them back as the fact that they are in compati ble sharing means that the field annotations can only be from the pairs given in ta ble for Compatiblera in Sec and we prove the second case similarly using the SPLIT READ FA rule Soundness of the underlying entailment procedure as shown in 5 and the soundness of the rules given in Fig 4 together establish the soundness of verification with compatible sharing 14 6 Experiments We have built a prototype system using Objective Caml called HIPComp The web in terface of HIPComp allows testing the examples without downloading or installing the system The proof obligations generated2. mem S gt node M M As an example consider the memory approximation of the following predicate XMem x onode d p 11 y Sy We proceed by using the rules from Fig 2 for the data node x and predicate 11 XMem xnode d p x node QM M XMem 11 y Sy Sy node QM M XMem xr node d p 11 y Sy x USy mode QM M isData c isPred c c p S v linv 1 mem SOL XMem c p v u ar p e u XMem c p S v ap 9 L XMem K1 S1 L XMem k2 S2 L XMemienp a As XMem kitk2 a S1052 union La L2 Fig 2 XMem Translating to Memory Form CHECK MEM P Jw KANT CHECK OR MEM X Mem k Sz Lz P Jw kinni Pa Jw k2AT2 PH S S A X Mem 1 S1 L X Mem k2 S2 L2 subtype L Lx iH S S1 A Pg S S2 A subtype Lz L subtype L union Li L2 subtype union L1 L L Pi mem SOL P V 2 mem SOL Fig 3 Validating the Memory Specification As a consistency check on the memory specification we use the predicate defini tion to validate the user supplied memory specification In case the user doesn t provide a memory specification e g when using the A operator we automatically extend the predicate definition with set of addresses returned by the XMem function We use an existing underlying 6 entailment procedure denoted by H to discharge the entail ment during validation of memory specifications
3. Interprocedural Shape Analysis with Separated Heap Abstractions In SAS Springer LNCS pages 240 260 Seoul Korea August 2006 Aquinas Hobor and Jules Villard The Ramifications of Sharing in Data Structures In POPL 2013 S Ishtiaq and P W O Hearn BI as an assertion language for mutable data structures In ACM POPL pages 14 26 London January 2001 P Kelly V Maslov W Pugh and et al The Omega Library Version 1 1 0 Interface Guide November 1996 N Klarlund and A Moller MONA Version 1 4 User Manual BRICS Notes Series January 2001 Xuan Bach Le Cristian Gherghina and Aquinas Hobor Decision procedures over sophisti cated fractional permissions In APLAS pages 368 385 2012 Oukseh Lee Hongseok Yang and Rasmus Petersen Program analysis for overlaid data structures In CAV pages 592 608 2011 J Reynolds Separation Logic A Logic for Shared Mutable Data Structures In IEEE LICS pages 55 74 2002 Minh Thai Trinh Quang Loc Le Cristina David and Wei Ngan Chin Bi abduction with pure properties for specification inference In Programming Languages and Systems 11th Asian Symposium APLAS 2013 Melbourne VIC Australia December 9 11 2013 Proceed ings pages 107 123 2013 Aaron Joseph Turon and Mitchell Wand A separation logic for refining concurrent objects In POPL pages 247 258 2011
4. i e the stack s and heap h satisfy the constraint amp Function dom f returns the domain of function f Now we use gt to denote mappings not the points to assertion in separation logic The model relation for separation heap formulae is given in Defn I The model relation for pure formula s denotes that the formula m evaluates to true in s The last case in Defn I is split into two cases 1 c is a data node defined in the program P 2 c is a heap predicate defined in the program P In the first case h has to be a singleton heap In the second case the heap predicate c may be inductively defined Note that the semantics for an inductively defined heap predicate denotes the least fixpoint i e for the set of states s h satisfying the predicate The monotonic nature of our heap predicate definition guarantees the existence of the descending chain of unfoldings thus the existence of the least solution 12 Definition 1 Model for Specification Formula s h iVEbo iff s h 8 or s h 82 s h Avi n KAT iff Iri n s n Un Vn h k and sluir Un Vn 7 s h ki k2 iff Jhi h2 h Lhz and h hi h2 and s h k and s h2 Ke s h EKiAkKe iff s h k and s h ke s h kK1A k2 iff s h s and s h k2 and Compatible k1A r2 s h emp iff dom h 9 s h c X vi nQ ui n iff data c ti fi tn frt EP h s x Hr dom h x and r c fiw s v1 frown 8 Un and ui
5. but for a sequential setting indeed the notion of self stable concurrent abstract predicates is analogous to our condition for compatibility However since we are focused on sequential programs we avoid the use of environment actions and instead focus on checking compatibility between shared predicates Regional logic also uses set of addresses as footprint of formulas These regions are used with dynamic frames to enable local reasoning of programs Memory layouts 9 were used by Gast as a way to formally specify the structure of individual memory blocks A grammar of memory layouts enable distin guishing between variable array or other data structures This shows that when dealing with shared regions of memory knowing the layout of memory can be quite helpful for reasoning We use field annotations to specify access to memory in shared and overlaid data structures In the area of program analysis the work most closely related to ours is by Lee et al on overlaid data structures They show how to use two complementary static analysis over different shapes and combine them to reason about overlaid structures Their shape analysis uses the operator in the abstract state to capture the sharing of heaps in overlaid structures but they do not provide a general way to reason with shared heaps In contrast we verify that the shared heaps used by the predicates are compat ible with each other Thus we present an automated framework which can be used
6. by HIPComp are discharged using off the shelf constraint solvers Omega Calculator and Mona 14 In addition to the examples presented in this paper we can do automated verification of a number of challenging data structures with complex sharing The examples are hard to reason with separation logic due to inherent sharing and aliasing in heap For each of these examples we verify methods that insert find and remove nodes from the overlaid data structure Program Invariant LOC Time secs Sharing Comp Parameterized List al x A r1 y x s1 z 30 0 28 100 40 Compatible Pairs x pair f1 A A y gt pair A s2 12 0 09 100 25 LL and SortedLL 11 x A s11 y 175 0 61 22 22 LL and Tree 11 x A tree t 70 0 24 16 7 Doubly Circular List llnext x A lldown y 50 0 41 50 32 Process Scheduler al x A r1 y s1 z 70 0 47 33 23 Disk IO Scheduler 11 x A tree t 11 y 88 1 3 16 27 The above table summarises a suite of small examples verified by HIPComp All ex periments were done on a 3 20GHz Intel Core 17 960 processor with 16GB memory running Ubuntu Linux 10 04 The first column gives the name of the program The second column shows how we use the overlaid conjunction A to concisely specify the overlaid data structures in our experiments As shown in the table for the last two pro grams the key invariant of the overlaid data structure can also be a composite structure which intermixes and A operators It i
7. lt wi or C x U1 n inv T EP and s h x root 5 3 Soundness The soundness of rules given in figure A can be established using the semantic model and the definition of field annotations We now present the proof of soundness of these rules we start first with the rules for field annotations Rule DOWNCAST FA s h ac v u lt h s x gt r Ar c f gt ws v u lt w definition a gt h s x gt r Ar c fuslv Ak Ch weakening lt gt s h H aHc v Qu Ah ch definition 1 lt gt s h H xHc v Qu Thus x gt c v Qu u lt w tHc v Qu Rule SPLIT COMBINE FA s h H aHc v u 4 gt h s x gt r Ar c fws v u lt w definition 1 lt h s 2 Hr Ar c freas v Ah Ch Yu u lt 4 lt gt s h H nee QA Ah Ch definition 1 lt gt s h H aHc v A Ah Ch A s h H ar c v u lt gt s h H xec v Q A Arc v u definition 1 Thus x gt c v Qu lt aHc v Qu A z c v A Rule SPLIT READ FA ae c f ars v Ah Ch c v I Ah Ch v I Ah Ch v l QI Art c v I QI lt definition 1 h Eo fs fs l rH rrsc v As h arsc aryc v definition 1 Thus c gt c v I gt rHc v QI A v4c v I Using the rules for field annotations we prove the soundness of the elimination rule as follows Rule ELIM OVER CONJ
8. q A r1 q Sq AS S U root mem S gt node I QA QM A sl root S root nullAs V dd q Sq rootr node d I QA QA q s1 q Sq AS S U root mem S gt node I QA QA M The mem construct consists of a memory region along with a list of possible field annotations that the predicate unfolding would generate It allows us to syntactically check if two predicates that share memory region have compatible field annotations Looking at the memory specification of al and r1 it is easy to see that al does not affect or is compatible with r1 The id field is immutable in r1 and the only field which is mutable in al is absent in r1 Thus any updates made to the nodes in memory region sS using predicate al will not have any effect when accessing the same memory region using predicate r1 To avoid writing such verbose predicates with set of addresses and to make the specifications more concise we use the overlaid conjunction operator A Formulas using the A operator are translated automatically to those that use the operator with memory specifications For the shared process scheduler the memory region shared by the lists al is same as the one shared by r1 and s1 The A operator provides the hint to the system to force the memory on both sides to be the same Hence the key invariant of the data structure is captured more concisely as al x A rl y s1 z This formula is automatically translated by first enhancing the pre
9. separation to enable local reasoning for overlaid data struc tures by introducing a notion of compatibility Two predicates are compatible when updates to one will not affect the other despite spatial overlap In our threaded list exam ple above we can imagine splitting the structure into three pseudo disjoint compatible lists formed by the anext rnext and snext pointer chains A function that modifies some chains but not others can then frame away the part of the structure it does not use This can happen in several steps consider switching a process from sleeping to running First we frame away the anext chain Then we frame away the rnext chain leaving only a straightforward snext linked list on which we do a standard list remove We then frame rnext back in and snext away followed by a standard list add Finally we frame snext and anext back in restoring the entire structure All of the above means we need field level separation which we get by adding annotations to fields when a field is absent or inaccessible we mark it with A when it is present mutable we mark it with M Here is how this looks for our threaded list al root 8 root null AS V dp a Sa rootronode p I a M QA QA x al a Sa A S Sa U root rl root root null AS rootr node pQI QA r M QA rl r Sr AS S U root VJp r Sr sl root S root null A S V Jp s Ss rootnode p QI QA QA s M x s
10. to reason about compatible sharing in data structures An initial set of experiments with small but challenging programs confirms the usefulness of our method Similarly the recent work of Dragoi et al considers only the shape analysis of overlaid lists We extend these separation logic based techniques by going beyond shape properties and handling arbitrary data structures Our proposal is built on top of user defined predicates with shape size and bag properties that can express functional properties order sort ing height balance etc of overlaid data structures A separation logic based program analysis has been used to handle non linear data structures like trees and graphs 4 In order to handle cycles they keep track of the nodes which are already visited using multi sets We have proposed a specification mechanism to express different kinds of sharing and aliasing in data structures The specifications can capture correctness properties of various kinds of programs using compatible sharing We present an automated frame work which can be used to reason about sharing in data structures We have imple mented a prototype based on our approach An initial set of experiments with small but challenging programs have confirmed the usefulness of our method For future work we want to explore the use of memory regions and field annotations to enable automated verification of other intrinsic shared data structures that do not satisfy compatible s
11. 1 s S A S Ss U root These predicates specify the all list running list and sleeping list respectively Each list predicate is parameterized by a set of addresses S of nodes on that list Each points to predicate node annotates the ownership of its fields e g the points to in al has full ownership M of the first anext pointer field This claim is compatible with the r1 and s1 predicates since both of them are absent in that field An interesting case is the process id field pid All three of the predicates wish to share access to this field we still consider them to be compatible as long as the field is marked immutable I Our annotations are thus a kind of poor man s fractional permissions 3 in which A is analogous to the empty permission M is analogous to the full permission and I is analogous to an existentialized permission Although less precise than fractional per missions these annotations are sufficient for some interesting examples and we avoid some of the hassles of integrating fractional permissions into a verification tool 15 Since we have two compatible predicates we want to use to combine them al root Sr U S1 r1 root Sr sl root Ss Actually this is not quite right Although adding field level separation is not new B the standard way to do so introduces a subtle ambiguity The issue is that the amount of sharing of the objects is not fully specified in fact
12. Specifying Compatible Sharing in Data Structures Asankhaya Sharma Aquinas Hobor Wei Ngan Chin asankhs hobor chinwn comp nus edu sg Department of Computer Science National University of Singapore Abstract Automated verification of programs that utilize data structures with intrinsic sharing is a challenging problem We develop an extension to separation logic that can reason about aliasing in heaps using a notion of compatible shar ing Compatible sharing can model a variety of fine grained sharing and aliasing scenarios with concise specifications Given these specifications our entailment procedure enables fully automated verification of a number of challenging pro grams manipulating data structures with non trivial sharing We benchmarked our prototype with examples derived from practical algorithms found in systems code such as those using threaded trees and overlaid data structures 1 Introduction Systems software ofen uses overlaid data structures to utilize memory more efficiently and boost performance Consider maintaining the set of processes in an operating sys tem some are running while others are sleeping Sometimes we wish to access every process whereas other times we only wish to access e g the running processes To track this set efficiently we can use a threaded list whose nodes are defined as follows data node int pid node anext node rnext node snext Each node has four fields The first two are st
13. The rules for checking the memory specification are given in Fig 3 In the following discussion for brevity we represent a list of field annotations used in memory specification c u with L We define a subtype L1 L2 function on lists of field annotations The function returns true if all the field annotations of data nodes in L have a corresponding node in L and their field annotations are in the subtyping relation as defined in Fig Ip subtype L1 L2 ap V c uit in L1 4c us in L2 s t uy lt u2 The subtype function is used to check the validity of the memory specification by en suring that the field annotations defined inside the predicate are really subtype of those given by the memory specification For a predicate p v mem SL the judg ment Fmem SOL in Fig B checks the validity of the memory specification Rule CHECK MEM is used when the formula does not contain a disjunction while CHECK OR MEM is used when it does The main difference in the disjunctive case is how we handle of list of field annotations For the set of addresses S we ap proximate the heap in each disjunctive formula However the field annotations have to be computed for the entire predicate as the annotations may differ in different disjuncts 4 Verification with Compatible Sharing To verify programs with compatible sharing we make use of an existing entailment procedure for separation logic denoted by 5 The only additio
14. andard SLfp the operator does not enforce strict separation thus the left and right children can point to the same node and combine using the 1 2 permissions given to each node A more sophisticated permission system like tree shares can avoid this problem but it is not known how to extend a tree shares like model to fields We avoid this problem by using a definition of the operator that enforces strict object level separation Also we use field annotations that provide a simpler way to specify mutable immutable and absent fields If we use for object level separation and A for object level sharing then it is natural to introduce another operator A for object level sharing and field level separation The overlaid conjunction A is also practically useful to represent several data structures as shown in section 6 3 Specification with Compatible Sharing We extend the specification language of separation logic with memory enhanced pred icate definitions The specification language is as described in Fig 1 we use the su perscript to denote a list of elements Pp Ppo captures a precondition and a postcondition of a method or a loop They are abbreviated from the standard rep resentation requires and ensures amp and formalized by separation logic formula In turn the separation logic formula is a disjunction of a heap formula and a pure formula KAT We use the set constraints for representing memory regio
15. because our formulae are given a classical rather than intuitionistic semantics i e x pair f s means that the heap contains exactly a single pair object at the location pointed to by x rather than at least a single pair object at x We denote two disjoint pairs x and y with the separating conjunction which ensures that x and y cannot be aliased x gt pair f1 s1 y gt pair fo s2 In contrast to capture aliased pairs we use classical conjunction as follows x gt pair f1 81 A y gt pair fo s2 The A operator specifies must aliasing that is A ensures that the pointers x and y are the equal and that the object field values are identical i e f4 f and s so To support field level framing we use the field annotations introduced in section I to mark fields that are mutable QM immutable I and absent A Consider the following x gt pair f M s A y pair f 2 A s20M This formula asserts that the heap can be split into two disjoint parts the first of which contains a first half pair pointed to by x and the second of which contains a second half pair pointed to by y Since by default fields are mutable M and when a field is absent A we need not bind a variable to its value the formula can also be written as x gt pair f1 QA yopair A so All this seems simple enough but there is a subtle wrinkle notice that x and y may be aliased if the combined heap contains a single pair that has been
16. dicate definitions with memory specifications by using the XMem function from figure 2 Predicate definitions also can be enchanced with other pure properties following translation technique de scribed in section 7 of I8 And then forcing the memory region on both sides of A to be same As the final translated formula is exactly the same as given before the use of A provides a specification mechanism to precisely describe the user intention Provided by User al x A rl y s1 z Predicate extension with mem al x S A r1 y Sy s1 z Sz Translated form al x Sx A rl y Sy s1 z Sz AS SyUS Using the A operator makes the specification of methods utilizing overlaid structures less verbose Consider the following insert method which is called while scheduling a new process in the system The new process has to be inserted into al and depending on the status flag also in r1 or s1 The precondition of the method uses the A operator to specify the key safety property The use of overlaid sharing operator allows the user to express the precondition in a concise form Compatible sharing is used to verify this method as the inserts made to different lists can be shown to not interfere with each other void insert int id int status node x node y node z requires al x A rl y x sl z A status 1 ensures al x A r1 y x sl z requires al x A rl y s1 z A status 0 ensures al x A rl1 y x sl z node tmp n
17. ecifications and sharing operators Accord ingly we define our storage model by making use of a domain of heaps which is equipped with a partial operator for gluing together disjoint heaps ho h takes the union of partial functions when ho and h have disjoint domains of definition and is undefined when ho 1 and hi 1 are both defined for at least one location 1 Loc To define the model we assume sets Loc of locations positive integer values Val of primitive values with 0 Val denoting null Var of variables program and logi cal variables and ObjVal of object values stored in the heap with c firm favn denoting an object value of data type c where 11 Vn are current values of the corre sponding fields f fn Each field has an attached annotation from M J A J means that the corresponding field value cannot be modified while M allows its mutation and A denotes no access h Heaps a Loc fn ObjVal x M 1I A s Stacks ap Var ValULoc Note that each heap h is a finite partial mapping while each stack s is a total map ping as in the classical separation logic 17112 5 2 Semantic Model of the Specification Formula The semantics of our separation heap formula is similar to the model given for sepa ration logic 17 except that we have extensions to handle our user defined heap pred icates together with the field annotations and new sharing operators Let s h denote the model relation
18. ew node id null null null tmp next x x tmp if status 1 y rlinsert y tmp else z slinsert z tmp pred p v inv z mem S c u mspec Bpr gt Pp P V Aw KAr k i emp v gt c v u p v Kiftee E A A T n altAp a 8 8 B V1 v2 v null a lt 0 a 0 a n k kxv ai a2 max a1 a2 min ai a2 p n VES S1 82 S1C S2 WES r WES r S u n SUS S1NS2 S1 S2 v xz M I A M lt I lt A where pis a predicate v w are variables cis a data type u is a field annotation Fig 1 Specification Language 2 3 Comparison with Fractional Permissions In this section we show the difficulties that arise when using separation logic with frac tional permissions SLfp to represent overlaid data structures We avoid these issues by using field annotations and overlaid conjunction operator while specifying compatible sharing in data structures Applying fractional permissions as in SLfp to fields inside inductive predicates can unintentionally change the meaning of the predicate E g consider the following predicate definition of an immutable binary tree in SLfp tree root root null Vdd 1 r rootr node d 1 2 1 1 2 r 1 2 xtree 1 xtree r We restrict the use of fields in the predicate using the fraction 1 2 to give a read only permission However this predicate does not enforce a tree and is in fact a DAG In st
19. har ing like dags and graphs 16 References 11 12 13 14 15 16 17 18 19 Anindya Banerjee David A Naumann and Stan Rosenberg Regional logic for local rea soning about global invariants In ECOOP pages 387 411 2008 J Berdine C Calcagno and P W O Hearn Smallfoot Modular automatic assertion check ing with separation logic In FMCO Springer LNCS 4111 pages 115 137 2006 John Tang Boyland Semantics of fractional permissions with nesting ACM Trans Program Lang Syst 32 6 2010 Renato Cherini Lucas Rearte and Javier O Blanco A shape analysis for non linear data structures In SAS pages 201 217 2010 Wei Ngan Chin Cristina David Huu Hai Nguyen and Shengchao Qin Automated verifi cation of shape size and bag properties via user defined predicates in separation logic Sci Comput Program 77 9 1006 1036 2012 Cristina David and Wei Ngan Chin Immutable specifications for more concise and precise verification In OOPSLA pages 359 374 2011 Thomas Dinsdale Young Mike Dodds Philippa Gardner Matthew J Parkinson and Viktor Vafeiadis Concurrent abstract predicates In ECOOP pages 504 528 2010 Cezara Dragoi Constantin Enea and Mihaela Sighireanu Local shape analysis for overlaid data structures In SAS pages 150 171 2013 Holger Gast Reasoning about memory layouts In FM pages 628 643 2009 A Gotsman J Berdine and B Cook
20. l y Sy s1 z S2 A Sx Sy U Sz Fig 4Jalso lists the rules required during entailment with field annotations These rules are based on the definition of field annotations and the semantic model of the specification formula details are in appendix 5 2 Rule DOWNCAST FA says that we can always downcast a field annotation This means that a write M annotation can be downcast to read QI and a read annotation to absent QA The following examples use the DOWNCAST FA rule to check validity of entailments with field annotations x gt node v M p I x node v I p A Valid x gt node vQ I p I x node v I p A Valid x gt node vQI p I x node v M p A Invalid The absent annotation can always be split off or combined with any other annota tion as shown in rule SPLIT COMBINE FA Finally as given in rule SPLIT READ FA 11 the read annotation can be split into two read annotations Together these three set of rules allow exclusive write access and shared read access to fields Entailments showing the use of sPLIT COMBINE FA rule are given below x gt node v M pQI Fx node vQI p I Ax node v I p A x gt node v M pQM x node v M p A Ax node v A p M x gt node v I pQI Fx node vQI p I Ax node v I p A 5 Semantics and Soundness 5 1 Storage Model The storage model is similar to classical separation logic 17 with the difference that we support field annotations memory sp
21. ment procedure to reason about such sharing and integrate our ideas into an existing automated verification system Our prototype together with a web based GUI for easy experimentation and machine checked proofs in Coq is available at http loris 7 ddns comp nus edu sg project HIPComp 2 Motivating Examples In this section we illustrate the difference between the various conjunction operators x A and A and give the intuition behind compatible sharing We also show how to automatically check for compatible sharing in data structures using a notion of memory specifications 2 1 From Separation to Sharing As discussed earlier separation logic provides a natural way to represent disjoint heaps using the separating conjunction x However if two assertions both require some shared portion of memory then cannot easily combine them Consider the following simple example data pair int fst int snd Here pair is a data structure consisting of two fields fst and snd The following asser tior indicates that x points to such a structure with field values f and s x gt pair f s Our separation logic is both Java like and C like Our logic is Java like in the sense that heap locations pointers contain point to indivisible objects rather than individual memory cells avoiding the possibility of pointers pointing into the middle of a structure i e skewing On the other hand our logic is C like
22. n since we need to maintain the fact that f f gt On the other hand in the second example since fst is immutable on both sides of the conjunction we are able to frame away either side Therefore we deem the first example incompatible while we consider the second compatible Checking for compatibility is useful not only for the operator but also for A operator in the presence of aliasing as shown in the following examples x gt pair f1 A A y gt pair f2 s2 Incompatible xt gt pair f1 A A y gt pair A s2 Compatible 2 2 Shared Process Scheduler Recall that from section I the formula that we used to specify the threaded lists was as follows al x SyUSz A r1 y Sy s1 z S2 Even though this formula uses compatible sharing of heaps it is non trivial to prove that automatically Since the field annotations are hidden inside the predicate definition they cannot be exposed without doing an unfolding of the predicate In order to expose the information about the fields inside the predicate we introduce the notion of memory specifications We allow the user to specify the memory footprint of the predicate us ing the mem construct which is associated with the predicate definition The enhanced predicate definitions for the process scheduler are shown below al root S root nullAs V dd q Sq rootr node d T q QA A al q Sq AS S U root mem S gt node I QM QA A V dd q Sq rootr node d TI QA
23. nal operator we have is the overlaid conjunction We first describe the automatic translation used to eliminate A operator For overlaid conjunction operator A we must first identify the pairs of field annotations that are compatible The following table can be used to look 10 ELIM OVER CONJ SPLIT COMBINE FA Compatible K1A k2 ar e v u lt gt 1 L1 XMem k1 S2 L2 XMem K2 gt e v u A z c v A K1 kok AK2AS S2 SPLIT READ FA xec v I gt ar c v u u lt w tc v u a c v I A a4c v J DOWNCAST FA Fig 4 Rules with Field Annotations up compatible field annotations The A operator is similar to A except that the shared heaps must be compatible which can be checked using the Compatible function uz uz Compatibler a na pas Compatible kiAk2 af T S L1 XMem k1 S2 L2 XMem k2 QM A true eas ee V c uj in Ly 4 c ud in Le s t Compatible u1 u2 ara Eme crea ad fac te Gil imelist Comnet GI GA ne c Qus in Lo 3 c Qu in L s t Compatiblera ua u1 QA QA true As shown in Fig 4 the ELIM OVER CONJ rule first checks for compatible shar ing of heaps and then uses the X Mem function to get the set of addresses S and S2 which are added to the formula when A operator is replaced with Thus for the pro cess scheduler example from Sec 2 we get the following al x S A r1 y Sy s1 z Sz al x Sx A r
24. ns as shown in Fig I The predicate definition allows optional mem construct to be specified mem is useful in cases like the overlaid data structures where it is important to be able to specify that the memory regions of both overlaying structures are exactly the same In order to check compatible sharing between two predicates we take help of the XMem k function The XMem function whose definition is given in Figure 2 returns a sound approximation of the memory footprint of heap as a tuple of the form S c u which corresponds to the set of addresses and the list of field annotations used in memory specifications The function isData c returns true if cis a data node while isPred c returns true if c is a heap predicate We use lists L and L to represent the field annotations The function union L L2 returns the union of lists L and L We do not need to consider the pure formula 7 in XMem as it doesn t correspond to any heap In general can be disjunctive so we can have a number of possible approximations of memory for a predicate each corresponding to a particular disjunct Since memory specifications are essential to check compatibility in data structures we have machine checked the soundness proof of the XMem function in Coq We illustrate how the approximation function works on a linked list data node int val node next 11 root S root nullAs V dd q Sq rootr node d q 11 q Sg S S U root
25. raightforward a process id field pid and a pointer to the next process which may be running or sleeping anext The latter two are a bit trickier When a process is running rnext points to the next running process in the list skipping over any sleeping processes in between When a process is sleeping snext points to the next sleeping process in the list We maintain three external pointers into the structure one for the head of the entire list a the second for the head of the running sublist r and the third for the head of the sleeping sublist s Consider this picture The efficiency benefits of overlaid structures can be significant e g we avoid rep resenting nodes on multiple spatially disjoint lists and can visit each running process without needing to step through the sleeping processes The real drawback from our perspective is that programs utilizing overlaid structures are difficult to verify formally Separation logic enables compositional reasoning of heap manipulating pro grams and has been widely applied to automated verification 5 2 10 Separation logic uses the separating conjunction to connect assertions valid on disjoint portions of the heap enabling natural representations for many data structures such as lists and trees because their constituent subparts are spatially disjoint Overlaid data structures cannot be specified so naturally because the underlying structures share nodes in memory We extend the notion of
26. s essential to reason about compatible sharing when specifying and verifying such programs The third column lists the lines of code including specifications in the program The annotation burden due to specifications is about 30 of the total number of lines of code In the fifth column we show the shar ing degree it is defined as the percentage of specifications that use compatible sharing using field annotations The sharing degree varies across examples depending on the percentage of methods that use overlaid conjunction in their specifications As is clear from our benchmark programs the ability to specify sharing is impor tant to verify these data structures The last column Comp is the percentage of total entailments generated that make use of compatible sharing The compatibility percent age depends on the number of entailments that make use of the ELIM OVER CONJ rule to eliminate the overlaid conjunction The compatibility check is essential to verify sharing in these programs 15 7 Related Work and Conclusions Our sharing and aliasing logic is most closely related to Hobor and Villard II our work verifies only a subset of what they can do but we do so mechanically automatically The problem of sharing has also been explored in the context of concurrent data struc tures 7 19 The problem of sharing has also been explored in the context of concurrent data structures and objects 7 19 Our work is influenced by them
27. split in half fieldwise but need not be if the combined heap contains two distinct half pairs This ambiguity is inconvenient We introduce a new operator the overlaid conjunction A to indicate that the locations are the same although the fields are disjoint Thus when we write x gt pair f A A y gt pair A s2 we unambiguously mean that x and y are aliased and have been split fieldwise On the other hand hearafter when we use then x and y are not aliased just as was the case before we added fieldwise separation We do not use the ambiguous version of We are now ready to give an intuition for our notion of compatible sharing essen tially a conjunction A A and expresses compatible sharing when one side can be safely framed away Or in other words it is possible to reason over only one side of conjunction and ignore the other since they can be combined together later with out conflicts As the simplest example the following pairs are compatible because the separating conjunction guarantees that they exist on disjoint heaps x gt pair f1 s1 y gt pair fo s2 Consider next the following two uses of classical conjunction x gt pair f1 A A x pair f2 QA x gt pair f I QA A x4 pair f2QI QA The difference between the two formulae is that in the second example we have marked the field fst as immutable I Because fst is mutable m in the first example we are not able to frame away half of the conjunctio
28. the two are being used quite differently The first x separating al from the other two is actually more like a stan dard classical separation logic conjunction That is every node on the left hand side is also on the right hand side and vice versa the fields separate but the nodes precisely overlay one another In contrast the second separating r1 from s1 is much more like the standard classical field less separating conjunction That is the set of nodes are strictly disjoint no running process is sleeping and vice versa so even if r1 and sl had incompatible fields they would still be separate in memory This ambiguity means that the traditional field level is a bit too easy to introduce and unnecessarily painful to eliminate We resolve it by using two distinct operators A when we mean that nodes are identical and fields must be compatible and x which for us means that the nodes themselves are disjoint Thus we specify our threaded list as al x SyUS A r1 y Sy s1 z Sz We know that this predicate uses only compatible sharing because all of the fields on the lhs and rhs of the A are disjoint and the guarantees compatibility on the inner subformula It may seem that A is very specific to this example but that is wrong in Sec 6 we mention how we use it to reason about other overlaid data structures Contributions We develop a specification mechanism to capture overlaid sharing an entail
Download Pdf Manuals
Related Search