Seminar details

Abstract: PhD students present their work.
- 14:00 Hamza Rihani: WCET Analysis in Shared Resources Real-Time Systems
Abstract:
Predictability is an important aspect in real-time and safety-critical systems, where non-functional properties -- such as the timing behavior -- have high impact on the system correctness. As many safety-critical systems have a growing performance demand, old and simple architectures are not sufficient anymore. Multi-core systems offer higher processing speed but may lack the safety requirements. Recent many-core architectures, such as the Kalray MPPA, were designed to combine the performance benefits of a multi-core architecture with the required predictability. However, it is still hard to predict the execution time due to interferences on shared resources (bus, memory,...).

In this work we are interested in the analysis of accesses to shared resources. We first propose an approach, using Satisfiability Modulo Theory (SMT) and an SMT-solver to find the longest path with correct semantics and largest execution path. We demonstrate how this approach can be applied straightforwardly to a TDMA bus. However, it lacks flexibility and it is hard to extend to other architectures.

The Kalray MPPA architecture uses a multi-level arbitration policy to access a shared memory. The SMT-based analysis fails to scale for such configurations. We present another approach using an adapted existing framework that can be generic but very pessimistic. We also discuss how existing methods, based on ILP and SMT modeling and adapted for this purpose, can enhance the estimation of the Worst-Case Execution Time (WCET).

- 14:40 Denis Becker: Understanding, Measuring and Solving the Problem of SystemC Parallelization.
Abstract:
SystemC/TLM models are commonly used in the industry to provide an early SoC simulation environment. When SystemC has been standardized it has been chosen that simulators shall fulfill coroutine semantics, for many good reasons. Most of SystemC simulator implementations are sequential programs, due to coroutine semantics. Even when present, parallelization is still experimental. Though, with the increasing size and complexity of models, sequential simulations have become too slow and leave the parallelization opportunities provided by recent machines unexploited.
There have been several proposals for SystemC parallelization, but most of them do not solve our problem, because they can fundamentally not apply to our platforms at STMicroelectronics. We support this claim with a set of measurements performed on a case study used in production at ST.
We will see that the most time-consuming parts of our study case at ST consists in video encoders/decoders. Such components offer a good opportunity for parallel computing because they use queue communications. We propose to exploit this queue communication mechanism in order to simulate concurrently different blocks. The main issue is to keep the concurrent parts synchronized with the SystemC kernel, and to still fulfill coroutine semantics. The fact that every inter-module communication operates through the queue interface is our chance here. We will present our current solutions and their results on a test bench.
- 15:20 Santosh Arvind Adimoolam: Computing zonotopic invariants for some hybrid systems

Abstract:
We discuss methods for computing invariant zonotopes for two classes of hybrid systems: quasi periodic linear impulsive systems and discrete hybrid affine systems. Invariant sets are useful for proving stability and safety of a system. For quasi periodic linear implusive systems, we introduce a new class of sets called complex zonotopes for specifying invariants, which are extension of real zonotopes by having complex valued generators and combining coefficients. We shall motivate the reason for considering complex zonotopes and discuss two methods for computing complex zonotopic invariants. For discrete hybrid affine systems, we consider scaled real zonotopes for specifying invariants, which are zonotopes whose directions of generators and magnitudes of generators are specified separately. Our method is to find the magnitudes, also called scaling factors, for a fixed set of directions such that the scaled zonotope is a positive invariant. To this end, we derive a set of bilinear and linear constraints and propose a policy iteration technique for solving the bilinear constraints.