// ============================================================================
// Name:        ParallelPrefixSum
// Description: Given an array a[0..n-1], compute the sums of all prefixes
//              in parallel using n processes and store the results in an
//              array s[0..n-1].
// References:  G.R. Andrews. Concurrent Programming - Principles and Practice.
//              The Benjamin/Cummings Publishing Company, 1991.
// Parameters:  SIZE (size of array)
//              INFINITE (use variables with infinite bit width)
//              BITS (bit width for finite variables)
// ============================================================================

#ifndef SIZE
#define SIZE 4u
#endif

#ifdef INFINITE
#define TYPE int
#else
#ifndef BITS
#define BITS 4u
#endif
#define TYPE int[BITS]
#endif

module ParallelPrefixSum(TYPE a[SIZE], &s[SIZE], &t[SIZE], nat[sizeOf(2u*(SIZE-1u))] &d, event &ready, &fault)
   implements Spec(ready, fault) {
   sequence(nat[sizeOf(SIZE-1u)] i=0u .. (SIZE-1u)) {
      s[i] = a[i];
      t[i] = a[i];
   }

   d = 1u;
   while(d < SIZE) {
      parallel(nat[sizeOf(SIZE-1u)] i=0u .. (SIZE-1u))
         if(i >= d)
            next(s[i]) = s[i-d] + s[i];
      next(d) = d+d;
      pause;
   }

   emit ready;
   CheckSpec(s, t, fault);
}

// ----------------------------------------------------------------------------
// In the specifiaction we have to be careful with overflows. Comparing s[i]
// with t[i-1u]+t[i] would be wrong since the expression (s[i] != t[i-1u]+t[i])
// is computed with full bitwidths! To solve this problem, we use two loops.
// ----------------------------------------------------------------------------

module CheckSpec(TYPE &s[SIZE], &t[SIZE], event &fault) {
   nat[sizeOf(SIZE)] &i, &j;
   i = 1u;
   while(i < SIZE) {
      next(t[i]) = t[i-1u] + t[i];
      next(i) = i+1u;
      pause;
   }
   j = 1u;
   while(j < SIZE) {
      if(s[j] != t[j])
         emit fault;
      next(j) = j+1u;
      pause;
   }
}

spec Spec(event ready, fault){
   termination: A F ready;
   correctness: A G !fault;
}