Welcome to Synchron 2016

Description

 
This workshop is devoted to all aspects of synchronous programming: language design, compilation and code generation, formal verification, static analysis and testing, programming environments, execution platforms, semantics issues in synchronous concurrency and scheduling, modelling pragmatics, etc. It is an open forum where both students and senior researchers/engineers can present and discuss about ongoing work on the numerous topics related to synchronous programming. This traditional workshop is the annual rendezvous hotpot of the synchronous community and a 'must' event for anyone interested in keeping up with the latest developments in academic and industrial synchronous research.

Synchronous languages have been introduced in the 1980s to program safety-critical reactive and embedded systems. Such systems are characterised by their continuous concurrent interaction which is synchronised by logical clocks that ensure reactive progress and functional determinacy. The key advantage of the synchronous approach is its rigorous mathematical semantics which allows to build software tools to support correct-by-verification or correct-by-construction code generation for the programmers to develop critical embedded software faster and better.

Invited Speakers

Prof. Edward A. Lee, UC Berkeley.

Title: Resurrecting Laplace's Demon: The Case for Deterministic Models.

Abstract: In this talk, I will argue that deterministic models have historically proved extremely valuable in engineering, despite fundamental limits. I examine the role that models play in engineering and contrast it with the role that they play in science, and I argue that determinism is an extraordinarily valuable property in engineering, much more than science. I will then show that deterministic models for cyber-physical systems, which combine computation with physical dynamics, remain elusive in practice. I will argue that synchronous languages and their extension, discrete-event languages, combined with more deterministic processors, can solve this problem. I will then examine some fundamental limits of determinism, showing that chaos limits its utility for prediction, and that incompleteness means that at least for CPS, nondeterminism is inevitable.

