A Quick Introduction to Functional Verification of Array-Intensive Programs

TL;DR

This paper reviews key literature on verifying the functional correctness of array-intensive programs, crucial for ensuring optimized parallelized code remains correct.

Contribution

It provides a comprehensive overview of existing methods for functional verification in array-intensive program optimization.

Findings

Highlights importance of verification in parallelization

Summarizes verification techniques for array programs

Serves as a starting point for researchers in the field

Abstract

Array-intensive programs are often amenable to parallelization across many cores on a single machine as well as scaling across multiple machines and hence are well explored, especially in the domain of high-performance computing. These programs typically undergo loop transformations and arithmetic transformations in addition to parallelizing transformations. Although a lot of effort has been invested in improving parallelizing compilers, experienced programmers still resort to hand-optimized transformations which is typically followed by careful tuning of the transformed program to finally obtain the optimized program. Therefore, it is critical to verify that the functional correctness of an original sequential program is not sacrificed during the process of optimization. In this paper, we cover important literature on functional verification of array-intensive programs which we believe can be a good starting point for one interested in this field.

Tables

Table 1. TABLE I: A comparison among different methods based on transformations supported

Lit	Need hint	Loop	Recur	Arith	Vector	Parallel
[56]	$✓$	$✓$	$\times$	$\times$	$\times$	$\times$
[57]	$✓$	$✓$	$\times$	$\times$	$\times$	$\times$
[66]	$\times$	$✓$	$\times$	$\times$	$\times$	$\times$
[60, 59, 61]	$\times$	$✓$	$\times$	Linear	$\times$	$\times$
[81]	$\times$	$✓$	$✓$	$\times$	$\times$	$\times$
[70]	$\times$	$✓$	$\times$	$✓$	$\times$	$\times$
[74]	$\times$	$✓$	$✓$	$✓$	$\times$	$\times$
[77]	$\times$	$✓$	$✓$	$✓$	$\times$	$✓$
[80]	$\times$	$✓$	$✓$	$\times$	$✓$	$✓$

Full text

I Introduction

Recent days have seen a boost in high-performance computing due to the introduction of high performant GPUs and specially designed coprocessors, such as Xeon Phi. The primary workloads which have benefited from these new hardware are the array-intensive programs (also known as dataflow programs). These programs are amenable to parallelization and various application programming interfaces (APIs) exist which help in exploiting the many cores available nowadays on a machine, such as OpenMP [1] and OpenACC [2], and also to parallelize across multiple machines, such as MPI [3] and OpenCL [4]. However, although a lot of research has gone into improving parallelizing compilers [5, 6], these compilers are still not popular among experienced programmers who prefer applying hand-crafted transformations to a sequential program, followed by a tuning phase of the transformed program which finally results in an optimally performing program. In such a case, it is even more crucial to verify if the parallelizing transformation along with other optimizations, like loop transformations and arithmetic transformations, preserve the semantic equivalence of the sequential code. In this paper, we present a short survey of the significant work done in the field of functional verification of array-intensive programs.

Additionally, it is important to note that customized hardware has received a lot of attention recently due to the rapid proliferation of deep learning – be it coarse-grained reconfigurable architecture (CGRA) [7, 8], FPGA [9] or systolic array [10]. A lot of compiler frameworks have also come up to provide support for the heterogeneous architecture that may be used to train the neural networks, for example, Google’s Tensorflow XLA [11], Amazon endorsed NNVM [12] and Facebook’s Glow [13]. New programming methodologies are also being proposed to further boost programmer productivity by exploiting underlying architecture with minimal programming overhead; the work reported in [14], for instance, introduces an abstraction layer in the program called T2S (temporal to spatial) which takes a temporal definition (basically, the function to be computed) and generates its spatial mapping (i.e., decompose the specified function and map the decomposed pieces onto a spatial architecture, e.g., CGRA or FPGA). There is always a possibility that the compiler, e.g. [11, 12, 13], may have an implementation bug or the specification provided, say in T2S [14], has some inherent logical mistake because of which the prescribed functionality cannot be efficiently mapped to a given FPGA. We found that literature on verification of specifically tailored transformations for mapping neural networks onto heterogeneous architecture (which primarily consists of the transformations discussed in this paper) is still at a nascent stage. In particular, the work reported in [15] offloads the onus of compiler transformation verification by translating its internal representation (IR) to the well-known LLVM [16] IR and then leveraging existing verification techniques for LLVM compiler. Therefore, we believe that our paper should also appeal to those who are interested in designing and/or verifying compiler transformations directed towards deep learning applications or artificial intelligence, in general.

The rest of the paper is organized as follows. Section II illustrates the benefits of applying loop transformations and arithmetic transformations to array-intensive programs. Section III covers the various significant work done for verifying such programs with the help of an example. Section IV concludes the paper.

II Optimizing transformations

