Auto-Tuning High-Performance Programs
Using Model Checking in Promela

We aim at bringing together two research areas that have traditionally been disjoint:1) model checking used in formal verification of programs, and 2) auto-tuning used in the optimization of programs for modern high-performance architectures that comprise multi-core universal processors (CPU) and many-core Graphics Processing Units (GPU).

Auto-tuning [1] is an important case of the general concept of automated algorithm configuration and parameter tuning. It has become especially popular recently in developing parallel programs: it finds the values of the performance-critical program parameters that ensure optimal performance of the program code on a particular target architecture and problem data size. Typical examples of such tuning parameters for parallel programs in the OpenCL language are: number of threads, tile size, workgroup size, shared-memory block size, etc. The potentially large number of tuning parameters and their complicated interplay in influencing program performance makes it very difficult even for an expert to find a (near to) optimal combination of parameter values that ensures good performance on a particular machine and for a particular size of input data.

For the implementation of auto-tuning, an auto-tuning framework (auto-tuner) is used: the framework automatically generates a search space of parameter configurations and then examines this space by running the program for chosen configurations on a real hardware of the target high-performance system. The currently popular auto-tuners include OpenTuner [2], PATUS [3], ATLAS [4], FFTW [5], CLTune [6], ATF [7], to name a few. They use a variety of techniques to find the optimal solution, including simulated annealing, random search, genetic algorithms, machine learning, and dynamic programming. Only few of auto-tuners nowadays offer exhaustive search, which guarantees to find the optimal result but implies extremely high time costs for checking all possible configurations: the search for a solution of high quality may take several hours or even days on a high-performance system.

In this paper, we attempt to improve auto-tuning by using modern model checking tools. The goal of our approach is to automatically find good tuning parameter values faster than existing auto-tuners, and without using real hardware. Model checking is widely used for formal program verification: it checks the satisfiability of a particular program property for all scenarios of a program model behavior. Both the model and the property are specified using formal languages. For example, a program model can be represented as a Kripke structure, and a property as an LTL temporal logic formula. If the property is not satisfied then the model checking method can find a counterexample, i.e., conditions and sequence of actions of the model that imply that the property is not satisfied.

Our approach to auto-tuning based on model checking relies on exhaustive or swarm search by using a counterexample constructed during the verification of the optimality property for a program which is to be auto-tuned. We have been inspired by previous research on using counterexamples for solving optimization problems and, in particular, compiling optimal schedules for reactive systems [8, 9, 10, 11, 12]. A special edition of Dagstuhl seminar [13] was devoted to the interrelation of automatic planning/optimization and model checking methods. The recent progress in model checking has achieved that modern tools examine each element of the search space using various shortcuts, such as symbolic encoding, partial order reduction, and abstraction [14]. Due to these shortcuts, exhaustive exploration of larger search spaces can be done in a shorter time.

An important expected benefit of using model checking for auto-tuning is that the target high-performance architecture does not have to be available when searching for the optimal parameter values of a parallel program designed for this architecture. We are not aware of previous approaches to use model checking for auto-tuning programs designed for high-performance systems with modern multi- and many-core processors. Malik and Pena [15] use a custom model checker to compute optimal parameter configuration for multi-variable systems in the automotive industry. This task can be considered similar to auto-tuning, but it does not use the counterexample method that we apply in the present paper.

In this paper, the target area for auto-tuning are parallel programs written in OpenCL [16] which is an open standard approach to programming various modern architectures: multi-core CPU, many-core GPU, FPGA, and others. In order to ensure generality and flexibility of our approach, we assume the abstract platform model of OpenCL as our target architecture, rather than a particular kind of architecture. As our model checking tool, we use the SPIN verifier [17] with its modeling language Promela [18] whose semantics combines the CSP (Communicating Sequential Processes) [19] parallelism and the actor model [20].

