Processeurs prédictibles prouvés – ProTiPP

Aujourd’hui, les systèmes embarqués utilisent des algorithmes gourmands en puissance de calcul et doivent être déployés sur des plateformes multicoeurs. Par ailleurs, ils doivent respecter des échéances et nécessitent donc une vérification temporelle.
Le défi de la vérification temporelle de systèmes multicoeurs est de prendre en compte correctement les interférences d’accès aux ressources partagées. Pour limiter la complexité, les approches de l’état de l’art font l’hypothèse de la compositionnalité, qui permet de découpler l’analyse des temps d’exécution pire cas (WCET) sur chaque cœur, de l’analyse des latences d’accès aux ressources partagées (avec le coût des interférences). Mais cette hypothèse nécessite que les cœurs ne soient pas sujets à des anomalies temporelles, ce qui est probablement faux pour la plupart des processeurs du commerce. Malheureusement, la communauté manque d’outils qui permettraient de le vérifier formellement.
Le projet ProTiPP répondra à ces deux besoins en :
(1) réconciliant performance et prédictibilité. Les processeurs académiques conçus pour être prédictibles ne comblent pas les besoins en performance parce qu’ils désactivent généralement des mécanismes avancés difficiles à analyser (par exemple : exécution dans le désordre). Nous chercherons à rendre ces mécanismes prédictibles.
(2) fournissant un cadre formel pour prouver la prédictibilité temporelle. Nous concevrons des modèles formels de processeurs permettant l’expression et la vérification formelle de propriétés liées au temps. Plusieurs cadres seront étudiés (assistants de preuve, plateformes de développement formel basé sur le raffinement) pour répondre à la complexité croissante des processeurs.
Nous validerons notre approche en concevant un processeur RISC-V prédictible. Nous produirons un prototype sur FPGA ainsi qu’un outil de calcul de WCET, afin d’évaluer les performances moyennes et pire cas de ce processeur. Nos contributions seront diffusées en code open-source.