Algorithms, Machines and Languages
Informatics of Time and Events
This is essentially the subject on which Gérard Berry has been working since 1982, first as a researcher at the Paris Ecole des Mines, then at INRIA, and next as Vice-President for Research at Esterel Technologies, a company which develops and markets software workbenches for the certified design of critical systems in sectors such as avionics, rail and heavy industry. Gérard Berry developed Esterel, a synchronous language, along with its mathematical semantics, techniques of compilation towards conventional programming languages or electronic circuits, as well as related techniques for formal verification of temporal properties in software. This research was conducted in collaboration with teams from Verimag laboratory at CNRS Grenoble (Lustre language by Paul Caspi and Nicolas Halbwachs), INRIA Rennes (Signal language by Albert Benveniste and Paul Le Guernic) and Lassy laboratory in Nice (SyncCharts graphical formalism by Charles André). Esterel, Lustre and SyncCharts formalisms were unified under the Esterel v7 language dedicated to electronic circuit synthesis, followed by the SCADE 6 tool developed by Esterel Technologies and which is now a standard for critical embedded software. Worthy of note is that France has always played a leading role in this sector, which is now expanding globally.
Gérard Berry has also conducted research on asynchronous parallelism models in which parallel actors do not share a common time model. In 1992, with Gérard Boudol (INRIA), he defined the Chemical Abstract Machine (CHAM), a particularly simple mathematical formalism which has now become a conceptual standard in the field.
Lectures and seminars for 2012-2013 essentially discussed the synchronous model that forms the basis of the above-mentioned languages: design, mathematical semantics, compilation techniques and applications. Lectures and seminars for 2013-2014 expanded the approach to cover richer time models, combining synchronous and asynchronous time on the one hand and discrete time and continuous time on the other hand. These combined models underpin the most recent systems, including: real-time distributed software, multi-clock electronics, globally-distributed yet synchronized databases, combined simulations of physical phenomena with discrete and continuous components, mixed human performer/computer-synthesized music and Web services orchestration. Although currently becoming de facto standards, they still pose considerable scientific challenges, the most critical of which is cooperation between different time models.
Proving Programs: Why, When, How?
This is the overall title chosen for lectures in 2014-2015 and subsequent years. The conventional method for developing software is through testing, performed either with files describing software input data and events, or in physical situations for circuits and embedded software. Testing is effective to identify bugs, but one fundamental shortcoming is that it can never guarantee their absence. This was recognized as early as 1949 in a forward-thinking paper by Alan Turing, who suggested software tests should be replaced with actual mathematical proof of correctness. Many researchers have worked on the subject since the early days of computing, initially in an academic environment primarily. They developed several types of formal verification methods for programs and circuits, including: assertions, rewriting, abstract interpretation, logical deduction and verification of models. This basic research is both arduous and long-winded, and has helped to improve our understanding of the design and formal semantics of programming languages and programs themselves, while also allowing substantial progress in the more mathematical field of formal logic.
The maturing of various automatic verification computer systems and proof assistants has brought formal verification to the level of real-life applications, including in industry: key security properties verification in avionics (Dassault Aviation with Esterel), driving verifications for Parisian suburban (RER) and metro trains (using Jean-Raymond Abrial’s B-Method), correction of the Pentium chip’s floating-point arithmetic (by John Harrison, with HOL-Light for Intel and David Rusinoff et. al., with ACL2 for AMD), systematic verification of electronic circuit synthesis steps (effective model-checking techniques based on BDDs, SAT and SMT formal calculations), verification of track-switching and routing systems in large railway stations (by Prover Technology), verification of the SEL4 operating system kernel (by Gerwin Klein et. al. with proof assistant Isabelle), verification of the CompCert C compiler (by Xavier Leroy, with Coq). Surprisingly, techniques originally developed for computing have also found applications in mathematics, with Georges Gonthier proving major theorems such as the 4-Color theorem and, more importantly, the Feit-Thompson theorem on the classification of finite groups of odd order. (Note that Georges Gonthier had previously made fundamental contributions to Esterel in his doctoral thesis). Interestingly, computerized mathematical proofs have much to teach us about technical architectures required to prove large programs.
The lectures for 2014-2015 will seek to present the issues and different methods of proof within a broader context: such a presentation does not yet exist, as the above methods were developed in a rather scattered way. Lectures in subsequent years will examine the finer details of the main methods and their applications.
Current Research Topics of the Chair in Algorithms, Machines and Languages
Research currently conducted under the Chair covers three aspects: Web services orchestration, musical composition and new musical notations for algorithmic music, and the formal verification of an Esterel compilation kernel.
The orchestration of Web services and connected objects is presented in collaboration with Manuel Serrano’s team at INRIA Sophia-Antipolis. Web services are programs available on computers accessed remotely over the Internet and using the standard http protocol for communication. Rather than simply returning HTML pages for screen display, Web services return results that can be interpreted directly by the calling program, thus creating a comprehensive system of remote procedure calls over the network. Connected devices (smartphones, but also homes or cars) can be accessed in the same way. The distributed system generated by services and connected devices is fundamentally asynchronous, yet can be accessed through the relatively simple client-server model the Web’s http protocol allows. Our work is based on Hop, a language created by Manuel Serrano which considerably simplifies asynchronous processing. Hop replaces the “tower of Babel” of Web languages with a single language used to write distributed programs in the form of a single source code. It then compiles the programs and distributes fragments of local code across the different systems where the fragments are to be run. But there is more: all events associated with the communications network or provided by the connected objects must be managed harmoniously – this is known as “orchestrating the application”. To achieve this, a synchronous approach is ideal. This is why we defined and implemented HipHop, a specialized language layer within Hop. This synchronous language can be seen as a highly dynamic version of Esterel: an airplane always has two wings and three sets of wheels, while Web applications are inherently dynamic, with components that can appear or disappear at any time or cause multiple runtime errors. We have shown that the mathematical semantics in Esterel can be preserved in such a dynamic environment, while retaining the ability to dynamically change the very text of the HipHop program between two reactions to events. This is because the principle of synchronous reaction makes it possible to clearly separate reactions to event steps from reconfiguration steps, which is impossible in the asynchronous formalisms typically associated with the Web. All of this was presented in the lectures given in 2013-2014. However, HipHop is currently a mere prototype requiring additional development for it to become fully operational.
The second topic is computer-generated music. It is examined in collaboration with researchers and composers from IRCAM, as well as with composer Philippe Manoury, who also teaches at the Conservatoire in Strasbourg. Composers of contemporary music have long been working with forms of music combining human performers and electronic sounds. Until recently, the electronic elements were either recorded or performed in real time by a computer according to a fixed tempo which human performers had to follow. Through her outstanding doctoral thesis, Arshia Cont (a researcher at IRCAM) has developed Antescopo, a predictive sheet-music monitoring system. The system can identify in real time the various events described in the score (notes, for instance) and then help to understand – and to some extent, predict – how musicians play: tempo, articulation, etc. The result is that electronics can be controlled by the performers rather than the opposite. Obviously, this is a major development for composers and performers, and the system is now used in concerts all over the world. Its ability to detect events in real time also helps to condition the launch of complex electronic sections when specific events or sequences of events are detected. This raises the problem of musical notation for such sections: as computer reading skills are not limited, there is no need to string notes on a staff as in conventional sheet music. What’s more, it is now possible to inject randomness in the electronic sections. Adequate musical notation must then evolve towards new notions of algorithmic scores, where sounds and sound sequences are generated by arbitrarily complex algorithms. Another major issue is the management of errors which never fail to occur during performance – either human performer errors, or errors of the real-time monitoring system. These are all robust arguments in favor of creating algorithmic languages dedicated to music. A language prototype based largely on Esterel concepts is currently under development for Antescofo, and is already being used in concerts, but much more work will need to go into this fascinating and largely open field.
The most recent research topic is the construction of a proven compiler for the Esterel language kernel towards electronic circuit diagrams. This is the subject of ongoing postdoc work by Lionel Rieg, Assistant Lecturer for the Chair since September 2014. The idea is to program the compiler and its proof jointly in the Coq verification system, allowing automatic extraction of Caml code that is effective for the compiler. This work will build on Esterel’s formal semantics, as established by Gérard Berry and improved by Olivier Tardieu in the mid-2000s. We anticipate difficulties will arise with the finer translation points, as in any adventure of this kind. The purpose is also to use this research work as an example of formal proof for upcoming lectures, thereby building a bridge between past and present lectures on synchronous languages.
The multidisciplinary Chronos seminar
Since 2012, Gérard Berry has hosted a multidisciplinary seminar under the name Chronos, which is dedicated to time and events in five scientific fields: automation (control theory), computing, electronic music, computational neuroscience and bioinformatics. The seminar took the form of a network funded by the French National Research Agency (Agence National de la Recherche, ANR) in October 2012. The basic idea is to compare viewpoints from different disciplines connected by an obvious convergence of interests revealed in the first informal seminars. For instance, the study of numerous oscillators in the brain or that of the transition from unconscious to conscious information can be of benefit to the study of multiple synchronicities in automation and computing, which could in turn unveil new topics for reflection and computer simulation. The same type of convergence could also emerge between the treatment of time in systemic bioinformatics (cell simulation is one example) and computer time and events. All of this is basic research, i.e. research on fundamental topics, and it is therefore much too early for it to claim to deliver concrete results. However, it is precisely through this kind of network that research on the synchronous model and its extensions started and thrived. This type of flexible and informal research tool serves as a highly conducive framework for in-depth research, which is why we are particularly eager to thank the French National Research Agency for the support and funding it has offered.