We initially proposed our idea of using model checking for auto-tuning in the short, Russian-language paper [21] where we model the Nvidia’s Fermi architecture as an abstract multiprocessor with a warp scheduling for processing elements. The conference paper [22] refines our initial ideas and extends them by developing a first proof-of-concept implementation of auto-tuning for OpenCL programs using the SPIN model checker and conducting first experiments with it. This paper is a substantially rewritten and extended version of [22], with the following major additions: 1) we describe particular details of our approach, in particular we formally define the Promela processes for devices, units and the service clock, and 2) we significantly extend the scope of our experiments in that we describe a particular application of our approach to auto-tuning an OpenCL program for a representative example of computing problems based on reduction, namely, for computing the minimum in integer array.

The structure of this paper and its main contributions are as follows. Section 2 presents the idea of our approach as an adaptation of model checking and the technique of counterexamples to auto-tuning high-performance programs. Section 3 describes the standard platform model of OpenCL and how our abstract model of the OpenCL platform can be represented in the Promela language. Section 4 presents the use of the SPIN model checking tool for auto-tuning, i.e., finding the optimal parameter configuration of an OpenCL program. Section 5 discusses how we can adapt our general auto-tuning approach for the case of limited computation resources. Section 6 reports our extensive experiments with particular OpenCL programs and their results. In Section 7, we apply our model checking based approach to auto-tuning for a program that computes the minimal value in an integer array in parallel, and we compare results of our approach with the real execution of the program. Section 8 concludes our presentation, summarizes our findings, and provides an outline for future research.

Our main idea in adapting model checking to auto-tuning high-performance programs is based on using the general counterexample-guided approach as described, e.g., in [8]. We target multi-threaded programs that transform some input data to output data in a highly parallel manner. The task of auto-tuning such parallel programs is to find the values of performance-critical program parameters (we call them tuning parameters) that enable obtaining the result of the program in the minimum possible time.

We start outlining our approach by formulating a general optimality property as the over-time property $\Phi_{o}$ for the impossibility of program termination within a particular time interval as follows: ‘‘A parallel program cannot terminate within $T$ units of time’’, i.e., the program requires a run time that is longer than $T$. To formalize this property, we can use a temporal logic, such that the over-time property can be formally verified in the model that represents the execution of the parallel program on a particular target architecture, using some model checking tool. If this verification shows that the property is not satisfied, this means that the computation can indeed terminate within the model time $T$. In this case, the model checker constructs a counterexample that describes the conditions under which the program terminates within a model time not greater than $T$, and also the corresponding configuration of tuning parameters that are responsible for the achieved program’s performance. Next, we can gradually approximate the given termination model time $T$ and check the over-time property again and again, until we reach a minimal model time $T_{min}$ of the program: if we decrease this time by only one unit of time, the model checker will prove that the $\Phi_{o}$ property is satisfied, i.e., the program really cannot terminate within $T_{min}-1$ units of time. This way, we find both the minimal model run time of the parallel program and the corresponding values of tuning parameters to achieve this run time; in other words, we have auto-tuned our program.

For implementing this idea of auto-tuning using model checking, we should choose a suitable initial time value $T_{ini}$ and determine a procedure for moving from $T_{ini}$ towards the minimal model run time $T_{min}$. To find a minimal termination model time, we may use, for example, the bisection method shown in Fig. 1: predicate $C_{ex}(T)$ is true iff a model checker generates a counterexample for the model and $\Phi_{o}$ property with time $T$. The initial value of the termination model time $T_{ini}$ can be specified by simulating the program model: usually model checking tools allow for simulating model execution scenarios, such that it is possible to reveal the value of parallel program execution time in any of the scenarios.

Summarizing, our proposed method of using model checking with counterexamples for auto-tuning a parallel program proceeds in four steps, as follows:

1. 1.

   Represent the parallel program with its tuning parameters and target architecture in the language (in our case Promela) of a model checking tool (in our case - SPIN).

