Hubert Garavel

Gwen Salaün

Wendelin Serwe
email: wendelin.serwe@inria.fr

On the Semantics of Communicating Hardware Processes and their Translation into LOTOS for the Verification of Asynchronous Circuits with CADP

Keywords: Asynchronous circuit, asynchronous logic, asynchrony, Chp, formal method, Gals architecture, handshake protocol, hardware architecture, hardware design, Lotos, modelling, network on chip, process calculus, specification, structured operational semantics, translation, validation, verification nil deadlock 1 | skip null action n ; T n ] guarded commands T ::= break | loop terminations

Hardware process calculi, such as Chp (Communicating Hardware Processes), Balsa, or Haste (formerly Tangram), are a natural approach for the description of asynchronous hardware architectures. These calculi are extensions of standard process calculi with particular synchronisation features implemented using handshake protocols. In this article, we first give a structural operational semantics for value-passing Chp. Compared to the existing semantics of Chp defined by translation into Petri nets, our semantics is general enough to handle value-passing Chp with communication channels open to the environment, and is also independent of any particular (2-or 4-phase) handshake protocol used for circuit implementation. We then describe the translation of Chp into the process calculus Lotos (ISO standard 8807), in order to allow asynchronous hardware architectures expressed in Chp to be verified using the Cadp verification toolbox for Lotos. A translator from Chp to Lotos has been implemented and successfully used for the compositional verification of two industrial case studies, namely an asynchronous implementation of the Des (Data Encryption Standard ) and an asynchronous interconnect of a NoC (Network on Chip).

Introduction

In the currently predominating synchronous approach to hardware design, a global clock is used to synchronise all parts of a circuit. Unfortunately, the global clock requires significant chip space and power. Asynchronous architectures [START_REF] Hauck | Asynchronous design methodologies: An overview[END_REF] attempt at avoiding the issues arising from a global clock. There are two main kinds of asynchronous architectures: -Gals (Globally Asynchronous, Locally Synchronous) architectures replace the global clock with several local clocks, by splitting a design into asynchronous parts, each with a synchronous clock domain, and -asynchronous circuits totally remove the notion of clock.

In these architectures, the different parts of a circuit evolve concurrently at different speeds, with no constraints on communication delays. Such asynchronous designs reduce power consumption, enhance modularity, and increase performance [START_REF] Van Berkel | Scanning the technology: Applications of asynchronous circuits[END_REF]. However, they raise problems that do not exist in the synchronous approach, e.g. proving the absence of deadlocks in a circuit. Also, there is no widely established asynchronous design methodology with mature tool support available up to now.

To master the design of asynchronous circuits, adequate description languages are necessary. For this purpose, several process calculi (or process algebras) dedicated to the description of asynchronous hardware have been proposed, such as Chp (Communicating Hardware Processes) [START_REF] Martin | Compiling communicating processes into delay-insensitive VLSI circuits[END_REF], Balsa [START_REF] Edwards | Balsa: An asynchronous hardware synthesis language[END_REF], and Haste [START_REF] Peeters | Haste Manual, Version 3.0[END_REF] (formerly Tangram [START_REF] Kessels | The Tangram framework (embedded tutorial): Asynchronous circuits for low power[END_REF]). These hardware process calculi are based on similar principles as standard process calculi [START_REF]Handbook of Process Algebra[END_REF][START_REF] Fokkink | Introduction to Process Algebra[END_REF] such as Acp, Ccs, Csp, Lotos, µCrl, etc. Especially, they provide operators such as nondeterministic choice, sequential, and parallel composition. However, compared to standard process calculi, they offer extensions to express the low-level aspects of hardware communications, such as the implementation of synchronisation by handshake protocols. In particular, communication in Chp, Balsa, or Haste is not necessarily atomic as it is in standard process calculi, and may combine message-passing with shared memory communication. For instance, the probe operation [START_REF] Martin | The probe: An addition to communication primitives[END_REF] of Chp allows to check whether the communication partner is ready for a communication or not, but without performing the communication actually. Chp, Balsa, and Haste are supported by synthesis tools that can generate the implementation of a circuit from its process algebraic description. For instance, the Tast tool [START_REF] Renaudin | TAST Compiler and TAST CHP Language[END_REF] can generate netlists from Chp descriptions.

In this article, we focus on Chp, which is used in the geographical area of the authors by major actors, such as STMicroelectronics, France Telecom R&D, and the Cea/Leti laboratory. Although there exist synthesis tools for Chp, the verification of Chp descriptions still lacks tool support. Continuing previous work [START_REF] Borrione | Validation of asynchronous circuit specifications using IF/CADP[END_REF] towards verification of Chp, our goal is to enable the application of the Cadp toolbox [START_REF] Garavel | CADP 2006: A toolbox for the construction and analysis of distributed processes[END_REF] developed for standard process calculi, such as the international standard Lotos [START_REF] Iso/Iec | LOTOS -a formal description technique based on the temporal ordering of observational behaviour, International Standard 8807[END_REF], to the particular case of Chp. Therefore, we study the translation from Chp to Lotos, and consequently the formal semantics of Chp.

So far, the semantics of Chp has only been partially formalised by a translation into Petri nets; this formalisation was based on a subset of Chp supporting only pure synchronisation and closed systems [START_REF] Renaudin | From hardware processes to asynchronous circuits via Petri nets: an application to arbiter design[END_REF]. A formal semantics for full Chp is mandatory to ensure a safe development and verification of Chp designs. In this article, we address this problem by giving a formal Sos (Structural Operational Semantics) [7, chapter 3] semantics for value-passing Chp with communication channels open to the environment.

We present in a second step a translation algorithm from full Chp into Lotos. This algorithm is based on a structural induction on the Chp description. To minimise the state space corresponding to the generated Lotos code, our translation implements an optimisation based on code specialisation. This optimisation technique avoids as much as possible the generation of Lotos gates and processes by distinguishing several translation strategies for Chp channels depending on the use of probes in the Chp specification. A Chp to Lotos translator has been implemented and successfully used for the compositional verification of two industrial case studies.

The remainder of the article is organised as follows. Section 2 presents the main features of the Chp hardware process algebra, putting emphasis on the probe operation, an original feature of Chp. Section 3 defines an Sos semantics for Chp. Section 4 presents translation rules from Chp into Lotos. Section 5 briefly describes the Chp to Lotos translator implementing these translation rules, and reports about its application to two industrial case studies, namely an asynchronous implementation of the Des (Data Encryption Standard ) [START_REF]Data encryption standard (DES), Federal Information Processing Standards FIPS[END_REF] and an asynchronous communication interconnect of a NoC (Network on Chip) [START_REF] Beigné | An asynchronous NoC architecture providing low latency service and its multi-level design framework[END_REF]. Finally, Section 6 compares our approach with related work, and Section 7 gives some concluding remarks.

Main Features of CHP

In this section, we focus on the behavioural part of Chp [START_REF] Renaudin | TAST Compiler and TAST CHP Language[END_REF], and omit additional structures, such as modules and component libraries, which are intended to designers convenience but have no impact on the operational semantics. We do not detail the low-level aspects of concrete syntax, but present a high-level view of Chp, focusing on abstract syntax and semantics features.

The precise semantics of these constructs will be explained in Section 3. Most of them have a meaning as is usual in process calculi. Here we only elaborate on the non-standard constructs.

Informal Semantics of Parallel Composition in CHP

The collateral composition "," and the parallel composition of processes " ", which is used at the top level in " B0 • • • Bn ", correspond to two different notions of concurrency. The collateral composition "," specifies concurrent execution without any communication, whereas the parallel composition " " specifies concurrent execution with handshake communications between processes. In a process "B 1 ,B 2 ", if B 1 modifies a variable x, B 2 must neither access the value of x nor modify x, and the sets of channels used by B 1 and B 2 must be disjoint (which also prohibits two interleaved emissions or receptions on a same channel). In B1 B2 , there are also no shared variables between B1 and B2 .

Informal Semantics of Guarded Choice in CHP

A guarded command "B = @[V 0 ⇒ B 0 ; T 0 . . . V n ⇒ B n ; T n ]" expresses the choice between the behaviours B 0 , ..., B n . A B i can only be chosen if the boolean value V i , called guard, is valid. The "break" keyword indicates that the execution of B terminates; the "loop" keyword indicates that B must be executed once more, thus allowing loops to be specified in Chp. The choice is internal, i.e. other concurrent behaviours do not have control nor influence on the choice. The version of Chp implemented in Tast [START_REF] Renaudin | TAST Compiler and TAST CHP Language[END_REF] also allows deterministic guarded commands which are a particular case of nondeterministic guarded commands with mutually exclusive guards; without loss of generality we consider only nondeterministic guarded commands in this article.

Informal Semantics of Handshake Communication in CHP

Communication between concurrent processes in Chp is implemented by means of hardware handshake protocols. As mentioned in [START_REF] Renaudin | From hardware processes to asynchronous circuits via Petri nets: an application to arbiter design[END_REF], there exists several implementation protocols, such as the 2-phase protocol (based on transition signalling) and the 4-phase protocol (based on level signalling). Depending on the chosen protocol, each Chp channel c will be implemented physically as a set of wires x c needed to carry data transmitted on c, and two control wires c req and c gr implementing an access protocol to x c . Common to both protocols is that a communication on a channel c is initiated by the process active for c, which has to wait until the communication is completed by the passive process.

The 2-phase protocol for communication on a channel c between two processes B 1 (active) and B 2 (passive) consists of the following two phases:

(i) Initiation: B 1 sends a request to B 2 by performing an electrical transition ("zero-to-one" or "one-tozero") on c req . (ii) Completion: B 2 sends an acknowledgement (or grant ) to B 1 by performing an electrical transition on c gr ; the emitted value is assigned to the variable of the receiver using the wires x c . A 4-phase protocol consists of the following four phases:

(i) Initiation: electrical transition "zero-to-one" on c req (ii) Completion: electrical transition "zero-to-one" on c gr (iii) "one-to-zero" for c req (iv) "one-to-zero" for c gr

Informal Semantics of the Probe Operation in CHP

The probe operation of Chp was introduced in [START_REF] Martin | The probe: An addition to communication primitives[END_REF] and was found to be useful in the design of asynchronous hardware. The notation "c #" allows a passive process (either the emitter or the receiver) to check whether its active partner has already initiated a communication on c. The notation "c #V ", which can only be used

c c 1 c 2 client-2 client-1

arbiter

Fig. 1. Architecture of the asynchronous arbiter by a receiver, checks whether the emitter has initiated the emission of the particular value V . Thus, the probe allows a process to query information about the current internal state (i.e. whether the communication has been initiated or not) of a concurrent process without completing the communication actually.

The probe operation allows to express external choice in Chp: this can be done by including in the guards appropriate probe operations to guarantee that the chosen branch can be executed. The arbiter examples given in Section 2.6 illustrate this use of the probe operation. The probe operation also allows to implement multiple reads, by executing "c #V " several times, which avoids the hardware cost of an additional variable to store V .

Similar operators are also present in other hardware process calculi. For instance, Haste [START_REF] Peeters | Haste Manual, Version 3.0[END_REF] provides a "probe(c)" operation that can be used only in guards and is similar to "c #" in Chp. Balsa provides a particular form of reception, called input enclosure [START_REF] Edwards | Balsa: An asynchronous hardware synthesis language[END_REF], which allows the receiver to perform several commands before acknowledging the reception, whereas the emitter witnesses an atomic communication. Hence, in hardware process calculi, a rendezvous communication might be decomposed into different steps, corresponding to the handshake protocol used for implementing the rendezvous.

Notice that the abstract syntax allows to use the probe operator " #" in any expression, thus also in emissions and assignments. Although we are not aware of any application using behaviours such as "c 1 !c 2 #", we do not want to exclude them a priori, as they might be useful in some situations. For instance, the process "c!c #" transmits a boolean value to the active receiver, indicating whether the passive emitter is ready for the emission before (transmission of the value false) or after (transmission of the value true) the initialisation of the communication by the receiver.

Running Examples: Asynchronous Arbiters Without and With Priorities

Throughout this article we consider the example of an asynchronous arbiter presented in [START_REF] Renaudin | From hardware processes to asynchronous circuits via Petri nets: an application to arbiter design[END_REF], which we generalise in two ways: we use value-passing communications instead of pure synchronisations, and we model an arbiter open to its environment by keeping the shared resource outside of the arbiter itself.

Arbiters are commonplace in digital systems, whenever a restricted number of resources (such as memories, ports, buses, etc.) have to be allocated to different client processes. Figure 1 depicts the situation in which two clients compete for accessing a common resource. Each client transmits a request for the resource to the arbiter via an individual channel (c 1 or c 2 ). A third channel c allows the arbiter to emit the number of the selected client (1 or 2) to the environment, i.e. the resource. The arbiter chooses nondeterministically between the clients with pending requests. The corresponding Chp description is

