// ************************************************************************** // // // // 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 // // // // ************************************************************************** // // QuickSort [Hoar61a,Hoar61b,Hoar61c] is one of the most popular sorting // // procedures. Although its worst case behavior is O(n^2), its average // // behavior is O(n*log(n)), so that QuickSort is in average optimal. // // The implementation below is an iterative version of QuickSort that // // maintains a stack of pivot elements to keep track of the recursive // // calls. Note that these could also be made in parallel that implements // // a parallel version of QuickSort [Powe91]. The variable pvH is the head // // of the stack implemented by the array pivot, and there is an invariant that// // pivot[i]>pivot[j] for i>j and all i,j<=pvH. The partitions are then // // b[pivot[i]+1 .. pivot[i-1]]. // // ************************************************************************** // macro aSize = 16; macro iSize = 64; module QuickSort([aSize]nat{iSize} ?a,b, event ready) { [aSize]nat{aSize} pivot; nat{aSize+1} i,j,pvH,left,right; for(i=0..aSize-1) b[i] = a[i]; left = 0; right = aSize-1; pvH = 0; pivot[0] = right; do { if((left==right)|(left+1==right)) { // end of `recursion': maintain a potential swap if(b[left]>b[right]) { next(b[right]) = b[left]; next(b[left]) = b[right]; } // backtrack step to the next partition if(pvH>0) { next(left) = (pivot[pvH]==pivot[pvH-1]?pivot[pvH]:pivot[pvH]+1); next(right) = pivot[pvH-1]; next(pvH) = pvH-1; } else emit next(ready); w0: pause; } else { // determine next pivot element pivot[pvH+1] = left + (right-left)/2; next(pvH) = pvH+1; w1: pause; // in-place partition of b[left..right] wrt. b[pivot[pvH]] // first move pivot element to the right next(b[right]) = b[pivot[pvH]]; next(b[pivot[pvH]]) = b[right]; next(pivot[pvH]) = right; w2: pause; // now determine position of pivot element by j i = left; j = left; while(i<right) { if(b[i]<=b[right]) { next(b[i]) = b[j]; next(b[j]) = b[i]; next(j) = j+1; } next(i) = i+1; w3: pause; } next(b[right]) = b[j]; next(b[j]) = b[right]; next(pivot[pvH]) = j; next(right) = j; w4: pause; // now the array is partitioned wrt. to the pivot element, i.e. // b[i]<=b[pivot[pvH]] for i<=pvH and b[pivot[pvH]]<b[i] for i>pvH // proceed by determine the next partition and a new pivot element in it } } while(!ready); } drivenby Test01 { for(i=0..aSize-1) a[i] = i; dw: await(ready); for(i=0..aSize-1) assert(b[i] == i); } drivenby Test02 { for(i=0..aSize-1) a[i] = aSize-1-i; dw: await(ready); for(i=0..aSize-1) assert(b[i] == i); } drivenby Test03 { for(i=0..aSize-1) a[i] = ((i%2==0)?i:((aSize%2==0)?aSize-i:aSize-1-i)); dw: await(ready); for(i=0..aSize-1) assert(b[i] == i); }