2. 2.

   Formulate the over-time property $\Phi_{o}$ for the inability to terminate the program execution within time $T$ in the language of a model checking tool.

3. 3.

   Search for the minimal program termination time $T_{min}$ starting from an initial time $T_{ini}$ provided by a simulation of the model constructed in Step 1.

4. 4.

   Extract information about the optimal configuration of tuning parameters from the counterexample found for the minimal time $T_{min}$.

In this section, we describe how our auto-tuning method outlined in the previous section can be implemented for our particular use case – auto-tuning of OpenCL programs using the formal modeling language Promela and the verification tool SPIN for this language. We target OpenCL, because it covers programming for practically all currently used and emerging parallel architectures, including: universal multi-core processors (CPU), many-core Graphics Processing Units (GPU), FPGA, etc.

This section describes in detail how we implement the four steps of our counterexample-based approach (Section 2) in order to auto-tune OpenCL programs using the model-checking tool SPIN and its language Promela. Our modeling of OpenCL programs execution is based on the standard OpenCL semantics [16].

The OpenCL semantics prescribe that the OpenCL compiler allocates a host (CPU) connected to a device (CPU, GPU, or FPGA) for the execution of an OpenCL program. We assume that the device integrates $m$ units, and the work items of one workgroup are executed on one unit. Each work item in a workgroup is sequentially executed on one processing element of the unit: altogether $2^{mn}$ work items are executed simultaneously, with one instruction performed in one clock cycle. Since the Abstract OpenCL Platform Model does not care about warps (groups of work items for cooperative scheduling in hardware), our Promela model also does not consider warps. Our method can be customized for a particular hardware with its special warp policy by changing the orchestration of processing elements by their unit. Kernel code may contain conditional operators depending on the index of the work item. Without warp scheduling, different branches of such operators are simultaneously executed by the corresponding processing element performing the work item. Work items can use data from both local unit memory and global device memory, but local memory data is not available to the members of other workgroups running on other units.

The key aspect of auto-tuning are the tuning parameters that affect the performance of an OpenCL program. These parameters usually depend on size – the size of the program’s input data; the number of work items also depends on the size of the data. In this paper, we consider the following tuning parameters:

• •

  WG — the workgroup size (defined in the host program). With an optimally selected workgroup size, all processing elements of all units are fully and evenly loaded, which clearly leads to an improvement in the total computation time.

• •

  TS — the tile size (defined in the kernel). The optimal choice of the size of data blocks periodically loaded into the fast local memory minimizes the number of calls to slow global memory, which also leads to faster execution.

There exist practical cases when we may have several tile sizes (e.g., when the computation uses matrices of different size), but different sizes of workgroups are usually not required. Our Promela model for computations chooses tuning parameters in a non-deterministic manner by randomly selecting them in the range depending on the input data size. Obviously, the more non-determinism is in the model (in particular with an increase in the number of tuning parameters), the more resources are necessary to perform the model checking.

Summarizing, our auto-tuning problem is to find the optimal workgroup size WG and tile size TS for the abstract kernel abstract_kernel (Listing 2) and its host program, executed on the Abstract Platform as described in Section 3.1. For this problem, we now describe the particular steps of our Promela-based approach that relies on finding a counterexample, as outlined in Section 2.

The first step is the most time-consuming in our method as it is necessary to take into account all details of executing an abstract parallel OpenCL program on an abstract OpenCL platform. We define the following parallel Promela processes in $Promela$ $Abstract$ $Model$ for modeling this execution:

• •

  initial process main selects the values for the tuning parameters and starts the host and clock processes;

• •

  process host activates several processes device;

• •

  every process device launches its subordinate processes unit;

• •

  every process unit starts processes implementing its processing elements pex and their local memory barrier;

• •

  every process pex performs computations for the abstract_kernel;

• •

  every process barrier locally synchronizes processing elements pex;

• •

  service process clock implements global time counting.

