Synchronous Languages and System Design with EsterelOutlineSystem DesignSlide 4ApplicationsReactive System CharacteristicsSynchronous SystemsSynchronous LanguagesEsterel: BackgroundSlide 10Esterel: Basic PrinciplesOverview of SyntaxSyntax : await statementVariables and OrderingThe ABRO ExampleThe ABRO Example in EsterelCompilationTranslation to Boolean CircuitsSlide 19CausalityHarmful CyclesSlide 22Harmless CyclesSlide 24Slide 25Slide 26Slide 27Causality: A Real ExampleStrange CyclesSlide 30Slide 31Constructive Causality in EsterelExecuting Constructive CausalitySlide 34Slide 35Slide 36Slide 37Main Theorem (Shiple Berry from Brzozowski - Seger)Algorithms (Esterel v5)Slide 40Slide 41Dual-Rail Encoding to Implement Constructive AnalysisSlide 43Causality SummaryGraphical Symbolic DebuggingOptimizationLatch OptimizationSlide 48Latch Optimization : Exclusive SetsLatch Optimization : ResultsVerificationThe Esterel ToolsetECL ProjectECL Summary : LanguageECL Key FeaturesExample : simple CExample : add reactivity / concurrencyExample : complete ECL moduleECL compilationSlide 60Slide 62Example : post-compilationECL SummaryImplementing Esterel Programs in POLISSlide 66Slide 67Slide 68ExampleSlide 70Slide 71Slide 72Slide 73Slide 74Slide 75Slide 76Slide 77Slide 78Slide 79Slide 80Slide 81Slide 82Slide 83Slide 84Slide 85Termination signalSlide 87Using CompositionalitySummarySynchronous Languagesand System Design with EsterelEllen SentovichCadence Berkeley LaboratoriesOutline•Context : Reactive Systems•Principles : Synchronous languages•Esterel in-depth–Language, Compilation–Causality–Optimization and Verification•New applications: ECL•Implementing Esterel on CFSM networksSystem Design•Systems produce a steady sequence of input/output sequences•Inconvenient to specify sequences; need models and languages•Model–Simple and intuitive–Accurate enough model of physical reality–Mathematically efficient–General enough to allow different implementation styles•Language–Accurate expression of the model–Convenient and efficient expression of the design•Analysis•Implementation–compilation to hardware, softwareReactive Systems control data signalssensorssignalsvaluesEsterelStatechartsArgosEsterelStudioLustreSCADESignalApplications•Software and hardware controllers–process control, embedded systems,data-path control•Communication Protocols–software protocols,bus interfaces,cache coherence•Drivers–man-machine interface,systems drivers,pipeline logicConcurrency + DeterminismReactive System Characteristics•Reactivity–continually react at a speed determined by the environment•Concurrency–at least between system and environment•Strict time and reliability requirements•Deterministic•Mixed hardware/software implementationsSynchronous SystemsCycle based read inputs compute reaction produce outputsSynchronous within the same cycle at the same time (0-delay) (must be checked on implementation)Synchronous control propagation signal broadcastingEquivalent FSM implementation(good analysis techniques)Synchronous Languages•Invented for the design of reactive kernels–not the interactive interface or data management•Programmer views system as an instantaneous reactor to events•Program behavior is completely deterministic•Attempt to resolve concurrency and non-determinism (in other models)Esterel: Background•Esterel is one of a set of synchronous languages developed in France:–Esterel: reactive control–Lustre, Signal: data flow–Argos, SyncCharts: graphical•Esterel development goal: natural expression of control–Specific statements to deal with time, preemption–Departure from concurrency as interleaving and rendez-vous to concurrency as instantaneous propagation of controlEsterel: Background•Synchronous programming environment...–Language:•For control-dominated, reactive systems•Constructs for sequencing, concurrency, preemption–Compiler:•Produces sorted Boolean equations•Causality checking, symbolic debugging, verification•Implementation as C-code or digital circuitsEsterel: Basic Principles•Synchronous hypothesis : instantaneous communication•Communication via broadcast signals (event)–signals, sensors, variables–pure, valued–Boolean and arithmetic operators•Modularity : program = collection of modules•Concise programs : write things once !!•Concurrency, sequencing, preemption•Well-defined semanticsOverview of Syntax•Signal reading/writingemit S emit S(value) present S then p else q•Basic control and looping:halt loop p end run module•Sequencing, concurrencyp ; q p || q•Preemptionsuspend p when S abort p when Sweak abort when S abort when immediate SSyntax : await statement•Most basic signal control statementawait S•Equivalent toabortloophaltendwhen S•Note: “Await” always stops–consider await S; await S–versus await immediate S; await immediate SVariables and Ordering•Variable manipulation (local)V := value if V=value then p else q•Variable computations : orderedV := 5;V := V+1;Y := V;emit S(V)•Signal emissions (communication) : unorderedLegal: emit S; emit SIllegal: emit S(3); emit S(5) (non-deterministic)•Signal computations : orderedWell-defined: emit S; present SUndefined: present S then emit SThe ABRO Example•“Wait until both A and B have occurred, then output O, unless the reset R occurs”A BB/0A/OAB/ORRRNumber of states is exponential in inputsThe ABRO Example in Esterel•Wait until both A and B concurrency•Unless R preemption[await A || await B] ;emit Oabortwhen RloopendWrite things ONCE !!Code size is linear in inputs; efficient circuitCompilation•Esterel program extended finite state machine–finite # inputs, deterministic reaction finite program–FSM + data computations•Can be compiled to a single automata - EXPENSIVE!!–exhaustive exploration of set of control states–Esterel v3•Can be translated to sorted Boolean equations–Esterel v5•State machine is represented implicitlyTranslation to Boolean Circuits•Structural translation•Network of interconnected cells•Implementation of control:–control signal runs through the circuit–boot signal : latch, initially 1, thereafter 0•Each cell contains–signal input/output; control input/output–suspend, kill, resume signals–return codes (nested preemption)•One register per halting statementTranslation to Boolean Circuits•present S then p else
View Full Document
Unlocking...