Qui suis-je ?
Je m'appelle Matthieu Journault. Je suis doctorant, depuis le 1er Septembre 2016, dans l'équipe APR du LIP6. Mon encadrant est Antoine Miné.
Mon sujet de recherche est l'analyse statique modulaire précise par interprétation
abstraite pour la preuve automatique de correction de programmes et pour l’inférence de contrats.
- Static Analysis by Abstract Interpretation of the Functional Correctness of Matrix Manipulating Programs Accepted for SAS'16.
Matthieu Journault, Antoine Miné.
Abstract: We present new abstract domains to prove automatically the functional correctness of algorithms implementing matrix operations, such as matrix addition, multiplication, GEMM (general matrix multiplication), or more generally BLAS (Basic Linear Algebra Subprograms). In order to do so, we introduce a family of abstract domains parameterized by a set of matrix predicates as well as a numeric domain. We show that our analysis is robust enough to prove the functional correctness of several versions of the same matrix operations, resulting from loop reordering, loop tiling, inverting the iteration order, line swapping, and expression decomposition. Finally, we extend our method to enable modular analysis on code fragments manipulating matrices by reference, and show that it results in a significant analysis speedup.
- Power-Aware Replica Placement in Tree Networks with Multiple Servers per Client Accepted for Europar'2014.
Guillaume Aupy, Anne Benoit, Matthieu Journault, Yves Robert
Abstract: In this paper, we revisit the well-studied problem of replica placement in tree networks. Rather than minimizing the number of servers needed to serve all client requests, we aim at minimizing the total power consumed by these servers. In addition, we use the most general (and powerful) server assignment policy, where the requests of a client can be served by multiple servers located in the (unique) path from this client to the root of the tree. We consider multi-modal servers that can operate at a set of discrete speeds, using the dynamic voltage and frequency scaling (DVFS) technique. The optimization problem is to determine an optimal location of the servers in the tree, as well as the speed at which each server is operated. A major result is the NP-completeness of this problem, to be contrasted with the minimization of the number of servers, which has polynomial complexity. Another important contribution is the formulation of a Mixed Integer Linear Program (MILP) for the problem, together with the design of several polynomial-time heuristics. We assess the efficiency of these heuristics by simulation. For mid-size instances (up to 30 nodes in the tree), we evaluate their absolute performance by comparison with the optimal solution (obtained via the MILP). The most efficient heuristics provide satisfactory results, within 20% of the optimal solution.