II-A Applications of loop transformations

Multimedia and signal processing applications have witnessed extensive application of loop transformations and arithmetic transformations. In the following, we study several applications of loop transformations techniques during (embedded) software design.

The effects of loop transformations on system power has been studied extensively. The work reported in [17] underlines the effect of loop fusion, loop fission, loop unrolling, loop tiling, and scalar expansion on energy consumption. The futility of applying conventional data locality oriented code transformations for minimizing disk power consumption has been showcased in [18]. As a remedy, the authors of [18] suggest how both code restructuring and data locality optimization should be taken into consideration for designing a disk layout aware application optimization strategy. Specifically, the authors focus on three optimizations – loop fusion/fission, loop tiling and linear optimizations – for code restructuring and advocate a unified optimizer that targets disk power management by applying these transformations. In [19], the authors focus on an MPSoC architecture with a banked memory system. For this architecture, they demonstrate how code and data optimizations assist in reducing memory energy consumption for embedded applications with regular data access patterns. The work in [20] achieves minimization of the data memory requirements of processors by using a memory-conscious loop parallelization strategy. A data space-oriented tiling (DST) approach is proposed in [21] whereby the data space is logically divided into chunks called data tiles. DST has the potentiality to achieve better results than conventional loop tiling because it exploits inter-nest data locality since the data space is common across all loop nests that access it. A global approach to tackle data locality problem is prescribed in [22] which evaluates all the loop nests in an application to be run in an embedded MPSoC simultaneously and schedules the different constituent modules accordingly for parallel execution. In the context of an embedded chip multiprocessor, the method described in [23] underlines how reliability against transient errors can be enhanced without sacrificing execution time by replicating some of the operations being executed on active processors onto (otherwise) idle processors.

Loop transformations have found application in the design of system memory as well. For example, the authors of [24] explain a method in the context of multimedia applications running on MPSoCs that can reduce cache misses and also cache size. Specifically, loop fusion and loop tiling are employed to minimize cache misses, whereas a novel buffer allocation strategy is used to reduce cache size. This work is extended in [25] to handle dependence-free arrays additionally. Here an input-conscious tiling scheme for off-chip memory access optimization is proposed. The authors showcase that the input arrays play an as important role as the arrays with data dependencies when the objective is memory access optimization instead of parallelism extraction. Data reuse is a key process that may potentially reduce external memory access by exploiting the memory hierarchy. Loop transformations for data locality and memory hierarchy allocation are important procedures in the optimization flow for data reuse. A global approach that provides optimal results on external memory bandwidth and on-chip data reuse buffer size by combining loop transformations and memory hierarchy allocation can be found in [26]. An extension of this work is presented in [27] that optimizes on-chip memory allocation by loop transformations in the imperfectly nested loops. A dynamic loop tiling strategy is proposed in [28, 29] to enhance cache locality and obtain coarse-grained parallelism.

In [30], the authors undertake the challenge of reducing the total energy while maintaining the performance requirements for application with multi-dimensional nested loops. They have demonstrated that an adaptive loop parallelization strategy along with idle processor shut down and pre-activation can be critical in minimizing energy consumption without increasing execution time. The objective of the paper [31] is also the same as that of [30]. However, they apply loop fusion and multi-functional unit scheduling techniques to achieve that.

Loops containing nested conditional blocks can pose serious challenge to compilers while producing optimized code. This problem is tackled in [32]. This work statically analyzes the Boolean conditions appearing at branching states in the control flow of a program using a novel interval analysis technique. The outputs of interval analysis integrated with those of loop dependency are used to segregate the iteration space of the nested loops.

A survey on application of loop transformations in data and memory optimization in embedded system can be found in [33], whereas the benefits of these transformations outlined in [34] are targeted for a more general software design. For details on some of the pioneering work on program transformations targeting reduction of energy consumption in dataflow programs, one may refer to [35, 36]. Another work [37] tries to reduce the use of temporary arrays, which may eventually result in better register usage, by using loop fusion technique in multimedia applications before hardware/software partitioning is carried out. Loop transformations have also been applied to improve performance in coarse-grained reconfigurable architecture [38]. Applications of loop transformations to parallelize sequential code targeting embedded multi-core systems are given in [39, 40]. Interested readers are encouraged to look into [41, 42, 43, 44, 45] for several other loop transformation techniques and their effects on system design.

II-B Applications of arithmetic transformations

