Keywords: Algèbre de processus, architecture dirigée par les modèles calcul de processus, ingénierie dirigée par les modèles, méthode formelle, modélisation, sémantique du parallélisme, spécification, spécification formelle, système concurrent, système critique, validation, vérification

Réflexions sur le futur de la sémantique du parallélisme en général et des calculs de processus en particulier

Résumé :

Dans ce rapport, nous examinons la situation actuelle de la sémantique du parallélisme vis-à-vis de son impact industriel. Cet examen est à la fois rétrospectif et prospectif, et il englobe naturellement les calculs de processus, qui sont un vecteur majeur pour la dissémination des concepts de la sémantique du parallélisme. En considérant les succès, mais aussi les échecs, nous essyons d'identifier les causes qui, jusqu'ici, on empêché une dissémination plus large des calculs de processus. Ceci suggère une nouvelle génération de langages de spécification formelle qui combineraient les caractéristiques parallèles des calculs de processus avec les concepts usuels présents dans les langages algorithmiques. Finalement, nous soulignons deux évolutions majeures dans les industries du logiciel et du matériel qui ouvrent de nouveaux domaines d'application pour les recherches en sémantique du parallélisme.

Introduction

This report was inspired by two challenging questions raised during two scientific meetings held in 2006:

The first question was asked in Grenoble during an evaluation meeting of the author's research team. In essence, the question was the following: "Why are you trying to compile process calculi? Process calculi are formalisms to study theoretical aspects of concurrency, not programming languages to describe real-life systems".

The second question was asked in Palaiseau during the LIX Colloquium on Emerging Trends in Concurrency Theory. The question was very direct, if not provocative given the number of prestigious attendees in the audience: "Other fields of computer science have found useful applications in industry. Does concurrency theory have similar achievements? What are your success stories? Where are your victories? ".

Apparently antagonistic, both questions address in fact the very nature of concurrency theory, its applicability, as well as the status and impact of process calculi, which are a major -if not the prime -vector for the dissemination of concurrency theory results. All these points deserve a scientific discussion, and this is what the present report is about.

It is organized as follows. Section 2 recalls some important, yet partial, achievements of concurrency theory in general, and process calculi in particular. Section 3 discusses three main issues that often prevent process calculi from being widely used in industry. Section 4 mentions two important evolutions affecting the software and hardware industries, and discusses how these evolutions provide new opportunities to concurrency theory. Finally, Section 5 gives a few concluding remarks.

Impact of Concurrency Theory: Achievements

Concurrency theory is a field of computer science that has been producing many deep, fundamental results. As a tentative classification, we can mention: Models to represent the behaviour of concurrent systems: Petri nets, Labelled Transition Systems, Kripke structures, event structures, bigraphs, etc., Formalisms to specify concurrent systems at a higher abstraction level: process calculi, computer languages derived from process calculi, µ-calculus, etc., Semantics such as Structured Operational Semantics (Sos), algebraic laws, bisimulation relations, congruence properties, etc., Algorithms to compile, execute, and verify concurrent systems expressed using models and/or formalisms, Tools that implement (a significant subset of) the above results.

In this respect, the two questions quoted in the introduction sound like a reminiscence of the recurrent debate pure mathematics vs applied mathematics. Same as for pure mathematics (illustrated by the Bourbaki group), it exists a pure concurrency theory school, sometimes driven more by the abstract beauty of theoretical results than by their practical usefulness. But, as for applied mathematics (illustrated by J.J. Lions and colleagues), it also exists an applied concurrency theory community, that takes its inspiration from real-world problems.

From the beginning, concurrency theory has been rooted in concrete examples. It appeared at the end of the 60's as an attempt to understand problems in multiprocessor and timesharing systems. In the 80's, these motivations were still there; for instance, Milner's book on

H. Garavel

Ccs [START_REF] Milner | A Calculus of Communicating Systems[END_REF] was illustrated by a process scheduler that served as a running example; also, the Iso international standard Lotos [START_REF] Iso/Iec | LOTOS -A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour[END_REF] was designed to specify communication protocols and services formally.

A good argument supporting the "applicability" of concurrency theory is the impressive number of software tools developed during the past decades, such as Cadp [START_REF] Garavel | CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF], the Concurrency Workbench [START_REF] Cleaveland | The Concurrency Workbench[END_REF][START_REF] Stevens | The Edinburgh Concurrency Workbench (Version 7.1)[END_REF] and its American descendants [START_REF] Cleaveland | The Concurrency Factory: A Development Environment for Concurrent Systems[END_REF][START_REF] Cleaveland | The Concurrency Workbench of the New Century (Version 1.2). User's manual[END_REF], Fdr2 [START_REF]Failure-Divergence Refinement[END_REF], Fsp [START_REF] Magee | Concurrency: State Models and Java Programs[END_REF], Loewe [START_REF] Karjoth | LOEWE: A LOTOS Engineering Workbench[END_REF], the Lotosphere toolset [START_REF] Bolognesi | LOTOSphere: Software Development with LOTOS[END_REF], the µCrl toolset [START_REF] Dams | Specification and Implementation of Components of a µCRL Toolbox[END_REF][START_REF] Wouters | Manual for the muCRL Tool Set (Version 2.8.2)[END_REF], to mention only a few.

These tools have been used to model and analyze numerous real-life systems. In many cases, they allowed to discover interesting -sometimes, unexpected -properties, thus leading to better understood, more reliable systems. Taking the example of the Cadp toolbox, which we will use as a guiding thread throughout this report, there are nearly one hundred case-studies performed using Cadp and companion tools1 .

When dealing with real-life systems, concurrency theory has clearly won some battles. The progresses might have been slow, but they have been real. This can be seen, for instance, by considering the evolving complexity of the problems tackled using Cadp; over the years, the enhancements brought to this toolbox allowed to push away the state explosion limitations, thus allowing to study more complex systems, as well as systems modelled in finer detail:

In the 80's, one could analyze systems with less than 100 lines of Lotos.

In the 90's, one could analyze systems with less than 1,000 lines of Lotos.

In the 2000's, one can analyze systems with less than 10,000 lines of Lotos.

As part of the most recent case-studies -and because the question of "success stories" for concurrency theory was asked explicitly during the LIX Colloquium on Emerging Trends in Concurrency Theory -we should mention the FormalFame project2 between Bull and Inria, in which crucial parts of the Fame multiprocessor architecture used in Bull's NovaScale high-end servers and Tera10 machine (one of Europe's most powerful supercomputers) have been modelled using Lotos and verified using Cadp.

More generally, there are many research teams -especially in Europe -that are also applying theoretical concurrency to industrial problems. Based on the experience acquired in many casestudies, the typical methodology can be described by the three following steps:

1. Find a company that designs concurrent systems with a strong need for reliability. This step is rather easy, as there are more such companies than research teams in concurrency theory. Typical application areas are communication protocols, distributed systems, hardware architectures, embedded systems, security protocols, etc.

2. Select a concrete system under design by this company, model the salient parts of it formally using your favourite process calculus, and analyze this system using software tools for rapid prototyping, testing, verification, performance evaluation, etc.

