Home

The application of a resource logic to the non

1. 2 3 1 Resource actions 4 23 2 Hold isis la BRB Re esi 223 3 Initialisation e gd a da 2 3 4 Seguentialcomposition 2 3 5 Parallel composition 2 3 6 Process synchronisation 2 3 7 Non blocking requests 23 08 Try while and feq ii i ung Yap ae e ee 2 3 9 Repeatn times 6 4 6 24 Example derivations 3 Correctness of transition system 34 Introduction 42 0 Aw Wee lella sm e ES eve mx oe Sitiulalion s a ded Bk sa la m ge Bee lente a ae 3 3 Soundness of transitions 3 4 Weak bisimulation 3 5 KernelofnDemosstate 3 6 Correspondence between II and aDemos states 11 11 13 14 15 15 17 18 19 22 23 23 23 25 3 7 Correctnessoftranslatlons 64 3 7 1 Correctnessofg o 64 e Correctness OL elemi Addi y 65 Demos and PBI 66 44 PBL and oDemos 4 05 4 an eleme e e ate e e ee ed A 66 4 1 1 Intuitive account 68 42 DeadlockinPBI 69 431 Examples uui ara LAA RE a 70 43 1 Sub deadlock 72 Synchronous parallel rule 74 Dal Motivation kame dee kli e A A M 74 5 2 Soundness try and resource splitting 75 5 3 Soundness Synchrony 6 78 5 4 Deadlo
2. a putR u 1 hold 4 putR t 1 Cp 3 hold 3 putR u 1 putR s 1 dm getR u 1 BE bh od putR u 1 hold 4 C 3 hold 3 putR u 1 putR s 1 m getR u 1 E Ds lt putR u 1 hold 4 In 3 hold 3 putR u 1 Figure 5 3 Path derived deterministically using synchronous parallel rule 80 10 e 2 e P 3 4 O Filled circles represent states in which x holds Double lines indicate a tran sition derived using the synchronous parallel rule Figure 5 4 State space for kitchen example derived by the synchronous transi tion system As mentioned before though the reduced state space comes at a cost The tran sition system is not complete with respect to the operational semantics of Demos programs because the operational semantics defines asynchronous action In the sequel a shall represent satisfaction in PBI with the normal asynchronous semantics and R shall represent satisfaction with the synchronous parallel rule We see then that is not complete with respect to E Proposition 5 3 1 is not complete with respect to a That is there is a formula y and oDemos state R lt P with R lt P Ha v and R a P Ks e Proor Take R lt P to be the first state in the sequence above Then R lt P Ka anys t In but R a P Ks anys tx In Moreover is not even sound with respect to a and therefore
3. For the moment we shall not venture to extend the logic with e g the modalities of CTL or modal u Infinitary conjunction and disjunction shall though be allowed 1 4 3 Observable vs silent actions Hitherto we have failed to consider how the above modalities may take into account the distinction between observable and silent actions Two options exist 23 R lt P Ep iff R 7 Jipl R lt P Fe Ay iff R lt P E y and R lt P v Ra P evv iff Ra P E y or Ra P v Ra P 5 e v iff for all R a P ER lt P R a P E implies R a P Ev R lt a P Eevee iff for some S a Q S a Q eS R a P E S 4 Q o S lt Q D and S lt Q E y and S a Q v Ra P be v iff for all S a Q S S lt Q E implies R lt P e S 4 Q P v R lt P T for all R lt P es R lt P L for any R lt P es R a P Ip iff for some Re Res R a P E R aep R a P E In iff for some Q Prog R lt a P E er Q Ra P Z iff R a P Ce lt ep Table 1 3 Kripke semantics of PBI excluding modalities R lt PIElAe if Vaca R lt P R lt P7 implies R lt P Ep Ra P E 4 p if Jaca R lt P R P and Ra P l 6 Table 1 4 Kripke semantics of additive modalities of PBI 24 RPTE TAK new p R lt P E Alive R lt P 4 new p R lt P E A new p
4. W RL Then RL r f W RL The operational semantics tells us that EL EL with Pj PD body attrsi t1 inserted at some point Now g S R a putR r 1 body gg W where gr RL R W By consideration of the definition of gr we see that W getR r 1 body W and so we have g S Ra putR r 1 body gg getR r 1 body w g S R r lt body gE EL getR r 1 body W gt Rs body ge E bodys W which is exactly up to the associativity and commutativity of parallel pro cess composition g 5 getR r 1 resource available We have S P PD getR r 1 body attrs t EL RL The resource is available so 5 P PD body attrs t EL RL Without loss of generality thanks to the arbitrary order or RL it is a multiset rather 53 than a list let RL r tt RL and so RL r f RL by the operational semantics Now g S Ra body gz EL W where gr RL R W Considering gr RL we notice that R R r and so g S R r lt body ge W Finally R r lt getR r 1 body ge W R lt body ge EL W which is exactly g S getR r 1 the resource is unavailable We have S P PD getR r 1 body attrs t EL RL After execut ing getR r 1 we have S EL RL Without loss of generality let RL r ff W RL h
5. Jac A dS a S lt 0Q Q Proc and R a P gt Ra P o S Q and R a P Vac A VS a Saf0j o Ss Q kp Q Proc and R lt P R a P o S Q implies R a a1S lt Q1 and R lt P E S Q1 o T lt Q2 PD Ss Q Fe Jac A 38S lt 0Q1 T lt Q2 Proc and R lt P T lt 0Q2 and T lt Q3 v VacA VSa 0 Ta Q2 Proc a1S Qi and R a P E S Q1 o T a Q3 and R a P T Q implies T a Q5 E y Table 1 5 Kripke semantics of multiplicative modalities of PBI e The transition system could be augmented with rules to provide for all observable e Observable transition modalities could be introduced to complement gt They would be just as the modalities presented here other than requiring an observable action gt rather than any type We shall adopt the second solution it allows us to define distinct notions of program equivalence and otherwise results in a clearer notion of activity in the logic 1 5 Petri nets in PBI Petri nets can be used to represent evolving systems State of the system is described by the distribution of tokens to places forming a marking State evolves by the pre conditions a set of places of an action being met hav ing token along with all the post conditions a set of places being empty Following the action the places forming its post
6. lt P Entity P2 0 la b f lt P1 P2 D Ds PAR la b GETR getR Pi Vb alg la bf a Pi COMP Pj gt 1 05 lt Q111P2 f lt GETR Pj gt 15410 105 ald COMP getR Po 15 lt 1011102 47 At this stage we would not be able to derive any o transition As we still have code left to execute formally Q1 Q2 4 e we have not terminated cleanly we can deduce that the system has deadlocked 48 Chapter 3 Correctness of transitlon system 3 1 Introduction We now consider various properties of the transition system presented above These properties relate to the correctness of the system with respect to the operational semantics of Demos TBO The latest version of Demos Demos 2000 has a large command set Pragmatism leads us to consider a small subclass of Demos 2000 programs as we did above by not considering variables or value resources namely those written in tDemos with the Demos 2000 delaration format Demos is defined with its operational semantics in BT93 Specifically this avoids the notational burden of considering synchronization between processes and increases the brevity of our proofs The properties considered shall relate to the validity correctness of our tran sition system As shall be discussed we shall not be able to demonstrate the soundness of the transition system with r
7. S slej S lt le v RWS gleies gt R w S lt le py Rafli BLOG FF R lt g r1 72 CETNA where e e e getR r n getB r n getS x 1 re R neZ These definitions are relatively straightforward their value is that they deal with comma separated lists and define FF 36 2 3 8 Try while and req The try command introduces conditional choice into Demos The command try e then P etry ez then P attempts the atomic list of actions e1 If this succeeds P shall be executed Otherwise e is tested to see if P should be executed If none of the e pass the process waits no derivable transition until one does If more than one pass at the same time the earliest P shall be selected Hence we can define the rules for try 2 TRY R lt gle1 R lt e z Ra try e1 then P etry e2 then Q R lt P EA FF R gla Ralglezll R lt e TRY4 c Ra try ei then P etry e then Q R lt Q The while construct defines a loop while an expression is true a body of code will be executed Should the expression be false at the beginning of the loop iteration will stop The req command simply defines an atomic series of actions R lt g e R lt el Ra while e do Q gt R Q whiie e do Q WHILET FF glel R lt while c do Q gt R e WHILE R g e R e REQY 5 RENT R lt
8. body r ff 1 r tt Then g D R a body and by induction g Dj R a bodys R lt body Consequently by the definition of zz D R ra getR r 1 body R r lt getR r 1 body Dx 2We shall write in the sense of two states in II being exactly the same other than having possibly different event times Their translations into the transition system will thus be the same 60 a putR r 1 Similar to r R case a close Similar to r R case a hold t Then P hold t body and g D Ra hola t body Kernelisation yields g Dr Rafbody J By induction g D body hol1d t body Ra body R lt body g Dr Notice that the hold generates a non observable 7 transition so g D g Dr by the definition of We now generalise showing that the translation of any 1 Demos state into the kernel generates an element of the equivalence class Theorem 3 5 2 Translation of a 7Demos program into the kernel generates a member of the equivalence class That is Dy D or g D g Dx PROOF By induction on n EL W where WL the number of processes waiting on resources We shall say that two x Demos states are equal even if they have differing event times or the order of lists differs if that order is arbitrary as their intepretation in the transition system will be the same For convenience we shall have two b
9. req e R lt e 2 3 9 Repeat n times Assume that n is an integer constant We may then define the repetition com mand do that repeats a body n times DOn n gt 0 R lt do n P R lt P do n 1 P E R a do n P R lt fe UPS 2 4 Example derivations We now give some examples to show how transitions may be derived by the presented system 37 Example 1 Jobshop This example refers to the jobshop d2000 program supplied with Demos The code is given in full in Figure 2 3 We only show one of the numerous possible derivation sequences and omit the derivations that go through the instantiation of the entities resources and bins see Example 3 Hammers shall be written h and mallets m We shall first introduce some derived rules to make our derivations slightly more succinct The first allows us to skip some explanation of how we execute the parallel composition of sequential processes R lt P R a P7 R P Q R P Q R P Q P5 R P QIP COMP 1 PAR R a P R a P7 R a P Q P Y R lt P QIP PCOMP etc The second simplifies how we can write a simple get from a bin GETP NBLOCK R b lt getB b 1 R a e R b a g getB b 1 R a e 5 NBLOCK R b lt 9 getB b 1 R lt e etc We commence by showing how the while loop of the worker process is exp
10. Asex aoex3 gt y u um wey 7 x3e 4sey ev9e13 wey 1svo g1a38 Aza gt Asva y u aL ATL Cr gt y u Eme 1 Asvo gr93 5 gt svo y wu MOOTAN ouo svo ue SI 398 03 o q SI 31 3eu3 gol jo odAy 4Juo eq gol e 31e3s O uorjrsod e UT mou ST popuedxo doo 8TTUM sy YIIM ssooo4d 194gof MY T 41 FINODA gt ee ereulxrllr gt uoy 1 y uais3 139 P1m 99e113 02 p1ou ueua T w ya93 Aza gt puvoy y wu Eb ac p1eu x x gt pru puny y wu ueuya KI u193 Azye uoy KI 11 y103 z3 gt puoy y wu t uey KI puu g 93 1340 uoy KI Asvo g193 24 gt pru puny y au g 93 CLA S1OO IAN g193 gt pavu y wu pru ga23 5 gt pru puny y wu KT 6502 g3e3 6 gt pru puny y Y xr pru puny y wu fisva qof Aymoy p um pou e sya3 os pue srej qof Aseo ue 398 03 Satz mou SS9901d Y z PToul xl x gt pru puoy y nu 7 ec exeul rl x gt pru pany y uu Vq 0 epus UOTYeA lop e AG cz ptoul rl x gt pru pany y Y 7 i pr gandl p 57 gt pavy y wu gmd Ed INOOd EEE gt pru pany uus c 1 pru gand gt puny y u ind gol K3rorgrp umnrpour Y soseo o1 mou ssooo1d 19YJOAA OUT i G pew aand e y gt paou y we rereulrlx pou y uu ir pru gand gt puny y u um 1 ptou gt p
11. Np and relax the requirement that the post condition of a transition be empty before the transition can take place It is also posssible to encode Petri nets in PBI In essence all we do is take marked places as resources and the graph formed by pre post P T as the process term Graphically thhe process term would simply be the net with no places marked Writing N X to mean a Petri net N that has a sub net X and M for a marking set of marked places we can define a transition relation to describe the activity of Petri nets As an example STRAN mg M M pa N p t gt m M ma W p gt t gt m for an arbitrary net N p gt t ml with a transition t such that pre t p and post t m the pre and post conditions in this specific case each comprise of only one place With such a transition relation we can ask questions relating to the con sequences of additional places being marked and tokens being removed from places For example the semantics gives us that UN e m e asks if holds of a state in which only m is marked We may use the modalities to ask of the markings formed by transitions The correspondence between questions posed of Demos states and Petri nets is so great that the reader is referred to 84 1 for a discussion of the logic presented The invariance in the process term need not necessarily be so we could have a Petri net that changes Such a system
12. r b W to mean the resource list RL with the entry for r being r b W We use EL P 0 to mean the event list EL having P in place of Q thus possibly causing the order to be different if the times of P and Q are different The reader should be cautious as we use the subscript to indicate kernelisation following other subscripts Lemma 3 5 1 For all II states RL if g EL RL R lt P for some R lt P where P is non parallel then g EL RL Ra P R lt P g EL RL x PRoor By the definition of g we have g EL RL R agg W where gr RL R W Since the result is not the parallel composition of processes there is only one body of code in RL Irrespective of where it came from we may induce over the body of code i e P II found in some process descriptor 59 No code in body Notice that this would imply that the process came from the event list otherwise if it had been a process waiting on a resource we would have getR at the head of the body Kernelisation yields exactly the same process albeit possibly with a different event time Consequently g D g Dp As is reflexive g D g Dr P putR r 1 or close Again D Dy implies that g D g Dy so g D g Dx P getR r 1 There are two cases to consider either r t is in RL or r ff W is in RL If r t is in RL we have D Dy which implies g D g Dx so g D g Dr Otherwis
13. s putB 5 1 e In general we will have the following ew P R lt P E Malas yen A lo where p is some formula true in all states following a transition by any process with put at its head y_ following a transition by any process with get at its head and y following a transition by any other process 70 relates to partitions of the state both of processes and resources Returning to the intelligence agency example recalling that T holds for any state we see that the following holds 1C F 6 55 lt P H F T where C denotes the CIA line 6 denotes the MI6 line etc by 1F ale F and 1C 6 5 f a P HT So in general just as we can in propositional BI we may indicate that a resource r is available by the formula rx T Returning to the jobshop example we may wish to express that h and m are the only available resources Clearly 1h m f a P E h m T but also 1h m lt 4 P E h m T Rather than using T we should have used Ig 1h mfa P E hxmxIp This expresses that there are three partitions in the state one having only the resource h another having the resource m and the final one being an arbitrary process with no resource Suppose that we have a proposition c which denotes termination of the CIA process As has been illustrated it is not the case that in every possible execu tion the CIA process terminates 1C F 6 5 jaLPT E A lany anyT V amp c GEN This
14. P Q R a P Q7 2 The same swapping P and P This shall follow immediately from the symmetry of the parallelisation operator 1 a Raf Pi Q R lt P 11Q so must be able to derive the transition R lt P R lt P As R lt Pi R lt Ps we can also derive Ra P R lt P with R a P R lt PS We may then derive R lt P2 Q R lt P311Q and R lt P 11Q R lt 23110 b R lt PQ R lt P Q so R lt Q R Q Hence R lt P2 Q R a P2 Q and R P11Q R lt gt Another useful property of observational equivalence is that it is an equivalence relation it is reflexive symmetric and transitive Theorem 3 4 2 Observational equivalence is an equivalence relation PROOF We split the proof into proving the three sub properties That is for all R4 lt P Ro lt Pl and R3 lt Ps 1 Reflexivity Ri lt P Ri lt P 2 Symmetry R4 lt P Ra lt Pa implies Ra a P Ri lt P 58 3 Transitivity R lt Pi NR R35 lt P2 and Ro lt P5 RI R3 lt Ps implies R44 Al NR R3 lt P3 The proofs of 1 and 2 are immediate from the definitions of and bisimu lation 3 follows easily too 3 5 Kernel of x Demos states Let II be the set of states in the operational semantics of Demos ranged over by tuples D RL X The equivalence class of a state D with respect to 9
15. P Q If we are to derive a transition we must have the sub derivation SU H lt try e then P etry ez then Po Ha P where P P or P We know that neither e nor ez require any resources referenced by process Q by Consequently any transition from process Q will not use the resources required by e or e2 and so they are not contained in S Therefore any re sources that could be used by the try command thereby affecting the path chosen will not be hidden by inclusion in S Thus adding the resources in S to the environment will not affect the transition so we could equivalently derive SeS uHa try HYS P As this does not use a parallel execution rule it uses TRY this holds for both systems By induction there exists an integer m such that S wH Q gt H Q If then we apply the asynchronous parallel rule to first derive SwS wHa ltry Q WS y H lt a P1Q we can apply the same sequence of m transitions on to derive the required state It follows easily by transfinite ordinal induction that any state reachable by a sequence of transitions in the synchronous system is reachable by a sequence of transitions in the asynchronous system Lemma 5 4 2 For any k N there is a amp N such that If Ra P LR a P then R a P 7 R lt P We now prove that if deadlock is detected according to the synchronous transi tion system then the stat
16. R lt Q and R lt P xR lt Q and 2 for any transition R lt Q R lt Q where o Act we have R a P YR lt P and R a Q R a Q 1 We shall not allow bisimulation between states with different resource sets at this stage so if R zz S R lt P zx S lt Q for any P Q 57 Definition Observational equivalence relation We shall use to denote observable equivalence We write R lt 4 P R lt Q if there is a weak bisimulation between these states That is vi Ut xis a bisimulation It may be that is a congruence relation That is for any process V P contain ing P as a sub term if P Q then V P V Q where V Q is V P with P substituted for Q We do not need to prove this property but do require that if two states are observationally equivalent and we create the parallel composition of each of them with a third state observational equivalence is preserved Lemma 3 4 1 If R a P R a P then R a P Q R a P lQ for any process Q PROOF Very similar to CCS Mil89 pp 98 We shall demonstrate that x Ra P1 Q Ra P3 Q Ra Pi Ra P5 is a bisimulation To prove this we can show that for c Act and supposing R a P Q xR lt P2 Q 1 a Ra P Q R lt P Q implies R lt P Q R lt P 1Q and R lt P Q R lt PQ b R lt P Q R lt P 1Q implies R lt P2 Q F lt P211Q and R lt
17. UNS Sem sems eens 1 Tr Sem a 4 U AU puts 1 Bold seen Tr Sem sems Tr puts semS 1 U l j Tr Sem sems 14s r Av gt LS lt U 4 U Tr Sem gt 1S lt U 4 U Sem gt WalUlA U S Sem semS l Tr Sem lt TU 4 U hold 5 Tr Sem sems hold 5 Tr Sem sems puts semS 1 Tr Sem sems ev ms pa aso T T 22 150401 Example 3 Deadlock This example shows the transition system becoming deadlocked and gives a suggestion of how this may be expressed in the process logic This time we shall show processes and resources being created The code for this simple example may be found in Figure 2 5 In the following derivations we shall abbreviate the complete code of P1 by P getR a 1 Q and of P2 by P getR b 1 Qo 46 Res a 1 Res b 1 Class P1 1 getR a 1 getR b 1 hold 5 putR a 1 putR b 1 class P2 getR b 1 getR a 1 hold 6 putR a 1 putR b 1 Entity P1 P1 0 Entity P2 P2 0 Figure 2 5 Deadlock source code Di 15 Res a 1 ta fi RES 1 lt Res a 1 Res 5 1 la lt Res b 1 Similarly COMP4 la a Res b 1 Entity P1 0 a 5 f a Entity P1 0 D D3 la b lt Entity P2 0 la b j a P ENTITY la b lt Entity P1 0 Entity P2 0 la b a P Entity P2 0 ENTITY 5 a b
18. abbreviations shall be made for the diamond modality as well 1 3 2 General Hennessy Milner Logic Though the inductive definition above allows formulae to have nested modalities so far we can only make statements about processes after a finite number of steps Furthermore to assert that a program terminates before say 1000 steps would require a very long sentence 2There is no fixed convention for this abbreviation Its use shall be avoided wherever possible 16 With this in mind suppose that we generalise conjuction or its dual disjunc tion to require validity of all conjuncts indexed by a set I sH Nyi if Vel sey iel Given that we can express for arbitrary n that a program in state s terminates or at least stops running after exactly n transitions from some set A as s E A A L we may express the above property termination before 1000 steps succinctly as sk V QUAL 0 lt i lt 1000 Notice that we have abbreviated i 0 1000 by 0 lt lt 1000 If we allow infinitary conjunction i NU w where w is the first ordinal the least number greater than every number in N otherwise written N itself we shall interchangably write N for NU w we may express deadlock freedom of processes by the simple formula o 5 V AAL iENU w which is logically equivalent to A SAKAT iENU w The reader may gain some intuition as to the meaning of this sentence by unfo
19. conditions are then marked Several introductions to Petri nets exist e g Mur89 and the introduction to MBC 95 Petri nets can be represented graphically it is conventional to draw 25 R PIE Ajo if ac A R a P Y R lt 2P7 Ra P Ke R P TAle iff Vaca R lt P R P ARa P E e Ra P E Alto iff Jaca a S Q and R a P gt R a P e S Q and R lt P e Sa Q E e R lt P EMAIL we iff VaeA a S lt Q and R lt P R lt P e S Q implies R lt P o Sa Q E e R lt P KAN new iff Ja A a S Qi and R a P E S Q1 o T lt Q2 and R lt P T Q and Ta Q5 P e R lt P MAlnewp iff VaeA a1Sa Qi and R lt P E S s Qi o T lt Q2 and R lt P T Q implies T lt Q5 H y Table 1 6 Kripke semantics of observable modalities of PBI places as circles tokens as dots and actions as bars Pre conditions of actions are drawn as arrows leading into the action and post conditions are drawn as arrows leading away Figure 1 4 gives some examples More formally a net is a 4 tuple N P T pre post A marking Misa function giving the number of tokens in a given place We shall consider M P 0 1 Taking M to be the set of all markings P is the set of places circles T the set of transitions bars and pre post T M are functions that return the requi
20. formula expresses that there is a state from which the system can make no transition and the CIA process has not terminated cleanly We might like to consider the effect of removing MI6 s line would this allow the CIA to complete its task in all conditions We may express this in the logic as 10 F 6 55 lt P 6 A lany anyT V ec iEN Now 16 f fel E 6 For the above formula to be true then all we have to show is that C F 55 lt P E Aen lany any T Vec Notice that the choice of partition here is entirely deterministic Because MI6 s line is removed the MI6 process will not be able to proceed to take MI5 s line or the FBI s Consequently the CIA process will terminate properly so we do have lC F 6 5 f lt P E 6 x A hen yi V Eq iEN This illustrates how may be used to reason about subtraction of resources from a system It is a simple matter to ask if a partition exists that is non deadlocking R lt P D 07 This will hold only if there are deadlock free partitions S4 lt Pi and S2 lt Pa such that R lt P S 482 lt P Pa If we require a non trivial partition i e without one partition being null process we would ask R a P 97 MIp DP A Ip 1The following formula comes from the definition of deadlock see 4 2 2But not overall deadlock freedom 71 Now let us consider Suppose that we want to consider the effect of install
21. hard 1 m h easy lt J ho1 1 m h easy a J putB hard 1 m h easy 4 J J ho14 1 m h easy a J J putB hard 1 7 NBLOCKT WHILEZ m h easy lt gl m h easy lt m h easy lt a J m h easy lt K m h easy lt J J putB hard 1 m h easy a K J putB hard 1 PAR11 Thus we could write im h a J J W pup lm h easy a K J putB hard 1 W 5We shall adopt a syntactic equivalence that allows us to drop the brackets denoting multiset 40 DPreullrl xr p pou uu c 7r paoy aandl e yr gt utu gnd fud T pTou gt puny y u mal T puny qynd gt y wu CLANOO gt pou y uu oma T puny aynd gt yu 1 4 qof prey e soseo e1 SS9901d Jox10AA OUT pooy aand ry gt yu 1 paoy armdiiriirl gt yu 7 gt y us e gt y fue Sq Mey 08 gt y iw uva CIITHM MOOTEN popuedxo st d00J 9TTUM S 194gOf 19YI0UY a paoy aandl e 1 gt yu 1 papy yanndiiriir sex eoeza gt y wu gt yu C Aseq eoeza gt y u Fd INOOd HOVUL jU9TIS SI 3t OS uorjoe 99100S91 OJGISLA OU SULTOJ19d 41 PURUTUIOD 89217 I 9 129X9 MOT IM cr pavuy aaud r r i amp seg e exa gt y u S T puoy aandl y x gt Aspe y uu gaes anood
22. implies T lt Q4 Qi md Qi R lt P 4 y P Proc ER P a YU lt lel E SuT a Qi Qs Q1 Q2 Ta Q5 SWTs Q Q2 011102 Ta Q5 EP Ra P f lt P R a P a S e Table 4 1 Demos semantics of PBI 67 actions getR Ir ale getBp io ale getS la ale putR7 Ir ale putB Qo ale puts la ale 4 1 1 Intuitive account e Resource propositions r hold in states with no process component where r is the only resource available e Process propositions P hold in states with null resource component with P being the only process e The additive unit of A is T which holds in any state e The additive unit of V is L which holds in no state e The multiplicative resource unit Ir holds in states with no resource com ponent but allows an arbitrary possibly parallel process e The multiplicative resource unit p holds in states with only a null process component but allows an arbitrary resource component e The extraneous multiplicative unit holds in states with only a null process component and no available resources e The additive logical operators A V and are all as in classical boolean logic A allows us to assert that two propositions hold in a state V allows us to assert that at least one of two propositions holds in a state and gt allows us to assert that if one proposition hol
23. may fail to derive a transition by is GETR it is the only rule for which the side condition does not form a tautology with the other rules As the state is deadlocked the command at the head of every process therefore must be getR r 1 Moreover as the side condition is not met because we are not able to make a transition from this state we do not have any resource r that is requested We may only use the rule SPAR to execute certain commmands It may not be used to pass any getR r 1 command where either r is not available or r is referenced by some other process Beyond here the asynchronous system will be used Notice that necessarily does not hold where we fail to derive a transition in the asynchronous system We see then that R lt P Ed R a getR r 1 getR r 1 implies R lt P him R a getR r 1 getR rs 1 As any V Ip is equivalent in the two systems then R a P Fa any any T V Ip It is interesting that in the above proofs we have not used the fact that we do not use the SPAR rule to pass by putR r 1 commands where r is referenced by any other process We could therefore remove this restriction and preserve the correctness of deadlock detection Such a relaxation though would decrease the size of the class of formule equivalent in the synchronous and asyn chronous systems The synchronous system would for example be incomplete in det
24. oDemos as usual single step transitions in the transition system shall be denoted gt Explicitly observable actions shall be denoted gt Our transition system is non temporal it does not take into account any times inside the Demos program So for example it will completely ignore synchro nisation by any hold statement Consequently it will consider the execution of commands on resources in any and every order including those that are impos sible according to the operational semantics of the program which does take into account time 50 We can see therefore that for the full Demos system we do not have the fol lowing It R a P R a P then Ra P Ra P for some justified i e not something vacuous that makes the above triv ially true function f mapping transition system states to operational semantics states We may however consider the converse does our transition system simulate the operational semantics That is do we have the property If S gt S then g 8 gt gs where g maps states in the operational semantics to states in the transition system and 5 is the reflexive transitive closure of gt the effect of running an arbitrary number of steps including 7 transitions o Act In order to demonstrate such a relationship we must define the map g be tween states in the operational semantics and states in the transition system Firstly though to aid clarity of ex
25. p w is used to indicate that we can partition using o our current state one part satisfies p and the other Y p w indicates that if we add all that we need to satisfy p to our current state y will hold It may be helpful to consider a monoid based upon a notion of resource If we let R denote a multiset of discrete resources P R denote the set of all sub multisets of R and multiset union be 4 then we can define the monoid M P R 0j 9 The consequent intuitive meaning of m is that we can split the resource multiset m in two one part making p true and the other making w true m p Y intuitively means that given the resources to make p true if we add them to what we have in m y will be true Example Discrete resources For each resource r R define r 1r so for every resource r r holds iff r is the only available resource Also define a proposition Mmovepgx holding with wrench mallet it signifies that we can move a bolt iff we have a hammer and a mallet available lAs we have said not for example n metres of string that can be split into m and m metres of string where m m n for arbitrary m m ER 12 The Kripke discrete resource semantics gives hammer hammer hammer mallet W hammer hammer mallet hammer x mallet hammer mallet hammer T hammer mallet hammer T hammer x T hammer mallet hammer x hammer x T KK hammer mallet hammer
26. parallelisation rule Ti Path derived deterministically using synchronous parallel rule 80 State space for kitchen example derived by the synchronous tran Sion System se lb o 81 List of Tables 1 1 Kripke semantics of static BI 1 2 Semantics of CTL formule 1 3 Kripke semantics of PBI excluding modalities 1 4 Kripke semantics of additive modalities of PBI 1 5 Kripke semantics of multiplicative modalities of PBI 1 6 Kripke semantics of observable modalities of PBI 4 1 Demos semantics of PBI Introduction When we design complex systems we should ask questions of them before they are implemented will it run fast enough would it be more efficient for a human to do a particular sub task etc To answer such questions will require automation In the general case then how are we to automate such analyses of systems Perhaps the most obvious manner at least to the computer scientist with a disposition towards the practical is to simulate the design probably observing several runs of the simulation thereby repeating an experiment Though in principle this approach generalises to all types of system by Turing complete ness and normally requires little background knowledge other than an under standing of the system and the ability to program in some ways it is grossly unsatisfactory What if for example we are simulating a network and no run of the simulation h
27. stage though it would not be hard to extend the logic to allow recursion in the manner of modal y for example As before process resource terms shall be written R lt P where R represents the globally available resources and P represents the current state of the process We define the set of all such states to be S Res x Proc As is the case for BI the semantics of the logic is defined according to a Kripke resource monoid This time though we shall define the monoid over process resource pairs M Res x Proc en ep o C where Res x Proc is the set of all process resource terms S o is a composition operator ep eg is the identity element under o and E is a pre order on S As Sisa set of pairs we shall let R a P range over it Table 1 3 gives the Kripke resource monoid semantics of the non modal part of PBI This corresponds to the semantics of BI other than the multiplicative 6 Process BI 22 units p and Ig These are introduced to allow expression of zero resource and null process respectively So Inl er x Prog Ip Res x ep We may see the normal multiplicative unit of BI as Ig Ip Thus I is extraneous In the sequel we shall take modalities to bind more strongly than anything else between themselves they shall be of equal precedence 1 4 1 Additive modalities As the static logic BI has both additive and multiplicative operators it seems natural to introduce both addit
28. unsound transition rule is presented in Figure 5 2 76 o ni uoryes fojrered punosun 97 YIM opeur UOTYeALIOG 7 OM3IJ r aerv ule armo wa rtauvalr diml gt YY uy INNOSNA 7 lr auv gu ww e auval gt uwy r arm e w z earne yu WO0 l WOD ios layuval gt wy layval gt y ug ag arn a larml gt va E gt wy G Yu gt y uy T P u e IT 9393 5 gt yu LE 1u 4983 5 gt u 4r LA FMOOTAN fut p qul gt a GO Yus3 gt yu LA 77 Clearly this is wrong we did not use the mallet on the easy job as we should have done The error came from the fact that it was possible for us to give the mallet to the process executing HARD which did not need it whilst MID did not know that the mallet existed For this reason a logical resource weakening rule for transitions R a P R s P WEAK RWS lt P R yS lt P would also be unsound Two solutions exist to overcome this particular problem One is to adopt the rule RyH lt P Hs P R amp eHa Q Ha Q 01102 RYR amp Ha P Q H P Q SPAR This allows both derivations to see all the unused resources in the system The second solution is to disallow the command at the head of any process being try when considering the synchronous parallel rule We shall adopt the first solution 5 3 Soundness Synchrony The pres
29. x T hammer T l hammer mallet wrench k movepot T l hammer mallet wrench movepoit T l hammer mallet mMovegot mallet x mallet x T hammer mallet W mallet mallet x mallet x T The monograph Pym02 provides a substantially more detailed technical and comprehensive account of BI Though it is possible to encode action Petri nets are discussed in POY02 Pym02 into BI by attaching certain semantics the resource interpretation above does not have a notion of how resource evolves with the action of processes we are only able to make static judgements The necessary tools to describe action transition systems and modal logics are introduced below Notice that we have defined neither negation nor falsity in this system We could have included falsity 1 but this makes the associated natural deduction system incomplete With L we could define intuitionistic negation p y L We obtain a classical logic thence negation if E is equality 1 2 Transition systems Since the dissemination of Gordon Plotkin s notes on Structural Operational Semantics Plo81 as detailed in Plo03 it has become commonplace to de scribe the activity of programming languages as a one step relation between states defined structurally That is we give an inductive definition of the effect of each command on the state of the system This is normally presented in the proof tree natural deduction style P
30. 1 Approximants of X V X to form uX o V X Similarly the greatest fixed point may be found by iterating from the set of all states taking the intersection of the iterates An example of this is given in Figure 1 2 As an alternative to this interpretation the authors of BS01 propose the fol lowing maxim v means looping u means finite looping Consider the formula Z e V Z meaning that a state either makes c hold or some such state is reachable The maxim gives different meaning to the formulae uZ o V Z and vZ o V Z the former means that there is a finite length path to a state where c holds whereas the latter means that there is a possibly infinite length path to a state where o holds Notice that this does not imply that c holds in any particular state s 5 Figure 1 3 is an illustration of the semantics of this formula Further difficulty comes from the nesting of fixpoint operators which can be extremely difficult to interpret The reader again is referred to BS01 for a proper treatment of the logic An exercise for the reader is to decide which fixpoint operator should be used in the definition of deadlock freedom 5 Answer v giving D def vX A T A X 20 e e 0 6 I e 6 0 o9 O O a Zeroth approximant b First approximant Oo o O e O o9 O0 0 c Greatest fixed point Figure 1 2 Approximants of X A X to form vX 0 A X CER
31. Laboratories 2001 92
32. ON invent The application of a resource logic to the non temporal analysis of processes acting on resources Jonathan Hayman HP Laboratories Bristol HPL 2003 194 October 2 2003 E mail jmh00 doc ic ac uk business process Many systems exist that can be modelled as processes interacting analysis bunched through shared resources people factories and computer systems to implications name but a few Building upon a logic capable of reasoning about concurrency static resource models the Logic of Bunched Implications we demos tentatively define the semantics of a logic capable of reasoning about dynamic resource models The logic shall not consider the influence of timing on process interaction We give a brief overview of other process logics Hennessy Milner logic Computation Tree Logic and modal u which indicate how we may automate the system We illustrate how our dynamic resource logic may be applied to the analysis of Petri nets In order to conduct an analysis of processes we must have a formal representation for them we choose Demos and present its salient characteristics We give a formal definition of its nontime semantics and prove that this is in some sense correct Following consideration of how we apply our process logic to Demos models we propose a method for reducing the state space of models generated by considering a partially synchronous execution We show that such a system at least correctly detect
33. OO OSS a uZ o V Z b vZ o V Z Filled circles represent states in the fixed point solution for Z hollow circles represent states not in the fixed point solution for Z o holds in no state Figure 1 3 Differing semantics of least and greatest fixed points for an example state space 21 It is possible to encode all CTL formula quite simply in modal p PUY uZ v pA 4 e V PUY uZ v pA ZA 4 The definition of V U requires that we be able to enter a state in which Z holds because we do not assume that the transition relation is total In defining the modalities of CTL we make use of the modal jy equivalence UZ p vZ p e YGy lt vZap l Z e Gy ES vZyeA ZV 1 e YF ES uZyv ZA 2 IF y uZ v Z CTL may not however encode all formula written in modal u we see that modal is more powerful than CTL and also therefore CTL The Edinburgh Concurrency Workbench MS uses this fact natively the system checks assertions made in modal u but it is possible to load macros that convert formulae written in CTL or CTL to modal j Users that are not fluent in modal y can therefore use a simpler language 1 4 Modal BI The addition of modalities to BI was first suggested in POY02 Pym02 Fol lowing our pedagogical account of modal calculi we shall now extend these definitions to define PBI We shall not venture beyond the modalities of HML at this
34. PD P PD getR r 1 attrs 0 r tt D RL The operational semantics allows us to take the resource yielding P PD 0 Gr f RL The exec command allows us to take another step to r ff RL Assuming the well formedness of the program this atomic command in itself is not well formed we could alternatively have made this a special case in the COMP case below this is f R a P P putR r 1 Similar but we use assumption 4 to eliminate the possibility of a waiting process taking the resource straight away P c body cis a command and body some non parallel process Consider the cases for C c hold t 56 TS P hold t body We may only derive the transition R lt hold t body R lt body Op sem F R a hold t body P PD hold t body attrs 0 R The operational semantics yields upon execution of the hold P PD body attrs 0 R which is exactly f R lt body c getR r 1 or putR r 1 As before but we will not need to use the exec rule to reduce down to an empty event list The consideration of getR above could be placed here instead of above it was placed there to show how a proof that considered bins would be constructed P Pi Pa Assume without loss of generality that R lt P P2 R lt P Q We therefore have R lt Pi R lt Pf so b
35. REMISES RULE NAME CONCLUSIONS Condition This asserts that if we can derive by the set of rules all the premises then the conclusions will hold provinding the side consdition is met Thus as we have defined the transition relation structually we can prove properties of the relation by structural induction Consider as an example an elementary imperative programming language The one step transition relation shall be written gt A transition system shall represent state as a function from variables to values with s r c representing the system state s but with x having the value c If we let A e s represent 13 the result of evaluating the arithmetic expression e in state s we could define assignment as follows ASS ATe s c x e s gt s x e c This expresses that the program x e executing in an arbitrary state s ter minates after one step leaving the same state other than x is now c Ale s the result of evaluating e in s Together with a series of other rules for the various programming language constructs for example the sequential composition of commands s P s Pi s Py Pa gt s Pr Pa COMP this would define the transition relation gt 1 2 1 Labelled transition systems It is sometimes useful to label the the transitions between states As noted in Pit02 when we define the semantics of languages we usually have reduction transiti
36. September 9 15 2000 91 Plo81 P1003 POY 02 Pym02 TB94 TB95 TBO1 Tof01 Gordon D Plotkin A structural approach to operational semantics Technical Report DAIMI FN 19 University of Aarhus Denmark Computer Science Department 1981 http www dcs ed ac uk home gdp Gordon D Plotkin The origins of structural operational semantics Jornal of Functional and Logic Programming 2003 David J Pym Peter W O Hearn and Hongseok Yang Possible worlds and resources The semantics of BI Journal of Theoretical Computer Science to appear 2002 David J Pym The Semantics and Proof Theory of the Logic of Buched Implications volume 26 of Applied Logic Series Kluwer Academic Publishers Dordrecht July 2002 Chris Tofts and Graham Birtwistle Denotational semantics for process based simulation languages Part I demos Technical Re port School of Computer Studies University of Manchester 1994 Chris Tofts and Graham Birtwistle Denotational semantics for process based simulation languages Part I jdemos Technical Re port School of Computer Studies University of Manchester 1995 Chris Tofts and Graham Birtwistle Operational semantics of DE MOS 2000 Technical Report HPL 2001 263 Hewlett Packard Labo ratories Graham Birtwistle School of Computer Studies University of Leeds 2001 Chris Tofts Compiling DEMOS 2000 into Petri nets Technical Report HPL 2001 274 Hewlett Packard
37. U w 69 4 3 Examples We shall start by considering the modalities The additive modalities as we have said relate to transitions in which the resource component of state does not change We have then R lt hold 5 putR r 1 P T which expresses that the process can act without changing the available resource collection We also have lr a hola 5 putR r 1 getR r 1 putR r 1 E r Tp which expresses that every action that does not change the available resource collection gives a state in which r is the only available resource Notice that we do not have r x Ig the getR transition the only transition leading to a state in which r is unavailable does not match the semantics of the additive modality The additive modality does not refer to actions that will change the available resource collection so R lt putR r 1 which expresses that the process can make no action that does not change the available resource collection The multiplicative release modality is used for put X transitions So for exam ple lr s a putB b 1 E new b r 5 by the only transition 1 putB ls r lt putB b 1 1b r s a e and that putB 1 105 e The multiplicative acquisition modality is used for getX transitions lb r s a putB b 1 getB b 1 E new r s In by the only get transition 1 lb r s f allputB b 1 getB 0 1 Er
38. X where X could be R B or S command the resource is available There is no reason therefore why we cannot make a transition from this state for every process indexed by Cp N AR We may deduce that this case does not arise R a P Fa any T is never true if x holds so we may vacuously conclude R a P Es any T 5 4 2 Completeness of deadlock detection In order to show that the synchronous system is complete with respect to the asynchronous system that is if we detect deadlock in the asynchronous sys tem we will in the synchronous system we shall first show that if it is not possible to make a transition in the asynchronous system from an arbitrary state it is not possible to make a transition in the synchronous system Lemma 5 4 4 For all states R lt P Ra P Fa any gt RSP Fs any Proor By induction on R a P Assume that R lt P Fa any T As usual we shall consider only the case where P is the parallel composition of processes and holds Otherwise we would use exactly the same transition system and the statement would be easily provable Then there is no derivation concluding for any state R a P R lt P R a P Consequently as P is the parallel composition of processes there is no transition derivable for any of these In the synchronous system holds so we would require at least one derivation of a transition for a sub process to derive a transit
39. a so PUTS V ETT gt utS x n uto Ra ee Ra SP Proc Label x Code x Py Proc where P is the multiset version of powerset Code is the set of syntactically correct Demos programs and Label is the set of process labels The reader will of course recognise that this type Proc represents the solution of a recursive domain equation 35 Though we shall not write implicity modified synchronized process collections it is important that the reader recognizes that they exist So for example sequential composition is actually R 5 gt R lt 5 Ra 22 2 R lt 232 COMP R Rs 5 R lt 22 R s Is COMP re 2 3 7 Non blocking requests In order to define valid transition rules for try and while we shall need a non blocking multi request a request where the list of actions is atomic if any one of the requests fails the whole list fails and that we can detect failure of req will be similar We shall use the non program label g to denote such a request When we fail to complete a non blocking request we shall indicate this using the symbol FF R a getS x 1 gt R a e NBLOCK 5 5 R lt glgetS z 1 R a F a T NBLOCKE FRED JP Ple n NBLOCK l R a getR r n gt R e RY Ra g getR r n 5 R lt Je ABRO arate E NBLOCK R a o R lt e NBLOCKT R lt gli R lt 8J
40. and resource splitting Let us consider how we may formulate a rule that allows synchronous execution of processes If we include the simple intuitive rule R lt P R P S lt 90 S Q1 SPAR o RWS lt P Q R amp Ss a P Q the semantics of the transition system become unsound with respect to the operational semantics of Demos The unsoundness comes in part from the fact that we have considered only a simple split of resources in deducing a transition we may allocate one processes resources it does not need thereby depriving the other process of resources This error may manifest itself in a try command choosing the wrong branch 75 To give a concrete example of this consider the jobshop example 2 4 with one extra hammer Suppose that one worker has taken a medium difficulty job to do and the other has taken a hard job to do The state in then is lm h h a MID J H ARD J where MID is the procedure for a medium difficulty process try getR m 1 then hold 20 trace C Mid putR m 1 etry getR h 1 then hold 10 trace C Mid putR h 1 and H ARD denotes getR h 1 hold 20 trace Co Hard putR h 1 Define MID hold 10 traceC Mid putR h 1 HARD hold 20 trace C Hard putR h 1 representing the code to be executed if we have a middle or hard difficulty job respectively and have picked up a hammer The derivation from this state using the
41. anded and how a bin item is placed in the available resource collection NBLOCKT WHILE PARI 3 lm h j alg tm alel Um h f a W m h 5 lt a putB easy 1 W lm h j AYINA Um h 4 7 J putB easy 1 W GET lm h lt putB easy 1 Bee lm h e T PCOMP3 lm h f 4 J J putB easy 1 W E lm h easy 4 J J ho1a4 1 W where J is the code of the Jobber class W is the code of the Worker class and K try getB easy 1 then trace C Easy etry then J 38 Class Jobber While try getB easy 1 then Trace Doing easy hold 5 etry getB mid 1 then try getR mallet 1 then hold 20 trace Done mid putR mallet 1 etry getR hammer 1 then hold 10 trace Done mid putR hammer 1 etry getB hard 1 then getR hammer 1 hold 20 trace Done hard putR hammer 1 Class Work while putB easy 1 hold 1 putB hard 1 hold 1 putB mid 1 hold 25 Res mallet 1 Res hammer 1 Bin easy 0 Bin mid 0 Bin hard 0 Entity J1 Jobber 0 Entity J2 Jobber 0 Entity W Work 0 Hold 200 Hold 0 Close Figure 2 3 Jobber soruce code 39 We can now silently remove the hold from the head of the worker process and expand one of the Jobber s while loops NOTIME PAR 3 PAR m h easy 4 ho1d 1 m h easy lt putB
42. as a very large file being transmitted or any other rare event Clearly our results may be overly optimistic which could lead for example to us breaching the terms of a service level agreement Conversely what if our simulation has a few too many rare events large files This time our results may be overly pessimistic resulting in the over specification of the network at financial cost to us One answer to this is to run the simulation for longer so as to increase the probability that rare events are encountered Of course though given a finite amount of time our results will always be approximate An alternative approach is to construct an analytical model of the system to be analysed Returning to the network example a model would probably result in a set of equations to solve in order to obtain some measurements of the system s performance metrics The advantage of this is that one analysis gives exact results taking rare events into fair consideration and very often can be obtained much faster than by simulation The flip side is that generally we are only able to do this for particular classes of system For example the simplest analyses of queuing networks e g computer networks that transmit packets assume a negative exponential probability distribution of service time and arrival rate that is P Service time t x e Fortuitously many systems approximate very closely the assumptions made to build such m
43. ase cases n 0 There are no waiting or active processes Consequently D Di so g D g D is an equivalence relation and therefore reflexive so g D g Dx n l Q d Immediate by Lemma 3 5 1 n 21 The event and resource list translated into o Demos states will be of the form g D R lt Pi Po Let D D P P P3 and Da D P5 P P3 essentially deleting from the event and waiting lists a non zero number of processes Then g D Ra P and g D2 R P5 By induction R lt P Ra g Dix and R lt P2 RRa Pox g Dox Now by Lemma 3 4 1 Ra P P R Pi P5 Raf Piz Pox g Di Therefore because is an equivalence relation g D g Dx 61 z Demos states II ud BI t s states f E fe o Figure 3 1 The correspodence between states of the transition system and the of operational semantics 3 6 Correspondence between I and cDemos states As we used X in the previous section to mean the signature of a state in Demos to avoid confusion we shall use the upper case Greek letter 2 to denote the set of cDemos transition system states So g 1 9 and E f Q9 I The range of g when applied to states in the kernel IIy shall be written That is Ok E R lt P 3D Hz g Dy R lt P It is interesting to consider how our translations between II and oDemos states work when we restrict our attention to the kern
44. be noted though that the total composition relation described here makes proof search very non deterministic Take for example the formula ew v Not allowed if we define composition partially R lt P oS lt le R w Sa P to evaluate this we may have to consider adding every o Demos pro cess that can release a resource 4 3 1 Sub deadlock Consider again the jobshop example of 2 4 The worker process the input stream of jobs to do can as it is never deadlock Consequently if we consider the whole process we see that it is always possible to derive a transition using the worker process so the whole system may never deadlock Now this is not of very much use to us what we really want to know is whether or not the jobbers deadlock Deadlock of a process whether it be a sub process or not is defined to occur where no transition is derivable at any reachable future state For a sub process Pejo then a state is deadlock free with respect to Pj iff there is no reachable state from which P p does not act in any transition from any future state We can write this in PBI as po E 2M any e AU Mas UK an 3This is not the case if we consider a fair transition system 86 1 72 Note that we have used a set of action labels indicating action by Py K This set can be defined by pattern matching K a a Labelsanda 73 Chapter 5 Synchronous parallel rule 5 1 Motivation Consider a kitche
45. cesses is correct with respect to the non temporal action of processes in Demos We defined a kernel of Demos states capable of representing processes non temporally 6 1 Further work A number of aspects remain to be considered Shared resource Demos programs do not allow us to represent shared re source we cannot represent for example that processes P and P have access to a resource whilst P3 does not Our process logic similarly is not able to make such a distinction and it is not clear to see how we may extend it to do so without significantly modifying the logic Fairness and justice We have allowed processes to execute in an arbitrary manner e g in 5 4 2 we allowed the third process to be executed all the time ignoring the blocked first two processes Such biased execution may be considered to model improperly the actual characterisics of a sys tem Following from the discussion of fairness in GPSS80 Manna and Pnueli in MP83 suggest two characteristics of proper executions fair ness and justice We adapt their definition to our notion of concurrently executing processes TAs suggested by D J Pym 2This could represent the resource having been taken by P or P which are close to each other or the resource being generally unavailable to P3 87 e An execution sequence is said to be fair if it terminates finitely it is infinite and all finite processes terminate or otherwise cannot continue to ex
46. ck freedom equivalence in asynchronous and synchronous SYSTEMS PC a ote el A A ee e 82 5 4 1 Soundness of deadlock detection 82 5 4 2 Completeness of deadlock detection 84 Conclusions 87 6 1 L rther WOK exse te oe eae ee ee ee WE 87 List of Figures 1 1 1 2 1 3 1 4 2 1 2 2 2 3 2 4 2 5 3 1 3 2 5 1 5 2 5 4 Intelligence agency network and process design 9 Intelligence agency processexecutilon 10 Approximants of X V X to form uX o V X 20 Approximants of X A X to form vX o A X 21 Differing semantics of least and greatest fixed points for an ex amplestatespace ee 21 1 4 a goes to 1 4 b 1 4 c no action blocked by post condition 1 4 d no action not all pre conditions met 1 4 e poes to LA kasmak akel emme geni RU 27 BNF syntax of restriced Demos considered 30 Demos program for the intelligence agency example 30 Jobbersorucecode 39 Semaphoresourcecode 45 Deadlocksourcecode 47 The correspodence between states of the transition system and the of operational semantics 62 Bijection between kernel and transition system 64 Reachable state space for kitchen example derived by asynchronous transition Sy Ol suene we x eR As MAS 75 Derivation made with the unsound
47. cs of the CTL modal ities es E JFo Ls E A T Uy This means that there is a path in which p holds in some future state potentially holds e sH YF sEV TUg This means that along every path from s there is a state in which y holds q is inevitable 3Gy ES sE V TU g SE This means that there is a path from s where p holds in every state e sk VGy EE s E 23 TU g This means that for every path from s p holds in every state q is globally true VF is frequently written AF JG is frequently written EG etc We can represent deadlock freedom in CTL7 as DGTL 9 vey 1 3 5 Modal u The modal calculus a good introduction may be found in BS01 we sum marize the essentials here is a logic where formula may be defined recursively Deadlock freedom for example may be recursively defined with respect to a set of actions A as Do HATA A O T This states that a state is deadlock free if it is possible to go to another state and any state reached is also deadlock free As before we define the set of states in which a proposition p holds as v P S where S is the set of all states and P S is the powerset of the set of states P X Y Y X In the above example we have used as a variable over logical forumlae If a formula has a free variable Z we indicate this by writing it as p Z This may be regarded as a function p Z PS PS Now by th
48. ct x Q be tween programs and the resources they hold we shall use infix notation for the relation It is defined inductively according to the following set of rules which essentially give the exclusively resource sensitive non temporal structural op erational semantics of Demos programs As well as observable actions we shall allow silent non observable transitions such transitions shall be written R lt P gt R lt P Recall that this should decrease the level of non determinism within the proof system compared to an equivalence relation It may be useful later to define a new transition relation o def Tr o Tr ISilent and observable 2The inspiration for 7 obviously is CCS 31 where S denotes the reflexive transitive closuse of the relation S Alternatively we may define gt inductively P R lt P OBSERo P EC R4 P Ra P R a P R a P R lt P OBSER R a P R s P Ra P 3R lt P mR a P R a P OBSER gt v R a P R lt P The symbol P and Pi P5 Q is used frequently throughout this doc ument n general it ranges over processes including parallel processes It is also used to range over non parallel processes that is bodies of code The reader should extract the appropriate choice between these from the syntax of Demos code 2 3 Transition system cDemos We shall write R a
49. def O D E H gD ME is the set of states containing programs that are equal in some sense relating to the execution of the states to the state under consideration In our case this shall be observational equivalence in the transition system Suppose we want to find a member of the equivalence class for a particular state D We cannot simply construct D by checking every Demos state for equivalence the set of states II is infinite Instead we must obtain such a program which we will say belongs to the kernel of II Ix from its syntax Definition The xDemos state Dj IIx shall be the Demos state D EL RL with all the hold t commands removed and all times both in the event list and the resource lists set to zero If priorities existed in Demos and they do not we would equalise these too Where the first command of a process in the event list is getR r 1 and r is unavailable in RL the re maining body of code of the process is placed with the other kernelised process information in the waiting list of r The resource list of the kernel state has no extraneous resource entries that is there are no entries r ff where r is not referred to by any process We shall assume that the operational semantics are extended to maintain this property The following lemma asserts that the the corresponding kernel state for a non parallel process belongs to the equivalence class We use the notation RL
50. ds in a state so does another e The multiplicative conjunction of two propositions will hold in a state Ra P E o w if the state can be partitioned into two parts the partition being of resources and processes with one part making p hold and the other making hold e Multiplicative implication relates to the addition of resources or processes Ra P y v holds if all states in which y holds when composed with the state R lt P give states in which v holds e A y will hold if a state can evolve to a new state by a single action a A in which p holds given no change in the resource component of the state Similarly A y holds in a state if all transitions labelled a A lead to states in which p holds again with no change in the resource component 68 e R lt P H A o will hold if by some action o A there is a transition to a new state with a larger resource collection R a P gt R amp S a P with c S and RyS lt P E v Similarly A relates to all transitions with labels in A leading to states in which a proposition holds e Dually the negative multiplicative modalities relate to transitions leading to states with smaller resource collections They relate to transitions of the form RWS a P R P with the difference in resource specified by o S e Finally because our pre order is an equality our logic is classical so we have negation This allows us to assert that a proposition do
51. e Knaster Tarski theorem the function has least and greatest fired points that is there are least and greatest sets that are solutions to the equation Z p Z These shall be denoted Z p Z and vZ p Z respectively For reference the semantics of the fixpoint operators u and v is given by KZAZ II S15 2 Ns and lvZ e Z l Utsls c leo 4We shall see later that we should have used C rather than 19 One of the difficulties of writing formulae in modal is deciding which fixpoint operator to use and for the reader understanding the meaning of this choice We may gain some intuition if we consider the way in which the fixed points may be constructed To construct the least fixed point of a formula X e V X for the state space illustrated through Figure 1 1 we would start with the formula holding nowhere that is X 0 We shall call this the zeroth approximant written X Fig 1 1 a Now one application of the formula later we have X lo U the set of states with no transitions from them this is precisely the set of states where o holds or every transition from the state leads to a state in Fig 1 1 b This series of approximations continues until a fixed point is reached Fig 1 1 d C ens O 0 0 ii Q O O Q O O a Zeroth approximant b First approximant o o O 6 e 0 0 ME O OL O O O O c Second approximant d Least upper bound Figure 1
52. e for cleanly terminated states The restricted subset of Demos considered here has the useful property that one can deduce what resources are held by a given process by examining the code of the process under the assumption that the process code is well formed only puts resources that it holds for our restricted language this property can be checked syntactically Consequently we do not need to store this information e g in the process term The declaration of each process the Entity command attaches to each non parallel process a label Label where Label is the set of all process labels A process P labelled shall be written Pig For example if the jobbers in the jobshop example are called Bob and Alice we would write Jeo Il Alice The process label shall be included in the action label of any transition derived by a non parallel process so that in the process logic we will be able to determine which process is acting We shall illustrate this in the first rule defined below and in the definition of Entity otherwise for clarity it shall be omitted Moreover in the sequel except where this label is of particular interest to us we shall omit the process labels We shall assume that o allows labels to be carried through from sub derivations 2 3 1 Resource actions We commence by defining how processes acquire and release resources in cDemos To get a resource a process simply removes the resource from the collec
53. e r is not in R the available resource collection of g D or in R the available resource collection of g D Consequently irrespective of whether the process descriptor was in EL or waiting on rin RL we can derive no transition from g D nor can we from g Dr Thus g D g D P hold t Then g D R lt hola t the corresponding kernel state Di gives g Dk R lt fe Neither of these processes may make any observable transition hold t may only make a silent transition P P P Without loss of generality we may assume that P a body where a is a single command Consider the cases for a a getR r 1 Then P getR r 1 body and g D R a getR r 1 body There are two cases to consider either r R iff r t RL or r R iff r ff W RL e r R We can derive no transition from R lt getR r 1 body In the kernel g Dr R a getR r 1 body irrespective of whether body was in the waiting list of r or getR r 1 body was in the event list which we can derive no transition from e re R Then R R r and we may only derive the transition R r lt getR r 1 body gt R body Kernelisation yields D where the process is in the event list because r is available so g D R r a getR r 1 body from which we may only derive the transition R r lt getR r 1 body R lt body Now let D be the Demos state D body getR r 1
54. e really can deadlock Theorem 5 4 3 Soundness of deadlock detection 5 1 Ra P Fs Hany any VIp gt Ro P Fa any any TV IP PROOF If we dissect the formula 3 y7 any V Ip it expresses that any T VIp holds in some state reachable from R lt P Suppose then that the synchronous transition system leads to a state R a P Es any T V Ip By Lemma 5 4 2 we know that we can reach this state in the asynchronous system We must then show that R a P Ha any T V Ip Firstly notice that any T V Ip is logically equivalent to any T p Consequently from the semantics of A we have R a P E p As this is not 83 a modal formula the differing transition system will not affect its satisfaction so R a P Ha p All that remains to be proven then is that R a P Es any implies R a P Ha 7 any T Assuming R a P Es 7 anyT there are two cases to consider holds and does not hold If x does not hold we are unable to derive a transition using the asynchronous parallel execution rules and the synchronous parallel rule may not be used Immediately therefore we are unable to derive any transition in the purely asynchronous system so R a P Ha 7 anyT If x holds we know that there is at least one process with a non interfering command at its head Furthermore we know that if this command isa get
55. e the scope of our work we shall analyse the behaviour of processes when they interact through the acquisition and release of resources To borrow Robin Milner s famous jobshop example Mil89 consider two workers called jobbers a hammer a mallet and a stream of jobs to be done Considering the workers to be processes and the hammer and mallet to be resources we might want to ask all sorts of questions For example would we see a gain in productivity if we gave each jobber their own hammer and mallet A different class of question relates to classical concurrency do the jobbers deadlock not be able to take any action without having terminated Let us suppose that the jobbers are simple folk if they work in isolation they will work happily until the end of their day and will not deadlock They are also tidy folk leaving the resources as they found them at the start of the day so they return the tools to their correct place If the jobbers work at different times of the day we may conclude that they will not deadlock Should though our analysis of the activity of the jobbers take into account the times that they actually work C A R Hoare Hoa85 argues not our analysis would not take into account the outcome of a jobber arriving at work late and then working late a not inconceivable scenario Thus perhaps we should not argue that the system never deadlocks To give a more concrete example and further justification consider t
56. ecting whether any sub process could ever have to wait on a resource It is also interesting to consider the behaviour of the synchronous parallel rule on the following program while T getR r 1 getR s 1 putB t 1 getR s 1 getR r 1 getB t 1 The synchronous execution rule assuming a resource state Jr s tj will contin ually execute the third process Though this is fine with respect to detecting 2The side condition is implicit in the structure of the initial resource component 85 overall system deadlock we will not be able to detect that the first two processes may become stuck they will never pass their first commands so they may both always make a transition 86 Chapter 6 Conclusions We have presented some of a theoretical framework capable of conducting anal yses of discrete event processes that interact through shared discrete resources This has involved taking the Logic of Bunched Implications and extending its semantics to be able to consider both processes and resources In order to de scribe such processes we have taken a simulation language Demos and defined its non temporal action Demos is an ideal language for this task as well as being designed to model concurrently executing processes interacting through shared resources its operational semantics are defined This has allowed us to show that the transition system used by the logic that defines the action of pro
57. ection in the synchronous system dually soundness of deadlock freedom More formally for arbitrary amp A EN there exist K A such that IfR lt P Es any OU any T V Ip then 5 1 R P Fa any 7 any T V Ip l ER lt P Ha ay any T V Ip then a Ra P Es ang AA V Ip 5 4 1 Soundness of deadlock detection In order to show the soundness of deadlock detection we shall firstly show that any state reachable in one transition by the synchronous system is reachable by the asynchronous system Lemma 5 4 1 There exists a finite number of transitions n such that If R lt P gt R lt P then R a P gt R lt P PRoor By induction on the structure of synchronous transition derivations The non parallel cases are trivially true in neither system do we use the parallel execution rules The interesting case is where we have a try command in parallel with some other process as presented in 85 2 The other cases for SPAR follow quite easily from the fact that we can decom pose the derivation using SPAR to form two asynchronous derivations From the fact that the two processes do not interfere otherwise we would not be using SPAR we can deduce that the resources necessary to take both ac tions will be available in the asynchronous case if they were in the synchronous case 82 Returning to the try command case assume that RafPJESUS UH aftry e then P etry eg then
58. ectness of translations 3 7 1 Correctness of g As mentioned before in order to demonstrate that Theorem 3 2 1 that the transition system simulates xDemos is not vacuously true through choosing an artificial definition of g we must show the following property which relates to the soundness of the transition system with respect to the operational semantics of nDemos This is illustrated in Figure 3 1 We make use of the soundness property of the transition system Theorem 3 3 1 and Theorem 3 6 1 Theorem 3 7 1 Let gt represent the reflexive transitive closure of the tran sitions derivable according to the operational semantics Then VD D IL o Act g D gt g D implies Dj gt D PROOF By Theorem 3 3 1 R a P R a P implies f R a P f R a P The property applies for every sub transition to derive R lt P R a P so R a P R a P Now R a P ranges over g Dr so 9 Dx g D implies f g Dx gt FD By Theorem 3 6 1 g Dy gt g Dj implies Dj gt D Finally because g D g Dx g D gt g D implies Dj gt D as required 64 3 7 2 Correctness of f Simularly to demonstrate that we have not chosen an artificial f to make The orem 3 3 1 the soundness of the transition system vacuously true we require the following theorem which relies on the simulation theorem Theorem 3 2 1 and on Theorem 3 6 2 Theorem 3 7 2 Let gt re
59. ecute or it is infinite and all non halting processes are executed infinitely often e An execution sequence is said to be just if whenever a process is always able to take a transition that process will act infinitely many times CES86 describes how fairness may be integrated into a model checker Adopting such a fairness condition in the example of 5 4 2 above would prevent the third process executing through every transition and we could deduce that the system can deadlock It appears particularly important to require such a notion of fairness when we consider a parallel execution rule that may favour particular processes such as the one we defined Non syntactic resource ownership Our approach would be more general had we not relied upon the fact that at a given state it is possible to deduce what resources are held by a process from the syntax of the pro cess code For example if the following were allowed in Demos while putB r 1 or even try putB r 1 we would not be able to deduce from the syntax the resources held by the process It would therefore be necessary to keep a record of the resources held by each sub process in the transition system Just as processes explicitly hold other processes that are synchronised on them we would have ra representing a process P holding resources r s and t We chose not to do this in order to reduce the burden of notation Variables Most programmers will recognise the
60. el sets II and Qg Looking at the definitions of g and f they do not seem to lose any information about the state For some v Demos state in the kernel D Ik given its representation in cDemos g Dp Qk we would expect to be able to determine Dp Similarly given f R lt P we would expect to be able to determine R lt P We ask then the question does f undo g and g undo f Theorem 3 6 1 For any state D Ilz f g Dr Dr PROOF OUTLINE By induction on EL WL where WL is the list of processes waiting on resources 3 may be read as list length We shall refrain from giving the normal recursive definition 62 First consider the resource list and note that the collection of resource labels is preserved as is the availability of each resource Also notice that the each non parallel sub process label is preserved The interesting case is where EL WL 1 and the only process is in the waiting list of some unavailable resource r WL Applying g gives a process with getR r 1 at its head and application of f removes this putting the process back into the waiting list of r Notice that we do not consider the case where getR r 1 is the command at the head of the event list and r is unavailable as this is not a kernel state Therefore we do not have a problem deciding from g D whether a process has or has not yet executed the getR r 1 command T
61. em 15 4 UIA U S Sem 3 SYNC 4 S Sem Bia Tr Sem a le Ds Ul 14 le PAR 15 4 U A U S Sem 1 Tr Sem a TA UA U We shall now allow the left user process to take the semaphore m GETS 1 Pr Sem a A U getS BE ee Da T DEM semS PAR semS y i 1 Tr Sem lt 4 04 07 51 5 lt m sz i 0 As there are now no processes waiting in semS the right user process cannot proceed and so the critical region is not entered 44 class sem while sync semS Trace Im back n Entity theSem sem 0 class User while getS semS 1 hold 5 Trace Have s n putS semS 1 Entity U1 User 0 Entity U2 User 0 Hold 50 Entity U3 User 0 Hold 50 HOLD 0 CLOSE Figure 2 4 Semaphore source code 45 Following two T transitions to skip the hold 5 trace C have part of the ac tive user process we may re activate the semaphore process PUTS putS semS 1 U l is Tr Sem sems putS semS 1 U OS Tr Sem sems PUS 2 aU Tr Sem Da PARI la v P 2 afU Tr Sem A U A T transition will remove the Tr part of the semaphore process which is just 8 trace command We may derive all following states using similar derivation trees So starting again we could obtain this sequence US lt U U Sem 1j s IA UqUl Sem 15 lt 4 014 U Sem ae 15 lt A UA
62. en these states This defines a Kripke frame essentially just a set of states with transitions between them We then define an evaluation function for propositional atoms in each state h s p T L an alternative notation to this is s p gt h s p A modal logic allows us to write formula over the transitions between worlds in the frame So for example we can write given that I am in world s in every reachable world something holds Regarding worlds as program states the relation between worlds as time or program execution we obtain an important type of modal logic temporal logic We see that temporal logics allow us to reason about the activity of processes In their simplest form they allow us to make assertions about the state of a process after one execution step this is easily generalised to multiple steps as shall be outlined below 1 3 1 Hennessy Milner Logic Here we shall give an account of Hennessy Milner logic which was introduced in HM80 HMS5 Our notation shall follow that presented later in Mil89 in 1 3 2 we shall generalise the following definition to match the system of Mil89 Firstly in order to create a well founded inductive definition of modal formule we shall need to define when an atomic proposition is satisfied The definition is straightforward a state s satisfies an atomic proposition p written s p iff s p where p is the set of states in which the proposit
63. ence RL r ff W RL where W is W with P PD body attrs t inserted at the appropriate point g S R lt getR r 1 body gg V where gr R R V No tice that by the definition of gg gr RL R V getR r 1 body Consequently g S R agg V getRr1 body which thanks to the associativity and commutativity of the parallel composition operator is g S Now as IM by definition is reflexive we have g S g 5 or equivalently g S g S as required As we stated earlier we must also show that g faithfully translates states belong ing to the operational semantics A number of preliminaries must be covered first so this is presented in 3 7 1 3 3 Soundness of transitions As we have already stated we do not have the obvious soundness property stating that any transition derived by our transition system could have been derived according to the operational semantics The transition system was designed to take no heed of synchronisation by time nor does it take into account the priority of processes We should though be able to prove soundess with respect to the operational semantics with the following assumptions 1 All event times are ignored i e t 0 or some other arbitrary constant for all PD entries 2 All priorities are ignored 3 The orders of the event list and waiting lists consequently are arbitrary 4 When a resource
64. entation so far has failed to take into one thing into account we do not necessarily want to consider processes executing synchronously Take for example the following processes p E getR r 1 getR s 1 putR r 1 putR s 1 p do 2 putB b 1 JgetR s 1 getR r 1 The only path derivable from here using the synchronous rule is lr s lt PiP etR s 1 putR r 1 putR s 1 ors ee 1 je 1 getR r 1 getR putB putR r 1 putR s 1 mad bb getR s 1 getR r D getR putB gt By executing synchronously we missed the deadlock that would have occurred if the two putBs had executed first In effect the transition system that we have described so far in this section could be simulated in the operational semantics by removing all hold commands and inserting hold k for some constant k between all the other commands How then can we reconcile our desire for a state space reduction with the necessity of considering all interactions between processes The answer lies in 78 identifying which commands could affect the execution of other processes we shall say that they interfere with other processes We can choose to branch only on these commands whilst executing non interfering commands synchronously So for example if a process has a series of commands on a resource that is not referenced by any other process we will not introduce any new paths to be examined when m
65. es not hold in a given state The inclusion of negation makes redundant we could use the equivalence y v p Vw If we want to reason about an arbitrary type of action occuring we would form the disjunction of diamond modalities or the conjunction of the box modalities We shall introduce the following abbreviations R lt P E Alanyy iff R lt P E Alzes Alis A Ale new Rs P E A anyy iff R lt P F C sewto V A new V 4 Recalling the definition of Ir the formula r Ip holds in states where r is the only available resource with an arbitrary process term We shall soon see a formula representing r being one of the free resources Recalling the definition of Ip the formula P Ip holds in states where P is the only process in the state with an arbitrary collection of resources 4 2 Deadlock in PBI As presented in 1 3 2 deadlock freedom in Hennessy Milner logic is defined as D A AHAT iENU w We must make a few adaptations to this to make it suitable for us Firstly we must select an appropriate modality we shall choose the any modalities Secondly we wish to relax the requirement that the process never terminates to requiring that if it is in a non terminated state it can take an action We do this by requiring Ip the proposition indicating clean termination or non termination in every state Consequently the PBI formula for deadlock freedom in Demos is DP A Tay A anyT Vip icN
66. espect to the operational semantics in the familiar sense This is to be expected we intentionally made the transi tion system non time sensitive and so transitions derived may not be possible according to the temporal time based constraints actually in place mDemos allows us to consider the essential aspect of Demos programs the interaction of processes through shared resources In essence there are three main commands getR The command getR r 1 acquires one item of r from the globally avail able resources thus making it unavailable to other processes If r is not available at the time of request the process will wait until it is available putR The command getR r 1 releases one item of r making it available to all other processes If a process is waiting for the release of r it will be activated Otherwise it will be placed in the resource pool 49 hold The command hold t signifies that the process waits T time units before resuming execution We shall assume that processes have been initialised correctly failing to make this assumption adds little to the presentation Therefore we will not consider Entity etc State in the operational semantics is represented by a 3 tuple S EL RL X e Sisa function that records the various syntactic definitions found within the system It will contain for example class definitions and resource labels As we are not going to consider any commands that manipulate X e g c
67. et of processes waiting on a resource r is given by def wp r PI KIP r wa TP R2 We are now in a position to define our translation f FR lt PD EL RL 55 where EL RL Wr dody a a P R A attrs hp body t 0 Y Lr tt st re RSW r ff W st re IPD PD body hp body 0 s t body wp r PD body attrs t We shall now proceed with the body of the proof which shall be by induction on the structure of cDemos processes Theorem 3 3 1 The transition system is sound with respect to a non time and non priority sensitive operational semantics That is If R 4 P R a P then F R a P f R P PROOF By induction on the structure of o Demos processes P P hold t TS Op sem We may only derive the transition R a hold 4 R lt e FRa P P PD hold t attrs 0 RL Executing the hold yields EL P PD attrs 0 Given the well formedness of states attrs so another execution gives EL RL RL Notice that f R lt el l RL EL RL P getR r 1 TS Op sem Assuming that we are able to make a transition the resource must be available so R R r for some R We have the transition R r lt getR r 1 gt R lt e Without loss of generatlity thanks to the arbitrary order of the resource list because r is available we may assume that f R lt
68. he case as it is with BI that we can define several semantics for the logic whilst preserving the correctness of the deduction system We choose to consider one of the simplest and the one that can have the simplest notion of resource the Kripke semantics The Kripke semantics of BI allows us to define the semantics through a math ematical structure called a monoid M gt M e o C 11 where M represents a domain for our monoid e represents the identity element under composition o is commutative and represents the composition of elements of M and Lisa pre order on M The semantics of BI based upon this monoid is given in Table 1 1 Let m M p be an atomic proposition y range over propositions and pll M be the set of states in which the proposition p holds Then the Kripke semantics is given by mp if me pl MEPAY iff m E v and m Ev MmEPVY iff meEpormewy mbowv iff forallnEm n H implies n v meypey iff forsomen n M mEnon and n y and n ky m E p y iff forallne M nkE q implies mon E y Table 1 1 Kripke semantics of static BI There are two types of operator in the logic additive and multiplicative The additive operators A and are just as in intuitionistic propositional logic A is used to indicate that more than one formula holds in the state and is implication More interesting are the multiplicative operators In
69. he com munication network of Figure 1 a Nodes represent intelligence agencies in the UK and the US and arcs represent dedicated secure communication channels perhaps based upon quantum encryption that can only be owned by one node at a time in a sense they are resources The hub in the centre of the diagram is capable of serving many lines at once and represents no limitation on the system It is important to abstract away the irrelevant when modelling so we 1 We could also consider the hammer and mallet to be very simple processes which alludes to the consideration of resources as processes under certain circumstances shall ignore its behaviour Suppose that MI6 has a process that starts every day at 12 43GMT which sends some data from MI5 to the FBI To do this it claims ownership of the MI6 line followed by the MI5 line then the FBI line Once a process in this case an intelligence agency starts to get a line no other process can start to get the same line Between each acquisition a 2 minute pause occurs to allow some handshaking protocol to occur Similarly the CIA has a process that starts every day at 12 40GMT which sends information from the FBI to MI5 in doing this it claims the CIA line the FBI line and then the MI5 line These processes are rpesented in in Figure 1 b What normally happens is that the CIA process has control of the MI5 line before MI6 tries to acquire it Consequently the MI6 process waits
70. heorem 3 6 2 For any state R lt P Q note that we do not require that R lt P be in Qk LAR lt Pa R lt Pa PROOF OUTLINE By induction on the structure of RafPJ We first note that the action of g after f on an arbitrary state R a P results in the same re source collection R We also note that the labels of non parallel processes are preserved Again there is essentially one interesting case If P getR r 1 body and r R body will be placed in the waiting list of r in R a P g will restore the getR r 1 command Otherwise for a non parallel process the code will be placed in the event list of f R a P g will not add anything to the front thus restoring R lt P A bijection between two sets A and B is a function that maps every element of A to exactly one element of B with every element of B being mapped onto exactly once Corollary 3 6 3 f is the inverse function of g or equivalently g is the inverse of f when we consider the sets of kernel states That is for D II and R a P Qk 7 gf Ra PD amp R lt PD and f g Dx Dx Consequently g is a bijection from 9 to II and f is a bijection from II to Or PROOF The proof is immediate from the above theorems and the definitions of inverse functions and bijections 63 May contain hold t No hold t Figure 3 2 Bijection between kernel and transition system 3 7 Corr
71. here gr RL R W Similarly we have g S R lt a ge body W where gr R R W By the associativity and commutativity of parallelisation this is just the same as the state derived by executing the hold in the transition system R a ho1d t body R lt body gz EL W putR r 1 There are two subcases for this instruction Nothing is waiting on the resource Then S P PD putR r 1 body attrs t EL RL After we have exe cuted putR we have state S P PD body attrs t EL RL We know that r was previously unavailable so without loss of generality thanks to the order of RL being arbitrary RL r ff RL and RL r t RL Now g S R lt putR r 1 body gg W where gr RL W R With appropriate selection of parallelisation and sequential composition rules we can derive the transition R lt putR r 1 body gg W gt R r lt body ge EL W the actual label j putR is unimportant so shall just call it o Consider g S R lt body gg W by the definition of gg because no processes were waiting on r W W and R R r so we have the the state obtained by the transition system There are processes waiting on the resource S is as before After putR we have S P PD body attrs t EL RL Assume without loss of generality that RL r ff P3 PD bodyi attrsi t1
72. ing a new line from the hub to the FBI Would this result in deadlock freedom The question would be posed in the logic as D 10 F 6 5 a P F D The only state model satisfying F is F f e Thus to answer the above question we must resolve satisfaction of 1C F F 6 5 f a P DP It turns out that this is true either the CIA process or the MI6 process may end up blocked but the other will eventually release the resource that it is waiting on The multiplicative modalities are also quite interesting we could now use the positive given the possible inclusion of processes a better term might be compo sition modalities 4 and Alf to indicate a new process being generated This occurs with an Entity command and would require to be extended by T ney 1 lt class Similarly we could use the positive a better term now might be decomposition modalities to indicate processes being removed This could be through the termination case of parallel composition or through an explicit kill command which does not exist in Demos With such rich multiplicative modalities it may be desirable to exlude the case where the number of processes changes in this manner from the additive modality Further consideration of this though is beyond our current scope We shall therefore use the additive modalities for Entity declarations etc and leave and defined only where necessary on the resource actions It should
73. ion for P By induction we can make no transition for a sub process in the synchronous system so we can derive no transition for P in the synchronous system To prove the completeness of deadlock detection is quite complicated We shall therefore present only an outline of the proof Moreover we shall consider only acquisition through getR the cases for getS and getB are similar as is acquisition through try lAn alternative proof would note that this case is vacuously true if x holds we must be able to make a transition so we must be able to make a transition in the asynchronous system We have given the full proof to illustrate how we could prove the property with a more relaxed condition 84 Theorem 5 4 5 Completeness of deadlock detection 5 2 If there is a path to a deadlocked state in the asynchrounous system there is a path to a state in the synchronous system That is for arbitrary R lt P R lt P Fa any any V Ip gt R lt P Fs any any V Ip PROOF OUTLINE We start by assuming an arbitrary state R lt P such that R a P Ka any T V Ip This is equivalent to R a P Ha any T A Ip By the semantics of A R a P Ha 7 anyT and R lt P Ha p By Lemma 5 4 4 we see that R a P E 7 any Whether Ip holds in a state is independent of the transition system so R a P E Ip Now notice that the only rule we
74. ion holds Similarly the definitions of conjunction and disjunction follow the additive cases of Table 1 1 s p q iff s H p and s H q and s pVqifs pors Hq Suppose that a process is in a state s If by some action in a set A a transition from s can be derived to a state in which a possibly temporal formula p 15 is true we write s 4 p where A is pronounced diamond A If all transitions derivable from s by actions in A lead to states in which p holds we write s H Alp pronounced box A In a more formal notation Definition Simple modalities sE A p if Ja s ac Aand s 5 s and s Ey sE Aly if Vo s acA and s 5 s implies s p Pictorially these express the following S 9 SEC 9 S 9 sE e gt Assuming the existence of negation within our logic it is not hard to see that the following eguivalence exists between the modalities Ap c A e We may choose then only to define one of the above modalities within the basic logic and define the other to be a derived modality In the sequel it shall be convenient to use an abbreviated syntax to define the action set Assuming that the set of all action labels is A we shall write a a for a a A for AMA a a for A a a for In particular we shall make use of which abbreviates A The obvious symmetric
75. is released it is not necessarily a waiting process that acquires the resource it could be either a process in a waiting list or a process about to enter a waiting list i e with getR at its head In order to prove the property we firstly need to define the map from the transition system state to state in the operational semantics f We use a number of auxiliary functions 54 hp defines the resources held by a non parallel process note here that we assume that the programs passed are well formed that is they only put resources that they own etc denotes subtraction from a multiset hr 5 hp getR r D P he Pl tr hp putR r 1 P np ppetrj h shall be the multiset of all held resources KAN ANADAN A P E hp P P not parallel wg defines the multiset of process resource pairs where the process is waiting on the resource wa R Y wa P Q R wr P W wr Q wg c P R der ULP r 5 m andr R w is just the multiset of waiting processes without the resource that they are waiting on w P R t P st G LP we P R 5 mset simply splits parallel processes into a multiset of non parallel pro cesses mset e Y mset P E P where P not parallel mset Pi P gt 1 def mset P 8 mset P2 The multiset of active processes is just the multiset of all processes minus the multiset of waiting processes a P R E mset P V w P R The s
76. ive and multiplicative modalities into our process logic Presented in Table 1 4 the additive modalities describe process evolution with out a change in the resource component For resource formule yp such a defini tion would allow the arbitrary introduction and removal of additive modalities R lt a P yr er RForm R lt P E er and similar for box and elimination rules where yr RForm inicates that PR is a resource formula DLa 1 4 2 Multiplicative modalities We shall define four multiplicative modalities ew dew new and new in Table 1 5 In contrast to the additive modalities we do not have the arbitrary introduction of modalities to resource propositions Intuitively they refer to transitions that involve contraction or expansion of the resource component The distinction between the diamond and box modalities is conventional the diamond modalities refer to the existence of a transition satisfying a property and the box modalities refer to all transitions satisfying a property The dis tinction between the and modalities is more interesting The positive multiplicatives refer to transitions that involve releasing a resource and process component specified by the relation The negative modalities refer to transi tions that acquire or remove a specified resource and process component we denote this using though it could be the same relation
77. lass and cons we shall frequently omit it when discussing state e RL is the resource list a list of 3 tuples id avail WL id is the resource name or label avail tt ff is a boolean indicating whether the resource is taken and WC is a list of processes waiting on the resource non empty only if not avail e EL is the event list P PD code attrs t It is a list of processes not waiting on any resource Processes are represented by a pair comprising a label and the process descriptor The process descriptor is another 3 tuple comprising the code remaining to be executed the resources held by the process and the simulation time at which the next command is to be executed The reader is referred to B T93 for the formal presentation of the operational semantics In the sequel to match the account presented in B T93 we shall only consider one item get put with each identifier in the resource list being unique that is only one of any resource shall exist 3 2 Simulation We shall represent the globally available resources in the transition system by R Process terms shall be bracketed P The state of a program in the transition system is of the form R a P an equivalent representation in the operational semantics shall be written f R lt P Transitions derived according to the operational semantics shall be denoted gt note that this is unlabelled to distinguish it from observable transitions made in
78. lding the conjunction It expresses that the process is not stuck in this state that every state reachable in one transition is not stuck and so we can perform another transition that every state reachable in two transitions is not stuck and so we can perform another transition 1 33 CTL The Computation Tree Logic of CES86 allows some temporal properties to be expressed more simply than the Hennessy Milner logic described above does as well as being more amenable to model checking The definition of CTL in CES86 requires that the transition relation is total i e every state has a next state We regard this as unreasonable for our purposes so we shall not require this Letting AP be the set of all atomic propositions the following two rules induc tively define the class of CTL formule 1 Every proposition p AP is a CTL formula 2 ara f p and v are CTL formule so are y y A v y y YlpUy and gU LLI 17 The semantics attached to the formulae composed of first order propositional logic operators is conventional as for the box and diamond modalities Y pU y intuitively means whatever path is chosen from the given state p will hold until v holds and b actually does hold somewhere Similarly J3 pUv intuitively means a path can be chosen where p holds until holds and b actually does hold somewhere A path is an possibly infinite sequence of states s0 1 where Vi gt 0
79. lusion of an arbitrary number of e processes Thus 1f lt e is the identity element under o The semantics of PBI following from these definitions is presented in Table 4 1 Finally we must define the relations and for the multiplicative modalities These define respectively the resources acquired and released by particular 66 R lt P Er Ra P EpAw Ra P evwv R lt P F e Ra P R lt P F Ra P R lt P Ra P H 4 R lt P E Ala R lt P F Aa R P E A cM pew R lt P e R lt P Ra P Ra P R lt P Ip Ra P iff iff iff iff iff iff always for any iff iff iff Ra P R a P a 15 4 Q Ra P Ra P Ra P RaP for all S lt S Q Q 2 for some e A R lt P Ra R lt P p for all a A R lt P Ra R lt P p Ja A a Sa Q and R lt P and RWS Va A a Sa Q and R lt P PQ a lr 5 ale y and R lt P y or Ra P y p implies R lt y implies RWS lt P Q E Y PES for some S a Q S a Q e 2 SwS lt Q Q and S lt Q E e and S a Q Ev l S P and P implies 5 RuSa P lg 5 9 2 Ru S a P Q implies RWS a P llQ E y dac A a18S and R lt P and SW T and T lt Q3 Vac A a S and R lt 4 P and Sw T
80. mmand at the head of the event list We may assume without loss of generality that the choice of the transition to make is decided solely by the command at the head of the event list Generality is not lost as this provides an arbitrary selection from the processes with equal but still the least event time assuming insertion order is arbitrary where equal event times occur The event list is empty We have S RL According to the operational semantics the program halts with an error As there is no next state the statement is vacuously true Lead object has no actions left We consider two cases attrs amp Then the program halts with an error so again the statement is vacuously true attrs Then S P PD t EL RL The operational semantics gives S EL RL By the definition of gg g S g S and as i reflexive we have g S 2 g S as required close Then S P PD close body attrs t EL R The operational se mantics tells us that the program halts and that there is no next state so the statement is vacuously true hold t Then we have S P PD hold t body attrs evt EL RL By ap plying the rule for hold we obtain S EL RL where EL is the same 52 as the original event list with t added to evt and consequently causing a re order of the event list and hold t removed Now g S R a hola t body ge W w
81. n in which there is a knife a pair of scissors a mother and her child The mother uses the knife and then the scissors before returning them Adopting our Demos representation for processes and letting k represent the knife and s the pair of scissors her activity is modelled by the following sequence of actions Pm getR k 1 getR s 1 hold 5 putR s 1 putR k 1 The child only wants to use the scissors for a short period of time and they are not allowed to use the knife Their Demos representation is P getR s 1 hold 1 putR s 1 We want to ask if having the mother and the child in the kitchen at the same time will cause deadlock Letting putative consequence asking whether a formula is satisfied in a particular model be written the question is represented formally by l5 k f aLPm P 97 In the logics presented above HML CTL and modal the complexity of model checking such questions increases as the state space generated by the transition system increases Figure 5 1 shows the program fragment of the states that may be generated using the transition system with the parallel composition rule presented above Branching occurs where more than one transition is derivable from a particular state there is non deterministic choice of the next state to enter into For example at state 1 1 either the child may take the scissors or the mother may take the knife For the transition system presented abo
82. odel checking We shall therefore require a condition that dictates when to use the synchronous parallel rule and when to use the asynchronous rule s To capture intereference some auxilliary functions are required Firstly the multiset of resources accessed by a non parallel process res getR r n def Ir J res putR r n E irj res getB b n 1 res putB b n bj res sync z de lsync x res getS x n e sync x res c P e res c w res P res c C de res c W res C res pc en EJ res e1 res es y res P Y res Pa i 0 where sync_x is a token indicating synchronisation on a pool 2 res anything else The command that may next be executed by a non parallel process is its head defined as follows def head c c head c P EJ The function res shall return the multiset of resources accessed by parallel processes res ie Sy rea P Q res P wres Q P not parallel Take the set of indices of a parallel process P to be Inp that is if P Pil P4 then Inp 1 n The set of indices of non interfering pro cesses processes with non interfering commands at their head shall be written Cp defined as keIp i def cnt f To ensure that the synchronous parallel rule does not prevent us entering the true deadlocked state we shall also require that it only be applied to processes that are able to act This set of processes is res head P A
83. odels Proving that the assumptions behind such models are met for example that the time between packet arrivals follows a negative expo nential distribution though is somewhat more complicated and subjective simulation has the same problem manifested in the problem of how to choose the distributions or sample data that we use to parameterise the simulation We must now move on to decide upon the type of system that we are to model Naturally we cannot hope to provide a mathematical model for all types of system able to answer all types of guestion We shall consider a notion again familiar to computer scientists that of processes and give the definition found in DED73 Process A continous and regular action or succession of actions taking place or carried on in a definite manner a continuous natural or artificial operation or series of operations Central to our analysis of processes of course shall be the environment in which they operate In particular a process may be acting in an environment with other processes we shall say that the processes are acting in parallel or concurrently It has long been known before even the first parallel computer was built that it is difficult to reason about parallel processes as noted in the very first item to appear in the Communications of the ACM Per58 Our work to provide some degree of automation should therefore be of some value In order to further restrict th
84. ommunication and Concurrency International Se ries in Computer Science Prentice Hall 1989 Series editor C A R Hoare Zohar Manna and Amir Pnueli How to cook a temporal proof system for your pet language In Proceedings of the 10th ACM SIGACT SIGPLAN symposium on Principles of programming lan guages pages 141 154 ACM Press 1983 Faron Moller and Perdita Stevens Edinburgh Concur rency Workbench user manual version 7 1 Available from http www dcs ed ac uk home cwb Tadao Murata Petri nets Properties analysis and applications Proceedings of the IEEE 77 4 541 580 April 1989 OED The Shorter Ozford English Dictionary Oxford University Press third edition 1973 Peter W O Hearn and David J Pym The logic of bunched impli cations Bulletin of Symbolic Logic 5 2 215 243 June 1999 Pawel Paczkowski Proving total correctness of concurrent programs without using auxilliary variables Technical Report ECS LFCS 89 100 University of Edinburgh Laboratory for Foundations of Com puter Science November 1989 Alan J Perlis Announcement Communications of the ACM 1 1 1 1958 Letter from Saul Gorn Andrew M Pitts Operational semantics and program equivalence In G Barthe P Dybjer and J Saraiva editors Applied Semantics Advanced Lectures volume 2395 of Lecture Notes in Computer Sci ence Tutorial pages 378 412 Springer Verlag 2002 International Summer School APPSEM 2000 Caminha Portugal
85. ons which describe real action within the system and simplification ac tions which describe for example modifications to syntax Though it may be considered desirable to define the transition relation solely in terms of reduction transitions using a number of auxilliary relations to describe simplification labelling allows us to make explicit the r le of each transition Furthermore labelling shall allow finer queries to be made in the modal logic as shall be indicated later though non labelled systems are commonplace e g MP83 As we have already stated when we come to desribe Demos we shall be consid ering the interaction between processes working on resources In particular we shall consider the available resources within the system that is those that have not been acquired by any process This shall be described by a multiset we let R R range over such multisets of resource and P P Q range over the code remaining to be executed We shall call R a P a state of the transition system Transitions are of the form RafPJ gt R a P We read this as Initially all the resources in R are available and we have an active process P After an action a the resources in R are available and the active process is P We distinguish two classes of transition o transitions and 7 transitions o transitions indicate action and 7 transitions indicate silent or invisible actions related to the simplification rela
86. our theoretical approach could well be extended to a notion of continuous resource Thus the system developed herein shall operate on discrete event discrete resource processes Not coincidentally we shall consider a simulation language Demos that has both these properties MI6 line MI6 CIA line MI5 li FBI line a Communication network MI6 CIA Get MI6 line Get CIA line Get MI5 line Get FBI line Get FBI line Get MI5 line transfer data transfer data Release all Release all b Communication processes Figure 1 Intelligence agency network and process design 00 eL 8 2 9 24 vS cL AN 0 2 9v cL 9r cL vel An Orci MI6 MI6 MI6 CIA CIA MI6 CIA MI6 CIA CIA End transfer get FBI End MI6 Take MIS transfer wait for MI5 get MI5 start get MI6 get FBI start get CIA a Normal execution 00 1 8S cL 9S cL vS cL cz 0S cL 9v cL 9v ci YvcL crcl Orci No activity deadlock MI6 wait for FBI CIA wait for MIS MI6 get MI5 MI6 start get MI6 CIA get FBI CIA start get CIA b Deadlocking execution Figure 2 Intelligence agency process execution 10 Chapter 1 Logical Framework 1 1 The static Logic of Bunched Implications The Logic of Bunched Implications OP99 BI allows us to reason about re so
87. present the reflexive transitive closure of the tran sition relation gt Then for all RafPJ f R lt P AR lt P implies Ra P R lt P PROOF By Theorem 3 2 1 for all D D c II D D implies D 5 g D Now f R a P F R a P IL so f R lt P F R P implies g J R PP gt g R lt 1P Theorem 3 6 2 gives us f R lt P F R a P implies R a P gt R a P7 as required 65 Chapter 4 Demos and PBI We have now defined in abstract terms the logic that we shall use PBI and a transition system for Demos programs It remains to consider how we integrate the two and what we are able to express in the resulting system 4 1 PBI and cDemos Recall that the definition of the semantics of PBI given in 1 4 was by a monoid M Res x Prog e E The monoid that we shall use to define the logic for Demos models shall be denoted Mp Mp He R x Proc 5 e p The composition relation o combines states in Q R x Proc It simply forms the multiset union of the resource component and the parallel composition of the process component R lt P o S lt Q Rw S lt PQ The comparison pre order is a simple equivalence R lt P 8 lt Q 4 R SAP Q considers pairs to be equal iff they have the same resource multisets and their process terms are the same up to the commutativity and associativity of parallelisation with the inc
88. pression we shall introduce a new syntactic abbreviation for the parallelisation operator that operates outside the semantic brackets Pi Po P R Pi e Pi We shall define g through three auxilliary functions e gp shall convert processes in the event list to transition system processes gal fel gE P PD c gn EL g e P PD attrs t EL E a EL def lel if b close yeke ellemeye i E b body p l lg otherwise gw Shall convert lists of waiting blocked processes to processes of the transition system wer fel gw r P PD body attr t WL getR r 1 body p li law WL To convert the resource list ident avail waiting R B Proc we shall define gg R B Proc gt R Proc the operator shall combine these pairs def R Pea SU S Qua Rw S Pen Qua 51 or S QD gr r tt RL rS fel e gR RL gr r E W RL U gw W e gr RL We may now define our map between states in the two systems g EL RL X Rage EL W where gr RL R W Theorem 3 2 1 Let S EL RL be a reachable state in a y Demos program which evolves in one step of the operational semantics to S EL RL Then this is simulated in the transition system That is for some series of o If S 9 then g S 4 g S Proor By analysis of the cases of next command to be executed the co
89. red markings before and after a given transition arrows As described in POY02 Pym02 it is possible to encode Petri nets in BI We denote composition of markings M and N M N and define _ Jj 0 Mp 0ANp 0 M Nyp 1 otherwise This restricts our attention to the variant of Petri nets where at most one token occurs in any place shall denote the empty marking i e for all p p 0 We consider only finite Petri nets so dom M is finite 26 a b c Ho d omo ls e Figure 1 4 1 4 a goes to 1 4 b 1 4 c no action blocked by post condition 1 4 d no action not all pre conditions met 1 4 e goes to 1 4 27 Thus POY02 defines a pre ordered commutative monoid M E Petri nets therefore give semantics to BI We represent action transitions between Petri net markings using C So for example N C M iff from M a number of transitions lead to a marking N This interpretation makes in a sense a global temporal operator similar to VG in CTL m E Y vy is true if in all reachable states if is true then w is true We also lose the ability to describe only the current marking using multiplicative conjunction As mentioned before we chose to allow only one token per place in each marking Depending on the application it would be quite easy to generalise away from this restriction we would simply take M N P gt N and M N p Mp
90. res AR ili Inp head P getR r n gt res head P R 79 We shall execute all non interfering processes synchronously until there are none left at which point we shall use the non deterministic asynchronous parallel rules Thus the condition is ChnABEO 4 The synchronous parallel execution rule then is R WH lt P gt H lt P SPAR EXE 4 Her Ri P 7 Ha lker Peller P7 The asynchronous parallel execution rules are unchanged other than having the condition In Figure 5 3 we present an example series of transitions derivable with this rule Notice that there is no choice of which transition to derive this particular path is derived completely deterministically from the given state Following a T transition to remove the null process we would now use the asynchronous transition rules to consider the interfering executions Figure 5 4 shows ther reduced state space of the kitchen example Notice that the it is much smaller than that derived by the asynchronous system with only one branching point getB r l getR u 1 getR t 1 putR u 1 hold 4 getR s 1 lr s tS lt hold 3 putR u 1 hold 4 C 1 3 putR t 1 putR s 1 getR u 1 getR s 1 getB getR utR u 1 hold 4 hold 4 f ud m d putR u 1 putR t 1 CE putR s 1 getR u 1 hold 4 Rap ca putR u 1 hold 4 putR t 1 C 3 hold 3 putR u 1 putR s 1 getR u 1
91. riables or bins or synchronisations with values Returning to our intelligence agency example we may model the system in Demos by the program of Figure 2 2 The trace omitted indicates no deadlock We shall use the abbreviation e for the null process a process incapable of any action Letting Prog be the set of correct processes derived from the BNF description the set of processes is Code e U Prog Writing for the parallel composition of processes and for the sequential composition of processes see later the following structural equivalences should be taken to 29 Prog Decl cond Res r n Bin r n Entity class t Class name Decl close Prog Prog hold t getR r n putR r n cat putB r n sync z getS x n putS z n try cond then Decl etry cond then Decl while cond do Decl do n Ded reg cond Entity class t hold t Decl Decl getR r n getB r n getS x n cond cond Figure 2 1 BNF syntax of restriced Demos considered cons ACT TIME6 4 cons ACT TIMECIA 4 class MI6 4 getR MI6_line getR MI5_line getR FBI_line 1 hold 2 1 hold 2 1 hold 2 hold ACT_TIME6 putR FBI_line class CIA 1 getR CIA_line getR FBI_line getR MI5_line 1 putR MI5_line 1 putR MI6_line 1 1 hold 2 1 hold 2 1 hold 2 hold ACT TIMECIA putR MI5 line 1 putR FBI line 1 p
92. s gt Si and is the transition relation of the labelled transition system If the path is finite there must be no derivable transition from the last state Using this definition Table 1 3 3 defines the semantics of CTL CES86 gives a relatively straightforward algorithm for model checking CTL formulae where the state space of the given process is finite sop if soe l so Fe iff soy So v uv if so and so Fy so vvv if so H gor so EY so p iff for some state s and action a A a so s and s E p so F y if for all states s and actions a so gt s implies s y so E V yUy iff for all paths so s1 H gt Ol si EVAVIO lt j lt i sel l 50 D pUw iff for some path so 51 LU Table 1 2 Semantics of CTL formule Deadlock freedom may be represented in CTL as DOT 3rTU 4 1 3 4 CTL CTL provides a relatively clear language for expressing how propositions hold through the evolution of processes In many cases however it is sufficient to use a subclass of CTL formula called CTL7 3 As we do not require that the transition relation be total our definition of path differs from that in CES86 in that we allow finite sequences 18 CTL does not have the J3 U or V U modalities but does have JF VF 3G and VG These are defined as follows through the semanti
93. s deadlock Internal Accession Date Only Approved for External Publication Copyright Hewlett Packard Company 2003 Acknowledgements Firstly I would like to thank the Enterprise Solutions Department and HP Labs asa whole for providing such a pleasant working environment Thanks also to David Pym for a great deal of useful discussion on the logical side of this work his contribution to this cannot be over estimated Last but by no means least I would like to thank Chris Tofts for proposing this project guiding me into the subject area provid ing a wealth of knowledge and generally making the time I spent producing this so enjoyable Contents 1 Logical Framework 1 1 The static Logic of Bunched Implications 1 2 Transitions ystems s 2 24 ce yi See E a e a 1 2 1 Labelled transition systems 13 ModalandTemporallogic s 13 1 Hennessy Milnerlogic 1 3 2 General Hennessy Milner Logic 133 KOTE e 4373 ble 3 ch Ie as a ae 199 ODE mm E si e me pe ere Oia he ot 1 3 5 Modal iri O E BAR PASADA A ted l4 Modal BE Syra oiana aiaa Yem Vie ere ene e emini kek 14 1 Additive modalities 14 2 Multiplicative modalities 14 3 Observablevs silentactionss 1 5 Petrineisin PBD 0 20 eo aa a 2 Demos 2 L Introduction ci dak kk x 22 Transition rules uon A A A ee 23 TransitionsystemoDemos
94. tem for our logic Such a system should be proven correct sound and complete with respect to the semantics defined here To conclude we have seen how we can extend the Logic of Bunched Implications to consider processes in a simple manner to achieve an expressive and clear way of formally reasoning about processes that interact on shared resources 89 Bibliography AB96 BS01 BTa BTb BT93 BTO1 CES86 FOL Gir87 GPSS80 HM80 Andrea Asperti and Nadia Busi Mobile petri nets Technical Re port UBLCS 96 10 University of Bologna Department of Computer Science May 1996 Julian C Bradfield and Colin Stirling Modal logics and mu calculi an introduction In J Bergstra A Ponse and S Smolka editors Handbook of Process Algebra pages 239 330 Elsevier http www dcs ed ac uk jcb 2001 Graham Birtwistle and Chris Tofts Getting demos models right Part I Practice Graham Birtwistle and Chris Tofts Getting demos models right Part II and theory Graham Birtwistle and Chris Tofts Operational semantics for process based simulation languages Part l rdemos Transactions of the Society for Computer Simulation 10 4 299 334 1993 Graham Birtwistle and Chris Tofts DEMOS 2000 A Semantically Justified Simulation Language August 2001 http www demos2k org E M Clarke E A Emerson and A P Sistla Automatic verifica tion of finite state concurrent systems
95. the opera tional semantics of Demos Proposition 5 3 2 is not sound with respect to a That is there is a formula p and oDemos state R lt P with R lt P E v but R a P Ka v PROOF With Ra P as before Ra P a anys t In but Ra P Es A anys t Ip This holds even in a system without negation e g consider evaluating s Ir on the first state of the above sequence We postulate though that there is a syntactically defined class of formule for which s is sound and complete We anticipate that deadlock freedom DP is in this class Though the definition of this class is beyond us at the moment we shall proceed to show that deadlock freedom is indeed sound and complete in the synchronous system 81 5 4 Deadlock freedom equivalence in asynchronous and synchronous systems Recall that the formula for deadlock freedom for Demos in our HML type logic is DF A Actlany Act any T V Ip iENU w This formula will be equivalent in both transition systems if e any state reachable in the synchronous system that is deadlocked is also reachable in the asynchronous system and e any deadlocked state reachable in the asynchronous system is also reach able in the synchronous system The first condition relates to soundness of deadlock detection in the synchronous system dually completeness of deadlock freedom the second relates to com pleteness of deadlock det
96. tion of available resources if it is available If it is not the process will not be able to pass the command thus simulating the process waiting for the resource Re leasing a resource is just a case of replacing the resource in the collection The rules for bins and actual resources are the same in oDemos in Demos itself however bins are used to model resources that may be generated or consumed 32 by processes For example a process that must withdraw 50 from a bank account b before executing P should be modelled getB b 50 P GETR getR R r lt getR r n 9 Rafe PUTS P Ra putR r n R r a le GETE ae R r lt getB r n R a e PUTS ae R lt putB r n R r a e Note that in the rules PUT we have assumed that processes are well formed in that we have not checked that they own the resources that they are returning 2 3 2 Hold As we have already stated our model of Demos programs shall not consider time Thus the transition for hold t shall be NOTIME R lt hold t Ra e effectively skipping the command Notice that we have used a r transition to indicate that this is not observable 2 3 3 Initialisation It is also possible to define initialisation of the program allowing a little vague ness by assuming that we are passed the code of class rather than just its name This could be resolved by introducing a f
97. tion of fairness in execution see 96 1 One approach that may be adopted is to only allow one process to execute one step in order to form a transition of the parallel system forming a so called asynchronous transition system The choice of which process to execute is arbitrary or non deterministic R lt P R a P R lt P1 P2 R lt P Po PAR R a P R a Pj R a P P5 R lt P P7 PAR 2 x We must also consider the cases where one of the parallel processes terminates R lt Pi R a e PARre 1 PAR 70 1 Ra P P R PJ R lt P gt R e PARre 2 PAR 702 R lt PP R lt P Alternatively we may define a rule schema to allow easy access to parallel processes One may consider this to be a derived set of rules or consider the above to be specific instances of this this is similar to the Expansion Law of CCS c Pati esum PAR ESI E lt P n gt 1 Rallies 5 Rs Piena Pil iel 34 with a similar rule PAR te See 85 for consideration of a rule for synchronous parallel execution 2 3 6 Process synchronisation A powerful feature of Demos is that it is able to model synchronisation between processes For example a process representing a train may synchronise with a process representing a station to represent loading unloading The train process will once it has placed itself in the sync pool of arrived trains not be able
98. tions described above that perform syntactic operations to expand loops and skip by commands that are not considered An alternative would have been to define an equivalence relation based upon syntax to indicate that we consider pairs of states to be the same For example given that our consideration is of action rather than time we would consider R lt hold t putR r 1 and R a putR r 1 to be equivalent Such an equivalence relation though would decrease the tractability of search in a language such 14 as Prolog the arbitrary introduction of hold commands do 0 loops etc the symmetry of the equivalence relation being the key problem would be allowed so we choose to define the 7 relation which is not symmetric An excellent account of labelled transition systems is given in Pac89 along with a method for analyzing assertions made of programs 1 3 Modal and Temporal Logics The Free Online Dictinary of Computing FOL defines a modal logic to be An extension of propositional calculus propositional logic with operators that express various modes of truth So rather than just being able to express p is true we might be able to express that p is possibly true p is necessarily true p is true at some point in the future g is true in the next state and so on Formally adopting the Kripke semantics of modal logics we define a set of states or worlds W and a relation R betwe
99. to perform any action until it is released by the station after it has been allocated a platform and all the passengers have boarded To define synchronisation we must have a notation for representing processes waiting in a pool and processes holding other processes Notation P shall represent a process P that has synchonized on a pool a This shall lie in the resource term R When this process is claimed by another process it shall be written P A process Q holding a multiset of processes S 1 Pi 2 Prl lt that syn chronised on pools 21 2 shall be written 2 i We see then that a process is actually a pair consisting of the remaining code and the processes synchronised on it Where the collection of processes that synchronised on a process is not affected by a rule for example sequential com position does not itself modify the collection of synchronized processes though a sub derivation may do so in general we shall not specify this in the rule for RafPJ R lt P it shall be implicit in P and P Otherwise where the collection is explicitly modified we shall write rules of the form P o IP Ro 5 Z The upper case letter S denotes a multiset the lower case letter s denotes a single item The above definition extends in the obvious manner to parallel processes SYNC R lt sync 2 P R P alel GETS zn ADN etS x n getS7 RPI EEE R
100. unction X classname code Again notice that we have defined a 7 transition ENTITY class name R lt Entity class name t P PES Ra classtname P RES R a Res r n 5 R r a e BIN R lt Bin b n E3 R b a e A t 3It may be more useful to split the hold into two transitions R lt hold t parc for model checking some properties e g mutual exclusion over a critical region 33 2 3 4 Seguential composition The seguential composition of program code is relatively straightforward to define one command is executed which changes the state of the system with the rest of the program remaining c shall range over single commands which may be compound e g while loops There are two cases to consider Firstly the first command executes completely R a c gt R e R lt c P gt R a P COMP re If the command at the head executes to give an intermediate step we place this back in front R lt c 4 R lt P COMP a R lt fc Pa gt R lt Pi Pa PLA e 2 3 5 Parallel composition We say that processes are acting in parallel or concurrently if more than one process is running at the same time We shall use to represent parallel composition of processes Each parallel process providing it is not blocked waiting for a resource not free in R may be executed At this stage we choose not to define a no
101. until the MI5 line is released thereby avoiding deadlock This execution is illustrated in 2 a Now suppose that the CIA process takes an extra two minutes to gain control over the FBI line possibly because of interference during the handshaking period At 12 46 the CIA process will try to gain control over the MI5 line but will fail it is now owned by MI6 and so will wait for it to become available At 12 47 the MI6 process will try to acquire the FBI line but will also fail it is owned by the CIA and so will wait Both the CIA and the MI6 processes then will wait indefinitely they are in deadlock This execution is shown in 2 b Unfortunately if we had taken time into account when deciding upon deadlock freedom from our model we would never have known that deadlock could occur and would fail to see the inherent flaw in the system This could be dangerous for MIG and similarly the CIA MIS which has responsibility for coun terespionage might notice that its secure link with the outside world was never available and investigate why this was so We have considered a discrete event system we do not consider actions on resources to happen over a period of time Further our consideration shall be of discrete resource systems So rather than having 2 4 litres of oil that we can partition to allocate to processes as we wish we shall consider n units of oil where n N n is a non negative integer However
102. uny y wu gt puny y wu 1 etou gt puny y u uva CLINOD HINILON POAOWIOI MOU SI SSIDOIA I9YJOAA OY JO pou ayy ye T PTOU oy 42 gt cz ptoal xr P pou y gt ec eteul xllr fC PTW 29279 02 pToUl gt puny y UTe go 9A YOIYM wor z ptoul MP C PTW 202879 0Z Prou gt puny y E eo ereulwlr uona 1 y uas3 L149 PIWN 99e13 0z pTou ueya 7 u3e3 Arq gt puny y u qof Ayjorgrp urmnrpouir sy o3op duroo 0 spoou Y Lu OY Sur3398 ssooo1d 1oqqof eures oY MOYS 03 anre ou SI 019 UL 1930 oAoqe ouo Y O Te IUuls 901 UOTYEALIOP Y PTING IM 43 Example 2 Semaphore This simple example considers a synchronisation based semaphore and may be found in the Demos distribution as me4 d2000 though for conciseness we ignore the third user The code is given again in Figure 2 4 Again we omit the initial declations of entities etc We first define for convenience A getS semS 1 hold 5 trace have putS semS 1 S sync semS trace back Tr U the code of User while do A Sem the code of Sem while do S We shall expand the while loops that control the processes NBLOCK r WHILEX PAR Wall 15 tel e 1510 15 L4 U 15 a U U Sem 15 LA U U Sem Very similar derivations justify 15 lt 4 UNUN Sem 15 lt 4 UA Ul Sem and 15 4 U 4 U S
103. urces Given a particular collection of resources a model we ask whether propositional formulze hold Technically BI is a logic based around bunches tree like structures of propo sitions and in the predicate case constants It seeks to combine the addi tive semantics of intuitionistic logic giving standard meaning to the operators A V with the multiplicative semantics of Girard s Linear Logic Gir87 giv ing the operators x The multiplicative connectives essentially allow us to make the kind of assertions that we would like to make about systems with resources When we write formule in BI the multiplicatives shall bind more strongly than the additives conjunction shall bind more strongly than disjunc tion which in turn binds more strongly than implication and negation binds strongest of all All binary operators are taken to be right associative this is only of importance to the implications the other binary operators are com mutative and associative For example Pe VN b 7 prp A v Logics are defined in two parts syntax and semantics The syntax of the logic is just a way to write down sentences that relate to the semantics Attached to the syntax may be a deduction system taking sentences written according in the language defined by the syntax to derive other syntactically correct sen tences The semantics of the logic defines what the formula written in the syntax actually mean It may well be t
104. usefulness of variables and they are indeed allowed in Demos 2000 It would be a relatively simple matter to extend the transition system to take this into account We would introduce a variable state component to take this into account Transitions then would be of the form R lt P s R a P s Variable state would be simply a map from variable labels to variable values s Var Float We chose not to introduce this as our account is theoretical and whilst it is not difficult to introduce variables into an implementation proofs can become less succinct with their inclusion The semantics of PBI presented in this document have been defined with proof search in mind If we were to write a model checker though it is anticipated that it will not be able to check all formule for example to check the formula R a P E In v could involve us considering adding all syntactically correct processes being placed in composition with P Clearly as the set of all processes is infinite 3That is numeric variables e g x 4 y 5 rather than resource variables 88 such a simple implementation would lead to a non complete model checker It would be acceptable however to provide a model checker complete for only a fragment of the logic It may also be necessary to consider a logic other than the general Hennessy Milner style logic used here similar to CTL or modal p Finally we have not given a deduction sys
105. using temporal logic specifica tions ACM Transactions on Programming Languages and Systems TOPLAS 8 2 244 263 1986 The Free On line Dictionary of Computing http foldoc doc ic ac uk Jean Yves Girard Linear logic Theoretical Computer Science 50 1 102 1987 Dov M Gabbay Amir Pnueli Saharon Shelah and Jonathan Stavi On the temporal analysis of fairness In Proceedings of the 7th ACM SIGPLAN SIGACT symposium on Principles of programming lan guages pages 163 173 ACM Press 1980 Matthew C B Hennessy and Robin Milner On observing nondeter minism and concurrency In J W de Bakker and Jan van Leeuwen 90 HM85 Hoa85 MBC 95 Mil89 MP83 MS Mur89 OED73 OP99 Pac89 Per58 Pit02 editors Automata Languages and Programming 7th Colloquium volume 85 of Lecture Notes in Computer Science pages 299 309 No ordweijkerhout The Netherland 14 18 July 1980 Springer Verlag New York Berlin Heidelberg Matthew C B Hennessy and Robin Milner Algebraic laws for nondeterminism and concurrency Journal of the ACM JACM 32 1 137 161 1985 C A R Hoare Communicating Sequential Processes International Series in Computer Science Prentice Hall 1985 Series editor C A R Hoare M Ajmone Marsan G Balbo G Conte S Donatelli and G Franceschinis Modelling with Generalized Stochastic Petri Nets Series in Parallel Computing Wiley 1995 Robin Milner C
106. utR CIA line 1 Res CIA line 1 Res FBI line 1 Res MI6 line 1 Res FBI line 1 Entity CIA 12 60 40 12 40 Entity MI6 12 60 43 12 43 Figure 2 2 Demos program for the intelligence agency example 30 exist PQ QIP Polo PlQ1 1102 Ple P sP Jel Pse P We shall though define the transition system so as to make these equivalences unnecessary in the derivation of transitions The reader shall recall that in our definition of PBI we required a transition relation to describe the activity of processes This is presented in the following section and shall be called vDemos 2 2 Transition rules Notation Let R denote the set of actual resources ro r shall range over R In the seguel we shall find it convenient to think of processes as resources We can define the set of resources actual and processes def R Py R Y P Pnoc where P R denotes the set of all sub multisets of R R R shall denote a multiset of resources multiset operations shall be as set operations tagged with a R r shall denote the multiset R with one unit of resource r added That is R r Rut We shall write r for w1r5 A state in the transition system shall be represented by a pair s Rx Prog We let the set of all states be Q def R x Proc Let the set Act be the set of actions that any Demos program may make ranged over by o We can define a transition relation C Q x A
107. ve the only time we may have such non deterministic choice is where we have the parallel composition of processes where more than one is active 4 e not waiting on a resource The astute reader may have noticed that when considering deadlock it was not essential to distinguish whether the first action was or was not the mother T4 1 2 3 4 5 6 1 e e e 2 9 P 3 9 9 4 e e e The axes are labelled by numbers representing the line of code being executed Pn P 1 getR k 1 getR s 1 2 getR s 1 hold l 3 hold 5 putR s 1 4 putR s 1 5 putR k 1 6 So for example 4 3 putR s 1 putR k 1 putR s 1 Arrowed lines indicate which states may be derived from each state Figure 5 1 Reachable state space for kitchen example derived by asynchronous transition system picking up the knife and then considering the real interaction Why then did we need to generate a whole collection of states to distinguish this possibility In terms of process interaction it would have been more efficient to force the first action to be the mother taking the knife Of course the reader could argue that it is the r le of the modeller to weed out such irrelevances Unfortunately though the modeller may not know in advance which processes we wish to model interaction between so this cannot be expected 5 2 Soundness try
108. would describe a dynamic Petri net AB96 Unlike our presentation of additive modalities here we could perhaps consider additive modalities as referring to transitions in which only the marking changes and multiplicative modalities as referring to transitions in which the net may change Further consideration of this though is beyond our current Scope 28 Chapter 2 Demos 2 1 Introduction Demos BTO01 is a simulation language for modelling processes executing in parallel that interact through taking and then relinquishing control of re sources As indicated by the title of the manual BTO01 the value of the language is that its operational semantics is clearly defined TBOI It is possible therefore to define translations between Demos programs and other systems and then prove the translation correct For example Demos programs can be translated to CCS processes TB94 TB95 BTa BTb and to Petri nets Tof01 again if we fail to model time Because the translation is demonstrably correct we can have confidence that any results obtained of a Demos model by say translating to CCS and then using the Edinburgh Concurrency Workbench MS are correct We refer the reader to B TOI for an introduction to the language This document in order to maintain a concise notation shall consider only a subclass of Demos programs the syntax of which is given in Backus Naur form in Figure 2 1 Notably this does not include va
109. y induction f R lt P gt F R lt a PD We must show that this execution matches the execution of fF R a Pi P5 P is either waiting on a resource or it is not if it is it will be placed in the waiting list of some resource It therefore will not affect the execution of this command If P5 is placed in the event list thanks to the arbitrary order of the event list it is possible that Pj s execution may be followed again Moreover this property is maintained through the execution of any intermediate steps made by P due to all times being equal 3 4 Weak bisimulation To consider some further properties it will be useful to have a notion of equiv alence between states we shall adopt observational equivalence similar to that developed in Mil89 Observational equivalence between states informally tells us that any visible in our case ignoring T transitions series of transitions from one of the states can be made if and only if it can be made from the other More formally writing Act for the set of all actions and Act for the set of observable actions e Act Act r Definition Weak bisimulation Let x represent a relation between states in the transition system i e x C 0 We shall use infix notation writing R a P x R a Q rather than R lt P R lt Q x x is a weak bisimulation between states if 1 for any transition R lt P R a P where e Act we have R a IQ

The application of a resource logic to the non

Contents

Download Pdf Manuals

Related Search

Related Contents