// ************************************************************************** //
//                                                                            //
//    eses                   eses                                             //
//   eses                     eses                                            //
//  eses    eseses  esesese    eses   Embedded Systems Group                  //
//  ese    ese  ese ese         ese                                           //
//  ese    eseseses eseseses    ese   Department of Computer Science          //
//  eses   eses          ese   eses                                           //
//   eses   eseses  eseseses  eses    University of Kaiserslautern            //
//    eses                   eses                                             //
//                                                                            //
// ************************************************************************** //
// ShearSort is parallel sorting algorithm that is performed on a MxN array.  //
// The sorted sequence will finally be mapped to the array in a snake-like    //
// row major indexing scheme, as eg.                                          //
//                                                                            //
//     01 02 03 04                                                            //
//     08 07 06 05                                                            //
//     09 10 11 12                                                            //
//     16 15 14 13                                                            //
//                                                                            //
// The algorithm is due to [Scherson & Sen, 1989], and works by performing    //
// a loop of column sorts and row sorts until the array is sorted. The        //
// version below makes use of selection sort to for the column and row        //
// sorting phases which is not that efficient.                                //
// ************************************************************************** //

macro N = 4;
macro M = 4;
macro I = 64;

module ShearSelectionSort([M*N]int{I} ?a,[M][N]int{I}b, event ready) {
    bool swapped,firstRound;
    // gather the input row-wise in the matrix
    for(i=0..(M-1))
        for(j=0..(N-1))
            b[i][j] = a[i*N+j];

    firstRound = true;
    weak abort
        loop {
            // column-wise sorting in parallel
            for(j=0..(N-1)) do || {
                // sort column b[0..M-1][j] by SelectionSort
                nat{M} imin;
                for(k=0..(M-1)) {
                    // find the minimum b[imin][j] of b[k..M-1][j]
                    imin = k;
                    for(l=k+1..(M-1)) {
                        if(b[l][j] < b[imin][j])
                            next(imin) = l;
                        pause;
                        // here, b[imin][j] is the minimum of b[k..l][j]
                        assert(forall(p=k..l) (b[imin][j]<=b[p][j]));
                    }
                    // swap b[k][j] with b[imin][j]
                    if(imin!=k) {
                        next(b[k][j]) = b[imin][j];
                        next(b[imin][j]) = b[k][j];
                        next(swapped) = true;
                    }
                    pause;
                    // an invariant is here that b[0..k][j] is already sorted
                    assert(forall(p=1..k) (b[p-1][j]<=b[p][j]));
                }
            }
            if(!swapped&!firstRound) emit(ready);
            else next(swapped) = false;
            // row-wise sorting in parallel
            for(i=0..(M-1)) do || {
                // sort row b[i][0..N-1]
                nat{N} jmin;
                for(k=0..(N-1)) {
                    // find the minimum/maximum b[i][imin] of b[i][k..N-1]
                    jmin = k;
                    for(l=k+1..(N-1)) {
                        if(i%2==0) {
                            if(b[i][l] < b[i][jmin])
                                next(jmin) = l;
                        } else {
                            if(b[i][l] > b[i][jmin])
                                next(jmin) = l;
                        }
                        pause;
                        // here, b[i][imin] is the minimum/maximum of b[i][k..l]
                        if(i%2==0)
                            assert(forall(p=k..l) (b[i][jmin]<=b[i][p]));
                        else
                            assert(forall(p=k..l) (b[i][jmin]>=b[i][p]));
                    }
                    // swap b[i][k] with b[i][jmin]
                    if(jmin!=k) {
                        next(b[i][k]) = b[i][jmin];
                        next(b[i][jmin]) = b[i][k];
                        next(swapped) = true;
                    }
                    pause;
                    // an invariant is here that b[i][0..k] is already sorted
                    if(i%2==0)
                        assert(forall(p=1..k) (b[i][p-1]<=b[i][p]));
                    else
                        assert(forall(p=1..k) (b[i][p-1]>=b[i][p]));
                }
            }
            if(!swapped&!firstRound) emit(ready);
            else next(swapped) = false;
            firstRound = false;
        }
    when(ready);
}
drivenby Test01 {
    // generate already sorted sequence
    for(i=0..M*N-1) a[i] = i;
    dw: await(ready);
    // check that rows are sorted in snake-like order
    for(i=0..M-1) 
        if(i%2==0)
            assert(forall(p=1..N-1) (b[i][p-1]<=b[i][p]));
        else
            assert(forall(p=1..N-1) (b[i][p-1]>=b[i][p]));
    // and check that the first and last column are sorted
    assert(forall(p=1..M-1) (b[p-1][0]<=b[p][0]));
    assert(forall(p=1..M-1) (b[p-1][N-1]<=b[p][N-1]));
}
drivenby Test02 {
    // generate reversed sorted sequence
    for(i=0..M*N-1) a[i] = M*N-1-i;
    dw: await(ready);
    // check that rows are sorted in snake-like order
    for(i=0..M-1) 
        if(i%2==0)
            assert(forall(p=1..N-1) (b[i][p-1]<=b[i][p]));
        else
            assert(forall(p=1..N-1) (b[i][p-1]>=b[i][p]));
    // and check that the first and last column are sorted
    assert(forall(p=1..M-1) (b[p-1][0]<=b[p][0]));
    assert(forall(p=1..M-1) (b[p-1][N-1]<=b[p][N-1]));
}
drivenby Test03 {
    for(i=0..M*N-1)
        a[i] = ((i%2==0)?i:((M*N%2==0)?M*N-i:M*N-1-i));
    dw: await(ready);
    // check that rows are sorted in snake-like order
    for(i=0..M-1) 
        if(i%2==0)
            assert(forall(p=1..N-1) (b[i][p-1]<=b[i][p]));
        else
            assert(forall(p=1..N-1) (b[i][p-1]>=b[i][p]));
    // and check that the first and last column are sorted
    assert(forall(p=1..M-1) (b[p-1][0]<=b[p][0]));
    assert(forall(p=1..M-1) (b[p-1][N-1]<=b[p][N-1]));
}