Hamza Rihani

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.