{c, c 1 , c 2 }, {}, client-1 client-2 arbiter
where all three channels have an active emitter and a passive receiver, the set of variables is empty, and the three processes are described as follows:

  arbiter without priorities   client-1: @[true ⇒ c 1 !; loop] client-2: @[true ⇒ c 2 !; loop] arbiter: @[c 1 # ⇒ (c!1, c 1 ?); loop c 2 # ⇒ (c!2, c 2 ?); loop]
This example shows how the probe operation allows to model external choice. The arbiter uses probe operations to check whether a client has a pending request for the resource; since the arbiter selects a client only if a request for this client is pending, the clients can influence the choice made by the arbiter. Without the probe operations, the arbiter might select client-1 even if client-1 has no pending request; in this case, any request of client-2 (even if pending) is granted only after waiting for and handling a request of client-1.

To illustrate the general case of probes used in expressions, we extend this arbiter in order to distinguish high and low priority requests. In this new system, the behaviour of both clients differs, since client-1 can emit requests with different priorities. In this case, a boolean parameter is sent along channel c 1 to indicate whether the request has a high (parameter set to true) or normal (parameter set to false) priority. Consequently, client-1 has precedence when submitting a priority request. The corresponding Chp description is

{c, c 1 , c 2 }, {x}, client-1 client-2 arbiter
where the boolean variable x -taking values in the set {true, false} -is local to the arbiter, and where the three processes are described as follows:

  arbiter with priorities   client-1: @[true ⇒ c 1 !true ; loop true ⇒ c 1 !false ; loop] client-2: @[true ⇒ c 2 !; loop] arbiter: @[c 1 # ⇒ (c!1, c 1 ?x); loop c 2 # and (not(c 1 #true)) ⇒ (c!2, c 2 ?); loop]
In this example, requests from client-1 can always be served, while the arbiter accepts requests from client-2 only if client-1 is not trying to access the resource with a high priority.

A Structural Operational Semantics for CHP

In this section, we propose an Sos semantics for Chp with value-passing communications. This semantics allows probe operations in any expression, extending a previous version [START_REF] Salaün | Translating hardware process algebras into standard process algebras -illustration with CHP and LOTOS[END_REF]Section 3], which allowed probe operations only in guards.

This semantics is defined without expanding communications according to a particular handshake protocol. This approach is general in the sense that it gives to any Chp description C, X , B0 • • • Bn a unique behavioural semantics by means of an Lts (Labelled Transition System). In this Lts, a state consists of two parts: data and behaviour. A transition corresponds either to an observable action (communication on a channel)2 or an internal action, noted τ . 3 As stated by the semantics of Chp given in [START_REF] Renaudin | From hardware processes to asynchronous circuits via Petri nets: an application to arbiter design[END_REF], internal actions are generated whenever a process assigns one of its local variables. Our definitions follow the usual interleaving semantics of process calculi, i.e. at every instant, at most one (observable or internal) action can take place.

We first present the notion of environment that gives the semantics of the data part of Chp. Then, we define the behavioural semantics of Chp in two steps, starting with the semantics of a single process Bi taken in isolation, followed by the semantics of a set of communicating processes " B0 • • • Bn ". Finally, we relate our semantics to the approach of [START_REF] Renaudin | From hardware processes to asynchronous circuits via Petri nets: an application to arbiter design[END_REF].

Environments

A key semantic difficulty in Chp is the treatment of the probe operation, since this operation exploits the fact that communication is not atomic at the lower level of implementation. Inspired by the actual hardware implementation of Chp, we associate to each channel c a shared variable noted x c that is modified only by the process active for c and might be read by the process passive for c. For a channel c with an active emitter, the type of x c is type(c). The active emitter assigns the emitted value to x c when initiating the communication, and resets x c (to the undefined value, noted "⊥") when completing the communication. A variable x c is equal to ⊥ iff all initiated communications on c have been completed. For a channel with an active receiver, the type of x c is the singleton {ready}, meaning that the active receiver has initiated the communication. Formally, we define the extended set of variables as X * = X ∪ {x c | c ∈ C}, and define X * i as the set of the local variables of Bi and all the variables x c such that channel c is used by Bi . Notice that the additional variables x c ensure, for each channel c with an active emitter, that a value sent by the active process on c can be read or probed as often as desired by the passive process before completion of the communication.

We define an environment E on X * as a partial mapping from X * to ground values (i.e. constants), and write environments as sets of associations "x → v" of a ground value v to a variable x. Environment updates are described by the operator ⊘, which is defined as follows:

(∀x ∈ X * ) E 1 ⊘ E 2 (x) = E 1 (x) if E 2 (x) = ⊥ E 2 (x) otherwise
The environment obtained by resetting a variable x to ⊥ in an environment E is defined by the function reset (E, x):

(∀x ′ ∈ X * ) reset (E, x) (x ′ ) = ⊥ if x ′ = x E(x ′ ) otherwise
The semantics of a value expression V is defined by an evaluation function eval (E, V ), which behaves as usual, but takes the probe operation into account. eval (E, V ) can be undefined, since Chp (contrary to Lotos) does not force all variables to be initialised. In the sequel, we suppose that all variables are properly initialised.

eval (E, x) = E(x) eval E, f (V 1 , . . . , V n ) = f eval (E, V 1 ), . . . , eval (E, V n ) eval (E, c #) = true ⇐⇒ E(x c ) = ⊥ eval (E, c #V ) = true ⇐⇒ E(x c ) = eval (E, V )

Behavioural Semantics for a Single Process

Our semantics associates to each process Bi an Lts S i , L i , -→ b , E i , Bi , where: -The set of states S i contains pairs E, B of a process B and an environment E on X * i . -The set of labels L i contains emissions, receptions, τ actions (representing internal transitions, such as assignments to local variables), and a particular label √ representing successful termination.

-The transition relation "-→ b " is defined below by Sos rules derived from those used for Bpa ε (Basic Process Algebra with empty process ε) in [7, chapter 3], extended with values and environments. As for Bpa ε , we write E, B √ as a shorthand notation for E, B √ -→ b E, nil . -The initial state is E i , Bi , where the initial environment E i assigns the undefined value ⊥ to all variables of X * i . This Lts is constructed using a function H that maps each channel to an element of the set {neutral, active, passive}; for each Bi , the actual value of H is the function H i defined in Section 2.1.

Rules for nil. There are no rules for nil because nil is in a deadlock state and cannot evolve.

Rules for skip. Similar to the empty process ε of Bpa ε , the process skip can always be executed and terminates successfully.

E, skip √

The difference between a deadlock and a process that terminates successfully is subtle. In both cases, no more transition is possible, but a successful termination is always preceded by an observable transition with special label √ . The same approach to distinguish deadlock states and terminating states using special transitions is also used in other process algebras, such as Bpa ε or Lotos.

Rules for Assignments. An assignment can always be executed and modifies the environment by updating the value of the variable to be assigned.

E, x:=V

τ -→ b E ⊘ {x → eval (E, V )}, skip
Rules for Emissions. A passive emission can always be executed.

H(c) = passive E, c!V c!eval(E,V ) --------→ b E, skip
An active emission on a channel c involves two successive transitions: the first (internal) one assigns a value to the shared variable x c , which is initially set to ⊥, and the second one completes the communication by resetting x c . This two step approach is general enough to represent 2-phase and 4-phase protocols.

H(c) = active eval (E, x c ) = ⊥ E, c!V τ -→ b E ⊘ {x c → eval (E, V )}, c!V H(c) = active eval (E, x c ) = ⊥ E, c!V c!eval(E,V ) --------→ b reset (E, x c ), skip
Rules for Receptions. These rules are dual of those for emissions.

H(c) = passive E, c?x c?eval(E,xc) --------→ b E ⊘ {x → eval (E, x c )}, skip H(c) = active eval (E, x c ) = ⊥ E, c?x τ -→ b E ⊘ {x c → ready}, c?x H(c) = active eval (E, x c ) = ⊥ V ∈ type(c) E, c?x c?V ---→ b reset(E, x c ) ⊘ {x → V }, skip
Contrary to the first rule, which uses the value of x c as the received value, the third rule enumerates all possible ground values V that might be received on channel c.

Rules for Sequential Composition. The first rule applies as long as behaviour B 1 has not terminated.

The second rule indicates that when B 1 can terminate successfully, the execution of B 2 starts.

L = √ E, B 1 L -→ b E ′ , B ′ 1 E, B 1 ;B 2 L -→ b E ′ , B ′ 1 ;B 2 E, B 1 √ E, B 2 L -→ b E ′ , B ′ 2 E, B 1 ;B 2 L -→ b E ′ , B ′ 2
Rules for Collateral Composition. The two first rules correspond to the independent evolution of behaviours B 1 and B 2 , respectively. The third rule expresses that when both behaviours terminate, the collateral composition terminates successfully.

L = √ E, B 1 L -→ b E ′ , B ′ 1 E, B 1 ,B 2 L -→ b E ′ , B ′ 1 ,B 2 L = √ E, B 2 L -→ b E ′ , B ′ 2 E, B 1 ,B 2 L -→ b E ′ , B 1 ,B ′ 2 E, B 1 √ E, B 2 √ E, B 1 ,B 2 √
Rules for Guarded Commands. The rules for guarded commands express that a branch whose guard is true can be selected. As in [START_REF] Renaudin | From hardware processes to asynchronous circuits via Petri nets: an application to arbiter design[END_REF], the selection of a branch is modelled by an internal transition, reflecting that choice is internal in Chp. If the chosen branch ends with "break", the guarded command terminates when the branch terminates. If it ends with "loop" the guarded command will be restarted once more after executing the branch.

(∃i ∈ {1, . . . , n}) eval (E, V i ) = true T i = break E, @[V 0 ⇒ B 0 ; T 0 . . . V n ⇒ B n ; T n ] τ -→ b E, B i (∃i ∈ {1, . . . , n}) eval (E, V i ) = true T i = loop E, @[V 0 ⇒ B 0 ; T 0 . . . V n ⇒ B n ; T n ] τ -→ b E ′ , B i ; @[V 0 ⇒ B 0 ; T 0 . . . V n ⇒ B n ; T n ]

Semantics for Communicating Processes

The semantics of a Chp description C, X , B0 • • • Bn is defined by the parallel composition of the (n + 1) "local" Ltss S i , L i , -→ b , E i , Bi produced from the individual processes Bi and the corresponding functions H i according to the rules of Section 3.2. Formally, this composition is a "global" Lts S, L, -→, E 0 , B0 , . . . , Bn , where: -The set of states S contains tuples E, B 0 , . . . , B n consisting of (n + 1) processes B 0 , . . . , B n and a global environment E on X * = n i=0 X * i . E is the union of the local environments E i on X * i of the processes Bi . The sets X * i are disjoint for the sets X i (local variables of Bi ), but for each binary channel c connecting Bi and Bj (i = j), the variable x c occurs in X * i and X * j ; this is not a problem, since x c is only modified by the process active for c.

-The set of labels L is the union of the sets of labels L i minus those labels that correspond to receptions on binary channels. We represent synchronised communications (i.e. an emission and a reception) using the same symbol "!" as for emissions (following the convention used in the Lts generated from Lotos using Cadp [START_REF] Garavel | CADP 2006: A toolbox for the construction and analysis of distributed processes[END_REF]). -The transition relation "-→" is defined by the three Sos rules Internal, Com, and Env below.

-The initial state is E 0 , B0 , . . . , Bn , where E 0 is the empty initial environment, i.e. (∀x ∈ X * ) E 0 (x) = ⊥. Let internal (L) be the predicate that is true iff L is either a τ or corresponds to a communication on a port (i.e. a unary channel open to the environment):

(∀L ∈ L) internal (L) ⇐⇒ L = τ ∨ (∃c ∈ C) (∃V ∈ V) (L = c!V ∨ L = c?V ) ∧ port (c)
The first Sos rule describes the evolution of the i-th process B i independently of the others. It models either an assignment to a variable, or the communication on a port c that is open to the environment and does not need to be synchronised with another process B j (i = j).

(∃i ∈ {0, . . . , n}) E, B i L -→ b E ′ , B ′ i internal (L) E, B 0 , . . . , B i , . . . , B n L -→ E ′ , B 0 , . . . , B ′ i , . . . , B n (Internal)
The next rule describes the communication between an emitter process B i and a receiver process B j exchanging values over channel c.

(∃i ∈ {0, . . . , n}) E, B i c!V --→ b E ′ , B ′ i (∃j ∈ {0, . . . , n}) E, B j c?V ---→ b E ′′ , B ′ j E, B 0 , . . . , B i , . . . , B j , . . . , B n c!V --→ reset (E ′′ , x c ), B 0 , . . . , B ′ i , . . . , B ′ j , . . . , B n (Com)
Note that i and j in rule (Com) are different and uniquely defined, since communications are binary (one emitter and one receiver for each channel). Note also that, if E ′ and E differ in rule (Com), the only possible modification (resetting x c ) is applied to E ′′ in the right hand side of the conclusion of rule (Com). The rules presented so far are sufficient to define the semantics of (closed) systems without passive ports, i.e. unary channels for which no process Bi is active. The following rule completes the semantics by modelling the environment as an active process that communicates with each passive port c:

(∃i ∈ {0, . . . , n}) H i (c) = passive (∀j ∈ {0, . . . , n}) ¬H j (c) = active eval (E, x c ) = ⊥ V ∈ type(x c ) E, B 0 , . . . , B n τ -→ E ⊘ {x c → V }, B 0 , . . . , B n
(Env) This rule is similar to those defining the semantics of asynchronous processes communicating via shared memory, as for instance concurrent constraint programming [START_REF] De Boer | A fully abstract model for concurrent constraint programming[END_REF] or concurrent declarative programming [START_REF] Serwe | On concurrent functional-logic programming[END_REF]Table 5.3,page 142]. Example 1 This example shows the necessity of rule (Env). Consider the following two processes B 1 and B 2 , which are derived from the arbiter of Section 2.6: Here, c 1 and c 2 are passive ports open to the environment. Without rule (Env), both B 1 and B 2 would be equivalent to the deadlock process nil. Thus, one would expect that in the behaviour "B 1 client-2", B 1 could be replaced by B 2 without modifying the semantics. However, "B 1 client-2" is equivalent to nil, but "B 2 client-2" is not -the corresponding Lts is shown in Figure 2. Rule (Env) solves this issue by giving a different semantics to B 1 and B 2 .

B 1 = @[c 1 # ⇒ (c!1, c 1 ?); loop] B 2 = @[c 2 # ⇒ (c!2, c 2 ?); loop] τ c!2 c 2 !2 c 2 !2 τ c!2 τ c!2 τ τ τ c 2 !2 τ Fig. 2. Lts for "B 2 client-2" of Example 1 c 1 !true c!1 c 2 c!2 c 1 !false c!1 c!1 c 1 !true c!2 c 1 !false c!1 c 2 c 2 c!2 c!2 c!2 c 2 c 2 c!2
Example 2 For the arbiter with priorities of Section 2.6, the Lts generated according to the operational semantics has 51 states and 112 transitions. After minimisation with respect to branching bisimulation [START_REF] Van Glabbeek | Branching-time and abstraction in bisimulation semantics[END_REF], the resulting Lts (Figure 3) has 18 states, 34 transitions, and 6 different labels corresponding to internal τ actions and communications on channels c, c 1 , and c 2 .

Comparison with the Existing Petri Net Translation

So far, the only existing semantics for Chp proceeds by a translation of Chp into Petri nets [START_REF] Renaudin | From hardware processes to asynchronous circuits via Petri nets: an application to arbiter design[END_REF]. This formalisation only handles a subset of Chp that, compared to full Chp presented in Section 2, is restricted in two ways: it allows only pure synchronisations (instead of value-passing communications), allows probe operations only in guards, and forbids ports open to the environment. By handling full Chp, our semantics client 1

arbiter client 2 c 1 # c 2 # c 1s c 1R2 c 1R1 c 1req c 1 c 1 ! c 1gr c 1 ? c 2 ? x:=2 c 2gr c 2req c 2R2 c 2s c 2R1 c 2 c 2 !
x:=1 allows to describe circuits with inputs and outputs properly. In this section, our goal is not to compare formally our semantics with the Petri nets encoding, but to explain the principles of such a comparison, and point out the differences between both semantics. This section is split into three parts. First, we introduce the basics of the Petri net encoding. Second, we sketch how Ltss can be obtained from these Petri nets. Last, we stress differences between Ltss generated from both approaches.

Translation of CHP to Petri Nets. Similar to our Sos semantics, [START_REF] Renaudin | From hardware processes to asynchronous circuits via Petri nets: an application to arbiter design[END_REF] defines the translation of a Chp description C, X , B1 • • • Bn into Petri nets in two successive steps: -In a first step, the Petri nets corresponding to the processes Bi are constructed separately following the patterns sketched in [START_REF] Renaudin | From hardware processes to asynchronous circuits via Petri nets: an application to arbiter design[END_REF]. Petri net places may be labelled with assignments, emissions, and receptions. Petri net transitions may be labelled with the guards of Chp guarded commands. -In a second step, the separate Petri nets are merged into one global Petri net. To model synchronisation on channels, [START_REF] Renaudin | From hardware processes to asynchronous circuits via Petri nets: an application to arbiter design[END_REF] gives two different translations, depending on the handshake protocol (2-or 4-phase) used for the implementation. In both cases, channels are modelled by additional places and transitions that encode the chosen handshake protocol. Notice that for each channel c the places labelled "c!" and "c?" are kept separate, i.e. there is no transition merging (contrary to [START_REF] Garavel | Compilation and verification of LOTOS specifications[END_REF] for instance). Example 3 Consider an adaptation of the simple arbiter of Section 2.6 in order to meet the restrictions of [START_REF] Renaudin | From hardware processes to asynchronous circuits via Petri nets: an application to arbiter design[END_REF] (no ports open to the environment). The corresponding Chp description is {c 1 , c 2 }, {x}, client-1 client-2 arbiter , where channels c 1 and c 2 have an active emitter and a passive receiver, where variable x is local to the arbiter, and where the three processes are defined as follows:

client-1:

@[true ⇒ c 1 !; loop] client-2: @[true ⇒ c 2 !; loop] arbiter: @[c 1 #1 ⇒ x:=1; c 1 ?; loop c 2 #2 ⇒ x:=2; c 2 ?
; loop] The corresponding Petri net for a 4-phase protocol is shown in Figure 4. Places are represented by circles, and transitions by thick lines. Whenever a place is both an input and an output place of some transition, we use a double-headed arrow (as for places labelled c 1req , c 1gr , c 2req , and c 2gr ). The Petri nets corresponding to the three processes are framed in dotted boxes. The places modelling the channels c 1 and c 2 are framed in dashed boxes.

Deriving an LTS from a CHP Petri Net. As for ordinary Petri nets, a Petri net model of [START_REF] Renaudin | From hardware processes to asynchronous circuits via Petri nets: an application to arbiter design[END_REF] has tokens in the places; the Petri nets generated from Chp descriptions are one-safe, i.e. each place contains at most one token. A transition can be fired when all its input places contain a token and its guard (if any) is true; after firing, the input places lose their token and the output places get a token. The Petri nets of [START_REF] Renaudin | From hardware processes to asynchronous circuits via Petri nets: an application to arbiter design[END_REF] have also a different behaviour than ordinary Petri nets, to take into account the actions attached to places. For instance, if two places with action (e.g. "c 1 !" and "c 2 !" in Figure 4) have a token, then interleaved

a q q 1 q 2 becomes t 3 t 4 t 4 t 3 t 1 t 2 t 1 t 2 a Fig.

Duplication of Petri net places

transitions have to be created for these actions. From [START_REF] Renaudin | From hardware processes to asynchronous circuits via Petri nets: an application to arbiter design[END_REF] and following discussions with the first author of [START_REF] Renaudin | From hardware processes to asynchronous circuits via Petri nets: an application to arbiter design[END_REF], we conjecture that these Ltss can be obtained by the following two steps:

-First, the Petri net needs to be transformed into a (more standard) Petri net model, in which actions are attached to transitions. As shown in Figure 5, each place q labelled with an action a (i.e. emission, reception, or assignment) is replaced by two places q 1 and q 2 , linked with a new transition labelled with action a. Place q is replaced by q 1 (respectively q 2 ) in the sets of output (respectively input) places of all transitions arriving in (respectively, leaving) q. In the case a transition t has q both as an input and an output place (i.e. t is linked to q with a double-headed arrow such as t 1 in Figure 5), q is replaced by q 2 in the sets of input and output places of t. -Then, the Lts is obtained by applying to the modified Petri net a marking graph construction algorithm extended with the evaluation of expressions and guards. The transitions of this Lts are labelled with the emissions and receptions attached to Petri net transitions. If a Petri net transition is not labelled with an emission or a reception, the corresponding Lts transition is labelled with τ .

Comparison of both Approaches. We can try to compare the Lts Sos obtained by our Sos semantics and Lts PN obtained after translation of Chp into Petri nets according to [START_REF] Renaudin | From hardware processes to asynchronous circuits via Petri nets: an application to arbiter design[END_REF]. Given that [START_REF] Renaudin | From hardware processes to asynchronous circuits via Petri nets: an application to arbiter design[END_REF] does not deal with value-passing communications and open systems, comparison is only possible for closed systems with pure synchronisations. Comparison of Lts Sos and Lts PN is not immediate, for several reasons. First, the places and transitions added to the Petri nets for the communication channels introduce τtransitions in Lts PN that have no counterpart in Lts Sos ; thus, Lts Sos and Lts PN are not strongly equivalent 4 . Second, the sets of labels of Lts Sos and Lts PN are different: on the one hand, Lts PN contains both "c!" and "c?" as labels, since the places labelled "c!" and "c?" are kept separate in the Petri net model of [START_REF] Renaudin | From hardware processes to asynchronous circuits via Petri nets: an application to arbiter design[END_REF]; on the other hand, for closed systems Lts Sos does not contain labels of the form "c?"; thus, comparing Lts Sos and Lts PN would require to rename into τ all labels of Lts PN corresponding to communications by active processes, and to replace all remaining "?" by "!".

Principles of a Translation from CHP into LOTOS

In order to check the correctness of asynchronous circuit designs, our approach is to translate Chp into Lotos so that tools for Lotos (namely, the Cadp verification toolbox [START_REF] Garavel | CADP 2006: A toolbox for the construction and analysis of distributed processes[END_REF]) can be applied.

Overview of LOTOS

Lotos (Language Of Temporal Ordering Specification) is a specification language for distributed open systems, standardised by Iso [START_REF] Iso/Iec | LOTOS -a formal description technique based on the temporal ordering of observational behaviour, International Standard 8807[END_REF]. A Lotos specification is composed of two parts: a process part based on Ccs [START_REF] Milner | Communication and Concurrency[END_REF] and Csp [START_REF] Hoare | Communicating Sequential Processes[END_REF], and a data part based on the algebraic data type language ActOne [START_REF] Ehrig | Fundamentals of Algebraic Specification 1 -Equations and Initial Semantics[END_REF]. We present hereafter only the subset of Lotos needed for expressing Chp; the data part being straightforward, we focus on the process part. For a complete description of Lotos, we refer the reader to existing tutorials, such as [START_REF] Bolognesi | Introduction to the ISO specification language[END_REF].

The following grammar uses the same conventions as for Chp, i.e. lower case identifiers stand for terminals and upper case identifiers stand for non terminals; x is a variable, s a sort, f a function, and g a gate for rendezvous communication.

V ::= x | f (V 1 , . . . , V n ) value expression O ::= !V emission | ?x : s reception B ::= stop deadlock | exit successful termination | let x : s = V in B 0 variable definition | τ ; B 0 internal action | g O 1 . . . O n ; B 0 rendezvous on gate g with offers O 1 , ..., O n | B 1 >> accept x 0 : s 0 , . . . , x n : s n in B 2 sequential composition | [V ]-> B 0 guarded behaviour | B 1 [] B 2 nondeterministic choice | choice x 0 : s 0 , . . . , x n : s n [] B choice over values | B 1 |[g 1 , . . . , g n ]| B 2 parallel composition | B 1 ||| B 2 parallel interleaving | P [g 1 , . . . , g m ](V 1 , . . . , V n ) process call F ::= noexit | exit(s 1 , . . . , s n ) functionality
The behaviour of a process B in Lotos is described using rendezvous communications, sequential and parallel compositions, guarded behaviours, nondeterministic choices, choices over values, process calls, etc. -Sequential composition ";" in Chp is symmetric, whereas Lotos has two different operators for sequential composition: an asymmetric action prefix ";" and a symmetric sequential composition ">>". Variables assigned on the left hand side of a Chp ";" can be used on the right hand side, whereas variables assigned on the left hand side of a Lotos ">>" must be explicitly listed (in an "accept ... in" clause) to be used on the right hand side. Furthermore, ">>" creates an internal τ -transition, contrary to the ";" operators of both Chp and Lotos. There are two options when translating Chp to Lotos. A simple approach is to generate Lotos code containing only ">>", but this adds unnecessary τ -transitions in the corresponding Lts, thus contributing to state space explosion. A better approach is to generate ";" whenever possible and ">>" only when needed. In this article, we adopt the second approach, which produces better Lotos code (in the sense that the corresponding Lts has less states and transitions) at the expense of a more involved translation. -Chp has a neutral element (skip) for its sequential composition, whereas Lotos lacks neutral elements for both ";" (which is asymmetric) and ">>" (which creates a τ -transition). -Chp has a loop operator, whereas Lotos does not; thus, Chp loops must be translated into recursive Lotos processes. -Chp expressions may contain probes, i.e. accesses to shared variables x c , whereas Lotos forbids shared variables. As a consequence, the translation of the probe operation requires the generation of additional transitions modelling accesses to communication channels. -Evaluation of an expression V is an atomic operation in Chp, whereas Lotos requires a sequence of as many transitions as there are probe operations in V . To preserve atomicity, we will introduce a semaphorebased locking mechanism discussed in Section 4.5. The remainder of this section is organised as follows. First, we introduce data-flow analysis and other auxiliary definitions. Then, we present preliminary simplifications of Chp descriptions prior to the translation. The translation function c2l itself is defined in two steps: translation of a single Chp process and translation of several Chp processes composed in parallel. Then, we illustrate the translation on the arbiter example. Finally, we discuss the possible relations between our Lotos translation with the Sos semantics of Section 3; to prepare this discussion, we will enhance the definition of the translation function c2l with remarks about preservation of branching equivalence during the translation.

Rendez vous communications in

Auxiliary Definitions

Data-flow Analysis. We introduce the following data-flow sets inspired from [27, Section 3]. Let def (B) be the set of all variables modified (in assignments or receptions) in at least one branch of process B:

def (nil) = ∅ def (x:=V ) = {x} def (skip) = ∅ def (B 1 ;B 2 ) = def (B 1 ) ∪ def (B 2 ) def (c!V ) = ∅ def (B 1 ,B 2 ) = def (B 1 ) ∪ def (B 2 ) def (c?x) = {x} def (@[V 0 ⇒ B 0 ; T 0 . . . V n ⇒ B n ; T n ]) = n i=0 def (B i ) Let def n (B)
be the set of all variables modified in all branches of process B:

def n (nil) = ∅ def n (x:=V ) = {x} def n (skip) = ∅ def n (B 1 ;B 2 ) = def n (B 1 ) ∪ def n (B 2 ) def n (c!V ) = ∅ def n (B 1 ,B 2 ) = def n (B 1 ) ∪ def n (B 2 ) def n (c?x) = {x} def n (@[V 0 ⇒ B 0 ; T 0 . . . V n ⇒ B n ; T n ]) = n i=0 def n (B i ) We have def (B) = def n (B)
for any behaviour B that does not contain a choice, i.e. a guarded command with more than one branch.

Let use v (V ) be the set of all variables read in value expression V :

use v (x) = {x} use v (c #) = ∅ use v f (V 1 , . . . , V n ) = n i=1 use v (V i ) use v (c #V ) = use v (V )
Let use(B) be the set of all variables used (in expressions of assignments, emissions, or guards) in a process B before any modification of these variables in B:

use(nil) = ∅ use(x:=V ) = use v (V ) use(skip) = ∅ use(B 1 ;B 2 ) = use(B 1 ) ∪ use(B 2 ) \ def n (B 1 ) use(c!V ) = use v (V ) use(B 1 ,B 2 ) = use(B 1 ) ∪ use(B 2 ) use(c?x) = ∅ use(@[V 0 ⇒ B 0 ; T 0 . . . V n ⇒ B n ; T n ]) = n i=0 use v (V i ) ∪ use(B i )
Functionalities. The Lotos functionality corresponding to a Chp process B is given by the function func(B, D, U ), where D and U are two sets (in fact, alphabetically ordered lists) of variables, specifying the context in which B is executed, precisely, the set of variables defined before B is executed, and used after B is executed, respectively.

func(nil, D, U ) = noexit func(skip, D, U ) = exit(D ∩ U ) func(c!V, D, U ) = exit(D ∩ U ) func(c?x, D, U ) = exit (D ∪ {x}) ∩ U func(x:=V, D, U ) = exit (D ∪ {x}) ∩ U func(B 1 ;B 2 , D, U ) = noexit if func(B 1 , D, U ) = noexit ∨ func(B 2 , D, U ) = noexit exit (D ∪ def (B 1 ) ∪ def (B 2 )) ∩ U otherwise func(B 1 ,B 2 , D, U ) = noexit if func(B 1 , D, U ) = noexit ∨ func(B 2 , D, U ) = noexit exit (D ∪ def (B 1 ) ∪ def (B 2 )) ∩ U otherwise func(@[V 0 ⇒ B 0 ; T 0 . . . V n ⇒ B n ; T n ], D, U ) = noexit if (∀i ∈ {0, . . . , n}) (func(B i , D, U ) = noexit ∨ T i = loop) exit D ∪ n i=0 def (B i ) ∩ U otherwise Let inf (B) be the predicate that is true iff func(B, ∅, ∅) = noexit.
Channels. Let chan v (V ) be the set of channels occurring in value expression V ; by definition, these channels are probed in V :

chan v (x) = ∅ chan v f (V 1 , . . . , V n ) = n i=1 chan v (V i ) chan v (c #) = {c} chan v (c #V ) = {c} ∪ chan v (V )
Let chan(B) be the set of channels occurring in behaviour B:

chan(nil) = ∅ chan(x:=V ) = chan v (V ) chan(skip) = ∅ chan(B 1 ;B 2 ) = chan(B 1 ) ∪ chan(B 2 ) chan(c!V ) = {c} ∪ chan v (V ) chan(B 1 ,B 2 ) = chan(B 1 ) ∪ chan(B 2 ) chan(c?x) = {c} chan(@[V 0 ⇒ B 0 ; T 0 . . . V n ⇒ B n ; T n ]) = n i=0 chan v (V i ) ∪ chan(B i )
Channel Profiles. In order to minimise the state space corresponding to the generated Lotos code, the translation of a channel c and of the communications on c depends on the profile of c, i.e. whether and how c is probed by the passive process for c. The profile of a channel c can take one out of three enumerated values:

unprobed : the channel c is never probed, single: any probe operation on c appears as a guard, e.g. "c 1 # ⇒ . . ." (as in the simple arbiter without priorities), and general : a probe on c is used in an expression, e.g. "c 2 # and (not(c 1 #true)) ⇒ . . ." (as in the arbiter with priorities, where both channels c 1 and c 2 have profile "general "). We define an order unprobed < single < general (the smaller the value, the more "efficient" the generated Lotos will be). We note "max(x, y)" the maximal element of the two profiles x and y;

Channel profiles for a Chp description are computed statically as defined below. Let a profile environment be a partial function mapping channels to their profiles; as for environments (see Section 3.1), we write profile environments as sets of associations c → {unprobed, single, general }, where c is a channel. We define

(∀c ∈ C) (E 1 ⊎ E 2 )(c) =      E 1 (c) if E 2 (c) is undefined E 2 (c) if E 1 (c) is undefined max E 1 (c), E 2 (c) otherwise
Let profile v (V ) be the partial function associating the "general " profile to each channel probed in the value expression V :

profile v (V ) = c → general | c ∈ chan v (V )
The boolean expressions occurring as guards in the "@[...]" operator need to handled differently from "ordinary" expressions. Indeed, if the outermost operation of a guard V is a probe on channel c, and V does not contain any other occurrence of a probe operation, the profile of c is "single". Let profile g (V ) be the partial function computing profile environments for those channels occurring in guard V :

profile g (x) = ∅ profile g f (V 1 , . . . , V n ) = profile v f (V 1 , . . . , V n ) profile g (c #) = {c → single} profile g (c #V ) = {c → single} if profile v (V ) = ∅ {c ′ → general | c ′ = c ∨ c ′ ∈ chan v (V )} otherwise
Let profile b (B, H) be the partial function computing profiles for channels occurring in the behaviour B, where parameter H is a partial function mapping channels to the set {neutral, active, passive} (see Section 2.1). Function profile b is defined as follows:

profile b (nil, H) = ∅ profile b (skip, H) = ∅ profile b (c!V, H) = {c → unprobed } ⊎ profile v (V ) if H(c) = passive profile v (V ) otherwise profile b (c?x, H) = {c → unprobed} if H(c) = passive ∅ otherwise profile b (x:=V, H) = profile v (V ) profile b (B 1 ;B 2 , H) = profile b (B 1 , H) ⊎ profile b (B 2 , H) profile b (B 1 ,B 2 , H) = profile b (B 1 , H) ⊎ profile b (B 2 , H) profile b (@[V 0 ⇒ B 0 ; T 0 . . . V n ⇒ B n ; T n ], H) = n i=0 profile g (V i ) ⊎ profile b (B i , H)
Finally, for a Chp description C, X , B0 • • • Bn , the partial function profile mapping a channel to its profile is defined by:

profile = n i=0 profile b ( Bi , H i ) ⊎ c → unprobed | c ∈ C ∧ port (c)
Notice that profile uses the profile "unprobed" as default value for each port; this simplifies the Lotos code produced by the translation and reduces the size of the corresponding state space.

Preliminary Simplifications

Prior to translation, we simplify all Chp processes by applying the following transformations in sequence: -All occurrences of skip are removed wherever possible, based on the facts that (1) skip is neutral element for sequential and collateral composition, (2) any branch "V ⇒ skip; loop" of a guarded command can be removed, and (3) any Bi equal to skip can be removed from " B0 • • • Bn ". After these transformations, skip may occur only in branches "V ⇒ skip; break" of guarded commands. -The abstract syntax tree of all processes Bi is reorganised so that the sequential composition operator ";" is right bracketed (based on the associativity of Chp sequential composition). After transformation, each sequence "B 1 ; B 2 ; B 3 " is bracketed as "B 1 ; (B 2 ; B 3 )", even if it was bracketed as "(B 1 ; B 2 ); B 3 " before. -If the rightmost process B n of a maximal sequence "B 0 ; . . . ;B n " is of the form "x:=V ", "c!V ", or "c?x", a final skip is added, leading to the sequence "B 0 ; . . . ;B n ; skip". This transformation simplifies the syntax-driven induction presented in Section 4.5. -For each process of the form "B 1 ;B 2 " such that inf (B 1 ), B 2 can be removed as it will never be executed.

Similarly, in each process of the form "B 1 ,B 2 " such that inf (B 1 ) = ¬inf (B 2 ), we replace the process B i (i ∈ {1, 2}) such that inf (B i ) is false, by "B i ; nil". Also, if ¬inf ( Bi ), then Bi is replaced by " Bi ; nil". These transformations are needed to obey the static check of functionalities in Lotos. After these transformations, all assignments and all communications (emissions and receptions) occur in prefix-form, i.e. they occur only in processes of the form "x:=V ; B", "c!V ; B", or "c?x; B". Precisely, Chp processes obtained after these transformations have the following syntax:

B ::= nil | skip | A;B | B 1 ,B 2 | @[V 0 ⇒ B 0 ; T 0 . . . V n ⇒ B n ; T n ] A ::= x:=V | c !V | c ?x | B 1 ,B 2 | @[V 0 ⇒ B 0 ; T 0 . . . V n ⇒ B n ; T n ]
where T and V are defined as in Section 2. In the sequel, we use this new grammar for the definition of the translation functions.

Translation of a Single Process

A Chp process Bi is translated into a Lotos process whose body is obtained using the recursive function c2l b (B, H, D, U, ∆), where B is a Chp process to translate, H is a mapping from channels to {neutral, active, passive}, and D, U , and ∆ are sets (in fact, alphabetically ordered lists) of variables necessary to compute the variables transmitted over Lotos sequential composition operators ">>". Intuitively, D is the set of variables that have a defined value before the execution of B, U is the set of variables that may be used after the execution of B, and ∆ is an auxiliary set of defined variables suitable for translating collateral compositions. We have the invariant property that D ⊆ ∆.

Translation of Channels. We apply code specialisation to optimise the translation of channels, i.e. the translation of a channel depends on its profile -"unprobed", "single", or "general ". -A Chp communication on a channel c of profile "unprobed" is translated directly into a single Lotos rendezvous on gate c. -The translation of a channel c of profile "single" also requires only one Lotos gate c. Probe operations are translated into communications on gate c; they are distinguished by an additional offer "!Probe", where "Probe" is a special constant belonging to an enumerated type with a single value. This translation is based on the value-matching communication feature of Lotos, which allows the emitter and the receiver both to synchronise on the same offer "!Probe". -A channel c of profile "general " is translated into a Lotos process channel c which manages the shared variable x c introduced in the Chp operational semantics. Five Lotos gates are introduced, namely three gates (c, c init , c probe) dedicated to the channel c, and two gates (probe enable and probe disable) common to all channels of profile "general". A Chp communication on c is translated into two Lotos communications: a binary communication on gate c init between the active process and channel c, followed by a three-party rendezvous on gate c between the emitter, the receiver, and channel c. A probe is translated into a binary communication on c probe between the passive process and channel c. Because channels are binary, for a given shared variable x c the potential conflicts on x c to be considered are only those between one single writer (the process active for c) and one single reader (the process passive for c). However, the situation is not so simple, because there are several shared variables and because each process may wish to read several variables simultaneously in an atomic step (during which one should prevent these variables from being modified).

Different approaches are possible to ensure atomicity of such a transition sequence, as for instance a locking mechanism, or a single process for all channel variables x c (so as to allow several channels to be probed in a single transition). We chose the locking approach for its modularity (when considering a subset of processes, only those channels linking the processes are required). Without loss of generality, we present in this article a single lock for all channels; using several locks (where all channels probed in a same expression share the same lock) might even lead to larger but equivalent state spaces (due to the interleaving of the confluent [START_REF] Groote | State space reduction using partial τ -confluence[END_REF] transitions).

The locking mechanism is implemented by the two gates "probe enable" (to acquire the lock) and "probe disable " (to release the lock). A shared variable can be modified (for initialisation -communication on c init -and reset after the communication on c) if no process owns the lock (i.e. if no process is between a synchronisation on probe enable and the next synchronisation on probe disable). Conversely, a shared variable can only be read if some process owns the lock. Stated otherwise, a synchronisation on probe enable places all shared variables in a read access mode, and a synchronisation on probe disable places all shared variables in a write access mode (this is the default initial mode).

The precise definition of channel c can take two forms: • If channel c links an active emitter and a passive receiver, the process channel c is defined as follows: Remark. Compared to the Chp operational semantics, the translation into Lotos introduces additional transitions (those containing "!Probe" offers, synchronisations on the gates probe enable, probe disable, and communications on gates of one of the forms c init and c probe). Anticipating the discussion about the correctness of the translation (see Section 4.10), these transitions should be hidden (i.e. renamed into τ ) when comparing the translation into Lotos with the Chp operational semantics.

process channel c[probe enable, probe disable, c, c init , c
2

Translation of Value Expressions. The translation of a value expression V is straightforward except for the probe operations that may occur in V . For each channel c probed by V , the shared variable x c must be read. Thus, each evaluation of a value expression V (in an emission, an assignment, or a guard) must be preceded by a sequence of communications with all channels probed by V . We define query probe(V 0 , . . . , V n ) = probe enable; c 1 probe ?x c1 : bool ?x c1 : s 1 ; . . . ; c m probe ?x cm : bool ?x cm : s m ; probe disable

where {c 1 , . . . , c m } = c ′ | profile(c ′ ) = general ∧ c ′ ∈ n i=0 chan v (V i
) is the set of channels of profile "general " probed by value expressions V 0 , ..., V n . For each probed channel c, this translation introduces two auxiliary variables, a boolean x c (which is true iff channel c is ready to communicate) and x c (which contains the value carried by c when x c is true).

Remark. There are only two places at which the translation generates synchronisations on probe enable and probe disable; the other one will be seen below during the translation of guarded commands. The above definition of query probe guarantees that a synchronisation on probe enable is eventually followed by a synchronisation on probe disable, since all rendezvous between probe enable and probe disable are communications with processes channel c that always accept to synchronise on gates c probe (after a synchronisation on probe enable). Thus, because there is only a single lock which is eventually released, the locking mechanism does not introduce deadlocks.

2 We define c2l v (x) as the function translating a Chp value expression into a Lotos value expression:

c2l v (x) = x c2l v f (V 1 , . . . , V n ) = f c2l v (V 1 ), . . . , c2l v (V n ) c2l v (c #) = x c c2l v (c #V ) = x c ∧ x c = c2l v (V )
Translation of nil. nil is translated into stop.

Remark. The Chp operational semantics and the translation into Lotos coincide in associating nil to a deadlock.

2

Translation of skip. Due to the preliminary transformations of Section 4.4, skip may only occur in a guarded command as a branch "V ⇒ skip; break" (this case is handled below as part of guarded commands) or at the end of a sequence. In the latter case:

c2l b (skip, H, D, U, ∆) = exit(ξ 1 , . . . , ξ n )
where {x 1 , . . . , x n } = ∆ ∩ U , and (∀i ∈ {1, . . . , n}) ξ i = x i if x i ∈ D or ξ i = "any type(x i )" otherwise.

Remark. The translation into Lotos generates a transition (labelled with "exit(ξ 1 , . . . , ξ n )") that corresponds to the √ -transition of the Chp operational semantics. 2

Translation of "c !V ; B" and "c ?x; B" when profile(c) = unprobed . Communication on a channel of profile "unprobed" is translated directly into a Lotos rendezvous communication:

c2l b ("c !V ; B", H, D, U, ∆) = query probe(V ); c !c2l v (V ); c2l b (B, H, D, U, ∆) c2l b ("c ?x; B", H, D, U, ∆) = c ?x : s; c2l b (B, H, D ∪ {x}, U, ∆ ∪ {x})
Remark. As regards the relationship between this translation and the operational semantics given in Section 3 for Chp emissions and receptions, four (i.e. 2 × 2) cases should be considered depending on: -Emission v. reception: the translation into Lotos generates, for a reception, single rendezvous on c for receptions; for an emission it generates a rendezvous on c that occurs after a sequence of transitions (communications on c probe and synchronisations on probe enable and probe disable, see the definition of query probe above), required to evaluate the value V . -H(c) = passive v. H(c) = active: in the former case, the first rule of the Chp operational semantics for emissions (respectively receptions) produces a single transition (communication on c); in the latter case, two transitions are produced: a first τ -transition (second inference rule on the left, corresponding to an assignment to the variable x c ) followed by a communication on c (third rule on the right). Thus, the four cases are the following: -Passive reception: both the Chp operational semantics and the translation into Lotos generate one single rendezvous on c. -Active emission: the τ -transition the Chp operational semantics matches the sequence of transitions (generated by query probe); if these transitions are hidden, branching equivalence is preserved. -Passive emission: the translation into Lotos introduces a sequence of transitions that, if hidden, preserve branching equivalence (this is a particular case of the more general notion of τ -confluence [START_REF] Groote | State space reduction using partial τ -confluence[END_REF]). -Active reception: the τ -translation generated by the second rule (on the left) of the Chp operation semantics for receptions is confluent; therefore the Lotos code can be optimised by not generating a τ -transition while still preserving branching equivalence. 2

Translation of "c !V ; B" and "c ?x; B" when profile(c) = general . The translation of an emission on a channel c depends whether H(c) is "active" or "passive": -A passive emission -when H(c) = passive -is translated as follows:

c2l b ("c !V ; B", H, D, U, ∆) = query probe(V ); c !c2l v (V ); c2l b (B, H, D ∪ {x}, U, ∆ ∪ {x})
-The translation of an active emission -when H(c) = active -requires in addition to initialise the variable x c before communication. Thus, the translation of an active emission is as follows:

c2l b ("c !V ; B", H, D, U, ∆) = query probe(V ); c init !c2l v (V ); c !c2l v (V ); c2l b (B, H, D ∪ {x}, U, ∆ ∪ {x})
The translation of a reception on a channel c of sort s = type(c) depends whether H(c) is "active" or "passive": -A passive reception -when H(c) = passive -is translated as follows: Remark. As regards the relationship between this translation and the operational semantics given in Section 3 for Chp emissions and receptions, three out of four cases are similar to the case where profile(c) = unprobed (see above). In the case of an active reception, the second rule (on the left) of the Chp operational semantics generates a τ transition, which is matched by the rendezvous on c init ; if c init is hidden, branching equivalence is preserved. 2

Translation of "c !V ; B" and "c ?x; B" when profile(c) = single. The translation depends on the value of H(c):

-If H(c) = passive, the translation is straightforward (identical to the "unprobed" case):

c2l b ("c !V ; B", H, D, U, ∆) = query probe(V ); c !c2l v (V ); c2l b (B, H, D, U, ∆) c2l b ("c ?x; B", H, D, U, ∆) = c ?x : s; c2l b (B, H, D ∪ {x}, U, ∆ ∪ {x})
where s = type(c).

Remark. Branching equivalence is preserved for the same reasons as for the "unprobed" case. 2 -If H(c) = active, the translation is more involved because the active process Bi must allow its passive partner to probe channel c an arbitrary number of times. Thus, the active process must allow any actual communication on c to be preceded by a (possible empty) sequence of communications with an additional offer "!Probe" (as mentioned during the translation of channels). This protocol is encapsulated in an auxiliary Lotos process channel c, the definition of which depends whether c is used for emission or reception.

• An active emission "c !V ; B" is translated as follows:

c2l b ("c !V ; B", H, D, U, ∆) = query probe(V ); channel c[c] c2l v (V ), x 1 , . . . , x n >> accept x 1 : s ′ 1 , . . . , x n : s ′ n in c2l b (B, H, D ′ , U, ∆ ′ ) where {c 1 , . . . , c m } = chan v (V ), (∀i ∈ {1, . . . , m}) s i = type(x ci ), U ′ = use(B) ∪ U , D ′ = D ∩ U ′ , ∆ ′ = ∆ ∩ U ′ , {x 1 , . . . , x n } = D ′ , and (∀i ∈ {1, . . . , n}) s ′ i = type(x i ). Process channel c is defined by: process channel c[c](x : s, x 1 : s 1 , . . . , x n : s n ) : exit(s 1 , . . . , s n ) := c !x; exit(x 1 , . . . , x n ) [] c !Probe !x; channel c[c](x, x 1 , . . . , x n ) endproc where s = type(c).
Remark. As for all active emissions, the translation into Lotos introduces a sequence of communications that, after hiding, matches the τ -transition generated by the Chp operational semantics, thus preserving branching equivalence. 2

• An active reception "c ?x; B" translates as follows:

c2l b ("c ?x; B", H, D, U, ∆) = channel c[c](x ′′ 1 , . . . , x ′′ n ) >> accept x ′ 1 : s ′ 1 , . . . , x ′ m : s ′ m in c2l b (B, H, D ′ , U, ∆ ′ ) where U ′ = use(B) ∪ U , D ′ = (D ∪ {x}) ∩ U ′ , ∆ ′ = (∆ ∪ {x}) ∩ U ′ , D ′′ = D ′ \ {x}, {x ′ 1 , . . . , x ′ m } = D ′ , {x ′′ 1 , . . . , x ′′ n } = D ′′ , (∀i ∈ {1, . . . , m}) s ′ i = type(x ′ i )
, and (∀i ∈ {1, . . . , n}) s ′′ i = type(x ′′ i ). Process channel c is defined by:

process channel c[c](x ′′ 1 : s ′′ 1 , . . . , x ′′ n : s ′′ n ) : exit(s ′ 1 , . . . , s ′ m ) := c ?x : s; exit(x ′ 1 , . . . , x ′ m ) [] c !Probe; channel c[c](x ′′ 1 , . . . , x ′′ n ) endproc where s = type(c).
Remark. As for the "unprobed" case, the translation into Lotos removes the confluent τ -transition introduced by the Chp operational semantics, thus preserving branching equivalence.

2 Notice that, contrary to the "general " case above, in the "single" case, the process channel c never needs (neither for an active emission nor for an active reception) to evaluate a probe, and, thus, never needs to synchronise on probe enable and probe disable.

Remark. Preservation of branching equivalence albeit the communications containing offers of the form "!Probe" introduced by the translation into Lotos (and that do not exist in the Chp operational semantics) is discussed during the translation of guards and the translation of guarded commands. 2

Translation of "x:=V ;B". An assignment to a variable x of sort S is translated as follows:

c2l b ("x:=V ;B", H, D, U, ∆) = query probe(V ); let x : s = c2l v (V ) in τ ; c2l b B, H, D ∪ {x}, U, ∆ ∪ {x}
Remark. The translation generates the internal transition "τ ", also present in the Chp operational semantics (see Section 3) and the Petri net model of [START_REF] Renaudin | From hardware processes to asynchronous circuits via Petri nets: an application to arbiter design[END_REF]. Moreover, as for emissions, if the value V contains probe operations, query probe introduces a confluent sequence of communications that, after hiding, preserves branching equivalence. 2

Translation of "A; B". This translation rule applies only if A is a collateral composition or a guarded command (all other cases have been handled before):

c2l b ("A; B", H, D, U, ∆) = c2l b (A, H, D, U ′ , D) >> accept x 1 : s 1 , . . . , x n : s n in c2l b (B, H, D ′ , U, ∆ ′ )
where

U ′ = use(B) ∪ U \ def n (B) , D ′ = D ∪ def (A) ∩ U ′ , {x 1 , . . . , x n } = D ′ , and ∆ ′ = ∆ ∪ def (A) ∩ U ′ .
Remark. The symmetric sequential composition operator of Lotos " >> " differs from Chp sequential composition by the fact that it creates a τ -transition. In general, this transition is not always confluent (as in the Lotos behaviour "(c; stop [] exit) >> B", which is equivalent to "c; stop [] τ ; B"). However, the preliminary simplifications applied to the Chp description forbid such situations, as the Lotos behaviour generated for A (which is either a collateral composition and a guarded command) always contains at least one transitions, so that the τ -transition created by ">>" is always prefixed by some other transitions, and thus cannot occur as the first transition of a non-deterministic choice. 2

Translation of "B 1 ,B 2 ". A collateral composition is translated as follows:

c2l b ("B 1 ,B 2 ", H, D, U, ∆) = c2l b (B 1 , H, D 1 , U, ∆ ′ ) ||| c2l b (B 2 , H, D 2 , U, ∆ ′ )
where

D 1 = D \ def (B 2 ), D 2 = D \ def (B 1 ), and ∆ ′ = ∆ ∪ def (B 1 ) ∪ def (B 2 ).
this case, a busy waiting is implemented (using a recursive call to P B ), so as to allow to probe the channels c 1 , ..., c l once more until some guard becomes true. The auxiliary process P B is defined as follows: process P B [probe enable, probe disable, gate( Bi , H)](x 1 : s 1 , . . . , x m : s m ) : F probe enable; c 1 probe ?x c1 : bool ?x c1 : type(x c1 ); . . . ; c l probe ?x c l : bool ?x c l : type(x c l ); (

c2l g (V 0 ) probe disable; c2l c B 0 , T 0 , H, D ′ \ def (B 0 ) \ use(B 0 ) , U, ∆ ′ [] • • • [] c2l g (V n ) probe disable; c2l c B n , T n , H, D ′ \ def (B n ) \ use(B n ) , U, ∆ ′ [] [ j∈{0,...,n} ∧ cond(Vj ) ¬c2l v (V j ) ] -> probe disable; P B [probe enable, probe disable, gate( Bi , H)](x 1 , . . . , x m )
) endproc where

∆ ′ = ∆ ∪ def (B) F = noexit if inf (B) exit type(x ′ 1 ), . . . , type(x ′ q ) such that func(B, D, U ) = exit({x ′ 1 , . . . , x ′ q }
) otherwise and where the translation of a branch is defined as:

c2l c (B j , break, H, D, U, ∆) = c2l b (B j , H, D, U, ∆) c2l c (B j , loop, H, D, U, ∆) = c2l b B j , H, D, D ∪ def (B j ) \ use(B j ) , D >> accept x 1 : s 1 , . . . , x m : s m in P B [probe enable, probe disable, gate( Bi , H)](x 1 , . . . , x m )
Remark. As regards correction, we must distinguish between two parts in the Lotos code generated for P B . There is first a prefix, which corresponds to the first line of P B , i.e. the sequence of transitions starting with probe enable and ending with "c l probe ?x c l : bool ?x c l : type(x c l )". Notice that this prefix is similar to the Lotos code generated by query probe(V 0 , . . . , V n ) in the translation of value expressions. This prefix is followed by a choice between (n + 1) branches: the first n branches are the lines starting with "c2l g (V i )" and the last branch is the line starting with the guard " j∈{0,...,n} ∧ cond (Vj ) ¬c2l v (V j ) ".

Notice that the guards of these branches are not necessarily mutually exclusive, because Chp guarded commands themselves can be nondeterministic. However, the (n+1) branches are exhaustive, since the guard of the last branch acts as a default case, so that always at least one branch can be taken. Moreover, the definition of P B guarantees that the synchronisation on probe enable is eventually followed by a synchronisation on probe disable, because all branches contain a synchronisation on probe disable, and all rendezvous between probe enable and probe disable are communications with the channel c processes (see the translation of channels with profile(c) = general ); these communications are always possible because each channel c process always accepts to synchronise on its c probe gate after a synchronisation on probe enable. Thus, as regards the preservation of branching equivalence: -The prefix preserves branching equivalence for the same reasons as for the definition of query probe(V 0 , . . . , V n ): after hiding, the transitions on the probe enable and c i probe gates become confluent. -Each of the first n branches starts with either one or two transitions that match, after hiding, the τtransition generated by the Chp operational semantics. Indeed, the definition of c2l g (V n ) implies that the i-th branch starts either, if cond (V i ), with a synchronisation on probe disable or, if ¬cond (V i ), with a communication having the form "c !Probe" or "c !Probe ?x : type(c)" followed by a synchronisation on probe disable. -The last branch has no direct counterpart in the Chp operational semantics. However, it consists of a synchronisation on probe disable followed by a recursive call to P B (without modification of the value parameters x 1 , ..., x m ). Thus, after hiding the probe disable gate, this branch just amounts to a τ -cycle, which preserves branching equivalence. 2

Translation of Several Concurrent Processes

In a nutshell, the parallel composition " " of Chp is translated into the Lotos operator "|[• • • ]|", because the underlying model of asynchronous concurrency (interleaving semantics) implemented by these two operators is basically the same. However, there are some "surface" differences between both languages worth being mentioned: -The parallel composition operator of Chp is n-ary but allows only binary communications; to the contrary, the parallel composition operator of Lotos is binary but allows n-ary communications. -Although in the general case certain involved communication patterns cannot be expressed in Lotos [START_REF] Garavel | A graphical parallel composition operator for process algebras[END_REF], translation into Lotos is always possible for Chp descriptions, since Chp channels have pairwise distinct names. -Although communication in Chp is always between two parties, the generated Lotos code contains three-party communications. This is no problem, since in the generated Lotos code any three-party communication is a communication on a channel c with profile(c) = general , which involves exactly two processes Bi and Bj (sender and receiver) plus one of the processes channel c representing the shared variable x c (see Section 4.5, translation of channels). -The synchronisation rules are not identical: in Chp, two processes synchronise implicitly on all common channels; in Lotos, processes do not synchronise on their common gates, but only on the set of gates g 1 , ..., g n explicitly listed inside the parallel composition operator "|[g 1 , ...,

g n ]|". The translation of a Chp description C, X , B0 • • • Bn is defined as: c2l (" B0 • • • Bn ") = c2l p (" B0 • • • Bn ", C) |[probe enable, probe disable, c 1 , c 1 probe, . . . , c l , c l probe, c i1 init , . . . , c ip init ]| ( channel c 1 [probe enable, probe disable, c 1 , c 1 init , c 1 probe] |[probe enable, probe disable]| • • • |[probe enable, probe disable]| channel c l [probe enable, probe disable, c l , c l init , c l probe] )
where function c2l p is defined as follows:

c2l p (" B0 • • • Bn ", C) = c2l b ( B0 , H 0 , ∅, ∅, ∅) if n = 0 c2l b ( B0 , H 0 , ∅, ∅, ∅) |[chan bin ( B0 ) ∩ C]| c2l p " B1 • • • Bn ", C \ chan bin ( B0 ) otherwise
where chan bin (B) = c | c ∈ chan(B) ∧ ¬port (c) is the set of binary channels occurring in process B, {c 1 , . . . , c l } = c | c ∈ C ∧ profile(c) = general is the set of all channels of profile "general " in C, and {i 1 , . . . , i p } = i | i ∈ {1, . . . , l} ∧ ¬port (c i ) are the indexes i such that c i ∈ {c 1 , . . . , c l } is a binary channel (and no port) of profile "general ". We distinguish between the constant C corresponding to the set of channels of the Chp description and the parameter C used in the recursive definition of c2l p to represent the set of channels for which a communication has yet to be generated. translated as a communication with offer "!Probe" (see Translation of Guards in Section 4.5). At last, the collateral composition is encoded as an interleaving " ||| " (of an emission on c and a communication on c i ). In both branches of the arbiter, the loop is translated in a recursive call to process arbiter.

The Lts generated from this Lotos code by the Caesar tool of Cadp has 72 states and 165 transitions after reduction modulo strong bisimulation. The Lts obtained after hiding all transitions containing a "!Probe" offer was proved (by the Bisimulator tool [START_REF] Bergamini | Bisimulator: A modular tool for on-the-fly equivalence checking[END_REF] of Cadp) to be branching equivalent to the one corresponding to the Chp operational semantics. Without code specialisation, the Lts generated by Caesar (also reduced modulo strong bisimulation) would have been about 20% larger, with 85 states and 198 transitions, still being branching equivalent.

Example of the Arbiter with Priorities

For the arbiter with priorities of Section 2.6, profile(c) = unprobed and profile(c 1 ) = profile(c 2 ) = general (because c 1 and c 2 are probed in an expression). The translation rules yield the following Lotos behaviour:

arbiter [probe enable, probe disable, c, c 1 , c 1 probe, c 2 , c 2 probe] |[ c 1 , c 2 ]| client -1[c 1 , c 1 init ] ||| client -2[c 2 , c 2 init ] |[ probe enable, probe disable, c 1 , c 1 init , c 1 probe, c 2 , c 2 init , c 2 probe ]|   channel c 1 [probe enable, probe disable, c 1 , c 1 init , c 1 probe] |[probe enable, probe disable ]| channel c 2 [probe enable, probe disable, c 2 , c 2 init , c 2 probe]  
where the processes channel c 1 and channel c 2 are obtained as described in Section 4.5 -Translation of Channels. The other processes are defined as follows:

process client -1[c 1 , c 1 init ] : noexit := c 1 init !true; c 1 !true; client -1[c 1 , c 1 init] [] c 1 init !false; c 1 !false; client -1[c 1 , c 1 init] endproc process client -2[c 2 , c 2 init ] : noexit := c 2 init ; c 2 ; client -2[c 2 ,
[] [x c2 ∧ ¬(x c1 ∧ x c1 )] -> probe disable; (c !2; exit) ||| (c 2 ; exit) >> arbiter [probe enable, probe disable, c, c 1 , c 1 probe, c 2 , c 2 probe] [] [¬(x c1 ) ∧ ¬ x c2 ∧ ¬(x c1 ∧ x c1 ) ] -> probe disable ; arbiter [probe enable, probe disable, c, c 1 , c 1 probe, c 2 , c 2 probe] ) endproc
Since channel c 1 (respectively c 2 ) has profile "general ", any active emission on c 1 (respectively c 2 ) is preceded by a communication on c 1 init (respectively c 2 init ) with process channel c 1 (respectively channel c 2 ) to allow probes. Similarly, execution of process arbiter starts with communications on gates c 1 probe and c 2 probe with processes channel c 1 and channel c 2 to check (or probe) whether a channel is ready for communication (first offer) and to retrieve the value possibly sent (second offer). Note that a third choice is added in process arbiter , whose guard corresponds to the negation of the two other guards, and whose body is a simple call to the process arbiter itself. This case is necessary to check again the possibility to probe channels c 1 and c 2 , if none of the probes was successful the first time.

The Lts corresponding to this Lotos specification, generated by the Caesar tool of Cadp and reduced modulo strong bisimulation, has 138 states and 303 transitions. The Lts obtained after hiding all labels corresponding to communications on gates c 1 init , c 2 init , c 1 probe, and c 2 probe was proved (by the Bisimulator tool of Cadp) to be branching equivalent to the one presented in Figure 3.

Correction Concerns about the Translation from CHP into LOTOS

Our translation algorithm from Chp into Lotos is implemented in a translator (see Section 5) that is being used by hardware designers for validating several asynchronous circuits. Interestingly, when discussing correctness issues with these designers, we received the feedback that a formal proof of correction for our translator was a low priority issue. In addition to the usual constraints (lack of resources and time-to-market pressure), we can mention the following reasons:

(i) In the hardware community, circuit designers rely on closed-source commercial tools to perform semantic translations, for instance to transform a high-level description into Rtl (Register Transfer Level ), to synthesise a netlist from an Rtl description, or to perform placement and routing for a netlist. In most cases, designers do not have any formal proof of correctness of for the complex algorithms present in these tools. There are even documented situations in which the tools are known to generate incorrect or inefficient outputs, which have to be corrected or optimised manually later. (ii) Even if the tools were fully reliable, with correction proofs available, it is still unlikely that designers would trust them blindly because of the huge costs arising from mistakes in hardware circuits. Instead, designers routinely use independent cross-checking tools to verify whether commercial translation tools have produced correct outputs or not. Examples of such tools are symbolic model checkers, which verify that a generated netlist is equivalent to its high level design, or Lvs (Layout Versus Schematic) checkers, which verify that an electric circuit obtained after placement and routing correctly implements its netlist. (iii) The intended use of our translator is to enable model checking of Chp descriptions. In general, formal semantics is not of prime importance to model checkers -some famous model checkers do not even have a formal definition for their input languages! This is partly justified by the use of model checkers for "bug hunting": the model checker finds possible problems, which are then analysed manually to understand if they are "real" bugs in the design or "false positives" (caused by excessive abstractions or issues in the model checker itself). However, even if model checkers are not fully proven (with a non-null, yet small, probability of reporting false positives or even omitting the real bugs), the use of model checking is still beneficial, as it often uncovers real problems that would have remained undetected otherwise. This was the case with our translator (see Section 5); we can also mention that no translation bug has been reported so far. Despite a formal proof of correction for our translator was considered of little practical interest by the end-users, the remainder of this section addresses this issue.

According to concurrency theory results, a natural approach to prove the correction of our translation would be to seek for an equivalence relation (such as a bisimulation) between the Lts (noted "Lts Sos ") obtained from a Chp description C, X , B0 • • • Bn using the proposed operational semantics for Chp and the Lts (noted "Lts Lotos ") corresponding to the Lotos specification c2l (" B0 • • • Bn ").

This task is not easy, since some Chp descriptions do not have a defined semantics, i.e. if they access variables that are neither initialised nor assigned before. For these Chp descriptions, our Sos semantics is undefined (as some variables evaluate to the undefined value "⊥"). To the contrary, Lotos has a set of static semantic constraints that rule out all Lotos descriptions in which a variable is used before being defined, so that each Lotos description satisfying these constraints has a "well-defined" dynamic semantics. Thus, only the subset of Chp that forbids accesses to undefined variables should be considered.

Lotos

Moreover, finding an equivalence is difficult, as Lts Sos and Lts Lotos have different sets of actions (i.e. labels of transitions). Indeed, due to the translation of the probe operation, Lts Lotos might contain additional gates (such as probe enable, probe disable, c init , and c probe) that do not exist in Lts Sos . We suggest to hide these additional gates using the "hide G in" construct of Lotos. However, this is not sufficient, since Lts Lotos might also contain additional offers "!Probe" which do not exist in Lts Sos . We suggest to apply a renaming operator (which does not exist in Lotos, but in other process calculi such as E-Lotos [START_REF]ISO/IEC, Enhancements to LOTOS (E-LOTOS), International Standard 15437[END_REF]) to rename into τ all labels containing a "!Probe" offer. Let Lts ′ Lotos be the Lts obtained from Lts Lotos after these hiding and renaming steps.

Lts Sos and Lts ′ Lotos are still not equivalent with respect to strong bisimulation, since the hiding and renaming steps introduce τ -transitions that do not exist in Lts Sos . Besides, the symmetric sequential composition operator ">>" of Lotos also introduces τ -transitions that do not exist in Lts Sos . Thus, our translation can only preserve a weak equivalence, i.e. an equivalence that handles τ -transitions differently from ordinary transitions.

Furthermore, as mentioned before in Section 4.5, the translation of guarded commands creates τ -cycles (namely, in the last branch of process P B , i.e. the line starting with " j∈{0,...,n} ∧ cond(Vj ) ¬c2l v (V j ) "). Thus, it is necessary to consider a weak equivalence relation that abstracts τ -cycles away. This suggests to consider branching bisimulation [START_REF] Van Glabbeek | Branching-time and abstraction in bisimulation semantics[END_REF], the strongest of the weak equivalences found in the literature.

To prove that Lts Sos and Lts ′ Lotos are branching equivalent, one should proceed in two steps: (1) consider each Chp process Bi separately, apply the preliminary simplifications described in Section 4.4, and prove that its translation into Lotos preserves branching equivalence -this can be done by induction on the syntax of Bi ; (2) extend this result to the parallel composition of several processes " B0 • • • Bn " taking into account that branching bisimulation is a congruence for the parallel composition operator of Lotos. Proof arguments and remarks that substantiate this have been given throughout Sections 4.4, 4.5, and 4.6.

Implementation and Applications

We developed a translator from Chp into Lotos, called Chp2Lotos, which supports full Chp including value passing communication, ports open to the environment, and hierarchical components. Chp2Lotos was developed using the Syntax and Lotos NT compiler construction technologies [START_REF] Garavel | Compiler construction using LOTOS NT[END_REF] and consists of 2,200 lines of Syntax, 13,400 lines of Lotos NT, and 3,900 lines of C. The translation is performed in several steps as depicted in Figure 6. The parsing and elaboration phases construct an intermediate representation, which is then optimised and simplified using the transformations described in Section 4.4. After computing the channel profiles, the translator generates Lotos code according to the translation functions defined in Sections 4.5 and 4.6.

Taking advantage of the possibility offered by the Cadp toolbox to implement Lotos data types using external C code, the predefined Chp data types have been directly implemented as C libraries, thus avoiding the recompilation of the generic data types each time the Lotos code is used for state space generation or verification.

We validated the Chp to Lotos translator on more than 500 Chp specifications, corresponding to about 14,500 lines of Chp, which (after translation and pretty-printing) generate about 34,700 lines of Lotos code. This increase in the number of generated lines is mainly due to the Lotos pretty-printer of Cadp, which puts each communication action on a separate line. We also applied the Chp to Lotos translator to two asynchronous circuits designed at the Cea/Leti laboratory in Grenoble (France) that we present with more details below.

Data Encryption Standard. The Des (Data Encryption Standard ) [START_REF]Data encryption standard (DES), Federal Information Processing Standards FIPS[END_REF] defines a method for encrypting information. It accepts as input two 64-bit words (a data and a key) and an operation mode (i.e. ciphering or deciphering), and outputs the (de)ciphered value. In this case study, we experimented Chp2Lotos on a Chp description of an asynchronous implementation of the Des (25 processes, which correspond to about 1,600 lines of Chp), which has also been studied in [START_REF] Borrione | Validation of asynchronous circuit specifications using IF/CADP[END_REF]. We focused on the control part, abstracting 64-bit words into a single data value.

Since this case study contains many concurrent processes, direct generation of the Lts failed due to lack of memory (after 70 minutes, the generated Lts had more than 17 million states and 139 million transitions). However, using the compositional verification techniques (decomposing, minimising, and recomposing processes) [START_REF] Lang | Compositional verification using SVL scripts[END_REF] of the Cadp toolbox, we generated an equivalent, but smaller Lts (16,910 states and 85,840 transitions) in 8 minutes on a SunBlade 100 (500 Mhz Ultra Sparc II processor, 1.5 GB of RAM). In a second step, several properties were proved on this Lts, such as deadlock freeness and some safety and liveness properties. As an example, we checked that after the reception of the three inputs (key, data, decrypt), an output is always returned. Once the Lts is generated from the Lotos specification, only a few seconds suffice to verify each property.

Asynchronous Network on Chip Architecture. As a second case study, we considered the Anoc (Asynchronous Network On Chip) architecture [START_REF] Beigné | An asynchronous NoC architecture providing low latency service and its multi-level design framework[END_REF][START_REF] Beigné | Design of off-chip and on-chip interfaces for a GALS NoC architecture[END_REF], which is used as the backbone of Faust, a 4 th generation wireless telecom baseband [START_REF] Durand | FAUST : On-chip distributed architecture for a 4G baseband modem SoC[END_REF]. Anoc implements the Gals paradigm, in which synchronous resources (e.g. memory, generic processor, dedicated hardware for Fourier transformation or Mpeg decoding) are linked via an asynchronous communication network, consisting of a set of nodes, each of which is connected to a resource and four other nodes. Although no assumption is made on the topology of the network as regards the architecture of the node, the Faust implementation of Anoc connects the nodes in a 2D-Mesh topology for several reasons (e.g. scalable bandwidth, easy placement and route on silicon).

Each network node provides lower-level network services, i.e. routing and arbitration of the transiting messages, called flits. Each node consists of five input controllers, which route incoming flits to one of the other four ports (a flit is never returned to the incoming port), and five output controllers, which arbitrate between flits heading for the same output.

In this case study, we dealt in particular with the verification of the most complex component of a node of Anoc, namely an input controller. As for the Des model, the Anoc model in Chp was abstracted by considering only four transmitted values (to identify different flits) plus the control information required for routing and handling packets (i.e. sequences of flits). Furthermore, we used a traffic generator (specified in Chp) to implement several realistic scenarios with packets of different length (one or more flits), either emitted sequentially or overlapping on different channels and to different destinations.

For each scenario, the Chp model of the input controller (about 1,200 lines of Chp) was translated into Lotos (about 3,600 lines of code) using Chp2Lotos (the translation takes less than one second). Then, we applied the compositional techniques of Cadp to generate the state space. The generation of the Lts corresponding to the input controller of Anoc for a particular cycle of four flits was automated using an Svl script [START_REF] Garavel | SVL: a scripting language for compositional verification[END_REF] (about 500 lines), which invokes automatically the different Cadp tools for state space generation, hiding, minimisation, and composition. The Svl script is generic in the sense that it can be used to generate the state spaces for all scenarios. For a typical scenario, the Svl script generates in about four minutes the corresponding Lts (1,300 states and 3,116 transitions), the largest intermediate Lts observed during the generation having 295,893 states and 812,283 transitions.

Independently from any Chp model, we enunciated functional properties describing the protocol behaviour of the input controller, such as protocol correctness (the input controller must comply at its inputs with the Anoc protocol, and transmit the incoming data to an output controller), data integrity (the contents of the communications must be preserved by the input controller), and correct packet routing (the input controller has to route all the flits of a packet in the right direction). These properties were verified using a generic Svl script (of about 250 lines), calling the model checking and equivalence checking tools of Cadp.

During this verification stage, in collaboration with the authors of [START_REF] Beigné | An asynchronous NoC architecture providing low latency service and its multi-level design framework[END_REF], we detected automatically a routing error -which previously had been found only manually and corrected in the synthesised and manufactured chip.

More details about the Anoc case study are presented in [START_REF] Salaün | Formal verification of CHP specifications with CADP -illustration on an asynchronous network-on-chip[END_REF]. Recently, Cea/Leti managed the compositional verification of the output controller of Anoc using Chp2Lotos and Cadp.

Last but not least, as for the simple arbiter example, the code specialisation technique proved to be effective in both case studies, by reducing the size of the intermediate state spaces up to a factor of 89 as regards states and 156 as regards transitions, which had the effect of reducing the overall run-time of the compositional generation and verification by a factor of two.

Related Work

In general, the semantics of hardware process calculi is not given in terms of Sos rules (as it is usual in the concurrency theory community), but rather by means of a translation into another formalism, e.g. handshake circuits for Tangram [START_REF] Van Berkel | Handshake Circuits: An Asynchronous Architecture for VLSI Programming[END_REF], Petri nets for Chp [START_REF] Renaudin | From hardware processes to asynchronous circuits via Petri nets: an application to arbiter design[END_REF], and Csp for Balsa [START_REF] Wang | Towards a unifying CSP approach for hierarchical verification of asynchronous hardware[END_REF]. In that respect, our Sos semantics is an original contribution allowing to bridge the gap between hardware process calculi and mainstream process calculi.

As regards the verification of asynchronous circuits and architectures, we distinguish two lines of related work: -A first line of work focusses on the verification of asynchronous designs without paying attention to synthesis. In these approaches, the asynchronous designs are specified in the input language of the verification tool to be used, such as Promela for Spin [START_REF] Baulch | Analyzing and verifying locally clocked circuits with the concurrency workbench[END_REF][START_REF] Rahardjo | SPIN as a hardware design tool[END_REF], Ccs for Cwb [START_REF] Clark | The verification of asynchronous circuits using CCS[END_REF][START_REF] Kapoor | Modelling and verification of delay-insensitive circuits using CCS and the Concurrency Workbench[END_REF], Lotos for Cadp [START_REF] He | Verifying and testing asynchronous circuits using LOTOS[END_REF][START_REF] Yoeli | LOTOS/CADP-based verification of asynchronous circuits[END_REF][START_REF] Yoeli | Verification of Systems and Circuits Using LOTOS[END_REF], or Csp for Fdr2 [START_REF] Wang | On process-algebraic verification of asynchronous circuits[END_REF][START_REF] Josephs | Gate-level modelling and verification of asynchronous circuits using CSPm and FDR[END_REF]. These approaches target gate level descriptions of asynchronous circuits [START_REF] Baulch | Analyzing and verifying locally clocked circuits with the concurrency workbench[END_REF][START_REF] Rahardjo | SPIN as a hardware design tool[END_REF][START_REF] Clark | The verification of asynchronous circuits using CCS[END_REF][START_REF] He | Verifying and testing asynchronous circuits using LOTOS[END_REF][START_REF] Yoeli | LOTOS/CADP-based verification of asynchronous circuits[END_REF][START_REF] Yoeli | Verification of Systems and Circuits Using LOTOS[END_REF][START_REF] Wang | On process-algebraic verification of asynchronous circuits[END_REF][START_REF] Josephs | Gate-level modelling and verification of asynchronous circuits using CSPm and FDR[END_REF] or explicitly model of wires of unbounded delay [START_REF] Kapoor | Modelling and verification of delay-insensitive circuits using CCS and the Concurrency Workbench[END_REF]. This is different from our approach, which aims at verifying high level Chp descriptions from which gate level models can be synthesised automatically. Furthermore, a common issue with these approaches is the necessity of having two different descriptions of the circuit, one for verification and one for synthesis. -A second line of work devises verification techniques for asynchronous designs described using hardware process calculi, for which synthesis tools exist. There are fewer works in this line; we can mention three such approaches.

• Firstly, the process algebra Circal (Circuit Calculus) and its associated tool [START_REF] Bailey | An exercise in the automatic verification of asynchronous designs[END_REF] have been designed for the automatic verification of circuits. A particularity of Circal is the possibility that several actions may happen simultaneously, which enables a precise modelling of systems combining synchrony and asynchrony. Recent extensions of Circal allow to specify timing and performance properties by adding observer processes [START_REF] Cerone | Property verification of asynchronous systems[END_REF]. Contrary to Chp, Circal provides no direct support for value passing communication, although this allows more abstract and concise models and is essential for describing large complex systems. Verification in Circal mainly relies on equivalence checking. By translating to Lotos and using Cadp, our approach offers a wider variety of verification techniques, including equivalence checking, model checking of µ-calculus formulae, as well as on-the-fly techniques, static analysis, and distributed and compositional verification. • Secondly, the Balsa language can also be used together with Csp. [START_REF] Wang | Towards a unifying CSP approach for hierarchical verification of asynchronous hardware[END_REF] starts with a Balsa description of circuits, and sketches, but does not detail, a translation from Balsa into Csp. Contrary to our approach, the handling of probe-like operations is simpler in [START_REF] Wang | Towards a unifying CSP approach for hierarchical verification of asynchronous hardware[END_REF], since Balsa's handshake enclosure is more restrictive than Chp's probe operation (in particular, the equivalent of a probe can be used only in guards). Furthermore, the approach of [START_REF] Wang | Towards a unifying CSP approach for hierarchical verification of asynchronous hardware[END_REF] does not translate a Balsa process B independently of the other Balsa processes communicating with B, whereas our approach without code specialisation is modular in the sense that it allows to translate each Chp process into Lotos regardless of its context.

• Thirdly, [START_REF] Borrione | Validation of asynchronous circuit specifications using IF/CADP[END_REF] is a precursor of our approach in the sense that it is also based on Chp and uses Cadp too. Contrary to our approach, [START_REF] Borrione | Validation of asynchronous circuit specifications using IF/CADP[END_REF] translates Chp into networks of communicating automata. Thus, [START_REF] Borrione | Validation of asynchronous circuit specifications using IF/CADP[END_REF] cannot handle Chp processes with intertwined sequential and parallel compositions, except by flattening parallel processes, which is less efficient than our translation from Chp into Lotos. Additionally, our approach brings support of the probe operation. As regards the efficiency of verification, we observed reductions of the Lts generation time by factors up to four on the same Des case study as [START_REF] Borrione | Validation of asynchronous circuit specifications using IF/CADP[END_REF]. Compared to a previous conference publication [START_REF] Salaün | Translating hardware process algebras into standard process algebras -illustration with CHP and LOTOS[END_REF], the present article brings original material. In [START_REF] Salaün | Translating hardware process algebras into standard process algebras -illustration with CHP and LOTOS[END_REF], the probe operations of Chp could only be used in guards; the present article lifts this restriction by supporting probe operations in any expression. Moreover, the present article introduces proof arguments about the correctness of the translation as well as code specialisation to optimise the translation. Finally, it reports on experiments on a much larger set of 500 examples, and features a second case study.

Conclusion

In hardware design, synchronous techniques have been predominating, but they face problems when implementing the global clock; asynchronous circuits and architectures are a promising approach to avoid these problems. A major issue is that asynchronous design is more complex than synchronous design, due to interleavings of concurrent processes. Thus, ensuring the correctness of asynchronous designs as early as possible is essential to avoid the cost of synthesising erroneous circuits. However, contrary to synchronous design, there does not yet exist an established methodology for the verification of asynchronous designs.

In this article, we proposed a formal semantics for the hardware process calculus Chp, including valuepassing communication, ports open to the environment, and probe operations. Moreover, our semantics is independent of any particular (2-or 4-phase) handshake protocol expansion used for circuit implementation. This semantics has been approved by our colleagues from Cea/Leti and the developers of the Tast tool. Based on this semantics, we formalised a translation of Chp into the international standard Lotos and implemented this translation in the Chp2Lotos tool, which has been validated on many examples.

Our work prefigures a framework for the design of asynchronous circuits and architectures, enabling asynchronous designs to be specified using Chp, then translated into Lotos, verified using the Cadp model checking and equivalence checking tools, and finally synthesised using the Tast tool. This tool chain has been applied successfully to two industrial asynchronous circuits and is being used for validating other parts of the Anoc architecture.

Fig. 3 .

 3 Fig. 3. Lts for the arbiter with priorities -minimised with respect to branching bisimulation

Fig. 4 .

 4 Fig. 4. Petri net for the arbiter in Example 3

  c2l b ("c ?x; B", H, D, U, ∆) = c ?x : s; c2l b (B, H, D ∪ {x}, U, ∆ ∪ {x}) -An active reception -when H(c) = active -additionally requires to initiate the communication on the channel c: c2l b ("c ?x; B", H, D, U, ∆) = c init ; c ?x : s; c2l b (B, H, D ∪ {x}, U, ∆ ∪ {x})

Fig. 6 .

 6 Fig. 6. Translation steps in Chp2Lotos

  Overview of the CHP to LOTOS TranslationWe highlight first the main features of the translation of Chp into Lotos: -Each Chp type (booleans, natural numbers, bit vectors, etc.) is translated into a Lotos sort (i.e. algebraic data types). -Each Chp operation is translated into a Lotos operation, which is implemented either using Lotos algebraic equations or directly by C code (as Cadp allows to import hand-written C code). -Each Chp channel c is translated into a Lotos gate with the same name c together with, in case c is probed, a Lotos process to handle variable x c . -Each Chp variable x is translated into one or more Lotos variables (i.e. value identifiers in the Lotos standard terminology) with the same name and the same type as x. Several Lotos variables might be required, since Lotos processes follow the functional paradigm in which a variable can be assigned only once (whereas Chp variables can be assigned several times).

Lotos allow to exchange several values -called offers -at the same time. The behaviour "choice x 0 : s 0 , . . . , x n : s n [] B" assigns to each variable x i a nondeterministically chosen value in the domain of sort s i , and then behaves as B. The so-called functionality of a Lotos process P is "noexit" if P never terminates, or "exit(s 1 , . . . , s n )" if P may terminate and return a possibly empty set of values of sorts s 1 , . . . , s n .

The definition of a Lotos process P involves a list of formal gates g 1 , . . . , g m , a list of formal parameters x 1 , . . . , x n of sort s 1 , . . . , s n , a functionality F , a behaviour B, and possibly other process definitions d 1 , . . . , d p :

process P [g 1 , . . . , g m ](x 1 : s 0 , . . . , x n : s n ) : F := B where d 1 , . . . , d p endproc 4.2.

  If channel c links a passive emitter to an active receiver, the translation is slightly simpler, as one can remove the parameter x of channel c comm since the value exchanged on c does not need to be stored:

	[]
	probe enable; (
	c probe !true; probe disable; channel c comm[probe enable, probe disable, c, c init , c probe]
	[]
	probe disable; channel c comm[probe enable, probe disable , c, c init , c probe] )
	endproc
	endproc

probe] : noexit := c init ?x : s; channel c comm[probe enable, probe disable, c, c init , c probe](x) [] probe enable; ( c probe !false !⊥; probe disable; channel c[probe enable, probe disable, c, c init , c probe] [] probe disable; channel c[probe enable, probe disable, c, c init , c probe] ) where process channel c comm[probe enable, probe disable, c, c init , c probe](x : s) : noexit := c !x; channel c[probe enable, probe disable, c, c init , c probe] [] probe enable; ( c probe !true !x; probe disable; channel c comm[probe enable, probe disable, c, c init , c probe](x) [] probe disable; channel c comm[probe enable, probe disable, c, c init , c probe](x) ) endproc endproc • process channel c[probe enable, probe disable, c, c init , c probe] : noexit := c init ; channel c comm[probe enable, probe disable, c, c init , c probe] [] probe enable; ( c probe !false; probe disable ; channel c[probe enable, probe disable, c, c init , c probe] [] probe disable; channel c[probe enable, probe disable, c, c init , c probe] ) where process channel c comm[probe enable, probe disable, c, c init , c probe]: noexit := c ?x : s; channel c[probe enable, probe disable, c, c init , c probe]

  c 2 init ] endproc process arbiter [probe enable, probe disable, c, c 1 , c 1 probe, c 2 , c 2 probe] : noexit := probe enable; c 1 probe ?x c1 : bool ?x c1 : bool ; c 2 probe ?x c2 : bool ; ( [x c1 ] -> probe disable; (c !1; exit) ||| (c 1 ?x; exit) >> arbiter [probe enable, probe disable, c, c 1 , c 1 probe, c 2 , c 2 probe]

The deadlocking process "nil" is not present in the version of Chp implemented in Tast[START_REF] Renaudin | TAST Compiler and TAST CHP Language[END_REF], but is required in Section 3 for a proper definition of the operational semantics.

Chp has no hiding or restriction operator; thus, all inputs and outputs are observable.

This is generally not the case in standard process calculi, in which an assignment to a local variable does not create an internal action, all actions being created by input/output communications.

Strong equivalence (or strong bisimulation)[START_REF] Milner | A Calculus of Communicating Systems[END_REF] treats τ -transitions like visible transitions.

Acknowledgements.

We are grateful to our colleagues Edith Beigné, François Bertrand, Yvain Thonnart, and Pascal Vivet (from Cea/Leti laboratory), as well as Marc Renaudin, Dominique Borrione, and Menouer Boubekeur (from Tima laboratory) for interesting discussions on Chp and Tast, in particular their explanations regarding the probe operation. We also thank the same colleagues from Cea/Leti laboratory for their cooperation in the Des and Anoc case studies.

Remark. The translation into Lotos exploits the similarity of the Chp operator "," with the Lotos operator " ||| ", the only difference being that the translation into Lotos introduces a synchronisation on the special termination gate, noted "δ", in order to express the synchronous termination of B 1 and B 2 . Because the preliminary simplifications (Section 4.4) always introduce a final "nil" wherever a process terminates (i.e. " Bi " is replaced by " Bi ; nil" when ¬inf ( Bi )), such δ-transitions always occur on the lefthand side of a Lotos ">>" sequential composition operator. Therefore, these δ-transitions are captured by the ">>" operator, which transforms them into τ -transitions, thus making them confluent (see the remark for sequential compositions).

2

Translation of Guards. If a guard V is of the form "c #" or "c #V ′ ", where channel c is of profile "single", then V is translated as a communication on the Lotos gate c with a "!Probe" offer. Otherwise, V is translated directly into a Lotos guard:

where x is a new variable (to receive the value of x c ) and the predicate cond (V ) is defined by

Remark. Compared to the Chp operational semantics, the translation into Lotos adds, in the case where profile(c) = single, a communication that -after hiding -corresponds to the τ -transition generated by the first rule for guarded commands in the Chp operational semantics (see Section 3 and the translation of guarded commands below). 2

Translation of Guarded Commands.

is translated into a call to an auxiliary process P B :

and where

i.e. {x i1 , . . . , x i k } ⊆ {x 1 , . . . , x m }, (∀j ∈ {1, . . . , m}) s j = type(x j ), and (∀j ∈ {i 1 , . . . , i k }) x j ∈ D. The "choice x i1 : s i1 , . . . , x i k : s i k " is used to assign nondeterministically chosen values to the variables x i1 , ..., x i k , which might be read when executing P B , but are not defined before the first call to P B . This is required, since Chp allows uninitialised variables to be read, whereas Lotos prohibits this using syntactic restrictions, which are too restrictive in some cases, as for instance the initialisation of a variable in the last iteration of a loop. If k = 0, the (empty) "choice" statement should be omitted. The semantics of a guarded command "@[V 0 ⇒ B 0 ; T 0 . . . V n ⇒ B n ; T n ]" requires to check all guards simultaneously. Thus, P B starts by reading the values of the variables x c for all channels that have profile "general " and are probed by some guard V j (j ∈ {0, . . . , n}). Formally, this set of channels is defined as

Then, P B offers the possibility to execute any branch B i ; T i the guard V i of which is true. An additional branch handles the case where all the guards containing a probe of channel of profile "general" are false: in 4.7. Optimisations of the Generated LOTOS Code

In addition to the aforementioned code specialisation technique (i.e. different translations of a channel depending on the profile), several other optimisations are possible.

-A Chp guard that is always true can be dismissed in the corresponding Lotos specification.

-Boolean expressions in Lotos guards could be simplified using standard techniques (boolean algebra or Bdd). -The "accept" construct needs to be generated only if some variable values must be transmitted over a sequential composition >> (see translation of the loop construct in Translation of Guarded Commands, Section 4.5 as an example). -If a guarded command is the left hand side of a sequential composition "@[ . . . ]; B ′ ", we generate a second auxiliary process P B ′ (for B ′ ); each "break" is translated into a call to P B ′ and the functionality F is computed with respect to B ′ . This optimisation avoids the introduction of a τ -transition due to the "exit" (generated by the translation of "break"). For each B i such that inf (B i ), T i is not translated at all. -In the definition of query probe(V 0 , ..., V 1 ), if the set of channels of profile "general " probed by V 0 , ..., V n is empty, the synchronisations on gates probe enable and probe disable are not required. -If none of the guards of a guarded commands probes a channel of profile "general", the synchronisation on gate probe enable is unnecessary and can be removed. In this case, to match the τ -transition generated by the Chp operational semantics, the synchronisation on gate probe disable must be replaced by a τ . Such optimisations have been implemented in the translator we will present in Section 5.

Example of the Arbiter without Priorities

For the arbiter without priorities of Section 2.6, profile(c) = unprobed (because c is never probed) and profile(c 1 ) = profile(c 2 ) = single (because any probe operation on c 1 and c 2 is a guard). The Lotos behaviour obtained by applying the translation rules of Section 4.6 is the following:

Processes client -1, client -2, and arbiter are defined as:

Processes client -1 (respectively client -2) repeat forever the auxiliary process channel c 1 (respectively channel c 2 ), followed by a recursive call (the Chp loop construct being translated into a recursive Lotos process call, see Translation of Guarded Commands, Section 4.5). Both processes channel c 1 and channel c 2 are obtained as described in Section 4.5 (translation of "c!V ", "single" case). As regards the process arbiter, Chp guarded commands are translated to a Lotos choice ([]). Guards consisting of a single probe are