The Meaning and Implementation of SKIP in CSP
Contents
1. divergences models In these models each process is represented by a set of behaviours Two processes are equal in a denotational model iff they have the same set of behaviours In this paper we consider only the traces and failures models In the traces model a process is modelled by the set of finite traces which are sequences of events from X that it can perform In the failures model a process is represented by a set of pairs each consisting of a trace and a set of events that the process can stably i e the process must not be able to perform a 7 refuse to perform after the trace Notation Given a sequence tr A and X C A the restriction of tr to X denoted tr X is inductively defined by removing events not in X as follows yf X x as X ead X ifwe Xx zs X otherwise If tr UU 7 t P amp Q iff there exist P Py Q where N tr tr a1 y and such that P gt P gt gt Py Iftr E P Q iff there exists tr such that tr tr and P Q P denotes that there does not exist a process P such that P 5 gt P 4 T Gibson Robinson and M Goldsmith The Meaning and Implementation of SKIP 1 2 Termination in CSP CSP also allows processes to be composed sequentially The sequential composition of P and Q denoted P Q runs P until it terminates at which point Q is run CSP defines the process SKIP as the process that immediately terminates Thus t2. the supercombinator for P Q has two formats The first format represents the rules that are active before P has performed a Vv whilst the second format is active after P has performed a v which will have been con verted into a 7 and represents how the transitions of Q are promoted Thus rules can also specify which format they transition into Further supercombinators are actually constructed recursively this is the key to efficiency For example assuming that each P is a low level machine then a single supercombinator is constructed for P P2 Ps P4 rather than three different supercombinators This is constructed by combining together the rules for the and operators T Gibson Robinson and M Goldsmith The Meaning and Implementation of SKIP 13 In our particular simulation it is this recursive construction that is the source of the in efficiency For example consider Q 4 _ yy P SKIP assuming that each of the P is represented as a low level machine this machine will have 2 formats since the supercombi nator has to have a format that represents Q being in any possible combination of the formats of each P SKIP process Since it is not possible or at least certainly not desirable to lazily construct formats this could add significant time and memory consumption to the check Recall that the only difference in the denotational semantics between the V as Signal and v as Refusable semantics is t
3. An example is given at the end of Section I 3 2 T Gibson Robinson and M Goldsmith The Meaning and Implementation of SKIP Contributions In this paper we propose a method of simulating Roscoe s termination se mantics using the Hoare termination semantics that requires only minimal changes to the ex isting operator definitions Further we prove that the simulation is equivalent to the original formulation Thus this provides a way of implementing both termination semantics inside of FDR with minimal changes Outline of Paper In Section 1 we introduce the relevant fragment of CSP and define the two main termination semantics In Section 2 we then develop and prove the correctness of a simulation of the Roscoe semantics in the Hoare semantics Further this simulation will be efficient in that it requires minimal changes to the existing operators We also discuss an optimisation to the transformation that will improve the performance of the simulation under FDR In Section 3 we summarise the results of the paper 1 CSP and its Termination Semantics In this section we give a brief overview of CSP and detail the two standard termination semantics for CSP 1 1 CSP CSP is a process algebra in which programs or processes that communicate events from a set X with an environment may be described We sometimes structure events by send ing them along a channel For example c 3 denotes the value 3 being sent along the chan nel c Fu
4. to the hiding involved in such a state both equations can refuse the whole of 5 7 as required Hence as this covers all possible cases for P the required result follows 2 3 Efficiency The solution sketched above is certainly efficient with regards to implementation since it requires only a straightforward substitution to be performed on a process However unfortu nately the transformation would cause FDR to produce less efficient representations of the various LTSs thus slowing down the refinement checking process and causing more memory to be consumed In order to explain the issue we firstly briefly review how FDR internally represents labelled transition systems LTSs FDR has two main internal representations of LTSs The simplest known as a low level machine is an explicit graph FDR s most useful representation is known as a supercombi nator A supercombinator takes a number of other LTSs and a set of rules that say how the transitions of the component machines combine together to produce the transitions of the overall machine For example a supercombinator for P Q assuming P and Q are repre sented as explicit graphs would have two component machines P and Q a rule for each non v event that P or Q can perform to promote the event a rule that causes the machine to perform a v when both P and Q do Further in order to support operators such as P Q these rules are arranged into formats For example
5. Communicating Process Architectures 2013 1 P H Welch et al Eds Draft 2013 2013 The authors All rights reserved The Meaning and Implementation of SKIP in CSP Thomas Gibson Robinson and Michael Goldsmith Department of Computer Science University of Oxford Email thomas gibson robinson cs oxz ac uk michael goldsmith cs oz ac uk Abstract The CSP model checker FDR has long supported Hoare s termination se mantics for CSP but has not supported the more theoretically complete construction of Roscoe s largely due to the complexity of adding a second termination semantics In this paper we provide a method of simulating Roscoe s termination semantics us ing the Hoare termination semantics and then prove the equivalence of the two dif ferent approaches We also ensure that FDR can support the simulation reasonably efficiently Keywords CSP FDR Model Checking Termination Introduction The process algebra CSP provides a way of composing processes sequentially such that a second process is only started once the first process has terminated There have been many different semantics proposed for termination in CSP The first semantics was proposed by Hoare in 1 This semantics is perhaps the most intuitive and probably the most useful for constructing CSP systems in practice since parallel compositions terminate only when all components do providing support for distributed termination In 2 Roscoe proposes a sec
6. E traces Sig Q T U traces Sig R 7 IH Theorem 2 4 A X tr 0 A Itr 7 tr X U 4 7 failures Sig Q N failures Sig R U tr X Itr tr OY tr A tr X U 7 failures Sig Q U failures Sig R UL O X X CETA 7 Vv traces Sig Q U traces Sig R Lemma 2 2 X 3tr 7 tr X U t failures Sig Q N failures Sig R U tr E X tr X U 7 failures Sig Q U failures Sig R Atr 0 Q tr E X tr X U 7 failures Sig Q O R failures Sig Q O Sig R 7 failures Sig Q O R 7 We can prove that the step marked holds by proving the following equivalence f r X tr AQ AItr tr ES Stra tr X U 1 failures Sig Q U failures Sig R U X X CETA 7 V E traces Sig Q U traces Sig R tr E X tr X U 7 failures Sig Q U failures Sig R A tr Firstly suppose tr X is a member of the left hand equation Then if tr X is a member of the first clause tr 4 and there exists tr such that tr UY tr and T Gibson Robinson and M Goldsmith The Meaning and Implementation of SKIP 11 tr X U 7 failures Sig Q Hence tr X is a member of the right hand equation as required Otherwise tr X must be a member of the sec
7. as Signal semantics but not in the V as Refusable semantics Outline In Section 2 1 we formalise the translation that we have sketched above We then prove the equivalence of the translation in Section 2 2 and then discuss the efficency of the translation in the context of FDR in Section 2 3 3An alternative method of solving this problem is to simulate each external choice P O Q as P O Q SKIP The problem with this simulation is that it produces processes that are much larger than the original process and more problematically will cause FDR to be unable to compile many recursive definitions 8 T Gibson Robinson and M Goldsmith The Meaning and Implementation of SKIP 2 1 Formalising The Translation We now formalise the above translation as follows Firstly we define how the new resolving tau T is treated by the existing operators by assumption 7 X so none of the existing operational semantic rules apply We define BSkip T v Q In order to ensure that a T occurs only directly before a v we add the following additional rule to P Q P Pp P Q gt P Q As a result of this rule note that P Q can only perform a 7 if Q can after P has terminated since any 7 of P is converted into a 7 Thus assuming Q only performs a 7 directly before a v the desired property immediately follows Further to each other operator we add an extra rule to promote 7 exac
8. ay of defining the operational semantics of CSP processes is by presenting Structured Operational Semantics SOS style rules in order to define the transition relation gt for e U 7 For instance the operational semantics of the exception operator can be defined by the following inductive rules PP ag P gt pl P PLP POQ SQ PQ Q 5P 0 Q PQ Q gt P O Q The interesting rule is the first which specifies that if P performs an event a A then P Q can perform the event a and then behave like Q i e the exception has been thrown The last rule is known as a tau promotion rule as it promotes any 7 performed by a component in this case P into a 7 performed by the operator The justification for this rule is that 7 is an unobservable event and therefore the environment cannot prevent P from performing the event Note that 7s from Q are not promoted since Q is not active Formally an argument P of a CSP operator Op is on iff it can perform an event i e there exists a SOS rule of the form P gt P Op P Onl P is off iff no such rule exists For example the left argument of the exception operator is on whilst the right argument is off Also given that the SOS rules for internal choice are PnNQ gt P PNQ S Q it follows that both arguments of M are off Conversely both arguments of L are on CSP also has a number of denotational models such as the traces failures and failures
9. d M Goldsmith The Meaning and Implementation of SKIP 5 P Q R and Q has a Y guarded SKIP where Y is the pre image of X under R 6 P Q Y and Q has an X UY guarded SKIP A process P has an unguarded SKIP iff it has a guarded SKIP A process P is problem atic iff either 1 P is an Independent operator one argument of P has an unguarded SKIP and there exists an on argument P of P such that P w for some a X or g 2 P has a problematic process argument For example consider the process P a SKIP O SKIP By the above definition this is rightly considered problematic since P is an independent operator and has an argument with an unguarded SKIP However P a SKIP and is thus intuitively unproblematic It is also formally unproblematic since a gt SKIP O SKIP has a a guarded SKIP Note that the above is indeed an over approximation For example consider the process P a SKIP O b gt SKIP Whilst P is unproblematic P a is identified as problematic even though P a b SKIP gt SKIP which is clearly unproblematic We believe that such processes should be sufficiently uncommon to ensure that the over approximation is a useful one We now prove that the above computes a sound approximation as follows Theorem 2 9 If P is not problematic then P contains no operationally discretionary sub process Proof Sketch This can be proven by a structu
10. e such b is left to the environment like The process P A Q initially behaves like P but allows Q to interrupt at any point and perform an event at which point P is discarded and the process behaves like Q The process P Oy Q initially behaves like P but if P ever performs an event from A the exception set P is discarded and P Q behaves like Q Recursive processes can be defined either equationally or using the notation u X P In the latter every occurrence of X within P represents a recursive call to u X P Non determinism can arise in a variety of ways in CSP processes For example non determinism can be explicitly introduced via operators such as the internal choice oper ator providing the arguments are semantically distinct Further and more subtly other operators can introduce non determinism when combined in certain ways For example a STOP Ua b gt STOP is non deterministic since b can be both accepted and T Gibson Robinson and M Goldsmith The Meaning and Implementation of SKIP 3 refused after performing an a For a more thorough description of non determinism see e g 3 There are a number of ways of giving meaning to CSP processes The simplest approach is to give an operational semantics The operational semantics of a CSP process naturally creates a labelled transition system LTS where the edges are labelled by events from XU r and the nodes are process states The usual w
11. eorem 2 4 failures Sig Q T Sig R 17 failures Sig Q R 7 P Q R In order to prove this case we firstly define using the definition from 2 the set of all interleavings of two traces s and t denoted s t sO IEW tu Vv we s II tf sv t lt sile s lt 5 O st It x as u ys 2 u u ars y ys U L y u u ys x ws Using the above we can now prove the required result as follows failures Q R failures Q SKIP R SKIP 12 T Gibson Robinson and M Goldsmith The Meaning and Implementation of SKIP tr YUZ Y iv 2 iv Ads t tres tA s Y failures Q SKIP A t Z failures R SKIP tr YUZ Y iv 2 iv Ads t tres t A s Y failures Sig Q BSkip 7 A t Z failures Sig R BSkip 7 TH failures Sig Q BSkip T Sig R BSkip 7 failures Sig Q BSkip Sig R BSkip 17 failures Sig Q Boe La BSkip T H failures Sig Q R 173 The step marked us justified by observing that forcing synchronisation on 7 does not alter the failures This is because in any state in which the first equation could perform a Tp it must be because a BSkip is doing so However note that it does not matter if a BSkip is blocked from proceeding by a synchronisation on a V or a 7 3 due
12. er the V as Signal semantics is the same as the value of Sig P 7 Plunder the v as Refusable semantics In order to prove that the translation produces the correct denotational values we firstly prove a couple of results about the operational semantics Together these essentially prove that 7 functions as discussed above Firstly we prove that 7 s always occur directly before v s 4Clearly we need to hide the newly introduced r event otherwise we will obtain extra traces T Gibson Robinson and M Goldsmith The Meaning and Implementation of SKIP 9 Lemma 2 2 Sig P 7 24 Q iff Sig P 2S Q Proof Sketch This follows by a trivial structural induction over P using the definitions of the modified operational semantics and the definition of Sig In particular note that BSkip always performs a 7 immediately before a v Otherwise if an operator performs a v then it must not be since cannot perform a v and thus it must be because an argument performs a v Thus the inductive hypothesis applies noting that all operators promote Ty We now prove a second operational result and prove that if a process can do a7 then the resulting state must be operationally equivalent to SKIP i e it can do a Vv but can perform no other event Lemma 2 3 Sig P X iff X b Q and for all a D7 X gt X for some X Proof Sketch This follows by a trivial induction over P noting that the translation e
13. hat the former adds extra failures In particular according to Equation I 1 failures P contains the extra failures tr X PA0 xcx Note that any process that just offers a v will already have all of the above failures Therefore the only processes that the above will add failures to are those that contain a choice between a visible event and a v For example SAK PChoice and SKIP SKIPChoice both contain choices between visible events and V s and thus have extra failures added However as processes such as P O SKIP are sufficiently unusual if we only apply the transformation to the relevant portions of a process the increase in cost will be negligible We formalise this as follows Definition 2 6 A process P is operationally discretionary iff P L Q and there exists a X such that P gt P Theorem 2 7 Let P be a process such that for all P such that P a P P is not opera tionally discretionary Then failures P failures P Proof Sketch This can be proven by induction over the process noting the above observa tion regarding the extra failures in failures P as opposed to failures P Checking if every state has a V alongside a visible event available is clearly not feasible due to the time required to check such a property Therefore we need to compute a sound over approximation of the operationally discretionary property We can do so by noting that an Independent
14. he V as Refusable semantics it cannot Thus it follows that to simulate this process correctly in the V as Signal semantics somehow the process must be altered to allow the a to be refused In the above example the only way that the a can be refused is if the external choice is resolved In order to solve this we add a new resolving tau event denoted Tr that is treated by all operators precisely as they treat v Thus in the above example a T would cause the LJ to be resolved leading to a state in which only V is offered and in particular refuses the a as required In our translation if we arrange that 7 always and only occurs directly before a v then it follows that we can correctly resolve LJ and other operators with Independent termination semantics and introduce the failures required by Equation I 1 We now discuss how to simulate correctly operators that have synchronising termination semantics In Section 1 4 we saw that SKIPChoice STOP is equivalent under V as Refusable semantics to a STOP whilst under v as Signal semantics it is equivalent toa STOP gt STOP since SKIPChoice can decide to terminate independently We can achieve the same effect by simulating the left hand side as SKIPChoice SKIP thus allowing the termination to resolve the external choice and introduce the failures required by Equation I 1 Note that this is essentially taking advantage of the equivalence P P SKIP that holds under the v
15. he process P a SKIP is the process that terminates after performing an a whilst the process Q P Q is a process that never terminates but performs an infinite number of a s it is equivalent to R a R The process Q represents a process that has terminated Note that whilst this is operationally equivalent to STOP we require a syntactically distinct process in order to define Roscoe s termination semantics The reason that this is required will become clear when the operational semantics of are defined under the Roscoe termination semantics in Section I 4 In order to define formally the semantics of termination the event vV X is added and SKIP is defined as v Q The operational semantics of sequential composition are defined as a v a pP aEcXU r oe i P5Q gt P Q P5Q gt Q Note that v since it represents termination should only ever appear at the end of a trace Clearly the above definition of sequential composition respects this In order to define termination fully in CSP we need to define how each of the CSP opera tors treat a v performed by one of their arguments If an operator has no on arguments e g M and gt then these processes are simply defined as non terminating If an operator other than sequential composition which has a special definition due to its central role in termination has one on argument e g and gt then the operator terminates precisely when it
16. inson and M Goldsmith The Meaning and Implementation of SKIP 7 SKIP However under the v as Signal semantics a gt STOP gt SKIP SKIPChoice since the extra failures that SKIPChoicea has as per Equation I 1 mean that the a can be refused as it can in a STOP gt SKIP More generally P P SKIP since in any state where the v can be performed by P all events other than V can already be refused 2 Simulating V as Signal We now consider how to simulate the V as Signal semantics under the V as Refusable se mantics Intuitively the difference between the two different semantics is that the v as Refusable semantics just treats v as a regular event and therefore in SKIPChoice SKIP O a gt STOP offers the deterministic choice between the v and the a In the v as Signal semantics whilst the choice is still offered it is no longer a deterministic choice since P can refuse the a cf Equation T T In order to define our translation we firstly consider how operators with Independent termination semantics are affected Firstly consider the process SKIPChoice STOP The LTSs for this process under the two different semantics are given in Figure I start start a a v as Refusable b v as Signal Figure 1 The LTS of the process SKIPChoice STOP under different termination semantics Note in particular that under the v as Signal semantics this process can refuse to do an a but under t
17. ion in a more theoretical context Acknowledgements We would like to thank Bill Roscoe for several interesting discussions on this work We would also like to thank the anonymous reviewers for providing many useful comments and interesting discussions T Gibson Robinson and M Goldsmith The Meaning and Implementation of SKIP 15 References 1 C A R Hoare Communicating Sequential Processes Prentice Hall Inc Upper Saddle River NJ USA 1985 2 A W Roscoe The Theory and Practice of Concurrency Prentice Hall 1997 3 A W Roscoe Understanding Concurrent Systems Springer 2010 4 H Tej and B Wolff A corrected failure divergence model for CSP in Isabelle HOL In FME 97 Industrial Applications and Strengthened Foundations of Formal Methods volume 1313 of Lecture Notes in Computer Science pages 318 337 1997 5 Formal Systems Europe Ltd Failures Divergence Refinement F DR 2 User Manual 2011 6 J Davies Specification and Proof in Real Time CSP Distinguished Dissertations in Computer Science Cambridge University Press 1993
18. nsures that whenever T occurs the resulting state is equivalent to SKIP Using the above we can now prove that our translation produces the correct traces Theorem 2 4 traces P traces Sig P 7 Proof This follows by a trivial induction on P noting that traces SKIP traces BSkip 1 We can now prove our that the translation produces the correct failures Theorem 2 5 failures P failures Sig P 7 Proof We prove the lemma by structural induction on P We elide the case for STOP since it is trivial P SKIP failures Sig SKIP 7 failures BSkip 1 failures SKIP 7 failures SKIP failures SKIP P a gt Q failures a Q X X CU a X U a tr X tr X failures Q X X CUO a X U a tr X tr X failures Sig Q 7 IH failures a Sig Q r failures Sigla gt Q 7 T 10 T Gibson Robinson and M Goldsmith The Meaning and Implementation of SKIP P OCA failures Q O R 0 X 0 X failures Q N failures R U tr X tr X failures Q U failures R tr A U X X CE A Vv traces Q U traces R X X failures Sig Q 7 N failures Sig R 7 U tr X tr X failures Sig Q 7 U failures Sig R 7 tr 4 O U X X Cu A v
19. ond clause and hence tr X C U7 and 7 v traces Sig Q U traces Sig R WLOG assume there exists S such that Sig Q LEE EAE note that the only state that can occur after V is 9 Hence by Lemma 2 3 7 Y failures S for any Y C X Hence as X C X it follows that 7 X U 7 failures S and thus X is a failure of the right hand equation as required Otherwise suppose tr X is a member of the right hand equation Thus tr and tr X U 7 failures Sig Q U failures Sig R WLOG assume tr X U 7 failures Sig Q There are two cases to consider Firstly assume tr OY Hence trivially it follows that tr X is a member of the first clause of the left hand equation Otherwise tr and hence tr must consist of one or more 7 s By Lemma 2 3 tr 7 and letting S be such that Sig Q a S S Q Hence Tr V traces Sig Q Further since the above holds for any such S it follows v cannot be refused after 7 and thus X C X Hence X is a member of the second clause of the left hand equation as required P Q R failures Q R tr X tr X U v failures Q U tr tr X trv traces Q A tr X failures R tr X tr X U V failures Sig Q 7 U tr tr X tr v E traces Sig Q 7 A tr X failures Sig R 7 IH Th
20. ond termination semantics that that has since become the de facto formalisation of termination in CSP Roscoe s primary motivation for defining this second semantics was to admit a correct treatment of the algebraic semantics of termination in CSP which was known 4 to be problematid under Hoare s termination semantics The CSP model checker FDR 5 has only ever supported the Hoare termination se mantics which is particularly unfortunate as it means that those learning CSP are unable to experiment with the more usual theoretical formalisation of termination Unfortunately adding support for a second termination semantics in FDR imposes a large overhead For efficiency reasons FDR requires several different definitions of every operator meaning that an increase in the number of operator variants quickly leads to the number of lines of code increasing Further the different termination semantics require different ways of calculating the denotational value of a process in particular the failures of a process which requires changes deep inside FDR Therefore for the sake of efficiency and in order to reduce the number of lines of code required it is highly desirable to develop a solution that allows Rosoce s termination semantics to be simulated using the already implemented termination semantics within FDR lFor example one would reasonably expect P SKIP P but this is not always the case under Hoare s termination semantics
21. onising operators can be defined analogously P23 0A0250 P Q2 For example the above process SKIPChoice can terminate immediately Equally SKIPChoice STOP a STOP since the right hand argument can never termi nate and thus blocks SA PChoice from terminating Conversely SKIPChoice SKIP a SKIP since the right hand argument cannot perform an a and thus blocks the left hand ar gument from performing it The value of a process in the denotational models is also affected by the termination semantics in use Under any of the termination semantics the traces of a process can be easily extracted using traces P tr I P P gt P The failures of a process P under the V as Refusable semantics denoted failures P can easily be extracted from the operational semantics failures P tr X 3Q P B QAX CDUU V A Qref X where Q ref X iff Q is stable i e Q gt and Vx E X Q LS For example considering P a gt STOP N b gt STOP a failures P because although the initial state of P is unstable P b gt STOP Further since b STOP is stable it follows that a failures b STOP and hence a failures P since P AL b STOP A direct consequence of the above definitions is that P is not necessarily equal to P SKIP which might reasonably be expected For example SKIPChoicea SKIP is equal to a STOP gt SKIP
22. operator only yields an operationally discretionary process if it has an argu ment that is SKIP and another argument that is a visible event Further a synchronising oper ator only yields an operationally discretionary process if one of its arguments is operationally discretionary and the remaining arguments can terminate Whilst the above works for a large class of operators incorporating hiding requires a little more complexity In particular consider the processes P a SKIP and P Y b STOP Note that this process has an operationally discretionary argument iff a Y Hence to detect the above we also need to track the set of events that are hidden and thus could result in a SKIP being reached by only 7 events We formalise this in the following definition Definition 2 8 A process P has a X guarded SKIP iff P Q for s X iff P is one of the following forms 1 P SKIP 2 P a Q a X and Q has an X guarded SKIP 3 P is either an Independent operator is a non deterministic choice or is a sequential composition and P has at least one argument that has an X guarded SKIP 4 P is a synchronising operator such that all of its arguments have X guarded SKIP s 5As Roscoe notes in 2 Hoare actually banned this process because it appears so unnatural Thus whilst our simulation is less efficient on such processes this is arguably a reasonable price for perversity 14 T Gibson Robinson an
23. owed to do so This is in contrast to the v as Refusable semantics in which an argument is not allowed to terminate until the other argument is ready to do so The second two clauses specify that as soon as one argument has terminated if the other argument wishes to terminate then the whole operator becomes SKIP which can immediately terminate The above rules also illustrate the need for Q and STOP to be syntactically distinct Clearly STOP SKIP should not be allowed to terminate since STOP cannot terminate However if the last two rules above used STOP rather than Q then this would allow the interleave to erroneously terminate Thus we need STOP and Q to be syntactically distinct so that we can differentiate between a process that has terminated via a tick and a process that has just deadlocked so we can define the termination semantics of synchronising operators The most important difference between the two semantics is how the denotational values are extracted from the operational semantics As stated above Roscoe views termination as something a process tells the environment it is going to do rather than something the envi ronment can choose Therefore after a trace if a process can terminate i e a V is available then it should be able to refuse to communicate anything apart from the V i e all events from X Thus the failures of a process P under the V as Signal semantics denoted failures P contains an extra clause versu
24. ral induction over P noting that in the defi nition of X guarded X is a sound approximation to the set of events that can be 7 s Hence since a non problematic process has no Independent operators that have on arguments that have unguarded SKIP s and visible events the required result immediately follows 3 Conclusions In this paper we have discussed the difference between the V as Refusable and V as Signal semantics In Section 2 I we specified a way of simulating the V as Signal semantics within the v as Refusable semantics before proving in Section 2 2 that the simulation is correct in that it produces the same denotational value in the V as Refusable semantics as the v as Signal semantics Lastly in Section 2 3 we discuss how the simulation can be inefficient when considering how FDR internally represents LTSs and proposed a solution that reduces the overhead for all but the most unusual of processes We believe that the technique that we have presented in this paper provides a way of sim ulating the V as Signal semantics within FDR with a relatively minimal number of changes We hope to implement the simulation in the context of FDR3 which will be released towards of the end of the year This will be the first time that the FDR refinement checker has sup ported checking refinements under different termination semantics which will hopefully be of wider interest to those who are interested in studying terminat
25. rther given a channel c the set c C contains those events of the form c z The simplest CSP process is the process STOP that can perform no events and thus represents a deadlocked process The process a P offers the environment the event a X and then when it is performed behaves like P The process P O Q offers the environment the choice of the events offered by P and by Q Alternatively the process P M Q non deterministically chooses which of P or Q to behave like Note that the environment cannot influence the choice the process chooses internally P gt Q initially offers the choice of the events of P but can timeout and then behaves as Q The process P 4 5 Q allows P and Q to perform only events from A and B respectively and forces P and Q to synchronise on events in AM B The process P Q allows P and Q to A run in parallel forcing synchronisation on events in A and allowing arbitrary interleaving of events not in A The interleaving of two processes denoted P Q runs P and Q in parallel but enforces no synchronisation The process P A behaves as P but hides any events from A by transforming them into a special internal event 7 This event does not synchronise with the environment and thus can always occur The process P R behaves as P but renames the events according to the relation R Hence if P can perform a then P R can perform each b such that a b R where the choice if more than on
26. s on argument does thus termination is promoted The remaining CSP operators which have two on arguments are grouped into one of the following two categories with regards to how they treat termination Independent Operators that treat termination independently terminate whenever any of their on arguments terminate e g O and A Synchronising Operators that synchronise termination terminate only when all of their on arguments terminate e g and 4 z A The semantics we consider in this paper treat O and A independently This makes sense intuitively since neither of these operators actually runs its arguments in parallel but instead allows actions from one to occur and then discards the other at some point Independent operators by definition simply terminate when either of their arguments do Therefore the termination operational semantics of independent operators do not vary between different termination semantics and we can therefore define them now We formally define the semantics for LI the operational semantics for other independent operators can be defined analogously P gt Q Q 0 roosa PuCoo 6 All of the CSP parallel operators i e etc synchronise termination of their argu ments_ Thus a parallel composition terminates only when all of its arguments do which can be useful when constructing systems since it corresponds to dis
27. s failures P in order to add these extra failures failures P tr X 4Q P gt QA X CDNU V A Qref X fu 1 1 U tr X P 4 0 xcx However as noted above the traces extracted from the two semantics are identical The addition of the above failures has a number of interesting consequences for the behaviour of processes that involve choices between V and visible events For example consider the process SKIPChoice defined in Section Under the V as Signal seman tics this now has the failure a since it can perform a v immediately which was not a failure under the V as Refusable semantics Thus SK PChoice a gt STOP a a STOP gt STOP under the V as Signal semantics since SKIPChoice may pos sibly refuse the a which would cause a deadlock Under the V as Refusable semantics SKIPChoice a STOP a STOP since the v can just be ignored Equally SKIPChoice SKIP SKIP under both semantics since environmental control over the a a is retained This suggests the most important difference between the two semantics under the V as Signal semantics the environment is unable to stop V from occurring whilst under the v as Refusable semantics the environment is free to choose v just like any other visible event Recall that under the V as Refusable semantics it is not necessarily true that P P SKIP In particular recall that SK PChoice SKIP is actually equal to a STOP gt T Gibson Rob
28. tly as T is promoted Note that if none of the arguments of some CSP operator perform a 7 then the above changes do not alter the semantics of the operator at all This should simplify the implementation of these rules In order to simplify the formalisation of the transformation we consider only a restricted subset of CSP that includes STOP STOP O and Note that this includes all cate gories of operators in terms of their termination semantics and thus the proof and transfor mation could easily be generalised to all CSP operators Definition 2 1 The v as Signal translation function Sig is defined on CSP processes as follows Sig SKIP BSkip Sig STOP STOP Sigla gt P Sa gt Sig P Sig P O Q Sig P O Sig Q Sig P Q Sig P Sig Q Sig P Q Sig P BSkip Sig Q BSkip Tr As discussed informally we ensure that a 7 occurs exactly once before a V by redefining SKIP in the obvious way We then ensure that synchronises on 7 to ensure that only one T can occur We prove that this holds in Lemmaj 2 3 Notation In the following we use X to denote U v 57 to denote U 7 and 5 7 to denote X U V 7 2 2 Proving Equivalence We now prove that our translation gives the correct result In particular since we are interested in using our translation in the context of FDR we check that the denotational value of a process P und
29. tributed termination In the following sections we describe how the two different termination semantics define the semantics of the synchronising operators Whilst this is true of the standard CSP semantics in 6 Davies defines a version of interleave that does not synchronise on termination but instead treats it independently The results of this paper could equally be applied to treat interleave s termination independently instead but we concentrate on the more usual semantics T Gibson Robinson and M Goldsmith The Meaning and Implementation of SKIP 5 1 3 as Refusable The Hoare semantics as used by FDR treats V as a refusable event Thus henceforth we refer to this as the the v as Refusable semantics The motivation for this semantics is that a process should be able to offer to the environment the option of terminating but the environ ment should be able to decide whether the process terminates or not For example consider the process SKIPChoicea SKIP O a STOP which we use as a running example under the v as Refusable semantics this process offers the environment the choice of either terminating or performing the event a Under the v as Refusable semantics synchronising operators only terminate when both of their arguments are ready to terminate and the termination is performed in lock step The operational semantics for termination of is defined as follows Again the operational semantics for other synchr
30. which is not equal to SKIPChoice This is because SKIPChoice SKIP SKIP since SKIPChoice can perform a v which is converted into a 7 by Hence a failures SKIPChoice SKIP since SKIPChoice SKIP gt SKIP and x failures SKIP for all x X However a failures SKIPChoice since SKIPChoice is stable and explicitly offers an a meaning the two sides are not equal 1 4 as Signal Roscoe s termination semantics for CSP known as the V as Signal semantics instead treats V as an event that cannot be refused by the environment Thus when a process decides 6 T Gibson Robinson and M Goldsmith The Meaning and Implementation of SKIP that it is terminating the environment is not allowed to prevent termination instead the pro cess immediately terminates and signals this to the environment via the V event Thus in the v as Refusable semantics the offer of a v can be thought of as a communication that the process can terminate if desired whilst in the V as Signal semantics the offer of a v means the process can terminate on its own accord The operational semantics for termination of is defined as follows Again the opera tional semantics for other synchronising operators can be defined analogously Ps Qa QS P Sa P QSQ Q PQP QIQ SKIP P Q gt SKIP In the above the first two clauses ensure that as soon as an argument wishes to terminate it is all
Download Pdf Manuals
Related Search