// ************************************************************************** // // // // 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])); }