ProgramAnalysis - Maple Programming Help

Online Help

All Products    Maple    MapleSim


Home : Support : Online Help : System : Information : Updates : Maple 2016 : updates/Maple2016/ProgramAnalysis

ProgramAnalysis

The ProgramAnalysis package is a new subpackage of the CodeTools package.  There are commands to analyze the data dependencies in for loops and to verify the correctness of while loops.

 

withCodeToolsProgramAnalysis

CreateLoop,DependenceCone,GenerateProcedure,IsLoopInvariant,IterationSpace,LoopInvariant,TrajectoryPoints,UnimodularTransformation,VerifyLoop

(1)

 

For loops

While Loops

For loops

For loops can be analyzed to determine their data dependencies and apply transformations to assist in their parallelization.  The commands support array indices that are polynomials with rational coefficients.  Here is an example of how a nested for loop can be transformed so that the inner loop can be parallelized:

 

The following procedure has dependencies across both the i and the j loop indices and cannot be easily parallelized in this form:

p  procA   local i, j:   for i from 1 to 3 do       for j from 1 to 3 do            Ai,j  Ai  1, j + Ai, j  1:       end do:   end do:end proc:

loop  CreateLoopp:

The dependencies in this loop cross both the i and j dimension, as can be seen in the equation of its dependence cone:

DependenceConeloop, A, di, dj;

0dj,dj1,di=1dj

(1.1)

Applying a transformation to the loop will change the relationship between the data dependencies:

transformation_matrix  1 | 1, 0|1;

1101

(1.2)

transformed_loop  UnimodularTransformationloop,transformation_matrix:

GenerateProceduretransformed_loop;

procAlocali,j;forifrom2to6doforjfrommax1,i3tomin3,i1doA[ij,j]:=A[−1+ij,j]+A[ij,j1]end doend do;returnend proc

(1.3)

This transformed loop no longer has a relationship between the dimensions its distance vectors:

DependenceConetransformed_loop,  A, dn, dm;

dn=1,0dm,dm1

(1.4)

The data dependencies in the loop body only depend on previously computed elements.  The pattern for updating the array in the original and transformed loops are shown below.  The inner loop of the transformed program corresponds to the anti-diagonal lines of the array updates.  These updated operations can be performed simultaneously since they only refer to previously updated array entries (those entries that point toward a particular array entry).

Original loop's array updates

Transformed loop's array updates

Legend

Red dots: Data points in array

Blue arrows: Read/write dependency between array entries

Green dotted lines: Order in which elements of the array are updated

The set of array indices for all values of the loop's index variables can also be computed:

ispace IterationSpaceloop;

1i,i3,1j,j3

(1.5)

isolveconvertispace,set;

i=1,j=1,i=1,j=2,i=1,j=3,i=2,j=1,i=2,j=2,i=2,j=3,i=3,j=1,i=3,j=2,i=3,j=3

(1.6)

While Loops

The while loop related commands can be used to formally verify that a procedure meets its specification.  The invariants of a while loop can be computed and, when combined with the pre-condition and guard condition of the loop, used to verify whether or not the post-condition will be satisfied.  This verification indicates whether or not the ASSERT statement after the loop will always be true.  Loops whose assignments are polynomials with rational coefficients are supported.

The following example shows how the invariants of a while loop can be computed and used to verify that the following program is free from errors and meets its specification encoded in the last ASSERT statement of the procedure:

 z3sqrt  proc a&comma; err     local r&comma; q&comma; p&semi;     r  a  1&semi;     q  1&semi;     p  1&sol;2&semi;     ASSERTa  4 and 1  a and 0 < err and p &gt; 0 and r 0 &semi;     while err  2 &ast; p &ast; r do         if 0  2 &ast; r  2 &ast; q  p then             r  2 &ast; r  2 &ast; q  p&semi;             q  q &plus; p&semi;             p  1&sol;2 &ast; p&colon;         else             r  2 &ast; r&semi;             p  1&sol;2 &ast; p&colon;         end if&colon;     end do&semi;     ASSERTq&Hat;2  a and a < q&Hat;2&plus;err&semi;     return q&colon;  end proc&colon;

 

Create the WhileLoop data structure:

loop  CreateLoopz3sqrt&colon;

In this case, a loop invariant needs to be computed to formally verify the loop:

invariant  LoopInvariantloop&comma; invarianttype &equals; absolute&semi;

2pr&plus;q2a&equals;0

(2.1)

The return value of true indicates that the procedure is guaranteed to meet its specification:

VerifyLooploop&comma; invariant&semi;

true

(2.2)