Compiler optimizations often involve several arithmetic transformations based on algebraic properties of the operator such as associativity, commutativity and distributivity, arithmetic expression simplification, constant folding, common sub-expression elimination, renaming, dead code elimination, copy propagation and operator strength reduction, etc. For example, the work [46] demonstrates how applying retiming, algebraic and redundancy manipulation transformations can drastically improve the performance of embedded systems. The authors of [47] investigate source-to-source algebraic transformations which aid in decreasing the execution time of expression evaluation; its benefit on performance has been recorded on many computationally intensive applications. They, basically, propose two algorithms based on factorization and multiply-add extraction heuristics to replace traditional associative commutative pattern-matching techniques. Another method that minimizes operation cost based on loop-invariant code motion and operator strength reduction is reported in [48]. An in-depth experimental analysis on the effectiveness of such source-level transformations at the level of number of execution cycles, before and after applying the optimizations, is given in [48] for two real-life multimedia application kernels. Application of algebraic transformations to minimize critical path length in the domain of computationally intensive applications is proposed in [49]. Apart from standard algebraic transformations such as commutativity, associativity and distributivity, they also introduce two hardware related transformations based on operator strength reduction and constant unfolding. A set of transformations such as common sub-expression elimination, renaming, dead code elimination and copy propagation are applied along with code motion transformations in the pre-synthesis and scheduling phase of high-level synthesis in the SPARK tool [50, 51]. The potential of arithmetic transformations on FPGAs is studied in [52]. It has been shown that operator strength reduction and storage reuse reduce the area of the circuit and hence the power consumption in FPGA. The transformations like height reduction and variable renaming reduce the total number of clock cycles required to execute the programs in FPGAs, whereas expression splitting and resource sharing reduce the clock period of the circuits.

III Verification of optimizing transformations

Let us consider the two functions shown in Figure 1. The function shown in Figure 1(b) has been obtained from that of Figure 1(a) by applying the following transformations.

Application of loop transformation: The for loop in program1 has been split into two (an instance of loop fission).

Application of arithmetic transformations: The statements S0 and S1 in program1 have been merged into one statement T0 in program2 – it is regarded as a linear arithmetic transformation. Moreover, distributive property of multiplication over addition has been applied to reduce the number of temporary array variables from two (I1 and I2) to one (I) – it is regarded as a non-linear arithmetic transformation because it involves multiplication of two array variables.

Application of parallelizing transformations: OpenMP directives have been introduced in program2 to make the execution of its for loops parallel.

Also note that the functions contain recurrence because the array C is defined in terms of previously defined elements of the same array. Now let us go through the various methods reported in literature for verifying these individual transformations or some combination of these.

Verification of loop transformations on array-intensive programs is a well studied problem. Some of these target transformation specific verification rules. The techniques reported in [53, 54], for example, proposed permutation rules for verifying loop tiling, loop reversal, loop skewing, loop interchange transformations in their translation validation approach. The rule set is further enhanced in [55, 56]. The primary issue with this approach is that the method had to rely on the hint provided by the compiler. The verifier needs the list of transformations that have been applied and the order in which they have been applied from the synthesis tool. Also, completeness of the verifier depends on the completeness of the rule set and therefore enhancement of the repository of transformations necessitates enhancement of the rule set.

The concept of fractal symbolic analysis is introduced in [57]. The idea is to reduce the gap between the source and the transformed programs by applying simplification rules repeatedly until the two programs become similar enough to allow a proof by symbolic analysis. The rules are similar to the ones proposed by [53, 54]. This method combines some of the power of symbolic analysis with the tractability of dependence analysis. The applicability of this technique again depends on the robustness of the provided rule set.

The design of a fully automatic verifier for loop transformations can be found in [58]. Preservation of data dependencies between the original and the transformed programs at a statement-level forms the central idea in this work. This method, however, does not have provision to handle arithmetic transformations. Since it is common that the arithmetic transformations and the loop transformations are applied together, direct correspondence between the statement classes of the original and the transformed programs does not always hold as necessitated by [58].

Off-the-shelf SMT solvers, such as CVC4 [59], Yices [60], or theorem provers, such as ACL2 [61], have also been demonstrated to verify loop transformations and arithmetic transformations [62]. It is more or less straightforward to model the equivalence of two programs with a formula. The validity of the formula can be checked by a SMT solver or theorem prover [62]; if the formula is found to be valid then the two programs are indeed equivalent. It is to be noted that although the SMT solvers and the theorem prover can be effective in handling linear arithmetic, presence of non-linear arithmetic often makes these tools falter in proving the equivalence; in such scenarios, these tools either output “unknown” indicating that they failed to prove either equivalence or non-equivalence of the programs or they time out without producing an output. It has been shown in[62] that state-of-the-art SMT solvers failed to verify most of the loop transformations and arithmetic transformations.

The method developed in [63, 64, 65, 66] assesses a restricted class of programs with affine indices and bounds, static control flow, single assignment form and valid schedule. This method presents a translation validation algorithm for verifying loop transformations, where the source and the transformed programs are modeled as Array Data Dependence Graphs (ADDGs). This method is promising since it is capable of handling most loop transformations without requiring any additional information from the compilers (or human expert). The primary limitations of this ADDG based verification technique are its inability to handle recurrences and arithmetic transformations. The ADDG based method is extended in two directions initially. In one direction, Verdoolaege et al. in [67, 68] enhanced the method to handle recurrences in programs. In another direction, Karfa et al. [69, 70] enhanced it to handle arithmetic transformations.

