Synchronous Languages

Lecture Notes
Real-Time and Embedded Systems Group
Wintersemester 2016/17

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, 24 Oct. 2016: Introduction (posted 24 Okt 2016, 9:30 hrs )
• Lecture 2, 24 Oct. 2016: Esterel I - Overview (posted 07 Nov 2016, 8:52 hrs )
• Lecture 3, 27 Oct. 2016: Esterel II - The Full Language (posted 07 Nov 2016, 15:53 hrs )
• Lecture 4, 7 Nov. 2016: Esterel II - Pragmatics (posted 10 Nov 2016, 13:53 hrs )
• Lecture 5, 11 Nov 2016: Esterel III - The Logical Semantics (posted 10 Nov 2016, 13:54 hrs )
• Lecture 6, 14 Nov. 2016: Esterel IV - The Constructive Semantics (posted 17 Nov 2016, 10:57 hrs )
• Lecture 7, 21 Nov. 2016: Esterel V - The Constructive Circuit Semantics (posted 21 Nov 2016, 10:00 hrs )
• Lecture 8, 24 Nov. 2016: Schizophrenia Problems (posted 27 Nov 2016, 17:43 hrs )
• Lecture 9, 28 Nov. 2016: Esterel Compilation (posted 27 Nov 2016, 17:48 hrs )
• Lecture 10, 1 Dec. 2016: SyncCharts (posted 15 Dez 2016, 10:39 hrs )
• Lecture 11, 6 Dec. 2016: SCCharts - Sequentially Constructive Statecharts for Safety-Critical Applications (posted 15 Dez 2016, 10:40 hrs )
• Lecture 12, 12 Dec. 2016: Code Generation for Sequential Constructiveness (posted 15 Dez 2016, 10:41 hrs )
• Lecture 13, 15 Dec. 2016: Sequentially Constructive Concurrency (posted 19 Jan 2017, 14:01 hrs )
• Lecture 14, 19 Jan. 2017: Sequentially Constructive Concurrency in Practice (posted 19 Jan 2017, 14:02 hrs )
• Lecture 15, 26 Jan. 2017: SCEst - Sequentially Constructive Esterel (posted 26 Jan 2017, 13:54 hrs )
• Lecture 16, 30 Jan. 2017: Strict Sequential Constructiveness (posted 31 Jan 2017, 14:59 hrs )
• Lecture 17, 30 Jan. 2017: Lustre (posted 30 Jan 2017, 10:26 hrs )

Lecture 1, 24 Oct. 2016: Introduction (slides+notes, slides, animated, posted: 24 Okt 2016, 9:30 hrs )

• About this Class
  • About this class and related classes
  • Practicalities
  • Literature
• Introduction to System Design
  • Embedded and reactive systems
  • Advanced design languages

Lecture 2, 24 Oct. 2016: Esterel I - Overview (slides+notes, slides, animated, posted: 07 Nov 2016, 8:52 hrs )

• 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

Lecture 3, 27 Oct. 2016: Esterel II - The Full Language (slides+notes, slides, animated, posted: 07 Nov 2016, 15:53 hrs )

• 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
  • 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

Lecture 4, 7 Nov. 2016: Esterel II - Pragmatics (slides+notes, slides, animated, posted: 10 Nov 2016, 13:53 hrs )

• 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

Lecture 5, 11 Nov 2016: Esterel III - The Logical Semantics (slides+notes, slides, animated, posted: 10 Nov 2016, 13:54 hrs )

• 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

Lecture 6, 14 Nov. 2016: Esterel IV - The Constructive Semantics (slides+notes, slides, animated, posted: 17 Nov 2016, 10:57 hrs )

• 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

Lecture 7, 21 Nov. 2016: Esterel V - The Constructive Circuit Semantics (slides+notes, slides, animated, posted: 21 Nov 2016, 10:00 hrs )

• The Circuit Semantics
  • Constructive circuits
  • The basic circuit translation
  • Translating the Esterel kernel
• To Go Further
  • G'erard Berry, The Constructive Semantics of Pure Esterel, Draft book, current version 3.0, Dec. 2002, Chapters 10 and 11, http://www-sop.inria.fr/members/Gerard.Berry/Papers/EsterelConstructiveBook.zip

Lecture 8, 24 Nov. 2016: Schizophrenia Problems (slides+notes, slides, animated, posted: 27 Nov 2016, 17:43 hrs )

• 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

Lecture 9, 28 Nov. 2016: Esterel Compilation (slides+notes, slides, animated, posted: 27 Nov 2016, 17:48 hrs )

• 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.

Lecture 10, 1 Dec. 2016: SyncCharts (slides+notes, slides, animated, posted: 15 Dez 2016, 10:39 hrs )

• 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

Lecture 11, 6 Dec. 2016: SCCharts - Sequentially Constructive Statecharts for Safety-Critical Applications (slides+notes, slides, animated, posted: 15 Dez 2016, 10:40 hrs )

• 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. http://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 http://rtsys.informatik.uni-kiel.de/~biblio/downloads/papers/isola14.pdf

Lecture 12, 12 Dec. 2016: Code Generation for Sequential Constructiveness (slides+notes, slides, animated, posted: 15 Dez 2016, 10:41 hrs )

• 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. http://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). http://rtsys.informatik.uni-kiel.de/~biblio/downloads/papers/tecs14.pdf

Lecture 13, 15 Dec. 2016: Sequentially Constructive Concurrency (slides+notes, slides, animated, posted: 19 Jan 2017, 14:01 hrs )

• 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

Lecture 14, 19 Jan. 2017: Sequentially Constructive Concurrency in Practice (slides+notes, slides, animated, posted: 19 Jan 2017, 14:02 hrs )

• 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

Lecture 15, 26 Jan. 2017: SCEst - Sequentially Constructive Esterel (slides+notes, slides, animated, posted: 26 Jan 2017, 13:54 hrs )

• 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. http://rtsys.informatik.uni-kiel.de/~biblio/downloads/papers/esop14.pdf
  • K. Rathlev, S. Smyth, C. Motika, R. von Hanxleden, M. Mendler. SCEst: Sequentially Constructive Esterel. In Proceedings of the 13th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE'15), Austin, TX, USA, September 2015. http://rtsys.informatik.uni-kiel.de/~biblio/downloads/papers/memocode15.pdf

Lecture 16, 30 Jan. 2017: Strict Sequential Constructiveness (slides+notes, slides, animated, posted: 31 Jan 2017, 14:59 hrs )

• Why restricting sequential constructiveness?
• Static Single Assignment
• Translation into Esterel

Lecture 17, 30 Jan. 2017: Lustre (slides+notes, slides, animated, posted: 30 Jan 2017, 10:26 hrs )

• 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

Notes:

• 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.