Home

Heaps and Hops

1. It is also equivalent to simply setting y to 42 y 42 21 1 2 Message passing put_cell e x main send cell e x local e f x new get_cell f e f open y receive cell f put_cell e x get_cel1 f dispose y close e f Figure 1 6 Cell passing The value of a message can also refer to an allocated location in memory in which case the ownership of it may be transferred from the sender process to the receiver process The pro gram of Figure 1 6 exchanges a memory cell between two threads put_cell and get cell by passing a message cell and then proceeds to close the channel As get_cell gets own ership of the memory cell it may modify it at will in particular it may safely dispose of it as in the example If put_cell tries and dereferences x after the send a race can occur get cellmay have already freed it which would result in a memory violation for instance a segmentation fault or a bus error Notice that the fact that ownership is transferred is not enforced by the syntax we could very well replace put ce11 by send cell e x dispose x and get_cell by y receive cell f without changing the overall effect of the pro gram or introducing a race condition In other words what is transferred operationally are mere values and the meaning we attach to them is an artifact of the informal proof of correctness of the program that we have in mind Endpoints themselves can be
2. r q send cell e x ix yel e r q If the endpoint itself is part of the message footprint then its control state has to be updated before we try and verify that ya X X r Y is part of the state Indeed the receive rule will simply add j X X r Y to the current state hence it must be up to date with regard to the endpoint s control state at the moment it was sent Updating the control state of the sending endpoint is the purpose of the interplay of and in the precondition In this case the following rule can be derived taking emp SEND2 succ r q a q FA X E Y MXb X E rqr X gt X r q y X X r Y kr send a E1 E2 emph The rule Senn of Figure 5 1 is a more general rule that accounts for both cases CHANNELDISPATCH and ExTCHOICE These two rules govern external choice and recep tion They have been made into two rules to simplify notations by treating separately each endpoint of an external choice composition This supposes that the components of a guarded program are reordered for the needs of the proof so as to group receives that target the same endpoint together 83 5 1 Proof system In the case of receive abiding by the contract is more intricate than in the case of send where the action merely has to be one of the available transitions of the contract Indeed for a particular endpoint at control state q of a contract for instance with
3. 20 Chapter 1 Concurrency and Ownership message a main local e f put val e x send a e x e f openO put_val e 42 get_val f close e f get_val f J y receive a f if y 42 print The answer is 42 else print What was the question again Figure 1 5 Value passing where pis a program x and e are variables and a a message tag we simply write x receive a e p Closing a channel Finally closing a channel takes as arguments two expressions point ing to the locations of both endpoints of a channel and disposes of them 1 2 2 Examples In the examples that follow we will use function calls which are not part of the syntax of our programming language However they can be simulated by inlining the code at the call sites provided that we are careful not to use mutually recursive functions We use e f for variables pointing to endpoints and x y for variables containing integers or pointers to regular memory cells The program of Figure 1 5 exchanges an integer value between two threads put_val and get val by passing a message tagged by a declared in the preamble of the program in Singf a would be annotated with a type for instance int and then proceeds to close the channel The variable y is global Except for the printing operations it is equivalent to the program below local e f e f open send a e 42 y receive a f close e f
4. HL07 Cristiano Calcagno and Peter W O Hearn On garbage and program logic In FoSSaCS volume 2030 of LNCS pages 137 151 2001 Cited on page 19 Cristiano Calcagno Peter W O Hearn and Hongseok Yang Local action and abstract separation logic In LICS pages 366 378 2007 Cited on pages 35 97 102 Mike Dodds Graph transformation and pointer structures PhD thesis 2009 Cited on page 68 Dino Distefano Peter W O Hearn and Hongseok Yang A local shape analysis based on separation logic In TACAS volume 3920 of LNCS pages 287 302 2006 Cited on page 5 Pierre Malo Deni lou and Nobuko Yoshida Buffered communication analysis in distributed multiparty sessions In CONCUR volume 6269 of LNCS pages 343 357 2010 Cited on page 64 Manuel F hndrich Mark Aiken Chris Hawblitzel Orion Hodson Galen C Hunt James R Larus and Steven Levi Language support for fast and reliable message based communication in Singularity OS In EuroSys pages 177 190 2006 Cited on pages 4 18 20 26 27 28 43 45 46 Robert W Floyd Assigning meanings to programs In Proceedings of the Symposium on Applied Mathematics volume 19 pages 19 32 1967 Cited on pages 3 69 Alain Finkel and Pierre McKenzie Verifying identical communicating pro cesses is undecidable Theor Comput Sci 174 1 2 217 230 1997 Cited on page 50 Alexey Gotsman Josh Berdine Byron Cook Noam Rinetzky and Mooly Sa giv Local reasoning
5. kr Y e Y r qg Q i receive ai Es pi V i 1 Z freevar ExTCHOICE kr d p d r olp Qj er pap vj Figure 5 1 Proof rules for copyless message passing 82 Chapter 5 Proving Copyless Message Passing This is an instance of the Senn rule where Ej gt X r q In this version the precondition requires the sending endpoint and the message footprint to be present in the current state and the message to be authorised by the contract in the current control state of the endpoint The footprint of the message has been instantiated with the correct parameters X for the source endpoint src X for the destination end point dst r for the role rl and Y for the value val As expected ownership of the message s footprint is lost after sending and the control state of the endpoint is up dated according to the contract Thus a proved program cannot access the pieces of state attached to a message after it has been sent only the recipient of the message will be able to further access it once it has received the message The following program is in particular not provable with I cell val gt and succ r q cell g xy ei xec ec 7 send cell e x x y eire r q y xl Swapping the two lines removes any possibility for a race and allows the proof to go through x y e lex gt Her r q y bells Qo y elkx gt y Aet
6. The result is the formula fr C transfer 0 xe 134 Chapter 7 Heap Hop The dispose x command that follows looks for a cell pointed to by x in its precondition and simply removes it which gives f gt C transfer_0 Finally sending ack puts f back in the transfer control state and then tries and find a sub formula corresponding to the footprint of ack In this case the footprint is emp so the whole process is trivial let us detail it anyway After the control state of the corresponding endpoint has been updated the send command is replaced by a jsr call that corresponds to consuming the message s footprint instantiated by the right parameters something that could not have been done before this phase as one needs to retrieve for instance the peer of the sending endpoint which can only be done by looking at the formula at that point of the symbolic execution More precisely a call send a E E E starting from formula is replaced with Ya CE E ge eee En JStg emp A where gt E pr E rl r true In the case at hand send ack is replaced with emp jsr emp As described earlier this call results in the entire formula being framed away because emp D for any and the symbolic execution reaches the end of the branch with this final current formula f gt C transfer Similarly the second branch of the conditional produces the formula f gt C end
7. n This contradicts the fact that T is admis sible by Definition 5 1 6 4 5 Boundedness of communications and deadlock freedom Lemmas 6 11 and 6 16 connect the fault and leak freedom properties of contracts to equiv alent properties on programs One could show similarly to the proof of these lemmas that a program with n bounded contracts only needs communication buffers of size n Unfortunately a program with deadlock free contracts is not necessarily deadlock free even when the program only manipulates one channel For instance using the deadlock free contract qo la one can prove the following deadlocking program e f o0pen C receive a f send a e close e f This is because the logical rules do not take account causality between different end points but only causality within the same endpoint Similarly contracts fail to account for interactions between different channels which can also cause deadlocks as in the program below whose channels abide by the same deadlock free contract as above receive a f1 receive a f2 send a e2 send a el 125 CHAPTER 7 Heap Hop This chapter describes the tool that has been developed during the course of the thesis named Heap Hop It takes programs annotated with logical formulas and contracts as input and outputs either Valid if all the functions have been successfully proved to comply with their specifications and the contracts are leak and faul
8. receive a e send a e false This is inconsistent because the program above does not diverge if a is present in e s queue at the beginning of the execution Thus we require message footprints to be precise which forbids this counter example As for concurrent separation logic we used the conjunction rule to derive unsoundness one might be able to have soundness with imprecise footprints if one gives up the conjunction rule The precision assumption comes into play in the proof of the locality of the command send see Lemma 6 5 page 114 5 3 3 Channel closure leaks As it stands the rule of close can hide a leak if messages were still present in the queues when the channel was closed Consider for instance the following contract and proof sketch for a program that sends a cell over a channel and closes it weakening steps are omitted cell e f xi e X f Y A X VC l g xY gt X 2 3 xeo send cell e x I gt x 0 close e f e f x lk emp 93 5 3 Restrictions of the proof system At the end of the execution of this program x is still allocated whereas the postcondition of the Hoare triple states that the heap is empty Hence the proof system alone cannot guarantee the absence of such leaks We will see in the next chapter that requiring the contracts to be leak free Definition 3 19 is enough to prevent them However another kind of leaks is still possible that does not d
9. 144 Ernst W Mayr An algorithm for the general petri net reachability problem In STOC pages 238 246 1981 Cited on page 54 Bibliography Maz86 Mil80 Mil99 Min67 OG76 O H04 O H07 OP99 ORYOI 05509 Rey02 Rey04 RGO8 SB09 ST77 Antoni W Mazurkiewicz Trace theory In Advances in Petri Nets volume 255 of LNCS pages 279 324 1986 Cited on page 6 Robin Milner A Calculus of Communicating Systems volume 92 of LNCS Springer 1980 Cited on page 6 Robin Milner Communicating and mobile systems the v calculus Cam bridge Univ Pr 1999 Cited on page 6 Marvin L Minsky Computation finite and infinite machines 1967 Cited on page 54 Susan S Owicki and David Gries An axiomatic proof technique for parallel programs i Acta Inf 6 319 340 1976 Cited on page 75 Peter W O Hearn Resources concurrency and local reasoning In CONCUR volume 3170 of LNCS pages 49 67 2004 Cited on page 73 Peter W O Hearn Resources concurrency and local reasoning Theor Com put Sci 375 1 3 271 307 2007 Cited on pages 17 65 73 74 Peter W O Hearn and David J Pym The logic of bunched implications Bul letin of Symbolic Logic 5 2 215 244 1999 Cited on page 3 Peter W O Hearn John C Reynolds and Hongseok Yang Local reasoning about programs that alter data structures In CSL volume 2142 of Lecture Notes in Computer Science pa
10. As far as the communication protocol is concerned we could have used any other spec ification that allows to send and receive the message cell and lead to a final configuration for instance the following contract cell Although the program obeys Ca as well as Cee the former choice is less sensible than 86 Chapter 5 Proving Copyless Message Passing message cell emp vale message fin emp val e 1 q val src contract C 4 initial state q 1 cell gt q state q fin gt q final state q put_cell e x e xik e 1 q xP1 send cell e x send fin e e e xi emp get cell f firfo 2 q 1 4 local y ee y receive cell f y ee i o 5 6 2 4 yo dispose y ee receive fin f y ee i 5 X 2 47 X5 5 1 q A X ee close ee f fi emp main emp local x e f x new x efl xe e f open C x e flrxo re Xx f YxX gt Y 1 q Y gt X 2 q put cell e x get_cell f x e f lr emp emp emp Figure 5 3 Proof of the cell and endpoint transfer the latter as provides less intuition about the communication protocol followed by the program Moreover f is not leak free As we have informally seen at the end of the previous section this means that we will not be able to prove that this program is leak free using our logic with C as cont
11. If 0 p v is provable then for any state c satisfying the formula p o P error and if p o skip o then o satisfies v 4 2 2 Small axioms One of the main features of separation logic is the soundness of the frame rule FRAME 6 p 9 px Y p o Y This rule states that whenever the execution of a program from a certain heap does not produce memory faults it will not produce memory faults from a bigger heap either a property called safety monotonicity and the extra piece of heap will remain untouched by the program throughout its execution we say that p is local In traditional models of separation logic where stacks are total functions whereas ours are partial the soundness of the frame rule requires the following side condition to be added freevar w n modifs p In the full correctness setting we would also require that p does not diverge on c The focus of this thesis is on partial fault avoiding correctness 69 4 2 Proof system Remark 4 1 Of course the classical frame rule using would be unsound AND FRAME WRONG 0 pto bnv p d Ay freevar p n freevar y This is due to potential aliasing Ifwe augmented Floyd Hoare logic with this erroneous frame rule we could derive the following false specification of the mutation of a memory cell x 32 x 52 x gt 52 x 321 y gt 32 x 52 x 5 52 y gt 32 With the frame rule o
12. Once both endpoints have sent the ChannelClosed message the channel is effectively closed This approach can easily be simulated in our setting In fact in several of the examples we have given for instance those of Figures 1 8 and 1 9 this is how the channels were closed the program implementing one side of the communication sends its endpoint over itself at the end of the communication for example send fin e e where e points to said endpoint and fin is the label chosen to indicate the end of communications The peer program can then receive this endpoint through its own endpoint and thus close the channel since it now holds both of its endpoints 1 2 4 Problems of interest In Chapters 3 and 5 we will introduce mechanisms to prove certain safety properties about programs that are specific to message passing Let us informally discuss them Boundedness For asynchronous communications a buffer is used to hold pending mes sages messages that have been sent and are waiting to be received It is often interesting to know whether a bound can be put on the maximum number of pending messages of all the executions of a program hence on the size of the buffer in which case communications are said to be bounded The communications of the list sending program Figure 1 9 are not bounded because arbitrarily many cells may be sent depending on the length of the list before the receiving process catches on We can write another version of t
13. The reasoning induced by separation logic is rooted in the following local reasoning idiom defined as such by O Hearn et al ORYO1 To understand how a program works it should be possible for reasoning and specification to be confined to the cells that the program actually accesses The value of any other cell will automatically remain unchanged Separation logic takes advantage of this idiom by maintaining assertions only about the portion of the heap that a program knows it will be the only one to access at this point in the Introduction execution what it owns in a sense in contrast to what it can access This form of reasoning supposes that in O Hearn s words processes mind their own business and typically gives rise to more concise proofs than those obtained by keeping track of aliasing constraints Moreover local reasoning proved to be an elegant tool for reasoning about concurrent programs as well provided that a clean separation between what is owned by each process can be established at any point in time This can benefit the analysis of copyless message passing programs Indeed the ownership reading of the heap allows us to translate our discussion about the transfer of the right to access the memory cells corresponding to the contents of a message into the following argument whenever a process sends a message it loses ownership of that portion of memory corresponding to the contents of the message co
14. V j 3i 3a 3q qi j a q ET wj u A configuration C is a proper deadlock if C is deadlock and not final A system is deadlock free if no reachable configuration is a proper deadlock A system is faulty if there is a possibility that at some point in time one participant is ready to receive certain messages but an unexpected one is at the head of one buffer Again the example depicted in Figure 3 2 is fault free whereas the one below can reach the faulty configuration q1 gp a the second machine is expecting a b message kan a a y a Definition 3 18 Fault free system We say that a configuration q1 qn w1 Wp of a system is an unspecified reception configuration if there are 1 j and a such that e Wj a wy e a qi j a q Ti 2 and e a a ai 7a q Ti 49 3 2 Verification of communicating systems A system is fault free if none of its reachable configurations leads to an unspecified reception Finally the final configurations of a system should be reachable only when all the com munications have been resolved and there is no message left in the queues that is final configurations should be stable This is the case for the system of Figure 3 2 if we take as final state q qf but not if we take for instance q q1 as the unstable configuration q 41 1 a would then be considered final Definition 3 19 Leak free system A system is leak free if al
15. aj rx W1 Wa ajs1i rja1 Az Tk a1 r1 az r The copying machine The copycat machine M is defined as A 2 Q U 1 2 icat Qcat endecat U 4 7 Harmerx Qu oy gt icat Teat Its structure depicted in Figure 3 3 is simple Following the notations of Bollig Bol06 we write a for a 0 and a lt q for a q Its modus operandi is to copy everything from its input buffer to its output buffer except for O0 lt q f which leads Mat into the state endeat from which no transition emanates In a run of the whole system nothing will be left to receive when this message is received and endecat will be the final state of Mat This machine will be the first to make a transition in the whole system filling the tape with the initial configuration of the Turing machine O qo 0 0 The transition machine Anticipating the needs of the proofs of the results of the next section we will build a machine that is deterministic positional and synchronising as is Meat Let us present how to encode Ms transitions Consider a transition T qi aj qi ay 4 T wherein the head is moving to the left This will be encoded by the part of the CFSM described in Figure 3 4 This fragment of CFSM can be decomposed into the left and right parts Which one is triggered depends on where the head of the Turing machine is positioned on the
16. by the operational semantics since to send on one endpoint one needs to modify its peer s buffer The other two conditions ensure that channels are well formed endpoints are paired into bi directional channels composed of two buffers 2 2 2 Notations The operational semantics is given as a set of rules that describe the reduction relation between a configuration p c where p is a program and c a state and either another configuration p o or an error written respectively po gt p o and p o gt error Because we are interested in race free programs we will force racy ones to fault Similarly we force programs in an unspecified reception configuration to fault This gives rise to two kinds of errors OwnError indicates an ownership error the program has tried to access a resource it does not currently own be it a variable a memory cell or an endpoint MsgError indicates a message error during a reception there is an unexpected message at the head of a receive queue so the receiving operation fails We write error for one of OwnError or MsgError in the rules that propagate an error through programming constructs We write for the reflexive and transitive closure of Explicit error detection is a rather unrealistic aspect of the semantics because threads would normally not fault when merely trying to access the same memory location and may or may not fault when receiving an unexpected message depending on the im
17. e is defined and equal to with init qo We need to show that there is C cconf a e such that do 40 1 1 gt e C We can apply the previous lemma If we are in the first case the result is immediate If we are in the second case then either VC cconf c 3C cconf a e C gt e C or cconf a e cconf c amp From the hypothesis that is ceremonious there is C e cconf a such that qo qo e C If cconf a e cconf a then C cconf a Otherwise since p a gt p a p a ProtoError hence cconf 6 amp Since moreover cconf a gt e cconf c e there are finally C cconf a e and C cconf a e such that qo 0 1 gt g C e C which ends the proof 6 3 Soundness 6 3 1 Locality up to interferences We prove here crucial technical lemmas about the properties of the open operational se mantics that will allow us to derive the soundness of our proof system in the next subsec tion The structure of the lemmas is similar in essence to previous work for instance by Brookes Bro07 or Vafeiadis Vaf07 There is however one important difference in the present setting interferences are needed to express the behaviour of an open program one that may receive messages from the environment or send to it because it possesses only one end of a particular channel which has non trivial consequences on the formulation of the
18. error or p2 0 error or there are disjoint states o 0 such that 0 g e of and 4 e 71 0 P1 01 and e p2 05 gt P3 0 Proof The first point is obvious from the semantics of and norace by using Lemma 6 5 1 For the second point let us proceed by induction on the length n of the computation of p pa the base case of a computation of length 0 being trivial Suppose that the proposition holds for n computation steps and that p p2 0 pi py a This execution can be decomposed as 1 pi p2 0 pY p3 o p po a By induction hypothesis for all o7 05 such that c e 05 0 either p or p3 faults respectively on 9 and 67 or there are disjoint states 7 o such that a c e o5 and pi 27 pi 0 and P3 093 gt Pa O2 We have to prove that either p or p faults respectively on and or that there exist pl py C and gg such that pj 8 7 pi 21 2 03 p2 9 and oy eg g For this purpose we perform a case analysis on the first step of the computation of p po e If this was an environment step then p pi pa p2 and Lemma 6 4 gives us oY and c5 such that 0 e 05 g If p did a step p1 0 gt pj g then by Lemma 6 5 either p1 0 error or there are aY 9 such that p1 0 pt a 09 gt 05 and 0 ea 0 By taking p3 p2 we finish the proof If p did a step the argument is symmetric 115 6 3 Soundnes
19. h k k gt MMC aia r keue Fils e E s amp k e1 2 1 ay k e2 61 2 gy qr finals k e1 k e2 u close E E2 s h k k skip s h k der 2 k N 61 821 Bls e Eo 2 amp 2 k e1 e2 1 qf k e2 1 2 91 df finals k e1 k e2 u close E1 E2 s h k k gt LeakError Fils 1 E2 s amp 2 k e1 e2 1 91 k e2 1 2 92 q q2 or q finals close E1 E2 s h k k gt ProtoError Fas 1 E s amp 2 k e1 5 r q en egorr l close E1 E2 s h k k gt OwnError Figure 6 3 Open operational semantics of channel creation and destruction Sending a message The semantics of send is shown in Figure 6 4 and is split into three cases Let us begin with the successful one the endpoint and the value are accessible the send is authorised by the contract and enough state is held to find a substate that satisfies the message s footprint Note that as discussed in the description of the Senp rule in the previous chapter the control state of the sending endpoint is updated before the message is sent so the footprint is checked against the updated state When the footprint cannot be found in this state an ownership error is issued Similarly if the send is not permitted by the current state of the contract a
20. then there exists o such that o i y and close o 0 To show that programs proved under fault free contracts enjoy the above property we will show that valid programs in the sense of the open semantics hence of Definition 6 8 are runtime valid when the contracts involved are fault free More precisely we say that p v is valid under fault free contracts if the contracts appearing in 4 and p are all fault free Lemma 6 9 fp 6 p a under fault free contracts then ler 9 p 4 If we manage to establish such a connection then the result we seek will follow immedi ately from the soundness result of the previous section The triple 9 p v is provable with fault free contracts if one of its proofs mentions only fault free contracts including the ones decorating p Theorem 6 2 If r p v with fault free contracts then ler 6 p v Proved programs are race free Let us begin by proving that a valid program is race free that is it does not reduce into OwnError in the closed semantics In particular we must prove that a race of p p on close o for the closed notion of race entails a race of the same program on c for the open notion of race 119 6 4 Properties of proved programs Lemma 6 10 For all well formed open state c if close c and p close o OwnError then p 1 gt OwnError Proof Leto s h k k and o close o sc he ke We proceed by structural induction on p
21. val src or Yin val gt dst We can specify that only the first endpoints of channels following the contract will be attached to a message a and that they will only be sent from an endpoint from the same role with the footprint Ya valo 1 Arl 1 A footprint context is written T and is of the form a1 y1 Qn Yn If all the formulas y are precise see Definition 4 1 the context is well formed As for locks and resources These formulas were called invariants in our original papers to emphasise their similarities to locks and CCRs We felt the need to change the terminology because they do not represent the state of a shared resource that has to be maintained but rather the ownership of a piece of state that is logically being trans ferred Footprint parameters play a similar role as the lock parameters of the storable locks of Gotsman et al GBC 07 80 Chapter 5 Proving Copyless Message Passing imprecise footprints can lead to unsoundness in the proof system We discuss this issue later in this chapter in Section 5 3 2 Since the set of message identifiers is fixed from the beginning contrarily to resources identifiers that can be declared within a program the context is actually fixed throughout the proof We reflect this in our notations by making it a subscript of the turnstile a triple provable under a context T is written tp 6 p 4 Finally when Q qo F T we write su
22. In 20 lt qf gt qsim There is also a final transition qsim gt endsim Consider now a transition 7 qi aj qir aj T wherein the head is moving to the right This will be encoded by the fragment of the CFSM described in Figure 3 5 The steps are similar to the left transition case except that we have to handle the case where we have to extend the tape to the right in addition to the cases where the head is at the beginning of the tape Consider for instance the loop going to the right and coming back to qsim from below This time ap is remembered only because the forwarding mechanism has to be embedded in every transition to obtain a deterministic machine Itis immediately 52 Chapter 3 Dialogue systems Figure 3 5 Encoding of a transition of M moving the head to the right sent back unchanged when the head is found followed by the updated letter aj Then we try to read the next letter In the case at hand the end of the tape has been reached and we get O The new head of the Turing machine is positioned on the final character by sending back O qi and we end the sequence by sending the terminating symbol Theorem 3 1 For every Turing machine SN there is a deadlock free positional and de terministic dialogue system that reaches its final state if and only if M halts P
23. Nom A os 24 1 2 4 Problems Of interest 26 1 2 5 Encoding locks and message passing into one another 28 1 2 6 Further examples of message passing 29 2 A Model of Copyless Message Passing 31 2 1 Programming language 31 24 ZHIE ain eT mC ee eem cR Ei i 31 2 1027 HTPMP Istud Se IER dur ant oe 33 2 2 Semantics DEA SAREE d SE eve xu ae 34 221 States ros Ro Re ERREUR AER Em M ath eS 34 2 2 2 INOtationis 5t ro ees Rode e wo hs eee Hie ed 35 22 3 Operational semantics 36 2 2 4 Properties of the operational semantics 40 Contents 3 vi Dialogue systems 3 1 Communicating systems AN O A NE 3 1 2 Dialogue systems and contracts 3 13 Semantics xi a ais bun A Lx es 3 1 4 Safety properties cia a as 3 2 Verification of communicating systems 3 2 1 Simulation of a Turing machine by a dialogue system 3 2 2 A decidable class half duplex systems 33 o s c g a orae d Up ve AP m A NE hs ba ae Pad 3 3 1 Syntactic sufficient conditions 3 3 2 Contract verification is undecidable Gonclusion 3 aa Ahaha AA A e deem d Concurrent Separation Logics AW ASSERUONS ai AA cade AE o A A Ge re B ange DAA ATT Models 25 08 seg ta e us dee Nan parles A2 A A ON 41 3 Se
24. Our verification technique will be a program logic that builds on the ideas of local reasoning Local reasoning Since copyless message passing assumes a shared memory between processes any verifica tion technique aiming at proving the correctness of programs using this paradigm will have to be able to cope with the memory also referred to as the heap Reasoning about memory manipulating programs has long stood up as a difficult topic in the area of the formal veri fication of programs which is mainly attributable to aliasing in a heap manipulating pro gram the same memory location may be accessed through multiple program variables all containing this location as value Whenever the contents of the memory at this location changes the update should be visible for all the processes that may access it through one of these variables From a verification standpoint this usually means that one has to keep track of all the ways a memory location could be aliased Aliasing makes reasoning about memory manipulating programs global in that sense which results in tedious proofs at best if one indeed dares to go and prove such programs in such a way Bur72 Bor00 Separation logic IOO1 Rey02 which is derived from the logic of Bunched Implica tions OP99 and extends Floyd Hoare logic Hoa69 Flo67 was proposed as a way to reason about such programs while avoiding the pitfalls that result from the tedious book keeping of aliasing constraints
25. The second difference is in the treatment of the local variable construct As in the case 107 6 2 Open operational semantics X1 Xn dom s Ei dom k amp En dom k E s e k e le r q k ei ai v i a succ r q lai al q x receive a E pj s h k k gt jal pi s x v h k control e lt q e 65 k es a Ej e k e e amp r q 3q succ r q a q TL xj receive aj Ej pj s h k k gt ProtoError ja Fils 1 amp mE amp En En k ei a v a Q Vj Ej gt aj a n xj receive a Ej pj s h k k gt MsgError j 1 Fils 1 amp amp En En k amp e 7 q Ja dq succ r g a q amp Vj e ej gt a 4 n xj receive a Ej pj s h k k gt ProtoError ja Figure 6 5 Open operational semantics of external choice and receive of new we now have to take into account not only the domain of the surface stack but also all the variables that are allocated in the footprints of the messages of all buffers in order to avoid creating ill formed states 6 2 2 Subject reduction Let us describe two properties of open states that are preserved by program reductions well formedness with respect to I which supersedes well formedness and being ceremo nious that is having buffers co
26. Xxf Yx Xb gt Y 1 q Y gt X 2 q put_list e x get_list f 3 xik emp Figure 5 4 Proof of the cell by cell list transfer 89 5 2 Examples atm a b a birar Cuser 2 wait br bank 2 wait 1 local k h id amt while true a b k h id amt I a Cuser 2 wait b gt Cbank 2 wait 4 k receive user_connect a id receive pin k send bank_init b id h receive bank_connect b a b k h id amt lr ar Cuser 2 wait b gt Cbank 2 wait ke E Chserssessions 2 i he E C pank session 2 i switch receive 4 amt receive deposit u k 4 send deposit h id amt amt receive withdraw_u k send withdraw h id amt switch receive receive success h send dispense k amt receive failure h 4 send overdraft k receive balance_u k send balance h id amt receive receipt h send receipt k amt send fin_u k k send fin_b h h Figure 5 5 Proof of a simplistic ATM to receiving the right to use it and sending an endpoint using the fin message is equivalent to relinquishing one s rights over it Moreover aside from the channels only values are exchanged the cell heap plays no role in this example The protocols of this program can once again be expressed with contracts The contracts used to initiate the communications with the user and the bank simply wait for connection requests The mech
27. a the following program would not block receive a f send a e Indeed the rule for receive says nothing about the contents of the queues of f in fact queues are not even present in our model so a semantics based on it may decide to receive whenever the contract allows it 2 What is sent does not necessarily match what is received In fact following the rules SEND and CHANNELDISPATCH the semantics of send corresponds to disposing of the message s contents and the one of receive to a non deterministic allocation of a portion of storage satisfying the message s footprint In particular the program e f open send a e 10 x receive a f close e f assigns 10 to x only if we choose such that it implies val 10 whereas it should always be equivalent to x 10 This highlights another issue of this semantics it depends on the footprint context which is supposed to be only an artifact of the proof 3 The semantics would hide both forms of leaks described earlier since the logic is not aware of them as far as the rules are concerned the contents of messages dis appear when sent and closing a channel is only about the endpoint heap not the corresponding buffers The next chapter is devoted to defining a satisfactory semantics and to establish the sound ness of our proof system with respects to this semantics Related work To the best of this author s knowledge this is the first extension
28. access it when it is being written A solution with two locks is presented Figure 1 4 Note that contrarily to the producer consumer problem any number of processes executing the code for readers can run in par allel with any number of processes executing the code for writers This solution is race and deadlock free but exhibits a new kind of misbehaviour it can be the case that readers 16 Consumer code while true with buf when items gt 0 4 x pop_buffer items do something with x Chapter 1 Concurrency and Ownership Producer code while true with buf when items lt BUFFER SIZE produce item push buffer x items X Y Figure 1 3 A solution to the producer consumer problem using CCR Reader code while true Y acquire r Writer code while true acquire w readers if readers 1 write here acquire w release r release w read here acquire r readers if readers 0 release w release r Figure 1 4 A solution to the readers writers problem using locks keep on interleaving their reads while never releasing the writing lock v thus preventing the writers processes to ever execute One should thus modify this program to ensure a fairness condition that forbids such executions This progress property is one of liveness some thing good eventually happens as opposed to the problems describe
29. and the empty heap The singleton stack is described by own x where the value of x can be specified separately if need be for instance own x x 42 is satisfied only by the stack x 42 and the singleton heap by E gt E contrarily to the case of the stack this suffices to fully specify a singleton heap A crucial feature of separation logic is the ability to split a state into two disjoint parts a i E Q1 da is true if there is a splitting c1 e o2 of o such that each substate satisfies a subformula As we will see in the proof rules this allows one to easily eliminate the issues that normally arise due to potential aliasing of memory locations The magicwand operator is the adjunct of Conjunction negation and universal quantification are standard 4 1 4 Derived formulas We can derive all the usual first order connectives from the language of Figure 4 1 and do so in Figure 4 3 Most of the formulas of Figure 4 3 should be self explanatory Let us detail the last two The formula E gt is true in a state where E can be evaluated to an allocated location of the heap and attached to the value E To negatively compare two expressions some care is needed one cannot simply define E E as E1 Ez else it would also be true of states that do not hold enough resources to evaluate E and E This is why Ej E and Ez E are added to the definition Although these formulas may seem tautological at first glance they
30. are translated into guarded non deterministic choices between each of their branches The guard is an extchoice command that is used during symbolic execution to check that each endpoint is ready to receive all the messages specified by the contract from the endpoints current states To see how the translation into verification conditions operates and in particular the role of jsr instructions let us consider the following example taken from the Heap Hop distri bution examples send_list hop and corresponding to the receiving end of the list transfer program presented Figure 1 9 page 24 get f fl gt C transfer local x e e NULL while e NULL if e NULL then f gt C transfer else el gt C end f gt Cfend pr e switch receive 4 x receive cell f dispose x send ack f e receive fin f 0 close e f emp This program is transformed into the following two verification conditions which can be observed by passing the verbose option to Heap Hop gt C transfer assign e 0 if 0 e then f gt C transfer else f gt C end e gt C end JS e xy if 0 e then f gt C transfer else f gt C end e gt C end 0 e close e f emp and if 0 e then f gt C transfer else f gt C end e gt C end 0 e extchoice cell fin if nondetO 42 then receive x cell dispose x send f ack else receive
31. based on abstract separation logic a framework for proof systems based on separation logic Heap Hop was first presented at the TACAS conference VLC10 The formalisation of contracts the modelling of the programming language and the proof of soundness presented here are original to this thesis Related work Program verification is too vast a domain of computer science to be faithfully surveyed in this introduction Let us compare the work presented in this thesis with existing litera ture on domains related to each of the three contributions pointed out above modelling of message passing programs and systems proof systems for concurrent program verification and automated verification of message passing programs The literature on the modelling of message passing concurrency is rich to say the least and has spawned a variety of models from communicating automata and process algebras to game semantics The behaviours of these systems have themselves been studied using other models such as message sequence charts or Mazurkiewicz traces Maz86 Models that belong to the family of process algebras are often derivatives of either the calculus of communicating systems CCS the pi calculus both introduced by Milner Mil80 Mil99 or Hoare s communicating sequential processes Hoa78 CSP Hoare and O Hearn have defined a denotational semantics for a message passing programming language close to CSP with dynamically allocated channels H
32. contract attached to the channel from its initial state Let us remark that this is not the case in general for arbitrary well formed open states Take for instance the following state s h e amp 1 qo amp 2 q0 e a v amp u la where is the contract do a The contents of the buffer of e is not coher ent with the fact that and e are both in the initial state of The only acceptable queues for and in this local state would be the empty ones In contrast the following states are ceremonious Cs h e e 1 qo e 2 qo e us E ap s h 1 1 amp 2 q0 c 8 a v Cs h e e e 1 41 e e 2 q1 e LE ap 110 Chapter 6 Open Behaviours and Soundness Let us formalise this intuition Definition 6 6 Ceremonious state Given a well formed open state c and an endpoint e such that cconf a e is defined and contract c e we say that o is ceremonious for e if 3C cconf c amp init init u u gt C A state o is ceremonious if it is well formed and ceremonious for each endpoint e such that cconf a is defined The set of ceremonious states is denoted by State and the set of ceremonious states that are well formed with respect to T by Statef Note that State c State and Statef c State Let us show that ceremon
33. done in any reasonable amount of time On the other hand if one is given a mathematical model of what the program does and a mathematical model of its specification one can try and formally verify that there is a match between the two Thus one can provide a mathematical proof of a program s correction which amounts to having successfully tested this program against all possible inputs Amongst the programs that one may wish to formally verify concurrent ones make for especially challenging problems while coincidentally being the ones most in need of for mal methods of verification Concurrent programs are already numerous and their num ber is bound to grow in the future Indeed due to a shift in the consequences of Moore s law which states that the number of transistors that can be placed on an integrated cir cuit doubles approximately every year recent years have seen a proliferation of computers containing more and more processors and cores capable of running in parallel a charac teristic that was previously the privilege of specialised high performance computers As a result programs are also forced to become parallel to take advantage of the increase in available computing power instead of merely relying on the frequency of single processors to increase Introduction Yet concurrent programming is still after decades of research on the subject a compli cated matter Whenever several processes interact towards a common go
34. e fin if 0 e then f gt C transfer else f C end e gt C end In this example the while loop gives rise to two verification conditions one in which it is bypassed and replaced by a generic sr instruction that sums up its effect and one that 132 Chapter 7 Heap Hop checks that the body of the loop preserves its invariant The switch receive construct is replaced by a conditional that simulates a non deterministic choice between its branches a fresh variable nondet0O is created to form the test of the conditional It is guarded by an extchoice command as described above which in this case states that f is ready to receive either cell or fin We will not give a formal description of the translation as it bears no other important details It should be straightforward to extrapolate from the explanation above One can show that the verification conditions associated to an annotated function are provable Hoare triples if and only if the specification of the function is also provable Because variables are treated as in conventional Hoare logic Heap Hop like Smallfoot has to ensure the absence of race conditions on variables without being able to rely on proof rules to do so This is achieved by tracking which variable is read or written by each function and ensuring that no pair of functions that both write to the same global variable are ever put in parallel This syntactic check is performed during the verificati
35. e gt Cfend A formal description of the symbolic execution algorithm used by Smallfoot is given in the paper Symbolic execution with separation logic by Berdine et al BCOO5b The procedure used by Heap Hop extends it to handle communication commands For instance the effect of a send can be described by the following inference rule px Ev cs Q ctt C pr E rl1 r p ym E E r Ej ES En jSry emp p 6 p xEb cs Q ctt C pr E rl r p send a E Ey En p succ C r Q la Q Similarly the rule for close takes this form 9 p 9 a 9 E ca Q ctt C pr E r 1 px E cs Q ctt C pr E r 2 p close E E p e QnQ n finals C 135 7 2 Internals 7 2 3 Entailment checking and frame inference During the symbolic execution phase one has to prove several entailments gt w and solve frame inference problems The decision procedure used by Heap Hop for formulas follows straightforwardly from the one of Smallfoot also described in Berdine ef al pa per BCOO5b Intuitively in the case of an entailment o 1 every predicate appearing in the right hand side formula has to be matched by the left hand side formula If this is the case it is removed from both sides and the entailment checking procedure continues with what is left on both sides The goal is to reach an entailment of the form emp emp where is made solely of a conjunctio
36. emp resource r r own x emp with r x with r x emp own x A emp Each individual thread can be proved as follows r own x emp with r own x emp x own x A emp emp Their parallel composition is proved using the logical equivalence emp lt gt emp emp 3Note that we did not prove that the final result of executing the whole program is to increment x by 2 One can use auxiliary variables la Owicki and Gries OG76 to achieve this 75 CHAPTER 5 Proving Copyless Message Passing In this chapter we show how to apply the local reasoning ideas of the previous chapter to the copyless message passing language with endpoints in the heap HiPMP presented in Chapter 2 The resulting logic marries contracts studied in Chapter 3 and separation logic within a proof system that discharges parts of the verification of a program to the verification of its contracts The contracts are annotations in the source code and are used to abstract the contents of the communication buffers in the models of the logic as well as to be able to assert further safety properties about communications Our analysis of a program p follows these steps 1 Decorate p with contracts at each open instruction 2 Prove a specification p v which ensures that p does not fault on memory accesses and obeys its contracts 3 Prove that the contracts are fault free and leak free in which case p do
37. error or p 9 OwnError 2 ifp a ex p o then either p a error or there exists 0 05 such that ec 0 0 po v pois 0 gt gu Proof The two parts of the lemma can be proved independently The first part of the lemma follows from a straightforward induction on the length of the derivation and a case analysis on p Let us focus on the second property For all commands except for communications and interferences this property actually has a stronger formulation identical to the usual locality principle of separation logic models where interferences are not needed and g remains untouched For all these commands and more generally for all programs p made only out of these commands if p c eo gt p a then either p g4 error or there exists 9 7 such that z 1 Ia g g 1 1 p a gt p 01 This is a standard result straightforward to prove by a case analysis on p Bro07 Vaf07 Let us now examine the case of open close send external choice receive and in terferences Let 9 s1 h1 k1 k and 9 02 ko e p e f open Straightforward e e e Endpointx dom k U ko implies e e e Endpoint dom k No interference is needed on 02 e p close FE E2 A step of interference can erase the endpoints involved if they are also present in k and p has deallocated them from k e Suppose that p send a E E2 that all the hypotheses of the successful
38. higher level Contracts are part of our framework as well our logic tries to prove a given program cor rect with respect to certain contracts while these contracts are analysed separately We were able to formally establish that good and bad properties of contracts sometimes rub off on the programs that implement them Moreover including contracts gave us the opportunity to formalise the ideas implemented by the Singularity Operating System such a formalisation was not provided by their authors We believe we have achieved such a clean separation of concerns in our approach Introduction Automation Reasoning about programs that are concurrent and have direct access to the heap is chal lenging Combating the complexity of such reasoning with local reasoning and compo sitionality makes for simpler proofs of programs Yet as we are interested in verifying concurrent memory manipulating programs without first abstracting their behaviour by casting them into models more amenable to other verification techniques like finite model checking CES86 the vast majority of properties this thesis tries to establish about pro grams are undecidable ones Nevertheless being able to give arguably simple human understandable proofs of programs supports the hope that these proofs may be automated at least to some extent Indeed one may circumvent this issue and write automatic tools nonetheless either by helping the tool for instance
39. i In particular true is not precise and neither is x Ik emp v x Ik x However emp xI emp and xIF x are all precise Without this requirement soundness is lost as first pointed out by Reynolds Let us show here why by rephrasing O Hearn O H07 Section 11 Let one emp 10 gt and suppose that the resource r has been assigned true as invariant which is imprecise Consider the following proof SKIP emp skip emp emp true skip emp true FRAME WEAKENING emp v one true skip emp true emp skip emp SOR emp v one with r skip emp 73 4 2 Proof system From this derivation one can prove the following two triples by either applying the proof above right away or by framing one first emp v one with r skip emp WEAKENING one with r skip emp emp v one with r skip emp WEAKENING emp with r skip emp FRAME emp one with r skip emp one WEAKENING one with r skip one The conclusions of these two derivations are incompatible The first says that ownership of the single cell is swallowed up by the resource while the second says that it is kept by the program Applying the conjunction rule with these two conclusions gives us as conclusion one A one with r skip one emp and finally using the rule of weakening one with r skip false This suggests that the ab
40. in general and contracts in particular As they are not specific to the class of dialogue systems we define them for the more general class of communicating finite state machines bounded system is one in which there exists a bound on the size of the queues For instance the system of Figure 3 2 is bounded but a system that contains the following machine is not because this machine can enqueue arbitrarily many a messages in buffer 1 48 Chapter 3 Dialogue systems lla Definition 3 16 Bounded system A system is k bounded if for all reachable configura tions q1 Qn W1 Wp wi k for all i A system is bounded if there exists a bound k IN such that is k bounded A system is in a deadlock state if each participant is waiting for one of the other partici pants to send a message In this case they are all stuck waiting for each other s messages Note that the special case where all participants are in a final state is not a proper deadlock since the run of the system is finished The system of Figure 3 2 is deadlock free in that sense but the one below is not q1 qp a u is a reachable deadlock configuration the second machine tries to receive from an empty channel Kan 0 0M Definition 3 17 Deadlock free system We say that a configuration q1 qn 1 wp of a system is a deadlock configuration if 1 all q are receiving states 2 all the inspected queues are empty
41. in the closed semantics This is done in two steps we first show that valid programs in the sense of the open semantics that is programs which do not reduce into an ownership error or a protocol error with fault free contracts do not fault on message receptions in the open semantics and then that message reception errors in the closed semantics correspond to errors in the open one Put together these two facts show that valid programs with fault free contracts have no unexpected receptions in the closed semantics Lemma 6 11 Fault correspondence Let c be a well formed state with respect to V If p o OwnError p c ProtoError and p o gt MsgError then there is e such that contract o e is defined and cconf a e contains an unspecified reception configuration for contract c e Proof Assume the hypotheses Since p o gt MsgError there is a guarded external choice for which an unexpected message is in one of the considered buffers say in the buffer of e Since p o OwnError e is in the domain of the local part of a hence contract o and cconf a e are defined Moreover since p o ProtoError the messages expected by the guarded external choice composition match exactly the ones of contract o Thus the unexpected message is also unexpected in any configuration of cconf a with respect to contract a hence cconf a e contains an unspecified reception configuration for contract a In particular if a progr
42. its environment The main results of this chapter are the soundness of the logic with respect to the open semantics Theorem 6 1 the connection between the validity for the open semantics with fault free contracts and the runtime safety of the closed semantics Theorem 6 2 and the 101 6 1 Open states leak freedom of programs provable under an admissible footprint context and leak free con tracts Theorem 6 3 Technical lemmas are kept in subsections 6 2 2 6 3 1 6 4 1 and 6 4 3 Many proofs of other variants of separation logic exist The original proof for concurrent separation logic is due to Brookes Bro07 and is also based on an intermediate open se mantics although a denotational model based on complete traces is used instead of an opera tional one as in this thesis This result was later made agnostic in the programming language and the underlying state model by the framework of abstract separation logic COY07 as discussed in the previous chapter Proofs for other extensions of separation logic include several ones for RGSep VP07 Vaf07 and for CSL with storable locks and threads either based on operational models GBC 07 or on an oracle semantics HANO8 Some of these proofs might be applicable to our logic and prove its consistency by somehow encod ing message passing into their framework Yet none of them include message passing or contracts as primitives and thus the links to the semantics of copyless messa
43. locality and parallel decomposition lemmas Lemmas 6 5 and 6 6 112 Chapter 6 Open Behaviours and Soundness 0 k e State gc p a p c Ia d k gt 6 k p a p p a p c s Figure 6 7 Open operational semantics of interferences Environment interferences Interferences from the environment are modelled by a sin gle rule given in Figure 6 7 The rule transforms an open state into one with the same local state but where the contents of the buffers may have changed The resulting state must re main ceremonious with respect to the footprint context The changes include the possibility for the environment to perform sends and receives on endpoints that are not directly con trolled by the program in accordance with their contracts and to open and close channels not visible to the program Interferences are denoted using a dashed arrow gt and tran sitions that are either a program step or an interference are written with a squiggly arrow ec TX This modelling is an over approximation of what a ceremonious environment that also respects the ownership hypothesis might really do with this definition the environment can modify the buffers of endpoints owned by the program and even of endpoints in the local state of the program provided that it leaves the buffers in a state coherent with the protocols of these endpoints An environment respecting the ownership hypothesis would not modify the buff
44. of endpoints all the cases that do not modify the endpoint heap trivially produce well formed states from well formed states Moreover since the contents of the queue are not important in the axioms the cases of send and receive are straight forward as well This leaves us with open and close In the case of open since the new endpoints e e are allocated in the endpoint heap at the same time and Channel held on o it still holds on o Suppose that Irreflexive does not hold anymore and let be such that mate k e The misbehaving endpoint cannot be one of the newly allocated ones since they clearly do not violate this axiom nor can it be one of the other endpoints since o is supposed to be well formed This leads to a contradiction Similarly Involutive only needs to be verified on the newly allocated endpoints on which it does hold The case of close is straightforward as it can be shown that any substate of a well formed state is itself well formed Semantic equivalence of programs Let us now show some basic properties of the programming constructs For instance one should be able to prove that is associative and that O and are associative and commutative This calls for a notion of program equivalence we take as a basis for such a notion a coarse denotational semantics based on the set of reachable states 41 2 2 Semantics Definition 2 1 P
45. of programs that make formal verifica tion challenging explicit memory management and concurrency To tackle these difficul ties we base our approach on two recent developments On the one hand concurrent separa tion logic produces concise proofs of pointer manipulating programs by keeping track only of those portions of storage owned by the program We use such local reasoning techniques to analyse the fluxes of ownership in programs and ensure in particular that no dangling pointer will be dereferenced or freed at runtime On the other hand channel contracts a form of session types introduced by the SinG programming language provide an abstrac tion of the exchanges of messages that can be used to statically verify that programs never face unexpected message receptions and that all messages are delivered before a channel is closed The contributions contained in this dissertation fall into three categories First we give semantic definitions to copyless message passing programs to the ownership transfers they induce and to channel contracts and link the three together In doing so we provide the first formal model of a theoretically significant subset of the SinG programming language In particular we show that some properties of channel contracts rub off on programs which justifies their use as protocol specifications Second we introduce the first proof system for copyless message passing based on separation logic and channel contr
46. of separation logic to mes sage passing that supports copyless message passing Not long after our own another ex tension to copyless message passing has been published by Bell et al BAW10 Their 98 Chapter 5 Proving Copyless Message Passing logic bears remarkable similarities to ours except on two points regarding communica tions firstly they support multiple producers and consumers communicating through a single channel that is they allow endpoints to be shared between processes secondly they do not consider safety of communications as an issue and thus do not consider contracts hence they model the contents of channel buffers explicitly in the logic In our setting sharing endpoints for instance by assigning permissions to them would prove troublesome in the logic if a process shares an endpoint with its environment then the control state as sociated to this endpoint may change at any time as a result of sends or receives performed by the environment on this endpoint Hence the logic may no longer keep track of the cur rent state of this endpoint reliably The proof of soundness of Bell ef al is closely related to our first published proof of soundness VLC09 where we overcome the difficulties that come with local reasoning in abstract separation logic by assigning histories to endpoints as they also do Other extensions of concurrent separation logic have been created in the past We have already mentioned how G
47. pi s xi v h k buffer e a j 1 Fils amp amp En s En 3j 3a 3v Ja buffer k e a v a amp Vj ep j aj a n xj receive a Ej p s h k gt MsgError jl Figure 2 5 Operational semantics of communications e For E1 Esto succeed the stack must be able to evaluate Ey and E and Ei must be allocated in h The mutation of this cell then takes place Communication commands are grouped in Figure 2 5 e f open allocates two fresh endpoint locations in the endpoint heap k and sets their value so that they point to each other and have initially empty buffers the empty word is written It faults if either e or f is not allocated in the stack close E E25 checks that the values of E and E point to endpoints which are each other s peer hence which form a channel If this is the case it deallocates them from the endpoint heap Note that any message remaining in the queues is lost which is often undesirable Part of our analysis will try to ensure that it is never the case that messages are left in the queues when a channel is closed If any of the conditions mentioned above is not satisfied the command faults send a E E25 looks up the value of E in the current stack which must be an allocated endpoint address of k the value v of E then fetches the peer e of e from 38 Chapter 2 A Model of Copyless Message Passi
48. qi j1a q Ti w wj a and qj qk and w wi for all k i and l j J e if T is a receive action j a then there is i 1 n such that qi j a q T wj a w and q qk and w wy for all k i and j We write gt and when G can be inferred from the context A run of a system is a sequence of consecutive transitions from the initial state Definition 3 15 Run of a system Given a system a run is a sequence of transitions 65s Cossus UK Eus Ci where k gt 0 C Cis1 and Co is initial The run is accepting if C7 is final If k 0 the run is simply Co it is accepting if Co is final A configuration is reachable if there is a run of the system that leads to it Tj Tj Kt1 s T1 T2 Tk T1 We write Co Ci Cha or Co Ck 1 for a run Co T2 Tk ORF A s C1 C Ca Cy Ch 1 sometimes omitting some configurations and writing 6e 0 instead We write for the reflexive and transitive closure of gt The accepting runs of our example Go of Figure 3 2 correspond to all the interleavings of the sequences of actions 1 a 1 b 27a 2 b and 17a 2 a 1 b 2 b that respect the precedence of a send over the corresponding receive for instance l a 1 b 1 a 2 a 17b 2 b 27a 4 Go uu awe CI q q2 ab 4 FE aet q 92 6 a gsx dE q q2 ab RES 2 b Dar 4 Qfruu 3 1 4 Safety properties Let us describe the properties we are interested in for dialogue systems
49. regions O H04 CCR for short see page 13 In this case proofs keep track of the resources available to a program via a con text A context lis a list of pairs r y that associates resource identifiers to separation logic formulas their invariants Resource invariants must hold when the resource is cre ated can be assumed every time a resource is successfully acquired and have to be asserted when the resource is released This behaviour is enforced by the rules of Figure 4 7 that are added to separation logic s proof system The sequents are extended to support contexts and are now of the form T p 4 Previous rules can be adapted to this new setting by adding I uniformly on the left hand side of each turnstile The resulting logic is called concurrent separation logic CSL Though it is but one concurrent version of separation logic it has the primacy of being the first one Note that the CCR rule prevents the same resource from being acquired twice since it removes the resource from the proof environment when entering the critical section This catches some of the possible deadlocks of programs Precision For the proof system to be sound the resource invariants must be precise for mulas Precise formulas unambiguously identify a piece of state Definition 4 1 Precise formulas A formula q is precise if for all instantiations i of log ical variables and all state c there is at most one substate o lt o such that o
50. role 1 each receive performed on this endpoint has to be one of the available receiving actions going out from q but conversely and because the choice of which message is in the queue is not in the hands of the receiving endpoint all possible receive actions should also be accounted for in the external choice composition This is what is required by the second premise of the rule ai 1 n a dq succ r q a q The third and last premise of the rule requires each possible continuation to be prov able with a precondition that differs from the precondition of the composition in three aspects the control state of the receiving endpoint is updated the piece of state attached to the message is tacked on the current state using the spatial composition and x is given a new value Z that corresponds to what the formula describing the footprint of the message states about the value of the message To give more intuitions on this rule let us consider an example with a single branch cell We let do a and T cell val gt The following proof is derivable x elre o 1 0 x receive cell e x elkx ZaA er 1 q1 Zo x elker 1 q1 x gt dispose x x eI e gt 1 q1 x e i e gt 1 q1 Soundness Although we will not prove the soundness of our proof system before the next chapter let us give an intuition about what is proved by
51. sent over channels in the sense that one may send the loca tion of an endpoint on a channel thus letting the receiving process know of the location of this endpoint which makes it possible for this process to use it to send and receive over it As we consider only point to point communications see next section concurrent accesses to the same endpoint are forbidden This usually means that further access to a cell or end point location sent over a channel is forbidden to the sending process as the receiving one may now interact with them In other words as already mentioned before ownership of the contents of a message is lost upon sending and granted upon receiving Using endpoint transfer it is possible to transfer a value indirectly over a channel by encapsulating it inside another channel as in Figure 1 7 In this example the address of a memory cell is sent over a private channel the receiving endpoint of which is sent to another process This process retrieves the endpoint and can then receive the desired address from it This program has a memory leak it fails to dispose the channel e ce11 f ce11 Another use for endpoint passing mentioned earlier and pictured in Figure 1 8 is for channel closing the example of Figure 1 6 can be extended by sending e over itself after sending x so that get ce112 can close the channel e f The same extension is possible 22 put cell indirect e x local e cell f cell e cell
52. similar to New starting from an empty heap it allocates two endpoint locations They are initialised according to the contract that decorates the open com mand and to point to each other CLosE The rule verifies that the two expressions given as arguments point to two endpoints that form a channel they point to each other and that are both in the same final state of the contract hence that the whole channel is in a final state according to the definition of dialogue systems associated to contracts If it is the case the channel is deallocated and the heap is considered empty SEND Let us consider a simplified version of this rule first in the case where the footprint does not mention the sending endpoint SEND1 succ r q a q Ei Xn E2 Y AX gt X r q X X m Y kr send a E1 E2 Ere X r q 8l 5 1 Proof system OPEN do init e f I emp Hp e f open e flke XAL Y A X Y 1 q0 Y gt X 2 90 CLOSE qy finals FA X1 Ea X A X gt Xo 1 gp x X2 X1 2 qy var E Ez IH kr close E o var E1 E2 lr emp SEND succ r q a q FA XA Ez Y MX X r q X gt X 1 8 X Xr Y x 9 kr send a E1 E2 4 CHANNELDISPATCH n gt AE Y Ax x true i 1 fa i 1 n a dq succ r q a q Vi Jd succ r q a q BS aper NA a On
53. tape if it is on the first letter then the left branch is taken otherwise the right one is taken and the letter that was read is remembered by the control state This allows the CFSM to travel deterministically along the tape while searching for the head Let us describe the second case the first one being similar The tape is unrolled until the head is found if when in the control state ay the machine receives another headless letter 51 3 2 Verification of communicating systems Figure 3 3 A few of the transitions of the copycat machine la Figure 3 4 Encoding of a transition of 9Jt moving the head to the left aw O an is sent back not pictured here and the machine moves in state apr The process is repeated until the head is found When this is the case that is when a lt q is received and assuming the previous letter was ap the machine sends back a q r effectively moving the head to the left and updating the control state of the Turing machine The final step is to send the updated letter under the previous location of the head ay Not pictured in the figures are transitions that reset the transition machine whenever we reach the end of the tape from every control state a there is a transition back to Qsim f um s 0 labelled by 0 and there is a loop from qsim to qsim consisting of two transitions qsim gt
54. that may be executed only when a specific resource is held This ensures mutual exclusion between the CCRs guarded by the same resource Resource This is a theorem of the folklore known as the data race free guarantee AH90 which has been formally proved to hold for many existing architectures recently Alg10 BP09 OSSO9 13 1 1 Concurrency and the heap declarations and usage are syntactically scoped Using resources we can write a correct race free version of our example resource r in x 0 local y local 2 with r 1 with r y x tli z x 1 X y X z Or more concisely writing x for x x 1 resource r x 0 with r x with r x All the executions of the program above are race free and give a final value of 2 for x Deadlocks Although they may be used to prevent races conditional critical regions can themselves introduce errors in the form of deadlocks as in fact any means of synchroni sation between programs A deadlock arises when two or more processes are waiting for each other to take a step in a cyclic fashion for instance process A is waiting for process B to take a step while B itself is waiting for A As neither of them can make any progress they are stuck forever Deadlocks can occur as soon as one has the ability to use nested CCR Consider the following example with ri with r2 skip with r2 4 with ri skip Suppose now that the process on
55. the environment in the sense that if owned a So ho ko they are not in the domain of the endpoint heap ko In this case these endpoints and every footprint of every message appearing in their buffers will appear in flat a but not in owned o or because some endpoints form a cycle of ownership as described in the previous chapter page 94 this is the case we want to eliminate 6 4 4 Leak freedom Let us study more precisely the formation and evolution of the unreachable portion of an open state c the difference between flat o and owned a over the execution of a pro gram which we mentioned above as it may be a symptom of a leak Complete states We call a state complete if the domains of its open endpoint heap and its owned endpoint heap coincide In other words the environment controls no endpoint whose peer is owned by the state the ownership of both endpoints of every channel present in this state can be retrieved by performing enough receives Definition 6 12 Complete state An open state a 0 k State such that owned o so ho ko is called complete if dom k dom k In particular if amp emp and c is complete then o and close o u where u is the empty closed state 2 Complete states have an empty unreachable portion their flattening coincides with their owned portion Lemma 6 15 Ifo 6 k is complete then flat o owned o Proof Let s h k The proof i
56. the immediate accesses of p from o ia p o iw p o Uir p o The predicate norace pi po c is defined as true if iw p1 0 Nia p2 o iw po oc n ia p o rene on is otherwise The semantics of all the other programming constructs is standard 2 2 4 Properties of the operational semantics Well formed states In this subsection we prove some properties that act as touchstones for the operational semantics presented above First the operational semantics does not create ill formed states from well formed ones 40 Chapter 2 A Model of Copyless Message Passing Program Immediate writes Immediate reads assume B p var B x E p x var E x new p x x E p x var E u E Fil E p Fils var E E2 dispose E p GE var E e f open p e f close E Eo p es E2 var E Ez send a E E2 p 1 var E1 E2 lxi receive a Ej pi 7 uM iun a UP var E otherwise Table 2 1 Sets of immediate writes and immediate reads of programs executing from a state s h k Lemma 2 1 For each well formed state o and program p if there are p o such that p o gt p o then c is well formed Proof Assume that p o gt p o that o s h k and that o s h k is well formed We need to prove that o satisfies Channel Irreflexive and Involutive Since they are solely properties
57. the left successfully enters the first critical region corre sponding to r1 before being interrupted The second process can then enter its first critical region corresponding to r2 which has not yet been claimed by the first process but cannot enter the next one corresponding to r1 The first process is now stuck as well and in fact the whole program is stuck in a deadlock The usual solution to avoid this kind of deadlocks is to assume an order that must be followed whenever a process acquires resources for instance that one should never attempt to acquire r2 before r1 This would forbid the problematic program above Locks Locks can simply be viewed as monitors where the beginning and end of criti cal regions are no longer statically determined but are instead made operationally explicit through the operations acquire 1 and release 1 where 1 is a lock identifier In this sense they are more general and allow more complex behaviours than monitors Moreover in most settings one can dynamically allocate new locks on the heap and hence have an unbounded number of them which complicates the analysis On the other hand this al lows fine grained synchronisation for instance by associating each node of a linked list to a different lock and then manipulating the list concurrently with an hand over hand lock ing scheme HS08 Although seemingly more complex some of these programs are also 14 Chapter 1 Concurrency and Ownership a
58. the notion of the reachable owned portion or reachable local state of a well formed open state c 6 k The owned portion of a state corresponds to every piece of state that can be reached in c by retrieving the footprints of the messages in the queues of the endpoints present in 6 adding them to the local state and then repeating the process until a fixpoint is reached The fixpoint is reached when the queues accessible from the last local state all have empty footprints In the definition below emp k sets the footprints of the buffers of k to it is the lifting to open endpoint heaps of the function Msgld x Val x State gt Msgld x Val x State a v 6 gt a v In particular flat emp k for all k Definition 6 11 Owned portion of a state Let c s h k k be a well formed open state The reachable owned portion or simply the owned portion owned a of the state c is defined inductively by e if flat k dom k then owned e s h k e otherwise let ox flat k dom k and k emp k dom k wk dom k 5 dom k Then owned c owned s h k e p k This definition is well founded since the number of buffers with non empty footprints decreases strictly at each step The resulting session state is well formed Reachable owned states allow us to circumscribe the part of the state that the program owns either directly in its local state or virtually because the correspondin
59. to flat c where the endpoints have been deallocated from the endpoint heaps From this observation it follows that close a 07 send If po p c then it is easy to see that since in the reduction rule 6 is moved from the local portion of the state to the receiving queue of the peer of the origin endpoint e or of using similar notations for a as for c More over if a is the message identifier and v its value then K amp k e and k e k e a v a hence n k n k buffer e e n k e a v k buffer amp buffer k a v which shows that close o 0 receive If p a gt p c then it is easy to see that since in the reduction rule O4 is moved from the receiving queue of the endpoint to the local portion of the state oy and or only differ in the value of x in the stack which now contains v Moreover if e is the receiving endpoint a the message identifier and v its value and n k e ai v a buffer k amp then n k e a buffer k e hence close a 0 The other programming constructs are straightforward cases By putting the three lemmas above together we get a proof of Lemma 6 9 hence of Theorem 6 2 121 6 4 Properties of proved programs 6 4 3 Owned portion of a state Our next property of interest is leak freedom However to define what constitutes a leak in the open semantics we first neeed to introduce
60. to receive from the buffer if it is empty nor should the producer process try to enqueue something if the buffer is already full To avoid these situations they must synchronise A solution with two signals non empty and non full is presented in Figure 1 2 The example assumes that the buffer can be accessed through the pushbuffer x and x popbuffer operations that respectively enqueues the value of x into the buffer and dequeues the first value in the buffer and stores it into x The producer can choose a new value to enqueue using any function produce item provided that this function does not introduce bugs of its own or attempts to wait or signal non empty or non full The capacity of the buffer is BUFFER SIZE and the number of items currently in the buffer is items initially 0 This implementation may deadlock as a result of the following race condition between the producer and the consumer Suppose that the consumer process notices that the buffer is empty and gets ready to sleep but before the wait non empty command is issued the producer process is scheduled and makes a whole pass it enqueues an item increments items and seeing that the buffer is empty signals the consumer However since the con sumer has not yet gone to sleep the signal is lost forever the consumer will then call sleep never to be awaken by the producer What can only happen then is that the producer fills up the entire buffer and puts itself to slee
61. when E does not evaluate to an address present in the heap Thus this rule stands for the following three rules x e dom s E h l v var x E dom s x El s h k 2 skip s x v h k x E s h k gt OwnError E l dom h x E s h k gt OwnError 2 2 3 Operational semantics The reduction rules of the operational semantics are given Figures 2 3 to 2 6 Let us review the effect each command can have on a given state s h k Figure 2 3 groups the stack commands skip does not alter the current state e assume B faults if B cannot be evaluated in the current stack Otherwise it will either block or do nothing depending on the truth value of B 36 Chapter 2 A Model of Copyless Message Passing B s true skip 0 gt skip 0 assume B s h k skip s h k x dom s E v x E 6 h k gt skip s x v h E Figure 2 3 Operational semantics of stack commands x e dom s l Cell dom h v Val x new s h k gt skip s x 1 k l v k E s 1 le dom h dispose E s h k skip s hx D k x dom s E h l v E s hk gt skip ls x v h k ES EA s Ez U le dom h E E s h k skip s h l v k Figure 2 4 Operat
62. while exploring the tree More precisely the threads have to collaborate and dynamically balance the load of their tasks The solution we propose to this hypothetical problem follows We suppose that the treat ment of each task consists solely of disposing of the corresponding node but in theory this could be an arbitrarily complex operation One of the threads called the left thread will dispose of the left children of all of the internal nodes of the tree and the other thread the right thread will dispose of all the right children Both threads hold one endpoint of a shared channel Initially if the tree is not empty the left thread starts with the left subtree one step down If this subtree is not empty it disposes of its root sends its right subtree two steps down over the channel and proceeds with the left subtree The right thread behaves symmetrically If the tree it is working on becomes empty the thread sends an acknowledgement and waits for a message It may either receive a new tree to be disposed or an acknowledgement The thread maintains a counter holding the number of tasks that it has sent and that have not yet been processed and acknowledged by the other thread When this counter reaches zero the other thread is done hence the communication can be stopped The code for the left thread is presented in Figure 7 4 The code for the right thread is symmetric it sends the left subtree and keeps the right one wh
63. 1 W2 is reachable with for instance jwi n4 and wa na If n gt 0 then since is half duplex by Lemma 3 4 wa u By Lemma 3 4 again and Lemma 3 3 the configuration can be reached from another configuration q q u u by a sequence of sending transitions only Thus n N If n 0 and n gt 0 the reasoning is similar Let us summarise the results obtained in this section Corollary 3 1 For every contract if is deterministic and positional then it is fault and deadlock free If moreover all its final states are synchronising then it is leak free and if all its states are synchronising it is bounded Proof Direct consequence of Lemmas 3 6 3 7 3 8 and 3 9 In particular Singularity contracts are bounded and free from faults deadlocks and leaks 3 3 2 Contract verification is undecidable Theorem 3 2 The following six problems are all undecidable 1 Input A synchronising and deterministic contract Output Whether or not is leak free 2 Input A synchronising and positional contract Output Whether or not is leak free 3 Input A synchronising and deterministic contract Output Whether or not is deadlock free 4 Input A synchronising and positional contract Output Whether or not is deadlock free 5 Input A synchronising and deterministic contract Output Whether or not is fault free 6 Input A synchronising and positiona
64. 138 TAZ Case studies a Ett a ge Si ER a a e 139 Conclusion 143 vii Remerciements Ma gratitude va en premier lieu tienne Lozes qui a encadr mes travaux avec enthousi asme gentillesse et rigueur scientifique Merci pour ta disponibilit sans faille Je remercie galement Cristiano Calcagno qui a guid mes premiers pas dans le domaine de la logique de s paration et qui a donn le point de d part de cette th se Je remercie Daniel Hirschkoff pour avoir parrain ma vie scientifique et Alain Finkel pour avoir dirig ma th se Je remercie toutes les autres personnes avec qui j ai eu l occasion de parler de science pendant ma th se et qui m ont encourag continuer Benedikt Bollig Steve Brookes Luis Caires Byron Cook Dino Distefano Rob Dockins Mike Dodds Philippa Gardner Maurice Herlihy Aquinas Hobor Florent Jacquemard Peter O Hearn Fran ois Pottier Hugo Torres Vieira Ralf Treinen Viktor Vafeiadis Hongseok Yang Nobuko Yoshida et bien d autres Merci tout le LSV Renaudeau et Iris repr sentent pour m avoir fourni un accueil chaleureux des voyages scientifiques panouissants et un environnement de travail stimu lant Big up aux Gawky Flutch Nicolas et Oanig et aux geeks de sos bgoglin Dain GruiicK iderrick julio Louloutte mandos mrpingouin nanuq Nimmy proutbot stilgar TaXules tonfa Vinz youpi Merci surtout ceux qui ont contribu rendre moins aride la t
65. A CFSM B Q qo T is positional if it has no mixed state A system is positional if all its constituting machines are The system Gg is both deterministic and positional 3 1 2 Dialogue systems and contracts Let us now introduce dialogue systems and contracts A dialogue system is a communi cating system of only two machines and two buffers 1 and 2 where each buffer is used in only one direction and a contract is a compact representation of a dialogue system whose CFSMs are each other s dual Definition 3 6 Dialogue system A dialogue machine is a CFSM M B Q q0 T where B 1 2 and where the actions of T are either all of the form 1 a or 2 a or all of the form 2 a or 1 a A dialogue system is a communicating system D F M Ma consisting of precisely two dialogue machines M 2 1 2 Qi qo Ti where Mi sends on channel 1 and receives on channel 2 and vice versa hence for each machine M the set T contains only actions of the form i a or 3 1 a Since on each machine of a dialogue system the sending actions are all performed over the same buffer and similarly for the receiving actions we will often omit buffer numbers in their presentation For instance the example of Figure 3 2a can be depicted as 7a 7b la lb The dual of a CFSM M is M where the actions n a are changed in n a and vice versa Definition 3 7 Dual actions dual machines The dual of an action n a is n a The dual of an ac
66. B hence B is defined If it evaluates to true then c 2 var B 1 B emp which is the postcondition If not then the program diverges hence the property is also satisfied ASSIGN NEW DISPOSE Lookup MUTATE OPEN CLOSE similarly straightforward SEND Suppose that FA X AE Y X X r q X X r q gt X Xr Y x g ik 116 Chapter 6 Open Behaviours and Soundness In particular the local part of holds ownership of var E E2 and of the endpoint pointed to by Ej Ifi X i X amp and i Y v then a i EX p X dana X zd X r q As X X r Y Thus s A k control e lt q i E y X X r Y Hence there are Ga and 6 such that 6 e6 6 64 i E Yal X X r Y and 6 i 6 This forbids the program to reduce to OwnError by the second reduction rule of send The premise of the SEND rule moreover forbids the program to reduce to ProtoError hence only the first and successful reduction rule of send applies and the resulting state is 0 k e k e a v 65 As previously stated 6 i hence the result Let us now assume that Hp 9 p 4 is not an axiom We discriminate on the last inference rule of the proof tree see Figures 5 1 4 5 and 4 6 Let again g s h k k e CHANNELDISPATCH Suppose that a i Y r q x The first precondition of the inference rule n o gt ACE Y Ax Xi t
67. Each state contains the list of outgoing transitions from this state To check determinism Heap Hop searches each of these lists of transitions for duplicate actions The fact that a contract is positional is as easy to establish Heap Hop makes sure that each list of outgoing transitions only contains actions in one direction either only sends or only receives Finally for each final state of the contract Heap Hop checks if there is a cycle consisting of either only sending or only receiving actions from that state by a naive reachability analysis from that state If this is not the case the contract is synchronising because all its final states are As we have discussed in Chapter 3 and more precisely in Corollary 3 1 contracts that satisfy all three of these conditions are fault and leak free As we have seen in Theorems 6 2 and 6 3 of the previous chapter programs that can be successfully proved using such con tracts are themselves reception error free and will not close channels with undelivered mes sages in them The conformance of the program to the declared contracts is checked at symbolic execution time using the logical rules described above and derived from those of 136 Chapter 7 Heap Hop Chapter 5 Heap Hop uses the criterion of Lemma 5 3 to check that the footprint context is admissible hence that leaks are completely avoided if the contracts are leak free 7 3 Output 7 3 1 Properties of the contracts If a cont
68. For all atomic commands the lemma follows straightforwardly either because the open semantics exhibits an extra faulting condition or from the fact that dom s dom s and dom h dom h The result is also straightforward to prove for all of the programming constructs reduc tions except for the case where p exhibits a race Suppose now that p pi paz and that norace p1 po 7 does not hold that is iw p1 o n ia p2 0 or iw p2 0 n ia p1 0 Y We need to show that given any splitting e 0 Of g either p1 0 gt OwnError or p2 0 gt OwnError Observe that in order for a program p not to reduce into an error in the open semantics the local state must contain in its domain all the variables and locations that it immediately reads or writes to that is the domains of the stack and heaps must contain a p c Thus the fact that these sets are not disjoint for p and pa implies that there is no way to split c into two disjoint substates over which p1 and pa would not fault Indeed in order for p1 and p not to fault respectively from c and c the domains of the stacks or the heaps of c and c must overlap Hence norace pi po does not hold and pi p c OwnError Proved programs with fault free contracts are message fault free We now turn to the second point of the runtime validity property that we wish to establish we show that valid programs with fault free contracts do not reduce into MsgError
69. OO8 Yet very few other models of message passing concurrency if any include simultaneously a tractable and realistic model of the heap None of them are able to model storable channels or contracts in a natural fashion Recent progress has been made in the verification of communicating automata our model of contracts Our analysis shares many concerns with the recent work of Stengel and Bul tan who have also studied the contracts of Sinc in a formal setting SB09 albeit not relating them to a general model of message passing programs A cousin of our analy sis of communications is the type system of Takeushi ef al THK94 HVK98 for a pro cess algebra derived from the pi calculus which describes channel protocols using session types and has been the starting point of a rich and growing literature In particular session types can be used to describe asynchronous communications between any number of partic ipants HYC08 whereas this thesis focuses on the binary case and to capture event driven Introduction programming HKP 10 Finally our own analysis of contracts has many roots in the study of half duplex communicating automata by Cece and Finkel CF05 None of these models apply to heap based communications and in particular to our model of storable channels In the domain of proof techniques for copyless message passing the logic of Bell et al BAW10 that also extends separation logic with copyless message passing is
70. Open operational semantics Open states composition The composition of two open states c 91 k and a 92 ko is defined provided that their local parts are disjoint and compatible as session states k and ky agree on the buffers of the endpoints in the intersection of their domains the resulting open state as defined below is well formed When this is the case we write c c and the composition is defined as 91 ki e 62 K5 61 e 95 ki U ko where the union of two partial functions f and g with the same codomain S is defined provided that they agree on the intersection of their respective domains of definition as dom f udom g S fug E us if x dom f g x ifxe dom g 6 2 Open operational semantics From now on let us consider as fixed a well formed footprint context I 6 2 1 Open semantics of programs Notations As for the closed semantics we define shorthands to describe updates to the current open state and more precisely to its local part If k e amp r q we write control k e for q role k e for r and k control e lt q for k e r q Given two session states 0 and 6 recall that 6 is a substate of G2 written 01 lt do if there is amp such that 61 e 0 o In this case amp is unique thus we can write 02 01 for the only such c Let us give the reduction rules of the open semantics The rules implicitly depend on I and ar
71. Session types THK94 represent another proposal to struc ture communications and have been implemented as an extension of Java called Session Java HYHOS Ordering of messages and reliability of channels When the two participants of a communication are physically apart for instance in the case of two machines communicat ing over the Internet implementation choices have to be made that may no longer ensure that messages arrive in the order they were sent or that they will arrive at all The Internet Protocol IP for instance ensures nothing of the sort and packets may even arrive twice or be corrupted during transport Most of the time an additional layer for instance the Transmission Control Protocol TCP controls such bad behaviours and restores the first in first out FIFO ordering of messages as well as their integrity As we are interested in communications that occur mostly within a single machine for instance in low level operating system code we choose not to concern ourselves with what could happen on longer distance communications and consider only reliable channels with a FIFO ordering of messages Closing a channel It is common in message passing languages to close a channel by closing each endpoint separately For instance in SinGf closing an endpoint on its own results in a special message ChannelClosed being sent to its peer The other endpoint can continue sending on the channel even after receiving the closing message
72. THESE Pr sent e d L Ecole Normale Sup rieure de Cachan en vue de l obtention du titre de Docteur en Informatique HEAPS AND Hops Soutenue le 18 f vrier 2011 par Jules VILLARD C PAYS cole Doctorale Sciences Pratiques C A C HAN devant un jury compos de Peter O HEARN rapporteurs Nobuko YosHIDA Cristiano CALCAGNO examinateur Byron Cook pr sident du jury tienne Lozes directeurs Alain FINKEL Abstract This dissertation is about the specification and verification of concurrent message passing programs that operate over a shared memory In this setting instead of copying messages over channels processes may exchange pointers into a shared memory where the actual con tents of messages lay Channels are themselves objects in the memory or heap that can be communicated thus achieving full mobility This flexible and efficient programming paradigm must be used carefully every pointer that is communicated becomes shared be tween its sender and its recipient which may introduce races To err on the side of caution the sender process should not attempt to access the area of storage circumscribed by a mes sage once it has been sent Indeed this right is now reserved to the recipient who may already have modified it or even disposed of it In other words the ownership of pieces of heap hops from process to process following the flow of messages Copyless message passing combines two features
73. acts The proof sys tem discharges parts of the verification of programs on the verification of their contracts The marriage of these two techniques allows one to prove that programs are free from mem ory faults race conditions and message passing errors such as unspecified receptions and undelivered messages Moreover we show how the logic and contracts cooperate to prove the absence of memory leaks Third we give an implementation of our analysis Heap Hop iii that takes annotated programs as input and automatically checks the given specifications and deduces which of the properties above are enjoyed by the program Heap Hop requires pro grams to be annotated with pre and postconditions for each function loop invariants and the channel contracts that communications should obey iv Contents Abstract iii Remerciements ix Introduction 1 Table of notationS 5 2 La iia y Quem AO a a a a 8 1 Concurrency and Ownership 11 1 1 Concurrency and the heap 11 1 1 1 Concurrent programs 11 1 1 2 Race free programs 12 1153 Synchronisati nzs c aka Ge SAAR OR RE Oe dee RES 13 LTA Ownership choo hee ee EES Pe Sk ea RS 17 LLS M m fries La be up CO Dae vu web Ee ES 19 1 2 Message passing e n i0 pk ee a 20 1 2 1 Communication primitives 20 1 2 27 S XAMPI S LE loto ee ad adi 21 1 23 Design choices eri a baw Eo
74. aders writers While the producer consumer problem is easily solved using message passing because its solution essentially simulates message passing this is not the case for the readers writers problem In fact to implement a solution of the readers writers prob lem using message passing one essentially re implements locks The solution proposed 29 1 2 Message passing Consumer code Producer code while true while true x receive item f x produce_item send item e x do something with x here Figure 1 10 A solution to the producer consumer problem using message passing Reader code Writer code while true while true send read_request e y produce_item x receive value e send write_request e y receive write_ack e do something with x here Figure 1 11 A solution to the readers writers problem using message passing Figure 1 11 assumes that the endpoint e used in each instance of readers and writers is dif ferent each time All the peers of these endpoints are held by a central authority which takes care of granting reading and writing rights only when mutual exclusion is ensured We omit the code for this process Note that the code for just the readers and writers is still simpler than its locking counterpart but only because the mutual exclusion mechanism happens outside of it 30 CHAPTER 2 A Model of Copyless Message Passing This chapter describes t
75. aglini and Nobuko Yoshida Global progress in dynamically interleaved multiparty sessions In CONCUR volume 5201 of LNCS pages 418 433 2008 Cited on page 144 Josh Berdine Cristiano Calcagno and Peter W O Hearn Smallfoot Modular automatic assertion checking with separation logic In FMCO volume 4111 of LNCS pages 115 137 2005 Cited on pages 130 131 147 Bibliography BCOO5b BCY06 Bol06 Bor00 BP09 Bro07 Bur72 BZ83 CC77 CDOY06 CES 86 CFO5 CFI96 148 Josh Berdine Cristiano Calcagno and Peter W O Hearn Symbolic execution with separation logic In APLAS volume 3780 of LNCS pages 52 68 2005 Cited on pages 133 134 135 136 Richard Bornat Cristiano Calcagno and Hongseok Yang Variables as re source in separation logic Electr Notes Theor Comput Sci 155 247 276 2006 Cited on pages 65 67 72 Benedikt Bollig Formal Models of Communicating Systems Languages Au tomata and Monadic Second Order Logic Springer 2006 Cited on pages 45 51 Richard Bornat Proving pointer programs in hoare logic In MPC volume 1837 of Lecture Notes in Computer Science pages 102 126 2000 Cited on page 3 G rard Boudol and Gustavo Petri Relaxed memory models an operational approach In POPL pages 392 403 2009 Cited on page 13 Stephen Brookes A semantics for concurrent separation logic Theor Comput Sci 375 1 3 227 270 2007 Cited on
76. al the number of ways they have of misbehaving skyrockets Worse the errors they make may depend on subtle timing issues between the actions of each process This makes them hard to detect and reproduce using traditional debugging tools especially since merely trying to observe a problem may hide it away Formal methods have thus an important role to play in verifying concurrent programs Finally it is worth mentioning that designing the models that form the basis for formal verification is often a difficult task in itself This is particularly true in the concurrent setting where the effect of interactions has to be carefully taken into account In this thesis we are interested in the formalisation and formal verification of message passing programs Our goal is to define a realistic model of a particular class of such pro grams and to analyse some of their properties in a manner that is suitable to some level of automation Amongst the many properties that one may wish to establish for message passing programs we have chosen to focus on those which ensure that a program never goes wrong that is in safety properties Copyless message passing Parallel programs in all generality need means to synchronise and communicate with each other Message passing is a theoretically elegant tool to achieve this if a process wishes to communicate a value it sends it to another process if two processes should wait for each other before advancing furth
77. also specifies an arity n is message a n 6 A tag z with an arity of 0 has no parameters is sent using send z and is received in branches of the form receive z E p Heap Hop checks that arities are used consis tently by the program If some arities are not explicitly declared in the file Heap Hop infers 128 x v E E Exor E E E E E x E new x Bt E gt t E dispose E e f open C close E E send a E BE x Este x1 c switch receive r1 Tar P P if B p else p while B p f E MRE f E gt Xar a receive a E Chapter 7 Heap Hop expressions variable value arithmetic operations boolean expressions commands variable assignment memory allocation field lookup field mutation memory deallocation channel creation channel destruction send p receive branch programs atomic command switch receive sequential composition conditional loop function call parallel composition Figure 7 2 Syntax of the Hop programming language them from the program 7 1 2 Contracts The protocols of a program are described using contracts In the future Heap Hop may sup port more general dialogue systems to specify protocols Contracts are required to have at least one initial state and need not be deterministic positional or synchronising However these three properties are checked by Heap Hop which will issue appropriate warnings if
78. am p reduces to MsgError from a ceremonious state c but not to OwnError or ProtoError then either p is decorated by a faulty contract one that 120 Chapter 6 Open Behaviours and Soundness is not fault free or amp contains one Indeed the contract configurations of channels are all reachable in c and in the states resulting from the execution of p on c hence one of the contracts can reach an unspecified reception configuration Lemma 6 12 For all well formed open state c if p close o MsgError then either p c gt MsgError or p c gt OwnError Proof Straightforward Proved programs follow their specifications Finally let us show that the last part of the runtime validity definition holds for valid programs Lemma 6 13 For all well formed open state o if p o gt p o then either p a error with error LeakError OwnError ProtoError or there exists a State f such that close a o and p o gt y c Proof We proceed by case analysis on p Let a 6 k flat a f o Sc he k and o s h k Suppose that p o p o and p a 4 error We have to show that there exists c such that close o o and p o gt p c stack and heap commands straightforward In the case of new observe that we can pick the same location as in o because dom hy dom he open straightforward close the flattening of the resulting state flat c is equal
79. anguage which we hope this dissertation has shown to be useful concepts in the context of message passing program verification 146 ABSO01 AH90 AJ93 Alg 10 BAW10 BBLO9 BCC 07 BCD 08 BCOO5a Bibliography Aurore Annichini Ahmed Bouajjani and Mihaela Sighireanu TReX A tool for reachability analysis of complex systems In CAV volume 2102 of LNCS pages 368 372 2001 Cited on page 7 Sarita V Adve and Mark D Hill Weak ordering a new definition In ISCA pages 2 14 1990 Cited on page 13 Parosh Aziz Abdulla and Bengt Jonsson Verifying programs with unreliable channels In L CS pages 160 170 1993 Cited on page 54 Jade Alglave A Shared Memory Poetics PhD thesis Universit Paris 7 and INRIA 2010 Cited on page 13 Christian J Bell Andrew W Appel and David Walker Concurrent separa tion logic for pipelined parallelization In SAS volume 6337 of LNCS pages 151 166 2010 Cited on pages 7 98 Kshitij Bansal R mi Brochenin and tienne Lozes Beyond shapes Lists with ordered data In FOSSACS volume 5504 of LNCS pages 425 439 2009 Cited on page 69 Josh Berdine Cristiano Calcagno Byron Cook Dino Distefano Peter W O Hearn Thomas Wies and Hongseok Yang Shape analysis for composite data structures In CAV volume 4590 of LNCS pages 178 192 2007 Cited on page 68 Lorenzo Bettini Mario Coppo Loris D Antoni Marco De Luca Mariangi ola Dezani Cianc
80. anisms for connecting to the user and to the bank are different in one 90 Chapter 5 Proving Copyless Message Passing case the user initiates the connection while in the other the ATM does luser_connect Cu bank_init Chank wat X bank_connect gt The contract between the user and the ATM follows the structure of the program 2overdraft withdraw_u dispens ia Cuser_session E 1 E operation pee deposit_u balance_u fin u receipt This contract points out the fact that this ATM could be improved as noted by Honda et al to allow several operations in a row until the user quits The protocol between the ATM and the bank abides by the following contract withdraw C bank session i 7d deposit fin b balance lreceipt Both contracts are strikingly similar which reflects the fact that the ATM acts as a relay between the user and the bank The footprints associated to the messages that open and close communication channels in this example are as follows user_connect amp val gt Cuser_session 2 i Joank connect val gt Cbank_session 2 i fin u val gt Cuser session 2 end end val src Vin_b val gt Cpank session 2 end end val src 91 5 3 Restrictions of the proof system Since all the other messages convey mere values their associated footprint is emp All the contracts of thi
81. annels are associated to contracts Although its main purpose is to help us prove the soundness of our logic this second semantics also highlights the impact that contracts have on the verification of programs Indeed we connect this second semantics both to the first operational semantics of programs and to the semantics of contracts Secondly we provide a proof system for copyless message passing programs with con tracts based on separation logic The logic discharges parts of the verification of the program Introduction on the verification of its contracts thus realising the claim made by Singularity that con tracts should provide a clean separation of concerns between the different aspects of the verification of copyless message passing programs Our analysis can prove in particular that a program causes no memory fault or leak has no race condition and that channel communications are safe from both unspecified receptions and undelivered messages Thirdly we have developed a tool Heap Hop that takes annotated programs as input and automatically answers whether its specification is correct or not using our logic and whether it enjoys the properties mentioned above The logical fragment manipulated by Heap Hop makes the entailment problems between formulas decidable while being powerful enough to permit symbolic execution Our proof system was first presented in the APLAS conference VLCO9 with a different proof of soundness
82. anner Given a contract X Q qo E T we write init for go and finals for F 3 1 3 Semantics In the following and unless specified otherwise G is a communicating system E Mj M with M 2 B Q 40 7 and B 1 p A configuration of a system often written C specifies the current state of each machine of the system and the contents of the buffers Definition 3 10 System configuration Given a system where B p the set of con figurations of the system is T1 Qi x We distinguish three particular kinds of configurations the initial configuration final ones and stable ones where all buffers are empty We write for the empty word Definition 3 11 Initial configuration The initial configuration of the system is dise 25 Mons cesi 47 3 1 Communicating systems Definition 3 12 Final configuration A configuration q1 qn W1 Wwp is final if diia qa F Definition 3 13 Stable configuration A configuration qi qn w1 wp is stable if wi for all i A communicating system dictates how to go from one configuration to the other Definition 3 14 System transition relation Given a communicating system the tran sition relation e of 6 is defined as the union of the relations 56 for TE Uta Ti where T 91 Gn W1 Wm 6 qd qu WI Wh is defined as follows e if 7 is a send action jla then there is 1 n such that
83. annot prove termination it could prove leak freedom if contracts were richer For instance one could use arbitrary dialogue machines instead of contracts for specifying the communication protocols In this case the protocol followed by the program 140 Chapter 7 Heap Hop can be much more accurately described by the following system D NOR Y lack ack work lack ack 2 es EA work work Note that both endpoint of the channel follow the same protocol and not dual ones In particular the communications are not half duplex Although this dialogue system is not leak free itis deadlock free Using a similar method as with contracts one could prove that the load balancing program obeys this dialogue system and that as a result the program will not get stuck waiting for a communication Yet the program is also leak free and moving to general dialogue machines alone does not help in proving this To achieve this one would have to augment dialogue systems with counters Informally one would specify the communications using the following ex tended dialogue system D where transitions can be guarded by testing a counter k or k or incrementing it with k or decrementing it with k Iwork ack lwork ack 1 ket Q lack ke lack pi 9000 BR BN work work The final state now also specifies that k k 0 One can extend the definitions of Chapter 3 and show that is indeed leak free whenever the final configu
84. anslate properties of contracts into properties of the program and to define what the environment is allowed to do in particular it will only be able to produce ceremonious states We first define the contract configurations associated to a channel in a given open state Let c 0 k and flat c sy he ky The set of channels of o is the set of pairs e e such that at least one of e e belongs to dom k chans a e e mate ky e e Note that because at least one of the two endpoints of a channel of c must appear in the domain of k f the channels of c are all associated to a contract the roles of the endpoints are known and so is the control state of at least one of the two endpoints Notations Given an open state g such that flat o sp hy kp if k e e r q is defined then we write contract o for role a for r and control a for q Given an open buffer a a1 v1 01 an Un On We write word a for a1 an Definition 6 5 Contract configuration of a channel Let o be a well formed open state such that flat o sg hg kg and e e e chans o The set of contract configura tions cconf a e associated to e or to e is E dom ks gt q control kp us word k e word e e e dom ky q control k y e A ceremonious state is one in which in every set of contract configuration of every channel there is a configuration reachable by the
85. arallel decomposition lemma to p skip one obtains the soundness of the FRAME rule WEAKENING CONJUNCTION DISJUNCTION EXISTENTIAL Straightforward RENAMING We can prove by structural induction on the formulas that for all o and and for all variables x and y 6 4 amp o if and only if x gt y 7 d x y It can also be proved by a straightforward structural induction on the program that for all p p c error if and only if p x gt y a x y error and that p a c if and only if p x gt y o x gt y 0 x gt y These facts entail the soundness of the RENAMING rule 6 4 Properties of proved programs This section is dedicated to the consequences of the soundness theorem on proved programs we show that proved programs whose contracts are fault free enjoy runtime safety Theo rem 6 2 that is they do not reduce into any error in the closed semantics and that programs proved under an admissible footprint context and with leak free contracts enjoy leak free dom Theorem 6 3 Let us begin by defining how to obtain a closed state from an open one 6 4 1 From open states to closed states To transform an open state into a closed one one first needs to transform its open buffers into closed ones Given an open buffer o a1 v1 k1 an Un kn we write o for its canonical projection onto a closed buffer in Msgld x Val n a a1 v1 an Un This notion is easily extended to proje
86. are not they only hold if E and Ez can be evaluated on the current stack With our definition E1 E holds if both expressions evaluate to different values on the current stack and with the current values of logical variables e 99 We use as a wildcard for instance E is read as 3X E X To lighten formulas and following the variable as resources tradition BCY06 we write x1 xnlk for own x1 own xn Finally the set var of the program variables of a formula is defined as usual by structural induction on the formula Quantifications bind only logical variables and there are no binders for program variables in the syntax of assertions We sometimes write o o to mean that c i for all 2 67 4 1 Assertions true VX X X false true 1 V 9 201 D2 Di 25 2d1 V 2 Q Da 5 61 gt 2 02 gt 01 1IX pVWX 0 emp emp A emp E gt Eo E amp Ep true E Eo By E A E Esa F Es Figure 4 3 Shorthand formulas Examples Let us give a few examples of formulas and what they denote Formula Denotation x e 32 y e 52 two cell heap x gt 32 y gt 52 unsatisfiable the heap is made of one cell with conflicting values xk Ayt one cell heap x y x 32 x 32 unsatisfiable x cannot be present in the stacks on both sides of 4 1 5 Inductive predicates Finally we need a way of describing inductive structures in the heap
87. asons including the following ones the processes are executed on different machines the processes are executed on different processors of the same machine the processes are executed on different cores of the same processor the processes are executed on a single core together with a scheduler that decides of an interleaving of the instructions of each process any combination of the above In general processes execute independently for instance unrelated user applications on a desktop computer meaning that all the data they manipulate have manipulated in the past or will manipulate in the future live in disjoint areas of the memory Processes may also need to share or exchange data and this is of course when interesting things happen Inter process communications mostly happen via shared portions of states message passing or variations of one of these two paradigms for instance remote procedure calls akin to message passing We call resource a shared variable or portion of memory The rest of this section is devoted mainly to a survey of shared variable concurrency for heap manipulating programs This will be useful in the rest of the thesis to be able to com pare our analysis for message passing with existing ones for shared variable concurrency In the low level details of operating systems there may be some sharing even in this case for instance via dynamically linked shared libraries or system calls When
88. at most one process at a time can also be found in the very design of the Singularity OS HLO7 Each Singu larity process owns a portion of the state that is called local to the process and that can only be accessed by it or be given back to the operating system In particular local states cannot be shared between processes Memory locations that are destined to navigate between pro cesses are allocated in the exchange heap Its functioning is described as such in the paper Language support for fast and reliable message based communication in Singularity OS by F hndrich et al FAH 06 where Singularity channels are introduced Although all processes can hold pointers into the exchange heap every block of memory in the exchange heap is owned accessible by at most one process at any time during the execution of the system Note that it is possi ble for processes to have dangling pointers into the exchange heap pointers to blocks that the process does not own but the static verification will prevent the process from accessing memory through dangling references To make the static verification of the single owner property of blocks in the exchange heap tractable we actually enforce a stronger property namely that 18 Chapter 1 Concurrency and Ownership each block is owned by at most one thread at any time The fact that each block in the exchange heap is accessible by a single thread at any time also provides a useful mutual exclu
89. ation either the send should not be a a message or the switch receive should include another case for this message Asitis it corresponds to what C c and Finkel call an unspecified reception in the paper Verification of programs with half duplex communication CF05 An unspecified reception configuration corresponds to a configuration in which a machine is definitively blocked by its inability to receive the head messages present in its input channels This kind of deadlock is also considered as disastrous by the session type community a key result in this area is that well typed programs do not exhibit this error THK94 Finally in Sing that inspired our own language a switch receive would fault in this case FAH 06 If the message at the head of the buffer is not the expected message or the channel is closed by the peer the receive fails Interestingly enough the solution first proposed by Singularity to eliminate these dead locks was unsound as shown by Stengel and Bultan SB09 who corrected it independently from our own work which came to the same conclusion and solution presented in Chap ter 3 Leak freedom When a communication channel is closed nothing guarantees that its buffers are empty As a result the following program leaks a memory cell that could have been retrieved from the channel had it not been closed abruptly e f open x new send cell e x x 0 close e f Without ga
90. can also define predicates that describe the data along with the shape of a dynamic 68 Chapter 4 Concurrent Separation Logics structure BBLO9 Rey02 for instance to prove total correctness of a sorting program Finding more elegant and systematic ways to define inductive predicates with or without data is challenging and a concern orthogonal to this thesis and more akin to the domain of shape analysis 4 2 Proof system 4 2 1 An extension of Floyd Hoare logic In addition to the assertion language separation logic is an extension of Floyd Hoare logic or simply Hoare logic a logic used to specify and prove programs Hoa69 Flo67 The term separation logic usually refers both to the assertion language and to the proof sys tem that uses it Floyd Hoare logic statements are called Hoare triples and have the form p v where and v are formulas in our case separation logic formulas and p a program A Hoare triple o p v has the following informal semantic reading in the partial correctness setting For any state c satisfying if p o skip 0 then o satisfies 4 These triples are proved formally by constructing a derivation tree from a set of rules There is typically one such rule per programming construct and logical rules to rewrite the formulas of a triple Separation logic is tuned towards a fault avoiding interpretation of triples The goal is to obtain the following soundness statement
91. cation of memory manipulating programs for years before it found an elegant solution with separation logic 19 1 2 Message passing most of previous efforts made the non aliasing constraints explicit resulting in a blow up of the formulas that were used as specifications compared to their variable only counterparts 1 2 Message passing When two processes wish to communicate via asynchronous message passing they must share a buffer One process may then send or queue messages on the buffer that the other one can receive or dequeue Our communication model is heavily inspired from the one of the Singularity OS FAH 06 communication buffers are grouped pairwise into bi directional asynchronous channels Access to a channel is performed via two endpoints on which one may both send to a buffer and receive from the other achieving bi directional communication A similar model of communication is the IPC inter process communica tion socket model found in many operating systems In our setting the communications are moreover copyless sending a message does not result in copying its contents over the channel but rather in sending a mere pointer to the location of the message s data in mem ory This assumes a shared memory between processes which can be achieved for instance if they are run on the same machine We first introduce informally the communication primitives of our message passing lan guage We then discuss the design ch
92. cc r q T for the state q such that q 3 q is a valid transition of the contract in the role r that is either r 1 and q 7 q T orr 2 and q 7 q T There is at most one such q since all the contracts we consider are deterministic Proof system Let us present our proof system for the HirMP language The rules of separation logic presented in the previous chapter Figures 4 4 4 5 and 4 6 are modified by uniformly adding r to the left of each Hoare triple The rules for channel creation and destruction and for communications are given in Figure 5 1 We write y E E Ez E4 for y src E dst lt Ez rlE3 val E4 Unfortunately the variables as resource model without permissions forces us to perform some squirming around to read the same variable in two different parts of a formula sepa rated by a separating conjunction each time this situation arises we have to first store the value of the incriminated variable into a logical variable and use the latter to refer to it This is for the greater good as it will lighten the notations of our upcoming proof of soundness For instance the formula x y y xis inconsistent a variable may not appear in both the domains of disjoint stacks and one should rather write x XAy Y MX gt Y Y o X to say that x and y point to each other Let us review the five new rules and how they ensure that both ownership and the con tracts are respected OPEN The rule is
93. cing it in the example above that is moving send cell e x one line earlier could result in a fault as the cell pointed to by x is not owned by this thread after it has been sent 23 1 2 Message passing put list e x get list f local t local x ee while x 0 t x tail ee 0 send cell e x while ee 0 x t switch receive send fin e e x receive cell f dispose x ee receive fin f 3 close ee f Figure 1 9 Cell by cell list passing and hence may have been deallocated in between the two instructions The linked list can also be sent in one single message as once a process knows where the head of the list is all the other cells become reachable The resulting program would then be similar to the one of Figure 1 8 This is another example where the meaning attached to messages of a program depends on what the program does The same message may indicate a transfer of ownership of a single memory cell or of a whole linked list 1 2 3 Design choices Asynchronous or synchronous Communications may be either asynchronous or syn chronous in the latter case the sending of a message must wait until the other party is ready to receive and this exchange acts as a synchronisation point between the two whereas in the case of asynchronous message passing the sending operation can return immediately In this case the maximal size of what can be stored in the channel matters beca
94. cket org jvillard heap hop http mercurial selenic com 138 Chapter 7 Heap Hop Figures Let us now present some executive compliant key figures about Heap Hop s code base All figures include comment lines Heap Hop in its current form represents 5018 lines of OCamL code and ships with 1273 lines of original examples The Smallfoot code base while retaining its essence has undergone much changes omitting examples 925 lines were removed and 2316 lines were added including lines that were modified 7 4 2 Case studies Examples presented so far Most of the examples presented in this manuscript includ ing for instance the cell by cell list sending program and the modelling of an ATM are included in the examples subdirectory of the Heap Hop distribution Let us present an other example that ships with Heap Hop that introduces what we believe to be an interesting problem the load balancing problem for binary trees This problem is only partially solved by Heap Hop Load balancing What we call the load balancing problem for two threads is this given a binary tree whose nodes represent some tasks which we assume to be of equal cost in terms of computing power one tries to distribute these tasks to two threads running in parallel such that both threads end up treating an approximately equal amount of tasks The tree is not supposed to be balanced and its shape is not known in advance so the algorithm has to distribute the tasks
95. ct an open endpoint heap k onto a closed one 7 k with the obvious lifting of 7 and open states onto closed ones overloading 7 once more State gt State 1 s h k k e s ho n k This projection is unfortunately too coarse for our needs as much of the state may be buried inside the open buffers Instead we define the closed state close a corresponding to by the projection above applied to the flattening of c 118 Chapter 6 Open Behaviours and Soundness Definition 6 9 Closed state of an open state The closed state close a of an opened state o k such that flat a sp hy ky is defined as close a ss hg m k The closed state associated to a well formed open state is also well formed Lemma 6 8 For all e State close o is well formed as a closed state Proof The constraint Channel follows from the OChannel condition on c and Ir reflexive Involutive and Injective from the well formedness of the local part of flat c 6 4 2 Runtime validity Let us show that programs proved under fault free contracts do not reduce into an error in the closed semantics More precisely let us show that such programs are runtime valid Definition 6 10 Runtime validity We say that a triple o p v is runtime valid and write ler d p v iffor all i and c there exists a such that a i close o 0 and e p o 4 OwnError and e p o MsgError and e f p 0 skip o
96. current word written on the tape and the position of the head We assume without loss of generality that every Turing machine starts 50 Chapter 3 Dialogue systems on an empty tape that the right end of every configuration is marked by O 0 that the machine never reaches the final control state q until the very end and that hen this hap pens the tape is again empty The initial and final states are thus respectively O qo O 0 and 0 q 0 0 The encoding of a Turing machine M using a dialogue system intuitively uses the buffers to store the current configuration One of the machines then simulates the transitions of W while the other ones acts as a mere copycat This allows the simulating machine to cycle freely through the configuration to find the position of the head at each transition perform the transition locally as this only requires the memory of the immediate surroundings of the head and cycle again to repeat this process Let M iu Qu Tm O qo qr be a Turing machine The dialogue system that will model M is F Msim Meat as defined below Intuitively using r to denote an element of Q u 0 a configuration will be coded by the system s global configuration qsim cat W1 W2 where 01 wo is a rotation of Con that is there exists a 7 such that Con a1 r1
97. d before which were all about safety properties something bad should never happen This thesis will only be about safety properties 1 1 4 Ownership One way to distinguish between racy and race free programs is to see racy programs as those violating the following ownership hypothesis as formulated by O Hearn in the paper Resources concurrency and local reasoning O H07 Ownership Hypothesis A code fragment can access only those portions of state that it owns 17 1 1 Concurrency and the heap In this hypothesis a portion of state contains variables and memory locations and own means either that the program has shared access to it if it only ever reads from it or exclusive access if it writes to it It should not be confused with the portion of state reachable from the program variables it can be a mere fraction of it or even contain unreachable locations which is usually a sign that the program has a memory leak it is in charge of a part of the memory that it is unable to access One can imagine each variable and memory location to be decorated with the identifier of the process or processes that owns it and that a process accessing a cell that it does not own provokes a runtime error If all processes abide by the ownership hypothesis they will never run into such an error Of course this decoration should only be to paraphrase O Hearn in the eye of the asserter in reality it has no operational
98. different contexts for instance an endpoint cannot be freed using the dispose command and a cell cannot be used to send messages Thus a cell can point to any value but an endpoint points to its peer and to its buffer The latter represents the pending messages waiting to be received on this endpoint it is a word of pairs a v where a is a message identifier and v a value Equivalently there could be only one heap that associates one of two sorts to each allocated locations similarly to the work of Gotsman et al on storable locks GBC 07 where the different sorts that coexist in the same one heap are one for locks and one for regular memory cells The stack follows the same idiom variables must be owned by the program to be acces sible without a risk of a race condition If c s h k e dom k and k e a e is called the peer or mate of e and is denoted by mate k e or mate o e and a is called the buffer of e and is denoted by buffer k e or buffer o e Each state s h k should be well formed in the sense that the following axioms hold Ve e dom k mate k e e dom k Channel Ve e dom k mate k e e Irreflexive Ve dom k mate k mate k e Involutive The first condition ensures that if the domain of the endpoint heap contains one endpoint of a channel then it also contains its peer As we will see in Section 2 2 this is required 34 Chapter 2 A Model of Copyless Message Passing
99. ditions are glued to gether to form the post condition of the parallel composition Had we not considered stacks as partial functions there would be numerous side conditions attached to this rule Bro07 BCY06 CHOICE and STAR Standard LocaL The rule allocates a new variable z which is used to prove p The variable must be tracked throughout the proof of p and still be present at the end when itis disposed FRAME See earlier discussion WEAKENING This is a standard Floyd Hoare rule whose soundness follows directly from the definition of what a valid Hoare triple is CONJUNCTION DISJUNCTION EXISTENTIAL and RENAMING Standard We give below the soundness of separation logic adapted to our setting We will not prove it here as it is not the focus of this thesis For any program p Hip if the triple o p v is provable then for any state c and any interpretation i if o i then p o error and if p o skip c then o iE Y 4 2 4 Conditional critical regions As discussed in Chapter 2 there exist many programming language tools to allow the dif ferent components of a program to synchronise Historically the first mechanism that was 72 Chapter 4 Concurrent Separation Logics RESOURCE Tr toh pty resource r in p v CCR Te b AB pid x T r r 9 with r when B p 9 Figure 4 7 Proof rules for conditional critical regions included in separation logic was conditional critical
100. e send rel e 1 The authority for a given lock is given by the following code assuming two threads that send locking requests on e and e while true switch receive 4 receive acq e1 send ack el receive rel el receive acq e2 send ack e2 receive rel e2 More robust solutions that could handle an unbounded number of locks and threads can be programmed if we extend the switch receive construct to wait on a linked list of endpoints This extension exists for instance in Singularity 1 2 6 Further examples of message passing To conclude this chapter let us show how message passing can be used to solve the producer consumer and the readers writers problems Producer consumer As our setting embeds the concept of a buffer in the synchronisa tion primitives themselves the producer consumer problem has a very easy solution pre sented Figure 1 10 Contrast it with the same solution using CCR Figure 1 3 page 17 The message passing solution assumes a channel e between the producer and the consumer processes over which messages of type item may be exchanged Note that the communica tion is uni directional from the producer to the consumer This solution is race free fault free and deadlock free A leak free full fledged version would require an extra message to signify the end of production The communication buffer is unbounded but as usual could be bounded by adding acknowledgement messages Re
101. e which must match the role of the endpoint sending them The following lemma shows that this is indeed sufficient to ensure admissibility It also implies admissibility of footprints that contain no endpoints Lemma 5 3 Sufficient admissibility condition Any footprint context I such that there is r 0 1 such that for all y T E ya X true gt yA X gt 7 true n rl r is admissible Proof Suppose that I is not admissible and let us reuse the notations of Definition 5 1 There is 9 s h k such that s h k E jer Yo Ei Es ri vi and for all i I dom k and k e 6i 3 ri Suppose that J 1 n In particular there are 1 s1 h1 k1 E Yo ene T1 Un n Sn An kn Yon En Ens Tn Un We can assume without loss of generality that none of the endpoint heaps ky kn is empty if one of them kj is then 9 6 and Gcr 45 Y Ei Tj Uj also form a witness that I is not admissible Let us show that the role of all the sending endpoints of the messages whose footprints form the proof of non admissibility of I are of the same role r Because all the endpoint heaps k are non empty it is the case that for allie J GE Yo Eis Ej ri Vi A X gt true Hence by application of the hypothesis of the lemma Gi E Yb Ei e Ti Vi A X gt 7 trueari r Let us now show that supposing that I is not admissible is ab
102. e Eng 23 5 279 295 1997 Cited on page 7 Maurice Herlihy and Nir Shavit The Art of Multiprocessor Programming Morgan Kaufmann Pub 2008 Cited on pages 13 14 Kohei Honda Vasco Thudichum Vasconcelos and Makoto Kubo Language primitives and type discipline for structured communication based program ming In ESOP volume 1381 of LNCS pages 122 138 1998 Cited on page 6 Kohei Honda Nobuko Yoshida and Marco Carbone Multiparty asynchronous session types In POPL pages 273 284 2008 Cited on pages 6 63 144 Raymond Hu Nobuko Yoshida and Kohei Honda Session based distributed programming in Java In ECOOP volume 5142 of LNCS pages 516 541 2008 Cited on pages 7 26 Samin S Ishtiaq and Peter W O Hearn Bl as an assertion language for mutable data structures In POPL pages 14 26 2001 Cited on page 3 Cliff B Jones Specification and design of parallel programs In IFIP Congress pages 321 332 1983 Cited on page 7 Leslie Lamport How to make a multiprocessor computer that correctly exe cutes multiprocess programs IEEE Trans Computers 28 9 690 691 1979 Cited on page 13 K Rustan M Leino and Peter M ller A basis for verifying multi threaded programs In ESOP volume 5502 of Lecture Notes in Computer Science pages 378 393 2009 Cited on page 7 K Rustan M Leino Peter M ller and Jan Smans Deadlock free channels and locks In ESOP volume 6012 of LNCS pages 407 426 2010 Cited on pages 7
103. e channel and instead send a mere pointer to the location of the message s contents in memory When a process receives such a pointer it gains the ability to access Introduction the contents of the message In effect the sender and the recipient of a message located in memory are sharing this piece of memory and one has to be careful to avoid some of the drawbacks of shared memory communications such as race conditions The communica tions of SinGf are in fact an example of copyless message passing which constitute the main interest of this thesis In this thesis we will explore one means of ensuring statically and automatically to some extent that programs communicating via copyless message passing do not encounter memory faults by requiring that a process sending a message loses its access right over its contents this right is transferred to the receiving process This condition is sufficient to ensure the absence of race conditions between processes Moreover we will insist on communications being ruled by channel contracts As we will see this reduces the check ing of certain communication errors in programs to an analysis of their channel contracts which are much easier to reason about Our programming language features asynchronous bidirectional FIFO first in first out channels each made of two endpoints endpoints are themselves exchangeable over channels in fact they are allocated on the heap like regular memory cells
104. e current local portion of state This operation is possible because we always assume the states we consider to be well formed a property we will see is preserved by the reduction rules in Lemma 6 2 hence flattable so dq is guaranteed to be compatible with s h k The message is then removed from the queue the value stored into the appropriate variable x and the control state of the endpoint is updated If no such successor exists ProtoError is raised If an unexpected reception occurs MsgError is raised Finally and similarly to the logical treatment of guarded external choice not taking into account all the possible messages that can be received according to its contract is a fault and the program reduces to ProtoError Programming constructs The semantics of the remaining programming constructs is given in Figure 6 6 The rules are identical to the closed semantics ones with two excep tions First the detection of races uses a different finer tuned as will see in Lemma 6 10 function based on the local part of the state which is closer to what is required by the PAR ALLEL rule of the proof system the predicate norace p1 po 7 is false if it is impossible to partition c into two substates with disjoint local parts on which each program can safely make a step Formally norace p1 p2 c holds if and only if there exist well formed open states c and such that c ec c and P1 01 OwnError amp p2 09 OwnError
105. e of the form p g gt p o or p o gt error with error LeakError MsgError OwnError ProtoError The errors MsgError and OwnError have the same intuitive meanings as in Sec tion 2 2 2 they represent respectively reception and ownership runtime errors A program raises LeakError if it closes a channel with undelivered messages thus creating a poten tial leak and ProtoError if it does not act according to one of its contracts either by performing an unauthorised action on a channel or because of a switch receive that is not exhaustive with respect to one of the contracts involved Stack and heap commands For the stack and heap commands the open semantics is derived straightforwardly from the closed one taking the local portion of the state as the main stack and heap The rules are shown in Figures 6 1 and 6 2 The semantics of new is the only one that requires special attention namely to avoid reusing a location that may be hidden in the contents of a queue which could result in an ill formed state 104 Chapter 6 Open Behaviours and Soundness B s true skip 0 gt skip 0 assume D s h k k gt skip s h k k x dom s E v x E s h k k gt skip s v h k k Figure 6 1 Operational semantics of stack commands flat s h k k sp hy ky x dom s le Cell dom hy v Val x new s h k k gt sk
106. e other one being symmetric Since is deterministic there is only one outgoing transition from q with label a hence there is only one transition from q with label a in the dual machine Hence both machines made the step to the same next state and q1 qo Lemma 3 4 Half duplex contracts A contract that is both deterministic and positional is half duplex Proof Let 3 Q qo F T be a deterministic and positional contract Suppose that is not half duplex By Lemma 3 2 there is a stable configuration C q1 42 u 1 accessible by a 1 bounded run qo 90 1 11 S qi 92 4 such that q1 a q1 T and q2 b q5 T hence qo b q5 T for some a b qi q5 By Lemma 3 3 q1 q2 hence there is in fact both a sending and a receiving transition from q in thus q is not positional which contradicts our hypothesis that is The converse is not true in general there are half duplex contracts that are neither deter ministic nor positional However it becomes true for deterministic trimmed contracts Definition 3 22 Trimmed contract A contract X Q qo F T is trimmed if ev ery control state is reachable from qo in the oriented graph Q T formed by the contract s states and transitions where T g q 37 q 7 0 ET 55 3 3 Contracts A non trimmed contract is one in which there are control states that are disconnected from
107. e the message has been fully sent In this case there is usually also a primitive to wait for the asynchronous send to finish In our setting sends are atomic in the sense that they return only once the message has been put in the receive buffer of its recipient Recipients of messages When sending messages one has to specify who the recipient of the message is This can be done either explicitly by naming the recipient in which case the name of the channel is implicit for instance by its process identifier as it can be done in MPI or implicitly by naming the channel instead We support the latter form with our channel model sending and receiving are performed on any of the two endpoints of a channel irrespective of whom they belong to Message tags and branching receives When a channel may carry messages of differ ent sorts one is usually faced with having to take different actions depending on the kind of message that is present at the head of the buffer One means of discrimination between such messages is to associate tags to each of them that unambiguously determine their type A language construct may then be used to discriminate messages according to their tags and take different actions for different tags In addition to our own setting this solution has been chosen by Singularity session types and the ERLANG programming language to name a few We have adopted the switch receive construct from Singularity One to one one t
108. em a real leak in the sense that the program has no means right or wrong to access them The footprint contexts ep Yep and ep Yop above are not admissible Let us show this for yep We take A ep 1 5 ep 2 Consider the following state 2 2 1 1 q E2 ei Es 1 q This state satisfies the combined footprints of the two messages OF Seelen Eas 0 85 Ven ers E2 0 2 As 6 owns the recipient endpoints 2 and of the two messages the footprint of ep is not admissible 95 5 3 Restrictions of the proof system Sufficient syntactic conditions Fortunately there are admissible footprint contexts For instance every footprint that cannot allow ownership of one or several endpoints is trivially admissible as is any set of such footprints However a context with the footprint of the fin message that we have used in our examples so far is not as it can be used to send both sides of a channel on themselves e f ikes Xaf Y X e Y r q Y gt X 67 7 send fin e e send fin f f e f i emp Fortunately there is an easy fix one can specify which side of the channel is to be sent within the footprint For instance allowing only the first endpoint to be sent can be achieved by taking Yin val gt dst 1 q or y val gt 1 q val src A broader solution consists in allowing to send endpoints of only a certain rol
109. en descending into the current tree Its annotations have been checked by Heap Hop as has been the full program included in the Heap Hop distribution The contract C that the program is proved to follow is the one that allows any sequence of messages work and ack on the channel Since Heap Hop does not yet support arithmetic the code in the distribution includes additional variables and code to handle the values of the counter i by predicate abstraction 139 7 4 Distribution message work tree val message ack emp dispose left e el gt C s pr _f f local 1 r t i is_waiting i 1 is_waiting 0 t 0 while i 0 fel gt C s pr _f if i 0 then emp else if is_waiting 0 then tree t else emp if is_waiting 0 while t NULL el gt C s pr _f tree t t 1 t gt 1 r t gt r send work e r i i 1 dispose t t 1 send ack e is_waiting 1 else switch receive t receive work e is_waiting 0 receive ack e i i 1 el gt C s pr _f Figure 7 4 Left thread for the load balancing binary tree disposal Iwork 2 lack work O ack Interesting questions about this piece of code include whether it terminates whether it deadlocks and whether it is leak free However Heap Hop cannot establish any of these properties It only manages to prove that the program is safe with respect to memory man agement Although Heap Hop c
110. ent we prove the soundness of our logic directly from a refined version of the operational semantics of Chapter 2 see Chapter 6 instead of the denotational se mantics provided by the abstract separation logic framework Thus we will not state the generic soundness result of abstract separation logic in this thesis as it would require more definitions and instead refer the interested reader to the original publication on abstract separation logic COY07 For our exposition it suffices to know that such a result exists Acoarse soundness result Since our proof system can benefit from the generic abstract separation logic soundness result let us give examples of the issues that a semantics derived 97 5 3 Restrictions of the proof system solely from our proof system would meet a more detailed account of which can be found in the original paper VLCO9 Let us give three example programs on which the semantics directly derived from the proof rules via abstract separation logic would be too coarse unlike the semantics we will develop in the next section 1 Receives may happen before the corresponding sending operation has happened In deed nothing in the proof rules prevents it nor is it prevented by the interleaving of traces and these are the only things taken into account to build the semantics of programs in abstract separation logic For instance given a freshly opened chan nel e f over which one may communicate the message
111. epend on properties of the communicating system but rather on those of the message footprints as we are just about to see 5 3 4 Cycles of ownership leaks Our proof system has a defect some memory leaks can go unnoticed by the rules when a message footprint holds permission on the recipient endpoint or more generally when the queues of a set of endpoints can contain a set of messages whose footprints when put together hold permission on all the peers of the endpoints of this set in other words when the footprints of these messages all contain the endpoints on which they have to be received This makes it impossible according to the logic for a program to access these endpoints and receive theses messages In other words the right to receive these messages is held by the messages themselves leading to an inextricable situation This problem is very similar in nature to the one encountered by Gotsman ef al with their proof system for storable locks GBC 07 Let us give some intuitions on the source of the issue For instance if yep emp Aval gt then the following program proof can be derived given a system that allows the sending of ep e f lr emp e f open eefire X Af Y A X o Yi q Y gt X v q send ep e f e flker r q In this example there is no ownership abiding way of closing the channel e since the ownership of the endpoint pointed to by f has been
112. er they may exchange messages and wait for corresponding acknowledgements The relative simplicity of the message passing paradigm while helping in writing concep tually simpler code usually comes with a cost in efficiency as this programming paradigm is quite remote from the inner operations of a machine This may explain why more basic primitives like spin locks semaphores or even memory barriers have often been favoured in programming languages although they are arguably more error prone than message pass ing for the programmer However message passing can also be an efficient programming paradigm as has been demonstrated by Singularity Singularity HLO7 is a research project and an operating system written from the premise that one may replace hardware memory protection mecha nisms by systematic static analysis of programs source code on the one hand and dynamic checking at runtime on the other hand which together ensure strict isolation between pro cesses Indeed Singularity can safely run processes sharing a single address space without hardware memory protection Executable programs are compiled from the SinG program ming language derived from Cf which supports an efficient form of message passing prim itives described below In SiNGf the contents of messages reside in a portion of the memory that is shared by all the processes Thanks to this a process wishing to send a message can avoid copying its contents over th
113. ers of endpoints owned by the program We claim that giving a more precise account of interferences is possible but that it would needlessly complicate the presentation since this over approximation is enough to prove the soundness of our logic Let us first make an observation about the behaviour of interferences on the substates of an open state which follows from the following lemma on ceremonious states Lemma 6 3 For all 6 e State and k e EHeap if 6 e 6 k e State then 0 k e Stateft Proof Removing pieces of the local state merely removes constraints on the resulting open state Lemma 6 4 For all pairs of compatible open states d a such that o e Statef if 1 01 903 gt 0 then there are o a such that o e o5 o and D OT Ey Ta gt 095 Proof Leto 61 k and 0 02 k4 According to the hypotheses there is k such that 01 02 k U ky gt 01 ed2 k k 113 6 3 Soundness By definition of interferences 61 e 62 k e Statef hence by Lemma 6 3 61 k Statef so a gt 61 k and similarly for 74 which concludes the proof We can now state the locality and parallel decomposition lemmas which are crucial in gredients of the proof of soundness of the next subsection Lemma 6 5 Locality For all program p and open states a and such that o4 0 ctt and c e g State 1 if p 0 ed error then p c
114. es sage corresponds to a transfer of ownership Thus we attach to each message a formula of our separation logic called its footprint Different messages can be associated with differ ent footprints we attach the same footprint to messages of the same tag This is a natural choice as the same tag is usually used for messages with the same meaning A footprint can mention four parameters in the form of special free logical variables src dst rl and val When a message is sent the proof system will check that the footprint holds for a particular instantiation of these variables src is instantiated by the source endpoint dst by its peer the destination endpoint rl by the role of the sending endpoint and val by the value of the message When it is received the variable that the value of the message is assigned to becomes equal to the val parameter and dst and src are replaced according to the location of the receiving endpoint and its peer respectively This form of reasoning is justified by the fact that the values denoted by these parameters are assured to remain constant between the time when a message is sent and the time when it is received For example the footprint for a message containing the location of an allocated cell like in the example of Figure 1 6 page 22 can be ce val gt Similarly sending an endpoint over itself like in the example of Figure 1 8 page 23 can be expressed by the footprint Yin val gt
115. es are made distinct from the original source and are released publicly and under the same license Heap Hop inherits this license from Smallfoot Contents of the distribution Heap Hop s release contains the source code of the tool written in OCAML with a Makefile to compile it auto matically a battery of examples e a succinct user s manual e an emacs major mode to help editing examples and running Heap Hop on them The emacs major mode is an extension to the emacs text editor that includes syntax highlighting for the Hor language Although still under active development Heap Hop is considered as stable by its authors and a public official version numbered 1 0 has been released Unstable versions with more features are also available publicly for testing purposes Website Heap Hop s official website at the time of this writing is located at http www lsv ens cachan fr Software heaph hop This contains the tarball distri bution an online documentation a summary of the case studies and other resources such as scientific papers associated to Heap Hop Heap Hop is also hosted on the bitbucket website to benefit from a dedicated infrastruc ture that provides a mailing list a bug tracker and an online Mercurial a free distributed source control management tool repository which allows anyone to download the latest version and submit patches to the code http doc trolltech com 3 0 license html http bitbu
116. es not fault on message receptions and does not close channels with undelivered messages 5 1 Proof system 5 1 1 Session states Let us introduce session states which will be the models of our logic The memory model of separation logic is augmented with an endpoint heap Instead of attaching words of message tags and values to endpoints like in Chapter 2 we abstract away from the contents of the buffers and attach a contract and a control state to each endpoint More precisely a channel is associated to a contract and each of its endpoints is associated to one of the two roles 1 or 2 in the dialogue system corresponding to the contract and a current control state This gives rise to concise predicates to describe the states of endpoints and as we will see in the next chapter allows one to prove that programs respect their protocols directly into TI 5 1 Proof system the logic The logical states or session states are elements amp s h k of State State Stack x Heap x Session Stack Var fin Val Heap Cell fi Val det x Role x Control Session Endpoint fa Endpoint x Ctt In the definition above Control denotes the set of control states Role 1 2 and Ctt denotes the set of deterministic contracts Forbidding non deterministic contracts simplifies the presentation non deterministic contracts would require the logic to keep track of a set of possible control states for each endpoint instead of a s
117. essor Programming by Herlihy and Shavit HS08 provides insights on the subject Vafeiadis describes how to formally prove some of them in his thesis Vaf07 Race free programs On the other hand race free programs programs without race con ditions have several advantages that make them attractive for programmers and easier to verify In particular as Reynolds points out Rey04 their semantics is grainless one does not have to take the precise atomicity of primitive commands into account to give a semantics to race free programs and an interleaving semantics suffices to account for con currency Moreover race freedom allows one to elude the details of the memory model as it restores sequential consistency the fact that only those outcomes obtained by an inter leaving of the executions of the processes are observed Lam79 on weak architectures 1 1 3 Synchronisation If one wants to eliminate race conditions one has to regulate access to resources For in stance for the program of Figure 1 1 one has to protect the increment of x so as to prevent interferences from other threads In other words one has to ensure mutual exclusion be tween the accesses to x no two threads may be accessing x at the same time when one of them is writing to it To this end one usually uses either locks or conditional critical regions Conditional critical regions Conditional critical regions CCR or monitors or Hoare monitors are pieces of code
118. esting theoretical challenges lie is the verification of such protocols Indeed our syntactic restrictions would no longer guarantee the desired proper ties on protocols Furthermore half duplex machines with counters do not have many good decidability properties as counter machines with at least two counters can simulate Turing machines New techniques would thus have to be developed Another possible extension to the expressivity of the verification is the addition of pa rameters to footprints in the following sense Suppose that one wishes to transfer a linked list over a channel but that instead of disposing of its nodes one by one as in the example shown previously one wishes to reconstruct the list cell by cell As itis we could not find a proof of such a program with our proof system because the footprints of messages have no means of mentioning the value that will carry the next message or the value that was carried by the previous one One possible solution for this example would be to add a parameter X to the footprint of the cell message which becomes allowed to mention both X and the next value X of X Ye emp A Val gt X a Val X The contract remains unchanged but if there are other messages between two cell messages they may carry the previous value of X onward For instance if each cell message is followed by an ack message the footprint of the acknowledgement message could be Yack emp A X X The proof system w
119. execu tion of p hold on c otherwise the command faults which also satisfies the lemma and that the execution results in o1 Because of the precision assumption on message footprints the session state amp chosen in c must be the same as the one from the execution on g It suffices to take 95 69 k k e a v 6a to have g 05 G Note that this reasoning would be invalidated by an imprecise footprint y for a in that case if we pick c to be the piece of state whose local part is the session state a 114 Chapter 6 Open Behaviours and Soundness chosen by the reduction of p on c to be sent away and if c contains another possible candidate 6 satisfying ya then the semantics could chose to send 6 starting from and the resulting state could not be connected back to g in particular it would contain Gq in its local part whereas a does not The case of receive is similar The requirement of having precise footprints does not impact the reasoning for this command since the piece of state to be received is already determined by the contents of the buffer If the step was an interference then the property to prove corresponds to Lemma 6 4 Lemma 6 6 Parallel decomposition For all pair of programs pi po for all state c and for all o Gy such that o e 0 1 ifpi pa a error then p1 0 error or p2 0 error 2 ifpil pa 2 p ps a then p1 0
120. eyond it in some others Below is a list of the discrepancies between the theory and the practise of our logic at the assertion level non deterministic contracts are supported hence the logic keeps track of sets of con trol states instead of just one control state as mentioned in Section 5 3 1 130 Chapter 7 Heap Hop the tool logic does not treat variables as resources hence the absence of own state ments the syntax of the logic is restricted so that implication between two formulas of this fragment is decidable see Section 7 2 which is not the case for the logic of Chap ter 5 Moreover disjunctions are restricted to case analyses so that formulas of this fragment are always precise the contents of cells and endpoints is addressed through a record notation endpoints do not use a separate predicate to distinguish them from regular cells In stead a special read only field ep set to 1 for endpoints and 0 for regular cells is used by Heap Hop to distinguish between the two possible types Endpoint related infor mation the peer contract role and set of control states of an endpoint is recorded in the fields pr cid rl and st corresponding respectively to the peer contract iden tifier role and control state of an endpoint These fields cannot be modified directly by programs only via the communication primitives of Hor 7 2 Internals 7 2 1 Verification condition The first phase of the processing of functio
121. f cell open send cell e cell x send ep e f cell Chapter 1 Concurrency and Ownership main 1 local x o f x new e f open put_cell_indirect e x get_cell_indirect f close e f get_cell_indirect f ideal y ff ff receive ep f y receive cell ff dispose y Figure 1 7 Indirect cell passing through a secondary channel put_cell2 e x main send cell e x local x e f send fin e e x new e f open get_cell2 f put_cell2 e x get_cell2 f local y ee y receive cell f ee receive fin f close ee f Figure 1 8 Cell and endpoint passing for the program of Figure 1 7 to avoid the memory leak spotted above Let us give a final version of the program that sends a whole linked list starting at x cell by cell through the channel in Figure 1 9 The receiving process get list cannot know anymore when the f in message will arrive so we use the switch receive construct between the two possible messages cell and fin which will select the appropriate branch depending on which one is available in the buffer The main function is as in Figure 1 8 We write x for the dereferencement of the pointer contained in x In this example we ignore the data that may be contained in the list hence each node of the list simply points to its successor in the list A particularity of the copyless message passing setting is that sending x before derefer en
122. for contracts in general and that they can be proved to always hold for Singularity contracts We will later use contracts as helpers to prove message passing programs in Chapter 5 and we will formally connect the properties of contracts to those of the programs that abide by them in Chapter 6 We begin by a general presentation of communicating finite state machines 43 3 1 Communicating systems EDE Figure 3 1 Relationships between dialogue systems DS half duplex dialogue systems HD contracts Ctt and Singularity contracts S 1 a 1 b Gl a Xm 2la 21b a ax l a a 1 b a 2 a as 27b b Figure 3 2 A pair of communicating machines 3 1 Communicating systems 3 1 1 Definition Figure 3 2 presents a communicating system made of two machines and two buffers 1 and 2 Figure 3 2a depicts a copycat machine that copies everything that is received on buffer 1 onto buffer 2 the CFSM of Figure 3 2b starts in state gg sends two messages a and b on buffer 1 and then receives them back on buffer 2 These two machines may interact at the end of their interaction the first one will be in state q again the second one in qf and all the messages will have been consumed As we will shortly see q q p is a good candidate to be a final state of this system Definition 3 1 Communicating finite state machine A communicating finite state machine CFSM for short is a 5 tuple 2 B Q qo T w
123. for instance linked lists or binary trees Following the tradition set by most of separation logic literature we will not give a formal semantics to such predicates only informal inductive definitions Defining them more formally is of course possible for instance using graph transformations Dod09 In this thesis we will use the following singly linked list segment and binary tree predicates lseg E F 5 E F emp v E FA3X E X Iseg X F tree E E 0 emp v AX Y Eel X r Y tree X tree Y When F 0 the list segment Iseg E F is terminated the list can be unfolded until there is no further successor In this case we may simply write list Note that the separating conjunction between each node guarantees that the list segment is acyclic To define binary trees we need a record model on the heap because a parent needs one pointer to each of its children which can be achieved with a slight extension of our model as explained in Chapter 2 page 32 As for linked lists the separating conjunctions in the definition ensure that all structures described by the formula are actual trees and not mere graphs or directed acyclic graphs Other more complicated shapes like doubly linked lists or lists of lists or red black trees of lists of trees can be described using the same kind of definitions Dod09 There has been some work in the past on composite data structures BCC 07 and arrays CDOY06 as well We
124. for storable locks and threads In APLAS LNCS pages 19 37 2007 Cited on pages 7 15 34 65 74 80 94 102 122 Aquinas Hobor Andrew W Appel and Francesco Zappa Nardelli Oracle semantics for concurrent separation logic In ESOP volume 4960 of LNCS pages 353 367 2008 Cited on page 102 Alexander HeuBner Tristan Le Gall and Gr goire Sutre Extrapolation based path invariants for abstraction refinement of FIFO systems In SPIN volume 5578 of LNCS pages 107 124 2009 Cited on page 7 Raymond Hu Dimitrios Kouzapas Olivier Pernet Nobuko Yoshida and Kohei Honda Type safe eventful sessions in Java In ECOOP volume 6183 of LNCS pages 329 353 2010 Cited on page 7 Galen C Hunt and James R Larus Singularity rethinking the software stack Operating Systems Review 41 2 37 49 2007 Cited on pages 2 18 149 Bibliography HOO8 Hoa69 Hoa78 H0197 HS08 HVK98 HYCO8 HYH08 1001 Jon83 Lam79 LM09 LMS10 May81 150 Tony Hoare and Peter W O Hearn Separation logic semantics for communi cating processes Electr Notes Theor Comput Sci 212 3 25 2008 Cited on page 6 Tony Hoare An axiomatic basis for computer programming Commun ACM 12 10 576 580 1969 Cited on pages 3 69 Tony Hoare Communicating sequential processes Commun ACM 21 8 666 677 1978 Cited on page 6 Gerard J Holzmann The model checker Spin IEEE Trans Softwar
125. g locations can become accessible after a certain number of receives Flattening gives an over approximation of the owned portion of a state Lemma 6 14 For all open well formed state c if flat a Gf ke then owned a x of Proof The proof is by induction on the number of steps in the computation of owned a In the base case we have owned 0 k 6 lt oy Suppose that the lemma is true for states whose owned portion is computed in up to n steps Let a 0 k be a state whose owned portion can be computed in n 1 steps and let amp s h k and Of flat k dom k and k emp k dom k w k dom k dom k as in the Gotsman et al use a similar notion that they call closure to get around the issue of cycles of ownership leaks GBC 07 122 Chapter 6 Open Behaviours and Soundness definition Let us moreover write T 0 k for the local part amp of an open state 0 k We have owned o owned 6 e p k by definition x my flat 6 e p k induction hypothesis 1 flat o k by definition of 6 and K 77 flat c This concludes the proof The other inclusion does not always hold some of the queues may be unreachable from the local portion of an open state Let us call the difference between flat a and owned c the unreachable portion of c This unreachable part may come from two sources either because some endpoints of the open endpoint belong to
126. g with the same codomain S is dom f wdom g S fug ee f x ifxe dom f g x if xe dom g In many models of separation logic stacks are total functions assigning values to variables and only the heap has a built in notion of ownership by being a partial function from locations to values Rey02 This gives rise to rather unpleasant side conditions in the proof rules and there is a tendency to treat variables as resources more systematically that is to define the stack as a partial map as well BCY06 We follow the latter approach 65 4 1 Assertions E logical expressions X logical variable x program variable v value E E E E arithmetic operations formulas E E boolean expression emp empty stack emp empty heap own x ownership of a single variable Er E singleton heap Pro separating conjunction D o magicwand DA classical conjunction ad classical negation VX first order quantification Figure 4 1 Syntax of CSL assertions X Var x Var v e Val 4 1 2 Syntax The assertions of separation logic grouped in Figure 4 1 describe what is considered to be owned in a given state that is the domains of the stack and heap of the state as well as the values of program variables and the contents of memory cells Logical expressions are identical to program expressions we will use E to denote both except for the fact that they may use logical variables as atoms in addition to program
127. ge passing and the semantics of contracts would be lost 6 1 Open states 6 1 1 Well formed open states Definition From now on the states defined in Section 2 2 1 are called closed states to avoid ambiguities The states defined in this chapter are called open states they account for the local view that the program has of the global state as well as the buffers of the endpoints of all channels with footprints represented by session states of the previous chapter added to each pending message Open states extend both closed states and session states They are elements c s h k k of State with State State x EHeap EHeap Endpoint fn Msgld x Val x State An open state o 0 k State can be decomposed as such if one thinks of it as the local state of a program e is called the local part of the state and is a session state that represents what is currently owned by the program that is what it may safely access and act upon k is an open endpoint heap that associates open buffers to endpoints An open buffer is one where pieces of local state are attached to each pending message in the buffers The domain of k must be sufficiently large to associate a buffer to all the endpoints that are allocated according to c and to their peers in other words to each channel These endpoints can come from two sources either they belong to the local state or they belong to one of the footprints stored in k itself T
128. ges 1 19 2001 Cited on page 3 Scott Owens Susmit Sarkar and Peter Sewell A better x86 memory model x86 tso In TPHOLs volume 5674 of LNCS pages 391 407 2009 Cited on page 13 John C Reynolds Separation logic A logic for shared mutable data structures In LICS pages 55 74 2002 Cited on pages 3 65 69 John C Reynolds Toward a grainless semantics for shared variable concur rency In FSTTCS volume 3328 of LNCS pages 35 48 2004 Cited on page 13 Mohammad Raza and Philippa Gardner Footprints in local reasoning In FoSSaCs volume 4962 of LNCS pages 201 215 2008 Cited on page 70 Zachary Stengel and Tevfik Bultan Analyzing Singularity channel contracts In SSTA pages 13 24 2009 Cited on pages 6 28 43 45 59 George S Sacerdote and Richard L Tenney The decidability of the reachability problem for vector addition systems preliminary version In STOC pages 61 76 1977 Cited on page 54 151 Bibliography THK94 Vaf07 VLCO9 VLC10 VP07 YDBH10 152 Kaku Takeuchi Kohei Honda and Makoto Kubo An interaction based lan guage and its typing system In PARLE volume 817 of LNCS pages 398 413 1994 Cited on pages 6 26 28 63 88 92 Viktor Vafeiadis Modular fine grained concurrency verification PhD thesis University of Cambridge 2007 Cited on pages 7 13 65 74 102 112 114 Jules Villard tienne Lozes and Cristiano Calcagno Proving copyless me
129. gic to copyless message passing which validates programs with respect to their contracts To prove its soundness we define a second semantics for our programming language where the logical reasoning attached to copyless message passing is given an operational meaning This second semantics is related to the first in a way that is independent of the properties of the program and lets us explore the links between a program and the contracts that it abides by some of the crucial properties of contracts good or bad rub off on programs Thus the verification of a message passing program amounts to its provability in our proof system as much as it amounts to verifying its contracts Testing and validating our approach was helped by the Heap Hop tool developed dur ing this thesis that implements our technique to automatically verify annotated message passing programs Richer protocol specifications Starting from this work several directions are amenable to further research in verifying message passing programs First of all contracts are but one means of specifying protocols and several other options could have been considered As discussed at the end of the last chapter one possibility would be to consider more general dialogue machines extended with counters We believe that our logic can easily cover such an extension as do the semantic models we used What would become problematic how 143 Conclusion ever and where we believe inter
130. gular 53 3 3 Contracts language This shows that the language contained in the only non empty queue of C is in fact always regular Let us remember this as the following lemma Lemma 3 1 CF05 Let C be a reachable configuration of a half duplex system and a be an execution that reaches C from the initial configuration Co of There exist C a and Qs such that L Co 5 A C 2 the execution Co 25 C is 1 bounded and C is stable and 3 a2 consists only of sending actions To see why the class of half duplex systems is recursive C c and Finkel give the fol lowing lemma about non half duplex systems which we will also use to characterise half duplex contracts in the next section Lemma 3 2 CF05 A dialogue system F WM Ma is not half duplex if and only if there exist two transitions q1 1la q Ty and qo 2 b q5 T such that the state 1 09 5 is reachable by a 1 bounded execution Intuitively a system that is not half duplex can reach a stable configuration from a 1 bounded execution from which both machines can perform a sending action This condition is also obviously sufficient for the system not to be half duplex since if both machines perform their respective send the two corresponding buffers will become non empty Channel systems with errors In the case of a finite alphabet of messages unreliable or lossy channel systems are known to have good decidability properties Indeed give
131. h a state q forces the two machines to synchronise between two consecutive stops at q To simplify the presentation we only define this notion for dialogue machines where the criterion is easier to express although it could be extended to arbitrary machines and systems Definition 3 23 Cycles Let M 2 B Q init T be a dialogue machine A cycle in M is a tuple of control states q0 qn n gt 1 where qo qn and VO k lt n dr B x 4 x X dk T qy 1 T A cycle is a sending resp receiving cycle if all its transitions are sending resp re ceiving ones A cycle qo qn goes through q if 30 lt i n q qi Definition 3 24 Synchronising states A state q ofa dialogue machine M is synchronis ing if no sending or receiving cycle of M goes through it Note that in dialogue systems that are constructed from a contract a state of one of the dialogue machines is synchronising if and only if the same state is synchronising in the other machine We can thus talk freely about synchronising states of contracts and in fact this property can be directly checked on the contract itself For instance all the states of this contract are synchronising 2la 21b Non deterministic contracts may hide a leak as well In the contract below if each ma chines makes a different choice then they end in the same final state and can stop in the configuration qo q2 a u where there is still a in one of the q
132. he inter process communications of the Singularity OS project They were introduced by F hndrich ef al in the paper Language support for fast and reliable message based communication in Singularity OS FAH 06 along with sufficient syntactic conditions to ensure some safety properties However the lack of formal semantics lead to some bugs being discovered later on by Stengel and Bultan SB09 in published contracts of Singular ity Whenever we use the term Singularity contracts and unless specified otherwise we refer to contracts which satisfy the constraints imposed by Singularity in their fixed version by Stengel and Bultan We show that thanks to these restrictions Singularity contracts are free from reception errors leaks and deadlocks and have bounded communication buffers Moreover we show that they have the half duplex property only one channel may be non empty at any given time in the execution of contracts Figure 3 1 depicts the relationships between dialogue systems half duplex dialogue systems contracts and Singularity contracts In this chapter we give a formal semantics to these objects and study the decidability of the safety properties above which include the ones sought after by Singularity These properties are decidable for half duplex dialogue systems a result that follows directly from the fact that such systems have a decidable reachability set CF05 We will show that these properties are undecidable
133. he syntax and semantics of our message passing programming lan guage and formalises some of the ideas introduced in the previous chapter The semantics of the language is independent of contracts and logical specifications 2 1 Programming language 2 1 1 Heap manipulating Imperative Programming Language Grammar Let us define Hip the heap manipulating imperative programming language We assume that the following sets are defined the countably infinite set Var of program variables ranged over by e f x y e the countably infinite set Cell of memory locations ranged over by J the countably infinite set Val of values ranged over by v We suppose that Var n Cell Varn Val 2 0 Cell and Cell u IN Val The grammar of expressions boolean expressions atomic commands and programs is given in Figure 2 1 The syntax is defined algebraically to ease the definition of the operational semantics and of the logic However using assume and non deterministic choice one can recreate the usual if and while constructs of programming languages we write if D pj else po for assume B pi assume not B p2 Likewise while D pis syntactic sugar for assume B p assume not B 31 2 1 Programming language E expressions x variable v value E E E E arithmetic operations B E E BandB not B boolean expressions Cou instructions Skip inaction assume B assume condition x E variable assign
134. her Deadlock free contracts Similarly the contracts depicted below are respectively non deterministic and non positional and both exhibit a deadlock In the second example the first machine can perform the sequence of actions a b and its dual 5 a Thus they get both stuck waiting for c in the configuration qo q5 u 4 Lemma 3 7 Deadlock freedom For every contract if is deterministic and posi tional then is deadlock free Proof The proof follows the same reasoning as for Lemma 3 6 Leak free contracts Being deterministic and positional is not sufficient for a contract to be leak free because there could be a loop consisting only of sends and involving a final state In that case the system could stop before the receiving machine has gone as many times around the loop as the sending because both machines would be in a final state like in this contract 57 3 3 Contracts la To enforce bounded communications see Lemma 3 9 SinGf requires that all cycles in a given contract contain at least one send and one receive we can require the same condition restricted to those cycle containing a final state to prevent leaks We represent this by the notion of synchronising states of a dialogue machine They are the states q such that each cycle going through q must contain at least one sending action and one receiving action The name synchronising comes from the intuition that suc
135. here e Y is a finite alphabet of messages e B is a finite set of buffers 44 Chapter 3 Dialogue systems e Q is a finite set of control states e qo Q is the initial control state eTCQx Bx x X x Q is a finite set of transitions Given a CFSM M 2 B Q qo T we write init 90t for qo Notations 3 1 In this chapter the set of the buffers of a machine will always be a finite subset of IN We write for one of Elements of B x x are called actions and are written e g n a instead of n a We use T to range over actions For instance the machine depicted on Figure 3 2a is formally represented by the tuple Mo a b 1 2 4 da qo q To where the set of transitions To is To E q 1 a da q 1 b do da 2la q qv 21b q G Similarly the machine of Figure 3 2b is 9t a b q0 q1 42 93 47 q0 11 where T tao la qi 91 11b q2 92 2 a q3 qa 27b qr Let us group communicating machines together to form communicating systems Definition 3 2 Communicating system A communicating system is a tuple F Mi Mn of communicating machines M B Qi qo Ti that share the same alphabet of messages and the same set of buffers together with a set F TT Qi of final states For instance the system of Figure 3 2 is Go q qf Mo Mi The set of final states does not matter yet as no semantics is attached to it In
136. his gives rise to a rather complicated well formedness condition which is the subject of the rest of this section Flattening of a state As will become clear with the open operational semantics the footprints stored in the open buffers correspond to actual pieces of the global state that have been previously sent away Thus one should be able to reconstruct the global state by 102 Chapter 6 Open Behaviours and Soundness tacking all these footprints onto the local state an operation we call flattening Flattening is useful both to obtain a global picture of the current state that includes all the information stored in the pieces of state hidden in the buffers for instance to know who the peer of an endpoint is or what contract is associated to it and to establish a correspondence between the open and the closed semantics as we do in Section 6 4 For the flattening of an open state to be defined all the corresponding session states should be pairwise disjoint and compatible as session states When this is the case the open state is deemed flattable Definition 6 1 Flattable state An open state o 0 k is flattable if 6 and all the states Ca for all a v 6a k amp and e dom k are well formed and pairwise compatible as session states Flattable buffers and open endpoint heaps are defined similarly The following flattening function is defined on flattable open buffers and associates to an open buffer o the session sta
137. his program 26 Chapter 1 Concurrency and Ownership where the size of the buffers is bounded by 1 by adding acknowledgement messages af ter each send receive ack e is added after send cell e x in put_list and the corresponding branch of the switch receive of get_list becomes x receive cell f 1 send ack f dispose x In fact adding acknowledgement messages is a general recipe to bound the size of all buffers by 1 and to mimic the synchronous setting The Singularity OS for instance insists on all communication buffers being bounded by a bound that is known at the time the program is compiled FAH 06 Indeed the operating system itself uses message passing for communications and it must be able to operate even in an out of memory context when all the available memory has been allocated for instance because of a memory leak in one of the running programs in this case the faulty program is generally terminated by the kernel and its memory reclaimed Were the buffers unbounded they would have to be implemented as dynamic data structures for instance as linked lists and sending a message would need to allocate a new node in this list This is not possible in an out of memory context On the other hand if a bound is known on the size of a buffer it can be implemented by a fixed size array allocated once and for all and the channel will be able to operate without requiring any additional memory Deadlock freedom Co
138. ich shows that we need not restrict ourselves to contracts to obtain decidability where we could have used any half duplex dialogue system The restrictions include the fact that a contract should be deterministic and positional On contracts this is already enough to ensure the half duplex property The proof relies essentially on the following lemma Lemma 3 3 Let 2 Q q0 F T be a deterministic and positional contract For all execution qo qo 1 u 5 1 925 15 that ends in a stable state qi qo Proof Let us first remark that if o leads to a stable configuration by a 1 bounded run then a is even and a consists of consecutive sends n a and receives n a for some n and a Moreover by Lemma 3 1 and since the configuration resulting from the execution of o is stable there exists a 1 bounded execution of the system associated to that produces the same state We can thus assume without loss of generality that o is 1 bounded Let us show the lemma by an induction on the size of a If a 0 then q1 q2 qo Suppose now that n gt 0 and for all 1 bounded execution f of size strictly less than m if go 90 uu 5 q 4 u u then q q If la n there is n and a such that a B nla n a and by induction hypothesis nla n a B qo q0 u u ES a Qu u SS qi q2 u u In the last two steps either the first machine is sending and the second receiving or the opposite Suppose we are in the first case th
139. ics For instance x E p immediately writes to x and to x only regardless of what p is while any program of the form p po does not The way it is performed here is unfortunately not compositional in that we describe only the reduction of all of its branches at the same time In particular we lack a rule that would describe the behaviour of g1 O g2 solely in terms of the behaviours of g1 and g2 considered independently A modular description is in fact also possible but would not be simpler so we use the non modular one in this thesis 39 2 2 Semantics Pit p2 0 gt Pp1 0 P p2 0 gt P2 0 P1 0 gt pi o p1 0 error T 1 w F Di P2 0 pi P2 0 skip P2 0 P2 0 P p2 0 error 1 1 norace p1 p2 0 P1 0 ppc P1 0 error t f p1 p2 0 pi pa a p p2 0 error f norace p1 p2 0 P2 0 gt PDP p2 0 gt error 1 1 p p2 0 p pa 0 p p2 0 error skip skip 0 skip o p 0 skip p p 0 y dom s delete y s h k skip s N y h k v Val y dom s U freevar p local x inp s h k gt p x lt y delete y s y v h k Figure 2 6 Operational semantics of programming constructs immediately writes to or reads any resource it must first choose whether to execute p1 or p2 Table 2 1 gives the sets iw p 0 and ir p c for all programs p and states c Let us denote witch a p c
140. ics may be seen as an instrumentation of the closed semantics that makes apparent the ownership transfers that occur when communications are performed on the one hand and the obedience to the channel contracts on the other hand More precisely the open semantics of sending and receiving commands will be changed so that sending a message removes its footprint from the local view and receiving it adds the corresponding footprint So that what is received matches exactly what has been sent the transient footprint is stored in the receiving endpoint s buffer along with the message identifier and value Contrarily to the closed one the open semantics depends on a footprint context and a contract decoration of the program The open character of this new semantics is also reflected in that it makes interferences from the environment explicit Indeed interferences will be able to simulate the sending and receiving of messages on those endpoints not in the program s possession in order to account for the actions of the other programs that may be concurrently executing aside from the current one its environment This is necessary to study the parallel composition of two programs in a sound way as each program is analysed independently from the other as stated by the PARALLEL rule of Figure 4 5 page 71 one should be able to characterise the behaviour of one of them whatever the other one its environment does hence to account for the behaviour of
141. ingle control state Although we do not give here a full formal account of non deterministic contracts we will show how to extend our logic and proof system to support them in Section 5 3 1 These extensions are implemented in our tool Heap Hop which is not restricted to deterministic contracts As for closed states we define the peer mate k of an endpoint e in the domain of a session endpoint heap k if amp s h k e e dom k and k e we write mate k e or mate for e We only consider well formed states namely states s h k which satisfy Ve e dom k mate k e e SIrreflexive Ve e dom k mate k e e dom k gt mate k mate k e SInvolutive V amp 1 2 dom k mate k e1 mate k 2 gt 1 2 SInjective Ve el e dom k as pa SDual Ve e dom k k amp E Q q0 F T r q gt qeQ SControl The first two rules are the session states counterparts of the Irreflexive and Involutive rules for closed states seen page 34 The third one SInjective follows from Channel and Involutive in the closed model but since we do not require the equivalent of Channel for session states we add it explicitly The fourth one ensures that dual endpoints are assigned dual roles of the same contract and the last one ensures that the control state an endpoint is said to be at is one of the control states of its contract The set State is equipped with a composi
142. ional semantics 104 6 2 1 Open semantics of programs 104 6 2 2 Subject reduction a sse gr ee ke ob yee ree rehus 108 6 37 SOUNANESS orai da gis ad Ok chy Sew adhe by Bl oie rah Ge A AT 112 6 3 1 Locality up to interferences 112 6 3 2 Soundness zs de eS A he Kan ee a 116 6 4 Properties of proved programs 118 6 4 1 From open states to closed states 118 6 4 2 Runtime validity 119 6 4 3 Owned portion of a state 122 OAA Leak freedom ies 4 2e a dre 123 6 4 5 Boundedness of communications and deadlock freedom 125 7 Heap Hop 127 252 AA A O Se oq bte es 127 7 1 1 Programming language 127 11 22 Contracts or 6 E RE A on SS 129 7 1 3 Logical fragment 130 722 Anternals AAN a Xena oA e E LAS E e SR 131 7 2 1 Verification condition 131 7 2 2 Symbole execution 133 7 2 3 Entailment checking and frame inference 136 72 4 Contract verification 136 7 3 Output A SN PE os 137 7 3 1 Properties of the contracts 137 7 3 2 Hoare triple verification 137 7 4 Distribution io a en SE A a 138 74 1 Public distribution
143. ional semantics of heap commands e x E faults if E cannot be evaluated in the current stack or if x is not present in the stack otherwise the value of x is updated to E Cell manipulation commands are grouped in Figure 2 4 x new picks an unallocated address and assigns a non deterministic value to it The variable x is updated to contain l If x was not in the stack the command faults e dispose faults if either E cannot be evaluated on the current stack or if E l is not allocated in Otherwise it removes from the domain of h e x E faults if either E cannot be evaluated on the current stack or if E l is not allocated in h or if x is not present in the stack Otherwise the value of x is updated to the value contained at address l 37 2 2 Semantics e f e dom s e Endpoint dom k e f open s h k skip s e E f e h k E eu e e 1 Fils amp Fa s 2 k amp 1 2 01 k e2 1 02 close E E2 s h k gt skip s h k 1 2 Fils E2 s v mate k e e send a E E5 s h k gt skip s h k e buffer e lt buffer k e a v Xi X4 dom s Ej dom k amp amp Es s e dom k Fils buffer k a v a Tx receive a E pj s h k
144. ious states with respect to a footprint context are stable by trans formations by ceremonious programs those that do not reduce into a protocol error with the help of the following lemma For two sets of configurations S1 and S we say that there is a transition from 51 to S by the contract and write Si So if vVC eS 3Ce S C 5g C Lemma 6 1 For all p p 0 6 amp e if pop e e chans o e contract o e then 1 either contract o is undefined and cconf 6 amp init init u u 2 or contract o e amp amp e chans a and cconf a e gt e cconf o or cconf a cconf c e Proof Let a 5 k and o 6 k If the transition p c gt p c is not a channel operation then k k and the result is immediate Let us analyse the remaining cases Let us fix some e satisfying all the above hypothesis Let us assume first that e is not one of the two endpoints of the channel over which the instruction applies It can be observed that control e is either undefined in both o and a or defined in both c and a in which case control g e control c e recall that control o is defined according to the flattening of c Thus for an endpoint that is not one of the endpoints of the channel over which some action is performed the constraint is the same in and o and cconf a cconf c e which shows that case 2 above ho
145. ip s x 1 h 1 v k k E 1 le dom h dispose E s h k k gt skip s hx 1 k k x dom s E s 1 h l v x E s h k k gt skip s x o h k E Fils Ez U le dom h LE E gt s h k k gt skip s A L v k k Figure 6 2 Operational semantics of heap commands Opening and closing a channel The semantics of open and close shown in Fig ure 6 3 now takes the protocol of the channel into account open creates a channel in the initial state of the contract and close deletes it if both endpoints are in the same final state of their contract and their buffers are empty If this last condition is not satisfied close raises LeakError If the channel is closed in a non final state of the contract it raises a protocol error and if the endpoints given as arguments do not form a channel or are given in the wrong order this last condition could easily be dropped an ownership error is raised Like new open takes care not to reuse a location already present in one of the buffers so as not to create an ill formed state Because of the OBuffers constraint on well formed states picking the new endpoints outside of the domain of k is enough 105 6 2 Open operational semantics e f e dom s amp amp e Endpoint dom k qo init e open s
146. is well formed w r t the footprint context U if ec isa well formed open state e for all endpoint e dom ky if kg amp e r q then for all a v a k e a E Yale Er v Note that if c and 7 are both well formed with respect to I then 7 e g is also well formed with respect to I if and only if it is well formed Hence we do not need an additional notation for compatibility in that sense Let us detail what well formed open states with respect to a footprint context are in two special cases the context where no constraint is put on the footprints notice that in this case they are not precise hence the footprint context is ill formed and the one where all footprints are empty If Tirue is the footprint context where all messages are associated to the footprint true then c is well formed with respect to true if and only if it is well formed 109 6 2 Open operational semantics If Temp is the footprint context where all messages are associated to the footprint emp then 6 k is well formed with respect to Temp if and only if it is well formed and flat k Ceremonious states Ceremonious states emerge from the following intuition given a channel in an open state 6 k the contents of the buffers of the two endpoints in terms of message identifiers should be consistent with the control states of the contract that they are in according to c This notion is crucial to tr
147. k thanks to the construction of Msim and Meat So it must be that we are in the last case hence that endsim endeat u u is reachable which is equivalent to saying that M terminates by Theorem 3 1 This shows that checking whether a synchronising and deterministic contract is leak free is undecidable Following the same idea one may build the following synchronising and positional contract e Mim a start 3 dual Meat lolb Ib This contract has a leak if and only if M halts and it is synchronising and positional but not deterministic One may prove in the same way that deadlock freedom is undecidable for synchro nising contracts even if they are either deterministic or positional but not both as 61 3 3 Contracts 5 amp 6 we will see next It suffices to change the bottom part of the above contracts to the following Mir gt 3 dual Meat or By taking the first template we obtain a synchronising and deterministic but not positional contract that deadlocks if and only if the Turing machine M halts and by taking the second template we obtain a synchronising and positional but not deter ministic contract that deadlocks if and only if WM halts With the same reasoning and initial templates we prove undecidability of fault free dom for synchronising and deterministic or positional contracts with the following contract temp
148. l accepting runs end in a stable configuration Note that a system without accepting states is automatically leak free 3 2 Verification of communicating systems 3 2 1 Simulation of a Turing machine by a dialogue system Unfortunately given an arbitrary contract one cannot decide whether it satisfies any of the safety properties listed in the previous section The main reason behind this is that CFSMs can simulate Turing machines which was first noticed by Brand and Zafiropulo BZ83 the main idea of the proof is that an unbounded buffer can act as the tape of a Turing machine This result was later extended to dialogue systems of the form Mi Mi so called identical communicating processes by Finkel and McKenzie FM97 We extend it here to contracts that is systems of the form Wt dual 9t All the undecidability results presented in the next section are based on the encoding of Turing machines into dialogue systems presented below Definition 3 20 Turing machine A Turing machine is a tuple Q T 0 91 where e amp is the tape alphabet e Q is the finite set of states eT CQxXxQxXx a is the transition relation e O X uQ is the blank symbol qo Q and qy Q are respectively the initial and final states A configuration of a Turing machine 2 Q T O qo qf is a word from x 03 x Q x 85 0 0 that accounts for the current state of the machine the
149. l contract Output Whether or not is fault free Proof We reduce each of these six problems to the halting problem of Turing machines using Theorem 3 1 as a black box Let M X Q T 0 qo qf be a Turing machine and F Msim Mcat be the dialogue system equivalent to M by Theorem 3 1 60 Chapter 3 Dialogue systems 1 3 amp 4 Consider the following contract Cleak where a b X the incoming arrow into Mim goes to isim and the outgoing arrow comes from endsim and similarly for dual Mear Mein dual Mear This contract is synchronising and deterministic Let us show that it exhibits a leak if and only if DM halts Suppose that M halts the configuration endsim endcat u u is then reachable From this configuration the first machine will send b twice but only one b will be received by the second machine before the system comes to a halt in the final configuration end end u b which is not stable Conversely suppose that Cieak has a leak A run of the dialogue system associated to Cleak corresponds either to both machines having taken the left branch and executing in Msim or to both of them having taken the right branch thus executing in the copycat machine or and this is the behaviour that simulates a run of the Turing machine each one taking a separate way In the first as well as the second case it is straightforward to check that there is no lea
150. late Mim f UT dual Meat Conclusion Table 3 1 sums up our decidability results for contracts and dialogue systems 62 Chapter 3 Dialogue systems S bu WS D PY E S amp S S S x gt S S e F S S Y 2 E E Y None U U U U D Half duplex D D D D Yes Det amp Pos D D D D Yes Contract U U U U D Det amp Synch Contract U U U U D Pos amp Synch Contract U U U U D Det amp Pos amp Synch Contract D Yes Yes Yes Yes Table 3 1 Decidability results on dialogue systems D decidable U undecidable Yes the property is always true Det deterministic Pos positional Synch final states are synchronising The first three lines consist of known results Contracts vs dialogue systems As this table shows and perhaps surprisingly because of their syntactically restricted nature contracts are as undecidable as arbitrary dialogue systems when it comes to the safety properties that we are interested in Moreover the syntactic restrictions imposed on contracts in Singularity make the contracts half duplex Since half duplex dialogue machines already have all the required decidability properties and the class of half duplex dialogue machines is recursive one might as well abandon contracts and use half duplex systems instead However this is not to say that contracts are useless as a class of communicating ma chines Indeed one rarely need
151. lds Let us assume now that e is one of the two endpoints of the channel over which the instruction applies and reason by case analysis on the instruction 111 6 3 Soundness e close Since contract o e is defined by hypothesis e is not the closed chan nel This case is thus impossible open Case 1 above holds e send Let us show that case 2 above holds and in particular that cconf a gt e cconf a By symmetry we may assume that is the endpoint used for sending By the rule of send control c and control c e must be defined and equal to some control states q and q2 Moreover the rule also ensure that there is a transition q1 q2 in Let C2 q2 qh W2 W5 be a configuration in cconf c Then w w a and Cj qi q5 w2 wi gt C Moreover C1 cconf o since q is constrained in the same way in g and g receive and external choice Same arguments as for send Lemma 6 2 Subject reduction Jf c Statef and p o gt p a then o States Proof The fact that well formedness with respect to a footprint context is preserved by the reductions of a program is immediate from the reduction rules presented in the previous subsection Let us focus on the ceremonious property Let us check each point of the definition of ceremonious states for c Firstly itis flattable Secondly let chans o be such that contract o e
152. le and switch receive constructs function calls and messages with multiple parameters Moreover although this 127 7 1 Input message cell vall gt contract Cell initial state start cell gt end final state end 1 put_get emp local e f x x new e f open Cell put e x get f close e f emp put e x el gt Cell start xl send cell e x el gt Cell start get f fl Cell start pr _ee local y y receive cell f dispose y f gt Cell start pr ee Figure 7 1 Heap Hop input file corresponding to the cell transfer program does not appear in the syntax receive commands can be used as syntactic sugar for single branch switch receives The parallel composition is syntactically restricted to a parallel call of two functions Because function declarations are annotated with pre and post conditions this syntactic restriction allows Heap Hop to know what the splitting of resources between the two sides of a given parallel composition will be instead of having to enumerate and try them all At the beginning of the file are message tags declarations When declaring a new message tag with the message a 4 statement the user provides the number of parameters that messages with this tag will have called the arity of the tag or the arity of the message The arity of tag a is written ar a and the syntax of a message declaration that
153. leaked away This can be a means of detecting such pathological situations since most of the times channels will be closed at some point in the program However more extreme situations are possible where the whole channel disappears For instance with a footprint describing a whole channel chan emp val gt Y Y e val the following program proof can be derived given a system that allows the sending of chan e f lr emp e f open efite XAf YA X ER YCEr qg xY gt X v q send chan e e e f i emp More complicated examples can be crafted if we try and forbid the previous situation by taking Yep emp val gt X X dst which forbids sending the ownership of the recipient endpoint within the message For instance using two channels that lock each other e f ee ff lr emp 94 Chapter 5 Proving Copyless Message Passing e f open ee ff open e XA f YA Xwo Y Crg Y gt X 6 7 7 fet FE wage XK nier A X 5 Y ir q amp Y o X 67 7 send ep e ff send ep ee f e i e r q eer r q In this example the endpoint pointed to by f is in the queue of the one pointed to by ff and vice versa making it impossible for the program to retrieve any of these two endpoints without cheating the ownership assumption In the logic both endpoints have vanished from the assertions giving the false imp
154. ls As the technique relies mainly on the way entailments are checked we delay the discussion to after the exposition of the entailment checking al gorithm in Section 7 2 3 For now let us assume that such an algorithm is given Symbolic execution on an example Let us provide an informal description of the sym bolic execution procedure by applying it to the second verification condition obtained ear lier The first command is extchoice cell fin To expose the contract associated to f the precondition is first rewritten by substituting e by 0 and removing the correspond ing equality and then by performing a case split on the value of the test 0 0 As one of the formulas obtained presents a contradiction 0 0 it is discarded more precisely ver ification conditions of the form false p v are always true The remaining verification condition has f gt C transfer as precondition As the contract associated to f in the precondition gives only cell and fin as potential messages in the receive buffer which matches the list of messages for which f is ready the check is successful and the precondition is passed as is to the conditional that follows Each branch of the if then else construct is analysed separately In the first branch the receive transforms its precondition by updating the control state of f to the im plicit control state transfer_0 and by adding to it the invariant of the message cell correctly instantiated
155. mantics es gah ee BAR A el ee a AS 4 1 4 Derived formulas 4 1 5 Inductive predicates 42 POOL SYSUCI a etu rite ssl yas re Gen et n o Hee ed 4 2 1 An extension of Floyd Hoare logic 422 Smallaxioms os Gogh a e Wek dee a e HERR RE pas 423 ProoLrules ick o Ba ek Aes Sods 4 2 4 Conditional critical regions Proving Copyless Message Passing DL Proof systemi aira er le TE er RAE Me td a asides BP AMS DLAs ASESSLOM SLATES MEE 511 2 cASSertiols io a de beet os AQ AUR nte RUMOR 5 1 3 Rulesforcommunication 5 2 ExampleSu sut E ra EO PEE Pee eum avete Sd s gat 52 1 Cell and endpoint passing 5 2 2 Automatic teller machine 5 3 Restrictions of the proof system 5 3 1 Deterministic contracts 5 3 2 Precision of message footprints 5 3 3 Channel closure leaks 5 3 4 Cycles of ownership leaks 5 3 5 A first soundness result Related Work 4 4 sse date EAA EA EEO ee eR 43 46 47 48 50 50 53 54 54 60 62 65 65 65 66 66 67 68 69 69 69 70 72 Contents 6 Open Behaviours and Soundness 101 6 L Openistates ccv a AE DA A red ps 102 6 1 1 Well formed Open states 102 6 2 Open operat
156. meaning It is a useful proof artifact nonetheless We shall give formal definitions of these concepts in Chapters 4 and 6 If all the components of a program respect the ownership hypothesis then the following separation property from the same paper by O Hearn holds where one can think of a grouping of mutual exclusion as a particular lock or critical region identifier Separation property At any time the state can be partitioned into that owned by each process and each grouping of mutual exclusion A crucial concept of the ownership reading of the heap is that the partition of the state described by the separation property is not fixed but rather can dynamically change through out the execution of the program Theses changes occur either when a process allocates or deallocates portions of the state that it owns or at synchronisation points Thus acquiring a lock or a resource results in taking ownership of the portion of state attached to it and adding it to the portion of state owned by the process Symmetrically releasing a lock or exiting a critical region corresponds to gouging a portion of the owned state of the process to give to the corresponding resource As we will see in this thesis and especially in Chapter 5 the same reading can be given for message passing sending a message corresponds to a loss of ownership and receiving a message corresponds to a gain The idea that one should be able to attribute each memory location to
157. menable to compositional reasoning with separation logic for instance using the work of Gotsman et al GBC 07 or the marriage of rely guarantee reasoning with separation logic of Vafeiadis and Parkinson VP07 In the parallel increment example one could rewrite each side of the parallel composition using locks to protect the increments assuming a previously declared lock 1 although monitors are sufficient as seen above acquire 1 xtt release 1 Signals Another reading of locks is as wait and signal primitives acquiring a lock is similar to waiting for this lock to be free and releasing it is similar to signaling whomever is waiting for it that it is now free Signals are similar to locks in this regard but they may get lost when nobody is waiting for them Signals are used through two primitives signal and wait They take as argument an identifier much as CCR and locks do When calling wait c a process is put to sleep until another process calls signal c Signals that were issued while nobody had been waiting for them are discarded so the moment at which signals are fired can be crucial Let us illustrate this definition with the producer consumer problem a classic problem in concurrency The scenario is as follows two processes share access to a finite buffer in memory One of them the consumer pops elements from the buffer while the other the producer puts new elements into it The consumer process should not attempt
158. ment x new memory allocation x E memory lookup E E memory mutation dispose E memory deallocation p programs c atomic command p p sequential composition p p parallel composition p p non deterministic choice p iteration local x in p local variable declaration Figure 2 1 Syntax of the Hie programming language x Var and v e Val Records Although the syntax lacks a record model we can simulate one by taking Loc to be the set of strictly positive integers and adding a size argument to the allocation command new This allows programs to allocate consecutive cells in memory which can be accessed through pointer arithmetic to simulate field accesses For instance one would allocate an element of a doubly linked list with x new 3 and access its datum at x its forward link at address x 1 and its backward pointer at address x 2 Expressions could be extended with richer arithmetic operators e g x or or other basic data types like strings However the fragment presented above is sufficient for our exposition HIPCCR Hir does not provide any concurrency primitives to synchronise or communi cate between programs other than sharing access to variables without any protection mech anism such as locks HiPCCR is an extension of H r with constructs for declaring resources and using them inside conditional critical regions CCR It extends the grammar of Hip s 32 Chapter 2 A Model of Copyless Mes
159. mmunications like all means of synchronisation can introduce deadlocks A communication deadlock happens when two or more processes are blocked waiting for each other to send a message We can also call deadlock a situation where a process is waiting for messages of some kind on an endpoint but either another type of message arrives or no message at all For instance assuming that e and ee ff form two channels the two program snippets below can and will deadlock if executed with empty initial buffers send a e switch receive receive b f receive c f The program above deadlocks because the process on the right is waiting for b or c but a is sent The program below deadlocks because it waits for messages on the wrong channel it may not deadlock if another process sends a message a on ee at some point send a e receive a ff The program below shows a more intricate example of deadlock receive b e receive a f send a e send b f The deadlock disappears if the order of sends and receives is permuted on either side of the parallel composition or on both sides send a e receive a f receive b e send b f Fault freedom One of the examples of the previous paragraph requires more attention namely the first one in which the message at the head of the buffer is not one of the messages 27 1 2 Message passing expected by the switch receive This can be seen as an erroneous communic
160. n a sys tem where all the channels involved are lossy one can decide whether a given configuration is reachable or not from which the decidability of many safety problems follows AJ93 If messages arrive out of order then CFSMs are equivalent to counter machines because the queue is then a mere multiset of messages and sending and receiving are equivalent to respectively incrementing and decrementing the counter associated to the corresponding message In particular if we cannot test the emptiness of the queue that is if attempting to receive on an empty queue is blocking then it is equivalent to a vector addition system with states VASS In this case the reachability problem along with many others is also decidable May81 ST77 If there exists a non blocking receive primitive the system can encode counter machines which are as powerful as Turing machines Min67 starting from 2 counters hence two buffers 3 3 Contracts 3 3 1 Syntactic sufficient conditions Half duplex contracts As we will see in the upcoming sections contracts restricted as they are by their symmetric form still retain the power of Turing machines from dialogue 54 Chapter 3 Dialogue systems systems Theorem 3 2 However simple syntactic restrictions on contracts are sufficient but not necessary to ensure fault leak and deadlock freedom These restrictions imply in particular that the system described by the contract must be half duplex wh
161. n of equalities between expressions what Berdine et al call pure formulas In this case the entailment is true In fact the decision procedure used by Smallfoot and Heap Hop is complete as shown by Berdine et al BCOOSb with little adaptation hence the entailment is false if it cannot be reduced to one of the form o emp gt emp where is pure Frame inference as performed by Smallfoot and Heap Hop is closely connected to the procedure we have just described If we have to find a frame 4 such that 1 2 Y we try to prove 1 gt 6 using the procedure above If it succeeds the frame emp suffices If it fails however it will be because of one of the following two situations either a predicate of the right hand side cannot be matched by a portion of the left hand side formula even after normalisation in this case Heap Hop gives up on finding a frame The second case is that the procedure reaches an implication emp where is impure emp In this case one can show that is an admissible frame solution 1 2 7 2 4 Contract verification Heap Hop checks sufficient syntactic conditions to ensure that all contracts are fault free and leak free The conditions are the one dictated by Corollary 3 1 page 60 contracts must be deterministic positional and synchronising For this purpose Heap Hop stores each contract as an identifier a set of initial and final states and a list of states
162. n of this program one could expect the value of x to be 2 as it would be the case with two increments ordered in sequence However in a concurrent setting the final result can also be 1 as exhibited by the interleaving drawn in Figure 1 1 the first thread is scheduled first but is interrupted after the line y x 1 At this point the second thread starts and is executed entirely Now x y and z all hold 1 The first thread is finally allowed to finish and writes again 1 to x hence the overall effect has been to set x to 1 instead of 2 More generally races make apparent the level of atomicity or granularity of programs and even of basic instructions in their presence one has to precisely state what is guaranteed to execute without interruption 12 Chapter 1 Concurrency and Ownership Figure 1 1 Two unprotected increments in parallel and an interleaving which leads to the final state x 1 Of course not all races are bugs some programs are designed to be racy for efficiency purposes and much care is given to ensure that these races will not affect the program badly Yet even in these cases races are limited to instructions that are known to execute atomi cally like compare and swap or test and set these programs are closer to non blocking or fine grained concurrent programs than to truly racy ones Programs of this sort are nonethe less very hard to get right let alone formally verify The book The Art of Multiproc
163. ne can restrict the specification of programs to only be about the cells they actually access their footprint RGO8 This also means that we can give the axioms for atomic commands in a very minimalistic way Thus the following triple which states precisely and unambiguously the portion of state that is necessary for the command to successfully fire can be used as a so called small axiom for the mutate command MUTATE var E1 Ez IF FA d LEA Ez var E1 Ez IF FA md Ez 4 2 3 Proof rules The proof rules of concurrent separation logic adapted to our setting with variables as resources but without permissions and to the programming language Hip are split into the axioms for atomic commands of Figure 4 4 the rules for programming constructs of Figure 4 5 and the logical rules of Figure 4 6 Let us describe each rule Skip The program has already reached its final state Using this axiom and the frame rule one can derive o skip for any Assume If the test B is true the program terminates The stack must contain the variables of B AssiGN If the expression E can be read and the variable x can be written the value of x is updated to be the same as FE Lookup and MUTATE Similar except that E resp E must point to an allocated location New and Dispose Change an empty heap into a single cell and vice versa SEQUENCE This is the classical Floyd Hoare rule for composing programs sequentially the post condition
164. ng k to enqueue the pair a v in the buffer of resulting in a a v where is the concatenation operation over words The command faults if any of the lookups fails Note that sending never blocks and provided that appropriate resources are held always succeeds The case of receiving is more involved since it may only be performed inside an external choice block The reduction rule selects an available message in one of the endpoints buffers that is awaited by one of the receives In other words it selects a message a v such that x receive a E piis one of the guarded pro cesses of the external choice If it finds such a pair it pops it from the corresponding buffer and stores the value of the message in x If not there are two possibilities either the buffers of all the endpoints mentioned are all empty in which case the re ceive blocks or the pair at the top of one of the endpoints buffers is an unexpected one The latter case produces a MsgError error even when other branches could execute successfully Finally if any of the x is absent from the stack or if the expressions cannot be evaluated in the stack or if they do not all correspond to allocated endpoint locations the command faults and results in OwnError The semantics of programming constructs is given Figure 2 6 We write freevar p for the set of free variables of p which is defined as usual by structural induction on p as the
165. ng without endpoints and how they are applied We will soon show how symbolic execution is performed in our example but let us first introduce the frame inference problem Frame inference problem Along the way other entailments have to be checked In fact each jsr call requires an instance of the frame inference problem to be solved as described below 133 7 2 Internals Definition 7 1 Frame inference problem The frame inference problem consists in find ing given two formulas and a third formula 1 such that the following implication is valid p gx The name frame inference comes from its relation with the FRAME rule if one knows that 1 p 2 is provable and is given as a precondition one has to find a frame v such that 61 4 in order to apply the frame rule in the following way after a weakening step h v hi p toa 9 pio vj WEAKENING FRAME When the symbolic execution reaches a 1 jsr 92 instruction with as current formula it tries and solve the following instance of the frame inference problem is there a formula 4 such that p p1 Y If there is the symbolic execution resumes with the rest of the program and 4 as current formula Berdine et al explain how the frame inference problem is solved in Smallfoot in their pa per on symbolic execution BCO05b Adding endpoints to the heap model do not alter their algorithm in any but minor detai
166. ns consists in chopping each of them together with their specifications into several verification conditions Following the terminology of Berdine et al in their paper describing Smallfoot BCOO5a a verification condition is a triple 4 si v where si is a symbolic instruction that is a loop free sequential program described by the following grammar si c 0 jsrz v si si if B then si else si where c is the following set of atomic commands d assign x E new x lookup x E t mutate E t E free E open e C close E E send a E extchoice LM receive a E In the above grammar is used to denote a list of variables a list of expressions and LM a list of pairs E MD where E is an expression and M is itself a list of message identifiers hence if Expr is the set of expressions LM Expr x Msgld Because of the initial parsing phase all commands are now presented in terms of constructors instead of their syntax friendly versions For instance x new is translated into new x Function calls and parallel compositions are translated into jsr instructions inherited from Smallfoot and described as such by their authors BCO05a Semantically 4 jsrz v is a generic command It is the greatest relation satisfying the pre and post condition and subject to the constraint that only the variables in x are modified 131 7 2 Internals Switch receives
167. nsistent with the contracts and current control states of the endpoints Well formedness with respect to a footprint context Given a footprint context I it is natural to define the notion of well formedness w r f T for each element a v Ga of the buffer of an endpoint e whose peer is e and has role r it should be the case that Ga E ya amp e r v The set of all such states is denoted by State This will crucially help us in proving the soundness of the CHANNELDISPATCH rule receiving a message a 108 Chapter 6 Open Behaviours and Soundness P P2 0 gt p1 0 P P2 0 gt P2 0 pia gt p p g gt error pii P2 gt pi P2 0 skip p2 Z gt p2 T pi P2 0 gt error norace pi pa 0 pia gt pi c 1 0 gt error Pi p2 a gt pil pz 2 p p2 g gt error norace pi pa 0 P2 0 gt pz o P2 0 error p1 p2 0 gt p po 0 p p2 0 gt error y dom s p a gt skip p p o delete y s h k k gt skip s y h k k flat s h k k sp hy ky v Val y dom sy U freevar p local x in p s h k k p x y delete y s y v h k K Figure 6 6 Operational semantics of programming constructs from a state that is well formed with respect to I adds a piece of state verifying Ya to the local state Definition 6 4 State An open state o k with flat c sp hy ky
168. nversely when a process receives a message it gains ownership of that portion of mem ory This form of ownership transfer prevents the overlapping of areas of memory that are owned by different processes at a given time ownership of pieces of heaps hop from one process to another following the flow of messages Channel contracts The message passing paradigm is not without its own pitfalls for instance it can introduce deadlocks in programs when two processes each wait for the other to send a message or communication errors when an unexpected message is sent on a channel or when a channel is closed with undelivered messages still in its buffers Moreover the programmer may wish to export the protocol that is used on a particular channel for instance for others to use as an interface to its program To address some of these issues Singularity introduced contracts which are communicating automata used to specify such protocols Contracts also allow the SiNG compiler to statically verify some interesting properties about communications which sometimes have to be double checked at runtime in their case for instance the ab sence of deadlocks on a single channel or the existence of a bound on the number of pending messages Their authors make the following appealing claim of modularity FAH 06 The channel contracts provide a clean separation of concerns between interact ing components and help in understanding the system architecture at a
169. o many many to one In some cases one may wish to broadcast a message to a set of recipients instead of sending the same message over several individual channels Practically this could mean being able to duplicate an endpoint between several participants each allowed to perform only receives on it We only support point to point communications in this work Moreover we ensure a linear usage of channels sharing of endpoints is disallowed and only one process at a time may attempt to send or receive on a particular endpoint Life and death of channels In our setting channels can be dynamically allocated dis posed of and individual endpoints can be passed around through other channels thus al lowing the topology of the interconnection network between processes to change during the execution Acknowledging the fact that endpoints are allocated on the heap allows for a flexible handling of channels one benefit of which being that they may be stored inside arbitrarily complex mutable data structures Protocol specification It is often desirable to be able to describe what protocol a given channel follows that is which sequence of messages can be expected on this channel This can help in proving the safety of communications on any channel following this protocol for instance For this purpose we have chosen to borrow the notion of contracts from the http www mpi forum org 25 1 2 Message passing Singularity project FAH 06
170. of a program is taken as a precondition for its continuation 70 Chapter 4 Concurrent Separation Logics SKIP ASSUME emp skip emp var B lr emp assume CB var B 1 B emp ASSIGN x var E i E X emp x E x var E I x X Aemp LookuP x var E i E Y Y X x EE x var E i Y X x X MUTATE var E1 Ez IK By Re A Ey X E E5 var FE Ez Ir Bye X New xik emph x newO xik x gt DISPOSE var E lr E gt dispose E var E lr emp Figure 4 4 Proof rules for atomic commands SEQUENCE PARALLEL g p o teo wj piv hv tw Lo psp 9 oplp px CHOICE STAR H piy op v o p 6 6 p p v 0 p 0 LocaL own z j plx z own z vj 4 local x inp w z freevar p Y Figure 4 5 Proof rules for programming constructs 71 4 2 Proof system FRAME WEAKENING p p 9 gp pri voy px v p dx 9 pt CONJUNCTION DISIUNCTION gi p v1 O2 p s di p V1 bo p Wa 1 62 p i v2 21 V ga p i v Y2 EXISTENTIAL RENAMING o p V o p V 1X 6 p 3X Y o x yl px gt y i e y Figure 4 6 Logical proof rules PARALLEL The rule for parallel composition accounts for disjoint concurrency one has to be able to partition the state into two disjoint substates that form valid respective preconditions for each of the two threads The resulting post con
171. of the subexpressions is not an integer for instance for locations although one may consider that locations as integers to allow pointer arithmetic as discussed page 32 Finally given a function f we write f x v for the function f that has the same domain as f possibly increased by x if x was not in the domain of f and such that f x v and f y f y for all y dom f x We write f x S for the function f defined on dom f S such that f and f coincide on this new domain We further abbreviate modifications of the buffer of an endpoint by writing k buffer e lt a for k e mate k e a Although we will not use it in this chapter we also write for a function with empty domain and 11 v1 En Un for x1 V Tp Un For concision whenever possible we describe all the cases where executing a command will produce an ownership violation together with the reduction where the command exe cutes normally We do so by putting the premises that are necessary for the command not to fault in boxes A boxed premise indicates a reduction to OwnError from a state where the premise is either false or undefined Consider for instance the rule for memory lookup x dom s E 1 h l v x E s h k skip s x v h k It indicates that x LE will fault whenever x or one of the variables in E is not present in the current stack or
172. oices that have been made and the problems of interest related to the verification of message passing programs 1 2 1 Communication primitives Let us describe informally the communication primitives we have adopted in this thesis The primitives for opening a channel and sending and receiving are direct adaptations of the corresponding primitives in Singularity while closing is performed differently in our setting Opening a channel Opening a channel allocates two endpoints that are each other s peer or mate and have initially empty buffers Sending and receiving messages Each send and receive instruction of our language specifies a message identifier or tag for the kind of message that is sent or that is ex pected on the channel These tags can be thought of as representing the type of what is being transferred Receiving is only possible via a switch receive construct Each branch of this construct specifies an endpoint a tag and a continuation The semantics of switch receive is to select one of the branches that are ready to execute given the current contents of the various endpoints buffers perform the corresponding receive and call its continuation If none of the branches is ready to execute it sleeps until a new message ar rives on one of the empty buffers Sending on the other hand is asynchronous and always succeeds When there is only one branch in a switch receive for instance switch receive x receive a e p
173. on condition generation phase 7 2 2 Symbolic execution The second step of the automatic verification consist in symbolically executing the body of the verification conditions Starting from the first command the precondition is trans formed according to systematic rules that mimic the effect the command has on the state at the formula level The new formula is then used as the precondition of the remaining pro gram Thanks to the fact that verification condition bodies are sequential and loop free this process can be repeated until no command remains The resulting formula is then checked against the post condition in the last step of the verification described below More pre cisely a verification condition o p v is transformed into several entailment checks 1 that hold only if the verification condition is a provable Hoare triple Symbolic execution follows a finite set of rules that may be seen as rewrite rules between verification conditions one for each possible command at the head of the current program and additional ones to rewrite the current formula into a more canonical form in between the application of rules for commands For instance the rule for memory look up can be presented as the following inference rule 5 Bl gt p xex x Bolex pA x fresh o E E p x E gt t 0 The interested reader may refer to the article of Berdine et al BCO05b for details on the rest of the rules in a setti
174. operties that make all these variants valid models of separation logic that is models in which the FRAME and PARALLEL rules see Figures 4 6 and 4 5 are sound There are fundamentally two ingredients to it the underlying state model must be a sepa ration algebra and the atomic commands must behave as local functions over these states The model and proof system presented in this section fit the framework of abstract sep aration logic if one extends it to handle local variables and external choice Many other models can be used as a basis for a separation logic one can do away with the stack and reason only on the heap or attach permissions to variables and or memory locations to permit read only sharing between programs The main theorem of abstract separation logic is a generic soundness result for all these logics and models This result can be instantiated to recover Brookes soundness result see Section 4 2 3 In fact the soundness of our original message passing logic was first proved using abstract separation logic VLCO9 To achieve this we had to refine the proof system and the underlying model of abstract separation logic to account for synchronisation and communication issues Indeed as we will see below inferring soundness from the rules presented above would lead to a semantics for the programming language which would be a very coarse approximation of the one presented in Chapter 2 The approach exposed in this thesis is differ
175. or closed programs is given by Theorem 6 2 page 119 and leak freedom is discussed in Section 6 4 4 5 2 Examples Let us show how to prove a few typical examples Following the notations of Heap Hop we give the footprint formula associated to a message identifier in brackets next to its declara tion for instance message cell emp val 1 For clarity we allow the declaration of non mutually recursive functions in the syntax as they can simply be inlined at their call sites to obtain a program that conforms to the formal syntax A function declaration will also mention its expected pre and post condition The following code snippet indicates that 0 4 is provable f x 0 body of f y We also indicate intermediary steps of the derivation informally in the code comments lines beginning with We use Heap Hop s notations for contracts Let us begin by proving some of the examples described in Chapter 1 5 2 1 Cell and endpoint passing Cell passing We give a proof of the cell passing example of Figure 1 6 in Figure 5 2 As noted in Chapter 1 the message cell carries the ownership of the cell whose address is the value of the message This is reflected in the footprint emp val Notice that the transfer of ownership is visible in the pre and post conditions of put and of get As discussed when this example was introduced see page 22 one could imagine a vari ation of this example where put_cell retains
176. otsman et al have extended it to support storable locks and how their approach and ours were faced with similar problems in some respects They are how ever concerned with objects different in nature Vafeiadis on the other hand has extended separation logic to support rely guarantee reasoning However his work is about commu nications via shared variables and the connection to the message passing case is unclear short of implementing buffers and contracts using lower level primitives 99 CHAPTER 6 Open Behaviours and Soundness In this chapter we define an open semantics for programs with regards to which we prove the soundness of the logic of Chapter 5 This open semantics is a triple point between the proof rules the semantics of Chapter 2 and the contracts of Chapter 3 Indeed it gives an operational meaning to the ownership transfers suggested by the proof rules while being connected both to the natural semantics of programs of Chapter 2 henceforth the closed semantics and to the semantics of the contracts of the program This allows us to use the open semantics as an intermediate step in the proof of the soundness of our logic with respect to the closed semantics we first prove the soundness with respect to the open semantics and then connect the open semantics to the closed one Similarly we show that proved programs inherit the absence of unexpected receptions and undelivered messages from their contracts The open semant
177. ould be in charge of handling these parameters One could also go in another direction and try to find a more general model of concur rency or of message passing that would encompass our own It is a bit disappointing indeed that abstract separation logic was unable to give a natural meaning to message passing con structs and one may wish for such an abstract framework that would apply to more models of concurrency Finally instead of limiting channels and protocols to dialogues one could imagine mul tiparty conversations occurring on channels and specified by multiparty contracts These contracts could take the form of arbitrary communicating systems with any number of par ticipants for instance One could follow what has been accomplished by the session types community in this direction HYCO8 Progress Studying the relationship between progress properties of a program and the progress properties that can be established on the protocols it follows could allow one to prove that a program will never get stuck on a communication To this end one may be able to borrow some ideas from the Chalice tool LMS10 or from multiparty session types BCD 08 both of which can prove progress for programs using multiple communi cation channels Full featured programming language Besides augmenting the power of logical speci fications the programming language itself may be extended which would certainly prompt the need for extensions in our logic as
178. our logic The originality of our soundness result is that some of the properties that a successful proof of the program entails depend on the properties of the protocols that the program follows which can be studied separately We do not give here the formal statement of soundness as it is non trivial to express In particular it requires to make a connection between a closed state and a session state In the following argument we suppose that there is such a connection that allows us to say that a closed state satisfies a given formula of our logic Informally if a triple r 6 p v is provable and T is well formed then for all state c and interpretation 7 if there is a formula yy corresponding to the concatenation of the footprints of the messages in transit in c such that 0 2 yo then 1 p commits no ownership error in particular there is no race 84 Chapter 5 Proving Copyless Message Passing 2 p follows its specified protocols 3 if p terminates with the final state o then there is 7 corresponding to the concate nation of the footprints of the messages in transit in c and there is Y corresponding to some leaked state such that o i 4 yp V 4 if all the contracts of p are fault free then p commits no message error 5 if all the contracts of p are leak free and if additionally Il is admissible see Sec tion 5 3 4 then there is in fact no leak and 7 emp Our formal soundness statement f
179. ove program loops which is not the case For a more in depth ac count of this counter example and the possible remedies see the paper by O Hearn O HO7 Section 11 To summarise its conclusions one can abandon the conjunction rule to restore soundness but more often than not resource invariants are required to be precise in con current separation logic and its variants and extensions O H07 Bro07 GBC 07 Vaf07 We adopt the latter restriction Soundness Brookes has proved Bro07 that the soundness result stated earlier still holds for concurrent separation logic with conditional critical regions A key intuition to the proof is again the separation property exposed page 18 Let us show how it affects the soundness statement Given a resource context rj y Yn Yn and following Brookes notations we write inv I for the spatial conjunction of the invariants of I we write for the iterated version of n inv T Qoi i l Adapted to our setting Brookes statement of soundness becomes If 0 p v is provable then for any state c satisfying the formula inv T p o error and if p o skip o then o satisfies Y inv T Example We can now prove that the following example is race free The global variable x is shared between two threads that both increment it within a critical region this example was presented on page 14 74 Chapter 4 Concurrent Separation Logics own x A
180. own to its interactions with users and the bank hence the lack of code for checking the PIN of the user for instance This program does not fit our model stricto sensu communications between the ATM and the bank do not happen over a shared memory butrather over a communication network However we argue that verifying this program in the copyless setting still makes sense if we look at it from an ownership point of view Indeed receiving a new endpoint is equivalent 88 Chapter 5 Proving Copyless Message Passing message cell emp val e message fin emp Aval 1 q val src contract C initial state q 1 cell gt q fin gt q final state q put_cell e x e xlrer 1 3 x 1 4 local t while x 0 e x ti e 1 q list x 4 e x tlhe 5 1 9 xe T list T t x gt tl e x tlhe 1 q xe T list T t T send cell e x e x tiI ee 1 q list t x t e x tl ee 1 q list x e x tl e 1 q send fin e e e xIkemp get_cell f firf gt X 2 q 1 local y ee ee 0 while ee 0 f y eelr ee 0nf 2 q v ee XAX 5 6 1 q f X 6 2 4 1 switch receive y receive cell f dispose y ee receive fin f f y eelree XAf YAX Y C 1 q Y gt X E 2 q close ee f fi emp main x xiFlist x 4 local e f e f open C x e fielist x e
181. ownership of the cell pointed to by x and disposes it while the get_cel1 does nothing with the value it receives This behaviour is also compatible with our proof rules of course by changing the footprint associated to cell to emp we reflect the fact that no ownership transfer happens and the proof goes through for the new version The proof of put_cell for instance would become In the case of a single cell and if we ignore what is happening inside the endpoint heap send and receive are similar to dispose and new 85 5 2 Examples message cell emp vale contract C initial state q 1 cell gt q final state q 1 i put cell e x e xier Y 1 9 x o1 4 send cell e x e xir e o Y 1 9 get cell f flk f X 2 q 4 local y y receive cell f y i 5 X 2 4 y gt dispose y fif X 2 9 main emp 1 local x e6 f x new x efl xe e f open C x e flrxo gt e Xxft Yx X gt Y 1 q Y gt X 2 q put_cell e x get_cel1 f x e tlre Xxf Yx X Y 1 q Y gt X 2 q close e f emp Figure 5 2 Proof of the cell transfer e xier Y C 1 q x o send cell e x fe xlker Y 1 0 x o dispose x e xlker Y 1 9 With the original footprint emp val gt this proof would not succeed as dispose x requires that x points to an allocated memory cell in its precondition
182. p Both processes are now waiting for each other to issue a signal they are deadlocked Using conditional critical regions instead of signals one can write the simpler solution depicted Figure 1 3 This solution is race and deadlock free and even avoids the race not 15 1 1 Concurrency and the heap Consumer code while true if items 0 the buffer is empty wait wait non empty x pop buffer items if items BUFFER SIZE 1 the buffer was full but is not anymore signal non full do something with x Producer code while true if items BUFFER_SIZE the buffer is full wait wait non full x produce item push buffer x items if items 1 the buffer was empty but is not anymore signal non empty Figure 1 2 A solution to the producer consumer problem using signals with a potential deadlock mentioned above between the items and items instructions that the astute reader may have noticed in Figure 1 2 Readers writers problem Before closing this section let us present another classical problem that embodies another kind of concurrency idiom the readers writers problem This problem consists in orchestrating accesses to a shared portion of state that some pro cesses the readers wish to read while others the writers wish to write To avoid races only other readers may access the shared state when it is being read and nobody can
183. p now asserts the emptiness of the stack the cell heap and the endpoint heap The semantics of all the other predicates and operators is straightforwardly adapted from Figure 4 1 their former formulation needs not be altered but state composition and com patibility is now understood in terms of well formed ideal states composition 79 5 1 Proof system 5 1 3 Rules for communication Sending and receiving actions are a means of synchronisation between processes even though sending is asynchronous there is still a temporal constraint between the sending and the receiving of the same message Thus messages can be used to transfer ownership of pieces of state between the sender and the receiver of a message similarly to how the effects of other forms of synchronisations are mirrored in separation logic From this moment on we consider that all programs are annotated by deterministic con tracts at each open instruction in the source code Thus each e f open will hence forth be of the form e f open Intuitively each channel that is opened by a pro gram must declare the protocol that will take place on it This places an implicit restriction that the contract has to be the same for each channel created at the same program point This restriction also applies to SivGf and Session Java where programs are annotated in a similar fashion Footprints Similarly to other synchronisation mechanisms as locks and resources a m
184. p is leak free from any complete state o such that o In particular if Lis admissible and p emp p emp under leak free contracts then using the above theorem and Lemma 6 13 one can show that p u skip o implies a u Note that Theorem 6 3 is true of complete programs which execute from complete states One would need another theorem for open programs for which this is not necessar ily the case for instance by keeping track of the difference between flat o and owned c This is left to future work Let us decompose the proof of Theorem 6 3 into two lemmas corresponding to the two conditions that characterise leak free programs Lemma 6 16 Leak correspondence Let o k be a ceremonious state well formed with respect to I and containing only leak free contracts and p a program decorated only with leak free contracts such that p ProtoError Then p 6 k LeakError Proof Assume the hypotheses of the lemma and suppose that p 6 k LeakError by the leaking reduction rule of close for the channel e lt Because of the premises of this reduction rule e e e dom k where 6 s h k and there are a final control state qf and words a and a such that cconf a qs qf 0 0 and either a or a u Thus ay Of Qs a is not a stable configuration which contradicts the fact that contract a lt is leak free Lemma 6 17 Comple
185. pages 35 72 74 102 112 114 Rodney M Burstall Some techniques for proving correctness of programs which alter data structures Machine Intelligence 7 1 23 50 1972 Cited on page 3 Daniel Brand and Pitro Zafiropulo On communicating finite state machines J ACM 30 2 323 342 1983 Cited on page 50 Patrick Cousot and Radhia Cousot Abstract interpretation A unified lattice model for static analysis of programs by construction or approximation of fix points In POPL pages 238 252 1977 Cited on page 5 Cristiano Calcagno Dino Distefano Peter W O Hearn and Hongseok Yang Beyond reachability Shape abstraction in the presence of pointer arithmetic In SAS volume 4134 of LNCS pages 182 203 2006 Cited on page 68 Edmund M Clarke E Allen Emerson and A Prasad Sistla Automatic veri fication of finite state concurrent systems using temporal logic specifications ACM Trans Program Lang Syst 8 2 244 263 1986 Cited on page 5 G rard C c and Alain Finkel Verification of programs with half duplex com munication Inf Comput 202 2 166 190 2005 Cited on pages 7 28 43 53 54 G rard C c Alain Finkel and S Purushothaman Iyer Unreliable channels are easier to verify than perfect channels Inf Comput 124 1 20 31 1996 Cited on page 7 Bibliography CO01 COYO7 Dod09 DOY06 DY10 FAH 06 Flo67 FM97 GBC 07 HANOS HGS09 HKP 10
186. placed with its more algebraic counterpart the guarded external choice One can encode the former using the latter For instance switch receive x receive cell f 1 dispose x e receive fin f 33 2 2 Semantics becomes x receive cell f dispose x e receive fin f skip 2 2 Semantics 2 2 1 States States consist of a stack a cell heap that contains regular cells and an endpoint heap map ping endpoints to their peers and their receive buffers We write c s h k for elements of State defined below State Stack x Heap x EHeap Stack 2 Var fin Val Heap Cell fin Val EHeap Endpoint fin Endpoint x Msgld x Val As is standard for models of separation logic we model the heap as a finite partial map written fin from locations to values The domain of the heap corresponds to the al located addresses and for simplicity is unbounded in size although only a finite number of cells may be allocated at any given point in time Alternatively one may think of the domain of the heap as the set of memory cells that are owned in the current state The novelty compared to usual models of separation logic is the endpoint heap k The separation of dynamically allocatable resources into two distinct heaps is a purely cosmetic design choice that simplifies the presentation of the semantics because each type of object has a different type of image by the heap and is used in
187. plementation They could however end up in an incoherent state in the case of a race and as discussed in the previous chapter defining an exact semantics for this kind of behaviours is challenging to say the least In this thesis our goal is to certify that no such error happens thus we make them explicit even in the semantics This makes it easier to identify unsafe starting states for a program p they are the states c such that p o gt OwnError or p o MsgError This is a standard practise in models of separation logic Bro07 COYOT that reflects its fault avoiding interpretation of Hoare triples a proved program never runs into an error state If a program p does not reduce into an error from a given state c the reduction rules give the continuation p of p and the resulting state a nor p 0 p c If p is skip the program has successfully reached a final state c An expression E is associated to a value E by an evaluation that looks up the values of the program variables mentioned in E the set of which is written var E into the stack s If E mentions a variable not in the domain of the stack then E is undefined this will be the cause of an ownership error in many cases of the semantics The value of E is 35 2 2 Semantics computed by structural induction on the expression v 3 v xls s x Ei Ez 1 s E2 s Ei Eos 1 E2 Some of these operations are undefined if one
188. predicate to describe the endpoint heap ous formulas et separation logic formulas see Figure 4 1 Ej gt E gt r q singleton endpoint heap Semantics The predicate above describes an endpoint heap where only the address cor responding to E is allocated and points to its peer E follows contract with role r and is currently in the control state q of It moreover asserts the emptiness of the cell heap The latter consequence serves no theoretical purpose as we could leave the cell heap unspeci fied while describing the endpoint heap and vice versa However both heaps are really just one heap cut in two for simplicity which is more faithfully reflected by this design choice Moreover we find that it gives rise to more concise formulas in practise Formally s h k i e E gt Eo r q iff var E E2 dom s amp dom h amp dom k Els amp k E1 s LE s r a The semantics of the regular points to predicate is changed to stress that the allocated location is not an endpoint and the predicate emp now asserts the emptiness of both the cell and the endpoint heaps s h k i e E gt Ey iff var E1 E2 dom s amp dom k amp dom h Filset h Filss LE2 sa s h k i e emp iff dom h dom k In particular the formula X gt Y X Y r q is unsatisfiable the same location cannot be both a regular cell and an endpoint The shorthand emp emp A em
189. protocol error is raised External choice and receiving a message The reduction rules that correspond to re ceiving a message via a guarded external choice are shown in Figure 6 5 There are four cases it can either succeed and proceed with one of its branches or fail either because the receive is prohibited by the protocol or because an unexpected message is present at the head of one of the inspected queues or because although no unexpected message is nec essarily present the contract stipulates that a message that is not expected by the program could be available 106 Chapter 6 Open Behaviours and Soundness Fils 2 s v k e e v q succ r q a q Ga x s h k control e q 64 y amp amp rv send a E1 E2 s h k k gt skip s h k control e lt q oa E amp k e a v 64 Fils Fo v k e e r q succ r q a q 104 04 lt s h k control e q amp da E yale e r v send a E E5 s h k k gt OwnError File e k e 8 r q 3q succ r q la q send a Ej Ez s h k k gt ProtoError Figure 6 4 Open operational semantics of send In the successful case a message identifier is present at the head of an endpoint s buffer and the corresponding branch is selected Conversely to the case of send the footprint corresponding to the message is seized and added to th
190. ract According to our informal soundness statement the proof of Figure 5 2 shows that the cell passing program is race free fault free and leak free Let us now show that the same is true of the cell and endpoint passing program first seen in Figure 1 8 Cell and endpoint passing The proof sketch of the cell and endpoint passing program is presented Figure 5 3 As it is very similar to the previous one let us only discuss the 87 5 2 Examples footprint of the fin message This footprint uses the parameter src to specify that the end point in transit is the one from which the message was sent This is a crucial element of the proof had we chosen Yin emp A val gt 1 7 as a footprint the proof of put cell would still go through since implies y but the last two lines of the proof of get_cell would give the following failed proof attempt y 2 q ee receive fin f y f eel f gt 7 2 q eer 1 q close ee f The rule CLOSE cannot be applied because at this point ee f is not guaranteed to form a channel says nothing about the origin of the message so it could point to another endpoint with the same characteristics but from a different channel not related to f Alternatively one could have given as footprint emp val dst 1 q to specify that the transmitted endpoint is the other end of the channel and the proof would go through Indeed thanks
191. ract fails one of the checks mentioned above a warning is issued to the user appro priately if a contract is either non deterministic or non positional then Heap Hop warns that it cannot prove that programs are either leak free or fault free if a contract is not syn chronising Heap Hop warns that programs cannot be proved leak free The incriminated contract and control states are indicated to the user as part of the warn ing All warnings and errors in Heap Hop are output using a standard format to indicate the line number where the abnormality is For instance in the case of a non synchronising contract Heap Hop s output would be of the following form File non synch contract hop line 13 characters 0 125 WARNING contract C is not synchronizing there is a send cycle starting at state start WARNING program cannot be guaranteed leak free because of contract C This formatting is recognised by the emacs text editor for instance which allows the user to click on the warning to be directed to the relevant file and line Moreover contracts are also output as dot files so that the user can have a graphical representation of them 7 3 2 Hoare triple verification Once the contracts have been checked Heap Hop tries to prove that the specifications of the functions are true using the process described in Section 7 2 If it fails to prove that a certain specification or loop invariant holds it can be for one of two reasons which bo
192. rametrised inter 63 3 3 Contracts actions YDBH10 In particular Deni lou and Yoshida recently provided an analysis of multiparty communications that can among other things compute a bound on the size of the channels of a pi calculus process DY 10 whereas we analyse each bi directional channel separately Extending contracts to the multiparty case is certainly an interesting perspec tive as it would enable us to take into account causality information given by all channels at once and thus to perform a more accurate analysis 64 CHAPTER 4 Concurrent Separation Logics This chapter recalls the formalism of separation logic applied to the study of concurrent heap manipulating programs 4 1 Assertions 4 1 1 Models The typical domain of application of separation logic is the proof of heap manipulating programs Rey02 O H07 GBC 07 Vaf07 and as such the models of its assertions are often taken to be a stack and a heap Let us consider the following set of states State and recall the definition of Stack and Heap from Chapter 2 State Stack x Heap Stack 2 Var fin Val Heap Loc i Val The composition of two states 01 s1 h1 and o 52 ha is defined only when the domains of the two stacks and the domains of the two heaps are disjoint When this is the case we write c1 72 and the composition c e 0 is defined as 01 02 51 y 52 h y ha where the disjoint union of two partial functions f and
193. ration a a 0 0 is reached the buffers are empty This would show that if the program terminates then the whole tree has been properly disposed of If we replace disposal with some other operation on nodes this shows that the load balancing program treats all the nodes The proof system would not ensure that it terminates or that the tasks are balanced between the two threads 141 Conclusion Contributions Let us begin this conclusion by a summary of the contributions contained in this manuscript Firstly a formal semantics has been given to a message passing pro gramming language that is heavily inspired by the Sing language of the Singularity project This formalisation is an attempt both at giving a sound bedding to the ideas introduced in Singularity and at studying copyless message passing in all generality This effort is pursued on the protocol specifications of Singularity the contracts for which we also provide a for mal semantics in terms of the existing model of communicating automata Various decid ability questions are studied from which one may draw the conclusion that the constrained syntactic form of contracts gives them no theoretical advantage over the more general class of half duplex dialogue systems Nevertheless their practical usefulness as demonstrated by the Singularity project promotes them as the language of protocol specifications for our own logic Indeed we define an original extension of separation lo
194. ration logic to claim that automating the verification of programs in concurrent separation logic would likely result in progress in the automation of verification in our own setting There is however room for an additional sort of automation instead of specifying the protocols followed by the program one could wish to automate this process and infer contracts from a given program This process is likely to bear similarities to the inference of session types given a pi calculus process From the point of view of the asserter who has to verify existing programs that may not have been written with certification in mind it is crucial that formal tools only require a minimal amount of work from his part for instance annotating the parts of a program that a tool fails to verify 145 Conclusion Towards certified concurrent programming Writing correct concurrent programs has always contained a part of challenge for the programmer who must avoid the many pits of race conditions deadlocks and more generally must see to it that programs cooperate good manneredly instead of stepping on each other s toes One could hope to see programming languages rise that make this task easier by providing a strong formal bedding to the pro gramming constructs such that formal verification becomes possible even to non experts in the field Tools towards this end may include contracts for channel communications or explicit ownership tracking of resources by the l
195. ravers e de la th se Am lie M Arnaud D Arnaud S Delphine L Giinther S Juliette S Miles A Mouchy Philippe P Sylvain S j en passe et pas des pires Je remercie enfin Jade mes parents et ma famille pour tout ce qu ils m ont apport ix Introduction Modelling and verification of message passing programs The formal verification of programs strives to ensure with the certainty of a mathematical theorem that programs do what they were conceived to do Programs do not always behave as desired as one may experience in its everyday interactions with computers sometimes they crash or produce unexpected results What is a mere annoyance on a home computer can have dramatic consequences for more sensitive programs For instance in 1996 the Ariane 5 spatial rocket exploded in the atmosphere due to an integer overflow present in its code Despite careful examination by engineers the anomaly went undetected whereas formal methods could have been applied to prevent it Formal methods allow one to go beyond naive testing of programs Indeed tracking errors down by means of testing involves making sure that a program will behave correctly whatever its input Unfortunately the number of situations that a program can run into is most of the time virtually infinite Thus empirically testing the conformance of a program against a certain specification by running it against each possible configuration of the system cannot be
196. rbage collection this kind of error should also be eliminated In Singularity where the memory is garbage collected nothing is done to guard against these programs Copyless communications Finally one can wonder whether or not communicating in a copyless fashion introduces races or memory faults as we have already seen in the examples that were presented 1 2 5 Encoding locks and message passing into one another Shared memory and message passing are in all generality equally expressive one can transform any program using one of the two paradigms into an equivalent program using the other one Locks can of course encode message passing this is how message passing would be implemented in practise Let us discuss here the other way around One way to simulate locks using our programming language is by using one central lock ing authority per lock identifier by whom the other threads will be granted locks Each 28 Chapter 1 Concurrency and Ownership thread holds a different endpoint to each of the locks authorities Lock identifiers are thus replaced by endpoints to the relevant authority A thread can acquire a lock by sending an acq message to the central authority and then waiting for an ack message The lock is released by a rel message This gives the following pattern assuming that e is an endpoint through which the thread can communicate with the central authority send acq e 1 receive ack e Critical section her
197. re proving this claim let us show that we cannot say the same of non deterministic or non positional contracts For instance the following non deterministic contract is not fault free The first machine can send a then b while the dual one receives a and then tries to receive b whereas b is available Non positional contracts also embed a form of choice that can harm the safety properties since in a non positional state both machines may make dissonant moves 56 Chapter 3 Dialogue systems In the example above the first machine may send a then wait for b while the second one sends b and then wrongfully tries to receive a whereas a is available Lemma 3 6 Fault freedom For every contract if is deterministic and positional then is fault free Proof If is deterministic and positional it is half duplex Lemma 3 4 From Lemma 3 2 all executions are equivalent to a 1 bounded execution of the system fol lowed by a sending only phase If a fault occurs it must be during the first phase Dur ing this phase reachable states are of the form q q u u Lemma 3 3 q q a with q a q T or symmetrically q q u a with q a q T In the first case queues are empty so there can be no fault In the second and third case the machine that did not perform the send is obviously about to receive a since its dual was able to send it from the same state so there is no possible fault eit
198. ression that someone else may own them which could hide some leaks We will show in Section 6 4 4 that one may avoid these pathological cycles of ownership by considering only admissible footprints for which they are impossible For the formal definition we follow the terminology Gotsman ef al Definition 5 1 Admissible footprint context A footprint context T aj y1 dn Yn is admissible if it is well formed and if for all interpretations 1 there do not exist e a non empty finite set AC a1 an x Endpoint x Val A bi ei vi ie I for some finite I IN e endpoints e and roles r for each e and a state s h k such that s h k Gier Yo Ei El ri Vi such that for all i I e e dom k and k e ei 3 ri Informally a footprint context is admissible if it is impossible to send a certain number of messages that form a set A of tuples a e v where a is a tag in the domain of I e the source endpoint and v the value of the message whose footprints hold permissions on all the buffers wherein they will be stored the queues of the peers of all the source endpoints of A Indeed if the footprints hold such permissions then the program cannot rightfully receive any of the messages of A hence their contents are leaked from an ownership point of view and possibly unreachable for instance if one of the queues also contains a location that is not referenced from anywhere else which makes th
199. rogram equivalence A program p denotes a partial function p State f Stateu OwnError MsgError PI o gt o p o skip o w error p o error Two programs p and q are equivalent written p q if p q Note that we only take into account final configurations skip c and errors in this defini tion The following lemma groups together some typical equivalences between programs Lemma 2 2 For all programs p pi po and ps the following equivalences hold m p2 p3 p p2 p3 p p2 pa p skip p p p pa p3 p p2 pa p p2 p2 p p p p pi po P3 pi P2 pa skip p p Proof Straightforward by induction on the structure of the programs involved 42 CHAPTER 3 Dialogue systems Communicating finite state machines CFSM for short are a widely studied model of com municating systems and protocols in general Dialogue systems are communicating systems consisting of two CFSMs communicating over a bi directional FIFO channel modelled by two buffers They can be used to specify the protocols followed by the communication chan nels of a message passing program as defined in the previous chapter In all generality the buffers may be bounded or unbounded perfect or lossy We confine our study to unbounded perfect buffers for the reasons detailed in Section 1 2 3 Channel contracts are a special case of dialogue systems They have been used to specify all t
200. rograms are shown to respect ownership of resources to abide by their contracts and thus to communi cate in a safe way if their contracts so guarantee Chapter 7 This chapter presents our automatic proof tool Heap Hop Table of notations The notations used throughout the thesis are grouped in Table 0 1 Introduction Symbol Denotation empty set IN the set of natural numbers Z the set of integers 1 9 n m integers w word a B buffer contents u empty word or queue x y e f variables E program or logical expression B boolean program expression c command g guarded external choice p program v value e endpoint address o closed program state S stack h cell heap k closed endpoint heap M CFSM G system of CFSMs contract D dialogue system q control state of a CFSM C configuration of a CFSM a b c cell fin S 19 nM o message identifiers idealised local state idealised endpoint heap formulas invariant or footprint footprint context open state open endpoint heap Table 0 1 Notation used in the typescript CHAPTER 1 Concurrency and Ownership 1 1 Concurrency and the heap 1 1 1 Concurrent programs A concurrent program can be described by a collection of processes or threads executing simultaneously Each process consists of a sequence of instructions and simultaneity is meant in a loose way it may occur for a number of re
201. roof The dialogue system endcat ENdsim Meat Msim has all the properties that the theorem asks for 3 2 2 A decidable class half duplex systems A system is half duplex or has the half duplex property if there may never be more than one non empty buffer atthe same time in any of the executions A classical physical example is the one of a group of persons communicating via walkie talkies there are never two persons speaking at the same time Definition 3 21 Half duplex system A system is half duplex if for all reachable config uration qi qn W1 Wp there is at most one 1 p such that wi u Half duplex systems are known to have a regular reachability set CF05 in particular C c and Finkel have shown that all the safety problems we are interested in are decidable in polynomial time on the size of the alphabet and the number of control states of each individual machine on half duplex dialogue systems and that the half duplex property itself is decidable in polynomial time Intuitively every execution Co E C of a half duplex dialogue system can be turned into another execution Cp C4 A C2 that ends in the same configuration such that the run Co A C1 is 1 bounded C is stable its buffers are empty see Definition 3 13 and Ci C consists only of send actions by one of the two machines This sequence of sending actions is performed by a finite state machine thus it can be described by a re
202. rue i 1 ensures that the program has enough resources not to reduce to OwnError in one step The second one ai ie 1 n a Bd succ r q a q prevents both the second and the last of the four reduction rules of receive to apply hence p o ProtoError Let us assume that p o MsgError Then there is 2 such that p a gt pi Ls xi v h k eontrol e q i k es a Let us write c for the resulting open state Since o Statef 6 e Ya Y Y 3 r Z for some Z such that i Z v Hence oe iEexi ZA Y 9 Y r q x px Ya Y Y 3 r Z By induction hypothesis and since we know from the premises of CHANNELDISPATCH that er xi ZA Y gt Y r g Ya Y Y 3 r 2 pi 4 we can deduce that pj a OwnError pj 0 4 ProtoError and if piga skip o then o i v Hence p o 7 OwnError p o p ProtoError and if p o skip g then 07 1 Y ExtCuoice This rule is sound by a straightforward generalisation of the previous argument to multiple endpoints 117 6 4 Properties of proved programs SEQUENCE Straightforward PARALLEL Straightforward from Lemma 6 6 CHOICE STAR LocaL Straightforward FRAME Recall that for all program p p p skip Lemma 2 2 This is also true in the open semantics p o skip o if and only if p skip o skip o and p error if and only if p skip o error By applying the p
203. s 6 3 2 Soundness Before defining what it means semantically for a program to satisfy a specification given as a Hoare triple we need to define what it means for an open state to satisfy a formula of our logic Definition 6 7 Formula satisfaction for open states An open state o satisfies a formula written E Q if its local part does k k iepirkiiro Let us remark that formula satisfaction is stable under interferences from the environment Lemma 6 7 For all 9 0 Statef all formula and all valuation if o i e and o gt a theno ir Q Proof Immediate using the definitions of satisfaction and interferences the latter cannot change the local state of c which is the only part of the state that is used to determine whether or not g i E holds Definition 6 8 Validity A triple is valid with respect to a footprint context I written er 9 p v if for all logical stack i and all state o Statef if a i then the following properties hold 1 p a OwnError 2 p o ProtoError 3 if p 0 skip o then a i v Theorem 6 1 Soundness f r 0 p v then er 9 p v Proof We prove this theorem by induction on the structure of the proof of 0 p v Suppose first that it is one of the axioms of the proof system see Figures 4 4 and 5 1 We proceed by case analysis Let o s h k k e AsSUME Suppose that a i var B lr emp If follows that dom s var
204. s sage passing In APLAS volume 5904 of LNCS pages 194 209 2009 Cited on pages 6 97 98 99 Jules Villard tienne Lozes and Cristiano Calcagno Tracking heaps that hop with Heap Hop In TACAS volume 6015 of LNCS pages 275 279 2010 Cited on page 6 Viktor Vafeiadis and Matthew J Parkinson A marriage of rely guarantee and separation logic In CONCUR volume 4703 of LNCS pages 256 271 2007 Cited on pages 7 15 102 Nobuko Yoshida Pierre Malo Deni lou Andi Bejleri and Raymond Hu Pa rameterised multiparty session types In FOSSACS volume 6014 of LNCS pages 128 145 2010 Cited on page 64
205. s done by induction on the size of dom k x dom k If itis O then owned o 6 and k emp k thus flat o owned o emp k If dom k dom k E let oy flat k dom k and k emp k dom k w k dom k dom k We have owned c owned s h k e p k by defini tion Suppose that the lemma holds for all strict subsets of E In particular it is true for 123 6 4 Properties of proved programs owned s h k Ok k either dx contains some endpoints and the induction hypothe sis applies or it does not and then dom k dom k which contradicts E Thus flat c owned s h k e 6x k owned c Leak freedom for complete programs If the footprint context is admissible and the contracts are all leak free completeness of states is preserved by reduction This is not the case if T is not admissible or if the contracts are not leak free In the first case cycles of ownership may render unreachable the corresponding endpoints and the footprints con tained in their queues In the second case closing a channel may leak the footprints of the messages that were left in its buffers and not consumed This is captured by the following definition and theorem Definition 6 13 Leak free program A program p is leak free from a complete state o if e p o LeakError and eifp o gt p o then a is complete Theorem 6 3 fT is admissible and Fr 6 p v under leak free contracts then
206. s drift away from programming languages to concentrate on communicating automata and are thus more comparable to the analysis that Heap Hop performs on contracts They are more involved in that respect as they focus on semantic properties of systems whereas Heap Hop merely perform syntactic checks on contracts from which one can deduce the semantic properties of their behaviour Introduction Outline The outline of the rest of the manuscript is as follows Chapter 1 This chapter informally motivates the design choices of our message passing programming language and presents the main verification questions that this thesis will address Chapter 2 This chapter gives a formal syntax and operational semantics to our copyless message passing programming language Chapter 3 In this chapter the focus is on the semantics and properties of contracts Since some aspects of the verification of programs boil down to checking properties of their associated contracts as we show in the following chapters the decidability of various contract properties is investigated Chapter 4 This background chapter presents existing concurrent separation logics Chapter 5 In this chapter we introduce our extension of separation logic to copyless mes sage passing and discuss how to prove a few key examples Chapter 6 This technical chapter presents a second open semantics for our programming language and produces the soundness proof for our logic proved p
207. s example are deterministic positional and synchronising By Corollary 3 1 they are fault and leak free hence as we will see in the next chapter the pro gram itself is race fault and leak free One can give a session type for this program as did Honda et al in the aforementioned paper THK94 which would prove that it is fault free 5 3 Restrictions of the proof system 5 3 1 Deterministic contracts In this chapter as we have already pointed out the protocols have to be expressible using deterministic contracts Were we to allow non deterministic contracts in our analysis we would need the logic to keep track of the set of control states in which an endpoint might be in order to soundly account for non determinism instead of a single control state For instance an endpoint pointed to by x with mate X starting in state go of the contract la la es w could be in either one of the states gg or q after sending a hence would be best described by x gt X 1 q0 q1 As they have been described the proof rules would allow one to prove for a program p that sends a over x the triple x Er X 1 90 p x ES x 1 q1 whereas the semantics of p defined in the next chapter could choose to place x in the control state gg which even without a formal soundness statement in mind contradicts this post condition Modifying the proof rules of communications to handle sets of control states instead of singleton
208. s is quite straightforward one only has to extend succ to operate on sets of control states The definition of this new operation succ becomes succ r Q T Q iff Yg Q 3q Q succ r q 7 aq For instance in the contract above succ 1 qo la qo q1 succ 1 qo q1 la The proof rules for open and close are modified in the following way OPEN creates end points in the singleton set of states init and CLose requires that if the two endpoints are in the sets of possible control states Q4 and Q respectively and they follow contract with appropriate roles then Q1 N Q n finals is not empty 92 Chapter 5 Proving Copyless Message Passing 5 3 2 Precision of message footprints If footprints are not precise formulas a variation of Reynolds original counter example described page 73 can be replayed We have to devise a program p such that the triple one v emp p emp is provable Let us take T a true and be the following contract cell ao cell The following proof sketch can be formally derived using our proof system recall that one emp 10 eir e gt 1 0 one v emp receive a e elker 7 1 q1 one v emp true eic e o 7 1 g1 true send a e elke 1 qo This can obviously be used in lieu of the previous CCR example to produce a proof of elk et 1 qo one v emp
209. s more than contracts in practise For instance all the com munication protocols of the Singularity project which forms a fully functional operating system have been expressed using contracts Hence our logic defined in Chapter 5 and our tool described in Chapter 7 use contracts instead of general dialogue systems Session types Session types THK94 are a type system for a variant of the pi calculus where the types themselves may be seen as a kind of communicating system with primitives for sending and receiving messages of a certain type branching according to a message tag and recursion In their structure session types and contracts are very similar One difference is that while contracts only specify the sequence of message tags that occur on a channel session types describe both the sequence of messages and the type of these messages In a way they combine into one object both the contracts and the footprints of messages that we will introduce in Chapter 5 and use to specify the type of our messages Another difference is that the final state of a session types is always a state from which no communication can occur Although this may seem mundane at first this means that session types need not care about leak freedom every possible final state is automatically synchronising It is worth noting that session types have been extended to the multiparty case with an arbitrary number of participants instead of two HYC08 and even to pa
210. sage Passing e SE commands et see Figure 2 1 e openO channel creation close E E channel destruction send a E E labelled message sending p programs see Figure 2 1 g guarded external choice g guarded external choice x receive a E p guarded program g1 092 external choice Figure 2 2 Syntax of HipMP a e Msgld and e f Var programs in the following way pus programs see Figure 2 1 resource r in p resource declaration with r when B p CCR Once a resource has been declared it can be used to create conditional critical regions which will only execute if no CCR using the same resource is currently executing and if some boolean condition is satisfied The boolean condition can be omitted B true in the grammar above in which case we can simply write with r p 2 1 2 HiPMP Let us extend H r with message passing primitives and call the resulting language HiPMP We assume two extra countably infinite sets Msgld and Endpoint of respectively message identifiers ranged over by a and endpoint locations ranged over by e The two sets are disjoint and disjoint from previously defined sets with the exception of Val Although Msgld n Val endpoint locations are added as possible values Endpoint Val More over as for regular memory cells 0 Endpoint The syntax of HiPMP is given in Fig ure 2 2 The switch receive construct described in the previous chapter is re
211. set of variables x that appear in p outside of the scope of a local x in p construct For simplicity the local construct is treated as a statically scoped allocation and deal location of a fresh variable on the stack For this purpose a delete statement is appended at the end of the program that deallocates the local variable Since it only occurs in such instances the variable will always be allocated when delete is called hence we need not specify it as a requirement in the semantics The delete command is not part of the pro gramming language in particular it cannot be used by the programmer it is only an artifact of the semantics The semantics of a parallel composition p pa is all the possible interleavings of the actions of p and p possibly resulting in a fault if there is a race between the two programs The purpose of the predicate norace pi po 0 is to detect such races it checks if there is an immediate race between p and p that is if p and pa are both about to access to the same resource and one of them is trying to write to it Here a resource may be a stack variable a memory location or an endpoint of a channel Given a program p and a state c we define the sets iw p o and ir p o of resources that are respectively immediately written to and read by p in the state c Immediately means that said resources will be accessed by the program at the very next step of its execution according to the operational semant
212. sion guarantee This quote also highlights the idea that the separation has no operational meaning it is enforced by the Sing compiler so that runtime checks for separation or process isolation in their own words are not needed 1 1 5 Memories Explicit deallocation When considering memory manipulating languages two choices are possible with respect to how memory is deallocated This task can either be performed explicitly by the programmer or be delegated to a garbage collector that periodically frees unused memory Correctly disposing of unused memory cell is important for the well being of a system Indeed and although for simplicity we will model it as infinite in capacity memory is a limited resource Thus constantly allocating new cells that are never freed can exhaust this resource Failure to dispose of unused memory cells results in memory leaks In many programming languages memory leaks are not a concern because deallocation is handled implicitly by a garbage collector To give a few examples this is the case for OCAML Java Cf and most scripting languages like PERL and PYTHON On the other hand explicit deallocation is present in many so called low level program ming languages like C C and assembly languages It is a desirable feature if memory is scarce for instance in embedded systems or for memory intensive applications wherein the usage of memory should be optimised or finally for software that cannot bear the cos
213. specifying and verifying user level code we assume that the underlying operating system is sufficiently well behaved that we can safely elude these details 11 1 1 Concurrency and the heap 1 1 2 Race free programs A race condition occurs whenever there are at least two simultaneous accesses to a shared resource that are not protected by any synchronisation primitive such as a lock and at least one of them is a write A program whose executions may exhibit a race condition is called racy and race free otherwise More precisely two threads or processes are in a race condition if they simultaneously try to access the same resource and if at least one of them is trying to write to the resource This is most of the time considered as an error Indeed the outcome of races is not deterministic as it may not even correspond to one of the outcomes produced by interleaving the instructions of the two culprit processes This makes them very hard to detect and reproduce using traditional debugging tools This also complicates considerably the definition of the semantics of programs in particular the semantics of the parallel composition of two programs becomes unclear in the presence of races Racy programs Races often result in undesirable behaviours for instance reading an incoherent value because another thread is writing to it or eventually storing a scrambled value because of two simultaneous writes to a resource this can happen when wri
214. stance have one endpoint on the sending side but several on the receiving one This poses interesting theoretical challenges as well for instance when a message is simultaneously received by all its recipients how the corresponding footprint would be distributed amongst them and how to include this mechanism in a proof system is not obvious One can also wonder whether the concepts presented in this thesis apply to other existing message passing paradigms for instance to Posix pipes or to the ERLANG programming language or even simply to programs that implement a form a message passing simply by sharing buffers between threads without higher level language constructs Independently from message passing concerns the language itself could be more full fledged and support realistic programming constructs such as function calls which Heap Hop already support arrays or more general data structures In particular adding a support for arrays in Heap Hop would enable us to try and verify several message passing examples from the domain of intensive computing where arrays and matrices are often passed around between processes Automation Trying and automating the verification of message passing programs to the extent of minimal to non existent user interaction is a natural extension of our work on Heap Hop We believe that we have given to our message passing primitives a logical status close enough to the ones of other synchronisations in sepa
215. surd Consider any of the recipient endpoints for instance the first one 1 Because dom k is also in the domain of 6 for some i J and i E Yo i Ej ri Vi A amp ph eie true 96 Chapter 5 Proving Copyless Message Passing By hypothesis of the lemma it follows that dit h Ei E Ti Vi ei Eos Ti n true i Thus k e hule ri Since r r ri k e1 r1 Since moreover k amp 1 3 r1 we obtain a contradiction r 3 11 We found that this criterion is sufficient in practise as we have never needed more so phisticated ones in our case studies It is easier to check be it automatically on certain fragments or by hand than the general criterion It may be worth noting that the SING language also imposes an admissibility condition on the endpoints that may be sent over channels they may only be endpoints that are currently in a sending state of their contract Although this constraint arises in their setting because of garbage collection considerations we think that such a condition translated into a constraint over footprints may also be sufficient but not necessary to ensure admissibility 5 3 5 A first soundness result Abstract separation logic There are numerous variants of separation logics The goal of abstract separation logic developed by Calcagno O Hearn and Yang COY07 is to iso late the crucial pr
216. t of having a garbage collector running in the background for performance reasons Correct handling of explicit deallocation is also a crucial concern in cryptography where sensitive data residing in clear text in memory cannot be handed back to the operating system by a mere deallocation Otherwise an attacker might be given the same memory cells by the memory manager and read the secrets Instead extra cleanup is required every time such a resource is to be deallocated which forbids the use of a traditional garbage collector at least for these resources In this work we use a non garbage collected language thus we are also interested in proving the absence of memory leaks Furthermore we claim that our techniques can be adapted to handle garbage collected languages This hope is backed by the fact that sepa ration logic on which our own analysis is based has been successfully adapted to handle garbage collection in the past COO1 Ownership tracking The presence of the heap complicates the bookkeeping of what be longs to whom for programs that only manipulate variables it is easy to state that two pro grams operate on disjoint portions of the state one simply has to check that they use differ ent variable identifiers This is not possible anymore for memory manipulating programs because of aliasing two syntactically distinct variables may point to the same location in memory during the execution This problem has crippled the verifi
217. t free or the part of the proof that has failed A failed proof means that the specifications given by the user do not hold hence one cannot know if the program has a genuine bug or if the specifications could be refined to a point where they are true A proved program on the other hand is guaranteed to have all the good properties corresponding to the ones described in the last section of the previous chapter We first present Heap Hop s general modus operandi and then its public distribution which includes the case studies Heap Hop has been applied to 7 1 Input Heap Hop takes as input programs annotated with pre and post conditions for functions loop invariants message footprints and contracts More precisely Heap Hop s inputs are plain text files that can contain declarations for message identifiers contracts and functions The annotations are formulas of a fragment of our logic placed between brackets and written in plain text The contents of such a file containing the declarations necessary to prove the cell passing example of Figures 1 6 and 5 2 is reproduced Figure 7 1 This file is part of the Heap Hop distribution see Section 7 4 as examples cell hop The notations will be explained shortly 7 1 1 Programming language The programming language used by Heap Hop is a more practical version of the HirMP language named Hop Its syntax is shown in Figure 7 2 Hop supports records and field accesses if then else whi
218. tan SB09 The definition above corresponds to the fixed version Bounded contracts As mentioned above if we are more restrictive and assume that all the cycles of the contract contain at least one send and one receive then the contract is bounded Lemma 3 9 Boundedness For every contract if is deterministic positional and all its states are synchronising then is bounded The bound is moreover computable in linear time in the number of transitions in the contract Proof Let us assume without loss of generality that is a trimmed contract and show that the maximum size of the buffers in a run of the contract corresponds exactly to the maximum number of consecutive sending transitions of or to the maximum number of consecutive receiving transitions of whichever is the greatest Since all the control states of are synchronising both numbers are finite Let us write N for their maximum 59 3 3 Contracts Let us show that this bound is reached N corresponds to a sequence from a control state q of IN By Lemma 3 5 q q u u isa reachable configuration of the system as la la sociated to If N corresponds to a sequence of sending transitions q pS q then 4 q a1 aN u is reachable Symmetrically if N corresponds to a sequence pk e a1 an f of receiving transitions q gt gt q then q q u a1 a y is reachable Suppose now that a configuration q1 q2 w
219. te formed by the concatenation of the footprints in o where is the iterated version of the composition e of session states defined in the previous chapter fat a Ga a v 6a ea This represents the total amount of state that is stored inside a buffer We overload this function to concatenate the flattenings of all the buffers of a flattable open endpoint heap k flat k 2 flat k e eedom k Finally let us define the flattening of a flattable open state one whose open endpoint heap is flattable and compatible with its local state Flattening applies to an open state by tacking the flattenings of its buffers onto its local state Definition 6 2 Flattening of an open state The flattening of a flattable open state o k is defined as flat o k oe flat k We can now define the set State of well formed open states Definition 6 3 State An open state o 6 k is well formed if it is flattable flat o sp hg kp and the following conditions are satisfied dom ky dom k OBuffers Ve e dom ky mate kr e e dom k OChannel The conditions OBuffers and OChannel ensure that every endpoint allocated in any of the session states that appear in the open state c is associated with a buffer in k and so is its peer The other well formedness conditions imposed on closed and session states are already ensured by the fact that flat c is flattable see Lemma 6 8 for more details 103 6 2
220. teness preservation Leto Statef and suppose that all the con tracts appearing in p and are leak free and that T is admissible If o is complete then for all p and a such that pod D 0 p 8 the open state a is complete 124 Chapter 6 Open Behaviours and Soundness Proof The proof is done by case analysis on the reduction rule The case of close is proved with the help of Lemma 6 16 and the case of send by the fact that I is admissible Let us detail the second case Let g s h k k and o s h k k Cs h k control e q 64 k k e a v 64 Assume that c is not complete The difference between dom k and dom k can only come from endpoints in Gq which means that a f owned o By definition of owned one can deduce that e dom Kk otherwise the contents of its buffer in particular a would also appear in owned a Let Ga Sa ha ka and cycle sc he ke s hip k e owned o where flat o sf hy ky We have Ga lt O cycle This shows that either e appears in dom k or that there is e such that e is owned by the buffer of e and e e dom ka or more generally that there are En such that e e dom ke for all i and O cycle flat k 1 e e flat k en Thus 6 cycle E Dier Yo El Ei ri Vi where I the set of messages in the buffers of the various and koles el 3 ri for all 1
221. tes are not atomic for instance when writing a 64 bit long word to a memory where the writing unit is 32 bit Worse is the case of weak memory models in which the semantics of racy programs depend on the architecture to determine the exact outcome of a race it could be necessary to model the effect of all caches store buffers and other abstruse features of such architectures Thus races violate the atomicity of accesses to a resource one cannot assume in a racy execution that accesses to a resource respect a certain order From a higher level perspective for instance in object oriented programing where re sources may be objects composed of several memory blocks and methods to operate on them atomicity violations may put a resource in an incoherent internal state Usually each process assumes the shared resource to be in a certain state to respect a certain invariant and it could be the case that one process reads the contents of the resource while it is being manipulated by a second process that has temporarily put the resource into an inconsistent internal state Another case of erroneous racy execution occurs when the flow of a program is inter rupted by another program in a piece of code that was meant to be executed atomically by the programmer but was left unprotected Consider the program of Figure 1 1 where two non atomic increments of a shared variable x are performed in parallel and result in a race At the end of the executio
222. th result in an error pointing to the offensive line of code being issued either the symbolic execution is stuck at a particular command because the current precondition does not match the one of the command which means that the command cannot safely execute that is there is a possible memory fault or race at that program point or the result of the symbolic execution fails to entail the required post condition which means that the specification or loop invariant given by the user does not hold In either case the error is reported to the user with the current formula obtained by the symbolic execution and the location in the program where Heap Hop was stuck If extchoice detects a missing branch in a switch receive a mere warning is issued given the incomplete ness of relying on contracts to detect communication errors In practise however only one http www graphviz org Documentation php 137 7 4 Distribution of our case studies exposes such a warning despite being correct one of our solutions to the load balancing tree disposal problem exposed in Section 7 4 2 below which can be found in the file examples spawning_threads_tree_disposal hop 7 4 Distribution 7 4 1 Public distribution License Heap Hop is released under the Q Public License version 1 0 which can be found on Trolltech s website In particular its source code is publicly available and may be changed by anyone provided that the chang
223. the rest of the control states Any non trimmed contract may be turned into a trimmed one with the same operational meaning simply by deleting those states Lemma 3 5 For every deterministic trimmed contract is half duplex if and only if it is positional Proof The reverse implication is already proved by Lemma 3 4 Let us prove the direct implication Let us notice first that in the dialogue system associated to a trimmed contract 2 0 40 F T q q u u is always reachable Indeed q Q is reachable in the ori ented graph formed using Q as vertices and T as edges so there is a sequence of transitions qo 1 d1 4n 1 7n q from qo to q The following execution is thus valid where 7 7 for sending actions and 7 7 for receiving ones T Ti T T do Go 51 SS q1 qi ut Quis Mets gt gt q Yuu Suppose that is not positional There is q Q and ay a2 q and q2 such that q la1 q1 q a2 q2 T Since q 4 is reachable the following execution is valid 1 2 qo q0 u u gt q qu u q q 01 A q q2 Q1 a2 This execution is not half duplex Even trimmed half duplex contracts are not necessarily deterministic For instance the following contracts are not deterministic but half duplex nonetheless Fault free contracts Deterministic and positional contracts have more properties than just being half duplex they are fault and deadlock free Befo
224. they are not satisfied From a syntactic point of view each state of a contract is introduced separately with the state keyword which may be preceded by initial or final A state declaration 129 7 1 Input E s logical expressions _x logical variable x program variable n integer E E Exor E arithmetic operations q1 3qn set of control states p u t1 Ej tn E record expressions gous pure formulas E E boolean expression true true false false emp empty heap Erp allocated location list E1 E2 linked list segment tree E binary tree D D separating conjunction if B then else y precise disjunction Figure 7 3 Syntax of Heap Hop assertions consists of a set of transitions starting from this state Similarly to Singularity one can declare a sequence of transitions in one go and Heap Hop will create appropriately named implicit states For instance the contract declared with contract CellAck 4 initial state start cell gt ack gt end final state end 1 cell ack will be understood by Heap Hop as end 7 1 3 Logical fragment The formulas manipulated by Heap Hop are all within a decidable fragment of separation logic This fragment is described Figure 7 3 It is essentially the one used by Small foot BCO05a extended with assertions for endpoints This logic differs from the one defined in Chapter 5 on several points It is a restricted version of it in most respects but also goes b
225. tion law e defined as the disjoint union w of each of the components of the states provided that the resulting state is well formed sh k e s h k sws heh kw k When e a is defined we write 6 a Given two states amp and 6 6 lt 6 and are defined as usual remark that if there exists 9 such that cea a then 6 is unique The empty state is denoted by Session states form a partial commutative monoid To prove this we will need the following lemma Lemma 5 1 If lt and a is well formed then so is 6 78 Chapter 5 Proving Copyless Message Passing Proof Immediate by reductio ad absurdum and a case analysis on the well formedness condition that fails to satisfy Lemma 5 2 State e is a partial commutative monoid with unit Proof We have to show that State is stable by e and that e is associative commutative and admits as unit The only delicate point is the proof of associativity Let us first remark that if we drop the well formedness constraint then associativity is immediate This shows in particular that if 71 e 62e63 and 01 e 02 e03 are both defined then they are equal What is left to prove is that if 92 f 03 and 6 0 e 03 then 01 02 and 01 e 02 03 this is a consequence of the previous lemma 5 1 2 Assertions Syntax We extend the assertion language of separation logic of Figure 4 1 with the fol lowing
226. tion nla is n a Given an action T we write T for its dual The dual of a set of transitions T is T 2 7 r T The dual of a CFSM M B Q qo T is dual IO B Q qo T Note that the dual operation is involutive 7 7 hence dual dual M M The following definition formalises the channel contracts of Singularity FAH 06 without re strictions yet see Definition 3 25 Note that the set of final states is specified within the contract Definition 3 8 Contract A contract is a tuple 3 Q qo F T where T Q x x gt x Q A contract is not a communicating system per se but it is associated to a canonical one 46 Chapter 3 Dialogue systems Definition 3 9 Let be a contract 2 Q qo F T The communicating machine asso ciated to is Me X 1 2 Q qo q 12a q 2 a q e Tju a 2 a q q la q TH To the contract we associate the following dialogue system De De q a a F Me dual Me For instance consider the contract with final state end depicted by a double frame lfin end This contract denotes the following dialogue system with final state end end The properties of dialogue systems are extended to contracts in the obvious manner For instance a contract is deterministic if the dialogue system that it denotes is The dual dual of a contract is also defined in a straightforward m
227. to the LInjective axiom val dst 1 9 val gt 1 q A val src Sending a list cell by cell The proof of the copyless cell by cell list sending program sketched in Figure 5 4 uses the same message footprints but a protocol based on a slightly different contract that accounts for the a priori unbounded number of cells that can be sent over the channel The proof is quite straightforward We use brackets in while constructs to specify their loops invariants A new kind of possible error that this program could have is to omit one of the branches of the switch receive for instance the branch corresponding to the final message fin This would cause the program to block or fail depending on the semantics one gives to unspeci fied receptions when put list sends its endpoint at the last step unable to receive the fin message present in the buffer The proof system would detect this problem because the con tract states that two messages may be received from state q cell and fin hence the program should not attempt to receive only one of them 5 2 2 Automatic teller machine Figure 5 5 presents the proof of a simplistic automatic teller machine ATM that exhibits more complex communication patterns This example is taken from one of the first papers on session types Language primitives and type discipline for structured communication based programming by Honda ef al THK94 The functioning of the ATM is stripped d
228. tool lacks support for contracts and different message tags As a result each channel may only be used to transport one particular type of value whereas channels in our model may carry different types according to the current protocol state of the channel On the other hand Chalice is capable of analysing communications so as to prevent deadlocks LMS10 which Heap Hop does not not currently support Similarly the Session Java language HYHOS is an extension of Java which verifies channel communications specified using session types Programs are typed using an analysis that concentrates purely on ensuring the safety of communications Finally the Spin model checker Hol97 is capable of analysing programs communicating via asynchronous or synchronous channels The last two tools have only naive models of the heap which would surely impair the verification of copyless message passing programs There are few other tools capable of analysing communicating systems The TReX tool ABSO1 analyses timed automata that manipulate counters and communicate via lossy FIFO channels Lossy channels may non deterministically lose some of the messages that are communicated over them and form a class of systems easier to analyse than perfect channels CFI96 McScM HGS09 model checker for systems of communicating FIFO machines on the other hand is capable of analysing automata communicating via asyn chronous and reliable FIFO channels Both of these tool
229. tuitively when a communi cating system has reached a final state its communications may be considered as finished and the channels can be closed Let us define straight away some syntactic notions on systems relevant for the rest of this chapter Definition 3 3 Determinism A CFSM X B Q qo T is deterministic if for all states q Q and all actions T Bx x X q 7 q T and q T q T implies q q A system is deterministic if all its constituting machines are Definition 3 4 A state q of a CFSM B Q qo T is a sending state resp a re ceiving state if all the transitions leaving from it are sending resp receiving ones V q n a q e T resp V q n a q T A state that has at least one sending and one receiving transitions is called a mixed state n the literature on communicating automata see for instance the book by Bollig Bol06 determinism on sending actions is often seen as the following stronger property for all states q Q if q nla1 q1 T and q nia q2 T then a1 ag and qi q2 The definition of determinism for receive actions coincides with ours We have chosen a weaker definition because it is the one assumed by Singularity contracts FAH 06 SB09 and because it suffices along with other restrictions detailed below to ensure the good properties enjoyed by Singularity contracts 45 3 1 Communicating systems Definition 3 5 Positional
230. ueues 58 Chapter 3 Dialogue systems The same is true of non positional contracts In the following contract each machine can take a different branch which leaves one a message in each queue of the final configuration 91 41 a a However the three conditions together suffice to ensure leak freedom Lemma 3 8 Leak freedom For every contract if is deterministic positional and all its final states are synchronising then is leak free Proof From Lemma 3 2 each execution of from its initial state is equivalent to a 1 bounded execution that ends in a stable state C followed by a sending cycle in one of the machines As there is no sending or receiving cycle surrounding a final state if both machines are in the same control state then the final sending cycle is empty The final configuration is thus stable hence is leak free The SinGf language additionally requires non final states to be synchronising as well As we are about to see this ensures that communications are bounded Definition 3 25 Singularity contracts We call Singularity contract any contract that is deterministic positional and whose control states are all synchronising In a first version the SINGf compiler required all contracts to be deterministic and have only synchronising states but not to be positional Hence contrarily to their claim these contracts could lead to deadlocks as remarked by Stengel and Bul
231. use a possibly unbounded number of messages can be sent before they begin to be received If this num ber exceeds the capacity of the channel the send operation can either block until room is made for new incoming messages or fault depending on the implementation Synchronic ity can be retrieved from an asynchronous model by making each receive be followed by an acknowledgement message In this work we consider asynchronous communications with unbounded buffers to simplify the model We will provide in Chapter 3 a sufficient condition to ensure that buffers do not grow past a certain size Similarly the receive operation blocks when the buffer is empty whereas a more realistic setting should also include a non blocking receive or one with an optional timeout that would return a special value should the buffer remain empty after some time has elapsed We believe that the work presented in this thesis could easily be extended to include such behaviours as the switch receive construct of our language allows a program to wait for several kinds of messages on several channel endpoints simultaneously non blocking receives might be modelled by waiting on an additional channel for a timeout message delivered periodically by an auxiliary process Finally there also exists a more extreme case of asynchronicity for instance in MPI the 24 Chapter 1 Concurrency and Ownership message passing interface where sending returns even befor
232. variables and values The set of logical variables is denoted by LVar and its elements by X Y 4 1 3 Semantics The semantics of assertions is given by a satisfaction relation or forcing relation between a state c a map 1 LVar gt Val that assigns values to logical variables and a formula of separation logic The forcing relation is presented in Figure 4 2 Logical expressions are evaluated on both the program stack s and the logical stack t v s v x s s x X Ts 3 X Ei Eole E1 s Eole Fi Eos FA s i Eole Let us go through the table of Figure 4 2 The comparison of two expressions E E is true if they evaluate to the same value on s and i It is false if they evaluate to different values or if E or Es mentions variables not present in s The assertions emp 66 Chapter 4 Concurrent Separation Logics s h i EB E gt iff var Fy E2 dom s amp Fils E2 s s h iE emp iff dom s s h i emp iff dom h s h i amp own x iff dom s x s h i E Er E gt iff var Fy E2 dom s amp dom h E1 s amp h LEiTss L 2 5 5 d i E Q1 Q2 iff J01 02 0 01 02 amp 01 1 Q1 amp 09 1 da aiH 1 Do iff Vo ifoago amp o i gi thenoeo ie da oik oingo iff oik i amp Oo iE pa O iE Ad iff c it o DiEVX d iff VveVal o i X v o Figure 4 2 Semantics of concurrent separation logic s assertions and emp describe respectively the empty stack
233. very close to our own Their proof system is however only concerned with proving the safety of programs with respect to memory faults and as such do not include a treatment of contracts We discuss the relationship between our logic and theirs in more details on page 98 Among the numerous extensions of concurrent separation logic two in particular resemble our own Firstly RGSep VP07 Vaf07 which applies ideas of rely guarantee Jon83 to separation logic in order to obtain compositional proofs of concurrent programs communicating via shared memory Secondly the logic for storable locks of Gotsman et al GBC 07 whose aim is to handle dynamically allocatable locks much like we extend separation logic to handle dynamically allocatable channels A comparison between our work and these logics and in their proofs of soundness can be found in Chapter 6 Finally as far as automatic tools are concerned the SinGf compiler also operates in a setting with copyless message passing and contracts In fact the language we consider is directly inspired by SinGf However their compiler delegates parts of the verification to the runtime whereas we strive to keep the verification entirely static Moreover no formal study of their analysis has yet been published Another neighbouring tool is Chal ice LMO9 LMS10 which is capable of verifying programs written in a variant of Cp communicating via asynchronous unidirectional channels However the Chalice
234. well As far as communications are concerned sev eral extensions are conceivable to try and embrace the myriad of existing message passing paradigms Let us just mention a few of them In our current setting it is possible to spec The MPI library by itself proposes no less than 77 functions 128 in its most recent standardisation to configure and perform message passing 144 Conclusion ify a certain number of endpoints on which to wait for a new message to arrive A natural extension of this would be to provide the ability to wait on a linked list of endpoints This is useful for programs that have to manage an unbounded number of channels for instance a name server as found in the Singularity Operating System whose task implies maintaining channels open towards every running process One could also write a program with multiple producers and consumers over a same channel effectively sharing endpoints between processes This has already been discussed on page 98 and we believe that it would be relatively painless to add to our programming language but that it would be met with more resistance on the side of the proof system Indeed our abstraction of the buffer contents by contracts would no longer be sensible as the control states associated to endpoints would change freely when one of its sharers acts on it Another possible way of sharing channels would be to handle a broadcast mechanism on endpoints a channel would for in
235. with program annotations or by means of abstractions for instance by using an abstract domain of formulas as in the Space In vader tool DOY06 over which abstract interpretation techniques CC77 can be applied In this thesis we have taken the first approach and use annotated programs as input for our Heap Hop tool Contributions Let us now present the contributions of this thesis which are threefold Firstly we propose a modelling of a programming language which without being full fledged contains all the message passing primitives needed for copyless message passing and is already sufficiently rich in features to expose the intricate verification issues which follow from this paradigm This modelling itself has three components An operational semantics for programs in which messages are pure values This se mantics does nothing to explicitly track the ownership of each memory cell variable and channel endpoint However as our analysis strives to eliminate them racy pro grams which perform simultaneous accesses to the same variable memory cell or endpoint without proper synchronisation resulting in a race are forced to fault A formalisation of contracts in terms of communicating finite states machines a well known model of communications A second operational semantics for programs where messages carry the pieces of states whose ownership they are meant to transfer in addition to their values and where ch

Heaps and Hops

Contents

Download Pdf Manuals

Related Search

Related Contents