Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / TODO.org @ a703ed0c

History | View | Annotate | Download (4.22 KB)

1
* TODO refactoring + doc
2
- DONE separate lustre types from machine types in different files
3
- DONE split basic libs into backend specific files
4
- DONE define mli for core steps: normalization and machine code
5
- define mli for lustre_type and machine_type (Garion)
6

    
7
* TODO
8
** include files
9
** main function
10
*** add a clean test to forbid array arguments for main node
11
    (no available input/output methods)
12
** test suite
13
*** for complex dependency graphs (notably mem/mem cyclic dependencies)
14
*** for clocks
15
*** for arrays (non-generic nodes)
16
** compare with lus2c (verimag)
17
** extension
18
*** array access: done
19
*** add an option to dynamically check array accesses: done
20
*** power operator: done
21
*** automaton
22
*** annotations to ACSL
23
** init checking
24
*** to be done !!!
25
** normalization
26
*** sub-expression sharing seems to be not totally working: fixed
27
*** improve behavior for power and access operators:done
28
*** more type-directed normalization (notably to improve code gen for arrays): done
29
*** reuse of dead vars instead of systematically allocating new local vars
30
*** add a clean test for used but undefined nodes
31
** typing
32
*** correct typing of arith ops (real/int with subtyping ?)
33
*** display array dimensions with correct names: done
34
*** clocks must not be static inputs: done
35
** clock calculus
36
*** extension from named clocks to valued clocks ?
37
*** static inputs should be polymorphic, as global constants are: done
38

    
39
* Horn backend
40
** enum types for automaton
41
   - issues with MBranches and clocks
42
     - control-on-clock generates a "if cond then expr else nothing
43
     - it has to be expressed in a functional way to enable its expression as
44
       horn
45

    
46

    
47
-  The issue seems mainly to lie in the out = f(in) every cond
48
   this generates the follwoingg imperative statements
49
   if cond then f_reset(*mem) else {(nothing, ie. not reset)}
50
   f_step(in,*put,*mem)
51

    
52
   In the machine code, this is done by generating the sequence of 2 instructions
53
   1. if cond then MReset() else {}  (* creation of a conditional statement *)
54
   2. MStep()
55

    
56
- For Xavier: Syntactically, how could you "reset" an arrow? When we see an
57
  Expr_arrow, we introduce a MReset instance to the set of instruction on the
58
  reset function of the current node, but is there any mean to do it with
59
  "every" ?
60

    
61

    
62

    
63

    
64
x = expr when c
65

    
66
if c then
67
  x= expr
68

    
69
else {}
70

    
71
x = if c then expr else x
72
* Seal
73

    
74
The Seal library should be available from LustreV
75

    
76
lustrev -seal -node foo bar.lus 
77

    
78
shall inline completely the node foo in bar.lus and compile it as a
79
piecewise system: 
80
- Memories have to be identified and one needs to separate the update
81
  of the memories and the production of the output.
82
- The update block should be normalized so that any ite occuring in
83
  the definition of a memory should not define a local flow used in
84
  basic operations.  In other words, the definitions should look like
85
  mem_x = if g then e1 else e2 where e1 and e2 are either ite
86
  expression or expressions without ite. As soon as a not-ite
87
  expression is selected it cannot depend on the output of an ite.
88

    
89
In a first step this normalized update shall be printed in
90
stdout. Later it will associated to a SEAL datastructure through SEAL
91
API.
92

    
93
** Algorithm
94

    
95
*** 1. Computation of update block
96
- First we inline the node
97
- After normalization the memories are the variables defined by a pre
98
- Do we have to deal with arrows and reset?
99
- Develop a function to perform slicing. Restrict the node eqs to the ones used in these pre defs.
100
- one can also slice the expressions on the output variables
101

    
102
*** 2. Normalization: piecewise system
103
 ie. all ite pushed at the beginning
104

    
105
- use the scheduling to obtain the dependencies amongs eqs
106
- one can then iterate through eqs from the bottom to the top
107
  if the eq looks like x = if g then e1 else e2
108
  then tag x as ite(g,e1,e2)
109
  if the parent expr y = if g2 then x else ... make 
110
** More general use
111
Some ideas
112
- One could request multiple nodes: how to deal with these? Acting as
113
  as many calls to the basic procedure?
114
- Shall we keep the flatten update structure to the node? Another
115
  property on input could be propagated.
116
- The analysis will depend on bounds on input flows. Can we specialize
117
  the update blocks based on input values, ie. disabling some branches
118
  of the ite-tree?
119
- 
120

    
121
** TODO list
122

    
123
* Salsa
124
*