Such a collaboration with industry can be done in two ways. The modelling task can be done by computer scientists within academia (we call this the Dutch style, as this seems to be the usual approach for our colleagues working in Amsterdam, Eindhoven, Twente, etc.), or it can be done within the company itself (we call this the French style, as the author's research team prefers this type of collaboration).

Both styles have their respective merits. The Dutch style ("We model it for you") is easier when starting collaborations; it relieves the company from learning a process calculus and how to use the associated tools; it allows a fast and proper modelling, as computer scientists usually avoid the mistakes and delays typically observed with novice specifiers lacking experience in formal methods. On the contrary, the French style ("Learn and model it yourself ") is more demanding from the industrial partner, as it requires industry engineers to learn about process calculi. However, it has three advantages: the company can keep its confidential designs internally; computer scientists can focus on long-term research issues rather than spending their time investigating one particular industrial system; the collaboration, if successful, is likely to be pursued once the company has acquired a sufficient insight in formal methods.

3.

Reuse the feedback obtained from studying this real-life system to improve languages, algorithms, and tools, or even to start a new line of research. Such a virtuous confrontation to real-world problems characterizes the applied concurrency approach. For instance, this drove the Cadp developers into inventing new concepts of practical interest, such as efficient compiling algorithms for process calculi [START_REF] Garavel | Compilation et vérification de programmes LOTOS[END_REF][START_REF] Garavel | State Space Reduction for Process Algebra Specifications[END_REF], µ-calculus formulas extended with data [START_REF] Mateescu | Vérification des propriétés temporelles des programmes parallèles[END_REF][START_REF] Mateescu | Local Model-Checking of an Alternation-Free Value-Based Modal Mu-Calculus[END_REF], parameterized boolean equation systems [START_REF] Mateescu | Vérification des propriétés temporelles des programmes parallèles[END_REF][START_REF] Mateescu | Local Model-Checking of an Alternation-Free Value-Based Modal Mu-Calculus[END_REF], generic programming interfaces for on-the-fly verification [START_REF] Garavel | OPEN/CAESAR: An Open Software Architecture for Verification, Simulation, and Testing[END_REF], scripting languages for compositional verification [START_REF] Garavel | SVL: a Scripting Language for Compositional Verification[END_REF], real-time monitoring for distributed state-space generation [START_REF] Garavel | DISTRIBUTOR and BCG MERGE: Tools for Distributed Explicit State Space Generation[END_REF], etc.

3 Impact of Concurrency Theory: Some Failures So far, in spite of the achievements evoked in Section 2, the impact of concurrency theory has not been as strong as other fields of computer science. Concretely, most software engineers are not aware of the results brought by concurrency theory, and no mainstream language for specification or programming is based on the ideas behind process calculi.

For instance, the community working on object-oriented languages was more successful in spreading its ideas to a larger audience. Today, several mainstream programming languages (such as Java, C++, and C#) are based on the concepts developed by this community. Similarly, the community working on so-called "semi-formal" (actually, informal) methods was more successful in promoting formalisms such as Uml, Aadl, SysMl, etc.

There are at least two factors that prevent a wide dissemination of concurrency theory:

A first factor is certainly the mathematical style found in most concurrency theory articles and textbooks. Mathematical notations are certainly needed to deal with involved semantic points, but their usage beyond necessity should be avoided, not to create an entry barrier for newcomers.

A second factor is the central role played by process calculi. They are required to model systems formally, and to apply many results of concurrency theory (such as congruence results that allow a complex system to be verified compositionally using a "divide and conquer" approach). However, process calculi are not easily accepted by industry, for at least three main reasons, which we discuss hereafter.

Issue 1: Fragmentation

A first obstacle to the dissemination of process calculi is the existence of several calculi, similar in their principles but incompatible in their details. This creates confusion for industrial users, who are unsure about which language to adopt.

This fragmentation issue was recognized as soon as the mid 80's when a Iso standardization committee led by Ed Brinksma undertook the design of Lotos by merging the best features of Ccs [START_REF] Milner | A Calculus of Communicating Systems[END_REF][START_REF] Milner | Communication and Concurrency[END_REF], Csp [START_REF] Hoare | Communicating Sequential Processes[END_REF][START_REF] Brookes | A Theory of Communicating Sequential Processes[END_REF], and Circal [START_REF] Milne | CIRCAL and the Representation of Communication, Concurrency, and Time[END_REF] into a unique language. Although the standardization of Lotos in 1989 provided a foundation for ambitious research projects (such as the European projects Sedos, Lotosphere, Specs, Eucalyptus, etc.), Lotos failed to supersede or otherwise replace preexisting process calculi.

H. Garavel

In the United Kingdom, for instance, the Ccs and Csp communities continued working with their favourite calculi. It is worth noticing, however, that (according to the publications) the definition of Csp gradually evolved to become quite similar to Lotos, at least for the untimed aspects (see e.g. [START_REF] Davies | A Brief History of Timed CS[END_REF]), still with slightly different notations. Additionally, the principles of Csp gave birth to new languages such as Fdr2 and Occam [START_REF] Inmos | OCCAM 2.1 Reference Manual[END_REF] supported by compilers and verification tools.

Also, Lotos was never recognized as a standard in the Netherlands, except in Twente. Alternative languages -similar to Lotos but incompatible with it -were launched several years after the Lotos standard was issued, e.g. Psf [START_REF] Mauw | A Process Specification Formalism[END_REF] or µCrl [START_REF] Groote | The Syntax and Semantics of µCRL[END_REF].

This phenomenon is by no means specific to the concurrency theory community: a similar fragmentation occurred for almost every computer language. Another reason behind fragmentation is the fact that the usage of formal methods in industry is essentially a service activity; as such, it obeys a proximity criterion, meaning that an industrial company using formal methods will naturally co-operate with academic experts located in its neighbourhood. For this reason, English companies tend to use Csp, Dutch companies tend to use µCrl, French companies working with Inria tend to use Lotos, etc.

From an economical point of view, such a market fragmentation into "national" language communities is probably not optimal given the high costs of training and tool development.

On the long term, one unique language (or a few languages only) will probably emerge. On the short term, remedies against fragmentation can be taken, namely:

Source-to-source translators between different process calculi: for instance, the Vasy team of Inria is studying translators from Chp to Lotos [START_REF] Salaün | Translating Hardware Process Algebras into Standard Process Algebras -Illustration with CHP and LOTOS[END_REF], from Fsp [START_REF] Salaün | Translating FSP into LOTOS and Networks of Automata[END_REF] to Lotos, and from Fdr2 to Lotos; these translators aim at reusing for Chp, Fsp, and Fdr2 the verification functionalities of the Cadp toolbox [START_REF] Garavel | CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF] that was initially developed for Lotos.

Software gateways between different tool environments: for instance, the Sen2 team of Cwi and the Vasy team of Inria have developed connections between Cadp and the µCrl toolset, thus allowing to use the Cadp model checkers on µCrl specifications, as well as applying the µCrl minimizers to labelled transition systems generated from Lotos specifications.

Issue 2: Lack of Expressiveness

The "classical" process calculi (namely Lotos, Csp/Fdr2, and µCrl) allow to describe concurrent processes with complex data structures. Experience gained from numerous case-studies indicates that these calculi are sufficiently expressive for many industrial problems. However, there are certain classes of problems for which a greater expressiveness is needed:

1. Real-time aspects: The behaviour of certain systems depends not only on their interactions with their environment, but also on the quantitative amount of elapsed time. To model such systems adequately, several "timed" process calculi have been proposed, in addition to timed automata, timed Petri nets, etc.

Performance aspects:

For certain systems, one needs to model not only the functional behaviour, but also quantitative aspects, such as probabilities, rates, or throughputs of certain events. For this purpose, "probabilistic" and "stochastic" process calculi have been proposed, e.g. [START_REF] Bernardo | A Tutorial on EMPA: A Theory of Concurrent Processes with Nondeterminism, Priorities, Probabilities and Time[END_REF][START_REF] Bernardo | Corrigendum to "A Tutorial on EMPA: A Theory of Concurrent Processes with Nondeterminism, Priorities, Probabilities and Time[END_REF][START_REF] Hillston | Process Algebras for Quantitative Analysis[END_REF][START_REF] Hinton | PRISM: A Tool for Automatic Verification of Probabilistic Systems[END_REF], as well as means to reuse and extend "classical" process calculi for performance evaluation, e.g. [START_REF] Hermanns | Interactive Markov Chains and the Quest for Quantified Quality[END_REF][START_REF] Garavel | On Combining Functional Verification and Performance Evaluation using CADP[END_REF].

Mobility aspects:

There are systems in which concurrent processes and communication links between processes cannot be determined statically, but evolve dynamically. All the aforementioned "classical" process calculi offer some form of dynamicity, since they allow concurrent processes to be started and terminated dynamically (this is usually achieved by using recursion through parallel composition operators). As regards communication links, these calculi support value-passing communications as well as n-ary synchronization (broadcast) between processes. However, communication links between processes remain fixed statically.

A simple extension was proposed in [START_REF] Garavel | A Graphical Parallel Composition Operator for Process Algebras[END_REF], which suggests the introduction of an "n among m" parallel composition operator. This operator allows the dynamic creation or deletion of communication links between processes, simply by exchanging data values (e.g., integers) within a pool of concurrent processes. For instance, [START_REF] Garavel | A Graphical Parallel Composition Operator for Process Algebras[END_REF] shows how a "server" process and a "client" process can discover each other's existence dynamically and establish communication with the initial help of a "trader" process. A key point of this approach is that it remains compatible with model-checking verification tools based on finite state space enumeration.

A fundamental step forward was made with the introduction of "mobile" calculi (such as the π-calculus [START_REF] Milner | A calculus of mobile processes I[END_REF][START_REF] Milner | A calculus of mobile processes II[END_REF][START_REF] Sangiorgi | The π-calculus: a Theory of Mobile Processes[END_REF], the join calculus [START_REF] Fournet | The reflexive CHAM and the join-calculus[END_REF][START_REF] Fournet | The Join-Calculus Language -Release 1.05. Documentation and User's Manual[END_REF], etc.), which allow processes and channel names to move from one location to another. This further evolved with the even more general model of bigraphs [START_REF] Milner | Bigraphs as a Model for Mobile Interaction[END_REF]. These approaches bring full mobility, at the expense of introducing higher-order features that make state spaces potentially infinite. For this reason, verification of mobile calculi specifications often relies on theorem proving, as finite state model checking is not an option.

Considering the variety of case-studies tackled using different formalisms, it is clear that timed extensions have useful results for scheduling, that stochastic extensions are useful for performance and dependability studies, and that mobility extensions are useful to model evolving systems such as business processes. At the same time, given the number of industrial problems that do not require such extensions, it is clear that research on enhancements to "classical" process calculi remains an important research topic that should not be neglected.

Issue 3: Lack of User-Friendliness

If expressiveness is not so much an issue in many cases, user-friendliness is a major concern. It is generally admitted that the dissemination of process calculi is limited by their steep learning curve, which is mostly due to the fact that process calculi are significantly different from mainstream programming languages. This is a key problem in the aforementioned "Learn and model it yourself " approach. Formal specification is a time-consuming activity and industry lacks experts trained to formal methods.

The lack of user-friendliness, which greatly hampers the dissemination of process calculi, is the result of unappropriate technical decisions. Although process calculi were a scientific breakthrough, their design was not free from mistakes. We briefly evoke two main mistakes, which are directly related to the two questions raised in the introduction of the present report.

1. There is a frequent confusion between a calculus and a language. A calculus is a minimal language intended to the theoretical study of concurrency; it should have a minimal number of primitive constructs (following Occam's razor principle) to reduce the length of induction proofs.

To the contrary, a computer language is intended to specify real, complex systems. Such a language does not need to be minimal as a primary goal; instead, it should satisfy good properties, such as readability, which may require to add extra keywords in the syntax, and conciseness, which may require to enrich the language with non-primitive constructs for handling common situations.

H. Garavel

There have been many attempts to use a calculus in place of a language3 . This is clearly a mistake, since a programming language must be accepted by software and system programmers as a daily working tool.

2. There is another design mistake, which we could call the total algebra ideology. In this school of thinking, every language feature must be algebraical: a concurrent language is an algebra; a concurrent program is an algebraic term; the semantics of process operators is defined by algebraic laws; data values handled by concurrent programs are algebraic terms; functions to handle data values are defined by user-specified algebraic equations; etc.

Such a language might be appealing to some mathematicians but, considering the history of computing, it seems that the mass of software programmers tend to reject algebraical languages. In that respect, all attempts to reduce computer languages to algebra have failed with a remarkable consistency.

For instance, the Apl language [START_REF] Iverson | Notation as a Tool of Thought[END_REF], despite an initial sucess, steadily declined since 1980, surviving only in a tiny community. Interestingly, Apl concepts had little impact, contrary to its competitors Fortran and Algol, most features of which have been retained in modern programming languages.

The same could be said of algebraic data types and equational specifications, the popularity of which has gradually decreased after an early period of high scientific interest. Algebraic data types may still exist in some specification languages (process calculi such as Lotos and µCrl, of course, but also languages used in theorem provers) but they tend to be gradually supplanted by functional languages (as in Fdr2, for instance).

A simple example illustrates the practical consequences of these two mistakes. It is interesting to observe how process calculi answer the need for conditionals. Most process calculi do not provide the classical "if-then-else" construct; instead, they use guard operators, such as, in Ccs and Lotos, "[V ] → B", which expresses that behaviour B can only be executed if condition V is true, or, in Acp and µCrl, "B 1 ⊳ V ⊲ B 2 ", which expresses that, if condition V is true then behaviour B 1 is executed or else behaviour B 2 is executed. These various guard operators have an algebraic syntax -they can be seen as unary or binary operators over processes -and a minimal semantics -only one or two Sos rules. However, they are inadequate in practice, since the Ccs/Lotos solution requires two occurrences of V to express a trivial "if V then B 1 else B 2 " conditional, while the Acp/µCrl solution forces a counterintuitive ordering of V 's and B's when expressing nested conditionals such as "(

B 1 ⊳ V 2 ⊲ B 2 )⊳ V 1 ⊲ B 3 ".
We believe that the correct solution would be to have standard, properly bracketed conditionals of the form: if...then...[elsif...then...] * ...else...endif even at the expense of having a non-algebraic syntax and more Sos rules (see [START_REF] Garavel | A Wish List for the Behaviour Part of E-LOTOS[END_REF][START_REF] Garavel | NTIF: A General Symbolic Model for Communicating Sequential Processes with Data[END_REF] for a discussion).

The conclusion is clear: standard programming constructs ("if-then-else" and "case" conditionals, "for" and "while" loops, etc.) exist by themselves and should not be reduced to algebra. In essence, seeking for a minimal semantics and/or an algebraic flavour does not lead to optimal design choices. The shape of a concurrent language (i.e., the language constructs presented to end-users) should be based first on ergonomy considerations, following the lessons learnt from the history of computer languages.

Two Opportunities for Concurrency Theory

Away from the past, the context of computer science is changing rapidly, and its recent evolutions offer two new opportunities to revive the interest in concurrency theory.

Opportunity 1: Models Everywhere

From the beginning, concurrency theory has been based on models, i.e., descriptions of realworld systems, which are simplified4 to retain only those aspects pertinent to the study of concurrency. Quite early, these models have been made formal, especially with the advent of process calculi.

Although the concept of model is widely used in many branches of science and engineering (e.g., physics, biology, civil engineering, etc.), formal models of concurrency have been so far confined to specific topics (formal methods, model-checking) with little impact on computer science in general.

This situation is about to change, as other computer science communities (software engineering, distributed systems, object-oriented languages, etc.) also recognized the benefits of modelling for software and systems development, and started to promote it actively. This led to the design of Uml (Unified Modelling Language), followed by the Mda (Model Driven Architecture) and Mde (Model Driven Engineering) methodologies for software development. These methodologies lay the emphasis on models (real-world system abstractions seen as first-class entities) and transformations between models (which unifies several pre-existing concepts, such as translation and refinement). Compared to the approaches developed by the concurrency theory community, these methodologies exhibit three main differences:

1. The Mda/Mde specification languages are mostly graphical, based on the underlying assumption that graphical languages are more easily accepted by industry. On the contrary, process calculi (but a few exceptions) have a textual syntax, as this was deemed to be sufficient for the study of concurrency.

2. The Mda/Mde specification languages can be domain specific in the sense that each application domain can define (or customize) its own language to fit its own needs. To the contrary, concurrency theory seeks for generality and is independent from any particular application area, in the same way as linear algebra is the same for, e.g., both automotive and aerospace industries. Similarly, behind each process calculus (except a few calculi, such Circal and Chp [START_REF] Martin | Compiling Communicating Processes into Delay-Insensitive VLSI Circuits[END_REF][START_REF] Renaudin | TAST Compiler and TAST-CHP Language -Version 0[END_REF], which explicitly target at hardware circuits), there was an implicit motivation that this calculus should be general-purpose and expressive enough to model concurrent systems of various domains.

3. The Mda/Mde specification languages are informal (or semi-formal, which is not very different). For these languages, only the syntax is defined formally (using the notions of "meta-metamodel", "metamodel" and "model" which reformulate, in a graphical setting, the well-known concepts of Bnf grammar, language, and program, respectively). There is little semantics in the Mda/Mde methodologies. Static semantics constraints (such as identifier binding and type checking) are expressed using semi-formal languages such as Ocl (Object Constraint Language), which are not intended to allow computer-aided analysis. Dynamic semantics is totally ignored, in a sharp contrast with process calculi, for which dynamic semantics is the central topic, while syntax and static semantics aspects are kept to the minimum.

This suggests that the Mda/Mde methodologies could be enhanced by results from the concurrency theory, e.g., operational semantics, axiomatic semantics, behavioural typing, etc.

H. Garavel

Opportunity 2: Asynchrony Everywhere

Because concurrency is a difficult matter, its usage has been often limited to a few specific areas of computing, such as multi-user operating systems, databases, scientific computing, networking, and multiprocessor architectures. Today, the list of those areas is in expansion because of the global connectivity brought by the Internet (most machines and embedded devices are now interconnected), which opens new usages, such as Web services, mobility applications, etc.

At the same time, another major revolution is taking place on the front of multiprocessors.

For long, hardware design has been mostly "synchronous", meaning that all parts of a circuit would be synchronized by one single, central clock. In concurrency theory, this concept gave birth to synchronous process calculi, such as Sccs and Esterel.

There are good reasons for synchronous designs: synchrony is easier to master than asynchrony (thus making it easier to design correct circuits); it enforces determinism (thus enabling nonregression testing); it is well-supported by industrial computer-aided design tools.

The synchronous paradigm has been very successful: it allowed to improve the performance of microprocessors by increasing regularly clock frequencies, thus enforcing Moore's law.

At the same time, there have been some attempts to build "asynchronous" circuits using a different paradigm (absence of central clock). Even when successful, these attempts remained marginal compared to the wide success of the synchronous paradigm. The situation is changing, due to several factors:

The reduction of energy consumption is a key issue for the autonomy of embedded systems. As the silicon surface of circuits increases, the electric consumption increases too, and it is common that 50% or more of the energy is used only to propagate the global clock in every part of the circuit. Also, the regularity of synchronous designs makes them vulnerable to spying (e.g., by observation of their electromagnetic emissions), which is a drawback for secure applications such as cryptography. For these reasons, the synchronous design paradigm is being questioned, and there is a growing interest in asynchronous logic for circuit design [START_REF] Hauck | Asynchronous Design Methodologies: An Overview[END_REF][START_REF] Davis | An Introduction to Asynchronous Circuit Design[END_REF][START_REF] Spars | Principles of Asynchronous Circuit Design: A Systems Perspective[END_REF]. However, asynchronous logic is more error-prone than synchronous logic (with a higher risk of deadlocks for instance), thus giving a crucial role to functional verification. In this respect, process calculi and model checking tools can greatly contribute to the design of correct asynchronous circuits, e.g. [START_REF] Yoneda | Verification of Asynchronous Logic Circuit Design using Process Algebra[END_REF][START_REF] Wang | Opportunities and Challenges in Process-Algebraic Verification of Asynchronous Circuit Designs[END_REF][START_REF] Salaün | Formal Verification of CHP Specifications with CADP -Illustration on an Asynchronous Network-on-Chip[END_REF].

At a higher level, computer architectures are evolving to allow reductions in silicon surface and cost. Many circuits (such as arithmetic co-processors, digital signal processors, etc.) that used to be external to the microprocessor (i.e., on the motherboard) are now internal. The hardware buses themselves are moving from the outside to the inside of the microprocessor. Therefore, it is no longer efficient, nor even feasible, to have a unique clock to synchronize all these various hardware subsystems produced separately by different companies. Given that these subsystems are still designed under the sychronous paradigm, the least that must be done is to allow them to work asynchronously according to the Gals (Globally Asynchronous, Locally Synchronous) paradigm [START_REF] Daniel | Globally-Asynchronous Locally-Synchronous Systems[END_REF]. Again, languages and tools derived from concurrency theory can help to study such architectures, e.g. [START_REF] Baulch | Analyzing and Verifying Locally Clocked Circuits with the Concurrency Workbench[END_REF].

As regards microprocessors, the limits of Moore's law are about to be reached. Due to physical/electrical barriers, it will be no longer possible to increase the frequencies of processor clocks as before. The only solution found by hardware makers to continue delivering better performance is provide several processing units (called "cores") inside the same microprocessor. Thus, the competition between microprocessors will no longer be expressed in terms of clock frequencies, but in the number of cores (currently, 2, 4, or 8, and this number is expected to grow rapidly).

This should be a turning point in software development too. Because of the upper limit on clock frequencies, sequential programs will not run faster on multi-core processors than they run today on single-core processors (they might even run a bit slower). Only parallel programs will take advantage of multi-core processors, a situation that Tony Hoare, in his lecture given at the LIX Colloquium, characterized as follows: "From now on, software programmers will be responsible for maintaining Moore's law ". This will require major adaptations of existing applications, from a software industry that, so far, has been relying on hardware designers to get more performance and will be soon confronted to the difficulties of wide-scale concurrency.

Conclusion

Research in concurrency theory has produced a vast corpus of deep, valuable results. However, these results are only known, understood, and applied by a small fraction of computer scientists. As a consequence, their practical impact is not as strong as it could be, in spite of successful attempts at using process calculi to model and verify industrially critical systems. We believe, however, that concurrency theory still has an important role to play, and that the present context (see Section 4) is ideal for this:

Software systems modelling is becoming a standard industrial practice. There is an opportunity for the concurrency theory community to incorporate its results into the model-driven approaches, bringing semantics foundations and trying to replace informal models with formal ones.

Parallel computing facilities will be present everywhere, ranging from embedded devices and personal computers with multi-core processors to clusters and grids. Many software applications will need to be rewritten to fully benefit from these new architectures.

Combined to increasing demands for hardware and software reliability, these evolutions promise a bright future for the theoretical concurrency community. However, this will only happen if this community improves the dissemination of its theoretical results and devotes enough attention to applications. Otherwise, it is to be feared that results not transferred in proper time will be forgotten and reinvented somewhere else. To make such an "applied concurrency theory" agenda possible, three lines of actions should be considered:

1. The results accumulated by concurrency theory should be revisited from a Darwinian perspective: after the mutation phase, which gave birth to thousands of results, there should come a selection phase, in which the most useful results will be selected and presented to a larger audience. For instance, do we need so many process calculi? And do we really need to define fifty or more behavioral equivalences while we know that only three or four of them are sufficient in practice?

2. The results of concurrency theory are not easily applicable to languages based on threads, shared variables, locks, and semaphores, such as Java. It is therefore essential to maintain and increase the dissemination of process calculi. For doing so, one needs better languages than today. As discussed in Section 3, one should avoid unecessary fragmentation between multiple languages, and address the lack of user-friendliness (not simply expressiveness) -a major criterion for industrial acceptance.

In many formal specifications, it appears that only 20% of the code is devoted to concurrent aspects, while 80% of the code deals with standard data type definitions and sequential data manipulation. Therefore, process calculi should move away from a purely algebraical framework and get closer to mainstream imperative programming languages. Ideally, one should combine the classical concepts of structured programming (for data types and sequential computations) with the key features of process calculi (parallel H. Garavel composition, action hiding, formal semantics, compositionality, and congruence results). This approach would certainly reduce learning time for novice specifiers, since 80% of formal specifications would be similar to sequential programs, while only 20% would require specific training in concurrency theory. These ideas were pushed forward during the design of E-Lotos [START_REF]ternational Organization for Standardization -Information Technology[END_REF], and partly integrated into this international standard. Also, recent languages such as Lotos NT [START_REF] Sighireanu | LOTOS NT User's Manual (Version 2.4[END_REF], Chi [START_REF] Hofkamp | Chi 1.0 Reference Manual[END_REF], and Modest [START_REF] Bohnenkamp | MoDeST: A Compositional Modeling Formalism for Real-Time and Stochastic Systems[END_REF] seem to follow the same principles.

3. The times have gone, where formal methods were primarily a pen-and-pencil activity for mathematicians. Today, only languages properly equipped with software tools will have a chance to be adopted by industry. It is therefore essential for the next generation of languages based on process calculi to be supported by compilers, simulators, verification tools, etc. This also applies to new models for concurrency, such as mobile calculi and bigraphs. The research agenda for theoretical concurrency should therefore address the design of efficient algorithms for translating and verifying formal specifications of concurrent systems.

RR n 6368

This list is available from http://www.inrialpes.fr/vasy/cadp/case-studies.html.

See http://www.inrialpes.fr/vasy/dyade/formalfame.html for details. INRIA

On the opposite, Lotos was probably the first example of a language specifically designed not to be a calculus

nowadays, one would say "abstracted" RR n 6368


Gwen Salaün

Wendelin Serwe
email: wendelin.serwe@inria.fr

Yvain Thonnart
email: yvain.thonnart@cea.fr

Pascal Vivet
email: pascal.vivet@cea.fr

Formal Verification of CHP Specifications with CADP Illustration on an Asynchronous Network-on-Chip

Few formal verification techniques are currently available for asynchronous designs. In this paper, we describe a new approach for the formal verification of asynchronous architectures described in the high-level language CHP, by using model checking techniques provided by the CADP toolbox. Our proposal is based on an automatic translation from CHP into LOTOS, the process algebra used in CADP. A translator has been implemented, which handles full CHP including the specific probe operator.

The CADP toolbox capabilities allow the designer to verify properties such as deadlock-freedom or protocol correctness on substantial systems. Our approach has been successfully applied to formally verify two complex designs. In this paper, we illustrate our technique on an asynchronous Network-on-Chip architecture. Its formal verification highlights the need to carefully design systems exhibiting nondeterministic behavior.

Introduction

Process calculi are acknowledged as appropriate formalisms to describe concurrent systems. For the description of asynchronous hardware, several VLSI programming languages based on process calculi have been proposed, as for instance CHP (Communicating Hardware Processes) [START_REF] Martin | Compiling communicating processes into delay-insensitive VLSI circuits[END_REF], DI-Algebra [START_REF] Udding | A formal model for defining and classifying delay-insensitive circuits[END_REF], 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]), or BALSA [START_REF] Edwards | Balsa: An asynchronous hardware synthesis language[END_REF]. These languages allow the description of concurrent processes communicating via handshake synchronizations, and are supported by synthesis tools that can generate the implementation of a design from its process algebraic description. For instance, the TAST synthesis tool [START_REF] Renaudin | TAST Compiler and TAST CHP Language[END_REF] can generate QDI (Quasi Delay Insensitive) netlists from CHP descriptions and is being used to elaborate complex designs. However, for CHP specifications, few formal verification means are available, although they are essential in an asynchronous context to reduce the risk of errors in the design.

