// ************************************************************************** // // // // 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 // // // // ************************************************************************** // // The parallel prefix problem (also known a list ranking see [KaRa88]) is // // defined as follows: For an array x[0..N-1], we have to compute the values // // y[i] = sum(j=0..i) x[j] for all i=0..N-1. The module below computes these // // values in log(N) time using O(N) processors which is an optimal PRAM // // algorithm. // // The version below is due to Andrews. Concurrent Programming - Principles // // and Practice. The Benjamin/Cummings Publishing Company, 1991. // // ************************************************************************** // macro N = 8; module ListRanking3([N]int ?x,y,event !rdy) { nat{2*(N-1)} d; for(i=0..N-1) y[i] = x[i]; d = 1; while(d<N) { for(i=0..N-1) if(i>=d) next(y[i]) = y[i-d]+y[i]; next(d) = d+d; pause; } emit(rdy); assert(forall(i=0..N-1) (y[i] == sum(j=0..i) x[j])); } satisfies { termination: assert A F rdy; } drivenby { for(i=0..N/2-1) x[i] = i; for(i=N/2..N-1) x[i] = N-1-i; await(rdy); }