# The Constructive Semantics of Pure Esterel - Draft
## Version 3

Gérard Berry

► To cite this version:

Gérard Berry. The Constructive Semantics of Pure Esterel - Draft Version 3. 1999. hal-04963343

HAL Id: hal-04963343

https://hal.science/hal-04963343v1

Preprint submitted on 24 Feb 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
The Constructive Semantics of Pure Esterel
Draft Version 3

G. Berry

Centre de Mathématiques Appliquées
Ecole des Mines de Paris and INRIA
2004 route des Lucioles
06902 Sophia-Antipolis CDX, France

berry@sophia.inria.fr

http://www.inria.fr/meije/Personnel/Gerard.Berry.html

Dec. 16th, 2002
# Contents

1 Introduction 9

I Informal Presentation 17

2 The Pure Esterel Kernel Language 19

2.1 Signals and Reactions 19

2.2 Kernel Esterel Statement 20

2.3 The Intuitive Semantics 20

2.4 Comparison with Previous Kernels 23

3 Logical Correctness 27

3.1 Logical Correctness 28

3.2 Examples of Logically Correct Programs 28

3.3 Examples of Logically Incorrect Programs 30

3.4 A Strange Logically Correct Program 32

4 The Constructive Approach 35

4.1 External Justification Versus Self-justification 35

4.2 The Constructive Behavioral Semantics 37

4.2.1 Accepting Programs 38

4.2.2 Rejecting Programs 40

4.3 The Constructive Operational Semantics 41

4.3.1 Accepting Programs 41

4.3.2 Rejecting Programs 46

4.3.3 Summary of the Constructive Interpretation Scheme 46

4.3.4 Comparison With Previous Operational Semantics 47

4.4 The Circuit Semantics 47

4.4.1 The Logical Interpretation of Circuits 47
<table><tbody><tr><td>4.4.2</td><td>The Electrical Implementation of Circuits</td><td>48</td></tr><tr><td>4.4.3</td><td>Constructive Circuits</td><td>50</td></tr><tr><td>4.4.4</td><td>From Esterel Programs to Constructive Circuits</td><td>51</td></tr><tr><td>4.5</td><td>Complexity Issues</td><td>51</td></tr><tr><td>4.6</td><td>Constructive Symbolic Debugging</td><td>52</td></tr><tr><td>4.7</td><td>Comparison with Previous Attempts</td><td>54</td></tr><tr><td>II</td><td>Structural Operational Semantics</td><td>57</td></tr><tr><td>5</td><td>The Esterel Process Calculus Syntax</td><td>59</td></tr><tr><td>6</td><td>The Logical Behavioral Semantics</td><td>63</td></tr><tr><td>6.1</td><td>Events</td><td>63</td></tr><tr><td>6.2</td><td>Program and Statement Transitions</td><td>64</td></tr><tr><td>6.3</td><td>Trap Propagation and Completion Codes</td><td>65</td></tr><tr><td>6.4</td><td>The Logical Behavioral Semantics Rules</td><td>65</td></tr><tr><td>6.5</td><td>Reactivity and Determinism</td><td>68</td></tr><tr><td>6.6</td><td>Loop-Safe Programs</td><td>69</td></tr><tr><td>7</td><td>The Constructive Behavioral Semantics</td><td>73</td></tr><tr><td>7.1</td><td>The Must and Cannot Analysis</td><td>74</td></tr><tr><td>7.1.1</td><td>Intuitive Presentation</td><td>74</td></tr><tr><td>7.1.2</td><td>The Must, Cannot, and Can Functions</td><td>76</td></tr><tr><td>7.1.3</td><td>The Definition of Must and Can</td><td>77</td></tr><tr><td>7.2</td><td>Possible Variants</td><td>81</td></tr><tr><td>7.3</td><td>Elementary Properties of Must and Can</td><td>82</td></tr><tr><td>7.4</td><td>Definition of the Constructive Semantics</td><td>82</td></tr><tr><td>7.5</td><td>Correctness of the Constructive Semantics</td><td>84</td></tr><tr><td>8</td><td>The State Behavioral Semantics</td><td>85</td></tr><tr><td>8.1</td><td>The Extended Syntax</td><td>86</td></tr><tr><td>8.1.1</td><td>States as Decorated Terms</td><td>86</td></tr><tr><td>8.1.2</td><td>State Syntax</td><td>87</td></tr><tr><td>8.2</td><td>State Expansion</td><td>88</td></tr><tr><td>8.3</td><td>The State Behavioral Semantics</td><td>89</td></tr><tr><td>8.3.1</td><td>The Logical State Behavioral Semantics</td><td>90</td></tr><tr><td>8.3.2</td><td>The Constructive State Behavioral Semantics</td><td>94</td></tr><tr><td>8.4</td><td>Equivalence to the Standard Semantics</td><td>96</td></tr></tbody></table>
9 The Constructive Operational Semantics 99

III Circuit Translation 101

10 Constructive Circuits 103

10.1 Boolean Circuits 103

10.1.1 Textual Definition 103

10.1.2 Definition by Diagrams 104

10.2 The Logical Semantics 105

10.3 The Constructive Semantics 106

10.3.1 Constructive Value Propagation 106

10.3.2 Three-Valued Denotational Semantics 107

10.3.3 The Electrical Semantics 108

10.4 Syntactic Extensions 109

10.4.1 Hierarchical Circuits 109

10.4.2 Definitions by Implications 109

11 The Basic Circuit Translation 111

11.1 Structure of the Esterel Circuit 111

11.2 The subcircuit generated by a statement 112

11.2.1 Subcircuit Interface 112

11.2.2 Execution Scheme 113

11.2.3 Constructive Semantics of the Program and Circuit 114

11.3 Translating the Kernel Esterel Statements 114

11.3.1 Translation of Completion Codes 114

11.3.2 Translation of the Emit Statement 116

11.3.3 Translation of the Present Statement 116

11.3.4 Translation of suspension and strong preemption 118

11.3.5 Translation of Sequencing 119

11.3.6 Translation of Loop 121

11.3.7 Translation of Parallel 121

11.3.8 Translation of Trap and Shift 123

11.3.9 Translation of local signal declaration 124

11.4 The Global Environment 124

11.5 A Constructive Execution Example 126
<table><tr><td><b>12</b></td><td><b>Schizophrenia</b></td><td><b>129</b></td></tr><tr><td>12.1</td><td>A Correctly Translated Loop</td><td>130</td></tr><tr><td>12.2</td><td>Schizophrenic Parallel Synchronizers</td><td>130</td></tr><tr><td>12.3</td><td>Schizophrenic Signals</td><td>132</td></tr><tr><td>12.4</td><td>An Easy Solution</td><td>133</td></tr><tr><td>12.5</td><td>The Surface and Depth of a Statement</td><td>134</td></tr><tr><td>12.6</td><td>Multiple Reincarnation</td><td>137</td></tr><tr><td>12.7</td><td>Curing Schizophrenia</td><td>139</td></tr><tr><td>12.7.1</td><td>Incarnation Indices</td><td>139</td></tr><tr><td>12.7.2</td><td>Translation Sketch</td><td>140</td></tr><tr><td>12.7.3</td><td>Simple Examples</td><td>141</td></tr><tr><td>12.7.4</td><td>Correct Translation of P18</td><td>143</td></tr><tr><td><b>13</b></td><td><b>The Formal Translation to Hardware</b></td><td><b>147</b></td></tr><tr><td>13.1</td><td>Translation Environments</td><td>147</td></tr><tr><td>13.1.1</td><td>The Global Environment</td><td>148</td></tr><tr><td>13.2</td><td>Translation Rules</td><td>149</td></tr><tr><td>13.3</td><td>Correctness of the Translation</td><td>154</td></tr><tr><td>13.4</td><td>Extension to Loop-Unsafe Programs</td><td>154</td></tr><tr><td><b>14</b></td><td><b>Conclusion</b></td><td><b>157</b></td></tr></table>
List of Figures

<table><tbody><tr><td>Program P1</td><td>28</td></tr><tr><td>Program P2</td><td>29</td></tr><tr><td>Program P3</td><td>30</td></tr><tr><td>Program P4</td><td>30</td></tr><tr><td>Program P5</td><td>30</td></tr><tr><td>Program P6</td><td>31</td></tr><tr><td>Program P7</td><td>31</td></tr><tr><td>Program P8</td><td>31</td></tr><tr><td>Program P9</td><td>33</td></tr><tr><td>Program P10</td><td>36</td></tr><tr><td>Program P11</td><td>40</td></tr><tr><td>Program P12</td><td>41</td></tr><tr><td>Circuit C1 (equations)</td><td>47</td></tr><tr><td>Circuit C2 (equations)</td><td>47</td></tr><tr><td>Circuit C9 (equations)</td><td>48</td></tr><tr><td>Circuit C12 (equations)</td><td>48</td></tr><tr><td>Circuit C13 (equations)</td><td>48</td></tr><tr><td>4.1 Circuit C9</td><td>49</td></tr><tr><td>4.2 Circuit C12</td><td>49</td></tr><tr><td>Program P13</td><td>49</td></tr><tr><td>4.3 Circuit C13</td><td>50</td></tr><tr><td>Program P14</td><td>54</td></tr><tr><td>Program P15</td><td>74</td></tr><tr><td>7.1 Circuit for P15</td><td>75</td></tr><tr><td>10.1 Gate Symbols</td><td>104</td></tr><tr><td>10.2 Diagrams vs. Definitions</td><td>105</td></tr></tbody></table>
<table>
  <tbody>
    <tr>
      <td>11.1 Circuit associated with a statement</td>
      <td>112</td>
    </tr>
    <tr>
      <td>11.2 Circuit for a completion code k ≠ 1</td>
      <td>115</td>
    </tr>
    <tr>
      <td>11.3 Circuit for pause, i.e. completion code 1</td>
      <td>115</td>
    </tr>
    <tr>
      <td>11.4 Circuit for !s</td>
      <td>116</td>
    </tr>
    <tr>
      <td>11.5 Circuit for s?p, q</td>
      <td>117</td>
    </tr>
    <tr>
      <td>11.6 Circuit for s ⊃ p</td>
      <td>119</td>
    </tr>
    <tr>
      <td>11.7 Circuit for s &gt;&gt; p</td>
      <td>120</td>
    </tr>
    <tr>
      <td>11.8 Circuit for p; q</td>
      <td>120</td>
    </tr>
    <tr>
      <td>11.9 Circuit for p*</td>
      <td>121</td>
    </tr>
    <tr>
      <td>11.10 Circuit for p | q</td>
      <td>122</td>
    </tr>
    <tr>
      <td>11.11 The constructive Max circuit</td>
      <td>122</td>
    </tr>
    <tr>
      <td>11.12 Circuit for {p}</td>
      <td>124</td>
    </tr>
    <tr>
      <td>11.13 Circuit for ↑ p</td>
      <td>125</td>
    </tr>
    <tr>
      <td>11.14 Circuit for p\s</td>
      <td>125</td>
    </tr>
    <tr>
      <td>11.15 The global environment</td>
      <td>126</td>
    </tr>
    <tr>
      <td>11.16 Circuit for program P2</td>
      <td>127</td>
    </tr>
    <tr>
      <td>12.1 Circuit for sustain s = (!s; 1)*</td>
      <td>130</td>
    </tr>
    <tr>
      <td>Program P16</td>
      <td>130</td>
    </tr>
    <tr>
      <td>12.2 Incorrect basic circuit for (!s; (0 | 1))*</td>
      <td>131</td>
    </tr>
    <tr>
      <td>Program P17</td>
      <td>132</td>
    </tr>
    <tr>
      <td>12.3 Incorrect basic circuit for (((s?!o,0); 1; !s)\s)*</td>
      <td>133</td>
    </tr>
    <tr>
      <td>12.4 Correct circuit for (!s; (0 | 1))*</td>
      <td>135</td>
    </tr>
    <tr>
      <td>12.5 Correct circuit for (((s?!o,0); 1; !s)\s)*</td>
      <td>136</td>
    </tr>
    <tr>
      <td>Program P18</td>
      <td>138</td>
    </tr>
    <tr>
      <td>12.6 Multiple incarnations: program P18</td>
      <td>138</td>
    </tr>
    <tr>
      <td>Program P19</td>
      <td>141</td>
    </tr>
  </tbody>
</table>
# Preface

We present the reference semantical framework for the synchronous programming language Esterel, which we call the constructive framework. After a detailed explanation of the causality issues in the language and an intuitive presentation of constructiveness, we show the equivalence between three semantics: the constructive behavioral semantics, the constructive operational semantics, and the electrical semantics, which is based on a translation of Esterel programs into digital circuits. The main full abstraction result is that an Esterel program is constructive if and only if its possibly cyclic circuit reaches electrical stabilization in bounded time. The constructive semantics supersedes all previous semantical attempts for the definition of Esterel, while remaining perfectly compatible with them. The constructive semantics is compositional, unlike its predecessors.

The constructive semantics is implemented in the Esterel v5 compiler. This new compiler accepts all programs accepted by the previous Esterel v3 and v4 compiler, as well as all the constructive programs these compilers reject.

*This draft book is directed to the users of Esterel who want to understand the underlying language and semantics design, and, more generally, to the readers who are interested in language semantics. It complements the general presentation of Esterel called "The Foundations of Esterel", see [8], the Esterel Primer, [7], and the Esterel v5 Systems Manual [12]. Our central aims are to explain the design and properties of the constructive semantics, which, to our belief, should be the final one, to make causality issues understandable, a thing that has long been missing, and finally to fully explain the translation of Esterel programs into circuits.*

In the former releases 1.1 and 2.0 of this book, there were subtle bugs in the behavioral semantics rules. Please accept my apologies, and throw away copies. Fortunately, the circuit translation was already correct and so was the compiler. The bug in version 2.0 was found by Delphine Terrasse (now Kaplan), who tried to prove the correctness of the circuit translation using the COQ proof-checker [40]; many thanks to her. Some other minor mistakes have also been corrected.

The operational semantics was presented in version 1.0, but removed from version 1.1 and 2.0. This is because the author designed a much improved version but had no time to write it down yet; so far, he has chosen to favor the development of the v5 system over the writing of this book. Hopefully, the
operational semantics will be included in the next release. The other missing
parts concern the extension to data-handling and the implementation issues.

**Acknowledgements:** Our work on the constructive semantics owes much to Frédéric Boussinot, from École des Mines, Olivier Ploton and Robert de Simone, from INRIA, Tom Shiple, from Synopsys, and Ellen Sentovich, from Cadence. Many thanks to Ellen Sentovich, Emmanuel Ledinot (from Dassault Aviation), and John Plaice, who performed a careful proof-reading.

Comments from readers are very welcome. Please send them
by e-mail to berry@sophia.inria.fr.
# Chapter 1

# Introduction

Esterel [11, 14, 4, 5] is an imperative synchronous parallel programming lan-
guage dedicated to reactive systems [22]. Esterel is tailored for programming
hardware or software synchronous controllers for which the control-handling
aspects are predominant. Esterel programs are input-driven: they wait for
inputs and compute corresponding outputs in a cyclic manner. An input-
output computation is called a reaction. Synchrony conceptually means
that reactions take no time, or, equivalently, that outputs become available
as inputs become available. By abstracting away reaction times, synchrony
reconciles concurrency and determinism, and it greatly simplifies controller
programming. Furthermore, it becomes possible to use sophisticated imple-
mentation, optimization, and verification techniques commonly used in areas
such as process calculi or hardware design, and to extend them to software
applications [22, 41].

Other synchronous languages are the graphical languages Argos [29] and SyncCharts [1], also dedicated to controllers, the data-flow languages Lustre and Signal, and the TCCP timed concurrent constrained programming language of [35]. See [22] for a comprehensive survey of Esterel, Argos, Lustre, and Signal. Although it is not fully synchronous, Harel's Statecharts graphical formalism [25] clearly belongs to the same language family<fnref n="1" />

This book is devoted to the formal semantics of Esterel and to the trans-
lation of Esterel programs into Boolean circuits, upon which the current
Esterel hardware or software compiling and verification technology is based.

<footnote n="1">¹One can indeed see Maraninchi’s Argos formalism as a simplification of Statecharts with a fully synchronous semantics and André’s SyncCharts as an extension of Argos towards the greater expressive power of Esterel. Since SyncCharts can be translated into Esterel, its semantics is covered by this book.</footnote>
The book should serve as a reference manual for the language semantics and for the Esterel compiling algorithms. We shall not discuss programming style or adequacy to practical applications, this being done elsewhere. See [8] for a general overview, see [7] for the Esterel Manual, and [22, 2, 13, 3, 10, 32, 27] for examples.

The book concentrates on Pure Esterel, which is restricted to pure signaling. Pure Esterel is enough to express all the semantical difficulties and their solution. The extension to the full Esterel language that handles data of arbitrary data types will only be outlined; if not entirely straightforward, it raises no particularly difficult problems.

## The Constructive Semantics

The main semantics we present is called the *constructive semantics*. It is a major improvement over previous semantics discussed in [11, 5], since it solves the *causality problem* common to all synchronous formalisms, although particularly acute in Esterel. Many Esterel users have suffered from the insufficiencies of the previous attempts, and we hope that the constructive semantics will make them happy.

The constructive semantics is presented in several variants, which are shown to be equivalent. The variants serve different purposes. The *constructive behavioral semantics* is the simplest and the most abstract one. Its main use is to formally define what a program means. It is effective and it could be directly used to build interpreters and compilers; however, these would be very inefficient. The *constructive operational semantics* is a microstep semantics, which analyzes the fine structure of control and signal propagation in the reaction. It extends the original operational semantics of [11], which was used in the Esterel v3 compiler. The *circuit semantics* translates an Esterel program into a constructive Boolean circuit. It is the basis of the current Esterel v5 implementation.

The translation into a circuit avoids the state explosion problem, which occurred when translating Esterel programs into explicit automata, as in Esterel v3. Circuits can be directly implemented in hardware, or they can be simulated for software implementation. The vast amount of work on circuit optimization and verification can be used to optimize and verify hardware or software implementations of Esterel.

The path from the constructive behavioral semantics to the circuit semantics is not a trivial one, and half of the book is devoted to its formalization and correctness proof. The final result we obtain is that an Esterel
program is constructive if and only if its circuit electrically stabilizes for all gate and wire delays, this even if the circuit has combinational cycles. This result deeply roots our constructive approach in the physics of electronic designs.

The semantical study of Esterel we present is mostly implementation-oriented and it does not cover all possible fields of interest. All our semantics explain what happens within one reaction and handle sequences of reactions using state changes. We do not discuss *denotational semantics* where a program is directly seen as a flow transformer, forgetting about internal states. Such semantics are useful when dealing with compositionality issues and when mixing Esterel programs with programs written in synchronous data-flow languages, which is outside the scope of this book. Denotational semantics can be indirectly derived from the circuit translation, since defining the denotational semantics of circuits is easy. The reader interested in a direct denotational semantics can refer to G. Gonthier's thesis [18]. We do not discuss either *axiomatic semantics* where one is interested in characterizing term equality using algebraic rewrite rules. Such semantics are useful for program transformation and for proofs by rewriting. The axiomatic theory of Esterel remains to be done.

# A Short Overview

The book consists of four parts: informal presentation, structural operational semantics, circuit translation, and implementation.

## Part I: Informal Presentation

Chapter 2 describes the kernel of Pure Esterel: no-op statement "nothing", signal broadcasting "emit S", signal test "present S then p else q end", suspension "suspend p when S", sequencing "p; q", looping "loop p end", explicit concurrency "p||q", unit delay "pause", a "trap-exit" exception mechanism compatible with concurrency, and the local signal declaration "signal S in p end". The intuitive semantics describes instantaneous signal broadcasting and control transmission. Its cornerstone is the *signal coherence law*, which expresses that a signal is present in a reaction if and only if it is explicitly emitted in this reaction.

Chapter 3 discusses *logical correctness* of programs, which is the conjunction of *reactivity* and *determinism*. Reactivity is the ability to react to any input, while determinism is uniqueness of the reaction. Both properties
and control. Intuitively, a signal S must be emitted if some “*emit S*” statement must be executed, and it cannot be emitted if no such statement can be executed. A signal is set present if and only if it must be emitted, and it is set absent if and only if it cannot be emitted. Facts about signals feed-back to control: for example, in a test “*present S then p else q*”, if S is known to be present, then p must be executed and q cannot be executed. In turn, these facts make it possible to determine new signal statuses, and so on. The constructive analysis accepts all sensible cyclic programs. it rejects the aforementioned logically correct but counter-intuitive program P9, since the unique consistent signal status cannot be computed by fact-to-fact propagation but only as a self-justified hypothesis.

In the terminology of proof theory [17], the logical behavioral semantics is an extensional logic of presence or absence values, while its constructive version is an intensional logic of presence or absence proofs. This is very much in the spirit of constructiveness in the Curry-Howard isomorphism [17], but in a much simpler setting. This analogy explains why we call our new semantics a constructive one.

Using simple examples, Chapter 4 briefly presents the different technical approaches to constructiveness we shall deal with. It also includes a comparison with previous attempts to solve the causality problem.

# Part II: Structural Operational Semantics

All the formal semantics presented in this part define what happens in an instant. They are given in Plotkin's Structural Operational Semantics [34] inference-rule style. To enhance the readability of semantic definitions, we replace the original keyword-based syntax by an equivalent but terser process-calculus syntax, presented in Chapter 5 and first defined in [5].

Chapter 6 presents the formal definition of the *logical behavioral semantics* and defines what it means for a program to be reactive and deterministic. The inference rules define a reaction of a program *P* to an input *I* as an atomic transition *P* →<sub>*I*</sub> *P*', where *O* is the output and *P'* is the program that will execute the next reaction. The signal coherence law is embodied in two rules for local signal declaration, one for presence and one for absence. Reactivity and determinism are not built in since the two signal rules are not disjoint; they are imposed as additional conditions. Although the logical behavioral semantics accepts too many programs, it still plays an important safeguard role since any other semantics must be a refinement of it.
Chapter 7 presents the *constructive behavioral semantics*, which also defines atomic transitions $P \stackrel{O}{\rightleftharpoons}_I P'$. It is obtained by augmenting the logical behavioral semantics by the *must* and *cannot* predicates, which are defined inductively on statements. All the rules of the logical behavioral semantics are kept unchanged, except the signal presence rule, which receives the side-condition “S must be present”, and the signal absence rule, which receives the side-condition “S cannot be present”. The accepted programs are called *constructive* ones. We show that any constructive program is reactive and deterministic.

The simplicity of the logical and constructive behavioral semantics is offset by the need to change the program text from *P* to *P'* to handle the next reaction. In the *state* logical and constructive behavioral semantics presented in Chapter 8, we replace the rewriting by a much simpler marking of active delays in the original program, thereby defining a program state. This is just what we do in the Esterel v5 symbolic debugger. The state semantics are more practical, but the number of rules is roughly doubled. Both state semantics are shown to be equivalent to their rewriting counterparts, which proves in passing that Pure Esterel programs are finite-state.

Chapter 9 is devoted to the *constructive state operational semantics*. This semantics defines a reaction as a sequence of microsteps, where each microstep is either an elementary control transmission or the setting of a signal status. Parallel statements interleave the microsteps of their branches. The recursive computation of the *must* predicate is replaced by the actual execution of statements, which makes it much more efficient and somewhat more natural. However, the operational semantics is technically much more complex than the behavioral one. In particular, because of interleaving, there are several possible microstep sequences for a reaction. The main theorem refers to confluence and strong normalization: all microstep sequences yield the same result, in which all signal statuses are determined if and only if the program is constructive. It follows that the constructive operational semantics is equivalent to the constructive behavioral one.

