README (6586B)
1 kesterel2lustre -- compile Kernel Esterel to Lustre 2 Copyright (C) 2011 by Antoine Amarilli 3 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. 7 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. 11 12 You should have received a copy of the GNU General Public License along with 13 this program (see file "COPYING"). If not, see <http://www.gnu.org/licenses/>. 14 15 16 17 == 0. Description == 18 19 kesterel2lustre FILE parses the Kernel Esterel file FILE, compiles it to the 20 Lustre language and displays the result on standard output. 21 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: 25 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 39 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). 42 43 44 == 1. Dependencies == 45 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). 50 51 To compile kesterel2lustre, run: 52 53 make 54 55 56 == 2. Structure == 57 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. 80 81 82 == 3. Limitations == 83 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. 99 100 101 == 4. Testing == 102 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). 107 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]. 113 114 To run file test/at0.strl on input test/at0.in using the Esterel distribution, 115 run: 116 117 ./rungolden.sh at0 118 119 To run it using the kesterel2lustre compilation and Lustre distribution, run: 120 121 ./runtest.sh at0 122 123 To run all tests and compare the output of the two evaluation mechanisms, run: 124 125 ./testall.sh 126 127 128 == 5. Translation mechanism == 129 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. 134 135 In addition, a root node is produced to initialize the control and suspend 136 wires. 137 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. 143 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. 148 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. 153 154 The translation of signal is to propagate all information except the signal that 155 was declared as local. 156 157 158 == 6. Sources == 159 160 [Ber99] http://rw4.cs.uni-sb.de/teaching/esd07/papers/constructiveness3.ps 161 [Pou08] http://www.di.ens.fr/~pouzet/cours/mpri/MPRI08SolExamMP.pdf 162 [Est11] http://www.di.ens.fr/~pouzet/cours/mpri/esterelv5_92.linux.tar 163 [Lus11] http://www-verimag.imag.fr/~raymond/m2p/distrib/linux64/index.html 164 [Wik11] https://en.wikipedia.org/wiki/Esterel 165