Fig. 4 shows the sequence and communication diagram for these processes. Pairs of processes form master-slave structures: (host, device), (device, unit), (unit, pex), and (unit, barrier). The master starts (run), activates (go) and stops (stop) its slave processes. Slave processes report about termination (done). The processes communicate through handshake channels. In the diagram, we show only one instance for each process. Barrier synchronization is implemented using messages, by waiting for them to be sent by a predefined number of processes. Time is incremented in process clock after the completion of a computation step by all processing elements. Next, we describe our modeling design step-by-step in detail.

In Listing 3, we show how process main selects the values for tuning parameters WG and TS and starts processes host and clock. The number of devices ND, the number of units NU per device, and the number of processing elements NP per unit are global constants declared at the beginning of the model description, as well as factor GMT for the time of computations using the global memory in process pex. In our model, the number of running Promela processes is made up of one main process, one clock, one host, no more than ND devices, no more than NU*ND units, no more than NU*ND barriers, and no more than NU*ND*NP processing elements. We assume for simplicity that data size size is a power of 2. Therefore, the numbers WG and TS are also some random powers of 2. These powers are chosen in lines 14 and 16. Since Promela does not support exponentiation, randomly selected numbers can be obtained by appropriate bitwise shift of size. The number NWD of devices that should be started by the host (lines 14, 16) and the number NWU of units that should be started by every device (line 18) both depend on the number WGs of workgroups. The number NWE of processing elements that should be started by every unit depend on the size WG of a workgroup (line 20). These assignments minimize the number of simultaneously executing processing elements (line 22). In this process, we specify the current value of computation time T (line 23). In line 24, the model of parallel computations starts.

Listing 4 shows process host that activates NWD processes device in lines 6, 8. If the number of workgroups WGs is relatively small then it waits for their termination (line 11) and marks the termination of the target parallel computations in line 23 by variable FIN. Otherwise, this process reactivates the devices until all workgroups are served (line 17).

As an extension of our previous paper [22], we describe here in detail processes device and unit. Process device (Listing 5) starts its NWU instances of process unit in line 4, activate them in line 7 and awaits their termination in lines 11, 15, or 18, depending on the number of workgroups, like the unit process above waits their pexes. If the slave unit does not suppose to be reactivated, then the number of simultaneously working processing elements is decreased (lines 11 and 18). The device also reports about termination to its master – the host process (line 20). After stopping, the device stops all its units (line 22).

The process unit (Listing 6) starts its NWE processing elements pex and their local memory barrier (lines 6-8). Then upon receiving the activating signal from its master device, the unit process activate its pexes (line 11) and then waits termination of their work (line 14). If the size of every work group WG is less then the number NP of slave processing elements of the unit, after receiving reports from all activated pexes, the process unit goes to report about the termination to its master device in line 23. If it is not the case, the unit again activates the just finishing processing elements in line 17 until all all work items in the workgroup have been completed. Upon receiving the stop signal from its device, the unit process stops its barrier and all processing elements (lines 25-26).

Listing 7 shows the local synchronization process barrier: it synchronizes processing elements of one unit using the pex_b and b_pex channels. It receives a message from the pex processes about the suspension of their work and counts in the i variable the number of processes that are waiting for the termination of processing the local memory of other members of the group currently performing calculations (line 4). When it is equal to the number of processing elements NWE launched by its master unit, the barrier is considered passed and in line 5 the the barrier process allows the processing elements to continue computations.

Listing 8 shows in detail the work item process pex that performs computations of an instance of the kernel code abstract_kernel presented in Listing 2. The total number of these processes that are created in the Promela model depends on the size of the input data. The number of simultaneous pex processes depends on the number of units, which is significantly smaller than the total number of processes. Each of them is started by its own unit, whose Promela process is described in [24].