## Part III: Circuit Translation

In Chapter 10, we define the notion of a constructive circuit. Unlike classical circuits [21], which may not have cycles in their combinational part, constructive circuits are allowed to have combinational cycles. Constructiveness is exactly the characterization of safe cycles. We characterize constructive circuits in three equivalent ways: proof-theoretic, denotational, and electrical.
Building up on work by Brzozowski and Seger [15], Shiple [38, 39] has shown the following fundamental result guessed by the author: a possibly cyclic circuit is logically constructive if and only if, in any physical implementation into wires and gates, all wires stabilize in bounded time to a voltage encoding either 0 and 1, this for any electrical propagation delay in the wires and gates<fnref n="3" />. The result implies that constructive cyclic circuits can be used exactly as acyclic ones in synchronous circuit design.

In Chapter 11, we informally present the basic structural translation idea: to translate a statement, we first translate its substatements and we connect them by appropriate gates and wiring. The translation is explained by pictures. It improves the original translation of [4], which turns out to be inaccurate in the constructive setting.

The basic translation is relatively simple, but it does not work for all programs because of a rather intricate phenomenon we call *schizophrenia*. The problem is due to the possibility of reincarnating a statement several times in a reaction by instantaneously looping loops. We could avoid schizophrenia by restricting the class of programs we translate, but we do not like the idea of restricting the language. In Chapter 12, we carefully analyze schizophrenia and we find a cure for it: logic duplication.

The final translation is formalized and proved correct in Chapter 13. There, we use a textual presentation of (hierarchical) circuits, since logic duplication makes pictures too difficult to draw. The main theorem is that constructiveness of an Esterel program is equivalent to constructiveness of its circuit. The proof idea is that propagation of 1's in the circuit mimics the computation of the *must* predicate, while propagation of 0's mimics the computation of the *cannot* predicate. In other words, the translation directly implements the semantic rules of the behavioral semantics using simple Boolean gates.

## Part ??: Implementation

*Yet to be written. Will be shortly presented: an interpreter for constructive circuits. A compiler that uses BDD algorithms to check for constructiveness. Hardware circuit optimization. Extension to the full language. Software implementation and optimization.*

<footnote n="3">³In the up-bounded inertial delay model of [15].</footnote>
# Part I

## Informal Presentation
<figure><img src="image_2.png" /></figure>
# Chapter 2

## The Pure Esterel Kernel
Language

This section describes the kernel language and its intuitive semantics. It can be skipped by the experienced Esterel user.

### 2.1 Signals and Reactions

Esterel deals with broadcast signals. In most of this book, we limit ourselves to the Pure Esterel sublanguage, where the information carried by a signal is limited to a presence / absence status. In the full Esterel language, signal can also carry values of arbitrary types.

A Pure Esterel program or *module* has an input-output signal interface and an executable body, which is an imperative statement:

```
module M:
input names;
output names;
statement
end module
```

An *input event* specifies the presence / absence status of each input signal. A Pure Esterel program reacts to an input event by computing an *output event*, i.e. by assigning a status to each output signal. The reaction is conceptually instantaneous, and a reaction is also called an *instant*.

Reacting instantaneously is done repeatedly for input event sequences, also called *input histories*, thus generating *output histories*. The reaction to
an input history is "sequential" in hardware terminology: an Esterel program has a *state*, which is implicitly encoded in its executable body. The reaction to an input event provokes a state change, and the reaction to the next input in an input history is computed from the new state.

## 2.2 Kernel Esterel Statement

Pure Esterel statements are divided into *kernel statements*, which form the Kernel Esterel primitive core of the language and *derived statements*, which make programming more convenient but are definable as combinations of kernel ones. As far as semantic issues are concerned, only kernel statements matter. The kernel language we consider is that of [5]:

nothing
emit S
pause
present S then p else q end
suspend p when S
p; q
loop p end
p || q
trap T in p end
exit T
signal S in p end

By default, `;` binds tighter than `||`. One can use brackets `['` and `]']` to group statements in arbitrary ways. Both the `then` and `else` parts are optional in a `present` statement. If omitted, they are assumed to be `nothing`.

The statements are imperative and manipulate control flow and signal status. Most of them are classical in appearance. The `trap-exit` combination defines an exception mechanism fully compatible with parallelism. Traps are lexically scoped. The local signal declaration `"signal S in p end"` declares a lexically scoped signal `S`, which can be used for internal broadcast communication within `p`.

## 2.3 The Intuitive Semantics

We describe how signals are emitted and how control is transmitted between statements.
The status of an input signal is only determined by the input event. Explicit emission of an input signal by `emit I` is disallowed.

The status of a local or output signal is determined on a per-instant basis. In each instant, the status is absent by default. The only way to set a signal `S` present in an instant is to execute an `emit S` statement.

A statement can *start* in some instant; it then remains *active* within the instant and possibly for some further instants until it relinquishes control, either by terminating or by exiting a trap. The only way for a statement to stay active from one instant to the next one is to explicitly execute a *pause* statement, which pauses for exactly one instant. For example, consider the following statement:

```
trap T in
loop
    present I then
        emit O;
        pause
    else
        exit T
end
end
end
```

When started, the statement emits `O` if `I` is present, and it reproduces this behavior until the first instant where `I` is absent, where it terminates instan- taneously. Termination is provoked by executing the `exit T` statement, which provokes instantaneous termination of the enclosing `trap T` statement. Notice that the statement terminates instantaneously when started if `I` is initially absent. Notice also that the internal state encoded by the activity of the *pause* statement propagates from one instant to the next one.

Besides *pause*, all constructs propagate control in an instantaneous (or combinational) way. Signals are also broadcast and tested instantaneously. A statement that terminates or exits a trap in the same instant it starts is said to be *instantaneous*.

The intuitive semantics is defined by structural induction on statements:

* `nothing` terminates instantaneously.

* `pause` pauses in the current instant and terminates in the next instant. The pause statements act as state variables.
* An `emit S` statement instantaneously broadcasts the signal `S`, i.e. sets its status to present and terminates instantaneously. The emission of `S` is transient, i.e. valid for the current instant only.

* When a `present S then p else q end` statement starts, it immediately starts `p` if `S` is present in the current instant; otherwise it starts `q` if `S` is absent.

* In the `suspend p when S` suspension statement, `S` is called the *guard*. The *guard* controls execution of the body in each instant except for the first one, where it is ignored (masked in common terminology). In the initial instant, the body `p` is started; if `p` terminates or exits a trap, so does the *suspend* statement, and the *guard* is transparent. Interesting things only happen in the following instants if `p` paused in the first instant. Then, as long as `p` remains active, the *guard* signal `S` is tested for presence.

- If `S` is present, then `p` is not executed in the instant and it is kept frozen for the next instant. The whole *suspend* statement pauses. In this case, we say that `p` is *suspended* for the instant.

- If `S` is absent, then `p` receives the control for the instant. We say that `p` is *activated* for the instant. If `p` terminates or exits a trap, so does the *suspend* statement. If `p` pauses, then the *suspend* statement also pauses.

In other words, when `S` is present, we “steal the clock” from `p`. Notice that a *suspend* statement remains active until its body terminates or exits a trap, which can only occur in the first instant or in successive instants during which `S` is absent.

* When started, a sequence `p; q` immediately starts `p` and behaves as such as long as `p` remains active. If and when `p` terminates, control is passed instantaneously to `q`, which determines the behavior of the sequence from then on. If and when `p` exits a trap `T`, so does the whole sequence, `q` being discarded in this case. Notice that `q` is never started if `p` always pauses. Notice also that `emit S1; emit S2` emits `S1` and `S2` simultaneously and terminates instantaneously.

* When started, `loop p end` immediately starts its body `p`. If and when `p` terminates, it is immediately restarted. If `p` exits a trap, so does the whole loop. The body of a loop is not allowed to terminate
instantaneously when started; it must execute either a **pause** or an **exit** statement. A **loop** statement never terminates, but it is possible to escape from the loop by enclosing it within a **trap** and executing an **exit** statement.

* When started, a parallel statement `p || q` immediately starts *p* and *q* in parallel. The parallel statement remains active as long as one of its branches remains active, unless some branch exits a trap. The parallel statement terminates instantaneously if and when both *p* and *q* are terminated. The branches can terminate in different instants, the parallel waiting for the last one to terminate. Parallel branches may simultaneously exits traps. If, in some instant, one branch exits a trap *T* or both branches exit the same trap *T*, then the parallel exits *T*. If both statements exit distinct traps *T1* and *T2* in the same instant, then the parallel only exits the *outermost* of these traps, the other one being discarded.

* The statement `trap T in p end` defines a lexically scoped exit point *T* for *p*. When the *trap* statement starts, it immediately starts its body *p* and behaves as *p* until termination or exit. If *p* terminates, so does the *trap* statement. If *p* exits *T*, then the *trap* statement terminates instantaneously. If *p* exits an enclosing trap *U*, this exit is propagated by the *trap* statement.

* An `exit T` statement instantaneously exits the trap *T*. The corresponding *trap* statement is terminated, unless an outermost trap is concurrently exited (see the parallel and *trap* statements above).

* When started, the statement `signal S in p end` immediately starts its body *p* with a fresh signal *S*, overriding any that might already exist. The statement behaves as its body until termination or exit, except that the status of the local signal *S* is not exported.

## 2.4 Comparison with Previous Kernels

There are slight technical differences with the original kernel language and semantics of [11, 4]. We describe the differences and show how to recover the old kernel from the new one. This is an interesting exercise in Kernel Esterel programming.
* In the above presentation, a statement can exit at most one trap. If both branches of a parallel statement exits traps, then the parallel statement exits only the outermost one. In [11], a statement could exit a set of traps and the `trap` statement did the sorting. Both solutions are equivalent, but the new one has the technical advantage of yielding a nice numerical encoding of traps, see Chapter 5.

* The original `halt` statement, which pauses forever, is replaced by the `pause` statement, which pauses for one reaction only; `halt` is recovered as `loop pause end`.

* The original kernel used the `do p watching S` watchdog statement, which behaves as its body $p$ until the first following instant where $S$ occurs, where the whole watchdog statement terminates without transferring control to $p$ in this instant. The `watchdog` construct is used to abort the body when an event occurs. In the kernel, it is now replaced by the semantically simpler and more powerful `suspend p when S` suspension statement, which suspends its body instead of aborting it, see [5]. Recovering the `do p watching S` statement is a good example of kernel expansion:

```
trap T in
    suspend p when S;
    exit T
||
loop
    pause;
    present S then exit T end
end
end
```

The first parallel branch suspends the watchdog's body when $S$ is present, and, otherwise, it exits $T$ if $p$ terminates to propagate termination. The second branch makes the whole expansion terminate when $S$ occurs. The instantaneous combination of suspension and trap exit has the intended effect.

* In [11, 4], we assumed the existence of an always present `tick` signal. The new `pause` statement could be written `await tick`, i.e. `do halt watching tick`. If needed, the `tick` can now be derived as a local signal by executing
loop
    emit tick;
pause
end

in parallel with the module's body.
# Chapter 3

## Logical Correctness

The intuitive semantics specifies what should happen when executing a program, but it does not guarantee that an execution actually exists and is unique. Indeed, we shall need extra criteria for this to happen. In this chapter, we study the apparently simplest possible criterion, *logical correctness*.

In the intuitive semantics, we said that a signal S is absent by default and present if an “*emit S*” statement is executed. Let us rephrase this requirement in a more logical style, getting rid of imprecise notions such as “default” behaviors:

**The Logical Coherence Law:** *A signal S is present in an instant if and only if an “*emit S*” statement is executed in this instant.*

Logical correctness is simply the requirement that there exists exactly one status for each signal that respects the coherence law. Of course, there is a strong relationship between signal status and control propagation: a signal status determines which branch of a *present* test is executed, which in turn determines which *emit* statements are executed.

We shall see that paradoxical statements can be written between control and signals. All the problems we shall mention appear only within instantaneous reactions. Program states do not add extra complexity; they will be ignored until we present the formal treatment, from Chapter 6 on.

We begin by intuitively defining logical correctness of Esterel programs. We then give examples of logically correct and incorrect programs. Finally, we show that composing several logically incorrect programs may result in a logically correct one.
## 3.1 Logical Correctness

Consider a fixed program and a fixed input event. Given a global status, i.e. a status for each signal of the program respecting the given input event, the flow of control is entirely determined and each `emit` statement is known to be either executed or not executed. Therefore, one can check whether the coherence law is respected for each signal: the global status is logically coherent iff at least one `emit` statement is executed for each signal assumed present and no `emit` statement is executed for each signal assumed absent.

We say that the program is *logically reactive* (resp. *logically deterministic*) w.r.t. the input event if there is at least (resp. at most) one logically coherent global status. We say that the program is *logically correct* w.r.t. the input event if it is both logically reactive and deterministic. We say that a program is logically correct if it is logically correct w.r.t. all possible input events.

Pure Esterel programs can be analyzed for logical correctness by performing exhaustive case analysis. Given the status of each input signal, one can make all possible assumptions about the global status and check them individually. Therefore, logical correctness is decidable.

## 3.2 Examples of Logically Correct Programs

Our first example is the following Esterel program P1:

```pseu
module P1:
input I;
output O;
signal S1, S2 in
    present I then emit S1 end
||
    present S1 else emit S2 end
||
    present S2 then emit O end
end signal
end module
```

The program P1 has no internal state, and only its first reaction matters. It is easy to check that P1 is logically correct for all inputs:

* If I is present, the unique logically coherent assumptions are S1 present, S2 absent, and O absent. According to these assumptions,
the first **present** statement takes its **then** branch, the second **present** statement takes its empty **then** branch, and the third **present** statement takes its empty **else** branch. The "**emit S1**" statement is executed, justifying the assumption **S1** present. No "**emit S2**" and "**emit O**" statement are executed, justifying the assumptions **S2** absent and **O** absent. It is easy to check that no other assumptions are logically coherent.

* If I is absent, the unique logically coherent assumptions are **S1** absent, **S2** present, and **O** present. According to these assumptions, the first **present** statement takes its empty **else** branch, the second **present** statement takes its **else** branch, and the third **present** statement takes its **then** branch. The "**emit S1**" statement is not executed, justifying the assumption **S1** absent. The "**emit S2**" and "**emit O**" statement are executed, justifying the assumptions **S2** present and **O** present. It is easy to check that no other assumptions are logically coherent.

Our second example P2 is slightly more intricate since it involves a **pause** statement:

```pascal
module P2:
  signal S in
    emit S;
  present O then
    present S then
      pause
    end;
    emit O
  end
end signal
```

Notice that P2 is inputless. Inputless programs react on empty input events, i.e. on "clock ticks". The only logically coherent set of assumptions is **S** present and **O** absent. The "**emit S**" statement is executed, justifying the assumption **S** present. The "**present O**" statement takes its empty **else** branch, which implies that the "**emit O**" statement is not executed, justifying the assumption **O** absent. All other assumptions are incoherent as follows. Since the "**emit S**" statement is executed whatever assumption we make, an assumption where **S** is absent is incoherent. Now, assume **S** present
and `0` present. Then both `present` statements take their `then` branches and the `pause` statement is executed, which implies that the `"emit 0"` statement is not executed in the instant, contradicting the assumption `0` present.

## 3.3 Examples of Logically Incorrect Programs

We now turn to logically incorrect programs. The following inputless program `P3` is the simplest example of a non-reactive program :

```python
module P3:
    output 0;
    present 0 else emit 0 end
    end module
```

Clearly, no logically coherent assumption can be made for `P3`:

* Assuming `0` present is not justified, since the `"emit 0"` statement is not executed.

* Assuming `0` absent is not justified, since the `"emit 0"` statement is executed.

The next program `P4` is the simplest example of a nondeterministic program:

```python
module P4:
    output 0;
    present 0 then emit 0 end
    end module
```

For `P4`, there are two logically coherent assumptions:

* Assuming `0` present is justified since the `"emit 0"` statement is executed.

* Assuming `0` absent is justified since the `"emit 0"` statement is not executed.

To make examples shorter, we omit input-output declarations from now on. Inputs will be written `I`, `I1`, etc., and outputs will be written `O`, `O1`, etc.

Logical coherence problems may involve several signals. The following program `P5` is non-reactive:
module P5:
    present 01 then emit 02 end
||
    present 02 else emit 01 end

The case analysis shows that no assumption is logically coherent.

The following program P6 is nondeterministic:

module P6:
    present 01 then emit 02 end
||
    present 02 then emit 01 end

For P6, simultaneous presence or absence of 01 and 02 are logically coherent assumptions. It is interesting to try all combinations of then and else in the above examples; we leave this to the reader.

The next example P7 involves a pause statement:

module P7:
    present 0 then pause end;
    emit 0

This program is non-reactive:

* Assume 0 absent. Then, the present statement takes its empty else branch and terminates. The "emit 0" statement is executed, violating the assumption.

* Assume 0 present. Then, the present statement takes its then branch and pauses. The "emit 0" statement is not executed, violating the assumption.

The example P8 below shows that coherence analysis can be quite intricate when traps are involved:

module P8:
    trap T in
        present I else pause end;
        emit 0
    ||
        present 0 then exit T end
    end trap;
    emit 0
The program P8 is logically correct for I present, but it is logically non-deterministic for I absent.

* Consider the case I present. The only logically correct assumption is O present. Under this assumption, the "present I" statement takes its empty then branch and terminates, and the first "emit O" statement is executed, which suffices in justifying the assumption. The second present statement takes its then branch, the trap T is exited, the trap statement terminates, and O is reemitted, which is no problem. The opposite assumption O absent is incoherent since the first "emit O" is executed.

* Consider the case I absent. Whichever assumption we take for O, the pause statement of the first branch is executed, the enclosing present statement pauses, and the first "emit O" is not executed. Surprisingly, both assumptions O present and O absent are logically coherent:

- Assume O present. Then, the second parallel branch exits the trap T, the trap statement terminates, and the last "emit O" statement is executed, which justifies the assumption.

- Assume O absent. Then, the second parallel branch terminates without executing the exit statement and trap T is not exited. The parallel statement does not terminate since its first branch does not, and the trap statement does not terminate since its body does not. This implies that the last "emit O" statement is not executed. Since neither "emit O" statement is executed, the assumption O absent is coherent.

Replacing "then" by "else" in the second parallel branch would yield a program with no logically coherent behavior.

## 3.4 A Strange Logically Correct Program

Our last example P9 shows that composing programs can lead to counter-intuitive phenomena. The program is as follows:
module P9:
    present 01 then emit 01 end
    ||
    present 01 then
        present 02 else emit 02 end
    end

The first parallel branch is a copy of the nondeterministic program P4, while the second branch contains a copy of the non-reactive program P3 enclosed in an apparently innocuous "present 01" statement. Surprisingly enough, P9 is reactive and deterministic, since there is only one logically coherent assumption: 01 absent and 02 absent. With this assumption, the first present 01 statement takes its empty else branch, which justifies 01 absent. The second "present 01" statement also takes its empty else branch, and "emit 02" is not executed, which justifies 02 absent. Disproving the other assumptions is left to the reader.
# Chapter 4

## The Constructive Approach

Logical correctness is a sound semantics for Esterel. However, we have two strong reasons to reject it as the basis of the language. The primary reason is lack of fidelity to the programmer's intuition. A secondary but practically important reason is computational complexity. In this chapter, we present the constructive semantics, which solves both problems.

### 4.1 External Justification Versus Self-justification

In practice, programming in Esterel consists of analyzing input events to generate appropriate output signals, and using concurrent statements and intermediate local signals to create modular, well-structured programs. The programmer's natural way of thinking is in terms of information propagation by *cause and effect*. For example, in the statement

```
present I then
    emit O
end
```

the presence of I causes that of O, and the absence of I causes that of O.

Clearly, the programs P1, page 28, and P2, page 29, are well behaved as far as information propagation is concerned. For example, in P1 with I present, information is propagated as follows: the *then* branch of the first *present* statement is taken, S1 is emitted and therefore present; the *else* branch of the second *present* is not taken, and the only “emit S2” statement is not executed, which implies that S2 is absent; the only “emit O” statement is not executed, and O is absent. There is no need to study the other assumptions about S1, S2, and O.
On the other hand, in the logically correct program P9 that ends Chap-
ter 3 (page 33), there is no natural information propagation. The logically
coherent set of assumptions 01 absent and 02 absent happens to be self-
justified: for instance, the 01 absent assumption is valid since "emit 01"
is not executed, a fact that itself follows from the starting assumption 01
absent. Logical correctness of P9 only follows from the fact that no other set
of assumptions is self-justified.

In our opinion, accepting P9 as correct is logically possible, but not in ac-
cordance with the *intention* of the language, i.e. with its intuitive semantics
and with the intended sequential<fnref n="1" /> character of test statements. In an im-
perative language such as Esterel, when we write “present S then *p* end”,
we obviously mean “*first* test the status of S, *then* execute *p* if S is present”,
assuming that the status of S should not depend on what *p* might do. The
ordering implicit in the *then* word is not that of time, since everything is con-
ceptually instantaneous, but that of sequential causality. We want to allow
actual computation of the form “since S is present, we take the *then* branch”
and to forbid speculative computation such as “if we assume S present, then
we take the *then* branch”. Aside from the explicit concurrency ‘||’, all Es-
terel statements are sequential, and this character should be preserved in the
semantics. Here is an example involving an explicit sequence operator ‘;’:

module P10:
present 0 then nothing end;
emit 0

P10 is logically coherent with 0 present, but we do want to reject it: in the
logical semantics, the information that 0 is present flows backwards across
the sequencing operator, contradicting the basic intuition about sequential
execution.

In the *constructive semantics*, the idea of checking assumptions about
signal statuses is replaced by the idea of *propagating facts* about control flow
and signal statuses. Obviously, the name is borrowed from *constructive logic*,
in which one handles fact-propagating *proofs*, instead of handling values as
in classical logic (see [17]). The analogy will be made formal in Chapter 7
and Chapter 9, where we shall present the new semantics as a constructive
version of logical correctness.

Technically speaking, there are three equivalent ways to present the con-
structive semantics. We begin with the *constructive behavioral semantics*,

<footnote n="1">¹In classical programming terminology, not in hardware terminology!</footnote>
derived from the logical behavioral semantics by adding constructive restric-
tions to the logical coherence rule. It is the simplest way of defining the
language. Then, we present the *constructive operational semantics*, which
is based on an interpretation scheme expressed by term rewriting rules defin-
ing microstep sequences. It is the simplest way of defining an efficient in-
terpreter. Finally, we briefly present the *circuit semantics*, which is based
on a translation of programs into constructive circuits and is the core of the
Esterel v5 compiler.

## 4.2 The Constructive Behavioral Semantics

The *constructive behavioral semantics* retains the spirit of the logical coherence semantics, but it adds reasoning about what a program *must* or *cannot* do, both predicates being disjoint and defined in a constructive way. These disjoint predicates express the following facts respectively:

* A statement *must* terminate, *must* pause, *must* exit a trap T, or *must* emit a signal S.

* A statement *cannot* terminate, *cannot* pause, *cannot* exit a trap T, or *cannot* emit a signal S.

