compile Kernel Esterel to Lustre
git clone
Log | Files | Refs | README

README (6586B)

      1 kesterel2lustre -- compile Kernel Esterel to Lustre
      2 Copyright (C) 2011 by Antoine Amarilli
      4 This program is free software: you can redistribute it and/or modify it under
      5 the terms of the GNU General Public License as published by the Free Software
      6 Foundation, version 3.
      8 This program is distributed in the hope that it will be useful, but WITHOUT ANY
      9 WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A
     10 PARTICULAR PURPOSE.  See the GNU General Public License for more details.
     12 You should have received a copy of the GNU General Public License along with
     13 this program (see file "COPYING").  If not, see <>.
     17 == 0. Description ==
     19 kesterel2lustre FILE parses the Kernel Esterel file FILE, compiles it to the
     20 Lustre language and displays the result on standard output.
     22 Kernel Esterel is the subset of Esterel defined in [Ber99] p. 21 (quoted in
     23 [Wik11]). It is complete, in the sense that other Esterel constructs can be
     24 expressed with it. It is defined as follows:
     26 FILE ::= module NAME: input SIGS; output SIGS; EXPR end module
     27 SIGS ::= SIG | SIG, SIGS
     28 EXPR ::=   nothing
     29          | pause
     30          | EXPR; EXPR
     31          | EXPR || EXPR
     32          | loop EXPR end
     33          | signal SIG in EXPR end
     34          | emit SIG
     35          | present SIG then EXPR else EXPR end
     36          | suspend EXPR when SIG
     37          | trap TRAP in EXPR end
     38          | exit TRAP
     40 The abort construct is not supported because it can be implemented from those
     41 base constructs (see [Wik11], provided as test case test/myabort.strl).
     44 == 1. Dependencies ==
     46 kesterel2lustre requires a working Haskell installation along with the Parsec
     47 monadic parser combinator library (package libghc-parsec3-dev on Debian
     48 systems). The automated testing suite requires working Esterel and Lustre
     49 installations (see section 4).
     51 To compile kesterel2lustre, run:
     53   make
     56 == 2. Structure ==
     58 - main.hs: Main program.
     59   The main program reads the file and calls each of the subsequent steps in
     60   turn.
     61 - esterel.hs: Esterel.
     62   The Esterel AST.
     63 - lustre.hs: Lustre.
     64   The Lustre AST.
     65 - parse.hs: Parser.
     66   The parser (using Parsec) parses the input file to produce the Esterel AST (or
     67   an error). 
     68 - checker.hs: Instantaneous dependencies.
     69   The checker is called by the parser to detect loops with instantaneous paths.
     70 - scope.hs: Compute input and output signals and traps.
     71   The scope module recursively computes which signals can be emitted or read by
     72   a subexpression and produces an AST tagged with this information.
     73 - label.hs: Compute unique node identifiers.
     74   The label module recursively assigns a unique identifier to each AST node and
     75   produces an AST tagged with this information.
     76 - compile.hs: Perform the compilation.
     77   The compile module produces the Lustre AST from the Esterel AST.
     78 - produce.hs: Lustre code production.
     79   The produce module renders the Lustre AST to a string.
     82 == 3. Limitations ==
     84 - The program does not check that output signals can be raised and that input
     85   signals are read and are not raised.
     86 - The program requires exactly one "input" declaration and exactly one "output"
     87   declaration; furthermore, these declarations cannot be empty.
     88 - The program does not require signals to be declared with a Signal construct.
     89 - Signals and Traps live in the same namespace and no check is performed to
     90   ensure that one isn't used in place of the other. Undefined behavior will
     91   result if both are mixed.
     92 - The compile.hs file is ugly and messy.
     93 - There is no support for signal S1, ..., Sn in ... end. To achieve this, use n
     94   nested signal blocks.
     95 - present clauses must have a then branch and an else branch.
     96 - Instantaneous loops are detected, but there is no detection of cyclic
     97   constructs like present A then emit A else nothing end. Compilation of such
     98   programs will yield a Lustre program with causality loops.
    101 == 4. Testing ==
    103 kesterel2lustre comes with an automated testing suite to compare the behavior
    104 of the Esterel code (tested with the [Est11] distribution) and the behavior of
    105 the Lustre code produced by kesterel2lustre (tested with the [Lus11]
    106 distribution).
    108 The tests are the .strl files in the test/ directory, which will be run on the
    109 corresponding .in input files. Because of technical limitations, the test files
    110 should declare their input and output signals in alphabetical order. The test
    111 commands assume that a working Esterel and Lustre environment is available and
    112 properly set up. Some test cases were taken from examples in [Ber99].
    114 To run file test/at0.strl on input test/ using the Esterel distribution,
    115 run:
    117   ./ at0
    119 To run it using the kesterel2lustre compilation and Lustre distribution, run:
    121   ./ at0
    123 To run all tests and compare the output of the two evaluation mechanisms, run:
    125   ./
    128 == 5. Translation mechanism ==
    130 Each AST node is compiled to a Lustre node. All nodes have a control, suspend
    131 and reset input wire, and a control output wire. They also have input wires
    132 corresponding to the signals and traps that descendents of the AST are reading,
    133 and output wires for those that are produced.
    135 In addition, a root node is produced to initialize the control and suspend
    136 wires.
    138 The suspend wire is only used for the suspend construct. It is initialized to
    139 false in the root node, transmitted from each node to its descendents, and
    140 set to interesting stuff at the suspend nodes. Each node has two local variables
    141 to (1) store the information that the node has been suspended and (2) compute
    142 the real input control from this information.
    144 The translation of nothing, pause, emit, ';', present and loop is performed as
    145 in [Pou08]. The translation of '||' is performed as in [Pou08] with a slight
    146 change to allow signals from the two child nodes of the '||' to be propagated to
    147 their siblings.
    149 The translation of exit is to see the trap as a signal and emit it without
    150 relinquishing control. The translation of trap is to yield control when the trap
    151 signal is emitted, without propagating it to father nodes, and set the reset
    152 wire of the sub nodes to disable input control everywhere.
    154 The translation of signal is to propagate all information except the signal that
    155 was declared as local.
    158 == 6. Sources ==
    160 [Ber99]
    161 [Pou08]
    162 [Est11]
    163 [Lus11]
    164 [Wik11]