Transcript Aucun titre de diapositive

The Synchronous Programming
Model and Its Applciations
Gérard Berry
Chief Scientist
Esterel Technologies
www.esterel-technologies.com
[email protected]
Embedded Systems
• computers -> embedded and networked SoCs
• complete change in device interaction
• growing number of critical applications
airplanes, automobiles, medical devices, robot surgeon
smart cards, electronic wallets
Automatic
toll
Air Con
Radio
Light control
Alarm detection
Panel
Engine control
Sleep
detector
GPS
Gearbox
Airbags
Clutch
Direction
Supension
Global Coordination
Radar
ABS
Embedded Systems on Chip
• Many processing units
• Large embedded software
CPU
DSP
RAM
ROM
GLU
FPGA
Hardware or Software?
Ennemy number 1 : the bug
• Therac 25 : lethal irradiations
• Dharan's Patriot
• Ariane V
• Mars explorers
• High-end automobile problems
• Pentium, SMP cpu networks
• Telephone and camera bugs
Bugs grow faster than Moore's law!
As soon as we started programming, we found to our surprise
that it wasn’t as easy to get programs right as we had thought.
Debugging had to be discovered.
I can remember the exact instant when I realized that a large
part of my life from then on was going to be spent in finding
mistakes in my own programs.
Maurice Wilkes, 1949
How to avoid or control bugs?
• Traditional : better verification by fancier simulation
• Next step : better design
better and more reusable specifications
simpler computation models, formalisms, semantics
reduce architect / designer distance
reduce hardware / software distance
• Better tooling
higher-level synthesis
formal property verification / program equivalence
certified libraries
Classical computation models
are inadequate
• Turing complete => too powerful, too hard to verify
• No need for fancy dynamic memory allocation
• Concurrency is mandatory, but too difficult (e.g. threads)
• Determinism is mandatory, but contradicts concurrency
• Implementation of classical control theory not obvious
• Inadapted to circuit design
There are much simpler models !
Asynchronous data-flow: Kahn Networks, Ptolemy
simple, easy concurrency, nice semantics
widely used in multimedia devices
data-deterministic, but no support for distributed control
Domain-specific synchronous languages
simple, easy concurrency, nice semantics
determinism, distributed control
same source code compiled to hardware or software
Direct match with embedded systems foundations
control engineering : sampling theory, automata theory
circuit design : RTL logic, transactional modeling
Q
R
P
P||Q
Concurrency : the compositionality principle
d
t
Q
P
t’
t’’
P||Q
t’’ = t + d + t’
t’’ ~ t ~ d ~ t’
t~t+t
R
Only 3 solutions :
• t arbitrary
asynchrony
•t=0
synchrony
• t predictable
vibration
t arbitrary : Brownian Motion
H+
Cl
_
H+
_ HCL
Cl
H+
Cl
_
HCL
H+
HCL
Chemical reaction
_
+
H + Cl
HCL
Internet routing
Zero delay example:
Newtonian Mechanics
Concurrency + Determinism
Calculations are feasible
the most difficult real-time manoeuver ever
Here should be a fabulous drawing of Hergé’s
"On a Marché sur la Lune", in English
"Explorers on the Moon". French edition, page 10,
first drawing.
Drunk Captain Haddock has become a satellite
of the Adonis asteroid. To catch him, Tintin,
courageously standing on the rocket's side,
asked Pr. Calculus to start the rocket's atomic engine.
At precisely the right time, he shouts "STOP"!
This is the trickiest real-time manoeuver ever
performed by man. It required a perfect understanding
of Newtonian Mechanics and absolute synchrony.
t predictable : vibration
Nothing can illustrate vibration better than
Bianca Castafiore, Hergé's famous prima
donna. See [1] for details. The power of her
voice forcibly shakes the microphone and
the ears of the poor spectators.
[1] King's Ottokar Sceptre, Hergé, page 29,
last drawing.
propagation of light, electrons, program counter...
The synchronous model
Bianca Castafiore singing for the King
Muskar XII in Klow, Syldavia. King's Ottokar
Sceptre, page 38, first drawing.
Although the speed of sounds is finite, it is
fast enough to look infinite. Full abstraction!
If room small enough,
predictable delay implements zero-delay
Specify with zero-delay
Implement with predictable delay
Control room size (delay analysis)
Software Synchronous Systems
Cycle based
read inputs
compute reaction
produce outputs
Synchronous = within the same cycle
propagate control
propagate signals
Zero-delay : standard model in control theory
Hardware - the RTL model
REQ
OK
TRY
PASS
GO
GET_TOKEN
PASS_TOKEN
OK = REQ and GO
PASS = not REQ and GO
GO = TRY or GET_TOKEN
PASS_TOKEN = reg(GET_TOKEN)
Synchronous languages
• Started in the 80's
ESTEREL : Ecole des Mines / INRIA, SyncCharts : Un. Nice
LUSTRE : IMAG, SIGNAL : INRIA Rennes
SAO : Aerospatiale -> Airbus, Gala : Thalès
Reactive C : Ecole des Mines, TCCP : Xerox, Quartz : Karlsruhe,
Ptolemy : Berkeley, Lava : Chalmers, Xilinx
• Industrial use in the 90's
LUSTRE / SCADE : nuclear plants (Schneider), avionics (Airbus)
Esterel : avionics (Dassault), telecom
Signal / SILDEX : continuous control (SNECMA, EDF)
Ptolemy-based systems (CoCentric) : hardware & signal processing
• => Full development in the 2000's
Data vs. Control
signals
signals
control
data
values
Esterel
SyncCharts
Argos
PBS
values
Lustre
SCADE
Signal
Lava
Esterel v7
Data-Dominated Designs
Behavior steady,data flows
data path, signal processing, continuous control
Lustre / SCADE : sequential equations, declarative
0.
U
pre
Yt = sin(Xt) * cos(Yt-1)
*
+
X
sin
pre
1.
+
Y = sin(X) * cos(pre(Y))
cos
pre
boxes = operators
arrows = data flows
S
Control-Dominated Designs
Behavior keeps changing, little data handling
state-machine control
bus protocols, memory / cache / pipeline control
Esterel v5 / SyncCharts : imperative + hierarchical behavior
abort
sustain DmaReq
when DmaOk;
abort
abort
every ByteIn do
emit ByteOut (?ByteIn)
end every
when DmaEnd
when 10 MilliSecond do
emit TimeOut
end abort
boxes = states
arrows = transitions
names = signals
hierarchy = preemption
The Evolution: Mixed Designs
Tricky control path + extensive data path
Multi-mode signal processing, alarm detection and handling
Bus bridges, QoS arbiters, fancy memory control
• Software: SCADE incorporates Esterel state machines
• Hardware: Esterel v7 incorporates Lustre equations
• + more system-oriented design features
UML architecture description
configuration management
requirement traceability
Embedded software design flow
Informal specs
simulation
animation
SCADE
data flow
automata
Matlab / Simulink modeling
Formal verification
SAT + numbers
(Prover plug-in)
DO 178-B certifiable
code generator
Embedded C / ADA code
Semantics preservation + compiler certification:
= no unit test needed on C code. Airbus : 50% savings
Esterel v7 Hardware Design Flow
Paper spec
Esterel Spec
(unique reference)
C simulation
System C
FPGA proto.
Formal verification
Test generation
hardware : VHDL, Verilog
software: C, C++
semantics is preserved throughout the flow
UART with OPB Interface
Formal semantics
Data-Flow
functional fixpoint equations + clock calculus (Lustre, Signal)
balance equations (Ptolemy)
Integration within Haskell (Lava, O'Haskell)
Control-flow
transition systems, SOS rules (Esterel)
coalgebras, coinduction (Kieburtz, Pouzet)
constructive logic (Esterel, Mendler)
Programs exactly mean what they say
Structural Operational Semantics (SOS)
E’ k
p
E
p’
E’ k
p*
E
E’ k
p
E
p|q
k=0
p’ ; p *
F’ l
p’
q
q’
E
E’ U F’ max(k,l) p’ | q’
E
Kieburtz Coalgebra Style
Compilers
• Data-flow to software (Lustre / SCADE, Signal)
inline expansion, toplogical sorting
optimization: memory allocation, locality
(limited by traceability)
• Control-flow to hardware (Esterel)
structural translation to RTL + sequential optimization
program dependency graph + smart encoding (Columbia)
• Control-flow to software
RTL simulation in software (Esterel v5 / v7)
static scheduling of control-flow graph (Synopsys)
static scheduling of aggregated blocks (France Telecom, INRIA, Columbia)
Different communities, different needs
Safety-critical software : keep it simple
prefer graphical programming
add unit-delays to break cyclic dependencies
=> strong acyclicity constraints on dependencies
=> simplified state machines
Efficient hardware : maximal power
textual programming + some state machines
agressively pack computations in the cycle
play with combinational / sequential logic (pipeline)
accept clever cycles (reincarnation, combinational cycles)
=> minimal language restrictions
Different communities, same needs
Better specifications
golden models, linked to system models
formal contracts with subcontractors
Better synthesis
why recode by hand?
Better formal verification
property checking
sequential equivalence
Architects and designers start understanding
the value of formal methods
Conclusion
• A very simple specific computation model
valid for software and hardware
• A high degree of concurrency
but still deterministic
• Mathematical semantics
made understandable and usable
• Compiling to hardware and software
correct by construction
• Formal verification
based on mathematical semantics
Work in progress
• Improve the technology
compiling / synthesis: memory / gates footprint
verification, test generation: performance
• Extend the scope
software: distribution on networks
hardware: multiclock, clock gating
modeling of non-deterministic systems (SoC)
=> add controlled non-deterministic concurrency
Some references
•
Nicolas Halbwachs “Synchronous Programming of Reactive Systems”,
Kluwer Academic, 1993
•
Gerard Berry “The Foundations of Esterel”, Proof, Language and
Interaction: Essays in Honour of Robin Milner, MIT Press, Foundations
of Computing Series, 2000.
•
Gerard Berry, “The constructive Semantics of Pure Esterel”, on-line
book, http://www.esterel-technologies.com
•
Albert Benveniste et al. “The Synchronous Languages 12 Years Later”,
IEEE Proceedings of the IEEE, vol. 91, No. 1, 2003
•
Stephen Edwards, "languages for Embedded Systems", Kluwer,
•
Dick Kieburtz, "Reactive Programming for Embedded Controllers"
•
Dick Kieburtz, "Reactive Functional Programming"
http://www1.cs.columbia.edu/~sedwards/cec/