Process pex is connected by the handshake synchronization channels pex_b and b_pex with the local group barrier, and pex_u and u_pex with the master unit. In these channels, the work item receives start and stop commands, and also informs about the termination of computations. In our model, we abstract from the specific computations that the kernel performs, so we only use the computation time. We also assume that a computation in local memory takes one time unit, and a computation using global memory takes GMT units of time. This abstraction can be straightforwardly refined for a particular program and hardware.

Thus, in process pex we model only the number of computational steps performed by the kernel (the for loop in line 15), depending on the size of the input data and calls to global memory (lines 16 and 27) and to local memory (lines 19-23). Upon termination of the computation step, pex reports this event to the process that implements global time by increasing the counter of the currently running NRP_work processes (line 6 of inline macro long_work). Note that due to the blocking semantics of the Promela language, the process can proceed to the next stage of its computation only when the global time time is increased by 1 (line 7 of long_work). The ‘‘long work’’ modeling of computations of the abstract kernel function f, g1, g2 and h finishes after gt*tz time units, depending on the type of memory accessed. Synchronization on the local barrier occurs twice, as in the original kernel: line 10 of the kernel (Listing 2) corresponds to line 17 of the model (Listing 8), and line 17 corresponds to line 24. Process pex terminates (line 28) after writing its result into global memory.

Service clock process clock implements global time counting. This process increments the global time counter variable when all running pex processes (their number allNWE) reports by increasing the NRP_work shared variable that currently they are computing. The clock process stops when the global variable FIN is true. The time value at this moment is the time taken for the computation.

In specializing the over-time property $\Phi_{o}$ for the auto-tuning problem, we use the value of variable FIN that marks the end of calculations, and the final value time. The over-time formula without superindex is used in the model checking approach to general auto-tuning problem, while this formula with superindex ‘$p$’ is specialized for our method which uses Promela model. The SPIN property specification language is temporal logic LTL, such that we can write:

which corresponds to the statement ‘‘Always when the parallel program terminates, its execution time is greater than $T$.’’

The third step of our method finds the minimal time for which a parallel computation program can terminate. This step begins with launching the SPIN verifier with the constructed Promela Abstract Model and the formula $\Phi_{o}^{p}$ for some value of time $T$. We then decrease the value of $T$ until the SPIN stops generating counterexamples, i.e., until it agrees that the program cannot be executed in a time shorter than the final $T$. In our approach, we find the execution path with minimal model time. This path may not be the shortest one due to many model steps which do not increase the value of variable time. We indeed came across such paths in our experiments. The initial value of $T$ can be found using the simulation mode in SPIN. During simulation, SPIN reproduces one of the finite scenarios of the system behaviour, fixing the values of the variables used in the model at the end of the simulation. Therefore, we can use value time which corresponds to the end of the program in the simulated scenario. To decrease the value of $T$ in the next SPIN runs, we may use the bisection method shown in Fig. 1. The final counterexample gives the minimal model time value.

The final step of our approach is to analyze the last counterexample to extract the optimal configuration of tuning parameters. For counterexample analysis, SPIN provides running a simulation corresponding to the counterexample. In the auto-tuning problem, there is no need to search for the optimal computation path. Therefore, there is not necessary to analyze the transitions of the final counterexample. To solve our problem, we only need to extract the values of the tuning parameters WG and TS, which are known in the final counterexample simulation. The final values of the tuning parameters WG and TS form the optimal parameter configuration we are looking for.

As our solution requires a large number of interactions through channels, its straightforward implementation does not scale well: with an increase in the size of the input data, the memory required for the verification process in Step 3 begins to grow and may exceed the available physical memory of the computer, which we sometimes observed in our experiments.

We address the problem of limited resources by using the swarm model checking method proposed in [25, 26]. This method uses state hashes and therefore does not visit all possible states of the system. The swarm model checking starts several different verification tests checking the specified property during bounded time and with a bounded number of model steps. Similar to the standard model checking method, it generates counterexamples when one of the paths violates the property. The search of such a path can be parallelized across processor cores and even performed on different network nodes. In [27], we already applied this approach to the automatic solution of various puzzles and practical problems.

