TSD 2013
3rd Tsinghua Software Day
               
 Home  Organization  Lecture  Program  Local Infomation  Contact Us  
               
Synchrony by Marc Pouzet and Louis Mandel

We shall first introduce the notion of synchrony in hardware and software, before to describe a synchronous programming language and its verification tools based on SCADE, which is used, in particular, for the development of software for airplanes all over the world, including China. We shall then describe the main current challenges, in particular, the integration of time models in synchronous languages.

Some recent developments and extensions of Synchronous Languages by Marc Pouzet

Synchronous languages has been introduced in the 80's for programming embedded control software. The purpose was to allow the designer to model control-systems in a high-level language --- mainly data-flow equations, hierarchical automata and their parallel composition ---, built on a mathematically precise semantics, and to associate it with static analysis and code generation mechanism insuring that the target code is equivalent to the source model. All these language share the "synchronous model of time", namely that computations can be neglected at modeling time because the compiler is able to generate target code which is proved to run in bounded time and space. Several academic languages were developed, notably Esterel, Lustre, Signal, and Lucid Synchrone. The industrial language SCADE 6, based on Lustre and Lucid Synchrone, is now used for the development of the most critical parts of software in various domains, notably, avionics, power generation, railways, circuits, etc.

The success of the original synchronous languages has spurred the development of new languages, based on the same principles, that increase modularity, expressiveness and that address new applications like real-time video streaming, latency-insensitive designs, large scale simulations, hybrid (continuous/discrete) systems.

Lucid Synchrone is one of these new languages. It has served as a basis for experiment with several novel extensions including, higher-order functions, type systems for the clock calculus, hierarchical state machines with shared variables, signals and new compilation methods. Many of these ideas have been adopted in commercial tools, notably SCADE 6. New topics include techniques for allowing bounded desynchronisation through buffers (N-synchrony) and extensions for modeling continuous systems.

During my talk, I will present the mathematical principles of synchronous languages, the major extensions that has been done in the past, notably the mix of data-flow with hierarchical automata. Then, I will detail two recent research development:

  • The extension of synchronous languages to deal with computer intensive applications that communicate through bounded FIFOs (e.g., TV boxes);
  • The treatment of discrete and continuous-time to model, in a unified manner, both a discrete controller and its physical environment described by Ordinary Differential Equations (ODEs).

SMT Solving for Nonlinear Theories over the Reals by Edmund Clarke

We describe our open-source tool dReal, an SMT solver for nonlinear formulas over the reals. The tool can handle various nonlinear real functions such as polynomials, trigonometric functions, exponential functions, etc. dReal implements the framework of delta-complete decision procedures: It returns either unsat or delta-sat on input formulas, where delta is a numerical error bound specified by the user. When the answer is unsat, dReal produces a proof of unsatisfiability; when delta-sat, it provides a solution that witnesses the satisfiability of a delta-perturbed form of the input formula. With such relaxation, delta-complete decision procedures can fully exploit the power of scalable numerical algorithms to solve nonlinear problems, and at the same time provide suitable correctness guarantees for various correctness-critical problems.

Simulation technology for application development in the multicore era by Erik Hagersten

The recent trend in multicore architecture brings the promise of great performance at low cost. Just parallelize a single application or run several independent applications simultaneously in a throughput manner. However, multicores also introduce new bottlenecks that could result in slower-than-sequential execution, even if the application is embarrassingly parallel. Tuning for multicore requires insights into complex resource sharing (e.g., caches and bandwidth), thread interaction (e.g., synchronization, coherence and false sharing) and power consumption. Who cares how many FLOPS, MIPS, cores, or threads a chip has if its performance is limited by other factors?

In this talk I will advocate that simulation and modeling technology is needed, not only for hardware developers, but also for application developers. Such use requires two to three orders of magnitude lower overhead than traditional simulation technology. I will present statistical simulation methods, architecturally independent performance metrics and performance variability studies as three possible í░simulationí▒ technologies for such use.