From SSA to Synchronous Concurrency and Back

Keywords: code generation, compiler optimization, concurrency, declarative languages, embedded systems, language design, language implementation, real-time systems, semantics, software engineering, synchronous languages génération de code, optimisation de compilateur, concurrence, langages déclaratifs, systèmes embarqués, conception de langage, implémentation de langage, systèmes temps réel, sémantique, génie logiciel, langages synchrones

We are interested in the programming and compilation of reactive, real-time systems. More specifically, we would like to understand the fundamental principles common to generalpurpose and synchronous languages-used to model reactive control systems-and from this to derive a compilation flow suitable for both high-performance and reactive aspects of a modern control application. To this end, we first identify the key operational mechanisms of synchronous languages that SSA does not cover: synchronization of computations with an external time base, cyclic I/O, and the semantic notion of absent value which allows the natural representation of variables whose initialization does not follow simple structural rules such as control flow dominance. Then, we show how the SSA form in its MLIR implementation can be seamlessly extended to cover these mechanisms, enabling the application of all SSA-based transformations and optimizations. We illustrate this on the representation and compilation of the Lustre dataflow synchronous language. Most notably, in the analysis and compilation of Lustre embedded into MLIR, the initialization-related static analysis and code generation aspects can be fully separated from memory allocation and causality aspects, the latter being covered by the existing dominance-based algorithms of MLIR/SSA, resulting in a high degree of conceptual and code reuse. Our work allows the specification of both computational and control aspects of high-performance real-time applications. It paves the way for the definition of more efficient design and implementation flows where real-time ressource allocation drives parallelization and optimization.

Introduction

The Static Single Assignment (SSA) form [START_REF] Rosen | Global value numbers and redundant computations[END_REF][START_REF]Static single assignment book[END_REF] has proven an extremely useful tool in the hands of compiler builders. First introduced as an intermediate representation (IR) meant to facilitate optimizations, it became a staple of optimizing compilers. More recently, its semantic properties-e.g. functional determinism while still allowing for limited concurrency-established it as a sound basis for High-Performance-Computing (HPC) compilation frameworks such as MLIR [START_REF]Multi-level intermediate representation compiler framework (MLIR)[END_REF], where different abstraction levels of the same application1 share the structural and semantic principles of SSA, allowing them to co-exist while being subject to common analysis and optimization passes (in addition to specialized ones).

But while compilation frameworks such as MLIR concentrate the existing know-how in HPC compilation for virtually every execution platform, they lack a key ingredient needed in the high-performance embedded systems of the future-the ability to represent reactive control and real-time aspects of a system. They do not provide first-class representation and reasoning for systems with a cyclic execution model, synchronization with external time references (logical or physical), synchronization with other systems, tasks and I/O with multiple periods and execution modes.

And yet, as we shall see in this paper, while the standard SSA form does not cover these aspects, it shares strong structural and semantic ties with one of the main programming models for reactive real-time systems: dataflow synchrony [START_REF] Bergerand | Outline of a real time data flow language[END_REF][START_REF] Halbwachs | A synchronous language at work: the story of Lustre[END_REF], and its large and structured corpus of theory and practice of RTE systems design.

Contribution. Relying on this syntactic and semantic proximity, we extend the SSA-based MLIR framework to open it to synchronous reactive programming of real-time applications. We illustrate the expressiveness of our extension through the compilation of the pure dataflow core of the Lustre language. This allows us to model and compile all data processing, computational and reactive control aspects of a signal processing application. 2 In the compilation of Lustre, following an initial normalization phase, all data type verifications, buffer synthesis, and causality analysis can be handled using existing MLIR SSA algorithms. Only the initialization analysis specific to the synchronous model (a.k.a. clock calculus or analysis) requires specific handling during analysis and code generation phases, leading to significant code reuse.

The MLIR embedding of Lustre is non-trivial. As modularity based on function calls is no longer natural due to the cyclic execution model, we introduce a node instantiation mechanism. We also generalize the usage of the special undefined/absent value in SSA semantics [START_REF] Demange | Semantic reasoning about the sea of nodes[END_REF] and in lowlevel intermediate representations such as LLVM IR [START_REF] Lee | Taming undefined behavior in llvm[END_REF]. We clarify its semantics and strongly link it to the notion of absence and the related static analyses (clock calculi) of synchronous languages [START_REF] Benveniste | The synchronous languages 12 years later[END_REF].

Our extension remains fully compatible with SSA analysis and code transformation algorithms. It allows giving semantics and an implementation to all correct SSA specifications. It also supports static analyses determining correctness from a synchronous semantics point of view.

Outline. In Section 2 we formalize the SSA semantics. Section 3 extends SSA to allow reactive synchronous programming. Section 4.1 covers the embedding of Lustre into MLIR SSA and its compilation. In Section 4.2 we discuss our signal processing use case. We discuss related work in Section 5 before the conclusion in Section 6.

SSA syntax and semantics

The syntax and semantics of SSA form have been presented multiple times before, but we need to settle on one as a basis for extension. The particular SSA dialect we use is based on MLIR [START_REF]Multi-level intermediate representation compiler framework (MLIR)[END_REF], which uses a continuation-passing style (CPS) for the specification of φ operators, and uses opcode names br and cond_br for unconditional and conditional branches, respectively.

Core SSA syntax

The syntax, presented in Fig. 1, consists of a minimal SSA syntax (in black) extended with the constructs needed to represent function-based modularity (in red), and with the load and store operations allowing the representation of memory side effects (in green).

Syntactic correctness must be complemented by the respect of a number of structural properties. No two blocks of a function may have the same name, and branching operations (br and cond_br) may only reference existing blocks with the correct number of arguments. Each variable is either output of exactly one operation, or argument of a single block header. 3No two functions may have the same name, and calling a function assumes that it exists and has the correct interface. The interface of a function consists in the input arguments of its first basic block (which are also the function arguments) and the inputs of its return operation, which are the function outputs. If multiple return operations exist in a function, they must have the same number of arguments. Every function has an interface declaration, which summarizes the types of input and output arguments.

All SSA blocks are terminated by a return or a branch operation. These operations are called terminators.

Example

To illustrate the specific properties of reactive systems, and the differences between Lustre and SSA we use the small example of Fig. 2. The Lustre node (top) and MLIR SSA function (bottom) implement the same functionality, but we focus on the SSA function in this section. As we will see later, the latter could be the result of the compilation of the former.

Note that the MLIR SSA syntax requires that block identifiers start with "^" and that all variable names start with "%". It also provides more intuitive forms for the various operations: function calls specify the full function signature at their end; the comparison taking two input variables as arguments and producing one variable (the test result) has the syntax of line 22, which specifies the kind of test (sge for >=), the type of input data (i32), but not the type of the Boolean output, which is implicit (i1); operation select in line 23 outputs one of its data inputs based on the value of its Boolean test variable %ck (of type i1).

The blocks and the branching operations of an SSA function determine a sequential control flow graph (SCFG) structure, with the first block serving as control entry point. Inside each basic block, execution proceeds sequentially.

Our example is a stepper motor driver which receives rotation commands as increments in a 0.18 • basis, but can only actuate (issue physical commands to the motor) for 1.8 • at a time. For this reason, commands must be bufferized and only actuated when their number exceeds 10.

This behavior, typical of an embedded control system, involves a continuous interaction with the environment. In our example, this interaction is driven by the infinite loop formed by the SSA branching operations. Each iteration of the loop is an execution cycle during which the program reads its input %inc from its environment, performs computations, potentially actuates the motor and finally outputs %pos_nxt. Timely interaction with the environment is achieved through the function calls in violet, which are discussed in Section 3.

SSA operational semantics

For conciseness, we shall assume all variables (including Booleans) are semantically represented as integers. We also assume each operation of the program has a unique label, such as a program line number if we assume that no two operations share the same line.

Notations The cardinal of a set S is denoted |S|. We use the OCAML notation for lists: [] is the empty list, h :: t the list of first element h and tail t. To represent partial valuations (of variables, memory) we use fully defined functions, adding the special value ⊥-representing absence-to their codomain. We also denote ⊥ any function that is constant ⊥, regardless of its domain. Int is the domain of the integer type, and Int = Int ∪ {⊥}. Given a (mathematical) function f and a value x of its domain, f [x ← y] is the function that is identical with f everywhere except on x, where it has value y.

Execution state

The execution state of an SSA function f is one of:

• An initial state Start f (v 1 , . . . , v |in(b f 0 )| )
, where v i ∈ Int are the actual parameters of the function.

• A final state End f (w 1 , . . . , w O f ), where w i ∈ Int are the outputs of f (received as input by return). In blue, state manipulation.

