// ============================================================================
// Name:        FastMax
// Description: Find the maximal element in an array of numbers in constant
//              time using several processes. When two or more processes
//              concurrently write to the same location, they all write
//              the same value. Thus, no write conflicts can occur.
// References:  T.H. Cormen, C.E. Leiserson, R.L. Rivest. Introduction to
//              Algorithms. MIT Press, 1997.
// 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

#define MAXOFARRAY(a,m) (forall(nat[sizeOf(SIZE-1u)] i=0u .. (SIZE-1u)) (m >= a[i]))

module FastMax(TYPE b[SIZE], &a[SIZE], &max, bool &m[SIZE], event &ready)
   implements MaxSpec(a, max, ready) {
   sequence(nat[sizeOf(SIZE-1u)] i=0u .. (SIZE-1u)) {
      a[i] = b[i];
      m[i] = true;
   }

   parallel(nat[sizeOf(SIZE-1u)] i=0u .. (SIZE-1u))
      parallel(nat[sizeOf(SIZE-1u)] j=0u .. (SIZE-1u))
         if(a[i] < a[j])
            next(m[i]) = false;

   pause;

   parallel(nat[sizeOf(SIZE-1u)] i=0u .. (SIZE-1u))
      if(m[i])
         max = a[i];

   emit ready;
}

spec MaxSpec(TYPE a[SIZE], max, event ready) {
   termination: A F ready;
   correctness: A G (ready -> MAXOFARRAY(a, max));
}