The major drawback of using static schedules to execute dataflow applications is their high inflexibility. In real-time systems, periodic schedules make it easier to assert safety guarantees and to decrease the schedule size, but their characteristics remain hard to compute. This article presents an approach to automatically generate fixed priority schedules from a dataflow specification. To do so, precedence dependencies between actors in the dataflow graphs are abstracted, as well as the task periods, by using affine relations . This abstraction allows us to synthesize schedules efficiently considering two main objectives: the maximization of throughput and the minimization of buffer sizes. Given a dataflow graph to execute in a real-time environment, we transform it into an Affine Dataflow Graph (ADFG) and compute the task priorities, their mapping, the number of delays in the buffers, and the buffer sizes. This article is the first to present an overview of both theoretical and practical aspects of ADFG. On the theoretical side, it presents corrections and improvements on the fixed priority case. On the practical side, benchmark evaluations demonstrate the robustness and maturity of the approach that our scheduling synthesizer implements. Synthesized schedules are evaluated by using scheduling simulation and real-time implementation. Last but not least, the synthesized periods reach the optimal throughput if enough processors are available, and most of the time the periods reach the maximal processor utilization factor in the uni-processor case. Moreover, execution time of the synthesis is about only 1 second for the main proposed algorithms.

Novel memory architectures have been introduced in multi/many-core processors to address the performance bottle neck due to shared memory accesses. Taking the advantages brought by these architectures in scheduling analysis is still an open challenge. In this article, we present a scheduling analysis technique that exploits a shared multi-bank memory architecture to efficiently schedule parallel real-time applications modeled as synchronous data flow (SDF) graphs by minimizing the memory access contentions. Our approach aims at producing a static time-triggered schedule with the objective of minimizing the makespan and buffer size requirements while respecting consistency and data dependency constraints. An Integer Linear Programming formulation of the scheduling problem is presented, as well as a heuristic with significantly lower time complexity. Experimental results are given using synthetic SDF graphs generated by the SDF3 tool and applications available in the StreamIt benchmark.

The ANTAREX project developed an approach to the performance tuning of High Performance applications based on an Aspect-oriented Domain Specific Language (DSL), with the goal to simplify the enforcement of extra-functional properties in large scale applications. The project aims at demonstrating its tools and techniques on two relevant use cases, one in the domain of computational drug discovery, the other in the domain of online vehicle navigation. In this paper, we present an overview of the project and of its main achievements, as well as of the large scale experiments that have been planned to validate the approach.

Designing and optimizing applications for energy-efficient High Performance Computing systems up to the Exascale era is an extremely challenging problem. This paper presents the toolbox developed in the ANTAREX European project for autotuning and adaptivity in energy efficient HPC systems. In particular, the modules of the ANTAREX toolbox are described as well as some preliminary results of the application to two target use cases. 1

The ANTAREX project relies on a Domain Specific Language (DSL) based on Aspect Oriented Programming (AOP) concepts to allow applications to enforce extra functional properties such as energy-efficiency and performance and to optimize Quality of Service (QoS) in an adaptive way. The DSL approach allows the definition of energy-efficiency, performance, and adaptivity strategies as well as their enforcement at runtime through application autotuning and resource and power management. In this paper, we present an overview of the ANTAREX DSL and some of its capabilities through a number of examples, including how the DSL is applied in the context of one of the project use cases.

This presentation demonstrates a scalable, modular, refinable methodology for translation validation applied to a mature (20 years old), large (500k lines of C), open source (Eclipse/Polarsys IWG project POP) code generation suite, all by using off-the-shelf, open-source, SAT/SMT verification tools (Yices), by adapting and optimizing the translation validation principle introduced by Pnueli et al. in 1998. This methodology results from the ANR project VERISYNC, in which we aimed at revisiting Pnueli's seminal work on translation validation using off-the-shelf, up-to-date, verification technology. In face of the enormous task at hand, the verification of a compiler infrastructure comprising around 500 000 lines of C code, we devised to narrow down and isolate the problem to the very data-structures manipulated by the infrastructure at the successive steps of code generation, in order to both optimize the whole verification process and make the implementation of a working prototype at all doable. Our presentation outlines the successive steps of this endeavour, from clock synthesis, static scheduling to target code production.