Inria (Start f (v1, . . . , v |in(b f 0 )| ), cs, m) → (Run f (fst(b f 0 ), ⊥[in(b f 0 ) k ← v k | 1 ≤ k ≤ |in(b f 0 )|]
), cs, mem) (start) op(l) = "(v1, . . . , vn) = op_id(w1, . . . , wm)" (o1, . . . , on) = [[op_id]](s(w1) . . . , s(wm))

(Run f (l, s), cs, m) → (Run f (nxt(l), s[vi ← ai | 1 ≤ i ≤ n]), cs, m) (opcall) op(l) = "br bb(v1, . . . , v |in(bb)| )" (Run f (l, s), cs, m) → (Run f (fst(bb), s[in(bb)i ← s(vi) | 1 ≤ i ≤ |in(bb)|][loc(bb)i ← ⊥ | 1 ≤ i ≤ |loc(bb)|]), cs, m) (goto) op(l) = "cond_br v bb1(v1, . . . , v |in(bb1)| ) bb2(w1, . . . , w |in(bb2)| )" s(v) ∈ {0, ⊥} (Run f (l, s), cs, m) → (Run f (fst(bb1), s[in(bb1)i ← s(vi) | 1 ≤ i ≤ |in(bb1)|][loc(bb1)i ← ⊥ | 1 ≤ i ≤ |loc(bb1)|]), cs, m) (ifthen) op(l) = "cond_br v bb1(v1, . . . , v |in(bb1)| ) bb2(w1, . . . , w |in(bb2)| )" s(v) = 0 (Run f (l, s), cs, m) → (Run f (fst(bb2), s[in(bb2)i ← s(wi) | 1 ≤ i ≤ |in(bb2)|][loc(bb2)i ← ⊥ | 1 ≤ i ≤ |loc(bb2)|]), cs, m) (ifelse) op(l) = "return(v1, . . . , v O f )" (Run f (l, s), cs, m) → (End f (s(v1), . . . , s(v O f )), cs, m) (end)
op(l) = "(v1, . . . , vn) = call g(w1, . . . , w k )" (Run f (l, s), cs, m) → (Start g (s(w1), . . . , s(w k )), Run f (l, s)::cs, m) (call) op(l) = "(v1, . . . , vn) = call g(w1, . . . , w k )" (End g (x1, . . . , xn), Run f (l, s)::cs, m) Program execution Transition rules are provided in Fig. 3. An execution trace of an SSA specification is any sequence of transitions starting in an initial state. Note that if t = s 0 → s 1 → . . . → s n → . . . is a trace, then any prefix t n = s 0 → s 1 → . . . → s n is also a trace. We denote with ≤ the prefix order on traces, meaning we can write t n ≤ t.

→ (Run f (nxt(l), s[vi ← xi | 1 ≤ i ≤ n]), cs, m) (ret) op(l) = "w = load(addr)" s(addr) = ⊥ (Run f (l, s), cs, m) → (Run f (nxt(l), s[w ← m(s(addr))]), cs, m) (load) op(l) = "store(addr, v)" s(addr) = ⊥ (Run f (l, s), cs, m) → (Run f (nxt(l), s), cs, m[s(addr) ← s(v)]) (store)
Note that rules (ifthen) and (ifelse) define the behavior of a conditional branch only when the test variable is defined. When it is absent, execution cannot advance-it blocks. Execution also blocks when reaching a memory access rule with address ⊥. Otherwise, execution can advance. This requires defining the semantics [[op_id]] of all operations for ⊥ inputs. Note that maximal traces (in the sense of ≤) will either end in a final state, or when execution blocks, or never end.

Separation assumptions Our semantics separates, in both state expression and transition rules, the part corresponding to the SSA core from the extensions needed to represent function calls and memory. For instance, to consider only the core SSA semantics one simply has to remove call stack and memory terms from the specification state, and only consider the black rules of Fig. 3 (which do not access memory or call stack). Similarly, function call rules do not access the memory, and memory rules do not access the call stack.

Determinism and correctness

If we assume that all operations are deterministic (which in our formal framework amounts to assuming that [[op_id]] are partial functions) the sequentiality of the SSA execution implies its determinism: For each initial state s there exists a unique trace starting in s that is maximal in the sense of ≤.

Dominance

But determinism is not sufficient. Correctness also requires that execution never blocks. To ensure this, we will enforce a stronger property: that all variables are different from ⊥ whenever used in computations. Assume that variable v is assigned a value in basic block b, and that v is an input to operation o of basic block b . To ensure that v does not have value ⊥ when o is executed, one must ensure (as a necessary property) that any execution path reaching o passes through the definition of v. This happens if and only if one of the following conditions is true: While checking property D1 is straightforward, determining that D2 holds for any variable v and operation o using v is not tractable in the general case (Boolean satisfiability can be reduced to the decision of D2).

D1 b = b ,
For this reason, SSA-based compilation always ensures D2 by enforcing a sufficient property, named dominance, which can be checked using a low-complexity structural analysis of the SSA SCFG [START_REF] Cytron | Efficiently computing static single assignment form and the control dependence graph[END_REF]. Dominance is considered part of SSA form correctness, along with the syntactic correctness and the structural properties of Section 2.1.

Together, these structural properties ensure the correctness of SSA specifications that do not access memory. When memory is used, these properties must be complemented by a proof of the fact that each memory location is initialized before it is read.

From SSA to synchronous concurrency

In this section we extend the syntax and semantics of SSA with the operational mechanisms needed to represent synchronous concurrency. The extension leaves the (non-reactive) SSA semantics of Fig. 3 unchanged, and allows the application of all SSA code transformations. Thus, building on MLIR's extensible syntax and semantics, it is possible to model and generate code for reactive real-time applications without changing the existing code base (only introducing additional behaviors).

Cyclic execution

To represent the behavior of embedded systems, which interact with their environment in a continual and timely fashion, all synchronous languages have cyclic execution models. The execution of a synchronous program is an a priori infinite sequence of execution cycles. Execution cycles being non-overlapping, they form a logical time base: each operation happens in exactly one cycle which can be identified by its index. But synchronous logical time is not only a descriptive notion used during analysis. It is meant to allow the synchronization of cycle execution onto external time bases. For instance, periodic real-time execution is typically enforced by synchronizing cycle triggering (the logical time base) with a periodic HW timer. The SSA form also allows the representation of cyclic behaviors under the form of cyclic SCFGs, as exemplified in Fig. 2. However, what constitutes an execution cycle is not clearly identified, nor the mechanisms for synchronizing execution cycles with an external time base, nor how to constrain an operation to happen in a specific cycle. To allow SSA-based embedded real-time programming, we must allow the specification of all these aspects in a way that will be preserved by SSA-based code transformations and optimizations.

Tying the definition of execution cycles to the structural elements of SSA (the basic blocks) is tempting, but unfeasible, as basic blocks are not preserved by common optimizations. Another tempting approach is to extend the syntax and semantics of basic blocks and/or branching statements to explicitly identify some of them as execution cycle barriers. However, such an approach would require changes to much of existing SSA-related compiler code (such as dominance analysis or optimization algorithms), which we want to avoid.

The tick operation

The solution we chose is the introduction of a new operation tick to identify execution cycle barriers. To order operations with respect to these barriers, tick relies on two SSA mechanisms: dominance and memory access ordering.

Dominance-based ordering. The syntax of tick, provided in Fig. 4, shows that it can take as arguments any number of variables, which allows specifying that operations producing these variables are executed before the cycle barrier. It produces an optional variable %s of type none, which is the unit type of MLIR SSA. Like for the unit type of functional programming or the pure signals of synchronous programming [START_REF] Potop-Butucaru | Compiling Esterel[END_REF], a variable of type none represents pure synchronization. It carries no information but requires operations reading it to happen after the operation producing it. To facilitate the specification of such ordering constraints, we also introduce the sync operation which allows transferring the dependences of one or more variables onto another. The operation takes as input two or more variables. It copies the value of its first input onto its output as soon as all inputs have arrived.