Our goal is the verification of asynchronous hardware designs specified in CHP using existing model checking tools that are based on the exploration of LTSs (Labelled Transition Systems), also known as finite state machines. Examples of properties to be checked are the absence of deadlocks or the correct sequencing of communications in a protocol (some stimuli are always followed by the appropriate responses). In this work, we used the model checking tools available in the CADP toolbox [START_REF] Garavel | An overview of CADP 2001[END_REF]. CADP takes as input LOTOS [START_REF] Iso/Iec | International Standard 8807, International Organization for Standardization -Information Processing Systems -Open Systems Interconnection[END_REF] specifications, and provides an efficient tool for exploring the state space of a LOTOS description.

Our approach is based on the translation from CHP to LOTOS. Such a high-level translation has been chosen since CHP and LOTOS are both inspired by the process algebra CSP [START_REF] Hoare | Communicating Sequential Processes[END_REF], i.e., they are based on the same kernel of behavioral operators, namely sequential composition, choice, and parallel composition. This translation is not trivial though because CHP has some hardware related specificities that do not exist in LOTOS. In particular, communication in CHP is not necessarily atomic (as it is in standard process calculi): the probe operator [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.

A translator tool has been implemented and was used successfully for the verification of two industrial case studies designed at the CEA/Leti laboratory, namely an asynchronous implementation of the DES (Data Encryption Standard) [START_REF]Data encryption standard (DES). Federal Information Processing Standards FIPS[END_REF] and ANOC, an asynchronous Network-on-Chip architecture [START_REF] Beigné | An asynchronous NoC architecture providing low latency service and its multi-level design framework[END_REF]. This paper focuses on ANOC, the input controller of which is used for illustration purposes. We show how informal properties to be ensured are formalized and checked using the verification means available in CADP.

The organization of the paper is as follows. Section 2 overviews our translation from CHP into LOTOS. Section 3 shows how verification of hardware architectures is achieved using CADP tools. In Section 4, we present the ANOC architecture, and we illustrate in Section 5 the application of our approach on a part of ANOC. Section 6 compares our proposal with related work. Section 7 ends the paper with some concluding remarks.

Translation of CHP into LOTOS

Translating CHP into LOTOS is quite straightforward for most CHP operators, since both languages are based on the process algebra CSP (see Appendices A and B for a brief summary of both languages). Thus, communication in both directions (emissions and receptions), guarded behavior, sequential and parallel composition, and nondeterministic choice exist in both languages. There are, however, some noticeable differences. For instance, CHP types (Booleans, natural numbers, bit vectors, etc.) are translated into LOTOS abstract data types. Similarly, CHP operations are translated into LOTOS operations, which are implemented either using algebraic equations or, more efficiently, by external C code, using the possibilities offered by CADP. CHP loops are translated into recursive processes in LOTOS because LOTOS does not have a similar loop construct.

A major difference between CHP and LOTOS is the hardware-specific probe operation of CHP, which has no equivalent in LOTOS. A previous version [START_REF] Salaün | Translating hardware process algebras into standard process algebras -illustration with CHP and LOTOS[END_REF] of the translation focused on CHP behaviors using the probe only as a single operator in guards. To deal with the full specification of complex designs such as ANOC, we have extended our translation to handle probes in general expressions and to support complex datatypes and code specialization.

Translation of the Probe

A probe "c #" (activity probe) allows a passive process (either emitter or receiver) to check if its active partner has already initiated a communication on channel c without performing the communication actually. The notation "c #V " (value probe), which can only be used by a receiver, checks if the sender has initiated the emission of the particular value V . The probe operator enables a form of shared memory communication, and does not exist in classical process calculi based solely on message passing. Hence, its translation requires the generation of additional communications representing the access to the active channels to be probed.

To alleviate the overhead due to the general translation of probe operations, our approach uses code specialization, i.e., the translation of a communication channel c depends whether and how c is probed.

• unprobed channel: each CHP emission/reception is translated directly to its LOTOS equivalent.

• general case: the evaluation of an expression containing probes requires information on the state (commu- • single probe: if a channel c is probed in a guard (containing no other probe operation), the additional LO-TOS process can be avoided. In this case, the probe (passive side) is translated as a communication with an additional flag "!Probe" to distinguish it from a regular communication. The guarded statement can be executed as soon as the probe communication is possible. The communication on the active side is translated in a loop: both processes can interact on the probe communication 1 as often as necessary until the effective communication between them takes place. This translation is summarized in Figure 1 and detailed in [START_REF] Salaün | Translating hardware process algebras into standard process algebras -illustration with CHP and LOTOS[END_REF].

In case of a probed channel, the translation scheme simulates a two-phase protocol with the effective communication corresponding to the acknowledgement. Otherwise (unprobed channel), such a protocol is avoided to reduce the corresponding state space. The examples in the remainder of this paper use only the unprobed and single probe case.

Tool Implementation

A translator from CHP to LOTOS has been developed using the SYNTAX and LOTOS NT compiler construction technologies [START_REF] Garavel | Compiler construction using LOTOS NT[END_REF]. It consists of 2,200 lines of SYNTAX, 13,400 lines of LOTOS NT, and 3,900 lines of C. This tool has been validated on more than 500 CHP specifications, corresponding to about 14,500 lines of CHP. We emphasize that this tool allows a completely automated translation for full CHP including probes and hierarchical components.

As regards semantics preservation, the translation of the probe operation requires the generation of additional hidden communications leading to internal transitions labelled by τ ; thus it is impossible to preserve strong equivalence [START_REF] Milner | Communication and Concurrency[END_REF], which handles τ transitions similarly to visible transitions, but only weak equivalences that allow additional τ transitions. Our translation preserves observational equivalence [START_REF] Milner | Communication and Concurrency[END_REF], as checked in practice on many examples.

Architecture Verification with CADP

The verification technique implemented in the CADP toolbox [START_REF] Garavel | An overview of CADP 2001[END_REF] is called enumerative since it is based on the explicit enumeration of states. To verify properties of large state spaces, CADP incorporates different techniques, such as static analysis, distributed, and compositional verification, that help to circumvent the so-called state explosion problem.

In this section we focus on the use of CADP for the verification of asynchronous architectures. In a first step, an LTS that is smaller, but equivalent to the complete state space, is generated compositionally. This LTS is then used in a second step for the verification of the interesting properties.

Compositional State Space Generation

The underlying principle of compositional state space generation is "divide and conquer": instead of a single monolithic generation step, the state space of the complete system is obtained by alternating generation, minimization, and sub-system-composition steps. This approach is particularly efficient if the subsystems contain internal τ transitions (representing details not required for the composition with the rest of the system), some (or even most) of which might be removed during minimization modulo a weak equivalence abstracting from τ transitions.

The successful use of compositional state space generation requires some care, since the state space of some part of the overall system might be larger than the state space of the complete system. For instance, the state space of a simple buffer generated separately contains all possible values, whereas only some particular values might be buffered in the complete system. Thus, the state space of a specific part of the system should be generated only if the constraints imposed by its environment are also taken into account, so that only the relevant part of its state space is generated.

Furthermore, restricting the input values of the system allows to reduce the size of the generated state space. Different techniques can be used for this purpose.

• Using the idea of data independence, if some parts of the input values have no influence with respect to the interesting properties, they can be chosen constant, so as to abstract from differences in the data values which otherwise would multiply the size of the state space accordingly.

• A specific environment, i.e., additional CHP processes implementing the environment of the system guaranteeing that only realistic stimuli are provided, avoids the enumeration of stimuli that will never occur in practice. Here and in the sequel, a stimulus is a communication with a passive port, i.e., either sending a message to a passive input port or requesting the emission of a message from a passive output port.

A specific environment may also include additional ports on which messages are sent if an error has been detected.

• Exploiting symmetry arguments, the generation of a single state space taking into account all possible orderings of inputs can be replaced by the generation of several smaller state spaces corresponding to scenarios representing particular subsets (e.g., sequences) of the inputs. These scenarios should be expressed in CHP and integrated in the specific environment.

The compositional generation of the state space is facilitated by the use of SVL (Script Verification Language) [START_REF] Garavel | SVL: a scripting language for compositional verification[END_REF], which allows a high-level and concise description of the calls to the different CADP tools. The order in which the different processes are combined has to be determined manually following the data path of the stimuli, requiring knowledge about the architecture. Since this order does not depend on the scenario, a single SVL script can be used for the compositional generation of the LTSs corresponding to several scenarios.

Property Verification

In the following, we describe the techniques for the verification of three different kinds of properties relevant in the validation of asynchronous hardware architectures.

Deadlock Freedom.

Given the complete state space of a system, it is straightforward to check the absence of deadlocks by counting the number of successors of every state. In CADP, this property is printed as one of the standard characteristics of an LTS.

Notice that most of the remaining properties require a cyclic behavior. Thus their verification would fail if the system might deadlock.

Correct Stimulus-Response Protocol.

Code inspection allows to verify that a single basic process of an asynchronous design conforms to the basic protocol, i.e., executes a cyclic behavior producing from a set of stimuli {S 1 , . . . , S m } a set of responses {R 1 , . . . , R n }. To verify this property for more complex components, containing several subcomponents and processes, the following threestep approach relying on the equivalence checking tools of CADP can be used. 1. To check the cyclic occurrence of the whole set of stimuli, all transitions but the stimuli S i are hidden (i.e., transformed to τ transitions) in the generated LTS, and the resulting LTS is then compared to an LTS describing the cyclic arrival of stimuli in any order; this second LTS can be given explicitly, or be generated from a LOTOS or CHP description, namely the CHP process "[(S 1 , . . . , S m ); loop]".

2.

To check the cyclic occurrence of the whole set of responses, the same technique can be applied as for the stimuli.

3. To check that the set of stimuli generates the set of responses, it is now sufficient to choose a single stimulus S and a single response R and to verify that S generates R; the advantage is to avoid to consider all possible orderings of stimuli and responses. This step can be achieved by comparing with the LTS generated from the CHP description "[S;R;loop]".

Notice that it is not sufficient to compare the LTSafter hiding all transitions but the stimuli and responses -with a second LTS corresponding to the CHP process "[(S 1 , . . . ,S m );(R 1 , . . . ,R n );loop]", since this would require that the first response occurs necessarily after the last stimulus, which might not be the case if a response R j depends only on a subset of the stimuli.

Functional Properties.

General functional properties can be verified in two ways. A first approach is to enrich the specific environment with observer processes that monitor the stimuli and responses, and signal any detected error (e.g., faulty responses) by a particular Error transition or block the system as soon as an error is detected. In this case, the verification of the property is tantamount to checking the reachability of an Error transition or the absence of deadlock.

A second possibility is classical model checking. In this case, the property is expressed formally using a temporal logic, e.g., regular alternation free µ-calculus in CADP. Then, a model checker, EVALUATOR [START_REF] Mateescu | Efficient on-the-fly modelchecking for regular alternation-free mu-calculus[END_REF], is used to verify if the generated state space, possibly after hiding some transitions, satisfies the formula.

The temporal logic used in CADP allows two modalities:

• the formula "[ S ] ϕ" is true in a state s, if all transition sequences of the form S and starting in s lead to a state where ϕ is true.

• the formula "< S > ϕ" is true in a state s, if there exists a transition sequence of the form S, starting in s, and leading to a state where ϕ is true.

In both cases, the pattern of a transition sequence S in the modal operator can use regular expressions on predicates of transition labels. In particular, the predicate true is true for every transition; thus the regular expression "true*" describes a possibly empty sequence of transitions.

An Asynchronous Network-on-Chip

The verification approach described in Sections 2 and 3 is illustrated hereafter on the CHP specification of an actual asynchronous design, namely ANOC, an Asynchronous Network-on-Chip architecture [START_REF] Beigné | An asynchronous NoC architecture providing low latency service and its multi-level design framework[END_REF], which was 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].

This Section presents the asynchronous node of ANOC with a specific focus on its input controller, which will be used in Section 5 for illustration of our approach.

ANOC Outline

ANOC relies on the GALS (Globally-Asynchronous Locally-Synchronous) paradigm, in which synchronous resources communicate through a fully asynchronous network. Resources are connected to the network via a synchronous network interface providing all higher-level network services (packetization, flow-control, . . . ) and application services (synchronization, scheduling, . . . ), which connects to the switching fabric through a GALS interface, as described in [START_REF] Beigné | Design of off-chip and on-chip interfaces for a GALS NoC architecture[END_REF].

The five-port asynchronous network node is the elementary component of ANOC. It provides the lower-level network services, i.e., routing and arbitration of the transiting packets. It is actually made of five input controllers, which route incoming packets to one of the other four ports, and five output controllers, which arbitrate between packets heading for the same output.

Although no assumption is made on the topology of the network as regards the architecture of the node, it was chosen in the FAUST implementation of ANOC to connect the nodes in a 2D-Mesh topology, as seen in Figure 2.

It is crucial for any application that the interconnect structure transfers data without corruption, and with a sufficient level of QoS (Quality-of-Service). At a system level, a 2D-Mesh topology presents several advantages (scalable bandwidth, easier place and route on silicon), but also enables theorem proving thanks to its regular structure. For instance, using the "odd-even turn model" routing algorithm [START_REF] Chiu | The odd-even turn model for adaptive routing[END_REF], a routing of the communications in the network that avoids any deadly embrace can be computed.

Figure 2. FAUST network architecture

Such analytical methods can often guarantee high-level properties, but always rely on an ideal operation of the asynchronous nodes. It is hence necessary to verify, at design level, that a node strictly complies to the ANOC protocol.

Functional Specifications: ANOC Protocol

Formal verification has to rely on rigorous functional specifications of the design. In the following, we describe the network protocol of ANOC that the asynchronous node should implement.

Data-Link Layer.

The elementary piece of information transiting on the links of ANOC is called a flit (flowcontrol unit). In order to provide QoS in the network, ANOC was designed using two VCs (Virtual Channels) with different priority levels, used to transmit flits according to their precedence. A VC identifier is associated to every flit transiting in the network, and is propagated through a Send channel in the whole path, along with the actual Data.

The asynchronous node dispatches incoming flits inside its internal buffers according to this VC identifier, so that contention, i.e., the need for arbitration between two communications, may appear only between flits sharing the same VC. The arbitration between VCs was made static, so that VC0 always holds priority before VC1.

This mechanism actually creates two independent logical networks, one of which may be kept lightly loaded for low-latency signalling messages.

Additionally, a flit-based flow control mechanism had to be implemented to control the buffering capacity of each port on VC1. Indeed, the separation into VCs requires that the physical link between two nodes must be kept free for a new flit on VC0 after each flit on VC1. Since the link is shared by the two VCs, letting flits accumulate on VC1 more than the buffering capacity of the input controller would block flits of the other VC in the shared part. An Accept1 channel was therefore introduced, indicating that a new flit can be buffered on VC1 in the input controller. This defines on VC1 a data-link protocol where a token on the Accept1 channel is consumed by the emitter before each transmission on Send and Data, and is regenerated once the transmission is over. The protocol on VC0 is simpler, as it only requires simultaneous transmissions on Send and Data.

Network Layer.

In order to minimize the overhead of routing information in every communication, the ANOC protocol is based on packet switching: several consecutive flits are gathered, using a single VC, into a packet, which will be transmitted, on this VC, without interruption. This requires an identification of the first and last flits of a packet: we introduced therefore two additional bits to the 32 bit data path, coding the begin of packet (BOP) and end of packet (EOP) informations.

Furthermore, in order not to handle complex routing tables, we used static source routing of the packets. Routing information (path-to-target) is provided in the first flit (header) of a packet, as a vector of dibits containing the successive directions to follow. Each node actually uses the two lower bits of this vector in the first flit to route the whole packet in the given direction, and shifts the path-to-target so that it can be used by the following node. Considering only the VC identifier, BOP, EOP, the destination, and a 2-bit flit identifier, we can reduce the potential state space of the input controller from about 5 * 10 25 states to about 5 * 10 16 states2 . The fixed sequence used for the flit payload is made so that it reflects the data integrity, including the shift of the path-to-target.

BOP EOP

CHP Design of the ANOC Input Controller

The asynchronous node was first developed using a coarse description level in SystemC/TLM, which was used to set up the various layers of the ANOC protocol at a system level [START_REF] Beigné | An asynchronous NoC architecture providing low latency service and its multi-level design framework[END_REF]. Then, an equivalent functional CHP model of the node was written, and was later refined into elementary CHP processes that could be synthesized using a WHCB (Weak-Condition Half-Buffer [START_REF] Lines | Pipelined asynchronous circuits. Master's thesis[END_REF]) circuit template, and mapped onto a specific standard cell library.

We chose to apply our formal verification technique on the refined CHP model of the input controller of the ANOC node, whose behavior is the closest to the actual implementation in the FAUST chip.

The internal micro-architecture of the input controller is given in Figure 4, and was described more precisely in [START_REF] Beigné | An asynchronous NoC architecture providing low latency service and its multi-level design framework[END_REF]. In this figure, light grey processes are actually synthesized with combinational logic. The interface of the input controller complies, on the data-link side, to the ANOC protocol, and consists therefore of the signals in Data, in Send and in Accept1. The internal control and data signals from an input controller to the output controllers are:

• Data0 and Data1, buffered in the two VCs, that the input controller broadcasts to every output controller, only one of which will acknowledge the channel.

• Validi tod signals notifying the availability of a new flit on Datai to the output controller d.

• BOPi tod signals, notifying the begin of a packet, necessary to trigger arbitration on the output controller.

• EOPi signals, notifying the end of a packet, broadcast in the same way as Datai, necessary to enable a new arbitration on the output controller.

• Accept1 fromd signals from the output controller, indicating that a new flit can be sent on VC1.

A peculiarity in this design is the use of passive combinational splits at the output of the input controller, in order to reduce the gate count compared to a 34-bit passive-in / active-out commanded split. At implementation level, such a combinational split is indeed only a AND4 gate merging the "active low" acknowledgement signals, while the data wires are forked to every output controller.

This behavior was described in CHP using a passive output, which can be probed for communication requests by the output controllers. The actual notification of the output controllers is done by the Route Flit process, using the Validi tod signals.

The CHP code of such a process is given below:

Formal Verification of the Input Controller

The translation from CHP to LOTOS and compositional state space generation described in Sections 2 and 3 have been used to set up a formal model of the input controller of ANOC. Using this model, it is possible to check the functional properties describing its conformance to the ANOC protocol.

Translation of the CHP Design into LOTOS

First of all, for each considered scenario, the CHP design of the input controller (about 1,200 lines of code) is translated in less than one second into LOTOS (about 3,600 lines of code) using our translator tool. Let us show the LOTOS code obtained after translation of the CHP process Split Data0 shown above (find in Appendix B a summary of the LOTOS operators). The LOTOS process below is slightly simplified since we removed the explicit list of gates "[Data0 tod]" coming with every process call. The CHP process contains simple probes in its guards that are translated as communications in LOTOS with the specific offer "!Probe" to distinguish them from regular communications on the same channels. A branch of the choice structure in the LOTOS process can be executed if and only if an active process is ready to communicate on this particular channel with the process at hand.

State Space Generation

In order to provide realistic stimuli to the input controller of ANOC, several scenarios were used with packets of different length (one or more flits), emitted sequentially or overlapping on different channels and to different destinations. The composition order of the different processes used to build the state space of the input controller has been determined following the data path of the input values according to the architectural schema presented in Section 4.3.

The description of the 41 steps to generate the LTS corresponding to the input controller of ANOC for a particular cycle of four flits requires 483 lines of SVL. The script is generic in the sense that it can be used to generate the state space for all stimuli using only simplified flits as described in Figure 3. In the remainder of this section, we consider the scenario based on the sequence of four packets (each containing exactly one flit) sent on virtual channel VC0 alternatively to destination 0 and to destination 1. For this scenario, the SVL script generates, in about four minutes, the corresponding LTS with 1,300 states, 3,116 transitions, and 34 labels without any hidden internal transition. The largest intermediate LTS observed during the generation has 295,893 states and 812,283 transitions. Similar values are observed when the SVL script is used for the generation of LTS corresponding to different cycles of four flits.

Verification of the Functional Specifications

Even though the micro-architecture of the input controller was used during the state space generation, the properties to which it should conform were defined as if it were a blackbox. Thus, we enunciated functional properties, which describe the protocols at the interfaces, not biased by any structural hypothesis.

Similarly to the compositional state space generation, the verification of the properties uses a SVL script (of about 250 lines) which facilitates the calls to the different CADP tools, required for hiding and renaming of transitions, as well as equivalence and model checking. A further advantage of the script is the possibility to automate the verification of different scenarios. For a scenario with cyclic sequences of four flits, the execution of the script checking all the properties presented below takes about three minutes.

Infinite

Occurrence. The input controller may not reach a state where a communication may not occur anymore on an asynchronous channel. For every signal S, it should have a "quasi-cyclic" behavior in a closed system.

These properties were checked with the CADP toolbox as explained in Section 3.2. Every state of the state space has a successor, which means there is no deadlock state. Furthermore, for a signal S, the "quasi-cyclic" behavior is verified using the observational equivalence-checking technique to compare the LTS of the input controller with the LTS of a CHP process "[S!;loop]", after hiding every other signal in the input controller.

Protocol Correctness.

The input controller must comply at its inputs with the ANOC protocol, and transmit the incoming data to an output controller. On VC0, this means that an incoming flit will generate an emission to an output controller.

This was proven formally using a stimulus-response pattern, as described in Section 3.2: the two stimuli in Data and in Send together must lead to the three responses Validi tod, Datai, and EOPi, where the values of ithe virtual channel (0 or 1) -and d -the destination (0, 1, 2, or 3) -are obtained by inspection of the values communicated on in Data.

On VC1, an accept token must be used and regenerated accordingly, but this is actually done in the output controller. Environment processes simulating the output controllers were described in the specific environment of the input controller, which perform this task. The property describing this behaviour actually ensured correctness of the combination of these additional processes to the input controller. Decorrelation of the accept process from the forward data flow of the input controller can be seen in Figure 4 of Section 4.3: the architecture of the input controller is divided in two unconnected parts.

Data Integrity.

The content of the communications must be preserved by the input controller. Body flits should be transmitted without alteration, while header flits should be transmitted with their path-to-target field shifted, preserving the BOP, EOP, and header payload fields.

This functional property has been verified by integrating observer processes in the specific environment: the environment processes simulating the output controllers have been enriched in order to compare the data from the input controller with the expected result, determined according to the flit provided as a stimulus to the input controller.

Packet Routing.

The input controller has to route all the flits of a packet in the right direction. A header flit will be routed to the output controller specified by its destination field, while a body flit will use the same direction as the previous header flit.

The following formula expresses that after every sequence of transitions such that after an unspecified start a transition labelled with a request to emit a priority packet (predicate "on channel(0)") is followed by a transition labelled with a request to emit a data packet to destination 1 (predicate "to dest(1)"), the next communication on one of the channels Data0 tod (predicate "no Data0 toD()" is true for all other transitions) is necessarily on channel Data0 to1:

[true* . on_channel(0) . to_dest(1)] <(no_Data0_toD())* . 'Data0_to1'> true Unfortunately, this formula does not hold for the LTS (after hiding all transitions on channels different from in Send, in Data, and Data0 tod). The counterexample provided by EVALUATOR [START_REF] Mateescu | Efficient on-the-fly modelchecking for regular alternation-free mu-calculus[END_REF], the model checker of CADP, shows the possibility that, contrary to the design assumptions, two flits for the virtual channel 0 can be present simultaneously in the input controller, which can lead to a routing error, i.e., a flit is transmitted to a wrong output. This is confirmed by the following formula which expresses that in all transition sequences, after a communication on one of the channels "Valid0 tod" there has to be a communication on one of the channels "Data0 tod" before the next communication on one of the channels "Valid0 tod", which does not hold either: This routing problem has also been found by simulating the CHP description of the input controller using the TAST simulator for about 500.000 steps. The actual issue with simulation-based validation is to decide when the verification was thorough enough to claim a correct behavior.

The encountered problem lies in the use of the passive split that simulates broadcasting to every output controller. EVALUATOR exhibits the following sequence of communications (unrelated transitions are hidden):

in Send!0; In → Route Flit in Data!flit0; In → Shift Data Valid0 to0!; Route Flit → VC0 Out 0 Cmd Shift!bop0; Route Flit → Shift Data in Send!0; In → Route Flit in Data!flit1; In → Shift Data Valid0 to1!; Route Flit → VC0 Out 1 Data0 to1#true; VC0 Out 1 → Split Data0 Data0!flit0; Shift Data → Split Data0 Data0 to1!flit0; Split Data0 → VC0 Out 1 ERROR 1!;
VC0 Out 1 → In this sequence, flit0 is a header flit to output 0, and flit1 is a header flit to output 1.

The issue is that the active signals Valid0 tod are acknowledged by the outputs before the probe is actually done in Split Data0. Once Route Flit has sent both its outputs Valid0 to0 and Cmd Shift, a new incoming flit can trigger Valid0 to1 immediately afterwards. Both output controllers are therefore notified and may request the data, creating a non-exclusive guard in Split Data0, leading to an unwanted non-deterministic choice.

Nevertheless, this issue does not occur in the actual implementation of the node 3 . It is indeed an issue of interpretation of the CHP specification.

The circuit was synthesized using a WCHB [START_REF] Lines | Pipelined asynchronous circuits. Master's thesis[END_REF] circuit template. The slack (maximal number of tokens a single process can accumulate) of each WCHB process is only 1/2, due to the four-Phase reshuffling. Besides, the Split Data0 combinational process has a null slack. Hence, in the synthesized version, the Cmd Shift token at the output of Route Flit is not freed before Data0 was read, which happens only after Split Data0 was notified. This guarantees that no other token can be emitted to Valid0 tox, preventing the routing error. Yet, this property holds only if the slack between Route Flit and Split Data0 is less than 1. The system is said not to be slack-elastic [START_REF] Manohar | Slack elasticity in concurrent computing[END_REF].

However, on current implementations of the simulation and verification tools, communications on CHP channels are done atomically between two semicolons, and do not describe the acknowledgement of the data. This corresponds to a Full-Buffer (slack of 1) description of the asynchronous processes, except for Split Data0, thanks to the probe on output mechanism.

The slack increase in the CHP description of this non slack-elastic process allows an unwanted behavior, namely the routing of a flit to a wrong output.

To investigate this further, we modified the CHP description so as to reduce the slack of the processes by doubling the communications on each channel, which mimics a fourphase protocol. A first communication describes the raising phase on the signal (falling on the acknowledge), while the second describes the falling phase on the signal (rising on the acknowledge), the guards being evaluated according to the first communication. With each process modified following this principle, the LTS contains no error transition: the routing properties hold.

As for VC1, the routing correctness was already verified on the original CHP description. Thanks to the Accept1 flow-control mechanism, a single flit is allowed in the input controller. Even though an additional buffering stage is present on VC1, the overall slack is constrained to 1, and no interference can occur.

Related Work

As regards the application of model checking tools to asynchronous hardware designs in general, most approaches, e.g., [START_REF] Nowick | Practicality of state-machine verification of speed-independent circuits[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] Kapoor | Modelling and verification of delay-insensitive circuits using CCS and the Concurrency Workbench[END_REF][START_REF] Rahardjo | SPIN as a hardware design tool[END_REF][START_REF] Wang | On process-algebraic verification of asynchronous circuits[END_REF][START_REF] Yoeli | LOTOS/CADP-based verification of asynchronous circuits[END_REF], are based on a manual modelling of the design directly in the input language of the used verification tool, whereas we base the verification on design descriptions written by hardware designers -the same descriptions that are also used for synthesizing the circuits. As an example, [START_REF] Wang | On process-algebraic verification of asynchronous circuits[END_REF] introduces a model for the low-level description of asynchronous circuits on the hardware gate level, and presents the verification of safety and progress properties using FDR2 (via a manual translation to CSP). On the contrary, our approach focuses on the verification of high-level descriptions, from which concrete implementations in hardware can be derived automatically, for instance using TAST.

As regards verification of process algebraic descriptions of asynchronous designs, we are only aware of [START_REF] Borrione | Validation of asynchronous circuit specifications using IF/CADP[END_REF] and [START_REF] Kapoor | Verification and implementation of delay-insensitive processes in restrictive environments[END_REF]. [START_REF] Borrione | Validation of asynchronous circuit specifications using IF/CADP[END_REF] proposes a translation of CHP into networks of communicating automata. Contrary to our approach, [START_REF] Borrione | Validation of asynchronous circuit specifications using IF/CADP[END_REF] flattens CHP processes with intertwined sequential and parallel compositions, which is less efficient than our translation from CHP into LOTOS; we also observed reductions of the LTS generation time by factors up to four [START_REF] Salaün | Translating hardware process algebras into standard process algebras -illustration with CHP and LOTOS[END_REF]. [START_REF] Kapoor | Verification and implementation of delay-insensitive processes in restrictive environments[END_REF] presents techniques for equivalence and refinement checking of DI-Algebra descriptions. Our approach allows to verify a larger class of properties, i.e., alternation-free modal µ-calculus formulas.

Conclusion

In this paper, we have presented an approach for the verification of process algebraic descriptions of asynchronous architectures using the verification toolbox CADP originally designed for the verification of telecommunication protocols. Our approach is supported by a tool, capable of automatically translating full CHP into the international standard LOTOS. We validated our approach on two asynchronous designs, namely an implementation of the Data Encryption Standard [START_REF]Data encryption standard (DES). Federal Information Processing Standards FIPS[END_REF] and ANOC, the input controller of which was used in this paper as an illustrating example.

The node of ANOC required a careful CHP design using non slack-elastic processes. Some of the node properties were thus verified while manually taking the handshake expansion into account. In order to ease this verification task, we suggest to enrich the high-level CHP language with pragmas indicating the chosen handshake expansion to the simulation, synthesis and verification tools.

As regards future work, we are currently using our approach to ensure the correctness, before synthesis, of architectures designed at the CEA/Leti laboratory, in particular the next implementation of ANOC. In this context, we rely on the possibility to use our approach hierarchically, by isolating subsystems that are verified separately and seen as blackboxes when verifying properties of the global system.

Figure 1 .

 1 Figure 1. Single probe translation

Figure 3 .Figure 3

 33 Figure 3. Flit format

Figure 4 .

 4 Figure 4. Input controller micro-architecture

[

  true* . 'Valid0_to.' . (not 'Data0_to.*')* . 'Valid0_to.'] false

The value-matching feature of LOTOS ensures that two offers "!Probe" will synchronize.

These numbers are obtained by multiplication of the numbers of states of the separate processes; due to synchronizations, the actual number might be slightly smaller.

This was actually checked in a SDF (Standard Delay File) backannotated Verilog simulation of the node.

Acknowledgements

This collaborative work has been supported by the common laboratory of INRIA Rhône-Alpes and CEA/Leti as well as the Minalogic EmSoC MULTIVAL project.

The authors would like to thank their colleagues from the TIMA CIS group for providing the TAST CHP syntax, and for valuable discussions on the probe semantics.

A. Grammar of CHP

The behavior of a process B in CHP is described using assignments, communications, collateral and sequential compositions, and nondeterministic guarded commands (as implemented in the TAST tool [START_REF] Renaudin | TAST Compiler and TAST CHP Language[END_REF]):

B. Grammar of LOTOS

We only present in this appendix a very simplified grammar of the LOTOS notation, see [START_REF] Iso/Iec | International Standard 8807, International Organization for Standardization -Information Processing Systems -Open Systems Interconnection[END_REF][START_REF] Bolognesi | Introduction to the ISO specification language LOTOS[END_REF] for more details. The behavior of a process B in LOTOS is described using communications, sequence, guarded behavior, choice, parallel composition, and process call (to express a looping behavior):

process call G ::= τ internal action | g!V emission on gate g | g?x : t reception on gate g V ::= x | f (V1, . . . , Vn) value expression The parallel composition operator means that processes B1 and B2 synchronize on the gates g1, . . . , gn. As LOTOS gates are untyped, the type of received values must be specified for receptions.