About the speaker: Edward A. Lee is the Robert S. Pepper Distinguished Professor in the Electrical Engineering and Computer Sciences (EECS) department at U.C. Berkeley. His research interests center on design, modeling, and analysis of embedded, real-time computational systems. He is the director of the nine-university TerraSwarm Research Center (http://terraswarm.org), a director of Chess, the Berkeley Center for Hybrid and Embedded Software Systems, and the director of the Berkeley Ptolemy project. From 2005-2008, he served as chair of the EE Division and then chair of the EECS Department at UC Berkeley. He is co-author of six books and hundreds of papers. He has led the development of several influential open-source software packages, notably Ptolemy and its various spinoffs. He received his BS degree in 1979 from Yale University, with a double major in Computer Science and Engineering and Applied Science, an SM degree in EECS from MIT in 1981, and a PhD in EECS from UC Berkeley in 1986. From 1979 to 1982 he was a member of technical staff at Bell Labs in Holmdel, New Jersey, in the Advanced Data Communications Laboratory. He is a co-founder of BDTI, Inc., where he is currently a Senior Technical Advisor, and has consulted for a number of other companies. He is a Fellow of the IEEE, was an NSF Presidential Young Investigator, won the 1997 Frederick Emmons Terman Award for Engineering Education, and received the 2016 Outstanding Technical Achievement and Leadership Award from the IEEE Technical Committee on Real-Time Systems (TCRTS).

Prof. Stephen Edwards, Columbia University.

Title: Haskell to Hardware and Other Dreams.

Abstract: Moving forward, an increasing fraction of system-on-chip hardware will have to be application-specific to reduce energy consumption, yet most hardware is still designed using the register-transfer level technique that has changed little since the 1990s.

In this talk, I discuss our ongoing project designed to deliver the abstractions of 21st century programming languages to the hands of hardware designers.  Our goal is to translate arbitrary programs from the functional Haskell language into synthesizable RTL, letting designers focus on parallel algorithms instead of the minutiae of logic and flip-flops.  Adopting a pure functional approach provides Church-Rosser-style determinism in the presence of parallelism.

Our compiler dismantles features like recursion and algebraic data types into a dataflow representation that is then scheduled and translated into hardware.  Among other things, we show how to infer pipeline parallelism from tail recursion.

About the speaker: He obtained his Ph.D from the University of California, Berkeley in 1997, his MS from Berkeley in 1994, and his BS from the California Institute of Technology in 1992, all in Electrical Engineering. Before pursuing his academic career in 2001, he worked for two Electronic Design Automation (EDA) companies, Simplex Solutions, now part of Cadence, and Synopsys. Professor Edwards and his group explore automating the creation of software for embedded systems. They have developed numerous compilation techniques for the Esterel synchronous language for real-time control and are also developing domain-specific languages for device drivers and communication protocols.

Keynote

Prof. Albert Benveniste, IRISA / INRIA, Campus de Beaulieu.

Title: Structural analysis of multi-mode DAE systems, application to Modelica.

Abstract: Differential Algebraic Equation (DAE) systems constitute the mathematical model supporting physical modeling languages such as Modelica or Simscape. Unlike ODEs, they exhibit subtle issues because of their implicit latent equations and related differentiation index. Multi-mode DAE (mDAE) systems are much harder to deal with, not only because of their mode-dependent dynamics, but essentially because of the events and resets occurring at mode transitions. Unfortunately, the large literature devoted to the numerical analysis of DAEs do not cover the multi-mode case. It typically says nothing about mode changes. This lack of foundations cause numerous difficulties to the existing modeling tools. Some models are well handled, others are not, with no clear boundary between the two classes. In this paper we develop a comprehensive mathematical approach to the structural analysis of mDAE systems which properly extends the usual analysis of DAE systems. We define a constructive semantics based on nonstandard analysis and show how to produce execution schemes in a systematic way.

About the speaker: He graduated in 1971 from Ecole des Mines de Paris. He performed his These d'Etat in Mathematics, probability theory, in 1975, under the supervision of Paul-André Meyer. From 1976 to 1979 he was associate professor in mathematics at Universite de Rennes I. From 1979 to 2014 he has been Directeur de Recherche at INRIA, where he is now an emeritus. In 1980 Albert Benveniste was co-winner of the IEEE Trans. on Automatic Control Best Transaction Paper Award for his paper on blind deconvolution in data communications. In 1990 he received the CNRS silver medal, in 1991 he has been elected IEEE fellow, and in 2013 he has been elected IFAC Fellow. In 2008 he was winner of the Grand Prix France Telecom of the french Academy of Sciences. From 1986 to 1990 he was vice-chairman of the IFAC committee on Theory and was chairman of this committee for 1991-1993. He has been or is Associate Editor (at Large) for IEEE Transactions on Automatic Control, Associate Editor for Int. J. of Adaptive Control and Signal Processing, and Int. J. of Discrete Event Dynamical Systems. He is currently member of the Editorial Board of the Proceedings of the IEEE. From 1994 to 1996 he has been Directeur Scientifique (Senior Chief Scientist) at Inria. From 1997 to 2001, he has been chairman of the "software chapter" of the RNRT funding programme of the french ministeries for research and telecommunications, for telecommunications (Reseau National de la Recherche en Telecommunications). Since 1997, he has been responsible for INRIA of the joint Alcatel-INRIA research programme and is now chief scientist of the joint Bell Labs-INRIA research lab. He is member of the scientific board of INRIA, in charge of embedded systems area. He has been member of the advisory board of T-Source, a venture capitalist specialist in seed capital for the telecommunications sector. He is a member of the scientific advisory boards of Safran Group and Orange. From June 2011 to March 2014, he was co-heading the Center of Excellence (Labex) CominLabs in the area of telecommunications and Information systems. He has been elected to the Académie des Technologies in december 2011

The workshop topics cover, but are not restricted to, the following issues:

• Synchronous and asynchronous models for time and concurrency
• Safety-critical real-time systems
• Synchronous languages and programming formalisms
• Synchronous hybrid models for control theory
• Compilation techniques and code synthesis for single/multi-threaded, multi-core, multi-processing architectures
• Formal specification, type theories and model-theoretic verification of synchronous programs
• Test and validation of programs
• Modelling and simulation environments
• Timing Analysis for synchronous programs
• Component-based development of embedded systems
• Discrete and hybrid systems
• High-level hardware modeling and synthesis
• Novel language paradigms blending synchrony with asynchrony and non-determinism
• semantic abstraction and refinement
• Design methodologies, visualisation of complex reactive systems
• Case-studies, industrial and teaching experience reports

Previous editions of this workshop were held in:

• Kiel (Germany, 2015)
• Aussois (France, 2014)
• Dagstuhl (Germany, 2013)
• Le Croisic (France, 2012)
• Dammarie-les-Lys (France, 2011)
• Fréjus (France, 2010)
• Dagstuhl (Germany, 2009)
• Aussois (France, 2008)
• Bamberg (Germany, 2007)
• L'Alpe d'Huez (France, 2006)
• Qwara (Malta, 2005)
• Dagstuhl (Germany, 2004)
• Luminy (France, 2003)
• La Londe les Maures (France, 2002)
• Dagstuhl (Germany, 2001)
• Saint-Nazaire (France, 2000)
• Hyères (France, 1999)
• Gandia (Spain, 1998)
• Roscoff (France, 1997)
• Dagstuhl (Germany, 1996)
• Luminy (France, 1995)
• Dagstuhl (Germany, 1994)

The event is kindly supported by the Technologieallianz Oberfranken TAO,  Esterel Technologies and the German Research Foundation (DFG) project PRETSY2.