1 func @periodic1()->() { 2 ^reset: 3 %x0 = call @init() :()->tensor<64xi8>
As Fig. 5(left) shows, this way of enforcing ordering is particularly useful early in the compilation process, when aggregate n-dimensional data are represented with abstract types (such as the tensors of MLIR) manipulated with side-effect-free operations.

Ordering by side-effects We also assume that tick has unspecified side-effects, which means it cannot commute (during SSA code transformations) with operations that read or write memory. This way of enforcing ordering is particularly useful later in the code generation process, once buffer allocation of aggregate data has been done. This is the case in Fig. 5(right), which could be an implementation of the program in Fig. 5(left). Note that in both cases SSA code transformations (e.g. loop unrolling) can be applied freely, without changing the ordering of computations w.r.t. execution cycle barriers.

Structural properties

To ensure that the execution of a reactive SSA function is an infinite sequence of execution cycles, we will require that it does not contain return operations, and that each potentially unbounded cycle of the SSA specification contains at least one tick operation.

Compilation

The transformation of a standard SSA form specification into executable sequential code is a well-understood process. However, the introduction of tick fundamentally changes the SSA semantics by requiring a cyclic interaction with the environment/scheduler.

The way this interaction is traditionally implemented in the compilation of synchronous languages [START_REF] Potop-Butucaru | Compiling Esterel[END_REF][START_REF] Biernacki | Clock-directed modular code generation for synchronous data-flow languages[END_REF][START_REF] Bergerand | Outline of a real time data flow language[END_REF] is illustrated in Fig. 6. The control flow of the source code (function @n in our case) is completely restructured in order to produce a semantically equivalent program with a single tick operation (function @n_drv). To do this, the control and data state of the original function between execution cycles must be explicitly represented. In our example, this state is transmitted by the arguments of ^step and consists of:

• A Boolean value (of type i1) to determine whether in the next cycle we need to start @f or @g.

• A value of type i32 allowing the transmission of the output of @f to @g.

At the beginning of each cycle the state is decoded, the needed computations are triggered, then a new state is encoded and transmitted to the next cycle. This process is usually represented with a separate step function, in our case @n_step. Classical synchronous language compilers will usually produce just this step function and the data structure describing the application state. When used in conjunction with the dataflow modularity described in Section 3.3, this approach allows modular code generation4 [START_REF] Biernacki | Clock-directed modular code generation for synchronous data-flow languages[END_REF]. However, the driver function (in our case @n_drv), and in particular the implementation of tick, are usually not generated, being considered too implementation-dependent. This compilation approach has been long tested in practice [START_REF] Benveniste | The synchronous languages 12 years later[END_REF][START_REF] Halbwachs | A synchronous language at work: the story of Lustre[END_REF], where it has shown its strengths (most notably modularity), but also its limits. The limits are mainly related to the one-size-fits-all generated code with a single step function and a state representation that must cover the needs of all execution cycle transitions. In our example, the state value of type i32 is computed and transmitted between every two successive cycles, even though it is semantically produced (output of @f) only in odd cycles. A good measure of the inefficiency of the resulting code is given by the significant amount of work on its optimization, and in particular on the optimization of its state representation [START_REF] Potop-Butucaru | Compiling Esterel[END_REF][START_REF] Gérard | A modular memory optimization for synchronous data-flow languages: application to arrays in a Lustre compiler[END_REF][START_REF] Didier | Correct-by-construction parallelization of hard real-time avionics applications on off-the-shelf predictable hardware[END_REF]. It is important to note that, once the generation of the step function performed, classical compiler optimizations are confined to the scope of the step function, and optimizations involving multiple execution cycles must be specifically designed for each particular language and state encoding.

func @n()->() { ^start: %x = call @f(): ()->(i32) tick() call @g(%x): (i32)->() tick() br ^start } 1 func @n_step(i1,i32)->(i1,i32){
Our compilation method cannot follow this example and systematically restructure control to obtain a loop with a single tick. Not only because of the potential efficiency loss, but because in many cases the implementation must have a different structure. For instance, in avionics MIF/MAF applications [START_REF] Didier | Correct-by-construction parallelization of hard real-time avionics applications on off-the-shelf predictable hardware[END_REF] the implementation must have a structure similar to that of Fig. 6(left), where a global periodic pattern (the global loop, named major frame, or MAF) is split by the tick operations into time intervals of equal length (the minor frames, or MIFs), each containing a different code.

To allow the implementation, without restructuring, of any reactive SSA graph satisfying the structural properties defined above, we propose a return to the fundamentals of reactive systems design, by making explicit the interaction with the system scheduler. In our compilation approach, a reactive SSA specification such as function @n of Fig. 6(left) is seen as a sequential process running under a cooperative multi-tasking scheduler. Each time the execution of @n reaches a tick operation, the execution context (state) of @n is saved and control is given back to the scheduler. When the scheduler determines that a new execution cycle must be triggered, it restores the state of the process and gives it back the control. When this happens, execution of the tick operation terminates, and control is given in sequence. This operational mechanism, whose formal semantics is defined in Section 3.5, can be easily implemented on various execution platforms ranging from low-level timers on bare metal platforms [START_REF] Didier | Correct-by-construction parallelization of hard real-time avionics applications on off-the-shelf predictable hardware[END_REF] to POSIX system services such as longjmp (as we do in Section 4.2) and to RTOS services such as PERIODIC_WAIT in the avionics-oriented IMA/ARINC 653 standard [START_REF]Avionics application software standard interface. part 1 -required services[END_REF]. Most important, SSA code transformations and optimizations can be applied at their full strength while generating the executable code of the sequential processes.

Note that our proposal does not exclude the classical approach of compiling synchronous languages. Instead, it is complementary, allowing the modeling of implementation aspects that were previously not covered by code generation, and by allowing more expressiveness in the implementation.

Cyclic I/O

An embedded system will continually interact with its environment, cyclically reading inputs and writing outputs. In implementations, this is typically done by reading and writing memorymapped registers that can be represented with volatile C variables, or by calling dedicated I/O functions. Synchronous languages abstract away such implementation-dependent mechanisms under the form of input and output variables that can be read or written at each cycle, with two constraints related to the synchronous model:

• An output variable can be written at most once per execution cycle.

• All reads of an input variable during an execution cycle must return the same result.

For instance, in Fig. 2, the input inc of the Lustre program is read at each execution cycle.

By comparison, when not considering memory side effects, MLIR functions interact with their environment only twice:

• At the beginning of their execution, to read the value of their input arguments, which then remains constant during the execution of the function.

• When reaching a return operation, when the function completes.

These assumptions enable common SSA optimizations such as loop-invariant code motion. Volatile accesses to memory locations can sometimes be represented, like in the low level dialects of MLIR (LLVM, SPIRV), but they represent a particular low-level implementation, excluding others. The solution we chose to represent cyclic I/O is based on the representation of input and output channels with function arguments of the special types in(t) and out(t), where t is the type of data transmitted by the channel. Access to channel variables is done exclusively using the input and output operations, whose syntax is provided in Fig. 4. Operation input has a single argument of input channel type. Each time it is executed, input samples the channel for a value of the correct type, which is placed in the output variable. An output operation has two inputs: one output channel and a second variable (of the corresponding non-channel type) whose value will be written to the output.

To specify ordering relations between I/O operations and other operations, we use the same mechanisms discussed for tick in Section 3.1.1. On both input and output we assume unspecified side-effects, which prevents reordering with other operations that access memory and function calls. Both I/O operations also allow dominance-based ordering. For this reason, output has an (optional) output of type none.

Structural properties

It is required that only functions representing reactive behaviors use channel variables or the operations input and output. It is also required that reactive functions have only arguments of I/O channel type, and that no channel variable is output of an operation. It is also required that at most one input or output operation is performed on a given I/O variable between two instances of tick. This semantic property is usually enforced by requiring the respect of structural properties, e.g. by requiring that every SCFG path between two operations on the same channel contains a tick operation.

Compilation As explained above, various low-level mechanisms can be used to implement the operations input and output, the most typical being volatile variables and calls to I/O functions. For portability, our compiler takes the second approach, by: • Transforming each function argument of type in(t) into a function argument of type ()->(t), i.e. a reference to a function that takes no argument and produces one result of type t.

• Transforming each function argument of type out(t) into a function argument of type (t)->().

• Each input and output operation is transformed into a call to the corresponding function argument. Note the use of call_indirect, a version of operation call allowing calling a function transmitted by reference.

Fig. 7 provides a small example: a reactive program with one input channel and one output channel that copies at each cycle its input on the output. When the value produced by input or taken as input by output is an object stored in memory,5 much care must be exerted to avoid memory errors (accessing unallocated memory and memory leaks). In our implementation, we will assume that all memory-stored objects produced by an input operation are allocated and deallocated by the environment, with a lifetime finishing at the end of the current execution cycle. We also assume that memory-stored objects given as argument to an output operation are allocated and deallocated by the function, and that the environment no longer uses them when the next execution cycle begins.

Modularity

The modularity of SSA is that of sequential procedural programming. The modules of an SSA specification are the functions, which interact through function calls.

By comparison, the formal models underpinning synchronous languages are concurrent. In the most general settings, such as Esterel's constructive semantics [START_REF] Potop-Butucaru | Compiling Esterel[END_REF], the execution of two submodules of a specification can advance concurrently, synchronizing and communicating with each other in both senses. Determining that the execution of such a specification does not block (a process known as causality analysis) is in general undecidable, if integer data are allowed, and NPhard (untractable in practice) if the input language uses only Boolean variables. Furthermore, the implementation of such general specifications can be very inefficient due to intricate semantic rules.

For this reason, synchronous language compilers have early on imposed simple structural constraints allowing fast and modular compilation: In each module, the computations of an execution cycle must form an acyclic dependency graph, allowing fast scheduling and code generation. In this acyclic graph, to allow the separate compilation of a sub-module, its computations must be grouped together as a single graph node, meaning that they can be performed atomically.

To allow the representation of this mechanism in our SSA extension, we introduce the notion of instance of a reactive function @f, which is a process (with separate state) executing function %f under the system scheduler. Instances are uniquely identified (with lists of strings, in our implementation). We assume that the first reactive function of a specification has an instance identified with the empty list of strings [] that receives control when the system starts. All other instances are inductively defined and possibly given control during execution using the operation inst (syntax in Fig. 4): if i is an instance of function @f which contains operation "inst @g str", then instance str::i of function @g is automatically defined.

We provide in Fig. 8 an example of submodule instantiation. The system has two reactive functions and two instances: the implicit [] instance of function @main and one instance ["a"] of function @sum. Instance [] reads its unique input from the environment on odd cycles, triggers one tick of instance ["a"] in every cycle (giving it as input the value of %i) and outputs the last output of ["a"] in even cycles. Instance ["a"] of @sum has a state in which it accumulates the sum of inputs it receives on odd cycles. On even cycles, it computes and outputs variable %o.

Structural constraints

The number and types of input and output variables of an inst operation must match the signature of the reactive function it instantiates.

Compilation The compilation method based on conversion to step functions will implement sub-module instantiation using function calls [START_REF] Biernacki | Clock-directed modular code generation for synchronous data-flow languages[END_REF]. When conversion to a step function is not desired, we transform each instance into a process running under a cooperative scheduler. This mechanism extends that of Section 3.1.2 by clarifying how the scheduler passes the control between instances. When reaching an inst operation, the inputs and the control are transmitted to the instance, which then executes until reaching a tick operation, at which point it saves its state and returns the outputs to the caller, according to the rules of Section 3.5.

Signal absence

Consider the simple example in Fig. 6(left) and its implementation on the right. Note that the translation slightly changes the semantics of the program: On the left, the variable %x is transmitted only from odd cycles to even cycles. But in the translation result %x has been added to the program state, which is computed and transmitted at every cycle. Thus, in the ^false: basic block of @n_step, under SSA semantics, we need to return a value for %x, even if the source program does not require it.

In this case, the choice is natural: we maintain the previous value, which may later allow an encoding of the state in (persistent) memory. But using a constant of type i32 or a random value instead would have been correct, as this value will never be used.

But the choice is less obvious in other cases, such as for communication variables. In Fig. 8, function @sum outputs values only on even cycles, meaning that the value of %x1 in function @main is never correctly initialized (yet, the specification is overall deterministic, because this absent/undefined value is never used in computations).

Such situations are common in the synchronous modeling of multi-periodic systems, which explains why absence prominently figures in the semantics of all synchronous languages [START_REF] Benveniste | The synchronous languages 12 years later[END_REF]. To allow its explicit representation in SSA without breaking the structural correctness rules of SSA, we introduce operation undef (syntax in Fig. 4) which explicitly leaves its output variable absent/undefined. We could use it, for instance, in Fig. 6, function @n_step, basic block ^false, in order to leave the second return argument uninitialized.

For scalar values, undef is compiled into the llvm.undef value of LLVM IR [START_REF] Lee | Taming undefined behavior in llvm[END_REF]. For aggregate data allocated to memory, it translates into a lack of initialization after allocation.

Operation undef has not one, but two semantic interpretations, both covered by the rule of Fig. 9:

Absence In this case, α = ⊥, the semantic value introduced in Section 2.3.

Undefinedness In this case, α = * , where * is interpreted as a random integer value.

Both interpretations are fundamental. The second one is that of the implementation (and of LLVM IR), where the hardware locations always store values of type Int (even if we do not know which ones). In this interpretation, the execution of an SSA specification will always start with a random, yet fully defined, memory state, and SSA correctness ensures that, under semantic execution, no ⊥ value is ever used in computations or stored to memory.

op(l) = "v = undef" (Run f (l, s), cs, m) → (Run f (nxt(l), s[v ← α]), cs, m) (undef-α) Figure 9: Semantics of ⊥
The first interpretation is that of the abstract interpretation meant to determine whether uninitialized values are used in computations. In this interpretation, the execution of an SSA specification will start with ⊥ memory state. The execution of undef operations, access to uninitialized memory locations, or use of ⊥ function arguments will set to ⊥ variables that can afterwards be used in computations.

The two interpretations are related by a strong abstraction result. To define it, we organize Int as a Scott domain under the partial order defined by ⊥ ≤ x for all x ∈ Int. This partial order is extended pointwise on the variable states of an SSA function and on memory states. It is also naturally extended to function states by

Start f (v 1 , . . . , v k ) ≤ Start f (w 1 , . . . , w k ) and End f (v 1 , . . . , v k ) ≤ End f (w 1 , . . . , w k ) if v i ≤ w i for all i, and Run f (l, s) ≤ Run f (l, s ) if s ≤ s . It is also extended to call stacks by [s 1 , . . . , s k ] ≤ [s 1 , . . . , s k ] if s i ≤ s i for all i.
With these definitions, we can extend pointwise the partial order ≤ to execution states of an SSA specification.

Theorem Consider a non-reactive SSA specification. 6 Assume that all operation identifiers have monotonous semantics [[op_id]] : Int → Int. Let s a 0 → . . . → s a n be an execution trace under the abstract semantics of undef, and s c 0 → . . . → s c m an execution trace under its low-level semantics such that s a 0 ≤ s c 0 . Then: 1) if m < n, the low-level trace can be continued to a trace of length n, and 2)

