Amphi H, Ensimag
1 December 2017 - 10h00
Many-Core Timing Analysis of Real-Time Systems and its Application to an Industrial Processor (Phd Defense)
by Hamza RIHANI from Univ. Grenoble Alpes / Verimag
Abstract: Predictability is of paramount importance in real-time and safety-critical systems, where non-functional properties --
such as the timing behavior -- have high impact on the system's correctness. As many safety-critical systems have a
growing performance demand, classical architectures, such as single-cores, are not sufficient anymore. One increasingly
popular solution is the use of multi-core systems, even in the real-time domain. Recent many-core architectures, such as
the Kalray MPPA, were designed to take advantage of the performance benefits of a multi-core architecture while
offering certain predictability. It is still hard, however, to predict the execution time due to interferences on shared
resources (e.g., bus, memory, etc.).
To tackle this challenge, Time Division Multiple Access (TDMA) buses are often advocated. In the first part of this
thesis, we are interested in the timing analysis of accesses to shared resources in such environments. Our approach uses
Satisfiability Modulo Theory (SMT) to encode the semantics and the execution time of the analyzed program. To estimate
the delays of shared resource accesses, we propose an SMT model of a shared TDMA bus. An SMT-solver is used to find a
solution that corresponds to the execution path with the maximal execution time. Using examples, we show how the
worst-case execution time estimation is enhanced by combining the semantics and the shared bus analysis in SMT.
In the second part, we introduce a response time analysis technique for Synchronous Data Flow programs. These are mapped
to multiple parallel dependent tasks running on a compute cluster of the Kalray MPPA-256 many-core processor. The
analysis we devise computes a set of response times and release dates that respect the constraints in the task
dependency graph. We derive a mathematical model of the multi-level bus arbitration policy used by the MPPA. Further,
we refine the analysis to account for (i) release dates and response times of co-runners, (ii)
task execution models, (iii) use of memory banks, (iv) memory accesses pipelining. Further
improvements to the precision of the analysis were achieved by considering only accesses that block the emitting core in
the interference analysis. Our experimental evaluation focuses on randomly generated benchmarks and an avionics case
study.