Specifically, in [67, 68], the authors have modelled the programs as dependence graphs (DGs). Before delving into its details, note that a recurrence involves induction case(s), e.g. statement T2 in Figure 1(b), whereby the members of an array is defined in terms of previously defined members of itself, and basis case(s), e.g. statement T1 in Figure 1(b). Typically, proving the basis cases in the DGs obtained from the original and the transformed programs is straightforward involving symbolic substitution of the temporary arrays by input arrays. However, proving equivalence between the induction cases can be convoluted and hence this verification procedure takes an optimistic approach and initially considers that the induction cases in the two DGs are possibly equivalent and proceeds in a forward pass (using an operation called widening); the proof obligations that remain pending during the forward pass are tried to be resolved during a backward pass (using an inverse operation called narrowing). This two pass approach adopted in [67, 68] is found to be effective to handle a wide range of programs containing recurrences. In fact, this method has been proved to be successful in verying realistic multimedia systems in [71].

In other direction, a slice-level equivalence of ADDGs is proposed in [69, 70] (as opposed to path-level equivalence of [65, 66]), to handle arithmetic transformations such as, constant unfolding, common sub-expression elimination, distributive transformations, arithmetic expression simplification, etc., along with loop transformations. This method additionally incorporates a normalization technique [72] extended suitably to represent data transformations. It has also been adopted in checking correctness of transformations on the Kahn process networks (KPNs) for multimedia and signal processing applications [73]. Handling recurrences, however, remains as the main limitation of this technique. Recurrences create cycles in the ADDG representation of a program. In the presence of loops in an ADDG, obtaining the closed-form representations of the data dependence is hard. The work reported in [74], for the first time, proposes a unified method to verify loop and arithmetic transformation as well as recurrence. In [74], the verifier first identifies cyclic subgraphs in the ADDGs (arising from recurrences), then for each cyclic subgraph in the original ADDG, it tries to find an equivalent cyclic subgraph in the transformed ADDG; if one-to-one correspondence is found for all the cyclic subgraphs in the two ADDGs, then the entire ADDGs, with the cyclic subgraphs replaced by some uninterpreted functions (and thus reduced to cycle-free ADDGs), are compared in an identical way as mentioned in [70].

None of the above methods, however, handle parallelizing transformations and loop vectorization. An early work [75] proposes a static checker for analysis of a number of thread synchronization issues. Another work [76] proposes a similar approach for synthesizing synchronization implementation from a high level specification. However, the methods described in [75, 76] do not explicitly target loop transformations and cannot handle arithmetic transformations at all. The method of [74] was extended in [77] to handle data races which may arise on introducing parallelizing transformations. In [77], the authors model the programs as coloured-ADDGs. Specifically, nodes with different colours are maintained to capture the different parallelized regions of the program and if some thread originating in some coloured region of the program is found to be able to enter a differently coloured region of the program (signifying that no synchronization barrier exists between these two regions), then the method declares that parallelized program as unsafe because data race exists in that program. In [78], a method is proposed to detect if a loop can be parallelized or not. The authors have used seperation logic to detect that. In addition, the method also identifies the synchronization points which is required for parallel programs. Dutta et. al  [79, 80] has extended the work of Verdoolaege et. al. in [67, 68] for verification of loop vectorization and loop parallelization transformations. Specifically, they have shown how to construct a DG from the loop vectorized and the loop parallelized programs. The proposed work then applies the DG based method proposed in [67, 68] to check the equivalence. They have also enhanced the method proposed in [67, 68] to handle loop collapsing transformation.

IV Conclusion

Table I provides a list of the pros and cons of several key literature mentioned here. It is worth noting that while supporting as many transformations as possible is a desired property for a method, needing hints from the compiler to do so is typically considered to be undesirable because it requires explicit instrumentation for each compiler (synthesizing tool); moreover, a human expert may not always document one’s intuition for applying a transformation methodically. Although  [74] tries to bridge the gap between handling recurrences and arithmetic transformations, the treatment of recurrence in [67, 68] is more robust, for example, the method of [68] can additionally handle cases of mutual recurrence (also known as, co-induction). The arithmetic transformations are elegantly handled in [69, 70]. Therefore, it would be an interesting future work to apply the normalization techniques proposed in [69, 70] on the DG based method proposed in [67, 68] to handle both recurrence and arithmetic transformations elegantly. In addition, the work presented in [79, 80] can be used prior to this method to handle loop vectorization and loop parallelization transformations. We further envision that the verification techniques discussed here are also effective in verifying transformations applied by compilers targeting deep learning applications.