s a i ≤ s c i for all 1 ≤ i ≤ min(m, n).
Proof sketch Each of the semantic rules of Figures 3 and9 is monotonous in the sense of the Scott domain partial order on specification states. Then, each execution step will preserve the abstraction relation s a i ≤ s c i between abstract and low-level (concrete) states.

A corollary of this theorem is that guarantees obtained through analyses under the abstract semantics7 remain valid under low-level (implementation) semantics.

Formal semantics of reactive extensions

The final step of our SSA extension is the definition of the formal semantics of reactive SSA specifications formed of one or more instances of reactive SSA functions. Given a reactive function f, we denote with in f , respectively out f the ordered set of input channel variables of f. Given an instance i, we denote with r(i) its reactive function.

The execution state of a reactive SSA specification is represented with triples < i, I, m >, where m is the shared memory state, i is the currently active instance identifier, and I is a map associating to each instance identifier the instance state. The state of instance i is I(i) = (s, cs, si, so), where s is the state of the function f that is currently executing, cs is the call context, si : in r(i) → Int is the state of the input channels of i, and si : out r(i) → Int is the state of the output channels.

Under these notations, the operational semantic rules are provided in Fig. 10. The (local) rule transforms non-reactive SSA transitions of the instances (denoted with → and defined in Figures 3 and9) into transitions (denoted with ⇒) of the reactive system. All other rules involve reactive operations (interaction with the scheduler). Rules (in) and (out) deal with instance I/O. Rule (s-tick-α) is the only one that interacts with the environment by performing I/O and possibly time synchronization. Note that, like the (undef-α) rule of Fig. 9, it has two interpretations (α = ⊥ or α = * ). The rules (inst-α) and (tick) (in red) implement modularity.

Evaluation

In the previous section, our objective was to extend the SSA form with synchronous reactive features in the most general way that remains fully compatible with traditional SSA semantics and algorithmics (thus allowing implementation without changes to the existing codebase).

In this section, we evaluate the ability of this extension to support the specification and compilation of realistic applications with both reactive and HPC aspects. The reactive aspects of such applications must be specified in a high-level synchronous dialect, not directly in our lowlevel SSA extension. We show that the dataflow core of the Lustre synchronous language8 can be embedded as a new dialect, named lus, into the SSA-based MLIR compilation framework [START_REF]Multi-level intermediate representation compiler framework (MLIR)[END_REF]. This allows the specification (in MLIR) of applications where the reactive aspects are modeled at the Lustre abstraction level, while data processing is modeled at the abstraction level of other dialects such as affine (affine loops), linalg (linear algebra), or tf (TensorFlow graphs).

During compilation, reactive statements of the lus dialect are lowered9 into a mix of structured control flow (MLIR dialect scf) and the reactive SSA constructs introduced in Section 3 and grouped in a new dialect named sync. Operations of the sync dialect are later converted into low-level SSA (dialects std and llvm) and calls to external OS primitives following the compilation rules defined in Section 3.

The structured control flow, along with the data types and data processing code, are progressively lowered using the existing transformations of MLIR, which do not affect reactive semantics. Among others, these transformations allow buffer synthesis, i.e. the transformation of the abstract aggregate data used with lus-level synchronous specification (e.g. tensors) into memory objects along with allocation and deallocation operations, in a way that ensures the absence of both memory leaks and accesses to unallocated memory.

