// ************************************************************************** // // // // 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], the algorithm below determines its maximum using // // O(N^2) processors in constant time, i.e. one macro step. To this end, all // // pairs of elements a[i],a[j] are considered and m[i] = true is written to a // // local array m[0..N-1] in case a[i] < a[j] holds. Note that several writes // // may occur in this macro step, but all write the same value (so this is a // // CRCW PRAM algorithm). In a second part of the macro step, we can determine // // the maximum in that those indices having m[i]=false are determined. // // ************************************************************************** // macro N = 8; macro R = 8; 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); module Maximum_O1([N]int{R} ?a, int{R} max) { event [N]bool m; // set m[i] iff some a[j] is greater than a[i] for(i=0..N-1) for(j=0..N-1) if(a[i] < a[j]) m[i] = true; // thus, those i where m[i] is false are the indices of the maximum a[i] // note: there might be several such indices (containing the same value) for(i=0..N-1) if(!m[i]) max = a[i]; } satisfies { correct : assert(contains(a,max) & isArrayMax(a,max)); } 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)); }