Synchronous Languages
Lecture Notes
Real-Time and Embedded Systems Group
Summer Semester 2020
Lecturer: Reinhard v. Hanxleden
The slides+notes version is 4-up, includes notes, and uses a
printer-friendly coloring scheme. To save paper, empty
notes are eliminated, except when they are necessary to place
subsequent (non-empty) notes below the slide to which they belong.
The slides version of the lectures is as shown in class, without
animation (only one page per slide).
The animated version of the lectures is as shown in class,
including animation (may be multiple pages per slide).
The bottom of this page contains further notes.
- Lecture 1, 7 April 2020: Introduction
(posted )
- Lecture 2, 9 April 2020: Esterel I - Overview
(posted )
- Lecture 3, 16 April 2020: Esterel II - The Full Language
(posted )
- Lecture 4, 21 April 2020: Esterel II - Pragmatics
(posted 21 Apr 2020, 11:14 hrs
)
- Lecture 5, 23 April 2020: Esterel III - The Logical Semantics
(posted 28 Apr 2020, 13:48 hrs
)
- Lecture 6, 30 April 2020: Esterel IV - The Constructive Semantics
(posted 30 Apr 2020, 11:50 hrs
)
- Lecture 7, 7 May 2020: Esterel V - The Constructive Circuit Semantics
(posted 07 Mai 2020, 11:51 hrs
)
- Lecture 8, 14 May 2020: Schizophrenia Problems
(posted 19 Mai 2020, 10:59 hrs
)
- Lecture 9, 19 May 2020: Esterel Compilation
(posted 19 Mai 2020, 11:11 hrs
)
- Lecture 10, 26 May 2020: SyncCharts
(posted 26 Mai 2020, 11:36 hrs
)
- Lecture 11, 28 May 2020: SCCharts - Sequentially Constructive Statecharts for Safety-Critical Applications
(posted 27 Mai 2020, 10:57 hrs
)
- Lecture 12, 4 June 2020: Code Generation for Sequential Constructiveness
(posted 02 Jun 2020, 11:51 hrs
)
- Lecture 13, 11 June 2020: Sequentially Constructive Concurrency
(posted 11 Jun 2020, 11:50 hrs
)
- Lecture 14, 16 June 2020: Blech - Synchronous Programming at Bosch
(posted 16 Jun 2020, 15:04 hrs
)
- Lecture 15, 18 June 2020: Timed SCCharts
(posted 18 Jun 2020, 14:12 hrs
)
- Lecture 16, 23 June 2020: Lustre
(posted 30 Jun 2020, 10:57 hrs
)
- Lecture 17, 25 June 2020: From Lustre to SCCharts
(posted 26 Jun 2020, 10:30 hrs
)
- About this Class
- About this class and related classes
- Practicalities
- Literature
- Introduction to System Design
- Embedded and reactive systems
- Advanced design languages
- Introduction
- Signals and Synchrony
- The multiform notion of time
- A Preview of Esterel
- To Go Further
- G'erard Berry, The Foundations of Esterel, Proof, Language and Interaction: Essays in Honour of Robin Milner, G. Plotkin, C. Stirling and M. Tofte, editors, MIT Press, Foundations of Computing Series, 2000, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.53.6221
- G'erard Berry, The Esterel v5 Language Primer, Version v5_91, 2000 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.15.8212
- A Tour through Esterel
- The ABRO Example
- The SPEED Example, Signals and Variables
- Weak and Strong Abortion
- Modules
- Further Esterel Statements
- Further Basic Statements
- Process Suspension
- Variants of Discussed Statements, Trap vs. Abort
- Host Language
- The Kernel Language
- To Go Further
- Examples
- People Counter Example
- Vending Machine Example
- Tail Lights Example
- Traffic-Light Controller Example
- Interfacing with the Environment
- Available Alternatives
- Handling Inconsistent Outputs
- Events vs. State
- Logical Correctness
- Causality issues
- The logical coherence law
- Logical reactivity and determinism
- Instantaneous Feedback
- The Logical Behavioral Semantics
- Notation and Definitions
- The Basic Broadcasting Calculus
- Transition Rules
- Reactivity and Determinism
- To Go Further
- Gérard Berry, The Constructive Semantics of Pure Esterel, Draft book, current version 3.0, Dec. 2002 http://www-sop.inria.fr/members/Gerard.Berry/Papers/EsterelConstructiveBook.zip
- Gérard Berry, Preemption in Concurrent Systems, In Proceedings FSTTCS 93, Lecture Notes in Computer Science 761, pages 72-93, Springer-Verlag, 1993,http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.42.1557
- The Constructive Semantics
- External Justification vs. Self-Justification
- The Constructive Behavioral Semantics
- The Constructive Operational Semantics
- To Go Further
- Albert Benveniste, Paul Caspi, Stephen A. Edwards, Nicolas Halbwachs, Paul Le Guernic, Robert De Simone, The synchronous languages 12 years later, Proceedings of the IEEE, Jan. 2003 vol. 91, issue 1, pages 64-83, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.96.1117
- The Circuit Semantics
- Constructive circuits
- The basic circuit translation
- Translating the Esterel kernel
- To Go Further
- Schizophrenia and Reincarnation
- The Problem
- Solving the Reincarnation Problem
- Tardieu and de Simone (2004)
- To Go Further
- G'erard Berry, The Constructive Semantics of Pure Esterel, Draft book, current version 3.0, Dec. 2002, Chapter 12, http://www-sop.inria.fr/members/Gerard.Berry/Papers/EsterelConstructiveBook.zip
- Klaus Schneider and M. Wenz, A New Method for Compiling Schizophrenic Synchronous Programs, CASES 2001, http://es.cs.uni-kl.de/publications/datarsg/ScWe01.pdf
- Oliver Tardieu and Robert de Simone, Curing Schizophrenia by Program Rewriting in Esterel, MEMOCODE 2004 http://www1.cs.columbia.edu/~tardieu/papers/memocode04.pdf
- Esterel Compilation
- Automata-Based Compilation
- Netlist-Based Compilation
- Control-Flow Graph-Based Compilation
- Experimental Comparison
- To Go Further
- Stephen A. Edwards. Tutorial: Compiling Concurrent Languages for Sequential Processors. ACM Transactions on Design Automation of Electronic Systems (TODAES), 8(2):141-187, April 2003. http://www1.cs.columbia.edu/~sedwards/papers/edwards2003compiling.pdf
- Stephen A. Edwards and Jia Zeng. Code Generation in the Columbia Esterel Compiler. EURASIP Journal on Embedded Systems, vol. 2007, Article ID 52651, 31 pages, 2007. http://dx.doi.org/10.1155/2007/52651
- Dumitru Potop-Butucaru, Stephen A. Edwards, and Gérard Berry. Compiling Esterel. Springer-Verlag, New York, 2007. ISBN 9780387706269
- Jan Lukoschus and Reinhard von Hanxleden.Removing Cycles in Esterel Programs.EURASIP Journal on Embedded Systems, Special Issue on Synchronous Paradigms in Embedded Systems.http://www.hindawi.com/getarticle.aspx?doi=10.1155/2007/48979, 2007.
- SyncCharts (Safe State Machines)
- Comparison with Harel's Statecharts
- Simple Automata, Hierarchy, Concurrency/Parallelism
- A Tour of SyncCharts
- From Esterel to SyncCharts
- Step 1: Transform Esterel to SyncChart
- Step 2: Reduce to Fully Graphical SyncChart
- Step 3: Optimizations
- From SyncCharts to Esterel
- Examples
- Structural Translation
- Ordering States
- Motivation
- Contribution
- Overview
- SCCharts Overview
- Overview
- Features
- Core Transformations
- Extended SCCharts $rightarrow$ Core SCCharts
- Connector
- Signal
- Strong Abort
- Normalizing Core SCCharts & Implementation
- Compilation / Normalization
- Modelling SCharts
- Conclusion
- To Go Further
- R. von Hanxleden, B. Duderstadt, C. Motika, S. Smyth, M. Mendler, J. Aguado, S. Mercer, and O. O'Brien. SCCharts: Sequentially Constructive Statecharts for Safety-Critical Applications. Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'14), Edinburgh, UK, June 2014. https://rtsys.informatik.uni-kiel.de/~biblio/downloads/papers/pldi14.pdf
- C. Motika, S. Smyth and R. von Hanxleden, Compiling SCCharts - A Case-Study on Interactive Model-Based Compilation, Proc. 6th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2014), Corfu, Greece, LNCS 8802, pp. 443-462 https://rtsys.informatik.uni-kiel.de/~biblio/downloads/papers/isola14.pdf
- SCG Mapping & Dependency Analysis
- Compilation Overview
- The SC Graph
- Dependency Analysis
- Code Generation Approaches
- Circuit-based Approach
- Priority-based Approach
- Approach Comparison
- Schizophrenia Revisited
- Classic Approaches
- The SCL Solution
- Summary
- To Go Further
- J. Aguado, M. Mendler, R. von Hanxleden, I. Fuhrmann. Grounding Synchronous Deterministic Concurrency in Sequential Programming. In Proceedings of the 23rd European Symposium on Programming (ESOP'14), Grenoble, France, April 2014. https://rtsys.informatik.uni-kiel.de/~biblio/downloads/papers/esop14.pdf
- R. von Hanxleden, M. Mendler, J. Aguado, B. Duderstadt, I. Fuhrmann, C. Motika, S. Mercer, O. O'Brien, and P. Roop. Sequentially Constructive Concurrency - A Conservative Extension of the Synchronous Model of Computation. ACM Transactions on Embedded Computing Systems, Special Issue on Applications of Concurrency to System Design, July 2014, 13(4s). https://rtsys.informatik.uni-kiel.de/~biblio/downloads/papers/tecs14.pdf
- Motivation
- C, Java vs. Synchronous Programming
- The Control Example
- A Constructive Game of Schedulability
- Formalizing Sequential Constructiveness (SC)
- The SC Language (SCL) and the SC Graph (SCG) [Sec. 2]
- Free Scheduling of SCGs [Sec. 3]
- The SC Model of Computation [Sec. 4]
- Wrap-Up
- Synchronous Program Classes
- Summary
- Timed SCCharts
- To Go Further
- Reinhard von Hanxleden, Timothy Bourke, Alain Girault. Real-Time Ticks for Synchronous Programming. In Proc. Forum on Specification and Design Languages (FDL ’17), Verona, Italy, September 2017. https://rtsys.informatik.uni-kiel.de/~biblio/downloads/papers/fdl17.pdf
- Alexander Schulz-Rosengarten, Reinhard von Hanxleden, Frédéric Mallet, Robert de Simone, Julien Deantoni. Time in SCCharts. In Proc. Forum on Specification and Design Languages (FDL ’18), Munich, Germany, September 2018. https://rtsys.informatik.uni-kiel.de/~biblio/downloads/papers/fdl18.pdf
- A Short Tour
- Examples
- Clock Consistency
- Arrays and Recursive Nodes
- To Go Further
- Nicolas Halbwachs and Pascal Raymond, A Tutorial of Lustre, 2002 http://www-verimag.imag.fr/~halbwach/lustre-tutorial.html
- Nicolas Halbwachs, Paul Caspi, Pascal Raymond, and Daniel Pilaud,The Synchronous Data-Flow Programming Language Lustre, In Proceedings of the IEEE, 79:9, September 1991, http://www-verimag.imag.fr/~halbwach/lustre:ieee.html
- The notes here are typically posted right before or after
class. If you are curious about the whole curriculum of this class,
you can have a look at the lecture notes from the last
time this class was held.
- The lecture notes are generated with LaTeX and the beamer
class. The process of generating the various PDFs and the
following HTML overview and of uploading everything to the web server
is largely automated - which is convenient, but makes it easy to
overlook things that have gone wrong in the process. Hence, if
something appears to have gone wrong, please drop a note to Reinhard v. Hanxleden.