Transforming an algorithm into static single assignment (SSA) form

Question

Has below algorithm transformed correctly?

Problem 3. 2017. Feb.

Transform the following algorithm into static single assignment (SSA) form.

module Test ( [4] i n t ? a , i n t ?b , i n t ! c ) {

 i n t  t = b ;

 i n t x , y = 0 ;

 pause ;

fo r ( i = 0 . . 3 )

 { next ( x ) = y ∗ t ;

 pause ;

next ( y ) = x + a [ i ] ;

 pause ; }

 c = y ; }

Solution:

 i n t  t = b ;

int x[5]={0,0,0,0,0};

int y[5]={0,0,0,0,0};

pause ;

fo r ( i = 0 . . 3 )

 { x[i+1] = y[i] ∗ t ;

 y[i+1] = x[i+1] + a [ i ] ;

 pause ; }

 c = y[4] ; }

(we could use a corner case for i=0 and reduce the array sizes by one)

Answer 1

The following program was given:

module Test([4]int ?a, int ?b, int !c) {
    int t,x,y;
    t = b;
    x = 0;
    y = 0;
    pause;
    for(i=0..3) {
        next(x) = y * t;
        pause;
        next(y) = x + a[i];
        pause;
    }
    c = y;
}

The for-loop is thereby an abbreviation of a sequence of its body statements. If we unroll that for-loop, we get the following program:

module Test([4]int ?a, int ?b, int !c) {
    int t,x,y;
    t = b;
    x = 0;
    y = 0;
    pause; 
    next(x) = y * t;
    pause; 
    next(y) = x + a[0];
    pause; 
    next(x) = y * t;
    pause; 
    next(y) = x + a[1];
    pause; 
    next(x) = y * t;
    pause; 
    next(y) = x + a[2];
    pause; 
    next(x) = y * t;
    pause; 
    next(y) = x + a[3];
    pause; 
    c = y; 
}

In the above version, it is better seen that there are many assignments to the same variables x and y. We have to introduce fresh instances for each assignment to ensure a SSA form, and therefore get the following program:

module Test([4]int ?a, int ?b, int !c) {
    int t,x,x1,x2,x3,x4,y,y1,y2,y3,y4;
    t = b;
    x = 0;
    y = 0;
    pause; 
    next(x1) = y * t;
    pause; 
    next(y1) = x + a[0];
    pause; 
    next(x2) = y1 * t;
    pause; 
    next(y2) = x1 + a[1];
    pause; 
    next(x3) = y2 * t;
    pause; 
    next(y3) = x2 + a[2];
    pause; 
    next(x4) = y3 * t;
    pause; 
    next(y4) = x3 + a[3];
    pause; 
    c = y4; 
}

The above program is the SSA form that is required for a further mapping to a combinational circuit or a systolic array if the latter should be executed in a pipelined fashion. Note that for SSA form, it is no problem to read a variable more than once, but there should only be one assignment to each variable. 

Comments

Can we also give the SSA without unrolling the loop?

And for the SSA form is it allowed to make improvement changes before, that will not change the semantics (on own risk if the improvement are sound)
E.g:
module Test([4]int ?a, int ?b, int !c) {
    int t,x,y;
    t = b;
    x = 0;
    y = 0;
    pause;
    for(i=0..3) {
        next(x) = y * t;
        pause;
        next(y) = x + a[i];
        pause;
    }
    c = y;
}
changing to
module Test([4]int ?a, int ?b, int !c) {
    int t,x,y;
    t = b;
    x = 0;
    y = 0;
    pause;
    for(i=0..3) {
        next(x) = y * t;
        next(y) = y * t + a[i];
        pause;
    }
    c = y;
}
so that the SSA will look like:

module Test([4]int ?a, int ?b, int !c) {
    int t,x,y;
    [5] int x,y
    t = b;
    x[0] = 0;
    y[0] = 0;
    pause;
    for(i=0..3) {
        x[i+1] = y[i] * t;
        y[i+1] = y[i] * t + a[i];
        pause;
    }
    c = y[4];
}

---

You cannot do SSA form without unrolling the above loop with scalar variables since these are overwritten in the next loop iterations.

However, you can transform the loop to another kind of SSA form where the variables are replaced by arrays (which are then the different names) as you have done above. That is possible, and even shorter.