1 Esterel in Racket, for Racket Programmers🔗ℹ

One way to think of imperative computation is as if the program goes through a series of different states, where each step in the computation updates a bunch of variables, causing the program to be in a new state. In this sense, the computation proceeds through a series of different states as it executes and the programmer, to be able to understand and modify the program, must think about these state changes when imagining the program’s behavior. In this sense, Esterel is an imperative programming language but, unlike more conventional imperative programming languages, Esterel’s state changes are more restricted, giving the programmer more guarantees about the behavior of the program.

In Esterel, to restrict the state changes, the program is broken up in a series of instants (also called reactions). Within each instant, the entire program always sees a coherent, single state. That is, within an instant there are no state changes; instead each instant computes a new state and the entire Esterel program sees only that new state. Furthermore, each instant is captured via a construct in the programming language, pause. That is, each thread must, after some finite amount of time, invoke pause (or terminate or be aborted) and the time between these pauses always has a single consistent state, visible to the entire computation.

Of course, Esterel’s enforcement of determinacy during each instant applies only to Esterel programs and Esterel threads; Racket’s threads are not required to explicitly pause and remain as complex and difficult to reason about as ever.

Separating Esterel computation from normal imperative Racket computation, however, is simply a matter of wrapping esterel around some expressions. Any code that runs in the dynamic extent of those expressions is treated as Esterel code. Unfortunately, ordinary Racket mutable variables do not automatically become Esterel-like; instead, the Esterel code must use signals for any values that change over time. Unfortunately, Esterel computations do not check or guarantee that Racket code run during an instant is otherwise pure, and surprising behavior may result if Racket code uses mutation while it is running in an Esterel context. We return to this point in Using Continuations to Replay Reactions and How Mutation Causes Trouble; for now, simply imagine only pure Racket code running alongside Esterel.

1.1 A Traffic Light🔗ℹ

To make this abstract notation of state change and pauses and instants more concrete, let’s look at some code that controls a traffic signal with three lights: red, orange, and green. Red means that cars should stop; orange means that red is coming soon, so either slow in preparation to stop or finish transiting the intersection; green means that it is safe to transit the intersection.

To control the lights we will use three signals. A signal in Esterel has two states: either it is present or it is absent. Signals can also carry values, but to control our traffic light, we’ll just use presence to indicate that the light should be on and absence to indicate that it should be off. Here’s how we declare the signals:

(define-signal red orange green)

This introduces three new Racket identifiers, red, orange, and green, each bound to a signal.

To run an Esterel program, we need to wrap the code in esterel. Any code or helper functions can be invoked from inside. That is, Esterel code runs in the dynamic extent of esterel. For starters, let’s just make a traffic signal that is permanently red. Here’s the code to do that:

(define forever-red   (esterel    (let loop ()      (emit red)      (pause)      (loop))))

Looking at the code line by line, we see esterel, which wraps our Esterel program, then a recursive loop definition, followed by (emit red) which causes the signal red to be emitted and thus present. Then (pause), indicating that the instant is over. Once the next instant starts, it will pick up right at the pause, and go back around the loop, emitting the red signal again and pausing.

This code does not actually run yet, however. To run the code, we need to use react!. Each time we invoke react!, a single instant runs and react! returns the signals that were emitted, always red.

> (react! forever-red)

'#hash((#<signal: red> . #t))

> (react! forever-red)

'#hash((#<signal: red> . #t))

> (react! forever-red)

'#hash((#<signal: red> . #t))

In Esterel, repeatedly emitting a specific signal and pausing is a common pattern and is captured via the function sustain. Accordingly, this is the same program, but written more compactly:

(define forever-red   (esterel    (sustain red)))

Of course, we would like our traffic signal to change color so cars can pass through the intersection. Let’s say that our green should last two minutes, and then orange for four seconds, and then we’ll change to red. To set this up, we’ll introduce a signal that is emitted every second:

(define-signal second)

And now we turn to the loop that emits forever-red. A Rackety approach to this problem might be to change the loop so that it has a parameter and it counts the number of instants that passed where second is emitted, and based on that, emit the correct signal.

Instead, and because aborting is completely safe and reliable in Esterel, we can separate the code that is emitting the signal from the code that decides how long to wait, letting those the two tasks be handled in parallel, like this:

