// ************************************************************************** // // // // 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 // // // // ************************************************************************** // // Given an array a[0..N-1], compute its maximum in time O(log(N)) using O(N) // // processors. The algorithm is similar to list ranking making use of pointer // // jumping which is done here by index expressions. // // ************************************************************************** // macro N = 19; macro R = 128; macro K = log(N); macro WidthOfLevel(i,n) = (i==0 ? n : WidthOfLevel(i-1,(n+1)/2)); macro SumOfWidths(j) = sum(i=0..j) WidthOfLevel(i,N); macro idm(i,j) = (i==0 ? j : j+SumOfWidths(i-1)); macro isArrayMax(a,x) = forall(i=0..N-1) (a[i] <= x); macro isArrayMin(a,x) = forall(i=0..N-1) (a[i] >= x); macro contains(a,x) = exists(i=0..N-1) (a[i] == x); macro max(x,y) = (x<=y ? y : x); module Maximum_OlogN([N]int{R} ?a,int{R} max) { [SumOfWidths(K)]nat z; // first row determines the N operands z[idm(0,0..N-1)] for(j=0..N-1) z[idm(0,j)] = a[j]; // deeper levels determine the balanced binary tree for(i=0..K-1) let(w1 = WidthOfLevel(i,N)) let(w2 = (w1+1)/2) for(j=0..w2-1) z[idm(i+1,j)] = (2*j+1==w1 ? z[idm(i,2*j)] : max(z[idm(i,2*j)],z[idm(i,2*j+1)])); // determine the result max = z[idm(K,0)]; } drivenby { for(i=0..N/2-1) a[i] = i; for(i=N/2..N-1) a[i] = N-1-i; assert(contains(a,max) & isArrayMax(a,max)); }