Suchergebnisse

A typical challenge faced when developing a parametrized solver is to evaluate a set of strategies over a set of benchmarking problems. When the set of strategies is large, the evaluation is often done with a restricted time limit and/or on a smaller subset of problems in order to estimate the quality of the strategies in a reasonable time. Firstly, considering the standard SMT-LIB benchmarks, we ask the question how much the time evaluation limit and benchmark size can be restricted to still obtain reasonable performance results. Furthermore, we propose a method to construct a benchmark characteristic subset which faithfully characterizes all benchmark problems. To achieve this, we collect problem performance statistics and employ clustering methods. We evaluate the quality of our benchmark characteristic subsets on the task of the best cover construction, and we compare the results with randomly selected benchmark subsets. We show that our method achieves smaller relative error than random problem selection. ; The results were supported by the Ministry of Education, Youth and Sports within the dedicated program ERC CZ under the project POSTMAN no. LL1902, and by the ERC Project SMART Starting Grant no. 714034. This scientific article is part of the RICAIP project that has received funding from the European Union's Horizon 2020 research and innovation programme under grant agreement no. 857306.

12 pages ; Les processeurs multi-flot simultané (Simultaneous Multithreading ou SMT) peuvent être de bons candidats pour satisfaire les exigences en performances toujours croissantes des applications embarquées. Toutefois, les architectures SMT classiques ne présentent pas toujours la prévisibilité temporelle nécessaire pour permettre une analyse statique de temps d'exécution pire cas (Worst-Case Execution Times ou WCET). Dans cet article, nous analysons la prévisibilité de différentes politiques de contrôle des ressources partagées implémentées sur les coeurs SMT existants. Ensuite, nous proposons une architecture SMT conçue pour exécuter un thread temps-réel strict de façon à ce que son temps d'exécution pire cas soit analysable même si d'autres threads (non critiques) sont exécutés simultanément. Des résultats expérimentaux montrent que cette architecture reste performante, en moyenne et dans le pire cas.

12 pages ; Les processeurs multi-flot simultané (Simultaneous Multithreading ou SMT) peuvent être de bons candidats pour satisfaire les exigences en performances toujours croissantes des applications embarquées. Toutefois, les architectures SMT classiques ne présentent pas toujours la prévisibilité temporelle nécessaire pour permettre une analyse statique de temps d'exécution pire cas (Worst-Case Execution Times ou WCET). Dans cet article, nous analysons la prévisibilité de différentes politiques de contrôle des ressources partagées implémentées sur les coeurs SMT existants. Ensuite, nous proposons une architecture SMT conçue pour exécuter un thread temps-réel strict de façon à ce que son temps d'exécution pire cas soit analysable même si d'autres threads (non critiques) sont exécutés simultanément. Des résultats expérimentaux montrent que cette architecture reste performante, en moyenne et dans le pire cas.