(par (abort (sustain red)

#:when (present? next-stage))

(begin (await (present? second) #:n 90)

(emit next-stage)))

The Esterel form par runs each of its subexpressions (in this case, the abort and the begin) in parallel to each other; it finishes only after both of them finish. The abort runs its first argument (the call to sustain) until the code following the #:when returns #t, at which point it aborts it. That abort is the only way to terminate the first branch of the par. Meanwhile, the second branch of the par runs the await, which waits until there have been 90 instants when second is present. After that, the await call returns and, in that same instant, the emit of next-stage happens, ending the entire par expression.

and use with-signal to make a local signal, next-stage, which is available only in the body of the with-signal.

For a more developed version of this example with some GUI code to see the traffic light change color, see esterel/examples/traffic-light.

1.2 Causality🔗ℹ

There is a subtle point about the semantics of Esterel and how it manages to give the each instant its own consistent world view. One way to understand it is to think that each instant, instead of a totally ordered linear notion of time it has, instead, a weaker notion of time, called causality. That is, we do not know (or need to care) exactly which events came before or after which other ones; instead we need to know only which events cause other events: that is enough to determine the flow of the computation.

In order to see how these aspects of Esterel computation play out, let’s start with a simple program. In this program, because S is not set, the program takes the else branch of the conditional and emits O2.

(define-signal S O1 O2)

> (react!    (esterel     (if (present? S)         (emit O1)         (emit O2))))

'#hash((#<signal: S> . #f) (#<signal: O2> . #t))

We can see the effect of S not being emitted and O2 being emitted in the result of react!, as the hash maps S to #f and O2 to #t.

But Esterel does not require the emission to be sequentially ordered with the present? test. Since Esterel’s notion of parallelism is deterministic, this program is guaranteed to behave as the previous one, always emitting O1 and never emitting O2, even though the test for S is done in parallel to the emission of S.

> (react! (esterel            (par (emit S)                 (if (present? S)                     (emit O1)                     (emit O2)))))

'#hash((#<signal: O1> . #t) (#<signal: S> . #t))

To understand this, we must turn to the idea of causality. That is, instead of a conventional understanding of the two parallel branches of this par as running at the same time as each other, another way to think of them is that there is no causality relationship between the two evaluations and thus Esterel is free to run them however it wants, subject to other causality dependencies being obeyed. In other words, to Esterel, the difference between combining two expression in parallel or sequentially is that combining them sequentially forces a causality ordering on them, but combining them in parallel does not.

Even though par did not introduce a causal dependency in this program, there still is a causality dependency introduced. Specifically, each use of emit introduces a causality dependency between it and any uses of present? (for the same signal). So, in this program, (emit S) causes the call (present? S) to return #true and therefore therefore we can take only the branch that emits O1 and not the one that emits O2.

This notion of causality determining the behavior of the program also comes with the possibility of a new kind of error, namely ones with causality problems. Such programs in Esterel are called “non constructive” and react! will raise an error when it encounters one. Here’s an example:

(define non-causal   (esterel    (if (present? S)        (emit S)        (emit S))))

> (react! non-causal)

react!: the program is not constructive

the signal blocking progress can be emitted

signal: #<signal: S>

When looking at this program from a simple logical perspective, we can see that it makes no sense for S to be absent since that would cause the if to take the else branch which would cause S to be emitted.

But, from a causality perspective, it also makes no sense for S to be present. There is nothing that happens in the program before the call to present? passing S (and thus no emits happen). Thus, from a causality perspective, since there is nothing that can cause S to be present, S must be absent. In order for this program to be error-free, the (emit S) that happens in the then branch is effectively causing information flow to go “backwards”, against causation, as present? cannot decide to return #t without looking into the future beyond the moment where it is invoked. Accordingly this program is an error.

1.3 Using Continuations to Replay Reactions and How Mutation Causes Trouble🔗ℹ

This section tries to explain, at a high-level how Esterel in Racket runs code in order to convey an intuition for how using Racket-level mutable state goes wrong inside esterel.

When a program runs within an instant, it runs in two modes: “can mode” and “must mode”.See Berry (2002)’s Constructive Semantics of Esterel for a fuller description of the Can and Must functions that these modes mimic. First, the program runs in “must mode” where present? does not return #f, but instead blocks (present? might return #t if an emit for the corresponding signal happens). In this mode, the code is running very much like regular Racket code runs; internally par is creating racket-level threads and with-trap creates an escape continuation.

At some point, however, all of the threads that are still running get blocked on calls to present? where the corresponding signals have not yet been emitted. At this point, the program enters “can mode”. It collects the set of all of the continuations of all of the threads that are blocked in this manner and then runs each of them forward multiple times, once for each possible assignments of absent and present to each of the signals that’s being blocked on. After this completes, either some of those signals were never emitted during this process, or the program is non-constructive. If there were some signals that were never emitted, they are set to absent and we return to “must mode”. If all of the blocking signals were emitted during at least one of these runs, the program aborts with the non-constructive error.

Accordingly, if one of the threads performs some mutation, then that mutation is not rolled back by the continuations, so it will happen possibly a large number of times and certainly more than just once.