In order to use swarm model checking for alternative non-bisection searching, we can formulate the non-termination property $\Phi_{t}$ for the impossibility of program termination as follows: ‘‘A parallel program cannot terminate’’ (LTL formula $\Phi_{t}=\textbf{G}(\neg\texttt{FIN})$). We definitely know that our parallel programs that compute some output data must terminate. Hence, we expect that there is at least one counterexample which demonstrates that the program terminates and provides the termination model time. Swarm model checking produces several termination model times from several counterexamples, from which we can choose the minimal termination model time. To be sure that there is no smaller time, we launch successively swarm model checking with a decreasing model time and over-time property $\Phi_{o}^{p}$ in the following manner: we stop searching for the minimal termination model time if swarming with the current model time provides no results within the previous swarm execution time or this swarming finds no smaller times. In other words, the criterion for stopping the search for the optimal time is the ability of the SPIN swarm to find counterexamples, rather than the number of such findings. If the swarm does not find a counterexample as quickly as at the previous swarm launching, the counterexample with a smaller time value does not exist with very high probability. In future work, we plan to formally prove that the configuration of tuning parameters found by the swarm is indeed optimal.

Our algorithm in Figure 5 implements the described search strategy with two functions: Min_time_Swarm(F) and Exe_time_Swarm(F) for the minimal model time found by the swarm for formula F and the execution time of this swarm, respectively. Predicate Swarm(F,exe_time) is true iff the swarming formula F finishes within exe_time. Formula F_t is for the non-termination property, and formula F_o(T) is for the over-time property with time T.

In our implementation, we have developed a script that simulates each counterexample found by the swarm and finds values of time, TS and WG in the output. We also provide a simple program which, after the script has finished, sorts these counterexample results by time values with corresponding tuning parameters TS and WG.

We make an assumption (which corresponds to the situation in practice) that every device and every unit of a device work in exactly the same manner, i.e., it takes exactly the same time (and other resources) to perform computation of the same complexity. Hence, to estimate the computation time, we can abstract from the number of devices and the number of units in these devices and consider just one device and one unit with all its processing elements. Note that we cannot consider just one processing element because, in general, they compute different functions of different complexity depending on their local identifiers while the devices and units synchronize their work independently of the computation complexity. With this abstraction, the number of Promela processes is made up of one main process, one clock, one host, one device, one unit, one barrier and several processing elements. In the model used in our experiments [24], the total number of Promela processes is 10. Here, the only really large parameter is the input data size.

In Table 1 we show the results of a series of experiments conducted with the SPIN model checker (version 6.5.1). During the tests, we studied different sizes of input data for a platform architecture with the following parameters: one device, one unit and four processing elements.

We observe in the table of results that, up to input data size 32, exhaustive verification with over-time formula $\Phi_{o}^{p}$ was possible for our machine (an M1-based MacBook with 16Gb of RAM).

This auto-tuning finds optimal values of parameters with the shortest simulation time (parameter which is also calculated in our model). For reference, we include model steps, shown in SPIN simulation mode for the best counterexample. When the data size is significantly larger, we may hit the 16 GB memory threshold. Therefore, we run the swarm verification with non-termination formula $\Phi_{t}$ on 1-8 cores for given maximum verification time threshold, and the swarm process is now able to find a large number of counterexamples with trails to the final state FIN for larger data sizes. We also developed a runner script to process all the trails found by SPIN. It simulates a particular trail, obtains the simulation time and TS/WG parameters from the simulation output, sorts them by time and required steps. Using such a script finally helps to obtain the minimal time and optimal parameters from a bunch of trails. Getting multiple trails is possible due to -e parameter (create trails for all errors) during the verification and swarm run. We also had to increase maximum search depth depending on the input size with the last one set to $2\times 10^{8}$ by option -m.