The *must* predicate determines which signals are present and which statements are executed. The *cannot* predicate determines when signals are absent and it serves in pruning out false execution paths. The logical coherence law splits into two constructive sublaws, which are exclusive of each other, thus ensuring determinism at once:

* A signal is declared present if and only if it *must* be emitted.

* A signal is declared absent if and only if it *cannot* be emitted.

The predicates are defined by structural induction on statements, in a way
that respects the sequential character of all primitives besides concurrency.
In the recursive definition of the predicates, a signal can have three sta-
tuses: +, i.e. known to be present, –, i.e. known to be absent, or ⊥, i.e.
yet unknown. Technically, it is easier to define the *cannot* predicate as the
negation of a *can* predicate; there is no constructiveness problem in taking
such a negation since we only deal with finite sets. Here are some examples
of inductive definitions:
* In a sequence "p; q", one must (resp. can) execute *q* if *p* must (resp. can) terminate.

* For a test "present S then p else q end", there are three subcases:

- If S is known to be present, the test behaves as p.

- If S is known to be absent, the test behaves as q.

- If S is yet unknown, the test can do whatever *p* or *q* can do, and there is nothing it must do.

The main subtlety (and novelty) appears in the analysis of output or local
signals. The analysis being the same in both cases, we consider a local signal
declared by "signal S in p end".

First consider the *must* predicate. The idea is as follows. Assume we
already know that we must execute "*signal S in p end*" in some signal
context *E* that defines the status of visible signals. To find in which signal
context *p* must be executed, we must compute the final status of *S*. We first
analyze *p* in *E* augmented by setting the unknown status *⊥* for *S*. If we find
that *S* must be emitted, we propagate this information by re-analyzing *p*
in *E* with *S* present, which may generate more information about the other
signals. Similarly, if we find that *S* cannot be emitted, we re-analyze *p* in *E*
with *S* absent; this is the only place where the *can* predicate is used.

For the *can* predicate, we just recursively analyze *p* with status *⊥* for *S*.
We cannot do any better without performing a speculative computation,
since the *can* predicate can be computed for statements that must not be
executed.

We refer to Chapter 7 for the other statements and the formal definitions.

4.2.1 Accepting Programs

Programs are accepted as constructive ones if and only if fact propagation
using the *must* and *can* (or *cannot*) predicates suffices in establishing presence
or absence of all signals. For example, the constructive behavioral analysis
of P1, page 28, is as follows:

* If I is present, then the first *present* statement must take its first branch, emit S1, and terminate. From this, we deduce that S1 is present. Then, the second *present* statement must take its (empty) *then* branch and cannot take its *else* branch. Since the "emit S2" statement cannot be executed, S2 cannot be emitted, which implies
that S2 is absent. Finally, the third `present` statement cannot take its `then` branch, which implies that `O` cannot be emitted and is absent.

* If `I` is absent, then the first `present` statement cannot take its first branch, and the `emit S1` statement cannot be executed, which implies that `S1` is absent. Therefore, the second `present` statement must take its `then` branch, the `emit S2` statement must be executed, which implies that `S2` is present. Finally, the third `present` statement must take its `then` branch, and the `emit O` statement must be executed, setting `O` present.

Consider now the program P2, page 29, which we recall here for readability:

```pascal
module P2:
output O;
signal S in
    emit S;
    present O then
        present S then
            pause
        end;
        emit O
    end
end signal
```

We first start analyzing what the `signal S` statement must do with status $⊥$ for `O`. For this, we analyze its body with status $⊥$ for `O` and `S`. We immediately find that `S` must be emitted since we must execute the `emit S` statement. Therefore, we redo the analysis with status $⊥$ for `O` and $+$ for `S`. We reach the test for `O`. Since the status of `O` is unknown, there is nothing we must do and we can make progress only by analyzing what we cannot do in the branches of the test. In the `then` branch, there is a `present` test for `S`. Since `S` is known to be present, we cannot take the implicit `else` branch that would terminate. Since the `then` branch is a `pause` statement, it cannot terminate. Summing up things, the `present S` test cannot terminate. Therefore, the `emit O` statement cannot be executed and `O` cannot be emitted. As a consequence we must set `O` absent and redo the analysis of the program with status $-$ for `O`. We now find that we must take the implicit `else` branch of the `present O` test that terminates execution. The program is constructive since we have fully determined the signal statuses.
In the analysis, we never performed speculative computation based on *assumptions* about what we could do. We just propagated already established positive or negative facts. Fact propagation is monotonic: when a fact is established, it can never be contradicted later on.

Of course, the analysis involves tedious recomputation. Once we have set a signal status, we re-analyze the body of its declaration (the whole program for an output), and we re-establish facts we already know. The goal of the operational and circuit semantics is precisely to avoid recomputing known facts.

### 4.2.2 Rejecting Programs

Programs are rejected when the *must* and *cannot* predicates bring no information about the status of some signal. This is the case for the programs P3, page 30, and P4, page 30. For both programs, we find that `O` can be emitted since there are potentially reachable “`emit O`” statements, but that it is not true that `O` must be emitted. Since we cannot make any constructive progress on the status of `O`, we reject the programs. Notice that P3 and P4 are rejected for the very same reason by the constructive semantics, while they were rejected for two different reasons in the logical behavioral semantics, respectively, non-reactivity and non-determinism.

Generally speaking, all logically incoherent programs are rejected. Logically coherent programs can also be rejected as being non-constructive. This is the case for the strange example P9, page 33. For P9, the *can* analysis finds that both `01` and `02` can be emitted, and the *must* analysis finds that no signal must be emitted; since we cannot make any progress, we reject the program.

To understand further which programs are rejected, consider the following variant P11 of P2:

```pascal
module P11:
output O;
signal S in
    present O then
        emit S;
    present S then
        pause
    end;
    emit O
end
end signal
```
The "emit S" statement is now inside the then branch of the "present O" statement. The must analysis with status $⊥$ for O and S finds nothing we must do since we are not allowed to speculatively compute within the branches of the test for O. In the same status, the cannot analysis finds that both S and O can be emitted since it finds potentially reachable emitters. Therefore, we can make no progress and we reject P11.

The following program P12 is also rejected:

module P12:
present O then emit O else emit O end

The constructive analysis finds that O must not be emitted since it is not allowed to speculatively execute the branches of the test. We shall explain strong physical (electrical) reasons to reject P12 in Section 10.

## 4.3 The Constructive Operational Semantics

The constructive operational semantics is defined by a rewriting-based interpretation scheme, which gives a dynamic vision of program execution. Instead of reasoning about what we must do, we just do it. *A priori*, this looks like a better idea. However, the formal definition and technical treatment of the constructive operational semantics is much heavier than that of the constructive behavioral semantics. This is why we take the latter as the primary semantics.

### 4.3.1 Accepting Programs

We begin the intuitive explanation with the example of P1 with input I present. First, we decorate the declaration of each signal with a status in $+$ (present), $-$ (absent), or $⊥$ (unknown). Initially, all signals except inputs are unknown, and the body of the program is started, which is indicated by a bullet:
module P1:
input I+;
output O⊥;
• signal S1⊥, S2⊥ in
  present I then emit S1 end
||
  present S1 else emit S2 end
||
  present S2 then emit O end
end signal

The ternary parallel statement forks three execution threads:

module P1:
input I+;
output O⊥;
signal S1⊥, S2⊥ in
  • present I then emit S1 end
||
  • present S1 else emit S2 end
||
  • present S2 then emit O end
end signal

Such a move of bullets is called a *microstep*, following the terminology of [26].

When encountering a "present S" statement in a thread, we proceed as follows. If S is annotated with +, we transfer control to the **then** branch. If S is annotated with -, we transfer control to the **else** branch. If S is annotated by ⊥, we block until the status of S becomes + or -. Here, only the first thread can continue. Since I is known to be present, we can take the **then** branch of the first test, rewriting the program as follows:

input I+;
output O⊥;
signal S1⊥, S2⊥ in
  present I then • emit S1 end
||
  • present S1 else emit S2 end
||
  • present S2 then emit O end
end signal
In the next microstep, we execute `emit S1` that sets `S1` present and terminates the first branch:

```
input I+;
output O⊥;
signal S1+, S2⊥ in
    present I then emit S1 end •
||
• present S1 else emit S2 end
||
• present S2 then emit O end
end signal
```

Next, we take the implicit `then` branch of the second `present`:

```
input I+;
output O⊥;
signal S1+, S2⊥ in
    present I then emit S1 end •
||
    present S1 else emit S2 end •
||
• present S2 then emit O end
end signal
```

Since there is no more occurrence of `emit S2`, we cannot emit `S2` and we set `S2` absent:

```
input I+;
output O⊥;
signal S1+, S2- in
    present I then emit S1 end •
||
    present S1 else emit S2 end •
||
• present S2 then emit O end
end signal
```

We now take the implicit `else` branch of the last `present` statement:
input I$^+$;
output O$^-$;
signal S1$^+$, S2$^-$ in
  present I then emit S1 end •
||
  present S1 else emit S2 end •
||
  present S2 then emit O end •
end signal

Now, there are no occurrences of "emit O" reachable by the threads, and we cannot emit O any more. We set O absent as expected. Finally, we synchronize the three terminated threads to terminate the whole program:

input I$^+$;
output O$^-$;
signal S1$^+$, S2$^-$ in
  present I then emit S1 end
||
  present S1 else emit S2 end
||
  present S2 then emit O end
end signal
•

The execution of P1 with I absent is similar and left to the reader.

Let us now execute P2, page 29. We start from the following decorated statement:

output O$^-$;
• signal S$^+$ in
  emit S;
  present O then
    present S then
      pause
    end;
    emit O
  end
end signal
In three microsteps, we traverse the local signal declaration, we execute "emit S" that sets S present and we reach the test for O by traversing the sequencing operator:

```
output O⊥;
signal S⁺ in
    emit S;
• present O then
    present S then
        pause
    end;
    emit O
end
end signal
```

Since the status of O is ⊥, control is frozen at the "present O" test and we can perform no further trivial microstep. We now perform a *cannot* analysis just as in the constructive behavioral semantics. The analysis reports that O cannot be emitted. We use a microstep to set it absent:

```
output O—;
signal S⁺ in
    emit S;
• present O then
    present S then
        pause
    end;
    emit O
end
end signal
```

and we terminate execution by taking the implicit `else` branch of the test:

```
output O⁻;
signal S⁺ in
    emit S;
present O then
    present S then
        pause
end;
emit O
end
end signal
•
```
In the operational semantics, we avoid most of the recomputation that take
place in the constructive behavioral semantics. The reason why we can do
this is that statuses evolve in a monotonic way.

4.3.2 Rejecting Programs

Programs are rejected very much in the same way as in the constructive
behavioral semantics, i.e. whenever no progress can be made on signal sta-
tuses. Consider for example P3, page 30. There is no possible initial mi-
crostep, which prevents us from setting the status of 0 to +, and there is a
potential path to "emit 0", which prevents us from setting the status of 0
to -. Since we cannot make progress, we reject the program. All logically
incorrect programs are rejected in the same way, as is the logically correct
strange program P9, page 33.

4.3.3 Summary of the Constructive Interpretation Scheme

The interpretation scheme handles sequential threads of control forked by
parallel statements. Signals are shared objects having a three-valued status
in {+, -, ⊥} and initialized to ⊥, except for input signals, which are initial-
ized according to the input event. The status of a signal S changes from ⊥
to + as soon as an "emit S" statement is executed and from ⊥ to - as soon
as all the "emit S" statements have been found unreachable by the *cannot*
false path analysis. When a thread reaches a "present S" statement, it
remains there, frozen, as long as the status of S is ⊥, and it can resume by
taking the appropriate branch as soon as S has a non-⊥ status. If several
threads are enabled, any one of them can be chosen. Threads are stopped by
termination or by executing *pause* or *exit* statements, and parallel state-
ments synchronize stopped threads, as explained in the intuitive semantics.
Finally, the false path analysis explores all possible instantaneous paths to-
wards *emit* statements, taking into account all facts established so far and
making no speculative reasoning.

Given an input, a program is accepted if the analysis succeeds in setting
each signal status to a defined value + or -. Logical correctness is guaranteed
for accepted programs.

It is not obvious that the result is independent of the order in which
threads are executed and that the constructive operational semantics is
equivalent to the constructive behavioral one. This will be proved in Chap-
ters 9.
### 4.3.4 Comparison With Previous Operational Semantics

The constructive operational semantics can be seen as an improved version of the former operational semantics presented in [11] and used in the Esterel v3 compiler. Technically the improvement is brought by the finer *cannot* analysis that allows us to handle P2, page 29, which was rejected by the operational semantics of [11]. Semantically, the constructive operational semantics is fully equivalent to the constructive behavioral semantics, while the previous operational semantics lacked proper semantical characterization.

## 4.4 The Circuit Semantics

In the circuit semantics, we translate Esterel programs into Boolean digital circuits, i.e. systems of equations between Boolean variables.

In circuits, we deal with a set of Boolean variables split into disjoint subsets of input variables, output variables, and local variables. A circuit must specify an equation for each output or local variables, using either a Boolean expression or a *register* unit-delay operator that we shall ignore in this informal presentation, sticking to what is usually called combinational circuits. A Boolean solution of the equations defines a logical behavior.

### 4.4.1 The Logical Interpretation of Circuits

Given a circuit and an input, there may be no logical behavior, one behavior, or several behaviors. Therefore, we can define logical reactivity and determinism in the same way as for Esterel programs.

Let us re-examine some of the examples of the previous chapter in terms of behavior of Boolean circuits. The program P1, page 28 can be rewritten as follows:

circuit C1:
S1 = I
S2 =¬S1
O = S2

Since C1 defines an acyclic dependency relation between variables, it is trivial that C1 is logically reactive and deterministic. The program P3, page 30, corresponds to the following circuit C2:
circuit C2:
0 = ¬0

This cyclic circuit is not reactive. Similarly, P4, page 30, corresponds to the non-deterministic cyclic circuit "0 = 0".

The program P9, page 33, and P12, page 41, corresponds to the cyclic circuits C9 and C12 below:

circuit C9:
01 = 01
02 = 01 ∧ ¬02

circuit C12:
0 = 0 ∨ ¬0

The circuits C9 and C12 are logically reactive and deterministic, as are P9 and P12.

### 4.4.2 The Electrical Implementation of Circuits

Circuits are usually meant to be implemented using electrical wires and gates composed of appropriately wired transistors. The Boolean values 0 and 1 are represented by distinct voltages, say 0V and 5V. Wires propagate voltages with some delay, and gates compute Boolean functions of voltages with some delay. Electrical circuits are generally pictured using conventional symbols<fnref n="2" />. For example, the circuits C9 and C12 are respectively pictured in Figure 4.1 and Figure 4.2. For an acyclic circuit, such as C1, it is trivial that the output voltage remain stable after some delay if the inputs are kept stable. Stabilization is much less trivial for cyclic circuits. For non-reactive or non-deterministic circuits, one can always find delays such that the outputs never stabilize. The worst case is that of C2, which never stabilizes. For the logically correct circuits C9 and C12, one can find delays for which there is no output stabilization (left to the reader). This already means that electrical stabilization is not the conjunction of reactivity and determinism.

An example of a cyclic circuit that stabilizes for all delays is the following circuit C13, pictured in Figure 4.3:

<footnote n="2">²See Figure 10.1, page 104.</footnote>
<figure><img src="image_3.png" /><figcaption>Figure 4.1: Circuit C9</figcaption></figure>

<figure><img src="image_4.png" /><figcaption>Figure 4.2: Circuit C12</figcaption></figure>

circuit C13:
01 = I ^ 02
02 = not I ^ 01

In C13, the loop is electrically cut at one of the two **and** gates according to the value of I, since a single 0 on an **and** gate input is enough to generate a 0 on the output.

Notice that the non-stabilizing circuits C9 and C12 correspond to the non-constructive Esterel programs P9 and P12, while the stabilizing circuit C13 corresponds to the following constructive Esterel program P13:

module P13:
input I;
output 01, 02;
present I then
    present 02 then emit 01 end
else
    present 01 then emit 02 end
end
<figure><img src="image_5.png" /><figcaption>Figure 4.3: Circuit C13</figcaption></figure>

This suggests to relate constructiveness and electrical stabilization. For this, we need a theory of constructive circuits parallel to that of constructive Esterel programs.

### 4.4.3 Constructive Circuits

The appropriate theory of constructive circuits is presented in [38]. There are three equivalent frameworks for defining circuit constructiveness:

* **Constructive Boolean Logic:** a circuit is constructive for an input if one can compute all the local and output variables by applying the following constructive Boolean laws:

$$ 
\begin{array}{l}
\neg 0 = 1 \\
\neg 1 = 0 \\
0 \land x = x \land 0 = 0 \\
1 \land 1 = 1 \\
1 \lor x = x \lor 1 = 1 \\
0 \lor 0 = 0
\end{array}
$$

and by replacing a variable by its value when this value has been computed. Notice that the excluded middle law "$x \lor \neg x = 1$" is not valid in the constructive calculus unless $x$ has been proved to be 0 or 1, which explains why C12 is not constructive.

* **Denotational Semantics:** we interpret variables in Scott's ordered Boolean domain $B_{\perp} = \{\perp, 0, 1\}$. Given an input, the system of equation defines a monotonic (increasing) function $f$ from tuples of local and output variables to tuples of local and output variables. The circuit is constructive for the input if the least fixpoint $Y$ of $f$ is fully
defined, i.e. if the value of any variable in the tuple $Y$ is different from $\perp$.

* **Electrical Semantics:** we say that a circuit is constructive if, for all gate and wire delays, all wire voltages stabilize in bounded time, provided that the input wires are kept stable at voltages encoding the input values.

The equivalence between these three semantics is a strong full abstraction result that relates logical, denotational, and operational views. Its real strength comes from the physical character of the electrical semantics.

#### 4.4.4 From Esterel Programs to Constructive Circuits

The translation of Pure Esterel programs into circuits is a non-trivial process presented in Chapters 11 through 13. The translation we present extends the original translation of [4] by solving the schizophrenia problem, which we left unsolved in [4]. The solution involves performing appropriate logic duplication. All Esterel programs are now translated. To preserve constructiveness, the priority queue used in the original translation must also be modified in a quite subtle way, see Chapter 11.

The main result is that an Esterel program is constructive if and only if its circuit is. This implies that constructiveness in Esterel exactly corresponds to electrical stabilization: the full abstraction result for circuits also holds for Esterel.

## 4.5 Complexity Issues

In the application class towards which Esterel is targeted, namely hardware or software controllers, users definitely want fast simulation tools able to handle large programs involving hundreds or even thousands of signals. Given a program and an input, such a simulator should either perform the transition or report a semantical error such as non-reactivity or non-determinism. As far as full compilation goes, users can accept comparatively longer compilation and optimization times to generate efficient circuits or embedded software code, but they still want the compiler to take a reasonable amount of time.

Computing whether a program is constructively correct for a given input is efficient. For instance, the execution and false path pruning steps can be
efficiently implemented using pointers from `emit` statements to signals and from signals to `present` statements. Because of the reincarnation problem mentioned in [6], the worst case cost of the analysis of a program of size *n* is *n*². However, the squaring factors appears only for pathological examples, and the cost is roughly linear in practice.

In the Esterel v5 interpreter, we translate a program into a digital circuit and we run a linear-time constructiveness analysis algorithm for each input. Interpretation is very fast. In the Esterel v5 compiler, we analyze constructive correctness for all possible input. The easy case is when the circuit is acyclic, which is found in linear time. Then, the program is automatically correct. To analyze cyclic circuits, we use an algorithm based on Binary Decision Diagrams and presented in [38]. The algorithm is an extension of Malik's original algorithm [28] for sequential circuits. The algorithm checks for constructiveness, and, if it succeeds, returns an equivalent acyclic version of the circuit that can be implemented very efficiently. The current Esterel v5 compiler can handle cyclic programs of industrial size<fnref n="3" />.

As far as logical correctness semantics is concerned, even the simplest problem of computing the reaction of a program to a given input is NP-complete. The exhaustive search method we have presented in Chapter 3 is obviously impractical since it is exponential in the number of signals. Much less naive and more efficient algorithms such as the one presented in [24] can be adapted to Esterel using the translation into circuits. Such heuristic algorithms can work reasonably well on medium-size examples, but their time and space resource requirements are somewhat unpredictable and they will not scale to real-size examples. This is not acceptable for an interpreter.

## 4.6 Constructive Symbolic Debugging

The constructive semantics fits well with symbolic debugging, a must for practical applications of the language. In the Esterel v5 symbolic debugger, we use a coloring scheme to show control and signal status propagation within a reaction. Executed statements and emitted signals are highlighted in green. Replacing green by underlining, the execution of P1 with I present is pictured below:

<footnote n="3">³We are currently working on modular analysis of programs, but it is too early to report on the results.</footnote>
```
input I;
output O;
signal S1, S2 in
    present I then emit S1 end
||
    present S1 else emit S2 end
||
    present S2 then emit O end
end signal
```

The `signal` keyword is underlined since the signal statement is executed. The `|||` statements are underlined since they fork the control. The three `present` statements are underlined since they are executed concurrently. The `then` keyword and branch of the first `present` are underlined since this branch is executed, while the branches of the other two `present` statements are in normal font since they are not executed. The signals `I` and `S1` are underlined since they are present. Since each control thread is strictly sequential, the picture gives complete information about what is executed and what is not.

With `I` absent, the execution is pictured as follows:

```
input I;
output O;
signal S1, S2 in
    present I then emit S1 end
||
    present S1 else emit S2 end
||
    present S2 then emit O end
end signal
```

This form of symbolic debugging also applies to printing appropriate error messages for non-constructive programs. We can paint in red (here, italic) the frozen part of each thread and the signals with status $⊥$. For P3, page 30, the picture is

```
output O;
present O else emit O end
```

The `present` keyword is underlined since the `present` statement is executed. The declaration of `O` is in italic since the status of `O` is $⊥$, and the `then` and `emit` keywords are in italic to show where the thread is frozen.
## 4.7 Comparison with Previous Attempts

The Esterel v2 [9] and Esterel v4 compilers take a restricted topological approach to correctness. Write `S1 → S2` if there is a potential direct control path from a "present S1" statement to an "emit S2" statement, and build a signal dependency graph by gathering all such arrows. The dependency graph is required to be acyclic<fnref n="4" />. All accepted programs are constructively correct.

The topological approach is usually considered adequate for data-flow synchronous languages [23, 20] and manually designed hardware circuits, but it is insufficient for Esterel since it does not take care of false control paths, of inputs, and of states. The correct program P2, page 29, is rejected since there is an arrow `0 → 0`. However, the control path from "present 0" to "emit 0" is a false one, which is detected by the constructive analysis. Program P13, page 49, is also rejected, since there is a static cycle between `01` and `02`. However, P13 is constructive and accepted by Esterel v5.

The following constructive program P14 is also rejected by both Esterel v2 and Esterel v4:

```python
module P14:
    input I;
    output 01, 02;
    present 01 then emit 02 end;
    pause;
    present 02 then emit 01 end
```

As in P13, there is a topological cycle between `01` and `02`, hence the rejection. However, the constructive analysis finds that this cycle is a false one, since the dependency `01 → 02` is only meaningful for the first reaction, while the dependency `02 → 01` is only meaningful for the second reaction; P13 is accepted by Esterel v5.

