Geodesic
Autotuning parallel programs by model checking
Modelirovanie i analiz informacionnyh sistem, Tome 28 (2021) no. 4, pp. 338-355

Voir la notice de l'article provenant de la source Math-Net.Ru

The paper presents a new approach to autotuning data-parallel programs. Autotuning is a search for optimal program settings which maximize its performance. The novelty of the approach lies in the use of the model checking method to find the optimal tuning parameters by the method of counterexamples. In our work, we abstract from specific programs and specific processors by defining their representative abstract patterns. Our method of counterexamples implements the following four steps. At the first step, an execution model of an abstract program on an abstract processor is described in the language of a model checking tool. At the second step, in the language of the model checking tool, we formulate the optimality property that depends on the constructed model. At the third step, we find the optimal values of the tuning parameters by using a counterexample constructed during the verification of the optimality property. In the fourth step, we extract the information about the tuning parameters from the counter-example for the optimal parameters. We apply this approach to autotuning parallel programs written in OpenCL, a popular modern language that extends the C language for programming both standard multi-core processors (CPUs) and massively parallel graphics processing units (GPUs). As a verification tool, we use the SPIN verifier and its model representation language Promela, whose formal semantics is good for modelling the execution of parallel programs on processors with different architectures.
Keywords: optimization problem, auto-tuning of parallel programs, parallel programs, GPU programming, model checking, counterexamples, OpenCL, SPIN
Mots-clés : Promela. 
@article{MAIS_2021_28_4_a2,
     author = {N. O. Garanina and S. P. Gorlatch},
     title = {Autotuning parallel programs by model checking},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {338--355},
     publisher = {mathdoc},
     volume = {28},
     number = {4},
     year = {2021},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2021_28_4_a2/}
}
TY  - JOUR
AU  - N. O. Garanina
AU  - S. P. Gorlatch
TI  - Autotuning parallel programs by model checking
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2021
SP  - 338
EP  - 355
VL  - 28
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2021_28_4_a2/
LA  - en
ID  - MAIS_2021_28_4_a2
ER  - 
%0 Journal Article
%A N. O. Garanina
%A S. P. Gorlatch
%T Autotuning parallel programs by model checking
%J Modelirovanie i analiz informacionnyh sistem
%D 2021
%P 338-355
%V 28
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2021_28_4_a2/
%G en
%F MAIS_2021_28_4_a2
N. O. Garanina; S. P. Gorlatch. Autotuning parallel programs by model checking. Modelirovanie i analiz informacionnyh sistem, Tome 28 (2021) no. 4, pp. 338-355. http://geodesic.mathdoc.fr/item/MAIS_2021_28_4_a2/