int rank, nprocs, nsteps;
double rbuf, sbuf;
#define  LEFT(rank) ((rank) > 0 ? (rank) - 1 : nprocs - 1)
/*@ axiomatic OracleSpec {
  @   logic double oracle(integer t, integer i);
  @   axiom oracle_ax : \forall int t, i; t > 0 ==> oracle(t-1,LEFT(i)) == oracle(t,i);
  @ }
  @*/
//@ ghost int * sc;                         // send counters, one per proc
//@ ghost int * rc;                         // recv counters, one per proc
//@ ghost double * chans;                   // sending channels, one per proc
//@ ghost int * sizes;                      // sending channel sizes, one per proc
/*@ predicate inv0 = \valid(sc+(0..nprocs-1)) && \valid(rc+(0..nprocs-1)) 
  @   && \valid(chans+(0..nprocs-1)) && \valid(sizes+(0..nprocs - 1)) && 
  @   \separated(sc+(0..nprocs-1), rc+(0..nprocs-1), chans+(0..nprocs-1),
  @              sizes+(0..nprocs-1)); */
/*@ predicate inv1 = \forall int i; 0<=i<nprocs ==> 0<=sizes[i]<=1;
  @ predicate inv2 = \forall int i; 0<=i<nprocs ==> 0<=sc[i]<=nsteps;
  @ predicate inv3 = \forall int i; 0<=i<nprocs ==> 0<=rc[i]<=nsteps;
  @ predicate inv4 = \forall int i; 0<=i<nprocs ==> rc[i]==sc[LEFT(i)]-sizes[LEFT(i)];
  @ predicate inv5 = \forall int i; 0<=i<nprocs ==> (sizes[i]==1 ==> chans[i]==oracle(sc[i]-1,i));
  @ predicate inv6 = \forall int i; 0 <= i < nprocs ==> (sc[i]-rc[i]==0 || sc[i]-rc[i]==1);*/
#define inv (0 <= rank < nprocs && inv0 && inv1 && inv2 && inv3 && inv4 && inv5 && inv6)
/*@ requires \valid(x) && sizes[rank] == 0 && 0 <= rank < nprocs;
  @ assigns  chans[rank], sizes[rank];
  @ ensures  chans[rank] == *x && sizes[rank] == 1;
  @*/
void send(double * x);
/*@ requires \valid(y) && sizes[LEFT(rank)] == 1 && 0 <= rank < nprocs;
  @ assigns *y, sizes[LEFT(rank)];
  @ ensures *y == chans[LEFT(rank)] && sizes[LEFT(rank)] == 0;
  @*/
void recv(double * y);
/*@ requires inv;
  @ assigns sizes[0..nprocs-1], chans[0..nprocs-1], sc[0..nprocs-1], rc[0..nprocs-1];
  @ ensures sc[rank]==\old(sc[rank]) && rc[rank]==\old(rc[rank]);
  @ ensures sizes[LEFT(rank)]==1 && chans[rank]==\old(chans[rank]) && inv;
  @*/
void prerecv_interleave(void);
/*@ requires inv;
  @ assigns sizes[0..nprocs-1], chans[0..nprocs-1], sc[0..nprocs-1], rc[0..nprocs-1];
  @ ensures sc[rank]==\old(sc[rank]) && rc[rank]==\old(rc[rank]);
  @ ensures sizes[rank]==0 && chans[rank]==\old(chans[rank]) && inv;
  @*/
void presend_interleave(void);  
/*@ requires inv && sizes[rank]==0 && sbuf==oracle(0, rank);
  @ requires 0<nsteps && sc[rank]==0 && rc[rank]==0;
  @ assigns chans[0..nprocs-1], rbuf, sbuf, sizes[0..nprocs-1], rc[0..nprocs-1], sc[0..nprocs-1];
  @ ensures rbuf == oracle(nsteps-1, LEFT(rank));
  @*/
void exchange() {
  int t = 0;
  /*@ loop invariant inv && 0 <= t <= nsteps; 
    @ loop invariant t == 0 ==> sbuf == oracle(0, rank);
    @ loop invariant t > 0 ==> (sbuf == oracle(t-1, LEFT(rank)) && sbuf == rbuf);
    @ loop invariant t == sc[rank] && t == rc[rank];
    @ loop assigns sbuf, t, rbuf, sc[0..nprocs-1], rc[0..nprocs-1];
    @ loop assigns chans[0..nprocs-1], sizes[0..nprocs-1];
    @ loop variant nsteps - t;
    @*/
  while (t < nsteps) {
    presend_interleave(); send(&sbuf); 
    /*@ ghost sc[rank]++;*//*@ assert A0: inv6; */
    prerecv_interleave();
    /*@ assert A1: inv4;*/ /*@ assert A2: inv5; */
    recv(&rbuf);/*@ assert A3: inv5;*/ 
    /*@ ghost rc[rank]++;*/
    /*@ assert A4: inv4;*/ /*@ assert A5: inv6; */
    //sbuf = rbuf; 
    t++;
  }
}