In Esterel v3 [11], causality analysis is more elaborate and P13 and P14 are accepted. The analysis is performed on a per-state and per-input basis. Given a state and an input, an approximate analysis is run to detect what statements must and cannot do, just as in the constructive analysis. However, there is one difference: when analyzing a `present` statement that tests a yet unknown signal, the information known so far is not used to prune false branches (except for inputs). Because of this limitation, P2, page 29,

<footnote n="4">⁴Esterel v4 actually builds a graph between signal *incarnations*, correctly handling the reincarnation problem presented in [6], which Esterel v2 did not handle.</footnote>
is rejected. All possible states and inputs are explored in a systematic way, building the whole state graph of the program. The main weakness of the technique is that the state graph can become exponential in the size of the program, limiting Esterel v3 to comparatively small programs.

Esterel v5 combines the advantages of Esterel v3 and Esterel v4, without having their drawbacks, while accepting more programs and accepting them for clear semantical reasons. There is no need to build an explicit state graph, as in Esterel v3. Nevertheless, the analysis is done on a per-input and per-state basis, thanks to symbolic BDD-based algorithms presented in [38]. Furthermore, the semantical characterization of accepted programs is constructiveness, which can be viewed in several natural and equivalent ways. Nothing more precise can be said without entering into the formal aspects, which we now do.
# Part II

## Structural Operational Semantics
<figure><img src="image_6.png" /></figure>
# Chapter 5

## The Esterel Process Calculus
Syntax

The keyword-based programming language syntax we have used so far is convenient for actual programming and for presenting examples, but we find it too heavy to be comfortably used in the framework of mathematical semantics. From now on, we use an equivalent terse syntax in which Esterel takes the look and feel of a process calculus. This syntax was first introduced in [5]. The kernel constructs are written as follows:

<table><tr><td>nothing</td><td>0</td></tr><tr><td>pause</td><td>1</td></tr><tr><td>emit S</td><td>!s</td></tr><tr><td>present S then p else q end</td><td>s? p, q</td></tr><tr><td>suspend p when S</td><td>s ⊃ p</td></tr><tr><td>p; q</td><td>p; q</td></tr><tr><td>loop p end</td><td>p*</td></tr><tr><td>p || q</td><td>p | q</td></tr><tr><td>trap T in p end</td><td>{p}<br/>↑ p</td></tr><tr><td>exit T</td><td>k with k ≥ 2</td></tr><tr><td>signal S in p end</td><td>p\s</td></tr></table>

The main differences between the programming language syntax and the terse syntax are the removal of trap names, the introduction of an auxiliary *shift* operator ↑ *p* in conjunction with the trap operator *{p}*}, and the use of integer *completion codes* *k* ≥ 0 to encode the *nothing*, *pause*, and *exit*
statements.

We first explain completion codes. The **nothing** statement is encoded by 0, the **pause** statement is encoded by 1, and the “exit T” statement is encoded by 2 if the closest trap declaration is that of T, and by $n + 2$ if $n$ trap declarations have to be traversed before reaching that of T. This is illustrated on the following example:

```
trap U in
    trap T in
        nothing
        ||
        pause
        ||
        exit T
        ||
        exit U
    end
    ||
    exit U
end
```

which is encoded as follows in the terse syntax:

$$ \{\{0|1|2|3\}|2\} $$

The first “exit U” statement is encoded by 3 since one must traverse the declaration of T to reach that of U, while the second “exit U” statement is encoded by 2 since, in its context, the declaration of U is the closest trap declaration.

The idea of the encoding is as follows. Each control thread returns an integer completion code $k \ge 0$ when it has completed its execution in the instant. The completion code is generated by executing a $k$ statement, i.e. a **nothing**, **pause**, or **exit** kernel statement. Consider a parallel statement $p|q$. If $p$ returns $k$ and $q$ returns $l$, the parallel statement returns the maximum $max(k, l)$ of $k$ and $l$. This takes into account all the synchronization the parallel must perform:

* The parallel terminates if and when both branches have terminated, since $max(k, l) = 0$ is equivalent to $k = l = 0$.

* The parallel pauses if one branch pauses and the other one does not exit a trap, since $max(k, l) = 1$ implies $k = 1$ and $l \le 1$ or vice-versa.
* The parallel exits a trap if one branch does and exits the outermost trap only if both branches exit traps. This follows from the encoding of exit statements that starts from 2 and increases by 1 for each enclosing trap.

Having lost trap names in the terse syntax, we need the auxiliary `↑ p` shift operator, whose semantical effect is to increment by one all the completion codes greater than 1 in `p`, thus ensuring that `{↑ p}` is behaviorally equivalent to `p`. To illustrate the need for that operator, consider the Esterel watching derived statement whose kernel expansion was given in Chapter 2, page 24. In the terse syntax, `do p watching S` is written `s >> p`, and its kernel expansion is rewritten as follows:

$$s \gg p = \{(s \supset \uparrow p) | (1; s \? 2, 0)\}$$

Since the expansion adds an extra trap, it is necessary to write `↑ p` instead of `p` to ensure correct propagation of the exit statements internally executed by `p`.

In addition to the above kernel statements, we shall use the immediate suspension derived statement written `suspend p when immediate S` in the language syntax and `s ⊃ p` in the terse syntax. This statement differs from `s ⊃ p` only for the starting instant. In this instant, the signal `s` is also tested and `p` does not receive the control if `s` is present. The kernel expansion is as follows:

```
trap T in
loop
    present S then
        pause
    else
        exit T
    end present
end loop
end trap;
suspend p when S
```

The loop encodes the full Esterel statement `await immediate [not S]`". In terse syntax, the definition is

$$s \supset p = \{(s \? 1, 2)\}; s \supset p$$
which means “wait until the first instant where *s* is absent, then execute *s* ⊃ *p*”. Finally, we impose a minor restriction on programs that makes semantical definitions simpler: an input signal cannot be internally emitted, i.e. one cannot write !*i* if *i* is an input. This restriction ensures that input statuses are defined by the environment only. Any program that does not obey this restriction can be easily recoded using extra local signals (use one local signal per internally emitted input).
# Chapter 6

## The Logical Behavioral Semantics

This chapter is devoted to the formalization of the logical behavioral semantics. Although we reject this semantics as the basis of Esterel, we want to describe it formally for three reasons. First, it formally defines reactivity and determinism, which are the minimal requirements that any other semantics must obey. Second, it is mathematically simple and elegant. Third, in Chapter 7, we shall present the constructive behavioral semantics as a simple refinement of the logical one, leaving most rules unchanged.

### 6.1 Events