In Table 1, ‘‘Model time’’ is the time that is calculated in the Promela model (variable time), and ‘‘Verification time’’ is the time spent by the SPIN verifier or its swarm processes. In the last two columns of the table, we show the time required to obtain the first counterexample with a trail – the quickest sub-optimal solution of the problem (both using exhaustive and swarm methods) and its optimality as the ratio of the optimal solution modeling time to the time of the first counterexample (if the times coincide, we also take into account the number of steps spent).

Therefore, we can conclude that our method is feasible in practice: for small dimensions, we can prove that our interacting system terminates in the correct order. Once we hit the memory limits in the model checker, we can use the swarm method and get the approximate model time and target parameters with a full trace of execution after a series of quick model runs. Of course, this method is not yet applicable for modeling operations with really big data. However, we initially set ourselves goals to consider modeling with an abstraction from operations and data, since we are primarily interested in the sequence of their processing.

In this section, we demonstrate how our approach to auto-tuning based on model checking works for a particular application use case. Our use case is the problem of computing the minimal value in a very big integer array, we call it the Minimum problem.

We offer an OpenCL kernel program for the Minimum problem, run and tune parameters for it using Nvidia GPU P104-100 of the Pascal architecture. Then we show how the general Promela model defined in Section 4 can be modified to model a particular case of this parallel computation problem. Ultimately, we apply our method of counterexamples and thereby find the optimal tuning parameters for the Minimum problem.

The long-term goal of our research is the development of rigorous, formally-based methods for auto-tuning high-performance parallel programs by relying on the model checking approach, in particular using the technique of counterexample-guided search. The results of auto-tuning are the optimal values of tuning parameters that ensure the best possible performance of the given program on a particular parallel architecture for a particular input data size. As our current target, we address high-performance programs written in OpenCL which is an emerging open standard for programming various kinds of parallel architectures, including multi-core CPU, GPU, and FPGA. Our approach described in this paper is based on developing an abstract model of OpenCL computations and then expressing the model of program execution and optimality properties in the formal language Promela, such this model can be investigated by the popular model checking tool SPIN.

The main advantage of our logic-based approach to auto-tuning high-performance programs is that is can be applied without involving the particular target execution platform. Other than the existing auto-tuners, our simulation of the execution of OpenCL programs in Promela abstracts from specific computations, keeping the logic of interaction and synchronization of parallel program processes in the target parallel architecture. Due to the formal semantics of the Promela language, the model of a given OpenCL program can be viewed as the formal operational semantics of interaction and synchronization of parallel program processes on a selected platform and device architecture. By varying the parameters and algorithms of interaction between the components of an abstract device, it is possible to define and study specific processor architectures. This makes it possible to search for optimal program settings in the absence of real target processors, while existing auto-tuning frameworks cannot provide such an opportunity.

We plan to further improve our approach by customizing our general auto-tuning method for a specific application program executed on a specific hardware, in addition to computing the minimum on the Nvidia P104-100 processor. In particular, we are going to conduct a case study with matrix multiplication on the most recent Ampere GPU architecture by Nvidia Corp. Knowing the particular specification, for example of the Ampere architecture, we can customize the ratio of the global memory access time to the local memory access time, and the performance time for every function used in the program by considering all primitive operations in the function. We will also take into account specific organisation of communication in the architecture, for example between Ampere units and their processing elements.

In our future work, we will also add the communication time between processes to the model, as well as consider other settings, in particular, the number of work items. In addition, to improve our counterexample method, we are going to try using the never claim pruning from [30], and finding optimal values from [11], which avoids multiple runs of the SPIN verifier in the counterexample method. We also plan to improve the scalability of our counterexample method by modeling a warp-based scheduling [31], because due to warping, the number of simultaneously working processing elements becomes smaller, which implies reduction of interleaving non-determinism in the model. Finally, we will work on scaling up our approach to much larger sizes of input data.

We are grateful to the anonymous referees of the LOPSTR’22 symposium for their great help in improving the initial, shorter version [22] of this paper.