The result is a fully functional specification and compilation framework for reactive high-performance applications, which we evaluated on a non-trivial signal processing (vocoder) application.

Embedding Lustre in MLIR

The synchronous language that has reached the most widespread use is Lustre [START_REF] Halbwachs | A synchronous language at work: the story of Lustre[END_REF][START_REF] Bergerand | Outline of a real time data flow language[END_REF]. For space reasons, we only consider here its pure dataflow core-the SN-Lustre dialect of [START_REF] Bourke | A formally verified compiler for lustre[END_REF]-into which full Lustre can be translated.

A Lustre program, like that of Fig. 2(top), is called a node. It specifies a dataflow graph of statements connected through dataflow variables. Each variable is either an input of the node, or it is output of exactly one statement (single assignment property). Lustre follows a pure dataflow paradigm, with no use of load/store memory (no side-effects).

The semantics of Lustre is (intuitively) best described as a mix of dataflow operational and declarative aspects.

Operational interpretation As synchronous programs, Lustre nodes have a cyclic execution model. At each execution cycle, the list of statements of a node is traversed once, in an order compatible with the dependences determined by the variables. When traversed, a statement will read the value of its input variables, possibly perform some internal computations, and assign a value to its output variables. As the semantics of a node is not affected by the syntactic order of its statements, we can always assume (as a normal form assumption) that the statements already are in traversal order, as in Fig. 2(top). Dependences are defined as follows: Variable y being produced by statement p and used in statement c determines a dependency p → c in all cases except one: when c is a statement of the form "x = k fby y". In this case, p → c, as a form of anti-dependency ensuring that the value is read before being overwritten. This special handling of fby allows it to read the value assigned to its input variable in the previous execution cycle. This value is then assigned to the output of fby, allowing its use in the current cycle. In Lustre, this is the only mechanism allowing the specification of a state passed between execution cycles.

The value assigned to a variable in a cycle can be the special value ⊥ introduced in Section 2.3 to represent absence. Making a variable absent inside an execution cycle is done using the subsampling statement when. When statement "x = y when c" is traversed and the Boolean c has value true, x is assigned the value of y. If c is false or ⊥, x is assigned value ⊥. Absence is the dataflow mechanism of specifying conditional execution: A function call with ⊥ input variables will not execute its function, but instead assign all outputs to ⊥. This mechanism, specific to the dataflow programming paradigm, is used in lines 9 and 10 of Fig. 2 to specify that function actuate is executed only in cycles where variable ck is true. The counterpart of when is statement "x = merge c y z". Upon traversal, if c is true (resp. false), x takes the value of y (resp. z). Otherwise, x takes the value ⊥.

Declarative aspects (clock constraints) The purely operational interpretation defined above matches the standard Lustre semantics [START_REF] Bergerand | Outline of a real time data flow language[END_REF][START_REF] Biernacki | Clock-directed modular code generation for synchronous data-flow languages[END_REF][START_REF] Bourke | A formally verified compiler for lustre[END_REF] on correct Lustre programs where all fby statements are executed at every cycle.

However, Lustre allows a form of logical time modularity during specification, by allowing subsets of statements (including fby statements) to be executed under specific Boolean conditions. This is the case in the node of Fig. 11(left), which incrementally computes the sum of its positive input values. The statements in lines 7 and 8, which implement the computation of the sum, are executed only in cycles where ck is true. However, no operational mechanism constrains the execution of the fby statement.

Instead, each Lustre statement defines a clock constraint-a predicate relating the present/absent status of its input and output variables (and possibly their value) inside an execution cycle. In our example, two such clock constraints apply:

• Inputs and outputs of a function call or fby are either all ⊥, or all have a value different from ⊥.

• The inputs of a when are either both present, or both absent. Output is present iff the condition is true.

Determining the execution condition of each statement consists in solving the system of con- The lus dialect We have embedded the Lustre language constructs into MLIR. The lus representation of the Lustre node in Fig. 11(right) is provided in Fig. 12(left), with the lus keywords highlighted in blue. The MLIR definition of nodes is derived from that of SSA functions by replacing keyword func with node and requiring the compiler to check that a single basic block is present, terminated with operation lus.yield (which identifies the output variables).

While MLIR is SSA-based and its transformations mostly require the respect of dominance, it also allows specification under the weaker single assignment property, thus allowing the representation of cyclic dataflow graphs like the one in Fig. 12(left).

At the level of lus, we have implemented the clock inference algorithm. Along with data type correctness, single assignment, and causal correctness, the success of clock inference guarantees the correctness of a Lustre program. As the first two properties are automatically checked by the existing MLIR infrastructure, only causal correctness remains to be checked.

Normalization Once clock inference performed, we can transform the original program so that the operational interpretation correctly simulates it. This transformation, exemplified in Fig. 11, consists in ensuring that all fby statements are executed at every cycle (through the introduction of when and merge statements, in red in Fig. 11). We have implemented this normalization step in MLIR.

Lowering of lus to sync Once normalization performed, all fby operations can be collectively replaced with the continuation passing encoding of state specific to MLIR SSA. In Fig. 12(right) this is done using the basic branching mechanism of SSA, but the lowering phase we implemented in MLIR produces structured control flow operations (for). Once the state reencoding performed, determining the causal correctness of the program amounts to an SSA dominance check, performed automatically by MLIR.

The remaining lowering steps are the transformation of I/O variables of the lus node into I/O channels and explicit input and output operations, and the synthesis of imperative coditional control to ensure that each operation is only executed in cycles prescribed by clock inference. In 10 Which will fail for incorrect programs. Inria Fig. 12(right) this imperative control is implemented using core SSA branching statements, but our MLIR implementation uses structured control flow operations.

This completes the definition of our compilation method. Note that, in the implementation of our compiler, stock MLIR algorithms are used for all data type specification and implementation, causality analysis, and memory allocation. We have only had to implement analysis and lowering steps specific to the synchronous model of computation.

The pitch tuning vocoder use case

We illustrate the expressiveness our proposal and evaluate its effectiveness on a complex realtime sound processing application-a voice pitch tuning vocoder. The application is naturally modeled under a synchronous paradigm. It must cyclically sample the sound input and the other control inputs, update the control state, perform one step of the pitch tuning algorithm, and (if required by the current control status) drive the sound output.

The application has a complex data processing pipeline, involving Hann filering to reduce spectral leakage, move to frequency domain using the Fast Fourier transform (FFT), move to polar coordinates to separate magnitude from phase, the additive phase synthesis algorithm that performs the actual pitch change, move back to Cartesian coordinates and then to the time domain using the inverse FFT, and a final step of Hann filtering and additive accumulation. All these aspects are specified using the abstract aggregate types of MLIR (tensors) and operations of the linalg, scf, and std dialects.

The control of this pipeline is also complex. It involves multiple sliding windows and multiple feedback loops. In addition to the pipeline control, the application also features control related with the user interface, silencing the output (which involves shutting down unneeded pipeline steps) and altering the pitch correction. All of these are intuitively specified using the lus dialect.

Our compilation flow automatically performs buffer allocation and synthesizes low-level control ensuring the correctness and safety of the implementation. Various optimizations can be applied in the process, including loop fusion.

Related work

We advance the state-of-the-art in SSA by providing the syntactic constructs, structural rules, and semantics extensions allowing the representation of synchronous reactive behavior. This overall objective is fully original.

However, particular aspects of our extension have been covered in previous work, in particular predicated execution [START_REF] Carter | Predicated static single assignment[END_REF][START_REF] Ottenstein | The program dependence web: A representation supporting control-, data-, and demand-driven interpretation of imperative languages[END_REF] and the use of semantic absence/undefinedness [START_REF] Lee | Taming undefined behavior in llvm[END_REF][START_REF] Demange | Semantic reasoning about the sea of nodes[END_REF]. In previous SSA work, predicated execution is explicit: the predicates are represented at all points where they exert control. We allow an implicit predication specification, akin to dataflow semantics, where the absence of inputs determines absence of execution. This requires a clear definition of correctness, which is absent in [START_REF] Carter | Predicated static single assignment[END_REF].

Our treatment of semantic absence/undefinedness is also different from that proposed for LLVM [START_REF] Lee | Taming undefined behavior in llvm[END_REF]. Our objective is not to ensure that non-deterministic code (involving undefined values) preserves its set of traces unchanged under various optimizations. Instead, it is to guarantee that well-defined values are preserved by various optimizations, even in the presence of undefined behaviors affecting other variables. We attain this goal through the abstraction theorem of Section 3.4.