Given a set $S$ of signals, also called a *sort*, an *event $E$* is the definition of a status $b$ in $B = \{+, -\}$ for each signal. The sort of $E$ is written $S(E)$. Technically, we consider $E$ either as the subset of $S$ containing all signals having status $+$, or as a mapping from $S$ to $B$. The status of $s$ in $E$ is written $E(s)$. We write $s^+ \in E$ (resp. $s^- \in E$) if the status of $s$ in $E$ is $+$ (resp. $-$). We write $E \subset E'$ if $s^+ \in E$ implies $s^+ \in E'$ for any signal $s$. Given a signal $s$, the *singleton event* $\{s^+\}$ is defined by $\{s^+\}(s) = +$ and $\{s^+\}(s') = -$ for $s' \neq s$.

Given a signal set $S$ and a signal $s \in S$, we write $S\backslash s = S - \{s\}$. Given $E$ and $s \in S(E)$, we write $E\backslash s$ to denote the event of sort $S(E)\backslash s$ which coincides with $E$ on all signals but $s$.

Given an event $E$ of sort $S$, a signal $s$ possibly not in $S$, and a status $b$ in $B$, we define $E * s^b$ as the event $E'$ of sort $S \cup \{s\}$ defined by $E'(s) = b$
and $E'(s') = E(s')$ for $s' \neq s$. This construct is useful for signal scoping. Notice that the status of $s$ in $E$ is lost in $E * s^b$ if $s \in S(E)$: although declarations of local signals having the same name can be nested, as in $(p \setminus s) \setminus s$, the event $E$ does not need to be a stack since the outermost signal $s$ is not visible in $p$.

## 6.2 Program and Statement Transitions

The behavioral semantics formalize a reaction of a program $P$ as a *behavioral transition* of the form

$$P \xrightarrow{O} P'$$

where $I$ and $O$ are respectively an *input event* and an *output event*. The resulting program $P'$ is called the *derivative* of $P$ by the reaction. It represents the new state reached by $P$ after the reaction. Coding states by program texts is standard in process calculi definitions based on Structural Operational Semantic (SOS) rules [34, 31], which is the style we use here.

Reactions are computed using an auxiliary *statement transition* relation, which has the following form:

$$p \xrightarrow{E', k} p'$$

Here, $E$ is an event that defines the status of all signals declared in the scope of $p$, i.e. an assumption in the sense of Chapter 4, $E'$ is an event composed of all the signals emitted by $p$ in the reaction, $k$ is the completion code returned by $p$, and the statement $p'$ is called the *derivative* of $p$ by the reaction. The statement transition relation is defined by structural induction on statements according to the rules given below.

Given a program $P$ of body $p$ and an input event $I$, the program transition of $P$ is defined in terms of the statement transition of $p$ in the following way:

$$P \xrightarrow{O} P' \quad \text{iff} \quad p \xrightarrow{O, k} p' \quad \text{for some } k$$

This definition exactly expresses what we called the logical coherence of the global event $I \cup O$ in Chapter 3.

**Definition:** The program $P$ is logically reactive (resp. logically deterministic) w.r.t. $I$ if there exists at least (resp. at most) one program transition $P \xrightarrow{O} P'$. It is logically correct if it is logically reactive and logically deterministic.
## 6.3 Trap Propagation and Completion Codes

To handle trap propagation, we introduce two operators on completion codes. The $↓k$ operator is used to compute the completion code of $\{p\}$ from that of $p$, while the $↑k$ operator is used to compute the completion code of $↑p$ from that of $p$:

$$↓k = \begin{cases} 0 & \text{if } k = 0 \text{ or } k = 2 \\ 1 & \text{if } k = 1 \\ k - 1 & \text{if } k > 2 \end{cases}$$

$$↑k = \begin{cases} k & \text{if } k = 0 \text{ or } k = 1 \\ k + 1 & \text{if } k > 1 \end{cases}$$

The most important rule is $↓2 = 0$: it indicates that $\{p\}$ terminates when $p$ exits the trap, i.e. returns code 2. If $p$ exits an enclosing trap by returning a code $k > 2$, the exit is propagated as $k - 1$ to the upper trap since one level of trap has been traversed.

## 6.4 The Logical Behavioral Semantics Rules

The behavioral rules are as follows:

$$k \xrightarrow{0, k} 0 \qquad (compl)$$

$$!s \xrightarrow{\{s^+\}, 0} 0 \qquad (emit)$$

$$\frac{s^+ \in E \quad p \xrightarrow{E', k} p' \qquad (present +)}{s? p, q \xrightarrow{E', k} p'}$$
$$ \frac{s^- \in E \quad q \xrightarrow{F',l} q'}{s \? p, q \xrightarrow{F',l} q'} \qquad \text{(present -)} $$

$$ \frac{p \xrightarrow{E',k} p' \quad k \neq 0}{s \supset p \xrightarrow{E',k} s \supset p'} \qquad \text{(susp1)} $$

$$ \frac{p \xrightarrow{E',0} p'}{s \supset p \xrightarrow{E',0} 0} \qquad \text{(susp2)} $$

$$ \frac{p \xrightarrow{E',k} p' \quad k \neq 0}{p; q \xrightarrow{E',k} p'; q} \qquad \text{(seq1)} $$

$$ \frac{p \xrightarrow{E',0} p' \quad q \xrightarrow{F',l} q'}{p; q \xrightarrow{E' \cup F',l} q'} \qquad \text{(seq2)} $$

$$ \frac{p \xrightarrow{E',k} p' \quad k \neq 0}{p * \xrightarrow{E',k} p'; p*} \qquad \text{(loop)} $$

$$ \frac{p \xrightarrow{E',k} p' \quad q \xrightarrow{F',l} q'}{p | q \xrightarrow{E' \cup F', \max(k,l)} p' | q'} \qquad \text{(parallel)} $$
$$ \frac{p \xrightarrow{E', k} p' \qquad k = 0 \text{ or } k = 2}{\{p\} \xrightarrow{E', 0} 0} \qquad \text{(trap1)} $$

$$ \frac{p \xrightarrow{E', k} p' \qquad k = 1 \text{ or } k > 2}{\{p\} \xrightarrow{E', \downarrow k} \{p'\}} \qquad \text{(trap2)} $$

$$ \frac{p \xrightarrow{E', k} p' \qquad \text{(shift)}}{\uparrow p \xrightarrow{E', \uparrow k} \uparrow p'} $$

$$ \frac{p \xrightarrow{E'*s^+, k} p' \qquad S(E') = S(E)\backslash s}{p\backslash s \xrightarrow{E', k} p'\backslash s} \qquad \text{(sig +)} $$

$$ \frac{p \xrightarrow{E'*s^-, k} p' \qquad S(E') = S(E)\backslash s}{p\backslash s \xrightarrow{E', k} p'\backslash s} \qquad \text{(sig -)} $$

It is important to notice that all rules build a *single* statement transition, possibly as a function of several simultaneous statement transitions. This is how we handle synchrony.

If the return code *k* for a statement *p* is 0, i.e. if *p* terminates, then *p'* will always behave as 0 (**nothing**) in further instants. If *k* encodes a trap exit, i.e. if *k* > 1, the resulting statement *p'* is immaterial since it will always disappear by some application of rule (trap1). The rules exactly formalize the intuitive semantics given in Chapter 2:

* The rules (compl), (emit), (present+), and (present-) are trivial.

* In the (susp1) rule, we transfer control to *p* and generate an immediate suspension *s* ⊇ *p'* as the derivative for next instant if *p* does not terminate; remember that *s* ⊇ *p* is not a kernel statement but an abbreviation
of $\{(s?1,2)*\}; s \supset p$, see Chapter 5, page 61. If $p$ terminates, we use
rule (susp2) to explicitly return the 0 derivative: we cannot return $s \supset 0$
as in rule (susp1), since this term would pause in the following instant
if $s$ were present, preventing termination of a term such as $(s \supset 0) | 1$.

* The (seq1) rule expresses that a sequence pauses if $p$ pauses and that the sequence propagates the traps exited by $p$. The (seq2) rule expresses that control is instantaneously transferred to $q$ if $p$ terminates.

* The (loop) rule expands a loop once and requires the loop's body not to terminate instantaneously.

* The (parallel) rule performs the synchronization by using the $\max(k,l)$ maximum operation, as we explained in Chapter 5.

* The (trap1) rule expresses that a trap terminates if its body terminates or exits the trap. The (trap2) rule expresses that a trap pauses if its body pauses (case $k=1$) and that a trap propagates exits to outer traps (case $k > 2$). In rule (trap1) with $k=2$, we must explicitly return 0 as a derivative instead of $\{p'\}$, otherwise the term $\{2|1\} | 1$ would not terminate in the second instant.

* The (shift) rule is trivial.

* The (sig+) and (sig-) rules formalize the signal logical coherence law. In (sig+) and (sig-), the additional sort condition expresses that the sort of $E'$ does not contain $s$, which is handled specifically by an $E' * s^b$ operation. This is necessary to avoid propagating the local status of $s$ outside the $p \setminus s$ statement.

## 6.5 Reactivity and Determinism

Here is the formal definition of reactivity and determinism:

**Definition:** A program *P* is *reactive* w.r.t. an input event *I* if there exists a output event *O* and a program *P'* such that *P* <sub>*I*</sub><sup>*O*</sup> *P'*<sub>*I*</sub>. The program is *deterministic* w.r.t. *I* if there exists at most one output event and program. The program is *logically correct* w.r.t. *I* if it is reactive and deterministic w.r.t. *I*. The program is *logically correct* if it is logically correct for all input events and if its derivatives are logically correct.
Input-output determinism leaves some room for internal non-determinism. For example, consider the program $(s?!s, 0)\setminus s$. This inputless and outputless program is deterministic: it has no output and can only be rewritten into $0\setminus s$. However, it is internally non-deterministic since the local signal $s$ can be either emitted or not emitted. In constructive semantics, we shall forbid internal non-determinism, in the same way one forbids type-check errors even in dead code in classical languages. For this, we define strong determinism as follows:

**Definition:** A program $P$ is strongly deterministic for an input event $I$ if it is reactive and deterministic for this event and if, furthermore, there exists a unique proof of the unique transition $P \xrightarrow{O} P'$.

## 6.6 Loop-Safe Programs

In rule (loop), there is a side condition $k \neq 0$ to prevent instantaneous loops that would execute infinitely often their body in the instant. It is often useful to put a static restriction on programs to make instantaneous loops impossible and the side condition superfluous. For this, we define the set $K(p)$ of potential completion codes of $p$. First, we extend the $max(k, l)$, $\downarrow k$, and $\uparrow k$ operations to sets $K, L$ of completion codes as follows:

$$ 
\begin{aligned}
Max(K, L) &= \begin{cases} \emptyset & \text{if } K = \emptyset \text{ or } L = \emptyset \\ \{max(k, l) \mid k \in K, l \in L\} & \text{if } K, L \neq \emptyset \end{cases} \\
\downarrow K &= \{\downarrow k \mid k \in K\} \\
\uparrow K &= \{\uparrow k \mid k \in K\}
\end{aligned}
$$

(The cases $K = \emptyset$ and $L = \emptyset$ in the definition of $Max$ are not needed here, but they will be needed in Chapter 7.) Write $K\setminus 0$ for the set $\{k \in K \mid k \neq 0\}$. Then, $K(p)$ is defined as follows:

$$ K(k) = \{k\} $$
$$K(!s) = \{0\}$$

$$K(s \ ? \ p, q) = K(p) \cup K(q)$$

$$K(s \supset p) = K(p)$$

$$K(p; q) = \begin{cases} (K(p)\backslash 0) \cup K(q) & \text{if } 0 \in K(p) \\ K(p) & \text{otherwise} \end{cases}$$

$$K(p*) = K(p)\backslash 0$$

$$K(p | q) = \text{Max}(K(p), K(q))$$

$$K(\{p\}) = \downarrow K(p)$$

$$K(\uparrow p) = \uparrow K(p)$$

$$K(p\backslash s) = K(p)$$

The next lemma shows that $K(p)$ is a superset of the set of completion codes a statement can return.

**Lemma 1** If $p \xrightarrow{k} p'$, then $k \in K(p)$.

We can now define loop-safe programs.

**Definition:** A program $P$ of body $p$ is *loop-safe* if, for each substatement $q^*$ of $p$, one has $0 \notin K(q)$.

In practice, loop-safety is not a very restrictive condition and it makes life easier. However, we know of one case where users find it a little annoying. Assume that two input signals I and J are known to be incompatible, i.e. never present in the same instant. In full Esterel, this is asserted by writing

relation I#J;

Then, the following loop-unsafe program is obviously correct because the direct path from loop to “end loop” cannot be taken:
loop
  present I else
    p % non instantaneous
  end present;
  present J else
    q % non instantaneous
  end present
end loop

The solution to make the program loop-safe is to add a `pause` statement that will never be reached:

loop
  present I else
    p % non instantaneous
  end present;
  present J then
    pause % unreachable
  else
    q % non instantaneous
  end present
end loop
# Chapter 7

## The Constructive Behavioral Semantics

In the logical behavioral semantics, given a program *P* of body *p* and an input event *I*, there are exactly two places where we must make signal status assumptions: when searching for an output event *O* such that *p* $\xrightarrow[\mathrm{I}\cup\mathrm{O}]{\mathrm{O},\mathrm{k}}$ *p*', and when handling the local signal declarations that occur in *p*. In the constructive semantics presented in the sequel, we constructively enforce the choice of determinate statuses at the same places, in a way that ensures determinism by causal information propagation.

We shall present three different but equivalent views of the constructive semantics.

* The *constructive behavioral semantics* presented in this chapter uses the same semantic rules as the behavioral semantics, but it disambiguates the search for signal statuses by adding predicates telling whether signals *must* or *cannot* be emitted. Signals are declared present if they must be emitted, absent if they cannot be emitted. The predicates are computed recursively in a way that forbids speculative computation. Given an input event, if the calculation determines a status for each signal, then the program is said to be constructive w.r.t. the event. Then, reactivity holds by construction and determinism follows from the disjointness of the *Must* and *Cannot* predicates. If the calculation fails, the program is rejected as non-constructive.

* The *constructive operational semantics* presented in Chapter 9 is a more conventional microstep semantics acting on states. However, this
semantics is technically much more intricate since the microsteps are
relational and non-deterministic. A direct correctness proof would re-
quire proving very delicate confluence and strong normalization prop-
erties, such as the ones proved by Gonthier [18] for a former version of
the operational semantics. Here, we avoid these difficulties by proving
equivalence of the relational microstep semantics and of the functional
constructive behavioral semantics.

* In the *constructive circuit semantics* presented in Chapter 11 and Chapter 13, we translate an Esterel program into a Boolean sequential circuit that we interpret in a constructive (i.e. electrical) way. We show that propagation of 1's and 0's in the circuit's wires exactly performs the *must* and *cannot* computations and that program states are appropriately encoded into memory states. The circuit semantics avoids all the computational redundancies of the constructive behavioral semantics and yields very efficient hardware and software implementations of Esterel, which will be discussed in Chapter ??.

## 7.1 The Must and Cannot Analysis

We start by an intuitive presentation of the analysis. We then define the
functions *Must*(*p*, *E*) and *Cannot*<sup>*m*</sup>(*p*, *E*), where *p* is a statement and *E* is
a (partial) event. We discuss other possible choices for *Must* and *Cannot*
and we explain why we discard them. We present the constructive behav-
ioral rules, which differ from the logical ones only by adding appropriate
predicates in three places. Finally, we show that constructive programs are
reactive and deterministic, i.e. that the constructive behavioral semantics is
logically correct.

### 7.1.1 Intuitive Presentation

Consider the following statement P15:

```
present I then
    emit 01;
end

||
present J then
    present 01 then emit 02 else emit 03 end
end
```
<figure><img src="image_7.png" /><figcaption>Figure 7.1: Circuit for P15</figcaption></figure>

Assume first that the statement is a full program body with I and J in-
puts. Consider the case I and J present. Then, since we must execute
“present I”, we must execute “emit 01”, which implies that 01 must be
present. We must execute “present J”, “present 01”, and “emit 02”.
Therefore, 02 must be present. We cannot execute “emit 03”, which im-
plies that 03 must be absent since it cannot be emitted. All the signal
 statuses are determined. In the case I absent, J present, 01 and 02 cannot
 be emitted and are absent while 03 must be emitted and is present. The
 other cases are similar.

Things become more complex if we consider the P15 statement as a
fragment of a larger program, in a context where I and J are not inputs
but local signals the statuses of which are also being computed (to avoid
interference, we assume that there is no other emitter of 01, 02, 03 in the
global program). In this case, we must also explain how we propagate *must*
and *cannot* information when the statuses of I and J are yet unknown. There
are two subcases, depending on whether we already know from the recursive
reasoning context whether we must execute the statement; the cases are *yes*
or *unknown*, since we shall never need to analyze statements known not to
be executed.

Assume first that we know that we must execute the statement. Assume
I present and J unknown. Then, "emit 01" must be executed and 01 must
be present. However, since J is unknown, there is nothing we must do in
the second parallel branch, and, in particular, we cannot deduce any status for 02. However, we have enough information to deduce that the “emit 03” statement is on a false path since 01 is known to be present. Therefore, we safely deduce that we cannot emit 03. The circuit equivalent of P15, shown in Figure 7.1, gives another view of this reasoning. Saying that P15 must be executed is saying GO = 1. Since I = 1, one has 01 = 1, which is just enough to deduce 03 = 0, although GO' remains unknown. No value propagates to the 02 wire.

Assume now that we do not yet know whether P15 statement must be executed. Then, there is nothing we must do since we may not compute speculatively. However, we can still prune out false paths and compute what we cannot do. If I is yet unknown, no information propagates. If I is known absent, then we can constructively deduce that 01 cannot be emitted, which in turn implies that 02 cannot be emitted. In the P15 circuit, I = 0 is enough to deduce 01 = 02 = 0, even when GO is unknown.

In the *cannot* analysis, knowing whether a statement must be executed in fundamental. For example, in

```
emit S;
present S then emit 01 else emit 02 end
```

we can deduce that 02 cannot be emitted only if we know that the statement must be executed. Deducing the same while not knowing whether the statement must be executed would be speculatively reasoning about “emit S”.

So far, we have only reasoned about *Must* and *Cannot*. Technically, it is often easier to reason about the complement *Cannot* of *Cannot*, which we call simply *Can*. Therefore, we say “*p* can emit *S*” for “we cannot prove that *p* cannot emit *S*”. Beware, this shortcut can sometimes be slightly misleading. In case of doubt, always translate *Can* into the double negation *Cannot*.

### 7.1.2 The Must, Cannot, and Can Functions

The *Must* function determines what must be done in a reaction $P \xrightarrow{O} P'$, abstracting away the derivative $P'$ that will be recovered using the behavioral semantics rewrite rules. The *Must* function has the following form:

$$Must(p, E) = \langle S, K \rangle$$

where *E* is a *partial event* that associates a status in $B_{\perp} = \{+, -, \perp\}$ with each signal, where *S* is the set of signals that *p* must emit, and where *K*
is the set of completion codes that $p$ must return. For *Must*, the set $K$ is either empty, if we cannot derive any *Must* information, or a singleton $\{k\}$, if we can derive that $p$ must return $k$. It is impossible that $p$ must return more than one completion code.

To distinguish between the elements of the result pair, we use $s$ and $k$ subscripts:

$$Must(p, E) = \langle Must_s(p, E), Must_k(p, E) \rangle$$

The inclusion predicate $\subseteq$ and the union operator $\cup$ are extended componentwise on pairs $\langle S, K \rangle$.

The function $Cannot^m(p, E)$ is used to prune out false paths. Its type is similar to that of *Must*, but with an extra argument $m$ added in exponent:

$$Cannot^m(p, E) = \langle Cannot_s^m(p, E), Cannot_k^m(p, E) \rangle = \langle S, K \rangle$$

Here, the results $S$ and $K$ are respectively the set of signals that $p$ cannot emit and the set of completion codes that $p$ cannot exit when the input event is $E$. The extra argument $m \in \{+, \perp\}$ tells whether it is known that the statement $p$ must be executed in the event $E$, as explained before. It is recursively provided by the context when a statement is analyzed. The case $m = -$ will never occur in the recursion since *Cannot* will only be called for potentially executable statements.

Technically, it is simpler to define the set complement $Can^m(p, E)$ of $Cannot^m(p, E)$. The complementation is done componentwise, w.r.t. the set of visible signals for the signal part and w.r.t. the set of potential completion codes for the completion part. The set $Can_k^m(p, E)$ may be any subset of the potential completion set $K(p)$ defined in Section 6.6. It can be strictly smaller since we take signal information into account. In case of problems about the intuition of *Can*, always remember it really means *Cannot*.

### 7.1.3 The Definition of Must and Can

The definitions are trivial and identical for completion codes and signal emissions. The $m$ argument is unused here.

$$Must(k, E) = Can^m(k, E) = \langle \emptyset, \{k\} \rangle$$

$$Must(!s, E) = Can^m(!s, E) = \langle \{s\}, \{0\} \rangle$$

Consider now a signal test $s \ ? \ p, q$ and a partial event $E$. First, for both *Must* and *Can*, the definitions are easy if the status of $s$ in $E$ is either $+$ or $-:
we recursively analyze the first branch if the status is + and the second branch if the status is −, with the same m argument. If the status of s in E is unknown, Must and Can behave very differently. For Must, we return the empty signal set and the empty completion code set since none of the branches must be taken. For Can, we return the union of the signals the branches can emit and the union of the completion codes they can return, computed with $m' = \perp$ since no branch must be taken.

$$Must((s \ ? \ p, q), E) = \begin{cases} Must(p, E) & \text{if } s^+ \in E \\ Must(q, E) & \text{if } s^- \in E \\ \langle \emptyset, \emptyset \rangle & \text{if } s^\perp \in E \end{cases}$$ $$Can^m((s \ ? \ p, q), E) = \begin{cases} Can^m(p, E) & \text{if } s^+ \in E \\ Can^m(q, E) & \text{if } s^- \in E \\ Can^\perp(p, E) \cup Can^\perp(q, E) & \text{if } s^\perp \in E \end{cases}$$

Suspension is trivial, since, in an instant, a suspension acts as its body:

$$Must(s \supset p, E) = Must(p, E)$$ $$Can^m(s \supset p, E) = Can^m(p, E)$$

For a sequence $p$; $q$, we analyze $q$ only if $p$ must (resp. can) terminate, in which case the completion code 0 of $p$ is discarded. For Can, we analyze $q$ with argument $m' = +$ if $m = +$ and if $p$ must terminate, with argument $m' = \perp$ otherwise:

$$Must(p; q, E) = \begin{cases} Must(p, E) & \text{if } 0 \notin Must_k(p, E) \\ \langle Must_s(p, E) \cup Must_s(q, E), Must_k(q, E) \rangle & \text{if } 0 \in Must_k(p, E) \end{cases}$$ $$Can^m(p; q, E) = \begin{cases} Can^m(p, E) & \text{if } 0 \notin Can_k^m(p, E) \\ \langle Can_s^m(p, E) \cup Can_s^{m'}(q, E), \\ Can_k^m(p, E) \setminus \{0\} \cup Can_k^{m'}(q, E) \rangle & \text{if } 0 \in Can_k^m(p, E) \\ \text{with } m' = + \text{ if } m = + \text{ and } 0 \in Must_k(p, E) \\ \text{or } m' = \perp \text{ otherwise} \end{cases}$$
In the definition of *Must(p; q, E)*, we could also write the predicates using set comparisons, i.e. as *Must<sub>k</sub>(p, E) ≠ {0}* and *Must<sub>k</sub>(p, E) = {0}* . The result would be equivalent because *Must<sub>k</sub>(p, E)* is either empty or a singleton.

Notice that the set of signals that *p* must emit is not transmitted to *q*. We could do it, but we obtain the same effect using the simple rule above and a global iteration process: if *p* must emit *s* in a partial event *E* such that *s*<sup>⊥</sup> ∈ *E*, the analysis will call it again in the partial event *E* * s<sup>+</sup>*, in which case *s*<sup>+</sup> will effectively reach *q*. The same holds for propagating *s*<sup>-</sup> to *q* if *p* cannot emit *s*. The iteration is performed by the signal and global program rules described below.

For a loop, we analyze the body once. That the body cannot terminate
will be ensured by the constructive semantic inference rules.

$$
Must(p*, E) = Must(p, E)
$$

$$
Can^m(p*, E) = Can^m(p, E)
$$

For a parallel, we take the union of the signal sets and the extension of max
to sets of completion codes defined in Section 6.6:

$$
Must(p | q, E) = \langle \text{Must}_s(p, E) \cup \text{Must}_s(q, E), \\ \text{Max}(\text{Must}_k(p, E), \text{Must}_k(q, E)) \rangle
$$

$$
Can^m(p | q, E) = \langle Can_s^m(p, E) \cup Can_s^m(q, E), \\ \quad \Max(Can_k^m(p, E), Can_k^m(q, E)) \rangle
$$

Notice that *Must*<sub>*k*</sub>(*p* | *q*, *E*) is nonempty and is a singleton set if and only if *Must*<sub>*k*</sub>(*p*, *E*) and *Must*<sub>*k*</sub>(*q*, *E*) are singleton sets. As far as completion codes are concerned, one must be able to compute the codes that both branches must return to compute the code that the parallel statement must return. Using the *Max* set operation in the definition of *Can*<sup>*m*</sup>(*p* | *q*, *E*) is fundamental for adequate control propagation. For example, this operation ensures that a parallel cannot terminate if one of its branches cannot. This property would be lost if *Max* were replaced by a simple union, and this would lead to abnormally rejecting constructively correct programs such as ((*o*?0,0) | 1); !*o*, where the first parallel statement always pauses in the first instant because of its second 1 branch, breaking the potential cycle on *o*.

For trap and a shift, we apply the appropriate operators to the comple-
tion codes returned by the body:

$$
Must(\{p\}, E) = \langle Must_s(p, E), \downarrow Must_k(p, E) \rangle
$$
$$Can^m(\{p\}, E) = \langle Can_s^m(p, E), \downarrow Can_k^m(p, E) \rangle$$

$$Must(\uparrow p, E) = \langle Must_s(p, E), \uparrow Must_k(p, E) \rangle$$

$$Can^m(\uparrow p, E) = \langle Can_s^m(p, E), \uparrow Can_k^m(p, E) \rangle$$

The rules for the local signal declaration operator $p\backslash s$ are deeply different for Must and Can. For Must, because of the way the recursion works, the rule is used only if we already know that $p\backslash s$ must be executed. Since we have yet no information about the status of $s$, we first set this status to $\perp$ and we compute what we must and cannot do. If we find that $p$ must emit $s$, we take that fact for granted, and we re-analyze $p$ with status $+$ for $s$. If we find that $p$ cannot emit $s$, we know that $s$ must be absent and we re-analyze $p$ with status $-$ for $s$. Otherwise, we cannot make progress. In each case, we remove the status of the local $s$ from the emitted signal set, using the notation $\langle S, K \rangle\backslash s$ for $\langle S\backslash s, K \rangle$:

$$Must(p\backslash s, E) = \begin{cases} Must(p, E * s^+)\backslash s & \text{if } s \in Must_s(p, E * s^+) \\ Must(p, E * s^-)\backslash s & \text{if } s \notin Can_s^+(p, E * s^+) \\ Must(p, E * s^+)\backslash s & \text{otherwise} \end{cases}$$

For Can, we first analyze the body $p$ with status $\perp$ for $s$, with the same $m$ argument. If $m = +$ and if we find that the signal must be emitted, we re-analyze $p$ with status $+$ for $s$. For both $m = +$ and $m = \perp$, if the signal cannot be emitted, we re-analyze $p$ with status $-$ and with the same $m$. Otherwise, we return the result of the analysis of $p$ with status $\perp$ for $s$.

$$Can^m(p\backslash s, E) = \begin{cases} Can^+(p, E * s^+)\backslash s & \text{if } m = + \text{ and } s \in Must_s(p, E * s^+) \\ Can^m(p, E * s^-)\backslash s & \text{if } s \notin Can_s^m(p, E * s^+) \\ Can_s^m(p, E * s^+)\backslash s & \text{otherwise} \end{cases}$$

In the Can analysis, notice that the signal status can be set to $+$ only if $m = +$. This is necessary to avoid speculative computation.

The constructively correct program P2, page 29, is a good example to try these definitions.
## 7.2 Possible Variants

There are two places where we made non-obvious choices: the *Must* rule for signal presence test and the *Can* rule for local signal declaration. We now discuss these choices in more details.

Consider first $s?p,q$. The reader familiar with static analysis might find the following *Must* rule less conservative than ours:

$$Must((s?p,q),E) = \begin{cases} Must(p,E) & \text{if } s^+ \in E \\ Must(q,E) & \text{if } s^- \in E \\ Must(p,E) \cap Must(q,E) & \text{if } s^\perp \in E \end{cases}$$

We reject this intersection rule as performing speculative computation. The rule would accept P12, page 41, “present O then emit O else emit O end”. In this program, signal information flows backwards with respect to control, the typical thing we want to forbid.

For $p \setminus s$, one could think of making a perfect symmetry between *Can* and *Must*, writing

$$Can^m(p \setminus s, E) = \begin{cases} Can^m(p, E * s^+) \setminus s & \text{if } s \in Must_s(p, E * s^\perp) \\ Can^m(p, E * s^-) \setminus s & \text{if } s \notin Can_s^m(p, E * s^\perp) \\ Can^m(p, E * s^\perp) \setminus s & \text{otherwise} \end{cases}$$

Here again, we would perform speculative computation, since we would call *Must* even when $m = \perp^1$. For instance, we would accept the program

```
present O then
signal S in
    emit S
||
present S else emit O end
end
end
```

on the following grounds: since the body of the *signal* statement must emit *S*, the output *O* cannot be emitted and can be set absent. This reasoning speculatively executes the “*emit S*” statement.

<footnote n="1">¹The first draft version of this book actually used this rule. This was a deep mistake, sorry!</footnote>
Both variants above would ensure determinism. However, none of them obeys our intuition about fact-to-fact propagation and none of them is amenable to a natural operational and circuit semantics.

## 7.3 Elementary Properties of Must and Can

Remember that *Can* is an auxiliary tool to compute its complement *Cannot*, with

$$ Cannot^m(p, E) = \overline{Cannot^m(p, E)} $$

The interesting properties are best expressed using *Cannot* since their counterpart with *Can* would be contravariant (antimonotonicity instead of monotonicity, etc.). The first property implies that the *Must* and *Cannot* predicates are disjoint:

**Lemma 2** For any statement *p* and partial event *E*, one has $Must(p, E) \cap Cannot^m(p, E) = \{\emptyset, \emptyset\}$, i.e. $Must(p, E) \subseteq Cannot^m(p, E)$.

The next property is that the *Must* and *Cannot* predicates are Scott-monotonic; it is essential to define the input/output function of a program, see Section 7.4.

**Definition:** The Scott ordering $\leq$ on statuses is defined by $\perp \leq +$ and $\perp \leq -$. The Scott ordering is extended to partial events of the same sort by $E_1 \leq E_2$ iff $E_1(s) \leq E_2(s)$ for each signal *s* in the sort.

**Lemma 3** If $E_1 \leq E_2$, then $Must(p, E_1) \subseteq Must(p, E_2)$, and $Cannot^m(p, E_1) \subseteq Cannot^m(p, E_2)$. Furthermore, for any partial event *E*, one has $Cannot^\perp(p, E) \subseteq Cannot^+(p, E)$.

## 7.4 Definition of the Constructive Semantics

Given a program *P* of body *p* and an input event *I*, we compute the constructive behavioral semantics $P \stackrel{O}{\rightleftharpoons}_I P'$ of *P* for *I* in two steps. First, we compute the output event *O* using the *Must* and *Can* functions; this can fail if the status of some output or local signal cannot be determined to be either + or -, in which case the program *P* is declared non-constructive for *I*.
Then, if all signal statuses have been determined, we compute a behavioral transition $p \underset{I \cup O}{\stackrel{O, k}{\rightleftharpoons}} p'$, which yields the next state $p'$; this can fail only if the body of some loop is found to terminate instantaneously.

We begin by computing the output event. The idea is to iteratively compute $Must(p, I \cup O)$ and $Can^m(p, I \cup O)$, starting from an undefined $O$ where all output signal statuses are $\perp$, and repeatedly enriching $O$ using the $Must$ and $Can$ information generated by a pass, this up to stabilization. This is just what we did for local signals, extended to sets of signals. Because of Lemma 3, stabilization is guaranteed by monotonicity. The simplest way to formalize this process is to notice that it is the computation of the least fixpoint of a monotonic function.

**Definition:** Given a program $P$ and an input event $I$, we denote by $[[P]](I)$ the function on partial output events defined by $[[P]](I)(O) = O'$, where, for each output signal $o$, one has

$$O'(o) = \begin{cases} + & \text{if } o \in Must_s(p, I \cup O) \\ - & \text{if } o \in Cannot_s^+(p, I \cup O) \\ \perp & \text{otherwise} \end{cases}$$

(The restriction that an input signal cannot be internally emitted is essential here.)

Lemma 3 yields immediately monotonicity:

**Lemma 4** Given $P$ and $I$, the function $[[P]](I)$ is monotonic on output environments.

**Definition:** Given $P$ and $I$, the output event $O$ constructively computed by $P$ on $I$ is the least fixpoint of the function $[[P]](I)$. We say that $P$ is constructive for $I$ if $O(o) \neq \perp$ holds for any output signal $o$.

If $P$ is constructive for $I$, we have determined the output event $O$, and we are left with determining the new state $P'$ such that $P \stackrel{O}{\underset{I}{\rightleftharpoons}} P'$. As in the behavioral semantics, we use an inductive relation $p \stackrel{E', k}{\underset{E}{\rightleftharpoons}} p'$ and we determine $p'$ by $p \stackrel{O, k}{\underset{I \cup O}{\rightleftharpoons}} p'$. The definition rules of the constructive relation
are exactly those of $p \underset{E}{\stackrel{E', k}{\to}} p'$ in the logical behavioral semantics, except for
the local signal rules $(sig+)$ and $(sig-)$, which are made constructive:

$$
\frac{
  \begin{array}{l}
    s \in \mathit{Must}_s(p, E * s^{\perp}) \quad p \underset{E*s^{\perp}}{\stackrel{E'*s^{\perp}, k}{\to}} p' \quad \mathcal{S}(E') = \mathcal{S}(E)\setminus s \\
    \hline
    p\setminus s \stackrel{E', k}{\underset{E}{\to}} p'\setminus s
  \end{array}
}{
  \mathit{csig} +
}
$$

$$
\frac{
  \begin{array}{l}
    s \in \mathit{Cannot}_s^+(p, E * s^{\perp}) \quad p \xrightarrow[E*s^{-}]{E'*s^{-}, k} p' \quad \mathcal{S}(E') = \mathcal{S}(E)\setminus s \\
    \hline
    p \setminus s \xrightarrow[E]{E', k} p' \setminus s
  \end{array}
}{
  \mathit{csig} -
}
$$

Notice that the inference rules involve only total events since the status of
all signals is determined to be + or -, either by the above computation of
the output event or by the constructive local signal rules; this is why the
other behavioral rules can be left unchanged.

7.5 Correctness of the Constructive Semantics

The main result shows that the constructive behavioral semantics is logically
correct.

**Theorem 1** Let P be a program and I be an input event for P. If $P \underset{I}{\stackrel{O}{\to}} P'$
is provable in the constructive behavioral semantics, then $P \underset{I}{\stackrel{O}{\to}} P'$ is provable
in the logical behavioral semantics and it has a unique proof. The program P
is reactive and strongly deterministic w.r.t. I.
# Chapter 8

## The State Behavioral Semantics

The logical and constructive behavioral semantics define the semantics of Esterel with a minimal number of rules. However, there is a drawback: in a reaction $p \xrightarrow{k, E} p'$, the resulting term $p'$ is obtained by a non-trivial rewriting process. Furthermore, when chaining reactions, the rewritings pile up, which makes it difficult to understand the structure of the resulting statement in function of the initial one. This does not fit with elementary programming intuition, where one prefers to deal with control points moving in a fixed program text. The state semantics we describe in this chapter realizes this goal, while computing reactions in the same way as the behavioral semantics. The price to pay is an extension of the syntax and an increase in the number of rules.

We first introduce the extended syntax used to denote the state of a statement after a reaction. Next, we give the logical behavioral rules of the extended language, and we extend the *Must* and *Can* predicates to define the constructive behavioral semantics. Finally, we show the correctness of the logical and constructive state semantics w.r.t. the original semantics.
# 8.1 The Extended Syntax

## 8.1.1 States as Decorated Terms

Consider the simple inputless term $p = 1; 1; !s$. In the behavioral semantics, the sequence of reactions is:

$$1; 1; !s \xrightarrow{\emptyset, 1} 0; 1; !s \xrightarrow{\emptyset, 1} 0; !s \xrightarrow{\{s\}, 0} 0 \xrightarrow{\emptyset, 0} 0 \dots$$

In the state semantics, the idea is to keep the shape of the statement constant and to decorate it to indicate where control is pausing between reactions. Only occurrences of 1 are decorated<fnref n="1" />: we write $\hat{1}$ instead of 1 to indicate that execution has paused there and will resume from there in the following instant. The other statements need not be decorated since they are purely instantaneous. Using decoration, the above execution sequence becomes:

$$1; 1; !s \xrightarrow{\emptyset, 1} \hat{1}; 1; !s \xrightarrow{\emptyset, 1} 1; \hat{1}; !s \xrightarrow{\{s\}, 0} 1; 1; !s \xrightarrow{\emptyset, 0} \dots$$

The intuition is clear, but there is a slight difficulty. In the above example, the fourth statement is $p_3 = 1; 1; !s$, which is just the same as the initial statement $p_0$ from which execution starts. However, $p_3$ should be considered as being terminated, unlike $p_0$. To resolve this ambiguity, we replace the initial statement $p_0$ by the decorated term $\hat{1}; p_0$. Then, control initially resumes from the auxiliary head $\hat{1}$ statement, which is called the boot statement. Any standard undecorated program body such as $p_3$ is considered to be terminated.

With the boot $\hat{1}$ statement added, the execution sequence becomes:

$$\hat{1}; 1; 1; !s \xrightarrow{\emptyset, 1} 1; \hat{1}; 1; !s \xrightarrow{\emptyset, 1} 1; 1; \hat{1}; !s \xrightarrow{\{s\}, 0} 1; 1; 1; !s \xrightarrow{\emptyset, 0} 1; 1; 1; !s$$

Instead of the boot $\hat{1}$ statement, we could have used a termination marker. Using a boot statement is more natural in the circuit translation and avoids introducing a new end marker symbol in the language.

<footnote n="1">¹In the full user-level language, other statements can be decorated, for example `await`, `every`, and `loop-each`. The expansion of each of these user-level statements involves exactly one `1` statement, which makes decoration unambiguous (see [19]).</footnote>
8.1.2 State Syntax

We call *standard statements* the basic kernel statements introduced in Chap-
ter 5. We define a *state* $\hat{p}, \hat{q}$, etc., as a kernel statement where some part is
decorated or *selected* for execution. Finally, we say that a *term* $\overline{p}, \overline{q}$, etc., is
either a standard statement or a state. The grammar of states and terms is
as follows:

$$
\begin{array}{l@{\hspace{2em}}c@{\hspace{2em}}l}
\hat{p} & ::= & \hat{1} \\
        &     & s?\hat{p},q \\
        &     & s?p,\hat{q} \\
        &     & s\supset\hat{p} \\
        &     & \hat{p};q \\
        &     & p;\hat{q} \\
        &     & \hat{p}* \\
        &     & \overline{p}|\overline{q} \\
        &     & \{\hat{p}\} \\
        &     & \uparrow\hat{p} \\
        &     & \hat{p}\backslash s \\
\hline
\overline{p} & ::= & p \\
             &     & \hat{p}
\end{array}
$$

Notice that a subterm is selected if and only if it contains a selected pause
statement $\hat{1}$. In a state such as $s?\hat{p},q$, the only selected subterm is $\hat{p}$. Such a
state occurs if the test has taken its left branch in some previous instant and
if the execution of this branch is not yet terminated. A parallel branch can
be either a standard statement or a state. In $\hat{p}|\hat{q}$, both $\hat{p}$ and $\hat{q}$ are selected:
the parallel has been started in some past instant and both branches are still
active. A state of the form $\hat{p}|q$ corresponds to the case where the second
branch of the parallel is already terminated while the first one is still active.
For example, the state $(\hat{1};1)|\hat{1}$ becomes $(1;\hat{1})|1$ in the following instant.
There is no state of the form $s?\hat{p},\hat{q}$ or of the form $\hat{p};\hat{q}$, since one cannot be
pausing simultaneously in both arms of a test or of a sequence.

We now define the *base statement* $\mathcal{B}(\overline{p})$ of a term $\overline{p}$. For a standard
statement $p$, we set $\mathcal{B}(p) = p$. For a state $\hat{p}$, we strip the decoration, i.e. we
recursively replace the selected parts of $\hat{p}$ by their base statement, ending
with $\mathcal{B}(\hat{1}) = 1$ (formal definition left to the reader). To make the notation
lighter, given terms $\overline{p}$ and $\overline{q}$, we simply abbreviate $\mathcal{B}(\overline{p})$ and $\mathcal{B}(\overline{q})$ into $p$ and $q$,
always assuming that $\hat{p}, \hat{p}', \overline{p}, \overline{p}', \dots$, are extended statements having $p$ as
base statement.
## 8.2 State Expansion

States encode derivatives of a program by decorating the program's body, which implies that understanding the state semantics essentially amounts to understanding how the decoration encoding works. Given a starting term $p$, a derivative $p'$ obtained after the reaction to some input sequence, and a reaction $p' \xrightarrow{E', k} p''$, our goal is to obtain an equivalent state reaction $\bar{p}' \xrightarrow{E', k} \bar{p}''$ where $\bar{p}'$ encodes $p'$ and $\bar{p}''$ encodes $p''$ with the same base statement $p$. For this, we define the expansion function $\mathcal{E}(\bar{p})$ from terms to standard statements. One more example will be helpful. Consider the following statement reaction sequence:

$$ \begin{array}{l} (\!s | (s ? (1; !o), 1))\!s \xrightarrow[\emptyset]{\emptyset, 1} (0 | (0; !o))\!s \\ \phantom{(\!s | (s ? (1; !o), 1))\!s} \xrightarrow[\emptyset]{\{o\}, 0} (0 | 0)\!s \end{array} $$

The corresponding state reaction sequence is:

$$ \begin{array}{l} \hat{1}; (\!s | (s ? (1; !o), 1))\!s \xrightarrow[\emptyset]{\emptyset, 1} 1; (\!s | (s ? (\hat{1}; !o), 1))\!s \\ \phantom{\hat{1}; (\!s | (s ? (\hat{1}; !o), 1))\!s} \xrightarrow[\emptyset]{\{o\}, 0} 1; (\!s | (s ? (1; !o), 1))\!s \end{array} $$

For the first expansion, we use the rules $\mathcal{E}(\hat{1}) = 0$ and $\mathcal{E}(\hat{p}; q) = \mathcal{E}(\hat{p}); q$. This yields the expanded statement $0; (\!s | (s ? (1; !o), 1))\!s$ which is not quite the original initial statement but is clearly equivalent since the initial 0 disappears in any reaction. For the second expansion, we use the following rules:

* $\mathcal{E}(p; \hat{q}) = \mathcal{E}(\hat{q})$, which expresses that $p$ is already terminated and must be discarded if control is currently in $q$;

* $\mathcal{E}(\hat{p}\!s) = \mathcal{E}(\hat{p})\!s$, which is trivial;

* $\mathcal{E}(p | \hat{q}) = 0$ | $\mathcal{E}(\hat{q})$: the first branch is a standard statement, which means that it is already terminated and that it must be expanded into 0 in the current instant.
• $\mathcal{E}(s?\hat{p}, q) = \mathcal{E}(\hat{p})$, since the test for $s$ has already been performed and should not be performed again when executing the **then** branch.

This time, the expansion yields the exact second statement. For the third expansion, we use the rule $\mathcal{E}(p) = 0$ that turns any standard statement into 0. As for the first reaction, we do not exactly obtain the original third term $(0|0)\backslash s$, but the simpler term 0 has the same behavior in all reactions. Altogether, the expansion $\mathcal{E}(\bar{p})$ is identical to the corresponding original derivative up to some trivial arrangements of 0's.

Technically, the *expansion function* $\mathcal{E}(\bar{p})$ is defined as follows:

$$ 
\begin{align*}
\mathcal{E}(p) &= 0 \\
\mathcal{E}(\hat{1}) &= 0 \\
\mathcal{E}(s?\hat{p}, q) &= \mathcal{E}(\hat{p}) \\
\mathcal{E}(s?p, \hat{q}) &= \mathcal{E}(\hat{q}) \\
\mathcal{E}(s \supset \hat{p}) &= s \supset \mathcal{E}(\hat{p}) \\
\mathcal{E}(\hat{p}; q) &= \mathcal{E}(\hat{p}); q \\
\mathcal{E}(p; \hat{q}) &= \mathcal{E}(\hat{q}) \\
\mathcal{E}(\hat{p}*) &= \mathcal{E}(\hat{p}); (p*) \\
\mathcal{E}(\bar{p} | \bar{q}) &= \mathcal{E}(\bar{p}) | \mathcal{E}(\bar{q}) \\
\mathcal{E}(\{\hat{p}\}) &= \{\mathcal{E}(\hat{p})\} \\
\mathcal{E}(\uparrow \hat{p}) &= \uparrow \mathcal{E}(\hat{p}) \\
\mathcal{E}(\hat{p}\backslash s) &= \mathcal{E}(\hat{p})\backslash s
\end{align*}
$$

Notice that a selected suspension statement $s \supset \hat{p}$ is expanded into an immediate suspension $s \supset \mathcal{E}(\hat{p})$ as required by the behavioral semantics.

## 8.3 The State Behavioral Semantics

In this section, we directly define the logical behavioral semantics of the extended language. Then, we define the *Must* and *Can* predicates and the constructive behavioral semantics.
### 8.3.1 The Logical State Behavioral Semantics

The definition of the state behavioral semantics follows the same pattern as in Chapter 6. Let $P$ be a program of body $q$, and let $p = 1$; $q$. An *extended program* $\overline{P}$ of base $P$ has body an extended statement $\overline{p}$ of base $p$. The behavioral semantics formalize a reaction of an extended program $\overline{P}$ as a behavioral transition of the form

$$ \overline{P} \xrightarrow{O} \overline{P}' $$

If the body of $\overline{P}$ is the standard statement $p$, then $\overline{P}$ is considered to be terminated and it reacts to any input by producing no output. If the body of $\overline{P}$ is a proper state $\hat{p}$, the reaction is computed using an auxiliary inductive relation

$$ \hat{p} \xrightarrow{E', k} \overline{p}' $$

where the base statement $p$ is left unchanged according to our convention. As in Section 6.2, we set

$$ \hat{P} \xrightarrow{O} \overline{P}' \quad \text{iff} \quad \hat{p} \xrightarrow{O, k} \overline{p}' $$

The logical behavioral rules immediately follow from the definitions of the statement behavioral semantics and of the expansion function: to find what a proper state $\hat{p}$ can do, just inspect what $\mathcal{E}(\hat{p})$ can do.

The rules are split into two categories: *s-rules* start execution of a fresh statement $p$, while *r-rules* resume execution from a proper state $\hat{p}$. When two similar rules apply to both a state $\hat{p}$ and a standard statement $p$, we group them into a single *sr-rule* acting on a term $\overline{p}$, see for example rules (*sr-seq1*) and (*sr-seq2*) below.

$k \neq 1$

$$ \frac{k \xrightarrow{\emptyset, k} k}{k \xrightarrow{E} k} \qquad (s-term-exit) $$

$$ 1 \xrightarrow{\emptyset, 1} \hat{1} \qquad (s-pause) $$

$$ \hat{1} \xrightarrow{\emptyset, 0} 1 \qquad (r-pause) $$
$$ !s \xrightarrow{\{s^+\}, 0} !s \qquad (s-emit) $$

$$ \begin{array}{l} s^+ \in E \qquad p \xrightarrow{E', k} \bar{p}' \\ \hline s \? p, q \xrightarrow{E', k} s \? \bar{p}', q \end{array} \qquad (s-present +) $$

$$ \begin{array}{l} s^- \in E \qquad q \xrightarrow{F', l} \bar{q}' \\ \hline s \? p, q \xrightarrow{F', l} s \? p, \bar{q}' \end{array} \qquad (s-present -) $$

$$ \begin{array}{l} \hat{p} \xrightarrow{E', k} \bar{p}' \\ \hline s \? \hat{p}, q \xrightarrow{E', k} s \? \bar{p}', q \end{array} \qquad (r-then) $$

$$ \begin{array}{l} \hat{q} \xrightarrow{F', l} \bar{q}' \\ \hline s \? p, \hat{q} \xrightarrow{F', l} s \? p, \bar{q}' \end{array} \qquad (r-else) $$

$$ \begin{array}{l} p \xrightarrow{E', k} \bar{p}' \\ \hline s \supset p \xrightarrow{E', k} s \supset \bar{p}' \end{array} \qquad (s-suspend) $$

$$ \begin{array}{l} s^+ \in E \\ \hline s \supset \hat{p} \xrightarrow{0, 1} s \supset \hat{p} \end{array} \qquad (r-suspend +) $$

$$ \begin{array}{l} s^- \in E \qquad \hat{p} \xrightarrow{E', k} \bar{p}' \\ \hline s \supset \hat{p} \xrightarrow{E', k} s \supset \bar{p}' \end{array} \qquad (r-suspend -) $$
$$ \frac{\bar{p} \xrightarrow{E', k} \bar{p}' \quad k \neq 0}{\bar{p}; q \xrightarrow{E', k} \bar{p}'; q} \qquad \text{(sr-seq1)} $$

$$ \frac{\bar{p} \xrightarrow{E', 0} p \quad q \xrightarrow{F', l} \bar{q}'}{\bar{p}; q \xrightarrow{E' \cup F', l} p; \bar{q}'} \qquad \text{(sr-seq2)} $$

$$ \frac{\hat{q} \xrightarrow{F', l} \bar{q}'}{p; \hat{q} \xrightarrow{F', l} p; \bar{q}'} \qquad \text{(r-seq3)} $$

$$ \frac{\bar{p} \xrightarrow{E', k} \bar{p}' \quad k \neq 0}{\bar{p} * \xrightarrow{E', k} \bar{p} *'} \qquad \text{(sr-loop)} $$

$$ \frac{\hat{p} \xrightarrow{E', 0} p \quad p \xrightarrow{E'', k} \bar{p}' \quad k \neq 0}{\hat{p} * \xrightarrow{E' \cup E'', k} \bar{p} *'} \qquad \text{(r-do-loop)} $$

$$ \frac{p \xrightarrow{E', k} \bar{p}' \quad q \xrightarrow{F', l} \bar{q}'}{p | q \xrightarrow{E' \cup F', \max(k,l)} \bar{p}' | \bar{q}'} \qquad \text{(s-both)} $$

$$ \frac{\hat{p} \xrightarrow{E', k} \bar{p}' \quad \hat{q} \xrightarrow{F', l} \bar{q}'}{\hat{p} | \hat{q} \xrightarrow{E' \cup F', \max(k,l)} \bar{p}' | \bar{q}'} \qquad \text{(r-both)} $$
$$ \begin{array}{c} \hat{p} \xrightarrow{\frac{E', k}{E}} \overline{p}' \\ \hline \hat{p} | q \xrightarrow{\frac{E', k}{E}} \overline{p}' | q \end{array} \qquad \text{(r-left)} $$

$$ \begin{array}{c} \hat{q} \xrightarrow{\frac{F', l}{E}} \overline{q}' \\ \hline p | \hat{q} \xrightarrow{\frac{F', l}{E}} p | \overline{q}' \end{array} \qquad \text{(r-right)} $$

$$ \begin{array}{c} \overline{p} \xrightarrow{\frac{E', k}{E}} \overline{p}' \quad k = 0 \text{ or } k = 2 \\ \hline \{\overline{p}\} \xrightarrow{\frac{E', 0}{E}} \{p\} \end{array} \qquad \text{(sr-term-trap)} $$

$$ \begin{array}{c} \overline{p} \xrightarrow{\frac{E', k}{E}} \overline{p}' \quad k \neq 0 \text{ and } k \neq 2 \\ \hline \{\overline{p}\} \xrightarrow{\frac{E', \downarrow k}{E}} \{\overline{p}'\} \end{array} \qquad \text{(sr-prop-trap)} $$

$$ \begin{array}{c} \overline{p} \xrightarrow{\frac{E', k}{E}} \overline{p}' \\ \hline \uparrow \overline{p} \xrightarrow{\frac{E', \uparrow k}{E}} \uparrow \overline{p}' \end{array} \qquad \text{(sr-shift)} $$

$$ \begin{array}{c} \overline{p} \xrightarrow{\frac{E'*s^+, k}{E*s^+}} \overline{p}' \quad S(E') = S(E)\backslash s \\ \hline \overline{p}\backslash s \xrightarrow{\frac{E', k}{E}} \overline{p}'\backslash s \end{array} \qquad \text{(sr-sig+)} $$

$$ \begin{array}{c} \overline{p} \xrightarrow{\frac{E'*s^-, k}{E*s^-}} \overline{p}' \quad S(E') = S(E)\backslash s \\ \hline \overline{p}\backslash s \xrightarrow{\frac{E', k}{E}} \overline{p}'\backslash s \end{array} \qquad \text{(sr-sig-)} $$
### 8.3.2 The Constructive State Behavioral Semantics

To define the constructive behavioral semantics of the extended language, we add the *Must* and *Can* predicates to the local signal rules as before:

$$ s \in \text{Must}_s(\bar{p}, E * s^{\perp}) \quad \bar{p} \underset{E*s^{\perp}}{\stackrel{E'*s^{\perp}, k}{\rightleftharpoons}} \bar{p}' \quad S(E') = S(E)\setminus s \qquad (\text{sr-csig+}) $$

$$ s \notin \text{Can}_s^+(\bar{p}, E * s^{\perp}) \quad \bar{p} \underset{E}{\stackrel{E'*s^{-}, k}{\rightleftharpoons}} \bar{p}' \quad S(E') = S(E)\setminus s \qquad (\text{sr-csig-}) $$

the other rules of $\bar{p} \underset{E}{\stackrel{E', k}{\rightleftharpoons}} \bar{p}'$ being those of $\bar{p} \underset{E}{\stackrel{E', k}{\rightleftharpoons}} \bar{p}'$.

We extend the definition of *Must* and *Can* in such a way that $\text{Must}(\hat{p}, E) = \text{Must}(\mathcal{E}(\hat{p}), E)$ and $\text{Can}^m(\hat{p}, E) = \text{Can}^m(\mathcal{E}(\hat{p}), E)$, retaining the basic definitions of *Must* and *Can* for standard statements as they were given in Chapter 7. The additional definitions are:

$$ \text{Must}(\hat{1}, E) = \text{Can}^m(\hat{1}, E) = \langle \emptyset, \{0\} \rangle $$

$$ \text{Must}((s \? \hat{p}, q), E) = \text{Must}(\hat{p}, E) $$

$$ \text{Can}^m((s \? \hat{p}, q), E) = \text{Can}^m(\hat{p}, E) $$

$$ \text{Must}((s \? p, \hat{q}), E) = \text{Must}(\hat{q}, E) $$

$$ \text{Can}^m((s \? p, \hat{q}), E) = \text{Can}^m(\hat{q}, E) $$

$$ \text{Must}(s \supset \hat{p}, E) = \begin{cases} \langle \emptyset, \{1\} \rangle & \text{if } s^+ \in E \\ \text{Must}(\hat{p}, E) & \text{if } s^- \in E \\ \langle \emptyset, \emptyset \rangle & \text{if } s^\perp \in E \end{cases} $$
$$ \mathit{Can}^m(s \supset \hat{p}, E) = \left\{ \begin{array}{ll} \langle \emptyset, \{1\} \rangle & \text{if } s^+ \in E \\ \mathit{Can}^m(\hat{p}, E) & \text{if } s^- \in E \\ \langle \emptyset, \{1\} \rangle \cup \mathit{Can}_s^m(\hat{p}, E) & \text{if } s^\perp \in E \end{array} \right. $$

$$ \mathit{Must}(\hat{p}; q, E) = \left\{ \begin{array}{ll} \mathit{Must}(\hat{p}, E) & \text{if } 0 \notin \mathit{Must}_k(\hat{p}, E) \\ \langle \mathit{Must}_s(\hat{p}, E) \cup \mathit{Must}_s(q, E), \\ \mathit{Must}_k(q, E) \rangle & \text{if } 0 \in \mathit{Must}_k(\hat{p}, E) \end{array} \right. $$

$$ \mathit{Can}^m(\hat{p}; q, E) = \left\{ \begin{array}{ll} \mathit{Can}^m(\hat{p}, E) & \text{if } 0 \notin \mathit{Can}_k^m(\hat{p}, E) \\ \langle \mathit{Can}_s^m(\hat{p}, E) \cup \mathit{Can}_s^m(q, E), \\ \mathit{Can}_k^m(\hat{p}, E) \setminus 0 \cup \mathit{Can}_k^m(q, E) \rangle & \text{if } 0 \in \mathit{Can}_k^m(\hat{p}, E) \\ \text{with } m' = + & \text{if } m = + \text{ and } 0 \in \mathit{Must}_k(p, E) \\ \text{or } m' = \perp \text{ otherwise} & \end{array} \right. $$

$$ \mathit{Must}(p; \hat{q}, E) = \mathit{Must}(\hat{q}, E) $$

$$ \mathit{Can}^m(p; \hat{q}, E) = \mathit{Can}^m(\hat{q}, E) $$

$$ \mathit{Must}(\hat{p}*, E) = \left\{ \begin{array}{ll} \mathit{Must}(\hat{p}, E) & \text{if } 0 \notin \mathit{Must}_k(\hat{p}, E) \\ \langle \mathit{Must}_s(\hat{p}, E) \cup \mathit{Must}_s(p, E), \mathit{Must}_k(p, E) \rangle & \text{if } 0 \in \mathit{Must}_k(\hat{p}, E) \end{array} \right. $$

$$ \mathit{Can}^m(\hat{p}*, E) = \left\{ \begin{array}{ll} \mathit{Can}^m(\hat{p}, E) & \text{if } 0 \notin \mathit{Can}_k^m(\hat{p}, E) \\ \langle \mathit{Can}_s^m(\hat{p}, E) \cup \mathit{Can}_s^m(p, E), \\ \mathit{Can}_k^m(\hat{p}, E) \setminus 0 \cup \mathit{Can}_k^m(p, E) \rangle & \text{if } 0 \in \mathit{Can}_k^m(\hat{p}, E) \\ \text{with } m' = + & \text{if } m = + \text{ and } 0 \in \mathit{Must}_k(\hat{p}, E) \\ \text{or } m' = \perp \text{ otherwise} & \end{array} \right. $$
$$Must(\hat{p} | \hat{q}, E) = \langle Must_s(\hat{p}, E) \cup Must_s(\hat{q}, E), \\ \qquad \quad Max(Must_k(\hat{p}, E), Must_k(\hat{q}, E)) \rangle$$

$$Can^m(\hat{p} | \hat{q}, E) = \langle Can_s^m(\hat{p}, E) \cup Can_s^m(\hat{q}, E), \\ \qquad \quad Max(Can_k^m(\hat{p}, E), Can_k^m(\hat{q}, E)) \rangle$$

$$Must(\hat{p} | q, E) = Must(\hat{p}, E)$$

$$Can^m(\hat{p} | q, E) = Can^m(\hat{p}, E)$$

$$Must(p | \hat{q}, E) = Must(\hat{q}, E)$$

$$Can^m(p | \hat{q}, E) = Can^m(\hat{q}, E)$$

$$Must(\{\hat{p}\}, E) = \langle Must_s(\hat{p}, E), \downarrow Must_k(\hat{p}, E) \rangle$$

$$Can^m(\{\hat{p}\}, E) = \langle Can_s^m(\hat{p}, E), \downarrow Can_k^m(\hat{p}, E) \rangle$$

$$Must(\uparrow \hat{p}, E) = \langle Must_s(\hat{p}, E), \uparrow Must_k(\hat{p}, E) \rangle$$

$$Can^m(\uparrow \hat{p}, E) = \langle Can_s^m(\hat{p}, E), \uparrow Can_k^m(\hat{p}, E) \rangle$$

$$Must(\hat{p} \setminus s, E) = \begin{cases} Must(\hat{p}, E * s^+) \setminus s & \text{if } s \in Must_s(\hat{p}, E * s^+) \\ Must(\hat{p}, E * s^-) \setminus s & \text{if } s \notin Can_s^+(\hat{p}, E * s^+) \\ Must(\hat{p}, E * s^+) \setminus s & \text{otherwise} \end{cases}$$

$$Can^m(\hat{p} \setminus s, E) = \begin{cases} Can^+(\hat{p}, E * s^+) \setminus s & \text{if } m = + \text{ and } s \in Must_s(p, E * s^+) \\ Can^m(\hat{p}, E * s^-) \setminus s & \text{if } s \notin Can_s^m(\hat{p}, E * s^+) \\ Can_s^m(\hat{p}, E * s^+) \setminus s & \text{otherwise} \end{cases}$$

## 8.4 Equivalence to the Standard Semantics

As expected, the main result is that the standard semantics of a program *P* of body *p* and the state semantics of the program of initial state $\hat{1}$; *p* determine the same transition sequences and the same causality, in the sense that
corresponding derivatives react logically or constructively to the same inputs by producing the same outputs and corresponding derivatives. However, the standard and state transition systems are not exactly isomorphic because of the fact that a standard term reduction can leave some innocuous terminated terms that do not appear in the state semantics: consider for example the reduction $1; 0 \xrightarrow[\emptyset]{0,0} 0; 0 \xrightarrow[\emptyset]{0,0} 0$, which yields a proper 0 only in two steps. Technically, the right notion is that of (strong) bisimilarity well-known in process calculi [31] and not recalled in this draft.

Before stating the main result, we need a tool to relate standard terms that differ only by terminated initial subterms, such as 0; 0 and 0. This is *immediate equivalence* defined below:

**Definition:** We say that two standard statements $p$ and $q$ of the same sort $S$ are *immediately equivalent*, and we write $p \equiv q$, if, for all $E, E', k$, one has $p \xrightarrow[E]{E', k} p'$ if and only if $q \xrightarrow[E]{E', k} p'$. Similarly, we say that $p$ and $q$ are *constructively immediately equivalent*, and we write $p \equiv_c q$, if, for all $E, E', k$, one has $p \xrightarrow[E]{E', k} p'$ if and only if $q \xrightarrow[E]{E', k} p'$.

**Lemma 5** Let $\hat{p}$ be a state. One has $\hat{p} \xrightarrow[E]{E', k} \bar{p}'$ if and only if one has $\mathcal{E}(\hat{p}) \xrightarrow[E]{E', k} q$ for some $q$ such that $\mathcal{E}(\bar{p}') \equiv q$. One has $\hat{p} \xleftarrow[E]{E', k} \bar{p}'$ if and only if one has $\mathcal{E}(\hat{p}) \xrightarrow[E]{E', k} q$ for some $q$ such that $\mathcal{E}(\bar{p}') \equiv_c q$.

**Lemma 6** Let $p$ be a standard statement. Then one has $\mathcal{E}(\hat{1}; p) \equiv p$ and $\mathcal{E}(\hat{1}; p) \equiv_c p$.

**Theorem 2** For any standard statement $p$, the transition systems determined by $p$ in the logical (resp. constructive) behavioral semantics and by $\hat{1}$; $p$ in the logical (resp. constructive) state behavioral semantics are bisimilar.

The next result expresses that any Pure Esterel program is finite state. It directly follows from the fact that a program body can be decorated only in finitely many ways.

**Theorem 3** In the state semantics, any program has only finitely many iterated derivatives.
The Esterel v5 compiler can translate an Esterel program into a deterministic
finite automaton by exhaustively computing all iterated derivatives of the
initial state. In practice, a derivative is represented by the set of all selected
occurrences of 1 in the current state, which can be efficiently implemented
by a bitset.
# Chapter 9

## The Constructive
Operational Semantics

*This part of the book is currently being rewritten. It is not necessary to understand what follows.*
100CHAPTER 9. THE CONSTRUCTIVE OPERATIONAL SEMANTICS
# Part III

## Circuit Translation
<figure><img src="image_8.png" /></figure>
# Chapter 10

# Constructive Circuits

This chapter presents constructive (sequential) Boolean circuits. Circuits react to inputs by producing outputs and changing state, as do Esterel programs. Circuits are physical objects, with much simpler semantics as Esterel's. This is why we choose them as implementation targets. Producing a circuit out of a program does not imply a hardware implementation, since it is easy to simulate circuit execution in software. This is what the Esterel v5 compiler to C does.

Below, we shall use two equivalent presentations of Boolean circuits. In Chapter 11, we use circuits diagrams. In Chapter 13, we use systems of Boolean equations. Both presentations have been informally used in Section 4 and will be defined here.

## 10.1 Boolean Circuits

### 10.1.1 Textual Definition

A Boolean circuit $C$ is defined by a set $W$ of variables or wires and a set of wire definitions. The set $W$ is partitioned into a set $I$ of input wires, a set $O$ of output wires, and a set $L$ of local wires.

Boolean expressions $e, e'...$ are composed of wires $w$, constants 0 and 1, and connectives $\neg, \vee, \wedge$. Each output or local wire must be defined by exactly one wire definition. There are two kinds of wire definitions.

* An equality definition $w = e$ defines the value of $w$ to be that of $e$ in each instant.
<figure><img src="image_9.png" /><figcaption>Figure 10.1: Gate Symbols</figcaption></figure>

• A *register* definition $w := e$ defines the value of $w$ to be initially 0; subsequently, it is the value of $e$ in the previous instant.

The expression that appears in the right-hand side of the definition of wire $w$ is called $C(w)$. A wire defined by an equality definition is called a *standard* or *combinational* wire, and $S$ denotes the set of standard wires. A wire defined by a register definition is called a *register*, and $R$ denotes the set of registers. An output wire may be either a standard wire or a register wire. Therefore, one has $S \subset L \cup O, R \subset L \cup O, S \cap R = \emptyset, S \cup R = L \cup O, \text{ and } I \cup S \cup R = W$.

An *input event I* (resp. *output event O*) is an assignment of Boolean values to the input (resp. output) wires. A *state R* is an assignment of Boolean values to the register wires. The *initial state* assigns 0 to all registers.

### 10.1.2 Definition by Diagrams

In diagrams, a circuit is a graph of *gates* that represent Boolean operators linked by wires. Each gate may have several inputs and has only one output, which is the wire it defines. The conventional gates are pictured in Figure 10.1. The identity function is represented by the conventional *buffer gate*<fnref n="1" />; we could also use a unary *and* or *or* gate. Negation gates are pictured

<footnote n="1">¹In hardware terminology, there is no memory in a buffer.</footnote>
<figure><img src="image_10.png" /></figure>

$$O = I \wedge \neg R$$

$$R := O$$

<caption>Figure 10.2: Diagrams vs. Definitions</caption>

by a little circle and placed either on an input or on the output of a gate.

The wires in a circuit must be either primary inputs or driven by a single gate. However, for convenience, we allow an output to have no defining gate, in which case it is assumed to always have value 0.

To translate a system of definitions into a circuit diagram, one simply creates as many gates as there are Boolean operators in expressions and one register gate per register definition. To translate diagrams into equations, one introduces one wire name for each unnamed gate output and one writes the corresponding equations. An example of a diagram and its equational form is given in Figure 10.2.

## 10.2 The Logical Semantics

In the logical semantics, we are interested in the solutions of the system of equations that defines the standard wires. Given an input *I* and a state *R*, a *logical solution* is a set *S* of assignments of values 0 or 1 to the standard wires such that all standard wire equations are valid when interpreted with wire values given by *I*, *R*, and *S*. We say that a wire is *set* in a logical solution if it has value 1 and that it is *unset* if it has value 0.

Reactivity and determinism w.r.t. *I* and *R* are defined as existence and uniqueness of a logical solution, just as in Chapter 3, and logical correctness is the conjunction of reactivity and determinism. If a circuit is logically correct, then the output *O* is defined by the value of the output wires and the new state *R'* is defined by the values of the right-hand-side expressions
of the register definitions. We then write $R \xrightarrow{O} R'$.

## 10.3 The Constructive Semantics

As we mentioned in Section 4.4, not all circuits are logically correct (see circuit C2, page 47), and not all logically correct circuits should be accepted (see circuits C9, page 48 and Figure 4.1, and C12, page 48 and Figure 4.2). We now define the constructive semantics in three different ways: a proof-theoretic way, by defining constructive information propagation, a denotational way, by considering least fixpoints of Scott-monotonic functions, and an electrical way, by delay-independent electrical stabilization. These three definitions turn out to be equivalent, which shows that constructiveness is a very robust notion.

### 10.3.1 Constructive Value Propagation

Given an input $I$, a state $R$, a wire expression $e$, and a Boolean value $b$, we define the constructive evaluation relation $I, R \vdash e \leftrightarrow b$, read “for input $I$ and state $R$, the expression $e$ constructively evaluates to $b$”. The definition is:

$$
\begin{array}{l@{\qquad}l@{\qquad}l}
\text{for } w \in \mathcal{I} & I, R \vdash w \leftrightarrow b & \text{if } I(w) = b \\
\text{for } w \in \mathcal{R} & I, R \vdash w \leftrightarrow b & \text{if } R(w) = b \\
\text{for } w \in \mathcal{S} & I, R \vdash w \leftrightarrow b & \text{if } C(w) = e \text{ and } I, R \vdash e \leftrightarrow b \\
& I, R \vdash \neg e \leftrightarrow b & \text{if } I, R \vdash e \leftrightarrow \neg b \\
& I, R \vdash e \lor e' \leftrightarrow 1 & \text{if } I, R \vdash e \leftrightarrow 1 \text{ or } I, R \vdash e' \leftrightarrow 1 \\
& I, R \vdash e \lor e' \leftrightarrow 0 & \text{if } I, R \vdash e \leftrightarrow 0 \text{ and } I, R \vdash e' \leftrightarrow 0 \\
& I, R \vdash e \land e' \leftrightarrow 1 & \text{if } I, R \vdash e \leftrightarrow 1 \text{ and } I, R \vdash e' \leftrightarrow 1 \\
& I, R \vdash e \land e' \leftrightarrow 0 & \text{if } I, R \vdash e \leftrightarrow 0 \text{ or } I, R \vdash e' \leftrightarrow 0
\end{array}
$$

In the evaluation, the current value of a register $w$ is determined by $R$ and not by its definition expression $C(w)$, which is only used to determine the next value of the register. Notice that the value of a standard wire can be determined only by determining the value of its definition expression; this is the essence of fact-to-fact propagation. The following lemma shows that evaluation is deterministic.

**Lemma 7** For any wire $w$, if $I, R \vdash w \leftrightarrow b$ and $I, R \vdash w \leftrightarrow b'$, then $b = b'$.
We say that $\mathcal{C}$ is constructive w.r.t. $I$ and $R$ if, for any wire $w$, there exists a Boolean value $b$ such that $I, R \vdash w \leftrightarrow b$. As in the logical semantics, the output $O$ is such that the value of any output wire $w$ is $b$ if $I, R \vdash w \leftrightarrow b$ and the new state $R'$ is such that the new value of any register $w$ is $b$ if $I, R \vdash \mathcal{C}(w) \leftrightarrow b$. We then write $R \stackrel{O}{\underset{I}{\rightleftharpoons}} R'$.

By the lemmas, if $\mathcal{C}$ is constructive w.r.t. $I$ and $R$, it is logically correct w.r.t. $I$, and $R \stackrel{O}{\underset{I}{\rightleftharpoons}} R'$ implies $R \stackrel{O}{\underset{I}{\rightleftharpoons}} R'$.

Registers do not interfere with instantaneous constructiveness analysis, but they are important for global constructiveness. We say that a circuit is constructive if it is constructive w.r.t. each input $I$ and each reachable state $R$, where a reachable state is a state that can be reached from the initial state 0 by some input sequence.

See Section 4.4 for examples of constructive and non-constructive circuits.

### 10.3.2 Three-Valued Denotational Semantics

In the denotational semantics, we interpret wires in the three-valued Scott Boolean domain $B_{\perp} = \{\perp, 0, 1\}$, partially ordered by $\perp \le 0$ and $\perp \le 1$. The values 0 and 1 are called *defined values*, while $\perp$ is called the *undefined value*. The *or* and *and* operators are interpreted by the least monotonic functions that respect their pure Boolean outputs, which are classically called *parallel or* and *parallel and*, see [33]. Therefore, one has $\perp \vee 1 = 1 \vee \perp = 1$ and $\perp \wedge 0 = 0 \wedge \perp = 0$.

Consider a circuit $\mathcal{C}$ with $n$ standard wires, and number these wires from 1 to $n$. Let $S \in B_{\perp}^n$. Given an input $I$ and a state $R$, the circuit $\mathcal{C}$ defines a monotonic function $\mathcal{C}(I, R) : B_{\perp}^n \mapsto B_{\perp}^n$. For any assignment $S$ of values in $B_{\perp}$ to standard wires, this function defines another assignment $S'$, where the value of each standard wire $w$ is that of its definition expression $\mathcal{C}(w)$ computed in the environment $I, R, S$. Let $Y(I, R) \in B_{\perp}^n$ be the least fixpoint of $\mathcal{C}(I, R)$.

**Theorem 4** Let $\mathcal{C}$ be a circuit, let $I$ be an input, and let $R$ be a state. Then, for any standard wire $w_i$, one has $I, R \vdash w_i \leftrightarrow b$ if and only if $Y(I, R)_i = b$.

It follows that a circuit is constructive w.r.t. $I$ and $R$ if and only if all components of the least fixpoint $Y(I, R)$ are defined. Then, the new state is computed as usual as the value of the register definition expressions, which are all defined.
### 10.3.3 The Electrical Semantics

The electrical semantics deals with temporal propagations of idealized voltages through electrical gates that have delays. It is easier to explain with gates and wires, i.e. with diagrams. We use the *up-bounded inertial delay model* of [15]. We consider only the combinational part and ignore the registers, which play no role in the instantaneous analysis.

Wires are interpreted as functions from the positive reals (time) to {0, 1}. With any gate that drives a wire *w*, we associate a positive real number $\delta(w)$ called the *delay* of the gate. The following property must hold for the gate:

(i) If, at time $t$, the value of *w* changes from 0 to 1 or from 1 to 0, then the value of some input wire of the gate must have changed at some time $t'$ such that $t - \delta \le t' \le t$

(ii) If the values of the gate inputs are stable between time $t - \delta(w)$ and $t$ included, then the value of *w* at time $t$ is the Boolean value determined by the gate logical function and the input values.

We also allow for arbitrary wire delays by making it possible to insert delayed buffers anywhere on wires.

Notice that the delay model yields lots of freedom. For example, transient pulses shorter than $\delta(w)$ may or may not show up on the output. The only things that are required are that the output changes only because of inputs and that the output must receive its logical value if the inputs are kept stable long enough.

Given a circuit $C$, a delay assignment to gates, and an input $I$ kept stable from time 0 on, we say that the circuit *electrically stabilizes in time t* if all the wires keep a stable Boolean value after time $t$.

**Theorem 5** Let $C$ be a circuit, let $I$ be an input and $R$ be a state. Then $C$ if constructive if and only if, for any delay assignment, all wires stabilize after some time $t$. The stable electrical values of the wires are those determined by constructive Boolean propagation.

Since the number of inputs and states is finite, there is a maximum stabilization time valid for all inputs and all states. This time is called the *clock period*. After it has elapsed, one can set the new values of the registers and process new inputs<fnref n="2" />.

<footnote n="2">²Our model is not fully respective of electrical phenomena. One should wait for a setup</footnote>
Therefore, the constructive semantics abstracts away gate delays. Cyclic constructive circuits behave synchronously, as do acyclic circuits.

# 10.4 Syntactic Extensions

We now discuss the two syntactic extensions we shall need for the formal translation from Esterel to circuits.

## 10.4.1 Hierarchical Circuits

In the translation of Esterel programs into circuits, we shall define circuits by structural induction over statements. For this, we shall include already defined circuits in the new circuits we build and connect them using appropriate wires and gates.

In diagrams, we simply represent an included subcircuit as a rectangle with inputs on the left-hand side and outputs on the right-hand side and consider it as a new kind of gate.

In equational definitions, we use the same technique as for submodule inclusion in the full Esterel language. To include a subcircuit $C'$ in a circuit $C$, we simply write the name $C'$ in place of a definition in $C$. This amounts to renaming the local and register wires of $C$ by new names unknown in $C$ to avoid name clashes and copying the renamed definitions of $C'$ into $C$. The input and output variables of $C'$ are captured by the variables of $C$ that have the same name. An input variable of $C'$ can be captured by any variable of $C$. Since it has a definition in $C'$, an output variable of $C'$ cannot be defined elsewhere in $C$.

We can also rename input or output variables of $C'$ before copying it, using the notation $C'[w_1/w'_1, w_2/w'_2, \dots]$. Then the input or output names $w'_1, w'_2, \dots$ of $C'$ are captured by the names $w_1, w_2, \dots$ of $C$. The formal definition is trivial and boring.

## 10.4.2 Definitions by Implications

The Esterel circuits will contain many *or*-gates used to gather signal emissions and completion codes. Instead of making these gates explicit in the equations, we shall leave them implicit and define the output of an *or*-gate

<footnote>time when setting the new register values. Furthermore, we assume that standard wires are recomputed only from new inputs and that their old value has disappeared. See [39] for a more accurate discussion of the electrical model.</footnote>
as being separately implied by each input. This will greatly shorten our
formal translation in Chapter 13.

Syntactically, we use implication definitions of the form $w \Leftarrow e$, which are read “$e$ implies $w$”. There can be several implications $w \Leftarrow e_i$ per wire, and the value of $w$ is then defined by the equality $w = \bigvee_i e_i$. This way, an equation

$$w = e \lor e'$$

can be replaced by two implications

$$w \Leftarrow e$$

$$w \Leftarrow e'$$

which do not need to be syntactically related to each other. In hierarchical
circuits, the implication definitions of a wire will actually be scattered in
several subcircuits. This is the main advantage of the extension, which has
some object-oriented flavor: $w \Leftarrow e$ can be read “send $e$ to $w$ as an input”.

If a wire has one implication definition, it can only have other implication
definitions; it is not allowed to mix the different definition forms. A local or
output wire that has no definition in a circuit is assumed to be defined by
an empty implication and to have value 0. This exactly corresponds to our
previous graphical convention that an undriven output is implicitly unset.
# Chapter 11

## The Basic Circuit Translation

In this informal (but precise) chapter, we explain the basic principles of the translation of Esterel kernel programs into circuits. The translation we present is essentially that of [4], with a modification in the handling of the parallel statement w.r.t. constructiveness. The basic translation is only partially correct because of the schizophrenia problem already mentioned in [4]. This problem will be solved later on in Chapter 12.

### 11.1 Structure of the Esterel Circuit

The basic translation is purely structural, and it closely follows the state semantics rules. The substatements of a statement are first translated, and the obtained circuits are then combined using appropriate auxiliary gates and wiring.

Since only '1' (pause) statements are decorated in the state semantics, we associate a register with each '1' statement, all the other statements only generating combinational logic. Selected 'î' statements correspond to registers set in the current circuit state. An additional boot register is introduced to implement the added initial 'î' state. The reactions exactly correspond to clock cycles.
<figure><img src="image_11.png" /><figcaption>Figure 11.1: Circuit associated with a statement</figcaption></figure>

## 11.2 The subcircuit generated by a statement

We now describe the interface of the circuit generated by a statement and the way in which the circuit should behave.

### 11.2.1 Subcircuit Interface

The interface is pictured in Figure 11.1. The left pins and the leftmost top pin E are input ones, while the right pins and the rightmost top pin E' are output ones. The meaning of the pins is as follows:

* The **GO** input pin is used to start the statement afresh, i.e. to execute an s-rule in the state semantics. This occurs when **GO** is set.

* The **RES** input pin is used to resume the execution of a selected statement, i.e. to execute an r-rule in the state semantics. This occurs when **RES** is set.

* The **SUSP** input pin is used to suspend the execution of the statement, according to the state semantics rule (*r-suspend+*). Suspension occurs when **SUSP** is set. Then, the registers keep their current value unless killed because of the **KILL** input below.

* The **KILL** input pin is used to unset the registers of the statement in case of a trap exit. This occurs when **KILL** is set by the translation of a trap statement {*p*}, as specified by rule (*sr-term-trap*). The **KILL** signal is propagated by all statements towards the **pause** registers.
* The `SEL` selection output pin indicates that the statement is a state currently selected for resumption, i.e. that some internal **pause** register is set. The `SEL` signal is simply the disjunction of the internal registers.

* The output pins `K0`, `K1`, etc. correspond to completion codes. There are $n + 2$ such pins if $n$ is the number of traps in which the statement is enclosed. When the statement is either started or selected and resumed, the pin that corresponds to the completion code returned by the statement is set. If the statement is not executed, i.e. if it is not started, not selected, or not resumed if selected, then the statement circuit explicitly unsets all `K` pins. Notice that completion codes are unary encoded (one-hot in hardware terminology).

* The pins `E` and `E'` correspond to the signal interface. They are not simple pins but compound pins or *buses*, containing one elementary pin per signal visible in the scope of the current statement. The `E` input bus is for input to the statement, corresponding to the input event `E` in the semantics. The `E'` output bus pin is for output from the statement, corresponding to the output event `E'`. We shall freely extract specific signals `s` or `s'` out of `E` or `E'`. As for the `K` pins, the `E'` pins are explicitly unset when the statement is not executed, i.e. when $\neg(\mathbf{GO} \lor (\mathbf{RES} \land \mathbf{SEL}))$.

### 11.2.2 Execution Scheme

The basic execution scheme consists in first setting `GO` to start execution, and then setting `RES` at each clock cycle. At each cycle, control propagates combinationally within the statement circuit; the completion wire corresponding to the returned completion code is set, and the registers corresponding to the reached **pause** statements are set to resume execution from the right state in the next cycle. The visible Esterel signals are received and emitted through `E` and `E'`.

To suspend the statement for the cycle, we set `SUSP` instead of `RES` (`RES` and `SUSP` are never set at the same time). If the statement is preempted by some internal or concurrent trap exit, we set `KILL` to unset the **pause** registers.

The selection wire `SEL` is propagated upwards in compound statements. It remains set as long as some pause registers are set, i.e. as long as the statement is selected. It becomes unset at the cycle that follows termination or trap exit, unless the statement has been immediately restarted by some
loop. The `SEL` wire is necessary since `RES` may also be sent to currently un-
selected statements. When `RES` is set, unselected statements should remain
silent, i.e. should unset all output signal and completion wires. This is done
by internally anding `RES` and `SEL`.

Since it is possible to instantaneously loop back into a statement, several elementary behaviors of a subcircuit can be superimposed in the same instant. This will be neglected for the moment and fully analyzed in Chapter 12.

### 11.2.3 Constructive Semantics of the Program and Circuit

The circuit of a statement is carefully designed to achieve full correspondence
between the constructive information propagation in the circuit and the
constructive semantics of the source Esterel statements. The propagation
of 1's implements the *Must* calculation and state change as specified by
the semantic rules. The propagation of 0's exactly implements the *Cannot*
calculation. The partial statuses {+, -, ⊥} of a signal *s* are encoded as
follows: status is $s^+$ if the *s* wire has been proved to have value 1, status
is $s^-$ if the *s* wire has been proved to have value 0, and status is $s^⊥$ if nothing
has been proved for *s*. See Section 11.5 for a concrete example.

## 11.3 Translating the Kernel Esterel Statements

We now show by pictures how each Esterel kernel statement is translated
into a circuit. To make the pictures simpler, we use two conventions:

* Unused inputs are not pictured.

* Not all outputs are pictured. An omitted output is assumed to be explicitly unset, i.e. to be driven by a 0 constant (see Section 10.1.2).

### 11.3.1 Translation of Completion Codes

The translation of a completion code $k \neq 1$ (termination or trap exit) is
obvious: the `GO` input is connected to the corresponding completion output,
as shown in Figure 11.2. This implements rule (*s-term-exit*), as well as *Must*
and *Can* rules.

The translation of the `pause` statement, i.e. completion code 1, is pictured
in Figure 11.3. The `pause` register drives the `SEL` selection wire. The register
is potentially set in two cases:
<figure><img src="image_12.png" /><figcaption>Figure 11.2: Circuit for a completion code $k \neq 1$</figcaption></figure>

<figure><img src="image_13.png" /><figcaption>Figure 11.3: Circuit for *pause*, i.e. completion code 1</figcaption></figure>
<figure><img src="image_14.png" /><figcaption>Figure 11.4: Circuit for !s</figcaption></figure>

* when `GO` is set, i.e. when the `pause` statement starts, according to rule (s-pause);

* when `SUSP` and `SEL` set are set, i.e. when the `pause` statement is selected, according to rules (r-suspend+).

According to rules (sr-term-trap) and (sr-prop-trap), actual setting of the register occurs only if `KILL` is unset, i.e. only if the `pause` statement is not preempted by some trap exit.

Termination wire `K1` is set when `GO` is set, according to rule (s-pause). Termination wire `K0` is set when the `pause` statement terminates, i.e. when both `SEL` and `RES` are set, according to rule (r-pause). The *Must* and *Can* rules are also correctly implemented.

### 11.3.2 Translation of the Emit Statement

As shown in Figure 11.4, to translate !s, we just connect the input `GO` wire to the `K0` termination output pin and to the `s'` signal emission output pin. This implements rule (s-emit).

### 11.3.3 Translation of the Present Statement

The translation of a present statement `s?p`, `q` is shown in Figure 11.5. We put the circuits of `p` and `q` in parallel, we build a switch for the `GO` wire according to the value of the `s` input that we extract from `E`, we send `RES`, `SUSP`, and `KILL` to both subcircuits, and we join their outputs using *or* gates.

Since the switch on `GO` makes the respective `GO` inputs of the subcircuits incompatible, only one of them can be started at a time. Therefore, in each following instant, only one of the subcircuits can be selected, as in the state semantics. Constructive information propagation works as follows:

* When `GO` is set, i.e. when the circuit is started, there are three cases:
<figure><img src="image_15.png" /><figcaption>Figure 11.5: Circuit for $s?p,q$</figcaption></figure>
- The s wire is set, i.e. s is known to be present. The GO input of p is set, which implements rule (s-present+). The GO input of q is unset, and the circuit of q unset all its output pins. Since 0 is neutral for an or gate, the 1's and 0's generated by p propagate to the E' and Ki outputs, exactly as required by the definition of Must and Can.

- The situation is symmetrical if s is unset, i.e. if s is known to be absent.

- If s is yet unknown, then the GO inputs of the subcircuit are also unknown. No 1 propagates to outputs, yielding the $\langle \emptyset, \emptyset \rangle$ result required by the Must formula. As far as 0's are concerned, we must calculate

$$ \overline{Can^{\perp}(p, E) \cup Can^{\perp}(q, E)} = \overline{Can^{\perp}(p, E)} \cap \overline{Can^{\perp}(q, E)} $$

This is indeed what the output or gates implement, since 0 propagates through an or gate if and only if both inputs are 0. Correct computation of Can is propagated by induction from p and q to s? p, q.

* Assume RES is set. It is then broadcast to the circuits of p and q. There are two subcases:

- If SEL is unset, the circuit is not currently selected. This is also true for the subcircuits of p and q, which unset all their outputs. The output or gates adequately unset the outputs.

- If SEL is set, then only one of the subcircuits is selected. Assume it is that of p. Then, p is executed as required by rule (r-then), and q unset all its outputs, which ensures correct propagation of p's results and Can values by the output or gates.

### 11.3.4 Translation of suspension and strong preemption

The translation of the suspension statement $s \supset p$ is shown in Figure 11.6. Since suspension does not occur in the first instant, the GO wire is directly connected to the subcircuit's GO input pin. The resumption wire RES is anded with the selection wire SEL to avoid resuming an unselected subcircuit, and this conjunction drives a switch on the s signal, which is extracted from E. If s is absent, the RES input pin of the subcircuit is set for normal
<figure><img src="image_16.png" /><figcaption>Figure 11.6: Circuit for $s \supset p$</figcaption></figure>

resumption. If $s$ is present, the SUSP suspension pin of the subcircuit is set for suspension, and $K1$ is set since we must return completion code 1. Suspension of the subcircuit also occurs if the input SUSP wire is 1. The KILL wire is directly fed into the subcircuit.

Although it is not a kernel statement, it is practically useful to directly implement the strong abortion statement $s \gg p$ or “do $p$ watching $s$”, since its kernel expression given in Chapter 2.4 is quite heavy. The implementation is shown in Figure 11.7. Since preemption does not occur in the first instant, the GO wire is directly connected to the subcircuit’s GO input pin. The SUSP and KILL wires are also directly connected. Once and-ed with SEL, the RES wire drives a switch on $s$. If $s$ is absent, resumption is passed to the subcircuit. If $s$ is present, the subcircuit RES pin receives 0 and the KO termination pin receives 1 to indicate termination.

### 11.3.5 Translation of Sequencing

The translation of a sequence $p$; $q$ is easy and shown in Figure 11.8. The input GO wire is sent to the GO pin of $p$, and the termination wire KO of $p$ is sent to the GO input of $q$ to ensure immediate sequencing. All the other input wires are broadcast, and the output wires are or-ed. Correctness of the translation relies on the fact that the subcircuits of $p$ and $q$ cannot be both simultaneously selected.

Constructive propagation of 1's and 0's calculates *Must* and *Can* in the same way as for $s? p, q$. This is left to the reader.
<figure><img src="image_17.png" /><figcaption>Figure 11.7: Circuit for $s \gg p$</figcaption></figure>

<figure><img src="image_18.png" /><figcaption>Figure 11.8: Circuit for $p; q$</figcaption></figure>
<figure><img src="image_19.png" /><figcaption>Figure 11.9: Circuit for $p*$</figcaption></figure>

### 11.3.6 Translation of Loop

As shown in Figure 11.9, to translate a loop $p*$, we simply feedback the $K0$ termination wire into the $GO$ input. Of course, this can create combinational cycles. A cycle occurs if there is a direct path from $GO$ to $K0$. Requiring a program to be loop-safe is enough to make this problem harmless. Nastier cycles may appear through signal wires; their analysis deferred to Chapter 12. Since a loop cannot terminate, the output termination wire $K0$ has value 0, which is made explicit here for clarity.

### 11.3.7 Translation of Parallel

The circuit of a parallel statement $p|q$ is pictured in Figure 11.10. It is built by putting the circuits of $p$ and $q$ in parallel and synchronizing their outputs using a synchronizer subcircuit to achieve the required semantical effect, i.e. the *Max* computation of completion codes.

The $GO$, $RES$, $SUSP$, $KILL$ and $E$ wires are broadcast to the subcircuits of $p$ and $q$. The global $SEL$ output is the disjunction of the $SEL$ output of the components, and the output signal wires are *or*-ed according to the semantic rules.

The heart of the synchronizer is the constructive *Max* circuit pictured in Figure 11.11. Given two sets of completion codes $L$ and $R$, the *Max* circuit
<figure><img src="image_20.png" /><figcaption>Figure 11.10: Circuit for $p|q$</figcaption></figure>

<figure><img src="image_21.png" /><figcaption>Figure 11.11: The constructive Max circuit</figcaption></figure>
computes $Max(L, R)$ using the following formula<fnref n="1" />.

$$ 
\begin{aligned}
Max(L, R) &= \{max(l, r) \mid l \in L, r \in R\} \\
&= \{i \in N \mid i \geq min(L)\} \cap (L \cup R) \cap \{j \in N \mid j \geq min(R)\}
\end{aligned}
$$

Each of the three components of the intersection is computed by a row of **or** gates in the *Max* circuit. The auxiliary **LEM** and **REM** inputs are used to control the cases where the left or right set is empty. Assume for example $L = \emptyset$. In the circuit, this is represented by **LEM** = 1 and **L0** = **L1** = ... = 0. In this case, the upper part of the circuit is innocuous and the result is **R** as required by the formula $Max(\emptyset, R) = R$.

In the parallel circuit, **LEM** and **REM** are controlled according to rules (**r-both**), (**s-both**), (**r-left**), and (**r-right**).

* When resuming $\hat{p} \mid \hat{q}$ according to rule (**r-both**) or when starting $p \mid q$ according to rule (**s-both**), we know that each branch will return a termination code and we unset **LEM** and **REM**. Given the left and right completion codes $l$ and $r$, represented by $Ll = 1$ and $Rr = 1$, the *Max* circuits compute the maximum $k = max(l, r)$, represented by $Kk = 1$. In addition, the *Max* circuits propagate 0's as required by the computation of *Can*. For example, from $L0 = L1 = 0$ we deduce $K0 = K1 = 0$ without any knowledge of $R0$ and $R1$. (In [4], we used a simpler circuit to compute $max(k, l)$; it turns out that this circuit did not propagate 0's in the same way and did not implement the constructive semantics.)

* When resuming $\hat{p} \mid q$ according to rule (**r-left**), **REM** is set by the **nor**-gate in the parallel circuit, and the 0's and 1's of $\hat{p}$ are directly propagated to the outputs of the parallel circuit.

* When resuming $p \mid \hat{q}$ according to rule (**r-right**), **LEM** is set symmetrically.

### 11.3.8 Translation of Trap and Shift

The circuit for {$p$} is shown in Figure 11.12. As required by the definition of the $\downarrow k$ operator on completion codes, we or the termination wires of code 0

<footnote n="1">¹The reader familiar with the application of 2-adic number theory to circuits' [42] might prefer a beautiful arithmetico-logical formula due to G. Gonthier, where '–' denotes arithmetic opposite: $Max(L, R) = (L \lor \neg L) \land (L \lor R) \land (R \lor \neg R)$.</footnote>
<figure><img src="image_22.png" /><figcaption>Figure 11.12: Circuit for {$p$}</figcaption></figure>

(termination) and 2 (exit of current trap), to build the new termination wire K0. The wire K1 is left unchanged, and the other termination wires are shifted downwards.

In the translation of $\uparrow p$, shown in Figure 11.13, the completion codes are simply shifted according to the definition of the $\uparrow k$ operator.

### 11.3.9 Translation of local signal declaration

To translate a local signal declaration $p\s$, we simply close the signal $s$ by equating the $s$ and $s'$ wires. This is pictured in Figure 11.14. The closure can create combinational loops to be handled by the constructiveness analysis of the circuit, see Chapter 4.

Constructive information is correctly propagated according to the recursive definitions of Chapter 7. If $s$ is emitted by $p$, then $p$ sets $s'$, a fact that is fedback into $s$ as in the recursive definition of *Must*. If $s$ cannot be emitted, then $p$ unsets $s'$, which is fed back into $s$.

## 11.4 The Global Environment

To translate a full program of body $p$ into a circuit, we must place the circuit of $p$ in a suitable environment pictured in Figure 11.15. The GO wire is
<figure><img src="image_23.png" /><figcaption>Figure 11.13: Circuit for $\uparrow p$</figcaption></figure>

<figure><img src="image_24.png" /><figcaption>Figure 11.14: Circuit for $p\backslash s$</figcaption></figure>
<figure><img src="image_25.png" /><figcaption>Figure 11.15: The global environment</figcaption></figure>

initially set and then unset at all following cycles by the *boot register*, which corresponds to the added initial $\hat{l}$ in the state semantics. Notice that a register with a negation added on each side acts as a register initialized to 1. The *RES* wire is permanently set; the initial value 1 is harmless since no sub-circuit is initially selected. The global *SUSP* and *KILL* wires are permanently unset. The *K0* output is renamed into *DONE* to indicate that the body has terminated, an information that is not part of the semantics but convenient in practice. The global *SEL* and *K1* wires are useless. Finally, the input and output wires are respectively connected to the *I* and *O* signal buses.

## 11.5 A Constructive Execution Example

Using example P2, page 29, we now show how the constructive evaluation of an *Esterel* program is adequately performed by the constructive evaluation of its circuit. We recall the code of P2:

module P2:
signal S in
    emit S;
present 0 then
    present S then
        pause
        end;
        emit 0
    end
end signal
<figure><img src="image_26.png" /><figcaption>Figure 11.16: Circuit for program P2</figcaption></figure>

The circuit obtained from P2 is pictured in Figure 11.16. To make the drawing simpler, we simplified the translation of **pause**, using the global environment definitions `RES = 1` and `SUSP = KILL = 0`: in this environment, a **pause** statement boils down to a register.

In the first instant, the boot register sends a 1 to the `S`' wire, thus executing `"emit S"`, and a 1 to the test for `0`, which is represented by the leftmost **and** gates. Since `0`'s status is yet unknown, control cannot propagate further, neither to the `0+` wire, which triggers the **then** case, nor to the `0-` wire, which triggers the **else** case. However, the information `S' = 1` feeds back into the test for `S`, which is represented by the two middle **and** gates. From `S = 1`, we deduce `S- = 0`. Since the **pause** register is initially `0`, we deduce `0' = 0`, i.e. that we cannot emit `0`. From `0 = 0`, we now deduce `0+ = 0` and `0- = 1`, which determines all the other wires.
# Chapter 12

## Schizophrenia

The relatively simple translation of a loop-safe Esterel program *P* into a hardware circuit *C* we have given in Chapter 11 is essentially linear in size: the size of *C* measured in number of gates is linearly bigger than the size of *P* measured in number of kernel statements. If the circuit *C* is constructive, then it can be shown that the program *P* is also constructive and that the behavior of *C* coincides with that of *P*. However, the basic translation is only partially correct: there exist constructive programs that yield non-constructive cyclic circuits, because of the schizophrenia problem we study in this section.

The problem is related to combinational feedback. In the circuit construction, there are exactly three places where an output of a subcircuit is combinationally fed back into the same subcircuit:

* The translation of a loop *p**. This is the source of the schizophrenia problem.

* The translation of a trap statement {$p$}, where the K2 output is fed back into the KILL input. This feedback is harmless since the KILL wire is propagated straight to the registers by all statement translations. No combinational loop can be created.

* The translation of a local signal statement $p\s$. Creating combinational loops involving signals is normal, there as in Esterel proper. The whole point of constructive analysis is to determine whether signal loops are sensible.
<figure><img src="image_27.png" /><figcaption>Figure 12.1: Circuit for sustain s = (!s; 1)*</figcaption></figure>

12.1 A Correctly Translated Loop

Consider the statement “sustain S”, i.e. (!s; 1)*. The circuit translation
is pictured in Figure 12.1. The K0 output of the pause subcircuit feeds back
to the GO input, but no combinational cycle is created and the translation is
correct. Of course, the circuit almost vanishes by constant propagation.

In the second instant, the (r-pause) and (s-pause) behaviors are harm-
lessly superimposed in the pause subcircuit: both RES and GO inputs of the
subcircuit are set, and the subcircuit sets both its K0 and K1 completion
outputs.

12.2 Schizophrenic Parallel Synchronizers

Consider now the following apparently trivial variant of "sustain S":

module P16:
loop
    emit S;
    [ nothing || pause ]
end loop

written (!s; (0 | 1))* in terse syntax.
<figure><img src="image_28.png" /><figcaption>Figure 12.2: Incorrect basic circuit for (!s; (0 | 1))*</figcaption></figure>

Semantically speaking, the added **nothing** statement is completely in-
nocuous. However, the basic translation builds the non-constructive circuit
pictured in Figure 12.2. The **FORK** label shows where the parallel statement
starts. The loop feeds back the **K0** termination output to **FORK**. The unstable
combinational loop is drawn in dotted lines. In the first instant, the circuit is
constructive: **S** is emitted, the boot register is unset, and the **pause** register
is set. In the second instant, the **pause** register sets the two lower inputs
of the **K0** completion gate. Therefore, to compute the value of this gate, we
need to compute the dotted top input. For this, we have to compute the
value of the **FORK** wire, which itself requires computing the value of **K0**, hence
the non-constructiveness.

Consider now the state semantics. Omitting the auxiliary boot state-
ment, the state of interest is (!s; (0 | 1))*. The constructive state transition
is

$$
(!s; (0 | \hat{1}))^* \underset{s^+}{\stackrel{s^+, 1}{\rightleftharpoons}} (!s; (0 | \hat{1}))^*
$$

This transition is proved using rule (r-do-loop) in the following way:

$$
\frac{!s; (0 | \hat{1}) \underset{s^+}{\stackrel{\emptyset, 0}{\rightleftharpoons}} !s; (0 | 1) \qquad !s; (0 | 1) \underset{s^+}{\stackrel{s^+, 1}{\rightleftharpoons}} !s; (0 | \hat{1})}{(!s; (0 | \hat{1}))^* \underset{s^+}{\stackrel{s^+, 1}{\rightleftharpoons}} (!s; (0 | \hat{1}))^*}
$$

The first premise is proved using rules (r-seq3), (r-right), and (r-pause),
while the second premise is proved using rules (s-seq2), (s-emit), (s-both), (s-term-exit) for 0, and (s-pause) for 1.

The key point is that the parallel statement is *instantaneously reincarnated* by the loop: when resumption of state 0 | ˆ1 terminates, the parallel is reincarnated as 0 | 1. Each incarnation performs a separate transition:

$$ \frac{\hat{1} \underset{s^+}{\stackrel{\emptyset, 0}{\rightleftharpoons}} 1}{0 | \hat{1} \underset{s^+}{\stackrel{\emptyset, 0}{\rightleftharpoons}} 0 | 1} \qquad (r-right) $$

$$ \frac{0 \underset{s^+}{\stackrel{\emptyset, 0}{\rightleftharpoons}} 0 \quad 1 \underset{s^+}{\stackrel{\emptyset, 1}{\rightleftharpoons}} \hat{1}}{0 | 1 \underset{s^+}{\stackrel{\emptyset, 1}{\rightleftharpoons}} 0 | \hat{1}} \qquad (s-both) $$

In the basic circuit of Figure 12.2, there is a single parallel synchronizer whose wires cannot be reincarnated dynamically. We ask the synchronizer to perform two distinct synchronizations at a time, which is impossible. This is what we call schizophrenia. Clearly, some logic duplication is necessary to get rid of schizophrenia.

## 12.3 Schizophrenic Signals

Local signals are also subject to instantaneous reincarnation. Consider the following statement:

```python
module P17:
loop
    signal S in
        present S then emit 0 else nothing end;
        pause;
        emit S
    end signal
end loop
```

written (((s?!o,0); 1; !s)\s)* in terse syntax. In the first instant, S is absent, O is not emitted, and we reach the state (((s?!o,0); ˆ1; !s)\s)*, omitting the dead boot statement. In the second instant, execution resumes from ˆ1, the signal S is emitted, and the loop loops. Since the declaration
<figure><img src="image_29.png" /><figcaption>Figure 12.3: Incorrect basic circuit for (((s?!o, 0); 1; !s)\s)*</figcaption></figure>

of $S$ is re-entered, the body is executed with a *fresh incarnation* of $S$, which is not emitted. Therefore, the test takes its **else** branch, **O** is not emitted, and we are back to the same state.

The (simplified) basic circuit translation is pictured in Figure 12.3. The circuit is constructive, but it behaves incorrectly in the second instant. The $S'$ wire is set by the **pause** register, and it is directly fed back into the presence test. The test takes its **then** branch and provokes emission of **O** instead of taking its **else** branch as in the semantics.

The key point is that the basic translation does not take into account the scope of $S$. The statement is translated as if it were (($s?!o, 0$); $\hat{1}$; !s)*\s, which indeed emits $o$ in the second instant since $s$ does not reincarnate any more. A finer translation is clearly needed to correctly handle the instantaneous reincarnation of $S$ induced by scoping.

## 12.4 An Easy Solution

An easy solution is to duplicate the body of each loop, transforming $p*$ into ($p$; $p$)*, which is semantically equivalent. The parallel example becomes
loop
    emit S;
    [ nothing || pause ];
    emit S;
    [ nothing || pause ]
end loop

and the basic circuit now has two distinct synchronizers able to perform the
two simultaneous synchronizations. The signal example becomes

loop
    signal S in
        present S then emit 0 end;
        pause;
        emit S
    end signal;
    signal S in
        present S then emit 0 end;
        pause;
        emit S
    end signal
end loop

and the basic translation now allocates two distinct wires for the two syn-
tactically distinct local signals.

To correctly handle nested loops, duplication must be done in a recursive
way: inner loops must be first expanded before duplicating a loop body.
The circuit can become exponential in the size of the program, which is
not practical. Furthermore, registers get duplicated, which is very bad for
optimization and verification purposes. We need a better solution, which we
shall find by analyzing more carefully the structure of proofs in the state
semantics.

12.5 The Surface and Depth of a Statement

Schizophrenic conflicts are always created by rule (r-do-loop). In this rule,
the subjects of the premises are respectively a proper state $\hat{p}$ and the base
standard statement $p$. Therefore, conflict occurs only between the surface
and the depth of the circuit, which are defined as follows:
<figure><img src="image_30.png" /><figcaption>Figure 12.4: Correct circuit for (!s; (0|1))*</figcaption></figure>

* The *surface* is the part that is driven by the **GO** input. The surface acts when the statement is started.

* The *depth* is the part of the circuit that is driven by the **RES** input and the **pause** registers at resumption time. The depth acts when the statement is selected and resumed.

In the basic translation, the surface and depth need not be disjoint. In "sustain S", Figure 12.1, the !s statement is both in the surface and in the depth. In this case, everything works fine since it is harmless to emit a signal twice. In Figure 12.2, there is a single synchronizer for the surface and the depth. Since the surface and depth must simultaneously perform incompatible synchronization, the synchronizer is schizophrenic. In Figure 12.3, schizophrenia comes from the fact that there is a single signal buffer for the depth and surface signals, which should have distinct statuses at the same time.

The solution to avoid schizophrenia is to always keep the surface and depth entirely disjoint. This can be done without duplicating the registers,
<figure><img src="image_31.png" /><figcaption>Figure 12.5: Correct circuit for (((s?!o,0); 1; !s)\s)*</figcaption></figure>

using a reasonable amount of logic duplication.

A correct translation of P16 is pictured in Figure 12.4. It uses separate synchronizers for the surface and the depth. The top surface synchronizer is called SYN[0], and the bottom depth synchronizer is called SYN[1]. The parallel statement is initially started using the surface synchronizer, which detects pausing and sets K1[0]. In the next instants, the selected pause register sets the termination input R0[1] of the depth synchronizer SYN[1], which reports immediate termination of the parallel statement by setting the output K0[1]. The parallel is immediately restarted and the inputs L0[0] and R1[0] of the surface synchronizer SYN[0] are set. The surface synchronizer reports pausing by setting K1[0].

At first glance, the new circuit looks much bigger than the old one. However, when constants are propagated, almost nothing is left of the circuit, and there is no practical penalty to the duplication. The LEM and REM inputs are also handled in a simpler way:

* In the surface synchronizer, we set LEM = REM = 0 since we know that each branch will act and return a termination code when the parallel is started by setting GO.

* In the depth synchronizer, a branch will return a termination code if and only if it is selected. The negation of the branch selection wire is connected to the auxiliary input.
A correct translation of P17 is pictured in Figure 12.5. It uses two wires for S. The surface signal wire S[0] has input 0 since the surface incarnation of S has no emitter, and the depth signal wire S[1] is not connected to any gate since the depth incarnation is not tested for presence, as in the state semantics.

## 12.6 Multiple Reincarnation

So far, we have seen cases where a statement has two simultaneous incarnations. Nesting loops, traps, and parallel statements can lead to more complex situations with multiple reincarnation of parallels and signals. Consider program P18 in Figure 12.6. In the first instant, the three `pause` statements are selected, `S1` and `S2` are not emitted, and `not_S1_and_not_S2` is emitted. In the second instant, the constructive behavior is as follows:

* The three `pause` statements terminate, `S1` and `S2` are emitted, and `S1_and_S2` is emitted by the `present` statement.

* The trap `T2` is exited by the `exit T2`` statement, the inner loop loops, and a new signal `S2` is declared. This new signal is absent since it cannot be emitted, while the current `S1` is still present. The `present` statement is instantaneously re-executed with `S1` present and `S2` absent, and it emits `S1_and_not_S2`.

* The trap `T1` is exited by the `exit T1` statement and the outer loop loops. A new `S1` and a new `S2` are declared. Since none of these new signals can be emitted, the `present` statement is executed again with `S1` and `S2` absent, and `not_S1_and_not_S1` is emitted.

In this constructive behavior, `S1` has two simultaneous incarnations, a present depth incarnation and an absent surface incarnation, while `S2` has three incarnations, one present and two absent. In terms of depth and surface<fnref n="1" />, the first one in constructive execution order can be called a *depth-depth* incarnation since it is both in the depth of *signal S1* and in the depth of *signal S2*, the second one can be called a *depth-surface* incarnation since it is in the depth of *signal S1* and in the surface of *signal S2*, and the third one can be called a *surface-surface* incarnation since it is in the surface of both signal declarations. Accordingly, the `present` statement has three different active incarnations with three different behaviors.

<footnote n="1">¹Here, we ignore the parallel statements. See Section 12.7.4 for the accurate naming.</footnote>