Synchronous Languages

Lecture Notes
Real-Time and Embedded Systems Group
Summersemester 2015

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, 13 April 2015: Introduction (posted 09 Jun 2015, 12:13 hrs )
• Lecture 2, 15 April 2015: Esterel I - Overview (posted 09 Jun 2015, 12:24 hrs )
• Lecture 3, 29 April 2015: Esterel II - Pragmatics (posted 09 Jun 2015, 12:25 hrs )
• Lecture 4, 6 May 2015: Esterel III - The Logical Semantics (posted 09 Jun 2015, 12:26 hrs )
• Lecture 5, 13 May 2015: Esterel IV - The Constructive Semantics (posted 09 Jun 2015, 12:27 hrs )
• Lecture 6, 18 May 2015: Esterel V - The Constructive Circuit Semantics (posted 09 Jun 2015, 12:27 hrs )
• Lecture 7, 27 May 2015: Schizophrenia Problems (posted 09 Jun 2015, 12:27 hrs )
• Lecture 8, 1 June 2015: Esterel Compilation (posted 09 Jun 2015, 12:27 hrs )
• Lecture 9, 3 June 2015: Analysing Constructiveness (posted 09 Jun 2015, 12:28 hrs )
• Lecture 10, 3 June 2015: SyncCharts (posted 09 Jun 2015, 12:28 hrs )
• Lecture 11, 10 June 2015: SCCharts - Sequentially Constructive Statecharts for Safety-Critical Applications (posted 17 Jun 2015, 9:12 hrs )
• Lecture 12, 15 June 2015: Code Generation for Sequential Constructiveness (posted 17 Jun 2015, 9:14 hrs )
• Lecture 13, 22 June 2015: Sequentially Constructive Concurrency (posted 01 Jul 2015, 11:57 hrs )
• Lecture 14, 1 July 2015: Sequentially Constructive Concurrency in Practice (posted 06 Jul 2015, 13:02 hrs )
• Lecture 15, 6 July: SCEst - Sequentially Constructive Esterel (posted 06 Jul 2015, 13:03 hrs )

Lecture 1, 13 April 2015: Introduction (slides+notes, slides, animated, posted: 09 Jun 2015, 12:13 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, 15 April 2015: Esterel I - Overview (slides+notes, slides, animated, posted: 09 Jun 2015, 12:24 hrs )

• Main Concepts
  • Introduction
  • Signals and Synchrony
  • The multiform notion of time
  • A Preview of Esterel
• 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 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, 29 April 2015: Esterel II - Pragmatics (slides+notes, slides, animated, posted: 09 Jun 2015, 12:25 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 4, 6 May 2015: Esterel III - The Logical Semantics (slides+notes, slides, animated, posted: 09 Jun 2015, 12:26 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 5, 13 May 2015: Esterel IV - The Constructive Semantics (slides+notes, slides, animated, posted: 09 Jun 2015, 12:27 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 6, 18 May 2015: Esterel V - The Constructive Circuit Semantics (slides+notes, slides, animated, posted: 09 Jun 2015, 12:27 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 7, 27 May 2015: Schizophrenia Problems (slides+notes, slides, animated, posted: 09 Jun 2015, 12:27 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 8, 1 June 2015: Esterel Compilation (slides+notes, slides, animated, posted: 09 Jun 2015, 12:27 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 9, 3 June 2015: Analysing Constructiveness (slides+notes, slides, animated, posted: 09 Jun 2015, 12:28 hrs )

• Introduction
  • Motivation
  • Logic circuits
  • Well-behaved Cyclic Circuits
  • Constructive Circuits
• Analysis of Circuits without Latches
  • Breaking Circuit Cycles
  • Three-Valued Logic
  • Malik's Procedure
  • Shiple et al.
• Analysis of Circuits with Latches
  • Latches
  • Constructiveness Algorithm
  • Application to Esterel
• Quick Conservative Causality Analysis
  • Idea
  • Algorithm
• To Go Further
  • Francois Bourdoncle,Efficient chaotic iteration strategies with widenings,In em Formal Methods in Programming and Their Applications: International Conference Proceedings, volume 735 of em Lecture Notes in Computer Science. Springer, June 1993.
  • Sharad Malik,Analysis of cyclic combinational circuits,em IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 13(7):950-956, July 1994.
  • Thomas R. Shiple, Ga'erard Berry, and Herva'e Touati,Constructive Analysis of Cyclic Circuits,In em Proc. International Design and Test Conference ITDC 98, Paris, France, March1996.ftp://ftp-sop.inria.fr/meije/esterel/papers/ConstructiveAnalysis.pdf
  • K. Schneider and J. Brandt and T. Schuele,Causality Analysis of Synchronous Programs with Delayed Actions,Conference on Compilers, Architecture, and Synthesis for Embedded Systems (CASES),179-189, Sept. 2004.http://rsg.informatik.uni-kl.de/publications/data/ScBS04b.pdf
  • Ellen M. Sentovich,Quick conservative causality analysis,In em ISSS '97: Proceedings of the 10th International Symposium on System Synthesis, pages 2-8, Washington, DC, USA, 1997. IEEE Computer Society.

Lecture 10, 3 June 2015: SyncCharts (slides+notes, slides, animated, posted: 09 Jun 2015, 12:28 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, 10 June 2015: SCCharts - Sequentially Constructive Statecharts for Safety-Critical Applications (slides+notes, slides, animated, posted: 17 Jun 2015, 9:12 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, 15 June 2015: Code Generation for Sequential Constructiveness (slides+notes, slides, animated, posted: 17 Jun 2015, 9:14 hrs )

• SCG Mapping & Dependency Analysis
  • Compilation Overview
  • The SC Graph
  • Map to SC Graph
  • Dependency Analysis
• Code Generation Approaches
  • Circuit-based Approach
  • Priority-based Approach
  • Approach Comparison
• SCCharts Benefits
  • Schizophrenia
  • 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, 22 June 2015: Sequentially Constructive Concurrency (slides+notes, slides, animated, posted: 01 Jul 2015, 11:57 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, 1 July 2015: Sequentially Constructive Concurrency in Practice (slides+notes, slides, animated, posted: 06 Jul 2015, 13: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, 6 July: SCEst - Sequentially Constructive Esterel (slides+notes, slides, animated, posted: 06 Jul 2015, 13:03 hrs )

• Reactive Systems
• SCEst

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.