We also extend previous work on the compilation of synchronous languages [START_REF] Potop-Butucaru | Compiling Esterel[END_REF][START_REF] Biernacki | Clock-directed modular code generation for synchronous data-flow languages[END_REF][START_REF] Benveniste | The synchronous languages 12 years later[END_REF]. Existing synchronous language compilers profoundly restructure the code in order to match an execution model (which, as explained in Section 3.1.2, is in most cases sequential function calls, even though multi-threaded implementations have also been proposed [START_REF] Li | Multithreaded reactive programming-the kiel esterel processor[END_REF]). We fully avoid this by ensuring that every reactive SSA specification can be executed as is, and be subject to any correct SSA transformation. Synchronous-specific code transformations are still possible, but not mandatory.

More important maybe, instead of advancing the compilation of synchronous languages as a separate research field, we show that it can be seen as an extension of classical compilation, allowing the reuse of fundamental techniques for type checking, causality analysis, buffer allocation etc.

Conclusion

We presented an embedding of the Lustre synchronous reactive language into SSA, extending the MLIR framework to allow synchronous programming and code generation. We illustrated it by capturing the data processing, computational and reactive control aspects of a signal processing application. Our MLIR extension remains fully compatible with SSA-based analysis and transformations, while also capturing the synchronous composition of concurrent state machines, logical and physical time synchronization, and compilation passes specific to synchronous languages, such as clock calculus, causality analysis, bounded-memory and clock-directed code generation.

While there had long been connections between the semantics of functional languages, SSA and dataflow synchronous languages, this paper describes the concrete extension of SSA capturing the necessary elements for reactive control system. Furthermore, retaining all SSA-based compilation algorithms and reusing existing code unaware of the the specific synchronous concurrency semantics allows a tighter integration of reactive system modeling frameworks with the computationally intensive and general-purpose capabilities of MLIR-and LLVM-based frameworks for HPC and AI.

Since synchronous concurrency is highly popular in safety-critical environments, one important future direction is to fully formalize the core MLIR components our extension relies upon, and to prove its correctness. A related direction consists in exploring syntax and refinements for state-machines and control automata expressed in the Esterel synchronous language as well as hardware design languages such as Bluespec and Chisel. It is also important to further investigate which SSA-based algorithms can benefit the compilation flow of reactive control systems and how domain-specific methods for synchronous languages can enable greater automation and guarantees in the composition and memory management of concurrent systems in general.

  <ssa_spec> ::= <function> + <function> ::= func <fun_name> <fun_iface> <fun_body> <fun_iface> ::= (<type> * )->(<type> * ) <fun_body> ::= <block> + <block> ::= <blk _arg>:<blk _body> <blk _arg> ::= <block _name>(<tvar> * ) <tvar> ::= <var>:<type> <blk _body> ::= <op> * <term_op> <op> ::= (<var> * )=<op_id>(<tvar> * ):<type> * | <var> = load(<tvar>):<type> | store(<tvar>,<tvar>) <term_op> ::= cond_br <var> <blk _arg> <blk _arg> | br <blk _arg> | return(<tvar> * ) <op_id> ::= <arith_op> | <bool _op> | call <fun_name>

Figure 1 :

 1 Figure 1: SSA syntax

  L f and V f are respectively the sets of labels and of variables of an SSA function f, and b f 0 is its first basic block. The function containing basic block b is denoted fun(b). The ordered set of inputs of basic block b is in(b) ⊆ V fun(b) , and in(b) i is the i th input of b. The ordered set of variables assigned by operations of a block b is denoted loc(b). The label of the first operation in block b is fst(b). The operation associated with a label l ∈ L f is denoted op(l). If op(l) is not a terminator, then nxt(l) is the label of the next operation in its block. The number of arguments of a return operation of function f is denoted O f .

Figure 2 :

 2 Figure 2: Stepper motor driver in Lustre (top) and MLIR SSA (bottom). In green, control statements. In red, data processing operations. In violet, cyclic I/O and time synchronization. In blue, state manipulation.

Figure 3 :

 3 Figure 3: SSA semantics. Memory access rules in green. Function call rules in red. • A triple Run f (pc, val) formed of the label pc of the operation to execute next (the program counter) and a partial valuation val : V f → Int of all the variables. The execution state of an SSA specification is a triple (s, cs, m) formed of the state s of the function that is currently executing, a list cs of running states representing the call stack, and the current state m : Int → Int of the memory. An initial state of the specification has the form (Start f (. . .), [], m), where m is the initial memory state and f the function that serves as execution entry point. A final state of the specification has the form (End f (. . .), [], m).

  and the definition of v precedes o in b, either as block argument, or as output of an operation. D2 b = b , and any possible execution reaching b necessarily passes through b.

  Inria <type> += in(<type>) | out(<type>) <op> += (<var>?) = tick(<tvar> * ) | <var> = sync(<tvar> <tvar> + ) | <var> = input(<var>):<type> | (<var>?) = output(<var>:<var>):<type> | <var> = undef:<type> <op_id> += inst <fun_name> <inst_id>

Figure 4 :

 4 Figure 4: SSA syntax extensions for synchronous reactive programming. Grayed non-terminals are those of Fig. 1. "+=" extends an already-defined non-terminal.

11 }Figure 5 :

 115 Figure 5: Synchronizing computations w.r.t. execution cycle barriers (tick) to enforce periodic execution. Dominance-based (left) vs. side-effect-based (right).

2Figure 6 :

 6 Figure 6: Synchronous languages approach to code generation. Source code on the left, output on the right.

Inria

1 9 }Figure 7 :

 97 Figure 7: Code generation for I/O operations

Inria

1 13 }Figure 8 :

 138 Figure 8: Submodule instantiation example

1

  node s(i:int)returns(s:int) 2 var ck:bool;i1,s1:int;

9 10 tel 1 Figure 11 :

 910111 Figure 11: Time modularity (left) and its normalization

6Figure 12 :

 12 Figure 12: Lowering lus to sync in MLIR

Ranging from ML dataflow graphs and linear algebra specifications down to affine loop nests and optimized (tiled, vectorized. . . ) low-level code.

A vocal pitch tuning vocoder.RR n°9380

Which under classical notation amounts to the variable being output of exactly one φ operator.Inria

RR n°9380

One step function per hierarchic synchronous module, the state representation of a module including that of sub-modules it hierarchically includes, and its step function calling the step functions of sub-modules.Inria

Like the variables of type memref in MLIR.RR n°9380

Pompougnac & Beaugnon & Cohen & Potop-Butucaru

That may use undef, but not tick, cyclic I/O, or synchronous modularity.

That a program does not block or that a given variable or memory location has a specific (defined) value at a specific point during execution.RR n°9380

Chosen for its practical importance, as well as for its simplicity.

I.e. transformed into code at a lower abstraction level.Inria

route des Lucioles -BP 93 06902 Sophia Antipolis Cedex Publisher Inria Domaine de Voluceau -Rocquencourt BP 105 -78153 Le Chesnay Cedex inria.fr ISSN 0249-6399