This paper investigates the way state diagrams can be best represented in the polychronous model of computation. In this relational model, the basic objects are signals, which are related through data-flow equations. Signals are associated with logical clocks, which provide the capability to describe systems in which componentsobey to multiple clock rates. We propose a model of finite-state automata, called polychronous automata, which is based on clock relations. A specificity of this model is that an automaton is submitted to clock constraints. This allows one to specify a wide range of control-related configurations, either reactive, or restrictivewith respect to their control environment. A semantic model is defined for these polychronous automata, that relies on a Boolean algebra of clocks.

This paper presents a distribution methodology for synchronous programs, applied in particular on programs written in the Quartz language. The given program is first transformed into an intermediate model of guarded actions. After user-specified partitioning, the generated sub-models are transformed into Signal processes. Using the multi-clock calculation model of the Signal language, an optimized data-flow network can be automatically constructed. The optimization includes reducing the communication quantity and the computation load, with no change to the interface behaviors.

High-level architecture modeling languages, such as Architecture Analysis & Design Language (AADL), are gradually adopted in the design of embedded systems so that design choice verification, architecture exploration, and system property checking are carried out as early as possible. This paper presents our recent contributions to cope with clock-based timing analysis and validation of software architectures specified in AADL. In order to avoid semantics ambiguities of AADL, we mainly consider the AADL features related to real-time and logical time properties. We endue them with a semantics in the polychronous model of computation; this semantics is quickly reviewed. The semantics enables timing analysis, formal verification and simulation. In addition, thread-level scheduling, based on affine clock relations is also briefly presented here. A tutorial avionic case study, provided by C-S, has been adopted to illustrate our overall contribution.

The UML Profile for Modeling and Analysis of Real-Time and Embedded systems (MARTE) defines a mathematically expressive model of time, the Clock Constraint Specification Language (CCSL), to specify timed annotations on UML diagrams and thus provides them with formally defined timed interpretations. Thanks to its expressive capability, the CCSL allows for the specification of static and dynamic properties, of deterministic and non-deterministic behaviors, or of systems with multiple clock domains. Code generation from such multi-clocked specifications (for the purpose of synthesizing a simulator, for instance) is known to be a difficult issue. We address it by using the approach of controller synthesis. In our framework, a timed CCSL specification is regarded as a property whose satisfaction should be enforced for any UML diagram carrying it as annotation. To do so, CCSL statements are first translated into dynamical polynomial systems. Such systems can be manipulated using the model-checker Sigali to synthesize an executable property (a controller) which enforces the satisfaction of the specified timing constraints on the UML diagram with which it is executed.

Design of critical embedded systems demands for guarantees on the reliability of the implementation/compilation of a specification. In general, this guarantee takes either the form of a certified compiler, or the validation of each translation. Here we adopt the translation validation approach. In particular, we translate both the SIGNAL specification and the associated C simulator into LTSs. Then, an appropriate (successful) preorder test between both LTSs can be interpreted as a refinement between the C implementation and its source SIGNAL specification, otherwise, counter-examples are generated automatically. The feasibility of our approach is shown through examples.

The synchronous modeling paradigm provides strong execution correctness guarantees to embedded system design while making minimal environmental assumptions. In most related frameworks, global execution correctness is achieved by ensuring endochrony: the insensitivity of (logical) time in the system from (real) time in the environment. Interestingly, endochrony can be statically checked, making it fast to ensure design correctness. Unfortunately, endochrony is not preserved by composition, making it difficult to exploit with component-based design concepts in mind. Compositionality can be achieved by weakening the objective of endochrony but at the cost of an exhaustive state-space exploration. This raise a tradeoff between performance and precision. Our aim is to balance it by proposing a formal design methodology that adheres to a weakened global design objective: the non-blocking composition of weakly endochronous processes, while preserving local endochrony objectives. This yields an ad-hoc yet cost- efficient approach to compositional synchronous modeling.

This paper presents the techniques used for the compilation of the data-flow, synchronous language SIGNAL. The key feature of the compiler is that it performs formal calculus on systems of boolean equations. The originality of the implementation of the compiler lies in the use of a tree structure to solve the equations.