A Semantics to Generate the Context-sensitive Synchronized Control-Flow Graph (extended)

A Semantics to Generate the Context-sensitive Synchronized Control-Flow Graph (extended) Marisa Llorens, Javier Oliver, Josep Silva, and Salvador Tamarit Universidad Polit´ecnica de Valencia, Camino de Vera S/N, E-46022 Valencia, Spain {mllorens,fjoliver,jsilva,stamarit}@dsic.upv.es Abstract. The CSP language allows the specification and verification of complex concurrent systems. Many analyses for CSP exist that have been successfully applied in different industrial projects. However, the cost of the analyses performed is usually very high, and sometimes prohibitive, due to the complexity imposed by the non-deterministic execution order of processes and to the restrictions imposed on this order by synchronizations. In this work, we define a data structure that allows us to statically simplify a specification before the analyses. This simplification can drastically reduce the time needed by many CSP analyses. We also introduce an algorithm able to automatically generate this data structure from a CSP specification. The algorithm has been proved correct and its implementation for the CSP’s animator ProB is publicly available. 1 Introduction The Communicating Sequential Processes (CSP) [3, 12] language allows us to specify complex systems with multiple interacting processes. The study and transformation of such systems often implies different analyses (e.g., deadlock analysis [5], reliability analysis [4], refinement checking [11], etc.) which are often based on a data structure able to represent all computations of a specification. Recently, a new data structure called Context-sensitive Synchronized ControlFlow Graph (CSCFG) has been proposed [7]. This data structure is a graph that allows us to finitely represent possibly infinite computations, and it is particularly interesting because it takes into account the context of process calls, and thus it allows us to produce analyses that are very precise. In particular, some analyses (see, e.g., [8, 9]) use the CSCFG to simplify a specification with respect to some term by discarding those parts of the specification that cannot be executed before the term and thus they cannot influence it. This simplification is automatic and thus it is very useful as a preprocessing stage of other analyses. However, computing the CSCFG is a complex task due to the non-deterministic execution of processes, due to deadlocks, due to non-terminating processes and mainly due to synchronizations. This is the reason why there does not exist any correctness result which formally relates the CSCFG of a specification to its execution. This result is needed to prove important properties (such as correctness and completeness) of the techniques based on the CSCFG. 2 M. Llorens et al. In this work, we formally define the CSCFG and a technique to produce the CSCFG of a given CSP specification. Roughly, we instrument the CSP standard semantics (Chapter 7 in [12]) in such a way that the execution of the instrumented semantics produces as a side-effect the portion of the CSCFG associated with the performed computation. Then, we define an algorithm which uses the instrumented semantics to build the complete CSCFG associated with a CSP specification. This algorithm executes the semantics several times to explore all possible computations of the specification, producing incrementally the final CSCFG. 2 The Syntax and Semantics of CSP In order to make the paper self-contained, this section recalls CSP’s syntax and semantics [3,12]. For concretion, and to facilitate the understanding of the following definitions and algorithm, we have selected a subset of CSP that is sufficiently expressive to illustrate the method, and it contains the most important operators that produce the challenging problems such as deadlocks, non-determinism and parallel execution. We use the following domains: process names (M, N . . . ∈Names), processes (P, Q . . . ∈P rocs) and events (a, b . . . ∈Σ). A CSP specification is a finite set of process definitions N=Pwith P=M|a→P|PuQ|P2Q|P|| X⊆Σ Q|ST OP . Therefore, processes can be a call to another process or a combination of the following operators: Prefixing (a→P) Event amust happen before process P. Internal choice (PuQ) The system chooses non-deterministically to execute one of the two processes Por Q. External choice (P2Q) It is identical to internal choice but the choice comes from outside the system (e.g., the user). Synchronized parallelism (P|| X⊆Σ Q) Both processes are executed in parallel with a set Xof synchronized events. In absence of synchronizations both processes can execute in any order. Whenever a synchronized event a∈Xhappens in one of the processes, it must also happen in the other at the same time. Whenever the set of synchronized events is not specified, it is assumed that processes are synchronized in all common events. A particular case of parallel execution is interleaving (represented by |||) where no synchronizations exist (i.e., X=∅). Stop (ST OP ) Synonym of deadlock: It finishes the current process. We now recall the standard operational semantics of CSP as defined by Roscoe [12]. It is presented in Fig. 1 as a logical inference system. A state of the semantics is a process to be evaluated called the control. In the following, we assume that the system starts with an initial state MAIN, and the rules of the semantics are used to infer how this state evolves. When no rules can be applied to the current state, the computation finishes. The rules of the semantics change the states of the computation due to the occurrence of events. The set A Semantics to Generate the CSCFG 3 of possible events is Στ=Σ∪ {τ}. Events in Σare visible from the external environment, and can only happen with its co-operation (e.g., actions of the user). Event τis an internal event that cannot be observed from outside the system and it happens automatically as defined by the semantics. In order to perform computations, we construct an initial state and (non-deterministically) apply the rules of Fig. 1. (Process Call) (Prefixing) (Internal Choice 1) (Internal Choice 2) Nτ −→ rhs(N) (a→P)a −→ P(PuQ)τ −→ P(PuQ)τ −→ Q (External Choice 1) (External Choice 2) (External Choice 3) (External Choice 4) Pτ −→ P0 (PQ)τ −→ (P0Q) Qτ −→ Q0 (PQ)τ −→ (PQ0) Pe −→ P0 (PQ)e −→ P0e∈ΣQe −→ Q0 (PQ)e −→ Q0e∈Σ (Synchronized Parallelism 1) (Synchronized Parallelism 2) (Synchronized Parallelism 3) Pe −→ P0 (P|| X Q)e −→ (P0|| X Q)e∈Στ\XQe −→ Q0 (P|| X Q)e −→ (P|| X Q0)e∈Στ\XPe −→ P0Qe −→ Q0 (P|| X Q)e −→ (P0|| X Q0)e∈X Fig. 1. CSP’s operational semantics 3 Context-sensitive Synchronized Control-Flow Graphs The CSCFG was proposed in [7, 9] as a data structure able to finitely represent all possible (often infinite) computations of a CSP specification. This data structure is particularly useful to simplify a CSP specification before its static analysis. The simplification of industrial CSP specifications allows us to drastically reduce the time needed to perform expensive analyses such as model checking. Algorithms to construct CSCFGs have been implemented [8] and integrated into the most advanced CSP environment ProB [6]. In this section we introduce a new formalization of the CSCFG that directly relates the graph construction to the control-flow of the computations it represents. A CSCFG is formed by the sequence of expressions that are evaluated during an execution. These expressions are conveniently connected to form a graph. In addition, the source position (in the specification) of each literal (i.e., events, operators and process names) is also included in the CSCFG. This is very useful because it provides the CSCFG with the ability to determine what parts of the source code have been executed and in what order. The inclusion of source positions in the CSCFG implies an additional level of complexity in the semantics, but the benefits of providing the CSCFG with this additional information are clear and, for some applications, essential. Therefore, we use labels (that we call specification positions) to identify each literal in a specification which roughly 4 M. Llorens et al. corresponds to nodes in the CSP specification’s abstract syntax tree. We define a function Pos to obtain the specification position of an element of a CSP specification and it is defined over nodes of an abstract syntax tree for a CSP specification. Formally, Definition 1. (Specification position) A specification position is a pair (N, w) where N∈ N and wis a sequence of natural numbers (we use Λto denote the empty sequence). We let Pos(o)denote the specification position of an expression o. Each process definition N=Pof a CSP specification is labelled with specification positions. The specification position of its left-hand side is Pos(N) = (N, 0). The right-hand side (abbrev. rhs) is labelled with the call AddSpPos(P, (N, Λ)); where function AddSpPos is defined as follows: AddSpPos(P, (N, w))=                P(N,w)if P∈ N ST OP(N,w)if P=ST OP a(N,w.1) →(N,w)AddSpPos(Q, (N, w.2)) if P=a→Q AddSpPos(Q, (N, w.1)) op(N,w)AddSpPos(R, (N, w.2)) if P=Q op R ∀op ∈ {u,2,||} We often use Pos(S)to denote a set with all positions in a specification S. Example 1. Consider the CSP specification in Fig. 2(a) where literals are labelled with their associated specification positions (they are underlined) so that labels are unique. MAIN(MAIN,0)= (a(MAIN,1.1)→(MAIN,1)STOP(MAIN,1.2))k {a} (MAIN,Λ) (P(MAIN,2.1)2(MAIN,2)(a(MAIN,2.2.1)→(MAIN,2.2)STOP(MAIN,2.2.2))) P(P,0)=b(P,1)→(P,Λ)SKIP(P,2) (a) CSP specification || MAIN,Λ  MAIN,2 a MAIN,1.1 → MAIN,1 STOP MAIN,1.2 P MAIN,2.1 b P,1 → P,Λ STOP P,2 a MAIN,2.2.1 → MAIN,2.2 STOP MAIN,2.2.2 1 2 3 4 5 6 9 10 12 7 8 11 MAIN MAIN,0 0 (b) CSCFG Fig. 2. CSP specification and its associated CSCFG In the following, specification positions will be represented with greek letters (α, β, . . .) and we will often use indistinguishably an expression and its associated specification position when it is clear from the context (e.g., in Example 1 we will refer to (P,1) as b). A Semantics to Generate the CSCFG 5 In order to introduce the definition of CSCFG, we need first to define the concepts of control-flow,path and context. Definition 2. (Control-flow) Given a CSP specification S, the control-flow is a transitive relation between the specification positions of S. Given two specification positions α, β in S, we say that the control of αcan pass to βiff i) α=N∧β=first((N, Λ)) with N=rhs(N)∈ S ii) α∈ {u,2,||} ∧ β∈ {first(α.1),first(α.2)} iii) α=β.1∧β=→ iv) α=→ ∧ β=first(α.2) where first(α)is defined as follows: first(α) = α.1 if α=→ αotherwise We say that a specification position αis executable in Siff the control can pass from the initial state (i.e., MAIN) to α. For instance, in Example 1, the control can pass from (MAIN,2.1) to (P,1) due to rule i), from (MAIN,2) to (MAIN,2.1) and (MAIN,2.2.1) due to rule ii), from (MAIN,2.2.1) to (MAIN,2.2) due to rule iii), and from (MAIN,2.2) to (MAIN,2.2.2) due to rule iv). As we will work with graphs whose nodes are labelled with positions, we use l(n) to refer to the label of node n. Definition 3. (Path) Given a labelled graph G= (N, E), a path between two nodes n1,m∈N,P ath(n1, m), is a sequence n1,...,nksuch that nk7→ m∈E and for all 1≤i<k we have ni7→ ni+1 ∈E. The path is loop-free if for all i6=j we have ni6=nj. Definition 4. (Context) Given a labelled graph G= (N, E)and a node n∈N, the context of n,Con(n) = {m|l(m)=Mwith (M=P)∈ S and there exists a loop-free path m7→∗n}. Intuitively speaking, the context of a node represents the set of processes in which a particular node is being executed. This is represented by the set of process calls in the computation that were done before the specified node. For instance, the CSCFG associated with the specification in Example 1 is shown in Fig. 2(b). In this graph we have that Con(4)={0,3}, i.e., bis being executed after having called processes MAIN and P. Note that focussing on a process call node we can use the context to identify loops; i.e., we have a loop whenever n∈ Con(m) with l(n) = l(m)∈Names. Note also that the CSCFG is unique for a given CSP specification [9]. Definition 5. (Context-sensitive Synchronized Control-Flow Graph) Given a CSP specification S, its Context-sensitive Synchronized Control-Flow Graph (CSCFG) is a labelled directed graph G= (N, Ec, El, Es)where Nis a set of nodes such that ∀n∈N. l(n)∈ Pos(S)and l(n)is executable in S; and edges are divided into three groups: control-flow edges (Ec), loop edges (El) and synchronization edges (Es). 6 M. Llorens et al. –Ecis a set of one-way edges (denoted with 7→) representing the possible control-flow between two nodes. Control edges do not form loops. The root of the tree formed by Ecis the position of the initial call to MAIN. –Elis a set of one-way edges (denoted with ) such that (n1 n2)∈Eliff l(n1)and l(n2)are (possibly different) process calls that refer to the same process M∈ N and n2∈ Con(n1). –Esis a set of two-way edges (denoted with e) representing the possible synchronization of two event nodes (l(n)∈Σ). –Given a CSCFG, every node labelled (M, Λ)has one and only one incoming edge in Ec; and every process call node has one and only one outgoing edge which belongs to either Ecor El. Example 2. Consider again the specification of Example 1, shown in Fig. 2(a), and its associated CSCFG, shown in Fig. 2(b). For the time being, the reader can ignore the numbering and color of the nodes; they will be explained in Section 4. Each process call is connected to a subgraph which contains the right-hand side of the called process. For convenience, in this example there are no loop edges; there are control-flow edges and one synchronization edge between nodes (MAIN,2.2.1) and (MAIN,1.1) representing the synchronization of event a. Note that the CSCFG shows the exact processes that have been evaluated with an explicit causality relation; and, in addition, it shows the specification positions that have been evaluated and in what order. Therefore, it is not only useful as a program comprehension tool, but it can be used for program simplification. For instance, with a simple backwards traversal from a, the CSCFG reveals that the only part of the code that can be executed before ais the underlined part: MAIN = (a→STOP)k {a} (P2(a→STOP)) P=b→STOP Hence, the specification can be significantly simplified for those analyses focussing on the occurrence of event a. 4 An Algorithm to Generate the CSCFG This section introduces an algorithm able to generate the CSCFG associated with a CSP specification. The algorithm uses an instrumented operational semantics of CSP which (i) generates as a side-effect the CSCFG associated with the computation performed with the semantics; (ii) it controls that no infinite loops are executed; and (iii) it ensures that the execution is deterministic. Algorithm 1 controls that the semantics is executed repeatedly in order to deterministically execute all possible computations—of the original (nondeterministic) specification—and the CSCFG for the whole specification is constructed incrementally with each execution of the semantics. The key point of A Semantics to Generate the CSCFG 7 the algorithm is the use of a stack that records the actions that can be performed by the semantics. In particular, the stack contains tuples of the form (rule, rules) where rule indicates the rule that must be selected by the semantics in the next execution step, and rules is a set with the other possible rules that can be selected. The algorithm uses the stack to prepare each execution of the semantics indicating the rules that must be applied at each step. For this, function UpdStack is used; it basically avoids to repeat the same computation with the semantics. When the semantics finishes, the algorithm prepares a new execution of the semantics with an updated stack. This is repeated until all possible computations are explored (i.e., until the stack is empty). The standard operational semantics of CSP [12] can be non-terminating due to infinite computations. Therefore, the instrumentation of the semantics incorporates a loop-checking mechanism to ensure termination. Algorithm 1 General Algorithm Build the initial state of the semantics: state = (MAIN(MAIN,0),∅,•,(∅,∅),∅,∅) repeat repeat Run the rules of the instrumented semantics with the state state until no more rules can be applied Get the new state: state = ( , G, , (∅, S0), , ζ) state=(MAIN(MAIN,0), G, •,(UpdStack(S0),∅),∅,∅) until UpdStack(S0) = ∅ return G where function UpdStack is defined as follows: UpdStack(S) =    (rule, rules\{rule}) : S0if S= ( , rules) : S0and rule ∈rules UpdStack(S0) if S= ( ,∅) : S0 ∅if S=∅ The instrumented semantics used by Algorithm 1 is shown in Fig. 3. It is an operational semantics where we assume that every literal in the specification has been labelled with its specification position (denoted by a subscript, e.g., Pα). In this semantics, a state is a tuple (P, G, m, (S, S0), ∆, ζ), where Pis the process to be evaluated (the control), Gis a directed graph (i.e., the CSCFG constructed so far), mis a numeric reference to the current node in G, (S, S0) is a tuple with two stacks (where the empty stack is denoted by ∅) that contains the rules to apply and the rules applied so far, ∆is a set of references to nodes used to draw synchronizations in Gand ζis a graph like G, but it only contains the part of the graph generated for the current computation, and it is used to detect loops. The basic idea of the graph construction is to record the current control with a fresh reference1nby connecting it to its parent m. We use the notation G[nm 7→α] either to introduce a node in Gor as a condition on G(i.e., Gcontains node n). This node has reference n, is labelled with specification position αand its 1We assume that fresh references are numeric and generated incrementally. 8 M. Llorens et al. parent is m. The edge introduced can be a control, a synchronization or a loop edge. This notation is very convenient because it allows us to add nodes to G, but also to extract information from G. For instance, with G[3 m 7→α] we can know the parent of node 3 (the value of m), and the specification position of node 3 (the value of α). Note that the initial state for the semantics used by Algorithm 1 has MAIN(MAIN,0) in the control. This initial call to MAIN does not appear in the specification, thus we label it with a special specification position (MAIN,0) which is the root of the CSCFG (see Fig. 2(b)). Note that we use •as a reference in the initial state. The first node added to the CSCFG (i.e., the root) will have parent reference •. Therefore, here •denotes the empty reference because the root of the CSCFG has no parent. An explanation for each rule of the semantics follows. (Process Call) (Nα, G, m, (S, S0), ∆, ζ)τ −→ (P0, G0, n, (S, S0),∅, ζ0) (P0, G0, ζ0) = LoopCheck(N, n, G[nm 7→ α], ζ ∪ {nm 7→ α}) (Prefixing) (aα→βP, G, m, (S, S0), ∆, ζ)a −→ (P, G[nm 7→ α, o n 7→ β], o, (S, S0),{n}, ζ ∪ {nm 7→ α, o n 7→ β}) (Choice) (PuαQ, G, m, (S, S0), ∆, ζ)τ −→ (P0, G[nm 7→ α], n, (S0, S0 0),∅, ζ ∪ {nm 7→ α}) (P0,(S0, S0 0)) = SelectBranch(PuαQ, (S, S0)) (STOP) (ST OPα, G, m, (S, S0), ∆, ζ)τ −→ (⊥, G[nm 7→ α], n, (S, S0),∅, ζ ∪ {nm 7→ α}) Fig. 3. An instrumented operational semantics that generates the CSCFG (Process Call) The called process Nis unfolded, node n(a fresh reference) is added to the graphs Gand ζwith specification position αand parent m. In the new state, nrepresents the current reference. The new expression in the control is P0, computed with function LoopCheck which is used to prevent infinite unfolding and is defined below. No event can synchronize in this rule, thus ∆is empty. LoopCheck(N, n, G, ζ)=   (s(rhs(N)), G[n s], ζ ∪ {n s}) if ∃s.s t 7→N∈G ∧s∈P ath(0, n) (rhs(N), G, ζ) otherwise Function LoopCheck checks whether the process call in the control has not been already executed (if so, we are in a loop). When a loop is detected, the right- A Semantics to Generate the CSCFG 9 (Synchronized Parallelism 1) (P1, G0, n0,(S0,(SP1, rules) : S0), ∆, ζ0)e −→ (P10, G00, n00,(S00, S0 0), ∆0, ζ00) (P1k X (α,n1,n2,Υ )P2, G, m, (S0: (SP1, rules), S0), ∆, ζ)e −→ (P0, G00, m, (S00, S0 0), ∆0, ζ00)e∈Στ\X (G0, ζ0, n0)=InitBranch(G, ζ, n1, m, α)∧P0=  m(Unloop(P10k X(α,n00,n2,Υ )P2) if ζ=ζ00 P10k X(α,n00,n2,Υ )P2 otherwise (Synchronized Parallelism 2) (P2, G0, n0,(S0,(SP2, rules):S0), ∆, ζ0)e −→ (P20, G00, n00,(S00, S0 0), ∆0, ζ00) (P1k X (α,n1,n2,Υ )P2, G, m, (S0: (SP2, rules), S0), ∆, ζ)e −→ (P0, G0, m, (S00, S0 0), ∆0, ζ00) e∈Στ\X (G0, ζ0, n0)=InitBranch(G, ζ, n2, m, α)∧P0=  m(Unloop(P1k X(α,n1,n00,Υ )P20) if ζ=ζ00 P1k X(α,n1,n00,Υ )P20otherwise (Synchronized Parallelism 3) Left Right (P1k X (α,n1,n2,Υ )P2, G, m, (S0: (SP3, rules), S0), ∆, ζ)e −→ (P0, G00, m, (S000, S00 0), ∆1∪∆2, ζ0∪syncs) e∈X (G0 1, ζ1, n0 1)=InitBranch(G, ζ, n1, m, α)∧Left = (P1, G0 1, n0 1,(S0,(SP3, rules) : S0), ∆, ζ1)e −→ (P10, G00 1, n00 1,(S00, S0 0), ∆1, ζ0 1)∧ (G0 2, ζ2, n0 2)=InitBranch(G00 1, ζ0 1, n2, m, α)∧Right = (P2, G0 2, n0 2,(S00, S0 0), ∆, ζ2)e −→ (P20, G00, n00 2,(S000, S00 0), ∆2, ζ0)∧ sync ={s1es2|s1∈∆1∧s2∈∆2} ∧ ∀ (men)∈sync . G00[men]∧P0=  m(Unloop(P10k X(α,n00 1,n00 2,•)P20)) if (sync ∪ζ0) = ζ P10k X(α,n00 1,n00 2,•)P20otherwise (Synchronized Parallelism 4) (P1k X (α,n1,n2,Υ )P2, G, m, (S0: (SP4, rules), S0), ∆, ζ)τ −→ (P0, G, m, (S0,(SP4, rules) : S0),∅, ζ) P0=LoopControl(P1k X (α,n1,n2,Υ )P2, m) (Synchronized Parallelism 5) (P1k X (α,n1,n2,Υ )P2, G, m, ([(rule, rules)], S0), ∆, ζ)e −→ (P, G0, m, (S0, S0 0), ∆0, ζ0) (P1k X (α,n1,n2,Υ )P2, G, m, (∅, S0), ∆, ζ)e −→ (P, G0, m, (S0, S0 0), ∆0, ζ0)e∈Στ rule ∈AppRules(P1k X P2) ∧rules =AppRules(P1k X P2)\{rule} Fig. 3. An instrumented operational semantics that generates the CSCFG (cont.) 16 M. Llorens et al. (SP5) (SP4) ((a→STOP)k {a} ((MAIN,Λ),•,6,•)⊥, G5,0,([(SP4,∅)], S5),∅,∅)τ −→ (⊥, G5,0,(∅,(SP4,∅) : S5),∅,∅) State 5τ −→ State 6 where State 6 = (⊥, G5,0,(∅, S6),∅,∅) and S6= [(SP4,∅),(SP2,∅),(SP2,∅),(SP2,∅),(C1,{C2}),(SP2,∅)] State 7 = (MAIN(MAIN,0) , G5,•,(UpdStack(S6),∅),∅,∅) = (MAIN(MAIN,0), G5,•,([(C2,∅),(SP2,∅)],∅),∅,∅) (Process Call) State 7τ −→ State 8 where State 8 = ((a→STOP)k {a} ((MAIN,Λ),•,•,•)(P2(a→STOP)), G5[0 7→ (MAIN,0)],0,(S8,∅),∅,∅) and S8= [(C2,∅),(SP2,∅)] (SP2) (Choice) (P2(a→STOP), G5[1 0 7→ (MAIN, Λ)],1,([(C2,∅)],[(SP2,∅)]),∅,∅)τ −→ (a→STOP, G5[2 1 7→ (MAIN,2)],2,(∅, S9),∅,∅) State 8τ −→ State 9 where State 9 = ((a→STOP)k {a} ((MAIN,Λ),•,2,•)(a→STOP), G5,0,(∅, S9),∅,∅) and S9= [(C2,∅),(SP2,∅)] (SP5) (SP3) L R ((a→STOP)k {a} ((MAIN,Λ),•,2,•)(a→STOP), G5,0,([(SP3,∅)], S9),∅,∅)a −→ State 10 State 9a −→ State 10 where L=(Prefix) (a→STOP, G5[1 0 7→ (MAIN, Λ)],1,(∅,(SP3,∅):S9),∅,∅)a −→ (STOP, G5[7 1 7→ (MAIN,1.1),87 7→ (MAIN,1)],8,(∅, S10),{7},∅) R=(Prefix) (a→STOP, G5,2,(∅, S10),∅,∅)a −→ (STOP, G5[9 2 7→ (MAIN,2.2.1),10 9 7→ (MAIN,2.2)],10,(∅, S10),{9},∅) and State 10 = (STOP k {a} ((MAIN,Λ),8,10,•)STOP, G6,0,(∅, S10 ),{7,9},{7e9}) and S10 = [(SP3,∅),(C2,∅),(SP2,∅)] Fig. 5. An example of computation (step by step) with Algorithm 1 (cont.) A Semantics to Generate the CSCFG 17 (SP5) (SP1) (STOP) (STOP, G6,9,(∅,(SP1,∅) : S10),{7,9},{7e9})τ −→ (⊥, G6[11 8 7→ (MAIN,1.2)],11,(∅, S11),∅,{7e9}) (STOP k {a} ((MAIN,Λ),8,10,•)STOP, G6,0,([(SP1,∅)], S10),{7,9},{7e9})τ −→ State 11 State 10 τ −→ State 11 where State 11 = (⊥ k {a} ((MAIN,Λ),11,10,•)STOP, G7,0,(∅, S11),∅,{7e9}) and S11 = [(SP1,∅),(SP3,∅),(C2,∅),(SP2,∅)] (SP5) (SP2) (STOP) (STOP, G7,10,(∅,(SP2,∅):S11),∅,{7e9})τ −→ (⊥, G7[12 10 7→ (MAIN,2.2.2)],12,(∅, S12),∅,{7e9}) (⊥ k {a} ((MAIN,Λ),11,10,•)STOP, G7,0,([(SP2,∅)], S11),∅,{7e9})τ −→ State 12 State 11 τ −→ State 12 where State 12 = (⊥ k {a} ((MAIN,Λ),11,12,•)⊥, G8,0,(∅, S12 ),∅,{7e9}) and S12 = [(SP2,∅),(SP1,∅),(SP3,∅),(C2,∅),(SP2,∅)] (SP5) (SP4) (⊥ k {a} ((MAIN,Λ),11,12,•)⊥, G8,0,([(SP4,∅)], S12),∅,{7e9})τ −→ (⊥, G8,0,(∅,(SP4,∅) : S12),∅,{7e9}) State 12 τ −→ State 13 where State 13 = (⊥, G8,0,(∅, S13),∅,{7e9}) and S13 = [(SP4,∅),(SP2,∅),(SP1,∅),(SP3,∅),(C2,∅),(SP2,∅)] State 14 = (MAIN(MAIN,0) , G8[7 e9],•,(UpdStack(S13),∅),∅,∅) = (MAIN(MAIN,0), G9,•,(∅,∅),∅,∅) Fig. 5. An example of computation (step by step) with Algorithm 1 (cont.) 18 M. Llorens et al. Example 4. Consider the following CSP specification where each literal has been labelled (they are underlined) with their associated specification position. MAIN =a(MAIN,1.1)→(MAIN,1)a(MAIN,1.2.1)→(MAIN,1.2)STOP(MAIN,1.2.2)k {a} (MAIN,Λ)P(MAIN,2) P=a(P,1)→(P,Λ)P(P,2) Following Algorithm 1, we use the initial state (MAIN(MAIN,0),∅,•,(∅,∅),∅,∅) to execute the semantics and get the computation of Fig. 7. This computation produces as a side effect the CSCFG shown in Fig. 6 for this specification. In this CSCFG, there is a loop edge between (P,2) and (MAIN,2). Note that the loop edge avoids infinite unfolding of the infinite process P, thus ensuring that the CSCFG is finite. Loop edges are introduced by the semantics whenever the context is repeated. In Fig. 7, when process Pis called a second time, rule (Process call) unfolds P, its right-hand side is marked as a loop and a loop edge between nodes 7 and 2 is added to the graph. In State 4, the looped process is in parallel with a process waiting to synchronize with it. In order to perform the synchronization, the loop is unlabelled (State 5) by rule (SP4). Later, it is labelled again by rule (Process Call) when the loop is repeated (State 8 in Fig. 7 (cont.)). Finally, rule (SP4) detects that the left branch of the parallelism is deadlocked and the parallelism is marked as a loop (State 9), thus finishing the computation. a MAIN,1.1 || MAIN,Λ → MAIN,1 a MAIN,1.2.1 P MAIN,2 1 3 4 → MAIN,1.2 STOP MAIN,1.2.2 8 a P,1 → P,Λ P P,2 9 10 2 5 6 7 MAIN MAIN,0 0 Fig. 6. CSCFG associated with the CSP specification in Example 4 A Semantics to Generate the CSCFG 19 (Process Call) (MAIN(MAIN,0),∅,•,(∅,∅),∅,∅)τ −→ State 1where State 1 = ((a→a→STOP k {a} ((MAIN,Λ),•,•,•)P), G0[0 7→ (MAIN,0)],•,(∅,∅),∅,∅) (SP5) (SP2) (Process Call) (P, G1[1 0 7→ (MAIN, Λ)],1,(∅,[(SP2,∅)]),∅,∅)τ −→ (a→P, G1[2 1 7→ (MAIN,2)],2,(∅,[(SP2,∅)]),∅,∅) ((a→a→STOP k {a} ((MAIN,Λ),•,•,•)P), G1,•,([(SP2,∅)],∅),∅,∅)τ −→ State 2 State 1τ −→ State 2 where State 2 = ((a→a→STOP k {a} ((MAIN,Λ),•,2,•)a→P), G2,0,(∅, S2),∅,∅) and S2= [(SP2,∅)] (SP5) (SP3) L R ((a→a→STOP k {a} ((MAIN,Λ),•,2,•)a→P), G2,0,([(SP3,∅)], S2),∅,∅)a −→ State 3 State 2a −→ State 3where L=(Prefix) (a→a→STOP, G2[1 0 7→ (MAIN, Λ)],1,(∅,(SP3,∅):S2),∅,∅)a −→ (a→STOP, G2[3 1 7→ (MAIN,1.1),43 7→ (MAIN,1)],4,(∅, S3),{3},∅) R=(Prefix) (a→P, G2,2,(∅, S3),∅,∅)a −→ (P, G2[5 2 7→ (P,1),65 7→ (P, Λ)],6,(∅, S3),{5},∅) and State 3 = (a→STOP k {a} ((MAIN,Λ),4,6,•)P, G3,0,(∅, S3),{3,5},{3e5}) and S3= [(SP3,∅),(SP2,∅)] (SP5) (SP2) (Process Call) (P, G3,6,(∅,(SP2,∅) : S3),{3,5},{3e5})τ −→ (2(a→P), G3[7 6 7→ (P,2),7 2],7,(∅, S4),∅,{3e5}) (a→STOP k {a} ((MAIN,Λ),4,6,•)P, G3,0,([(SP2,∅)], S3),{3,5},{3e5})τ −→ State 4 State 3τ −→ State 4 where State 4 = ((a→STOP)k {a} ((MAIN,Λ),4,7,•)2(a→P), G4,0,(∅, S4),∅,{3e5}) and S4= [(SP2,∅),(SP3,∅),(SP2,∅)] Fig. 7. Computation of the specification in Example 4 with Algorithm 1 20 M. Llorens et al. (SP5) (SP4) ((a→STOP)k {a} ((MAIN,Λ),4,7,•)2(a→P), G4,0,([(SP4,∅)], S4),∅,{3e5})τ −→ State 5 State 4τ −→ State 5 where State 5 = ((a→STOP)k {a} ((MAIN,Λ),4,2,2) (a→P), G4,0,(∅, S5),∅,{3e5}) and S5= [(SP4,∅),(SP2,∅),(SP3,∅),(SP2,∅)] (SP5) (SP3) L R ((a→STOP)k {a} ((MAIN,Λ),4,2,2) (a→P), G4,0,([(SP3,∅)], S5),∅,{3e5})a −→ State 6 State 5a −→ State 6where L=(Prefix) (a→STOP, G, 4,(∅,(SP3,∅):S5),∅,{3e5})a −→ (STOP, G4[8 4 7→ (MAIN,1.2.1),98 7→ (MAIN,1.2)],9,(∅, S6),{8},{3e5}) R=(Prefix) (a→P, G4,2,(∅, S6),∅,{3e5})a −→ (P, G4[5 2 7→ (P,1),65 7→ (P, Λ)],6,(∅, S6),{5},{3e5}) and State 6 = (STOP k {a} ((MAIN,Λ),9,6,•)P, G5,0,(∅, S6),{8,5},{3e5,8e5}) and S6= [(SP3,∅),(SP4,∅),(SP2,∅),(SP3,∅),(SP2,∅)] Fig. 7. Computation of the specification in Example 4 with Algorithm 1 (cont.) 5 Correctness In this section we state the correctness of the proposed algorithm by showing that (i) the graph produced by the algorithm for a CSP specification Sis the CSCFG A Semantics to Generate the CSCFG 21 (SP5) (SP1) (STOP) (STOP, G5,9,(∅,(SP1,∅):S6),∅,{3e5,8e5})τ −→ (⊥, G5[10 9 7→ (MAIN,1.2.2)],10,(∅, S7),∅,{3e5,8e5}) (STOP k {a} ((MAIN,Λ),9,6,•)P, G5,0,([(SP1,∅)], S6),{8,5},{3e5,8e5})τ −→ State 7 State 6τ −→ State 7 where State 7 = (⊥ k {a} ((MAIN,Λ),10,6,•)P, G6,0,(∅, S7),∅,{3e5,8e5}) and S7= [(SP1,∅),(SP3,∅),(SP4,∅),(SP2,∅),(SP3,∅),(SP2,∅)] (SP5) (SP2) (Process Call) (P, G6,6,(∅,(SP2,∅):S7),∅,{3e5,8e5})τ −→ (2(a→P), G6,7,(∅, S8),∅,{3e5,8e5}) (⊥ k {a} ((MAIN,Λ),10,7,•)P), G6,0,([(SP2,∅), S7)],∅,{3e5,8e5})τ −→ State 8 State 7τ −→ State 8 where State 8 = (⊥ k {a} ((MAIN,Λ),10,7,•)2(a→P), G6,0,(∅, S8),∅,{3e5,8e5}) and S8= [(SP2,∅),(SP1,∅),(SP3,∅),(SP4,∅),(SP2,∅),(SP3,∅),(SP2,∅)] (SP5) (SP4) (⊥ k {a} ((MAIN,Λ),10,7,•)2(a→P), G6,0,([(SP4,∅)], S8),∅,{3e5,8e5})τ −→ State 9 State 8τ −→ State 9 where State 9 = (0(⊥ k {a} ((MAIN,Λ),10,2,•)(a→P)), G6,0,(∅, S9),∅,{3e5,8e5}) and S9= [(SP4,∅),(SP2,∅),(SP1,∅),(SP3,∅),(SP4,∅),(SP2,∅),(SP3,∅),(SP2,∅)] State 10 = (MAIN(MAIN,0), G6[3 e5,8e5],•,(UpdStack(S9),∅),∅,∅) = (MAIN(MAIN,0), G7,•,(∅,∅),∅,∅) Fig. 7. Computation of specification in Example 4 with Algorithm 1 (cont.) of S; and (ii) the algorithm terminates, even if non-terminating computations exist for the specification S. In order to prove these theorems, we need some preliminary definitions and lemmas. 22 M. Llorens et al. Definition 6. (Rewriting Step, Derivation) Given a state sof the instrumented semantics, a rewriting step for s(sΘ s0) is the application of a rule of the semantics Θ se −→ s0with the occurrence of an event e∈Στand where Θis a (possibly empty) set of rewriting steps. Given a state s0, we say that the sequence s0 Θ0 ... Θn sn+1,n≥0, is a derivation of s0iff ∀i, 0≤i≤n, si Θi si+1 is a rewriting step. We say that the derivation is complete iff there is no possible rewriting step for sn+1. We say that two derivations D,D0are equivalent (denoted D ≡ D0) iff all specification positions in the control of a rewriting step of Dalso appear in a rewriting step of D0and viceversa. The following lemma ensures that all possible derivations of Sare explored by Algorithm 1. Lemma 1. Let Sbe a CSP specification and Da complete derivation of S performed with the standard semantics. Then, Algorithm 1 performs a derivation D0such that D ≡ D0. Proof. We prove first that the algorithm executes the instrumented semantics with a collection of initial states that explores all possible derivations. We prove this showing that every non-deterministic application of a rule is stored in the stack with all possible rules that can be applied; then, Algorithm 1 restarts the semantics with a new state that forces the semantics to explore a new derivation. This is done until all possible derivations have been explored. Firstly, the standard semantics is deterministic except for two rules: (i) choice: the choice rules are evaluated until one branch is selected; and (ii) synchronized parallelism: the branches of the parallelism can be executed in any order. In the case of choices, it is easy to see that the only applicable rule in the instrumented semantics is (Choice). Let us assume that we evaluate this rule with a pair of stacks (S, S0). There are two possibilities in this rule: If Sis empty, this rule puts in the control the left branch, and [(C1,{C2})] is added to S0, meaning that the left branch of the choice is executed and the right branch is pending. Therefore, we can ensure that the left branch is always explored because the algorithm evaluates the semantics with an initially empty stack. If the last element of Sis either (C1,{C2}) or (C2,∅), the semantics evaluates the first (resp. second) branch and deletes this element from S, and adds it to S0. We know that none of the other rules changes the stacks except (Synchronized Parallelism), and they both ((Synchronized Parallelism) and (Choice)) do it in the same manner. Therefore, we only have to ensure that the algorithm takes the stack S0, selects another possibility (e.g., if C1 was selected in the previous evaluation, then C2 is selected in the next evaluation, i.e., if the head of the stack is (C1,{C2}) it is changed to (C2,∅)), puts it in the new initial state as the stack S, and the other stack is initialised for the next computation. This is exactly what the algorithm does by using function UpdStack. In the case of synchronized parallelism, the semantics does exactly the same, but this case is a bit more complex because there are five different rules than can A Semantics to Generate the CSCFG 23 be applied. In the standard semantics, non-determinism comes from the fact that both (Synchronized Parallelism 1) and (Synchronized Parallelism 2) can be executed with the same state. If this happens, the instrumented semantics executes one rule first and then the other, and all the way around in the next evaluation. When a parallelism operator is in the control and the stack is empty, rule (Synchronized Parallelism 5) is executed. This rule uses function AppRules to determine what rules could be applied. If non-determinism exists in the standard semantics, it also exists in the instrumented semantics, because the control of both semantics is the same except for the following cases: STOP Rule (STOP) of the instrumented semantics is not present in the standard semantics. When a STOP is reached in a derivation, the standard semantics stops the (sub)computation because no rule is applicable. In the instrumented semantics, when a STOP is reached in a derivation, the only rule applicable is (STOP) which performs τand puts ⊥in the control. Then, the (sub)computation is stopped because no rule is applicable for ⊥. Therefore, when the control in the derivation is STOP, the instrumented semantics performs one additional rewriting step with rule (STOP). Therefore, no additional non-determinism appears in the instrumented semantics due to (STOP). ⊥This symbol only appears in the instrumented semantics. If it is in the control, the computation terminates because no rule can be applied. Therefore, no additional non-determinism appears in the instrumented semantics due to ⊥. This symbol is introduced in the computation by (Process Call) or (Synchronized Parallelism 1, 2 and 3). Once it is introduced, there are two possibilities: (i) it cannot be removed by any rule, thus this case is analogous to the previous one; or (ii) it is removed by (Synchronized Parallelism 4) because the is the label of a branch of a parallelism operator. In this case, the control remains the same as in the standard semantics, and hence, no additional non-determinism appears. After (Synchronized Parallelism 5) has been executed, we have all possible applicable rules in the stack S, and S0remains unchanged. Then, the semantics executes the first rule, deletes it from S, and adds it to S0. Therefore, the same mechanism used for choices is valid for parallelisms, and thus all branches of choices and parallelisms are explored. Now, we have to prove that any possible (non-deterministic) derivation of MAIN with the standard semantics is also performed by the instrumented semantics as defined by Algorithm 1. We proof this lemma by induction on the length of the derivation D. In the base case, the initial state for the instrumented semantics induced by Algorithm 1 is in all cases (MAIN(MAIN,0), G, •,(S, ∅),∅,∅) where S=∅in the first execution and S6=∅in the other executions. Therefore, both semantics can only perform (Process Call) with an event τ. Hence, in the base case, both derivations are equivalent. We assume as the induction hypothesis, that both derivations 24 M. Llorens et al. are equivalent after nsteps of the standard semantics, and we prove that they are also equivalent in the step n+ 1. The most interesting cases are those in which the event is an external event. All possibilities are the following: –(STOP) In this case, both derivations finish the computation. The instrumented semantics performs one step more with the application of rule (STOP) (see the first item in the previous description). –(Process Call) and (Prefixing) In these cases, both derivations apply the same rule and the control is the same in both cases. –(Internal Choice 1 and 2) In these cases, the control becomes the left (resp. right) branch. They are analogous to the (Choice) rule of the instrumented semantics because both branches will be explored in different derivations as proved before. –(External Choice 1,2,3 and 4) With (External Choice 1 and 2) only τevents can be performed several times to evolve the branches of the choice. In every step the final control has the same specification position of the choice operator. Finally, one step is applied with (External Choice 3 or 4). Then, the set of rewriting steps performed with external choice are of the form: P0 τ −→ P1 (P0Q)τ −→ (P1Q)... Pn e −→ Pn+1 (PnQ)e −→ Pn+1 We can assume that (External Choice 1) is applied several times and finally (External Choice 3). This assumption is valid because (External Choice 2) is completely analogous to (External Choice 1);(External Choice 3) is completely analogous to (External Choice 4); and all combinations are going to be executed by the semantics as proved before. Then, we have an equivalent set of rewriting steps with the instrumented semantics: (P0Q)τ −→ P0 ,P0 τ −→ P1 ...Pn τ −→ Pn+1 Clearly, in both sequences, the specification positions of the control are the same. –(Synchronized Parallelism 1 and 2) Both rules can be applied interwound in the standard semantics. As it has been already demonstrated, we know that the same combination of rules will be applied by the instrumented semantics according to the algorithm use of the stack. The only difference is that the instrumented semantics performs an additional step with (Synchronized Parallelism 5), but this rule keeps the parallelism operator in the control; thus the specification position is the same and the claim holds. –(Synchronized Parallelism 3) If this rule is applied in the standard semantics, in the instrumented semantics we apply (Synchronized Parallelism 5) and then (Synchronized Parallelism 3). The specification positions of the control do not change. Lemma 2. Let Sbe a CSP specification, and D=s0 Θ0 ...Θn sn+1 a derivation of Sperformed with the instrumented semantics. Then, for each rewriting step A Semantics to Generate the CSCFG 25 si Θi si+1,0≤i < n, with si= (Pα, G, m, (S, S0), ∆, ζ), and si+1 = (Q, G0, n, (S0, S0 0), ∆0, ζ0); we have that nm 7→ α∈G0. Proof. The lemma trivially holds for all rules of the semantics. The only interesting case is synchronized parallelism. In the case of (Synchronized Parallelism 1, 2 and 3), function InitBranch inserts nm 7→ αinto G0, the first time it is evaluated. In the case of (Synchronized Parallelism 4), function LoopCheck returns another synchronized parallelism or a only if one of the processes has been marked as a loop. This only happens if a process call has been unfolded; and in turn, this only happens if (Synchronized Parallelism 1, 2 or 3) has been performed. The other possibility is that function LoopCheck returns a ⊥. In this case, ⊥cannot be further unfolded because no rule is applicable. Then, it must be the control of the state sn+1 and hence it is not required that nm 7→ α∈G0. Finally, (Synchronized Parallelism 5) starts a subderivation with a parallelism operator in the control and a non-empty stack. Therefore, another of the previous rules must be applied after it, and thus, the claim follows. Lemma 3. Let Sbe a CSP specification, and G= (N, Ec, El, Es)the graph produced for Sby Algorithm 1. Then, for each two nodes n, n0∈N,(n7→ n0)∈ Eciff the control can pass from l(n)to l(n0)and 6 ∃n00.(n7→ n00)∈Ecand (n00 7→ n0)∈Ec. Proof. The fact that 6∃n00. (n7→ n00)∈Ecand (n00 7→ n0)∈Ecimplies that the control can pass from nto n0directly, i.e., without a transitive relation. This condition is needed because the CSCFG only contains control-flow edges between those nodes where the control can pass from one to the other directly. Moreover, all the arcs in Ecare added to Gby the instrumented semantics. Therefore, we only have to prove that in every derivation Dof the semantics, for every new arc (n7→ n0) added to Ec, the control can pass from l(n) to l(n0). We prove this lemma by induction on the length of the derivation D. The base case starts with the initial state (MAIN(MAIN,0),∅,•,(∅,∅),∅,∅). Therefore the only rule applicable is (Process Call). This case is trivial because in the new arc nm 7→ α, l(m) = (MAIN,0) and l(n) = (MAIN, Λ). Hence, by item (i) of Definition 2 we have that the control can pass from l(m) to l(n). We assume as the induction hypothesis that the lemma holds in the ifirst rewriting steps of D, and we prove that it also holds in the step i+1. In the rewriting step i+1, one of the following rules must be applied: –(Process Call) This case is analogous to the base case, because in the new added arc nm 7→ α,mmust be the name of a process N, and n= (N,Λ). Therefore, by item (i) of Definition 2 we have that the control can pass from l(m) to l(n). –(Prefixing) Two new arcs are added to G.nm 7→ αand on 7→ β. Trivially, the control can pass from l(n) to l(o) by item (iii) of Definition 2. Moreover, by Lemma 2 we have that a node with the specification position of Pand parent owill be added to Gin the next rewriting step. Therefore, the control can pass from l(o) to Pos(P) by item (iv) of Definition 2. 32 M. Llorens et al. 2. Butler, M., Leuschel, M.: Combining CSP and B for Specification and Property Verification. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 221–236. Springer, Heildeberg (2005) 3. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Upper Saddle River, NJ, USA (1985) 4. Kavi, K.M., Sheldon, F.T., Shirazi, B., Hurson, A.R.: Reliability Analysis of CSP Specifications using Petri Nets and Markov Processes. In: 28th Annual Hawaii Int’l Conf. on System Sciences (HICSS’95), vol. 2 (Software Technology), pp. 516–524. IEEE Computer Society, Washington, DC, USA (1995) 5. Ladkin, P., Simons, B.: Static Deadlock Analysis for CSP-Type Communications. Responsive Computer Systems (Chapter 5), Kluwer Academic Publishers (1995) 6. Leuschel, M., Butler, M.: ProB: an Automated Analysis Toolset for the B Method. Journal of Software Tools for Technology Transfer. 10(2), 185–203 (2008) 7. Leuschel, M., Llorens, M., Oliver, J., Silva, J., Tamarit, S.: Static Slicing of CSP Specifications. In: Hanus, M. (ed.) 18th Int’l Symp. on Logic-Based Program Synthesis and Transformation (LOPSTR’08), pp. 141–150. Technical report, DSIC-II/09/08, Universidad Polit´ecnica de Valencia (July 2008) 8. Leuschel, M., Llorens, M., Oliver, J., Silva, J., Tamarit, S.: SOC: a Slicer for CSP Specifications. In: Puebla, G., Vidal, G. (eds.) 2009 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation (PEPM’09), pp. 165–168. ACM, New York, NY, USA (2009) 9. Leuschel, M., Llorens, M., Oliver, J., Silva, J., Tamarit, S.: The MEB and CEB Static Analysis for CSP Specifications. In: Hanus, M. (ed.) LOPSTR 2008, Revised Selected Papers. LNCS, vol. 5438, pp. 103–118. Springer, Heildeberg (2009) 10. Llorens, M., Oliver, J., Silva, J., Tamarit, S.: Transforming Communicating Sequential Processes to Petri Nets. In: Topping, B.H.V., Adam, J.M., Pallar´es, F.J., Bru, R., Romero, M.L. (eds.) Seventh Int’l Conf. on Engineering Computational Technology (ICECT’10). Civil-Comp Press, Stirlingshire, Scotland (to appear 2010) 11. Roscoe, A.W., Gardiner, P.H.B., Goldsmith, M., Hulance, J.R., Jackson, D.M., Scattergood, J.B.: Hierarchical Compression for Model-Checking CSP or How to Check 1020 Dining Philosophers for Deadlock. In: Brinksma, E., Cleaveland, R., Larsen, K.G., Margaria, T., Steffen, B. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 133–152. Springer, London (1995) 12. Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall, Upper Saddle River, NJ, USA (2005)