Pompougnac (project-team KAIROS), Ulysse Beaugnon (Google), Albert Cohen (Google

I(i) = (s, cs, si, so) (s, cs, m) → (s , cs , m ) < i, I, m >⇒< i, I[i ← (s , cs , si, so)], m > (local)

I(i :: i) = (Run g (l , s ), cs , si , so ) op(l ) = "tick" I(i) = (Run f (l, s), cs, si, so) op(l) = "(v1, . . . , vn) = inst nd i (w1, . . . , wm)"


Geoffrey Saunois

Frédérique Robin

Emmanuelle Anceaume
email: emmanuelle.anceaume@irisa.fr

Bruno Sericola
email: bruno.sericola@inria.fr

Permissionless Consensus based on Proof-of-Eligibility

Keywords: consensus algorithm, proof of eligibility, aggregation, asynchronous and permissionless environment, adaptive adversary

We propose a consensus algorithm whose objective is to decide on the same union of proposed values, such that with high probability all the values proposed by the honest nodes belong to the decision. Our algorithm has been designed to cope with an asynchronous and permissionless system. By relying on a proof-of-eligibility, our algorithm is tolerant to an adversary capable of instantaneously corrupting entities. A straightforward application of our algorithm is the design of permissionless distributed ledgers.

I. INTRODUCTION

Permissionless blockchains aim at achieving the impressive result of being a persistent, distributed, consistent and continuously growing log of transactions, publicly auditable and writable by anyone. Despite the openness of the environment and thus the inescapable presence of malicious behaviors, security and consistency of permissionless blockchains do not demand the presence of a trusted third party [START_REF] Nakamoto | Bitcoin: A peer-to-peer electronic cash system[END_REF]. In the seminal blockchains, i.e., Bitcoin and Ethereum, this achievement results from the tight combination of two ingredients: a randomized election of the next block of transactions to be appended to the blockchain and a short latency broadcast primitive. While the latter one relies on the properties of peerto-peer networks, the former one has so far been commonly implemented by solving proof-of-work (PoW). A PoW is a cryptographic puzzle that is provably secure against a large proportion of participants that may wish to disrupt the system, and allows to keep the rate at which blocks are created parametrizable and independent of the size of the system. Unfortunately, resilience of PoW-based solutions fundamentally relies on the massive use of computational resources, which is a real issue today. Numerous investigations have been devoted to find a secure alternative to PoW, but most of them either rely on the intensive use of a large quantity of physical resources (e.g. proof-of-space [START_REF] Ateniese | Proofs of Space: When Space Is of the Essence[END_REF], proof-of-space/time [START_REF] Moran | Proofs of space-time and rational proofs of storage[END_REF]) or make compromises in their trust assumptions (e.g. proofof-elapsed-time [START_REF]Hyperledger Sawtooth description[END_REF], delegated proof-of-stake [START_REF][END_REF]). In contrast, solutions based on proof-of-stake (PoS) seem to be a quite promising way to build secure and permissionless blockchains. Indeed, proof-of-stake relies on a limited but abstract resource, the crypto-currency, in such a way that the probability for a participant to create the next block of the blockchain is generally proportional to the fraction of currency owned by this participant. It is an elegant alternative in the sense that all the information needed to verify the legitimacy of a stakeholder to create a block (i.e., crypto-currency possession) is already stored in the blockchain. Finally, by being a sustainable alternative (creating a block requires a few number of operations), scalability concerns, exhibited by PoW-based solutions, should be a priori more tractable. However, an important condition for PoS-based blockchains to be secure is randomness: the creator(s) of the next block must be truly random, and the source of randomness must not be biaised by any adversarial strategy. So far, this has been addressed by two main approaches: chain-based consensus and blockwise Byzantine agreement. In the former approach (e.g. [START_REF] Bernardo | Ouroboros praos: An adaptively-secure, semi-synchronous proof-ofstake blockchain[END_REF]), a snapshot of current users' status is periodically taken, from which the next sequence of leaders is computed. In the latter one (e.g. [START_REF] Durand | Stakecube: Combining sharding and proof-of-stake to build fork-free secure permissionless distributed ledgers[END_REF], [START_REF] Gilad | Algorand: Scaling byzantine agreements for cryptocurrencies[END_REF]), a Byzantine agreement per block, relying on the properties of verifiable random cryptographic schemes, is achieved. While [START_REF] Durand | Stakecube: Combining sharding and proof-of-stake to build fork-free secure permissionless distributed ledgers[END_REF] is tolerant to a weakly adaptive adversary (i.e., a targeted attack needs a given amount of time before being effective), node corruptions in [START_REF] Gilad | Algorand: Scaling byzantine agreements for cryptocurrencies[END_REF] are effective once decided by the adversary. Algorand [START_REF] Gilad | Algorand: Scaling byzantine agreements for cryptocurrencies[END_REF] handles such a strong adaptive adversary by implementing proof-of-stake with a proof-of-eligibility. Proof-of-eligibility allows us to decide who is in charge of executing an action. When the eligibility is found out by each one individually, it is called a cryptographic sortition scheme [START_REF] Gilad | Algorand: Scaling byzantine agreements for cryptocurrencies[END_REF]. Note that in contrast to cryptographic sortition, proof-of-work cannot be attributed to a single user which explains the development of mining pools. In Algorand, participation to the agreement protocol is ephemeral and depends on the amount of stake owned on user account. However, by relying on account balance, Algorand may not defend against an adversary that will observe, during the very first rounds of the consensus protocol, the IP address of users with significant savings account balance and launch a targeted attack on these users. Since these users have a higher probability to be involved in the subsequent rounds of the protocol than those with low savings, by preventing these wealthy users from participating to these rounds, the adversary may strongly jeopardize rounds progress, and consequently prevent termination of the Byzantine tolerant agreement protocol from holding.

The objective of this work is to go a step further by deeply relying on ephemeral but provable user identities. These identities allow any user to act under multiple identities without depending upon a trusted third party. We use the so-called unspent transaction outputs (UTXOs) to implement such identities. An UTXO can be roughly seen as a singleuse account in the sense that once credited, an UTXO can be debited only once. An UTXO is uniquely characterized by a key pair (pk, sk) and its associated amount of stake. Each public key is related to the digital signature schema with the uniqueness property, which allows stakeholders to use the public keys (or a hash thereof) of their UTXOs as a reference to them, as demonstrated in the "Public Keys as Identities principle" of Chaum [START_REF] Chaum | Untraceable electronic mail, return addresses, and digital pseudonyms[END_REF]. Any two UTXOs created by the same user are unlinkable. Hence user u is publicly known as pk u if u owns the UTXO whose key pair is (pk u , sk u ). An UTXO is created when it appears for the first time in the output set of a transaction, and once it is referenced in the input set of another transaction, it cannot be used anymore. Hence, by using UTXOs as user identities, a user owns as many verifiable identities as he wants, and can easily spread all its coins over multiple and unlinkable UTXOs. Since UTXOs are ephemeral, the number of users continuously varies with the activity of the system. Hence the rationale of using UTXOs in the proofof-eligibility is to prevent the adversary from presuming on user wealthiness, and thus makes the above described targeted attack inefficient. This allows us to design a Byzantine tolerant consensus algorithm, which in presence of a rushing adversary, guarantees that all correct users of the permissionless system decide on the same union of proposed values with any high probability 1 -ε, with ε ∈ (0, 1), in a bounded number of rounds. To fit the context of blockchains, users propose their set of pending transactions as their input values, and the decision value is a union of pending transactions. When all the users propose the same set of pending transactions then with high probability the algorithm decides in three rounds, otherwise the number of rounds is upper bounded.

The remaining of the paper is orchestrated as follows. Section II presents the model of the system in terms of synchrony, communication, security, and user transactions. Section III specifies the problem addressed by this paper. Section IV describes the main tenets of our consensus algorithm. Section V presents an in-depth analysis of our algorithm.

II. SYSTEM ASSUMPTIONS

a) Asynchronous and permissionless system: By permissionless we mean a distributed system in which (i) the number of participants for carrying out the protocol is not known before hand, is not even known during the course of the execution, and may change over time, (ii) the right to contribute and to participate is not controlled by a (trustworthy) third authority, i.e. we do not assume the presence of any public key infrastructure (PKI), and (iii) participants communicate over a weakly but reliable connected communication topology. We assume an asynchronous environment, that is our algorithm does not make any synchrony assumptions, i.e. does not assume any bounds on the time needed for a message to be received by its recipients, nor on the computation time of the processes, nor on the individual drifts of clocks. b) Cryptographic functions: Users have access to basic cryptographic functions, including a cryptographic hash function h of hash-value size h and an asymmetric signature scheme that allows a user to generate a public and secret key pairs (sk, pk), and compute a signature σ sk,h (d) of any message d. Function h is modeled as a random oracle. Our algorithm relies on verifiable random functions (VRFs). A Verifiable Random Function (VRF) [START_REF] Micali | Verifiable random functions[END_REF] is the public-key version of a keyed cryptographic hash. It is a pseudorandom function that provides a proof of its correct computation. Only the holder of the private key sk can compute the hash, but anyone with corresponding public key pk can verify the correctness of the hash. c) Public Keys as Identities principle [START_REF] Chaum | Untraceable electronic mail, return addresses, and digital pseudonyms[END_REF]: Users own some minimal amount of stake (i.e., money), which gives them the right to participate to the algorithm. As said in the introduction, we adopt a simplified version of what is commonly known as the Bitcoin Unspent Transaction Output (UTXO) model. In the following, when we say that UTXO (pk u , sk u ) is selected to perform some action we mean the user that owns this UTXO is selected to perform some action. Symmetrically, when we say that some user u executes some action we mean the owner of UTXO < pk u , sk u > executes some action. d) Threat model: An adaptive adversary: We assume the presence of Byzantine (i.e. malicious) users which controls up to p A < 1/3 of the total amount of stake currently available in the system. This model, named the "stake threshold adversary" by Abraham and Malkhi [START_REF] Abraham | The blockchain consensus layer and bft[END_REF], is an alternative to the common threshold adversary model. It bounds the total number of parties the adversary controls relative to the total population of the system. It is an extension (or modification) of the computational threshold adversary introduced by Bitcoin, which bounds the proportion of the computational power owned by parties. Byzantine users can deviate from the protocol. They are modeled by an adversary. The adversary can perfectly coordinates all malicious users. It can learn the messages sent by honest users (i.e. non malicious users), delay them, and then chooses messages sent by malicious ones. Further the adversary is adaptive: it can select at any time which users to corrupt in replacement of corrupted ones (i.e. corruptions are "moving"). The adversary is computationally bounded so that it can neither forge honest nodes' signatures nor break the hash function and the signature scheme. Finally, we assume that all users (honest and malicious) share an initial knowledge that we call genesis block which contains an initial arbitrary UTXO set. We assume this block also shares the same properties as regular blocks. How to setup the genesis block is out of the scope of this paper.

