Où docteurs et entreprises se rencontrent
Menu
Connexion

Vous avez déjà un compte ?

Nouvel utilisateur ?

Mot de passe oublié

Real-time system design using formal verification of temporal predictability

ABG-83306 Sujet de Thèse
26/02/2019 < 25 K€ brut annuel
CEA LIST
Palaiseau - Ile-de-France - France
Real-time system design using formal verification of temporal predictability
  • Informatique
Real-time, memory contentions and timing anomalies, formal methods, processor architecture

Description

A PhD proposal is available at CEA Paris-Saclay within the DACLE division (Architecture, IC Design \& Embedded Software) in a team working on real-time systems. A joint scientific supervision will be realized with Telecom ParisTech. More information about CEA LIST
 

Context


Modern computer architectures are designed to alleviate the bottleneck between processors, and memory systems, leading to utilization of caches, (automatic) pre-fetching, branch predictors, and pipeline. Such complex architectures are also used in real-time system design to cope with the continuous increase in complexity and in performance requirements of software, in particular of so called mixed-criticality systems, mixing tasks of different levels of criticalities. Real-time tasks of a mixed-criticality system require to satisfy, a posteriori, stringent timing behavior under all conditions, i.e. in the worst-case scenario.  To this end, a worst-case analysis is first performed on each task, so that Worst-Case Execution Times (WCETs) are estimated. A schedulability analysis then combines together these WCETs, and the contention overheads associated due to the parallel execution with all the other tasks, in order to check whether timing constraints can be fulfilled or not.


The WCET analysis computes sound and (desirably) tight worst-case execution bounds, exploring, via convenient abstractions, all the execution paths of a program running on a computer architecture. This searching process is however complicated by the presence of of timing anomalies [1]. In essence, a timing anomaly is a counterintuitive behavior in the sense that the local worst-case timing behavior does not result in the global worst-case performance [2]. In a real-time system exhibiting timing anomalies, a worst-case analysis must analyze all potential executions of the real-time program, considering all potentially feasible hardware states. As hardware components improve the average execution time of programs and not their WCETs, the number of hardware states to explore in these analyses increases in modern
computer architectures.


Problem and related work


This large number of states to be explored by WCET analysis tools leads to a natural compromise between analysis precision and computational overhead (or even feasibility). WCET analysis tools consequently operate on an abstract model of the actual behavior of both, software and hardware. However, these models are currently unformal models, preventing the exploration of both hardware and software patterns to evaluate the predictability issues of existing systems or to guide the construction of predictable mixed-criticality systems by feeding these patterns to AI-based algorithms.

The automatic detection of timing anomalies is addressed in [3] by building a prediction graph which is a compact representation of instruction-level simulations of program paths. [4] uses bounded model checking to explore the abstract architecture state space. A sequence of instructions that generates a scheduling timing-anomalous behavior is built, enabling the identification of timing anomalies independently from a given code. However, no complexity analysis or runtime performance results are reported. Besides, the specifics of the formal models are not described. Lastly, [5] addresses the problem of timing anomalies with sound techniques, ranging from pipeline stalls at specific points of the hardware state [6] to overapproximation of local effects with integer linear programming. However, this work does not target mixed-criticality systems and the described abstract formal model does not support execution of real applications nor comes from an hardware description language.

 

Goals and expected contributions

In this PhD proposal, we target the design of formal models of hardware components of computer architecture and of their Instruction Set Architecture (ISA) to identify code-specific timing predictability issues [7]. The following two constributions are expected of this PhD thesis:

  • the design of appropriate abstractions for a feasible identification of code-specific timing predictability issues, a major concern as most commercial architectures are non-predictable. Automatic detection of anomalous timing behaviors is useful to later insert mitigation mechanisms in order to support the design of predictable systems.
  • the exploration of the trade-off between average and worst-case performances in order to support the efficient execution of mixed-criticality real-time systems over multicore architectures. Both software and hardware mitigations will be considered, such as the definition of appropriate compilation and/or scheduling rules or adapting the behavior of the hardware to the type of task currently being executed, as in [8].

As use cases, several hardware architectures will be considered, such as the predictable platform Patmos [9], but also close to COTS architectures such as RISC-V based processors.

 

References

[1] T. Lundqvist and P. Stenström. Timing anomalies in dynamically scheduled microprocessors. In RTSS, pages 12–21, 1999.
[2] J. Reineke, B. Wachter, S. Thesing, R. Wilhelm, I. Polian, J. Eisinger, and B. Becker. A definition and classification of timing anomalies. In WCET, 2006.
[3] G. Gebhard. Static timing analysis tool validation in the presence of timing anomalies. PhD thesis, Saarland University, 2013.
[4] J. Eisinger, I. Polian, B. Becker, A. Metzner, S. Thesing, and R. Wilhelm. Automatic identification of timing anomalies for cycle-accurate worst-case execution time analysis. In DDECS, pages 15–20, 2006.
[5] S. Hahn, M. Jacobs, and J. Reineke. Enabling compositionality for multicore timing analysis. In RTNS, pages 299–308, 2016.
[6] Sebastian Hahn and Jan Reineke. Design and analysis of SIC: A provably timing-predictable pipelined processor core. In IEEE Real-Time Systems Symposium (RTSS 2018), pages 469–481, Nashville, TN, USA, Dec 2018.
[7] Mihail Asavoae, Belgacem Ben Hedia, and Mathieu Jan. Formal executable models for automatic detection of timing anomalies. In Proc. of the 18th International Workshop on Worst-Case Execution Timing analysis (WCET 2018), Barcelona, Spain, July 2018.
[8] Farouk Hebbache, Mathieu Jan, Florian Brandner, and Laurent Pautet. Shedding the shackles of time division multiplexing. In IEEE Real-Time Systems Symposium, RTSS 2018, pages 456–468, Nashville, US, December 2018.
[9] Martin Schoeberl, Wolfgang Puffitsch, Stefan Hepp, Benedikt Huber, and Daniel Prokesch. Patmos: A time-predictable microprocessor. Real-Time Systems, 54(2):389–423, Apr 2018.

 

Nature du financement

Contrat doctoral

Précisions sur le financement

Financement CEA

Présentation établissement et labo d'accueil

CEA LIST

CEA-LIST, is one of three specialized technological research institutes of CEA (French Alternative Energies and Atomic Energy Commission) Technological Research Division (CEA Tech) and specializes on digital systems

Site web :

Intitulé du doctorat

Doctorat en Informatique

Pays d'obtention du doctorat

France

Etablissement délivrant le doctorat

Université Paris Saclay

Ecole doctorale

Profil du candidat

  • M.Sc. in Computer Science
  • Knowledge in: computer architecture, real-time systems, compilers, formal methods
  • Programming, preferably including HDL (Verilog, VHDL), functional languages, scripting
  • Excellent written and spoken English
  • Communication and writing skills
  • Teamwork motivation and autonomy

Date limite de candidature

Partager via
Postuler
Fermer

Vous avez déjà un compte ?

Nouvel utilisateur ?


Mot de passe oublié
Besoin d'informations ?

Vous souhaitez recevoir une ou plusieurs lettres d’information de l’ABG. Chaque mois des actualités, des offres, des outils, un agenda…

item1
item1