Synchronous Languages
Lecture Notes
Real-Time and Embedded Systems Group
Wintersemester 2018/19
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, 23 October 2018: Introduction
(posted 23 Okt 2018, 12:57 hrs
)
- Lecture 2, 29 October 2018: Esterel I - Overview
(posted )
- Lecture 3, 30 Oct. 2018: Esterel II - The Full Language
(posted 29 Okt 2018, 9:10 hrs
)
- Lecture 4, 6 Nov. 2018: Esterel II - Pragmatics
(posted 11 Nov 2018, 17:13 hrs
)
- Lecture 5, 12 Nov 2018: Esterel III - The Logical Semantics
(posted 18 Nov 2018, 16:53 hrs
)
- Lecture 6, 13 Nov. 2018: Esterel IV - The Constructive Semantics
(posted 18 Nov 2018, 16:49 hrs
)
- Lecture 7, 20 Nov. 2018: Esterel V - The Constructive Circuit Semantics
(posted 20 Nov 2018, 11:31 hrs
)
- Lecture 8, 26 Nov. 2018: Schizophrenia Problems
(posted 20 Nov 2018, 16:26 hrs
)
- Lecture 9, 3 Dec. 2018: Esterel Compilation
(posted 03 Dez 2018, 9:18 hrs
)
- Lecture 10, 4 Dec. 2018: SyncCharts
(posted 29 Jan 2019, 10:54 hrs
)
- Lecture 11, 10 Dec. 2018: SCCharts - Sequentially Constructive Statecharts for Safety-Critical Applications
(posted 29 Jan 2019, 10:55 hrs
)
- Lecture 12, 11 Dec. 2018: Code Generation for Sequential Constructiveness
(posted 29 Jan 2019, 10:55 hrs
)
- Lecture 13, 7 Dec. 2019: Sequentially Constructive Concurrency
(posted 29 Jan 2019, 10:56 hrs
)
- Lecture 14, 15 Jan. 2019: Sequentially Constructive Concurrency in Practice
(posted 29 Jan 2019, 10:57 hrs
)
- Lecture 15, 26 Jan. 2017: SCEst - Sequentially Constructive Esterel
(posted 22 Feb 2019, 9:26 hrs
)
- Lecture 16, 30 Jan. 2017: Strict Sequential Constructiveness
(posted 29 Jan 2019, 12:10 hrs
)
- Lecture 17, 29 Jan. 2018: Time in SCCharts
(posted 29 Jan 2019, 12:20 hrs
)
- Lecture 18, 4 Feb. 2019: Lustre
(posted 04 Feb 2019, 10:07 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
- DFG-funded PRETSY Project: www.pretsy.org
- 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
- Conservative Static Approximation of SC
- SC-Schedules
- Schedule Order
- Schedule / Program Classes
- Determining SC-Schedules with Priorities
- Priority-Based Scheduling [Sec. 5.2]
- Computing Priorities [Sec. 5.3]
- Summary
- Reactive Systems
- SCEst
- 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
- S. Smyth, C. Motika, K. Rathlev, R. von Hanxleden, M. Mendler. SCEst: Sequentially Constructive Esterel. ACM Transactions on Embedded Computing Systems (TECS) - Special Issue on MEMOCODE 2015, 17(2):33:1–33:26, December 2017. https://rtsys.informatik.uni-kiel.de/~biblio/downloads/papers/tecs17.pdf
- Why restricting sequential constructiveness?
- Static Single Assignment
- Translation into Esterel
- Sequentially Constructive Circuit Semantics for Esterel
- To Go Further
- A. Schulz-Rosengarten, S. Smyth, R. von Hanxleden, M. Mendler. On Reconciling Concurrency, Sequentiality and Determinacy for Reactive Systems - A Sequentially Constructive Circuit Semantics for Esterel. In 2018 18th International Conference on Application of Concurrency to System Design (ACSD), pages 95-104, June 2018. https://rtsys.informatik.uni-kiel.de/~biblio/downloads/papers/acsd18.pdf
- Reactive Systems
- SCEst
- Traffic Light Example
- Execution Models
- Dynamic Ticks
- Time in SCCharts: "clock"
- Multiclocks in SCCharts: "period"
- To Go Further
- 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.