III. THE ADDRESSED PROBLEM: THE MERGED-CONSENSUS

While the overall goal of this work is to build a permissionless blockchain, in this paper we will concentrate on the design of the consensus algorithm whose objective is to decide on a union of valid transactions. We will prove that all the honest users of the asynchronous and permissionless system decide on the same union of transactions and that the decision is reached in a finite and bounded number of rounds with any high probability. We will also show that our algorithm is tolerant to a strongly adaptive adversary capable of instantaneously corrupting entities. Such an adversary is also called rushing adversary. Clearly, by sequentially invoking an instance of the consensus with a sequence number, this will allow the construction of a permissionless blockchain.

The task that honest users want to solve is the Merged-Consensus which is formalized by the following properties.

• Termination: Each honest user u eventually outputs one decision value dec u ; • Agreement: For any honest users u and v that respectively decide dec u and dec v , then dec u = dec v ; • Validity: Any decision value dec contains at least the set of transactions proposed by an honest user.

IV. MAIN PRINCIPLES OF OUR MERGED-CONSENSUS ALGORITHM

The algorithm we propose to implement the Merged-Consensus specification in a permissionless system consists of several asynchronous rounds. By adopting the nice idea of user replacement [START_REF] Gilad | Algorand: Scaling byzantine agreements for cryptocurrencies[END_REF], each asynchronous round r, r ≥ 0, is run by a dynamically created committee whose members are selected among all the users (i.e. UTXO owners) of the system at round r. As said in the introduction, selection is achieved in a random, unpredictable, and non-interactive way with a cryptographic sortition mechanism. Correctness of our cryptographic sortition is ensured by guaranteeing that no obvious Byzantine strategy such as a concentration of the stake on a single manipulated UTXO or a massive sub-division of stake on a multitude of compromised UTXOs (Sybil attack), can bias user random selection. Mitigating the impact of the former strategy is achieved by assuming an upper bound on the amount of stake credited on UTXOs. Note that this is not a constraint since each user may create an arbitrary large number of UTXOs and the number of transaction outputs is not upper bounded. To prevent an adaptive adversary from manipulating committee members during round r, r ≥ 0, the action of each committee member is limited to a unique step of computation followed by a unique step of communication. Hence, if the adversary eavesdrops a message from a committee member u, it is too late for him to manipulate u since u will not execute any more steps in round r, and possibly in any other rounds of the algorithm. Recall that users are "short-lived" (a user is alive as long as its UTXO has not been spent).

Rule 1. Any UTXO stake amount is bounded by constant U .

Cryptographic sortition exports two functions: the DRAW and VERIFYDRAW functions. Function DRAW is a private function which allows users (i) to determine by themselves whether they are selected as a committee member of a given round r of the consensus algorithm, and (ii) to provide later and if necessary a proof of soundness of this selection. The DRAW function when invoked by UTXO < sk u , pk u >, has five arguments: the secret key sk u of the UTXO, a seed seed from which comes the randomness of the sortition, the expected number of stake τ selected by the current sortition, the amount of stake w u credited on UTXO < sk u , pk u >, and the total current amount of currency units W owned by all the users of the system. Computation of the seed is based on the most recent pieces of information known by every user. In our case, this is the hash of the last created block, that is the hash of the decision value decided by the preceding instance of the Merged-Consensus. The knowledge of W is obtained by successively reading all the blocks of the blockchain. Function DRAW is made of two steps, first a call to a VRF function which calculates a random and verifiable number h u , and second a weighted random sampling seeded with h u . The weighted random sampling computes the voting weight vote u of UTXO < sk u , pk u > during round r according to the amount of stake credited on this UTXO. This voting weight is used by UTXO < sk u , pk u > during round r of the consensus algorithm. If vote u is equal to 0, user u cannot participate to the r-th round of the consensus algorithm. Otherwise, vote u gives u the right to belong to the committee of round r, and represents the weight of u's vote during round r. Specifically, let vote u be the random variable representing the voting weight of UTXO < sk u , pk u > as computed by function DRAW. Random variable vote u has a binomial distribution B(w u , p) where probability p is equal to τ /W . The probability that UTXO < sk u , pk u > is selected is thus 1 -(1 -τ W ) wu . These random variables being independent, whatever the sub-division w 1 + w 2 = w of w, the distribution of the weight associated with w is the same as the sum of the weight associated with w 1 and w 2 : B(w, p) = B(w 1 , p) + B(w 2 , p). This guarantees that an adversary has no advantage in launching a Sybil attack: an adversary can create as many accounts as he wants, what will influence the probability of winning is the total amount of stake, not the number of accounts.

Function VERIFYDRAW is a public function that allows each user to verify the legitimacy of UTXO < sk u , pk u > to get a voting weight vote. This function is similar to DRAW except that it is called with the public key pk u of the UTXO and proof π u .

Any honest1 user of the system invokes the Merged-Consensus algorithm (invocation of Propose() with the set of locally pending valid transactions2 ), but participation to round r, r ≥ 0, depends on the outcome of the Draw function.

The following parameters are public knowledge: the seed of the current instance of the consensus, the expected number of stake τ selected by the lottery, the total amount of stake W in the system, µ ∈ (0, 1), and λ ∈ (0, 1) whose values are analyzed in the full version of the paper. From above, in expectation, for each round r, τ stakes are randomly selected among the W stakes of the system.

The Merged-Consensus algorithm is made of a succession of rounds r = 0, 1, . . . During round r = 0, committee members (i.e., those that successfully passed the DRAW function for round r = 0) propose their sets of pending transactions T by broadcasting the message m u = ⊥, 0, (pk u , π u ), T u , ∅, vote u to all the users. In rounds r > 0, committee members collect and merge proposed transactions. Each round r > 0 is made of the following two steps: collect of broadcast messages, and construction of the final set of transactions, together with the proof that those sets of transactions have been initially broadcast in round r = 0. The collect of broadcast messages step consists for committee members of round r in collecting sufficiently many messages broadcast during round r -1. By sufficiently many, we mean that the total number of votes of the senders of these messages must be larger than µτ . Conditions on the value of µτ are provided in the full version of the paper. To guarantee the convergence on a unique set of transactions with high probability, we first need to guarantee that messages only contain transactions that have been initially sent in round r = 0, and second we need to prevent the adversary from withholding the transactions it sent during round r = 0, and then progressively make honest committee members discover them during subsequent rounds. The first case is guaranteed by providing in message m u a proof (data structure M u ) asserting that all collected transactions have been initially proposed by the committee members of the previous round, and thus by induction by those of round r = 0. The second case is handled in round r = 2 and is detailed below. The second step consists in building the final set of transactions. Once valid messages have been collected, any committee member u tries to build the final set of transactions. Specifically, if r = 1, then the preliminary final set of transactions T u contains the union of all the transactions received by u during the round and variable IsF inalCnt = 0. It may happen that all the committee members of round r = 0 broadcast the same set of transactions, in which case the final set of transactions will not evolve anymore (Boolean IsF inal is set to true). Set T u together with the set of collected messages M u (which acts as a proof for T u ) is broadcast to all the users (Recall that by the proof-of-eligibility property, users determine by themselves whether they are selected as a committee member of a given round r which explains why any message must be broadcast to all users to be received by the intended recipients). Round r = 2 is particular and its objective is twofold: achieving faster convergence to the final set of transactions and preventing the adversary from withholding the transactions it sent during round r = 0, and then progressively making honest committee members discover them during subsequent rounds. This is achieved by keeping in the final set of transactions T u only transactions that have received sufficiently many votes (i.e. λµτ ). Parameter λ ∈ (0, 1) can be seen as a broadcast factor, whose value is analyzed in the full version of the paper. As for round r = 1, set T u together with the set of collected messages M u (which acts as a proof for T u ) is broadcast to all the users for the next round of the algorithm. Subsequent rounds r > 2 are run until convergence to the same set of transactions is reached. Convergence to the same final transaction occurs when some user u receives sufficiently messages from the previous round where IsF inal argument is set to TRUE. Again, by sufficiently, we mean that the cumulative votes of these messages is larger than µτ .

V. ANALYSIS Theorem 1 (Agreement). For any honest users u and v that respectively decide dec u and dec v , then dec u = dec v with probability 1 -ε.

Theorem 2 (Validity). Any transaction t belonging to an honest set broadcast at round 0 will appear into the final decision with probability 1 -ε .

Theorem 3 (Termination). Our algorithm completes in a finite number of rounds r, and r is upper bounded by r max with r max = 3 ( α/λ + 1) with probability 1 -ε.

All the proofs are provided in the full version of the paper.

Recall that we cannot compel Byzantine user to follow the protocol.

We can legitimately talk about the validity of a transaction. A transaction is valid if none of its referenced UTXOs have already been spent in some transactions belonging to a previous decision value, i.e., in a block belonging to the blockchain.