Autotuning Parallel Programs by Model Checking

This 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 counterexample method 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 counterexamples constructed during the verification of the optimality property. In the fourth step, we extract the information about the tuning parameters from the counterexample 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, which formal semantics is good for modeling the execution of parallel programs on processors with different architectures.