This shows you the differences between two versions of the page.
polymodel_verifier [2014/05/30 11:49] |
polymodel_verifier [2014/05/30 11:49] (current) |
||
---|---|---|---|
Line 1: | Line 1: | ||
+ | ======Verifier===== | ||
+ | |||
+ | ===Bundle Setup=== | ||
+ | I have prepared a bundle including Eclipse itself:\\ | ||
+ | http:// | ||
+ | The bundle is based on Eclipse Classic 3.7.1. | ||
+ | |||
+ | The above bundle contains all necessary plug-ins to use the following project:\\ | ||
+ | http:// | ||
+ | |||
+ | This verifier.IF.ada project contains examples to use the verifier. For trying out the verifier, I suggest that you download the bundle, and the above archived project, and then import the tar from '' | ||
+ | The examples are from our ompVerify paper (http:// | ||
+ | |||
+ | http:// | ||
+ | |||
+ | This is a jar file for the verifier. If run as a stand alone jar file, it verifies the legality of parallelization of some of the example programs. | ||
+ | When used as a library, please specify the program representation according to the textual interface specified at the bottom of this page and call VerifierExample.verify | ||
+ | |||
+ | ===Source Access=== | ||
+ | The following plug-ins are installed as jar files under dropins directory in the above bundle. | ||
+ | Sources to these projects are available in the GeCoS repository. | ||
+ | Please follow the instructions in this website (https:// | ||
+ | All plug-ins are located under trunk/ | ||
+ | |||
+ | * fr.irisa.cairn.eclipse.tom | ||
+ | * fr.irisa.cairn.jnimap.isl | ||
+ | * fr.irisa.cairn.model.integerlinearalgebra | ||
+ | * fr.irisa.cairn.model.polymodel | ||
+ | * fr.irisa.cairn.model.polymodel.ada | ||
+ | * fr.irisa.cairn.model.polymodel.isl | ||
+ | * fr.irisa.cairn.model.polymodel.prdg | ||
+ | * org.polymodel.verifier | ||
+ | |||
+ | ===Additional Plug-ins=== | ||
+ | The following plug-ins are required to use the verifier. | ||
+ | |||
+ | * EMF - Eclipse Modeling Framework SDK (2.7.1) | ||
+ | * From Indigo update site under Modeling cateogry | ||
+ | * Xtext Antlr Runtime Feature (2.0.0) | ||
+ | * From itemis update site (http:// | ||
+ | |||
+ | The bundle also contains subclipse for SVN access. | ||
+ | |||
+ | ===Using the Verifier=== | ||
+ | The provided interface takes the following information for each statement in a polyhedral region to verify: | ||
+ | * Polyhedral domain | ||
+ | * Schedule (as affine functions) | ||
+ | * Write access | ||
+ | * Set of read accesses | ||
+ | * Annotation for each dimension of the schedule specifying the type of the dimension. | ||
+ | |||
+ | The output of the verifier is an instance of VerifierOutput object, containing a flag to tell if the program was valid, and a list of messages from the verifier listing violations found in the program. The messages should contain sufficient information to give feedback to the user. | ||
+ | |||
+ | These input can easily be extracted from affine control loops (example later), and array dataflow analysis is performed using the provided information and then the resulting polyhedral reduced dependence graph (PRDG) is verified. | ||
+ | |||
+ | ===ISLSet and ISLMap=== | ||
+ | The verifier uses Integer Set Libarary (http:// | ||
+ | * ISLSets | ||
+ | '' | ||
+ | where the constraints are delimited by any of one '&', | ||
+ | * ISLMaps | ||
+ | '' | ||
+ | where the expressions are delimited by ',' | ||
+ | |||
+ | Note that ISL accepts much more general syntax than shown above, since ISLMaps are relations, and not functions, but the above is sufficient to express inputs to the verifier. | ||
+ | |||
+ | ===Example=== | ||
+ | The example is for C programs with OpenMP. The verifier is applicable for other programming languages with parallel constructs that can be viewed as '' | ||
+ | In case of X10, if the only statement in the body of a loop is '' | ||
+ | <code C> | ||
+ | void matrix_multiply(int** A, int** B, int** C, int N) { | ||
+ | int i,j,k; | ||
+ | |||
+ | #pragma omp parallel for | ||
+ | for (i = 0; i < N; i++) { | ||
+ | for (j = 0; j < N; j++) { | ||
+ | C[i][j] = 0; //S0 | ||
+ | for (k = 0; k < N; k++) { | ||
+ | C[i][j] += A[i][k] * B[k][j]; //S1 | ||
+ | } | ||
+ | } | ||
+ | } | ||
+ | } | ||
+ | </ | ||
+ | ==Statement Domains== | ||
+ | Each statement is surrounded by a set of loops with affine bounds. The polyhedral domain for each statement is simply the intersection of all loop bounds that surrounds a statement. There may be a '' | ||
+ | |||
+ | For the above matrix multiply, '' | ||
+ | * '' | ||
+ | * '' | ||
+ | |||
+ | ==Schedule== | ||
+ | The input schedule given to the verifier is the sequential schedule, treating '' | ||
+ | '' | ||
+ | The schedule is used to characterize the relative placement of the statements. In addition, we require that all statements are mapped to a common dimensional space via scheduling specification. | ||
+ | |||
+ | Although this is not a requirement, | ||
+ | For a loop with maximum depth '' | ||
+ | |||
+ | For the above matrix multiply, the schedules are: | ||
+ | * '' | ||
+ | * '' | ||
+ | |||
+ | Note that the 5th dimension is 0 for '' | ||
+ | |||
+ | ==Accesses== | ||
+ | Both reads and writes are specified as a pair of variable name and access function. | ||
+ | Variable names corresponds to the arrays read/ | ||
+ | The access functions are expressed as affine functions from the corresponding statement domains. | ||
+ | |||
+ | For the above example, '' | ||
+ | * Write '' | ||
+ | '' | ||
+ | * Write '' | ||
+ | * Read '' | ||
+ | * Read '' | ||
+ | * Read '' | ||
+ | |||
+ | ==Dimension Types== | ||
+ | One last piece of information given to the verifier is the annotation on each dimension of the schedule. | ||
+ | There are three types of dimensions: | ||
+ | * SEQUENTIAL : This dimension should be interpreted as time steps | ||
+ | * PARALLEL | ||
+ | * ORDERING | ||
+ | |||
+ | The parallel dimensions corresponds to loops that are parallelized by OpenMP '' | ||
+ | |||
+ | ==private clause in OpenMP== | ||
+ | When variables are declared as private in OpenMP, the variable is private to each iteration of the parallel loop. | ||
+ | Therefore, it is expressed by adding additional dimensions to the memory accesses, indexed by the loop iterator of the parallel loop, so that each iteration of the parallel loop access different memory location. | ||
+ | |||
+ | In other words, the following code: | ||
+ | <code cpp> | ||
+ | #pragma omp parallel for private(c) | ||
+ | for (i=0; i < N i++) | ||
+ | c += ... | ||
+ | </ | ||
+ | is translated as: | ||
+ | <code cpp> | ||
+ | #pragma omp parallel for | ||
+ | for (i=0; i < N i++) | ||
+ | c[i] += ... | ||
+ | </ | ||
+ | during verification. | ||
+ | |||
+ | |||
+ | ===Interface=== | ||
+ | |||
+ | ==Textual== | ||
+ | The following code is a possible interface based on arrays of Strings for testing purposes. | ||
+ | <code JAVA> | ||
+ | private static void matrix_multiply() { | ||
+ | |||
+ | String[][] statements = new String[][] { | ||
+ | new String[] {" | ||
+ | " | ||
+ | new String[] {" | ||
+ | " | ||
+ | }; | ||
+ | String[][] reads = new String[][] { | ||
+ | new String[] {" | ||
+ | new String[] {" | ||
+ | new String[] {" | ||
+ | }; | ||
+ | String[][] writes = new String[][] { | ||
+ | new String[] {" | ||
+ | new String[] {" | ||
+ | }; | ||
+ | String[][] dims = new String[][] { | ||
+ | //Legal 1D parallelization | ||
+ | new String[] {" | ||
+ | new String[] {" | ||
+ | |||
+ | //illegal parallelization of k dimension | ||
+ | //new String[] {" | ||
+ | //new String[] {" | ||
+ | }; | ||
+ | |||
+ | VerifierExample.verify(statements, | ||
+ | } | ||
+ | </ | ||
+ | |||
+ | ==Generic Interface== | ||
+ | For a more general interface, the user must construct the following data structure, called '' | ||
+ | In addition a map, Map< | ||
+ | |||
+ | '' | ||
+ | |||
+ | < | ||
+ | | ||
+ | |------variables | ||
+ | |------statements : List< | ||
+ | |||
+ | | ||
+ | |------ID | ||
+ | |------domain | ||
+ | |------schedule : AffineMapping | ||
+ | |------write | ||
+ | |------reads | ||
+ | |||
+ | | ||
+ | |-----variable | ||
+ | |-----accessFunction : AffineMapping | ||
+ | |||
+ | | ||
+ | |-----name : String | ||
+ | |||
+ | | ||
+ | | ||
+ | </ | ||
+ | |||
+ | |||
+ | '' | ||
+ | Once these two data structures are ready, the following two lines will invoke the verifier. | ||
+ | <code java> | ||
+ | VerifierInput input = VerifierInput.build(adaInput, | ||
+ | VerifierOutput output = Verifier.verify(ISLDefaultFactory.INSTANCE, | ||
+ | </ | ||
+ | |||