Home

Paper

1. Px and there exists an on P such that P recurses to N through only on arguments A syntactic process P has no named on arguments iff P is not a name and if P Op P Py then each on P has no named on arguments e A syntactic process P has l guarded recursion to N iff P does not recurse to N or P N and T N has 1 guarded recursion to N or P Op Pi Py and whenever Op P Py Op P Op P has 1 guarded recursion to N e A process environment T has correct simple recursion iff for every N P I for every instance of Op P Py within P and for each on P x If P is infinitely recursive then P does not recurse to N x If P is only 1 required then P does not recurse to N through only on arguments P has no named on arguments and F has 1 guarded recursion to N Since the definition of has correct simple recursion only mentions operator arguments that are only 1 required and infinitely recursive it follows that we can only allow operators that have only such arguments With this observation in mind we can state and prove our main result Note in the following as discussed after Definition 3 4 we weaken the equiva lence from strong bisimulation to equivalence in any CSP denotational model Theorem 3 6 Let P be a syntactic process and I be a syntactic process environment with correct simple recursion If every argument of every operator used in I or P is either infinitely recursive or onl
2. x B where n B is performed Hence we define Harness P n as follows Harness P n PIPrime Ofa nesy STOP A off gt STOP HRename where off is a fresh event and Prime maps every event x Xo to both x and x HRename renames as follows e Each event a Xo to every 2 B such that n a andn B i e where process n performs n and is not discarded e Each event a x x Xo to every x B such that d n a and n B i e process n performs a but is discarded e off to every x B such that n dom and n B i e process n is discarded by an event in which it does not partake We now define the regulator which has three principle responsibilities it must ensure that only events allowed by the current operator can be performed by the processes it must track which process on the left hand side corresponds to which process of the current oper ator and it must turn on processes according to the executed rule Thus the regulator takes the following parameters e the current operator e m the number of processes ever turned on e W a map from 1 n A to 1 m in particular if Y x y it means that the the x on argument of is the y on argument e x a map from 1 A to 1 Z a where a is the starting operator i e the operator for which Operator a was called in particular if x x y it means that the xt off argument of
3. The combinator operational semantics of an operator F P where P is a vector of processes is defined by e Each process of the vector P is defined as either on or off on arguments are indexed by positive numbers whilst negative indices refer to off arguments Intuitively an on argument of a process can perform visible events whilst an off argument cannot For example both arguments of O are on the first argument of 4 is on whilst the second argument of is off e A set of combinator rules that specify the operational semantics of the operator except tau promotion rules which are implicitly defined for precisely the on arguments A single combinator rule is of the form x T where is a partial function from the on indices to X If a y then the zt on process performs the event y If x dom then x does not perform an event x rT UX is the resulting event that the operator performs x T is a piece of syntax that represents the state of the resulting process T is generated from the following grammar T N N Op T T where the first clause represents an off argument the second clause a currently on argument and the third clause represents the application of an operator to a number of process arguments Further there are a number of well formedness conditions on T 1 on processes cannot be cloned i e each on index i can appear at most once in T there is no CSP operat
4. POQ Offers the choice between P and Q PNQ Non deterministically picks one of P and Q to behave as P A Runs P but hides events from A which become 7 P Q Runs P and Q in parallel enforcing no synchronisation P Q Runs P and Q in parallel enforcing synchronisation on events in A A P alle Q Runs P and Q in parallel enforcing synchronisation on events in AN B PIR Renames the events of P according to the relation R PO Q_ Runs P until an event in A occurs at which point Q is run PAQ Runs P but at any point Q may interrupt P perform an action and discard P Table 1 A summary of the syntax of CSP TThe process P 4 g Q allows P and Q to perform only events from A and B respec tively and forces P and Q to synchronise on events in A N B The process P Q runs P and Q in parallel and forces them to synchronise on events in A The mieten 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 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 a
5. is the y off argument of a We can then define the regulator Reg A m V x as follows 192 T Gibson Robinson Efficient Simulation of CSP Like Languages Reg A m y x 0 8 f b x B eRules a Q WU x U x z B gt Inepn m ii Harness ofProcs x f n m AlphaProc n Une 1 m IfI AlphaProc n Une m fl AlphaProc n Reg B m F IF Y U idm 1 m fI 2 Wp Xe x Note that the above regulator allows only those events that correspond to the current operator and whenever such an event occurs evolves into the state dictated by the rule that was chosen with the state being updated according to the definitions of f etc Roscoe then proves that the above simulation results in a CSP process that is strongly bisimilar to the original operator 2 2 A CSP m Simulation In this section we outline the alterations to Roscoe s simulation that are required in order to allow the simulation to be successfully modelled in CSP m The first major issue that prevents the above solution being compiled into CSP y is that the alphabets such as AlphaProc n are infinite because it is possible that an infinite number of processes can be turned on by an operator Thus since the on processes have to be able to be synchronised in any possible way AlphaProc n has to represent an infinite number of possible synchronisations patterns In order to prevent this we disallow operators that could turn on an inf
6. like Further many denotational models for CSP such as Lowe s Availability Model 10 have a derived operational semantics that is CSP like meaning that we are able to simulate these denotational models operationally 2 Simulating CSP Like Languages In this section we define Roscoe s simulation and then define an optimised CSP y simulation before proving the equivalence of the two We start in Section 2 1 by describing Roscoe s simulation including the internal format of the operational semantics and the CSP process Operator that simulates a particular operator In Section 2 2 we then explain the modifica tions that we made in order to construct a CSP y simulation Further we detail the changes that we made to enable the simulation to run efficiently and prove that the optimisation still result in a strong bisimulation Throughout this paper we will need to enlarge the set of events X that the environment offers Thus for the remainder of this paper we will use X to denote the set of events that the user uses in their script 9 2 X to include all semantic events such as v to indicate termination in the case of CSP X4 2 No to include all internal events used by the simulation We also use a special event tau No that will simulate a semantic T 2 1 Roscoe s Simulation In order to simulate arbitrary CSP like operators in 1 2 Roscoe defines a data structure in which the operational semantic rules of an operator are enc
7. A W Roscoe On the Expressiveness of CSP Draft of February 2011 available from ox ac uk files 1383 complete 3 pdf 2011 2 A W Roscoe CSP is Expressive Enough for Pi In A W Roscoe C B Jones and K R Wood editors Reflections on the work of C A R Hoare Springer 2010 3 C A R Hoare Communicating Sequential Processes Prentice Hall Inc Upper Saddle River NJ USA 1985 A W Roscoe The Theory and Practice of Concurrency Prentice Hall 1997 A W Roscoe Understanding Concurrent Systems Springer 2010 Formal Systems Europe Ltd Failures Divergence Refinement FDR 2 User Manual 2011 R Milner A Calculus of Communicating Systems Springer Verlag New York Inc Secaucus NJ USA 1982 204 T Gibson Robinson Efficient Simulation of CSP Like Languages 8 R Milner Communicating and Mobile Systems the Pi Calculus Cambridge University Press June 1999 9 G Lowe Extending CSP with Tests for Availability In Communicating Process Architectures pages 325 347 2009 10 G Lowe Models for CSP with Availability Information In EXPRESS 10 pages 91 105 2010 dx doi org 10 4204 EPTCS 41 7 11 P Armstrong G Lowe J Ouaknine and A W Roscoe Model Checking Timed CSP In Proceedings of HOWARD Festschrift for Howard Barringer 2012 12 Faron Moller and Perdita Stevens Edinburgh Concurrency Workbench user manual version 7 1 Avail able from http nonepages inf ed ac uk perdita cub 13 P J
8. Courtois F Heymans and D L Parnas Concurrent Control with Readers and Writers Commu nications of the ACM 14 10 667 668 1971 14 A W Roscoe and D Hopkins SVA a Tool for Analysing Shared variable Programs In Proceedings of AVoCS 2007 pages 177 183 2007 15 G Lowe Casper A Compiler for the Analysis of Security Protocols Journal of Computer Security 6 1 2 53 84 1998 16 Thomas Gibson Robinson Tyger A Tool For Automatically Simulating CSP Like Languages In CSP MCompSci Thesis University of Oxford 2010
9. Not only does it mean that model checkers can be easily constructed for other process algebras but it allows a language designer to experiment with the language whilst developing it For example suppose a user wants to create a process algebra to enable easy verification of a certain problem Previously to experiment with the language an entirely new model checker would have to be constructed making it difficult for the language designer to experiment with the language s capabilities during design Now a simulation of the language can be constructed trivially allowing experiments to be run whilst the language is being developed and therefore providing feedback into the design Outline In Section I we give a brief overview of CSP before considering what languages we are able to simulate within CSP by defining Roscoe s CSP like condition In Section 2 we explain Roscoe s original construction before giving a number of modifications that enable it to run efficiently In Section 3 we discuss the problem with recursion explain the refactor ings required to permit recursive definitions and prove that the refactorings produce seman tically equivalent processes Further we discuss the limitations of the recursion refactorings In Section 4 we describe the construction of the tool In Section 5 we detail the results of several experiments that were run in order to verify the effectiveness and performance of the simulation Lastly in Sectio
10. Then A m x configs a onProcs idt JonProcs idt JoffProcs 1 Proof Sketch Observe that in the definition of Reg A m Y x Reg evolves into states precisely the same as those on the left hand side of h in the definition of con figs Lemma 2 2 If Operator a onProcs offProcs internally uses the event x B then x B closure a onProcs offProcs Proof Sketch This follows from the observation that internally Reg participates in every event that Operator performs and thus the set of events that Operator uses is bounded by the set of events that Reg allows which given Lemma 2 1 closure extracts by definition One other issue with the definition of Operator is that it contains a large number of nested CSP operators meaning that FDR has to deal with a large complex stack of operators However observe that if a particular component n can never be turned off as is the case with CSP s parallel operator then Harness P n is equivalent to P Renamel Hence if we can compute the set of arguments that can be turned off it follows that we can easily decide when to compute the full harness In order to compute the set of arguments that can be turned off we define the function turned_of f a onProcs offProcs as W b A m Y x con figs a onProcs 41 lonProcs UG te Priest 5 2 B f Y x B Rules A b B The correctness of this opt
11. computing the renamings and the process alphabets we restrict ourself to the subset of renamings that could be used either by the current oper ator or any resulting operator This requires us to compute the set of all x B such that x B is permitted either by the current regulator or any regular we can evolve to To calculate the above set we firstly calculate the set of regulator configurations that the regulator can evolve into In particular we define the function con figs A m V x where the arguments are as per Reg as the least fixed point of the following function h Clearly no practical simulation could support such operators so this is not a restriction in practice T Gibson Robinson Efficient Simulation of CSP Like Languages 193 h X XU A m V x 0 8 f v x B Rules d m Y x X Thus it follows that con figs A m Y x consists of the set of all states that Reg A m Y x can evolve into Using the above the set of all events of the form 2 B that Operator a onProcs offProcs requires denoted closure a onProcs offProcs can be defined as po 0 x U a z B 9 2 8 f x B Rules d A m Y x con figs a onProcs id 1 JonProcs idt JofProcs 1 The correctness of the above is shown in the following lemmas Lemma 2 1 Suppose Operator a onProcs offProcs evolves into state in which Reg is in state Reg m Y x
12. contains an incorrect usage of external choice in this case the inlined version would be P a gt a gt P Ob gt P O P To solve the above we introduce a fresh name R for the process P O b P We then rewrite the definitions as P2a gt R R2a gt ROb gt P T Gibson Robinson Efficient Simulation of CSP Like Languages 199 Note that the above processes have no disallowed immediate recursions In general if an argument of a process is only k required we need to inline sufficiently to ensure that none of the first k events can ever be call Proc events If we do this then it follows that the resulting syntactic process will satisfy the preconditions of Theorem 3 6 and thus this can be applied to correctly simulate the process In order to formalise this we firstly expand the definition of has correct simple recursion to allow immediate recursion As before we concentrate only on operators where each argument is either infinitely recursive or only 1 required Again the definition could be generalised as required Definition 3 7 A process environment T has correct recursion iff for every N P L for every instance of Op P Py within P and for each on P 1 If FP is infinitely recursive then P does not recurse to N 2 If F is only 1 required then P does not recurse to N through only on arguments and P has 1 guarded recursion to N Note that the
13. new process algebra it would make sense to reuse existing model checkers where possible In papers on the expressiveness of CSP 12 Roscoe develops a simulation that given a CSP like language constructs a strongly bisimilar process in the process algebra CSP 3145 Thus as CSP has an efficient industrial strength model checker FDR 6 it should now be possible to check models written in other CSP like languages without having to develop a new model checker Whilst the name CSP like might appear to imply that only a small class of languages can be simulated using 1 2 most of the CSP like conditions are merely well formedness conditions and thus many other process algebras such as CCS 7 the 7 calculus and Lowe s Readyness Testing CSP extension 9 are either CSP like or can be easily converted into equivalent but CSP like formulations Further many denotational models for CSP such as Lowe s Availability model 10 have CSP like derived operational semantics that enable the model to be extracted using the standard CSP models The above would suggest that a tool that could automatically construct a simulation of processes written in a CSP like language given the operational semantics rules as input would be of value Unfortunately Roscoe s construction in was never intended to be used as an actual simulation In particular only non recursive processes can be simulated within FDR as the simulated recursive processes are infin
14. particularly problematic for the recursion refactorings since it is the only CSP operator where an argument that is infinitely recursive can also be recursed through For example consider the process P a 4 b gt P Of a STOP In this pro cess P recurses through the first argument of Oga which is infinitely recursivd gt cf Defi nition 3 3 However FDR has no problem compiling the above process because when the b is performed Ora is discarded meaning that a transition back to P is found as required There is no obvious way of altering the simulation to support an operator that might sometimes recurse and thus requires the call Proc event to not be consumed by a WrapT hread inside O but sometimes never recurses and thus requires that all call Proc events must be consumed by a WrapThread inside O In 1 Roscoe actually conjectures that it is impossible to simulate O 4 in such a way that FDR can successfully compile pro cesses that use it Thankfully such operators are sufficiently uncommon that the simulation we provide is still applicable to a very wide variety of operational semantics 4 Tool Support As part of this work we have constructed a tool called tyger written in Haskell that auto matically constructs the simulation and refactors the user s process definitions as above The input to tyger consists of two input files the first of which specifies the
15. pro cesses as discussed above However it is strongly bisimilar to the original process given Roscoe s results We now consider how to formalise the recursion refactorings we sketched in the preced ing section In order to formalise them we need to distinguish between the different ways that an operator can use the events performed by its arguments For example O only looks at the initial visible events performed by each of its arguments whilst looks at all the events performed by its arguments We formalise this difference in the following definition Definition 3 3 An on process argument P of a CSP like operator Op is 1 required iff P can perform a visible event i e there exists an inductive rule of the form wie AP P Nous Op cy Pi Op xs where a X An argument P of a CSP like operator Op is k 1 required iff there exists an inductive rule of the above form to a CSP like operator Op 4 Identity such that P is k required for Op An argument P of an operator Op is infinitely recursive iff P is k required for every k N An argument P of an operator Op is only k recursive iff P is k required but not k 1 required For example considering CSP both arguments of are infinitely recursive both argu ments of O are only 1 required the left argument of A is infinitely recursive but the right argument is only 1 required the left argument of 4 is infinitely recursive but the right is not r
16. second clause prohibits syntactic processes where the events for a process depend recursively on the process itself Clearly such processes are not well defined We now define how to inline process definitions in order to support the refactoring that was sketched above Note that the following transformation is only well defined if the process environment has correct recursion Definition 3 8 Given a syntactic process environment I the inlined process environment I is defined on each syntactic process contained in any process in I In particular dom I is the set of all Np where P is a subprocess of some P img T Further I is defined by I Nop Py Py Op inline Op 1 P inline Op N Pn Ny P N Np i is off inline Op i P T Nnr i is on and P N I Nop p i is on and F Op P Note that the second clause of T is well defined by the assumption in Definition 3 5 that T N N Further observe that the inline is semantics preserving since it is essentially just a renaming operation Thus if N dom I then sim N is strongly bisimilar to sim I N Clearly the inlining process will only terminate if no on argument recurses back to itself This is implied by the definition of has correct recursion in Definition 3 7 Theorem 3 9 Let T be a process environment with correct recursion and let I be the flat tened process environment of I Then I has co
17. Communicating Process Architectures 2013 185 P H Welch et al Eds Open Channel Publishing Ltd 2013 2013 The authors and Open Channel Publishing Ltd All rights reserved Efficient Simulation of CSP Like Languages Thomas GIBSON ROBINSON Department of Computer Science University of Oxford UK thomas gibson robinson cs ox ac uk Abstract In On the Expressiveness of CSP Roscoe provides a construction that given the operational semantics rules of a CSP like language and a process in that language constructs a strongly bisimilar CSP process Unfortunately the construction provided is difficult to use and the scripts produced cannot be compiled by the CSP model checker FDR In this paper we adapt Roscoe s simulation to make it produce a process that can be checked relatively efficiently by FDR Further we extend Roscoe s simulation in order to allow recursively defined processes to be simulated in FDR which was not supported by the original simulation We also describe the construc tion of a tool that can automatically construct the simulation given the operational semantics of the language and a script to simulate both in an easy to use format Keywords CSP CSP like FDR model checking Introduction Developing a model checker for a process algebra requires a significant investment of re sources particularly if the model checker is to be efficient Therefore rather than developing new model checkers for each
18. articular the inferred types are used to identify all processes within a file note that the processes here are essentially the syntactic processes of Definition 3 5 Then a call graph of the processes is constructed and the strongly connected components SCCs are deduced This enables the recursive processes to be identified which then allows the recursion refactorings to be run If the recursion refactoring specified in Section were applied exactly as specified this would result in many more named processes than are strictly necessary slowing down the simulation Thus instead the following recursion refactorings are applied instead e Every call from a recursive process to a recursive process is replaced by a call Proc event e Every call from a non recursive process to a recursive process Q instead calls the wrapped version WrapT hread Q so that call Proc s are processed e Every infinitely recursive argument Q of an operator is replaced by WrapT hread Q e Every argument that is only 1 required is inlined as per Section 3 4 Further in order to define the WrapThread process cf Section 3 2 the set of values that each recursive process can take has to be specified For example the following defines a recursive process P that takes a single integer value that can either be 0 or 1 P 0 1 gt Proc P x if x 0 then a gt P 1 else b gt P 0 Lastly the transformed processes are pretty printed to a file Th
19. ational semantics where congruence means that the denotational semantics may either be extracted from the operational semantics or calculated directly given the process For example the traces model represents each process by the prefix closed set of finite sequences of visible events that it can perform i e a process is represented by a subset of amp 188 T Gibson Robinson Efficient Simulation of CSP Like Languages 1 2 CSP Like Languages In 1 Roscoe proves that if an operator Op is CSP like then it is possible to construct a CSP process Op such that the LTSs representing Op and Op are strongly bisimilar In this section we define what it means for an operator to be CSP like Conventionally operational semantics are represented by SOS rules such as those given above for the CSP exception operator However given that the syntax of SOS rules is very general defining what CSP like means in terms of the rules would be rather difficult For example the following SOS rule is not a legal CSP like rule since no CSP operator allows an event to occur as the result of the absence of another event but is a valid SOS rule P gt P Op P Op P Therefore in 1 Roscoe instead uses a different presentation of operational semantics rules in which only CSP like operators are definable We now give a brief overview of this alter native presentation more information can be found in 115 Definition 1 1 From 1 5
20. being offered and behaves like T Gibson Robinson Efficient Simulation of CSP Like Languages 203 P if so and like Q otherwise Lowe demonstrated its usefulness by giving a notably simple solution to the readers and writers problem that was fair to the writers We were able to successfully simulate this with the simulation taking 60s to complete a safety check In the author s experience the performance of the simulation is perfectly adequate pro viding the number of events is resaonble but unsuitable when the set of events become large This is primarily because the alphabets used by the simulation become prohibitively large and FDR appears to have trouble manipulating them 6 Conclusions In this paper we presented a CSP adaptation of Roscoe s simulation that can be success fully used in FDR Further we gave a number of optimisations to Roscoe s simulation that ensure the resulting simulation runs reasonably efficiently We then proved that these optimi sations maintained the strong bisimulation between the original process and the simulation We also provided some automated recursion refactorings that permit a large class of recur sive definitions to be successfully compiled by FDR even though the standard simulation could not be We then sketched the construction of a tool that can produce the simulation automatically Lastly we described the results of several experiments that show the tool can effectively simulat
21. e other process algebras Future Work The overhead imposed by the simulation is essentially unavoidable and there fore there are unlikely to be ways of significantly improving the performance using the cur rent approach However one option would be to add support directly within FDR for di rectly constructing the state machines for CSP like languages This would entirely avoid the overhead of the simulation and further would negate the need for the complicated recursion refactorings required There are several programs that produce CSP scripts as output such as Roscoe s shared variable compiler and Lowe s Casper Security Protocol Compiler 15 The output of these tools can take a long time to compile sometimes because it was not possible to express certain behaviours as a simple combination of CSP operators Thus it would be interesting to consider if domain specific operators could be added to enable the above scripts to be ex pressed in a way that compiles more efficiently using the new refinement checker mentioned in the previous paragraph Acknowledgements I would like to thank Gavin Lowe who supervised a large part of this work as part of an Oxford undergraduate project 16 Further I would like to thank Gavin for reviewing an early draft of this paper and Bill Roscoe for many interesting discussions concerning this work I would also like to thank the anonymous reviewers for providing many useful comments References 1
22. elease version of FDR3 running in single threaded mode CSP model checking was performed using the same pre release ver sion of FDR3 in single threaded mode CCS model checking was performed using version 7 1 of The Edinburgh Concurrency Workbench 12 In order to directly measure the overhead of the simulation we simulated CSP itself Clearly there is no point in doing this in general but if we compare the time taken to check if a CSP process P satisfies a property to the time taken to check if the same property is satisfies by the simulation of P then it follows that any difference must be due to the overhead of the simulation Table 2 gives the time taken to check if a simple CSP model of the classic Dining Philosophers problem is deadlock free in particular it gives the time taken to find the first counterexample Whilst the simulation is slower note that the magnitude of the difference becomes less as the number of philosophers is increased Further the simulation is still reasonably performant and scales in an almost identical way to the non simulated version indicating that there should be no reason why larger models cannot be checked In order to demonstrate the that tool can effectively model other CSP like process alge bras we compared the performance of a simulation of CCS with a native CCS tool The Edinburgh Concurrency Workbench henceforth CWB As noted in Section I 2 CCS is actually not quite CSP like since 7 resolv
23. ent Using this we can now define a process WrapThread that is analogous to Loop above Note that much of the complexity in the following comes from the fact that the exception operator does not pass which event from the exception set was performed to its right argument We work around this by putting the exception operator in parallel with a regulator that remembers which call Proc event occurred WrapThread P P OfcattProc Start Proc Q gt WrapThread Q H uX callProc p gt startProc p X startProc call Proc call Proc start Proc Note that no call Proc events can propagate out of a process of the form WrapT hread P As callProc Z No it follows that we will have to add the following rule to the operational semantics of the Identity operator in order to allow the callProc events can propagate as discussed above call Proc p Pp P Identity P Identity P p Proc We might ask if similar propagation rules should be added to other operators for on argu ments However it is easy to see that in all but the case of the identity operator that if a callProc event were to propagate then information would be lost For example suppose P a gt P O Rand R b gt R As the call to R on the right of the external choice is replaced by a call Proc event it follows that the recursion would resolve the external choice which is clearly incorrect 196 T Gibson Robinson Efficient Sim
24. entity operator is denoted by Identity Rules Identity 1 a a Identity 1 1 a No Rules Prefiz a a Identity 1 1 1 1 Rules Parallel A 1 a 2 a a Parallel A 1 1 2 2 a A U 1 a Parallel A 1 1 2 2 th th a A U 2 a Parallel A 1 1 2 2 th th a A For the rest of this paper we assume that a function Rules has been defined for the language that we are attempting to model Operator Simulation We now define the process Operator a from 1 2 with some minor alterations that simulates the CSP like operator a The general form that the process will take is Operator a onProcs offProcs Harness P n AlphaProc n n P onProcs Une f1 JonProcs AlphaProc n Reg a onProcs id JonProcs 14 jogprocs 1 Rename tau In the above each on process is run in a harness that will both ensure that it is turned off when necessary and that renames its events to allow the simulation to function correctly The regulator process is responsible for ensuring that only events according to the current operator are allowed to occur Observe that the left hand side of the parallel in the above definition does not de pend on the current operator only the on processes Therefore only Reg differs between T Gibson Robinson Efficient Simulation
25. equired as it is off Note that by definition of an on argument each on argument is at least 1 required gt This is not a restriction in the tool but is added only to simplify the presentation T Gibson Robinson Efficient Simulation of CSP Like Languages 197 Using the above definitions we can now formalise the recursion refactorings that we sketched in Section Firstly we change every recursive calf to a process N to be a callProc event Further if an argument of an operator is infinitely recursive we apply W rapT hread to ensure that no call Proc events propagate out We formalise this as a func tion that returns a CSP process as follows Definition 3 4 Let I be a syntactic process environment and P a syntactic process rec_sim P is defined inductively by rec_sim Op P Py Operator Op lire Op 1 P irec Op N Py rec_sim N callProc N STOP rar Onu Nje Drapa pha i T N cis mnnnitely recursive rec_sim P otherwise irec Op i P rec_sim P Note that the above simulation will no longer be strongly bisimilar to the original process or indeed to sim P This is because whenever a recursion occurs there will be two extra T s resulting from the hidden call Proc events cf WrapThread Whilst this is of theoretical importance this is not of any consequence to the tool since all CSP denotational models equate P and T P Hence a particular refinement check w
26. es which is the CCS analog of O Hence in order to simulate CCS we instead introduce a new event ccs_tau which is used instead of tau in the operational semantics rules Then explicit ccs_tau promotion rules are added to each operator and ccs_tau is hidden at the top level of the simulation It follows that the re sulting operational semantics is CSP like although it is not compositional Once this change has been made the translation of the operational semantics into the form required for tyger is routine Table B details how long it took to verify if the Dining Philosophers problem is deadlock free for an increasing number of philsophers Whilst CWB outperforms the simulation for 6 philosophers or less for 7 philosophers or more the simulation actually outperforms CWB Further CWB was unable to falsify the property within 30 minutes when there were 8 or more philosophers whilst the simulation took just 54s to find a counterexample To a large extent this data justifies the motivation behind the tool Not only is the simulation able to effectively simulate other process algebras but is actually able to improve on the performance of custom tools largely thanks to the optimisation performed on FDR We have had success in simulating a number of other CSP like languages using tyger One interesting example is Lowe s readyness testing extension to CSP 9 This adds a new operator if ready a then P else Q that tests if the event a is
27. h newly turned on process Formally it is a map from 1 k where k is equal to the number of processes turned on to I a 1 where f a y indicates the x newly turned on process is a copy of the y off process e w specifies what the process arguments of p are which can either be currently on processes of a or newly turned on processes according to f Formally it is a map from 1 n 8 to 1 n a k where w y x indicates that the y argument of 3 is either if lt n a then the x on argument of a or otherwise the x n a newly turned on argument i e the f x n a off process of a e x specifies what the off arguments of are in terms of those of a Formally x is a map from I 8 1 to I a 1 where y y x means that the y off argument of 8 is the x off argument of a e B is the set of on processes that are discarded this was not present in Roscoe s model but it is added for clarity In the following we assume that there exists a function Rules that gives the rules for each operator in the language that is being modelled Thus Rules is a function from the set of all operators to the powerset of tuples x 6 f Y X B of the above form For ex ample assuming that the a operator is denoted as Prefiz a and that is denoted as A Parallel A a partial specification of the Rules function for CSP can be encoded as follows where the id
28. imisation can be proven as follows noting that Harness P n P Rename if n can never be turned off We elide the proof since it follows immediately from the definition of Reg and Lemmaj2 1 Lemma 2 3 If Operator a onProcs offProcs evolves into a state in which Harness P n has turned P off then n turned_of f a onProcs offProcs Having performed the optimisations we are now able to compile reasonably sized sys tems with little difficulty Note that the above optimisations do not alter Roscoe s original result since as proven above the optimisations do not affect the semantics of the Operator process 194 T Gibson Robinson Efficient Simulation of CSP Like Languages 3 Recursion As discussed in the introduction FDR cannot successfully compile simulations of recursive processes For example consider simulating CSP within CSP which we do for ease of expo sition only According to the simulation given in Section 2 the process P a gt P would be simulated by the process P Operator Prefiz a PY We calculate the definition of this as FDR would below writing H R for the renaming done by the Harness and R for the renaming done by Operator P Operator Prefiz a PY Reg Prefiz R tau a gt Harness P 0 l Reg Identity DR tau a Harness P 0 Reg Identity R tau a gt P HR l Reg Identity R tau Thus P which is P unwra
29. inite number of argu ments Hence we can now statically bound the maximum number of processes turned on to some number N Therefore the set of all the x B events is given by t B o eE 1 N gt Xoz Xo B C 1 NF We create a new CSP channel renamings that carries events from the above set Using this the remainder of the translation to CSP y is largely mechanical and is therefore elided Efficiency Unfortunately the naive translation of the above into CSP results in scripts that can only support at most a handful of events In order to make the simulation run efficiently a number of optimisations had to be made Some of the simpler optimisations included using sequences rather than sets to represent partial functions and using integers to identify events of the form x B rather than tuples However in order to make the simulation really run efficiently a number of more interesting optimisations were made as we now describe One problem with Operator is that the renamings channel has O 2N 0l Sio 2 members meaning that computing the Harness renaming or the set AlphaProc n will be slow However most operators will never use the majority of the events For example CSP s parallel operator over a set A requires only events of the form 0 a 1 a a 0 b 5 1 b 6 where a A b A In fact all standard CSP operators only use O Xo events Thus when
30. is file can be loaded into FDR and any assertions that are contained can be checked in the usual way Availability tyger has been open sourced and is available from https github com tomgr tyger Included with the code are several examples including a full simulation of CSP a simulation of Lowe s availability models 10 a simulation of Lowe s Readyness Testing extension to CSP 9 and a simulation of a portion of CCS 7 5 Experiments In order to demonstrate the effectiveness of the tool and to establish how efficient the simu lation is we performed a number of experiments which we now describe In this section all 202 T Gibson Robinson Efficient Simulation of CSP Like Languages Number of Philosophers Tool 3 4 5 6 7 8 9 10 Simulation 0 4 1 0 19 33 56 106 33 2 173 2 FDR lt 0 1 lt 01 lt 01 01 02 11 70 42 5 Table 2 Time in seconds to check if a CSP model of the Dining Philosophers is deadlock free for various numbers of philosophers Number of Philosophers Tool 3 4 5 6 7 8 9 CWB lt 0 1 lt 01 03 26 38 5 i i Simulation 0 6 0 8 18 30 8 9 53 9 384 0 Table 3 Time in seconds to check if a CCS model of the Dining Philosophers is deadlock free for various numbers of philosophers The CWB was unable to falsify the property within 30 minutes with 8 or more philosophers experiments were performed on a 64 bit Linux virtual machine with access to 2GB of RAM and two 2 2GHz cores The simulation was run using a pre r
31. ite state The simulation also im poses a very high computational overhead making it impractical for any non trivial problem Further the simulation is extremely complex to construct and the user has to construct the simulation manually 186 T Gibson Robinson Efficient Simulation of CSP Like Languages Contributions In this paper we explain how to alter Roscoe s simulation to allow it to be encoded in machine CSP henceforth CSP m We also give a number of optimisations to Roscoe s simulation to ensure that it can efficiently simulate processes We then prove that the resulting optimised simulation is still strongly bisimilar to the original process We also extend Roscoe s simulation to enable recursive processes to be simulated correctly by FDR We then prove that whilst this alteration is no longer strongly bisimilar it results in a process that is equivalent in all CSP models to the original process We also describe the construction of a tool tyger that takes as input the operational semantics rules of the language in a easy to use format and a list of process definitions to compile again in a natural format The tool automatically produces the CSP simulation described above and also automatically applies the necessary alternations to ensure that re cursive processes can be successfully simulated The output of this tool is thus a CSP file that can be passed to FDR or any other CSP tool This has a number of advantages
32. ming that the identity operator allows call PSim which we discuss further below we obtain the following PSim Loop Operator Prefiz a callPSim STOP Operator Prefiz a callPSim gt STOP OfcauPsimy PSim T Gibson Robinson Efficient Simulation of CSP Like Languages 195 a gt callPSim STOP HR Reg Identity R tau OfcallPSim PSim a gt callPSim gt STOP HR Reg Udentity R tau OfcattPsimy PSim a gt callPSim gt STOP H R Reg Identity R tau Of callP Sim PSim a callPSim gt PSim Hence it follows that PSim callPSim simulates PSim in a way that FDR can suc cessfully compile Note that PSim callPSim is no longer strongly bisimilar to P as there is a T transition whenever PSim recurses However as all CSP denotational models equate 7 gt P and P this is not of any consequence providing the processes are used in refinement checks which is the intention after all 3 2 Generalising the Solution In order to generalise the solution of Section I to arbitrary processes and operators we give a number of refactorings that must be performed on the simulated script The first refactoring will be as above thus we declare a new channel call Proc of type Proc for ease we assume process names may be sent over channels We then replace every call inside a recursive process to another recursive process P with a call Proc P ev
33. n 6 we draw conclusions and discuss future work 1 Background In this section we provide a brief overview of the fragment of CSP necessary to understand the remainder of the paper We also define what it means for an operational semantics to be CSP like which represents the class of operational semantic languages that we can simulate 1 1 A Brief Overview of 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 Further given a channel c the set c C X contains those events of the form c x 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 T Gibson Robinson Efficient Simulation of CSP Like Languages 187 Syntax Meaning a gt P Performs the event a and then behaves like P
34. nd the process behaves like Q The process P O4 Q initially behaves like P but if P ever performs an event from A P is discarded and P O04 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 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 NU 7 and the nodes are process states The usual way of defining the operational semantics of CSP processes is by presenting Structured Operational Semantics SOS style rules For example the operational semantics of P OQ Q can be defined by the following inductive rules P gt P acA P amp P b A P gt Pp POQ SQ PO Q gt P O 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 T performed by a component in this case P into a T performed by the operator The justification for this rule is that 7 is an unobservable event and therefore the operator cannot prevent P from performing the event CSP also has a number of congruent denot
35. oded In this section we start by defining this encoding before explaining the simulation Roscoe s encoding is an expansion of the combinator semantics as presented in Def inition in order to make the combinators more easy to work with As with the combi nator semantics operators such as A are considered as a family of operators one for each A C X Thus the only arguments of an operator are on and off processes Given an operator a we define n a as the number of on arguments and a as the number of off arguments Further we index the on arguments by 1 and off arguments by 1 i e a positive index i refers to the it on process of a whilst a negative index i refers to the it off process of a The operational semantics of an operator a is given by a set of tuples f Y X B where e specifies what event each on process must perform in order for this action to be performed Formally it is a partial map from 1 n a to Xo where x b means the on process performs b This corresponds precisely to in the combinator rules cf Definition I 1 e x is the resulting event from Xo that a performs e 6 is the resulting operator that this process evolves into CCS is not quite CSP like as 7 resolves choice However Roscoe shows how to simulate it in I 190 T Gibson Robinson Efficient Simulation of CSP Like Languages e f denotes which off process of a is used for eac
36. of CSP Like Languages 191 e g Operator ExternalChoice P Q and Operator Parallel d P Q How ever these have very different synchronisation patterns in the former P and Q do not syn chronise whereas in the latter P and Q synchronise on X Therefore it follows that the reg ulator needs to allow all possible synchronisation patterns to occur In order to ensure that we can simulate the two different synchronisation patterns we need to rename the events of each on process to allow the processes to synchronise together in any possible way The regulator could then be defined to allow only those synchronisations that correspond to the current operator Thus the general event form that will be used in the operator simulation will be a tuple x B where e is a partial map from on process to No i e if x y the zt process performs the event y e x is the resulting event e B is the set of on processes that are discarded As we have fixed the event format we are now able to define Rename as the function that re names each x B to x Further AlphaProc n can be defined to be the set of all x B such that n is affected i e n E dom orn B We now consider the definition of Harness P n The harness needs to run the process P as if it were the n on process renaming every event that it performs to one of the above form It also needs to turn this process off when an event of the form
37. ompile such a process More problematically any process of the form P Q O a STOP cannot be simulated since the Q will be converted to callProc Q STOP but call Proc events are not allowed by the simulation of O Thus it follows that the above simulation cannot deal with immediately recursive arguments We extend the simulation to support such arguments in Section 3 4 We can formalise the set of processes for which the simulation is correct as follows In the following definition we only consider operators where each argument of the operator is either only 1 required or infinitely recursive for simplicity The definition and subsequent results can be generalised to arguments that are only k required for k gt 1 4We don t actually need to change every recursive call it actually suffices to change only recursive calls by non recursive processes to recursive processes or by recursive processes to other recursive processes We do not formalise this version since it adds extra complications 198 T Gibson Robinson Efficient Simulation of CSP Like Languages Definition 3 5 e Given a syntactic process P in a process environment P recurses to N iff either P N or P N where T N recurses to N or P Op P Pn and one of the P recurses to N A syntactic process P recurses to N through only on arguments iff P N or P N and T N recurses to N through only on arguments or P Op P
38. operational semantics of the language For example the machine readable version of the SOS rules for the CSP exception operator as given in Section I 1 can be defined as follows Operator Exception P InfRec Q A Syntax Binary 3 gt 12 AssocNone Rule P a gt P a lt diff Sigma A P I A gt Q a gt P A I gt Q EndRule Rule P a gt P P I A gt Q a gt Q EndRule EndOperator In the above Exception P InfRec Q A specifies that the exception operator takes 3 arguments the first of which is a process that is infinitely recursive cf Definition 3 3 The Syntax line provides the information that tyger requires to parse the file In particular it specifies that the operator is a binary operator with concrete syntax 3 gt where 3 refers to the third argument i e A is non associative and has a precedence of 12 which is used to disambiguate non bracketed statements Using this line tyger dynamically con structs a parser using the Haskell Parsec library to parse this file The two Rule constructs gt Hence this violates the conditions of has correct recursion since P recurses through an infinitely recursive argument http hackage haskell org package parsec T Gibson Robinson Efficient Simulation of CSP Like Languages 201 are precisely the machine readable versions of the SOS rules from Section noting that diff Sigma A is
39. or that can clone an on argument 2 on processes cannot be suspended i e if T contains Op P Px where P j ie P is the 7 currently on process of Op then 7 must be an on argument of Op again no CSP operator can suspend and then later reactivate an on argument For example if T 1 then this represents the rule that discards the current operator and discards all process arguments except for 1 Alternatively if T 1 O 1 then the resulting state is the external choice of the 1 argument of the current operator and the newly started process 1 T Gibson Robinson Efficient Simulation of CSP Like Languages 189 For example the external choice operator has two arguments which are both on and the combinator rules consist of the set of all rules of the form a a 1 and a a 2 where a ranges over X The exception operator has two arguments the first of which is on whilst the second is off The set of combinator rules for consists of the set of all rules of the form a a 1 O 1 where a X A and rules of the form a a 1 where a A A CSP like operator is then defined as any operator whose operational semantics can be expressed by a combinator operational semantics A CSP like language is defined as a language in which every operator is CSP like Whilst this might appear to be restrictive it turns out that many process algebras including ccd and the z calculus 8 are CSP
40. ould hold on the original process iff it holds on the above simulation Note that the above simulation is not sufficient for every CSP like operator nor every syntactic process Thus we now consider what syntactic processes the above simulation can handle Firstly observe that the process P Q O P cannot be simulated since the avail able transitions of P directly depend on those of P Prohibiting such processes is an entirely reasonable restriction such a P is not well defined and would be rejected by any CSP based tool including FDR Also consider the process P a gt P STOP Again the simu lation will produce a process that cannot be compiled by FDR since the left hand argument is changed to WrapThread a callProc P STOP Hence when FDR compiles P after an a is performed another copy of P itself containing another copy of WrapThread will be spawned by the original WrapThread We claim that prohibiting such processes is entirely reasonable on the grounds that FDR cannot compile any such process either 1 required arguments require extra restrictions to be placed since by definition no re cursions can be permitted before a visible event has been performed For example the pro cess P P N STOP O a gt STOP is not well defined since the 7 of the M does not resolve the O and thus the transitions of P again directly depend on those of P We believe that such a restriction is reasonable since FDR would also fail to c
41. pped i times is equivalent to PRh P Pui a gt BI AR I Reg Identity R tau Whilst it is certainly true that P is equivalent to any of the other P FDR unsurprisingly does not detect this and instead loops looking for a transition back to P Therefore this results in an unbounded number of copies of Reg Identity being put in parallel In this section we start in Section 3 1 by outlining a simple solution to the recursion issue outline above In Section B 2 we then generalise this to allow a large class of recursive definitions to be compiled We then formalise the transformation and prove it correct in Sec tion 3 3 In Section 3 4 we expand the transformation to permit additional recursive processes to be compiled Lastly in Section 3 5 we discuss the potential limitations of the recursion refactorings presented in this section 3 1 A Simple Solution One solution to the problem above would be to periodically throw away the collection of identity operator regulators that have been spawned For example consider the following simulation of P a gt P PSim Loop Operator Prefiz a callPSim STOP Loop Q Q OfcauPsimy PSim When compiling PSim according to the definition of Loop whenever Operator Prefit a performs a call P Sim event the left argument of O callP3im would be terminated and PSim would be started again In particular if we calculate the definition of PSim as FDR would assu
42. rrect simple recursion Proof Let T and I be as per the lemma By definition of correct recursion and correct simple recursion it suffices to show for each N P I each Op P Py that is a subprocess of P and each on argument P that P has no named on arguments This follows immediately from the definition of inline For optimisation reasons the tool does not implement the refactoring exactly like this but instead detects when the recursion refactoring has to be applied and does so only to such processes This is discussed further in Section 4 3 5 Limitations The recursion refactorings that we have discussed above allow a large class of recursive pro cesses to be successfully simulated However there are fundamental limitations to the range 200 T Gibson Robinson Efficient Simulation of CSP Like Languages of operators that can be simulated in such a way One good example of an operator that can not be simulated using the above construction is the new CSP operator synchronising exter nal choice O4 11 This operator behaves likes a hybrid of external choice and generalised parallel In particular P O4 Q is resolved by P or Q performing a visible event outside of A whilst if P or Q wishes to perform an event from A it must synchronise with the other process Thus Os is equivalent to O whilst Os is equivalent to This operator is
43. the machine readable form of X A Note that tau promotion rules are omitted as they are automatically added After parsing the above file tyger performs a sort of type checking on the operational semantics and infers which arguments of the operators are off and on The type checking is necessary because the side conditions of the operational semantic conditions e g the a lt Sigma can be written in a simple functional language consisting of a simple set comprehen sions It also checks that the operators are CSP like by checking a number of conditions on each SOS rule For example it checks that no on arguments are cloned no on arguments are suspended amongst several other conditions The operational semantics are then converted into the form specified in Section 2 1 At this point the simulation script can be produced which is done by concatenating some constant code that implements the Operator process with some generated code for the Rules function The second input file contains process definitions which thanks to the dynamic parser construction can be specified using natural syntax For instance when defining a CSP pro cess one can simply write P a gt P b gt Q Further the script may contain defini tions using the functional portion of the CSP y language such as head lt x gt xs x The script is then type checked using an experimental CSP y type checker and then has the recursion refactorings applied to it In p
44. ulation of CSP Like Languages 3 3 Formalising the Solution We now consider how to formalise the solution sketched above and in particular we prove that the process that results from the transformations is equivalent in a sense we later for malise to the original simulation In order to prove this we firstly formally define what we are actually simulating In particular we define a syntactic process which corresponds es sentially to a process definition in a CSP y file Definition 3 1 A syntactic process P is defined by the grammar P Op P P N where N represents a process name and Op is a CSP like operator A process environment I is a function from process names to syntactic processes For simplicity we assume that T N is never a process name and is thus always of the form Op Given a syntactic process it is possible to construct a simulation of it using the pro cesses from Section 2 1 Thus we define a function sim P that given a syntactic process P returns the simulation of it For ease we assume that the Operator process defined in Section Z T can be given a single vector of processes rather than two vectors of on and off processes respectively Definition 3 2 The simulation of P in T denoted sim P is defined recursively by sim Op P Pnx Operator Op sim P1 sim Py sim N amp N Note that the above simulation cannot be compiled by FDR if it contains recursive
45. y 1 required then WrapThread rec_sim P sim P where equality is interpreted in any CSP model Proof Sketch Let P and T be as per the lemma Formally this theorem can be proven by a structural induction over P The correctness of this result follows primarily from the require ment that I has correct simple recursion This means that if an argument wishes to perform a call Proc event then the operator must have evolved into the Jdentity operator state which allows the call Proc event to propagate which can then be picked up by WrapThread 3 4 Immediate Recursions The above solution enables many recursive process definitions to be compiled but does not cover every possibility As noted above it does not correctly simulate processes that have im mediate recursion such as P a P O Rand R b gt R In particular in rec_sim P the right hand side of the external choice of P would be replaced by a call Proc event How ever as these are not allowed to propagate through the external choice it follows that only the choice of the left hand side would be presented The simplest solution to the above would be to inline the definition of R within P to yield the process P a P O b gt R which could be successfully simulated in particular it has correct simple recursion and thus Theorem 3 6 applies However this will not work on processes such as P a P O b P since after inlining the process still

Paper

Contents

Download Pdf Manuals

Related Search

Related Contents