Low power application architecture adaptation using SMT solvers
Adéquation algorithme architecture automatisée par solveur SMT
Résumé
We describe the Symsched methodology and environment for AAA design (Application Architecture Adequation). It allows to evaluate the energy/performance balance for a given embedded system. We translate the different components of the problem (application requirements et architecture provisions) in a system of equations and inequations made of integer variables for the modeling of temporal aspects and boolean variables for the modeling of admissible task mapping and resource states. We then submit this problem to an automatic search engine SMT solver (SAT Modulo Theories). We study the scalability of this methodology and its compromises with models expressiveness. We then study synthetic, realistic and real scheduling problems using this approach.
Nous décrivons l'environnement et la méthode Symsched dédiée à la conception conjointe dite AAA (adéquation algorithme architecture) prenant en compte les différents compromis performance énergie admissibles pour un système embarqué. Nous traduisons les descriptions des différents composants (exigences de l'application et capacités de l'architecture) en un système d'équations et inéquations composé de variables entières qui modélisent les aspects temporels et de variables booléennes qui modélisent les différentes alternatives de placement des tâches. Ce problème est ensuite soumis à un outil de résolution automatique de type SMT (SAT Modulo Theories). Notre objectif est d'étudier le passage à l'échelle de telles méthodes et donc le compromis entre le niveau de description et l'expressivité portant sur les différents aspects nécessaires à la modélisation. Nous appliquons ensuite cette technique à des problèmes d'ordonnancement abstraits, réalistes et réels.
Domaines
Autre [cs.OH]
Origine : Version validée par le jury (STAR)
Loading...