 %%%%% BCAST
\begin{minipage}{.65\textwidth}
\begin{programSmall}
  \ccode{int} bcast1(int root, int val) \\
  \redcode{ensures !(send \&\& exit) U(root) send} \\
  \lb{} \\
  \ \ int ct = 0; \\
  \ \ if (PID == root) \lb{} \\
  \ \ \ \   while (ct < NPROCS) \lb{} \\
  \ \ \ \ \ \  if (root != ct) \lb \\
  \ \ \ \ \ \ \ \  send(val, ct); \\
  \ \ \ \ \ \ \rb \\
  \ \ \ \ \ \ ct = ct + 1;    \\
  \ \ \ \  \rb{}  \\
  \ \ \rb{} else \lb{} \\
  \ \ \ \   recv(val, root); \\
  \ \  \rb{} \\
  \ \ return val; \\
  \rb{} \\
\end{programSmall}
\end{minipage}
\begin{minipage}{.35\textwidth}
\begin{programSmall}
  \ccode{int} bcast2(int root, int val) \\
  \redcode{ensures !(send \&\& exit) U(root) send} \\
  \lb{} \\
  \ \ int rootBasedID = (PID + NPROCS - root) \% NPROCS; \\
  \ \ if (rootBasedID != 0) \lb \\
  \ \ \ \   recv(val, 0);\\
  \ \ \rb \\
\ \  if (rootBasedID < NPROCS-1) \lb \\
\ \ \ \     send(val, rootBasedID + 1);\\
\ \   \rb\\
\ \  return val; \\
  \rb{} \\
\end{programSmall}
\end{minipage}

%%%%% REDUCE/GATHER
\begin{minipage}{.55\textwidth}
\begin{programSmall}
  \ccode{int[]} gather1(int root, int val) \\
  \redcode{behavior isRoot;} \\
  \redcode{\ \ assumes PID == root;} \\
  \redcode{\ \ ensures !(exit) U(0 .. NPROCS-1) send} \\
  \redcode{\ \ ensures recv U(0 .. NPROCS-1) send} \\
  \lb{} \\
  \ \ int ct = 1; \\
  \ \ int x; \\
  \ \ int[] ret; \\
  \ \ ret[root] = val; \\
  \ \ if (PID == root) \rb{} \\
  \ \ \ \   while (ct < NPROCS) \lb{} \\
  \ \ \ \ \ \  recv(val, any x); \\
  \ \ \ \ \ \  ret[x] = val; \\
  \ \ \ \ \ \ ct = ct + 1;    \\
  \ \ \ \  \rb{}  \\
  \ \ \rb{} else\lb{} \\
  \ \ \ \   send(val, root); \\
  \ \  \rb{} \\
  \ \ return ret; \\
  \rb{} \\
\end{programSmall}
\end{minipage}
\begin{minipage}{.45\textwidth}
\begin{programSmall}
  \ccode{int[]} gather2(int root, int val) \\
  \redcode{behavior isRoot;} \\
  \redcode{\ \ assumes PID == root;} \\
  \redcode{\ \ ensures !(exit) U(0 .. NPROCS-1) send} \\
  \redcode{\ \ ensures recv U(0 .. NPROCS-1) send} \\
  \redcode{behavior noRoot;} \\
  \redcode{\ \ assumes PID != root;} \\
  \redcode{\ \ ensures !(send \&\& exit) U((root+NPROCS-1)\%NPROCS) send} \\
  \lb{} \\
\ \   int ret[]; \\
\ \   int rootBasedID = (PID + NPROCS - root) \% NPROCS;\\
\ \     ret[PID] == val; \\
\ \   if (rootBasedID < NPROCS-1) \lb \\
\ \ \ \     recv(ret, rootBasedID + 1); \\
\ \ \ \     ret[PID] == val; \\
\ \   \rb \\
\ \   if (rootBasedID > 0) \lb \\
\ \ \ \     send(ret, rootBasedID - 1); \\
\ \   \rb \\
\ \   return ret; \\
  \rb{} \\
\end{programSmall}
\end{minipage}


%%%%% ALLREDUCE/ALLGATHER
\begin{minipage}{.55\textwidth}
\begin{programSmall}
  \ccode{int[]} twogatherBad(int root, int val) \\
  \redcode{behavior isRoot:}\\  
  \redcode{\ \ assumes PID == root}\\
  \redcode{\ \ ensures !exit U(0 .. NPROCS-1) send} \\
  \redcode{\ \ ensures recv U(0 .. NPROCS-1) send} \\
  \lb{} \\
  \ \   int[] ret; \\
  \ \   \redcode{\textit{//root: !(exit) U(0 .. NPROCS-1) send}}\\
  \ \   \redcode{\textit{//root: recv U(0 .. NPROCS-1) send}}\\
\ \   ret = gather(root, val); \\
\ \   ret = gather(root, ret); \\
\ \ return ret;\\
  \rb{} \\
\end{programSmall}
\end{minipage}
\begin{minipage}{.45\textwidth}
\begin{programSmall}
  \ccode{int[]} allgather(int root, int val) \\
  \redcode{ensures !exit U(0 .. NPROCS-1) send} \\
  \redcode{ensures recv U(0 .. NPROCS-1) send}  \bluecode{wrong? too strong?}\\
  \lb{} \\
  \ \   int[] ret; \\
\ \   \redcode{\textit{//root: !(exit) U(0 .. NPROCS-1) send}}\\
\ \   ret = gather(root, val); \\
\ \ \redcode{\textit{//!(send $\wedge$ exit) U(root) send}} \\
\ \   ret = bcast1(root, ret); \\
\ \ return ret;\\
  \rb{} \\
\end{programSmall}
\end{minipage}

\begin{minipage}{.55\textwidth}
\begin{programSmall}
  \ccode{int[]} alltoall(int[] vals) \\
  \redcode{ensures !exit U(0 .. NPROCS-1) send}
  \lb{} \\
  ...\\
  \rb{} \\
\end{programSmall}
\end{minipage}
\begin{minipage}{.45\textwidth}
\begin{programSmall}
  \ccode{int} scan(int val) \\
  \redcode{ensures !send U(0) send}\\
  \lb{} \\
\ \   int buf; \\
\ \   if (PID > 0) \lb \\
\ \ \ \     recv(buf, PID - 1); \\
\ \ \ \     val = reduce(buf, val); \\
\ \   \rb \\
\ \   if (PID < NPROCS-1) \lb  \\
\ \ \ \     send(val, PID + 1);  \\
\ \   \rb \\
\ \   return val; \\
  \rb{} \\
\end{programSmall}
\end{minipage}

\rule{\textwidth}{0.4pt}

%%%%%%% EXCHANGE/GAUSSIAN ELIMINATE

\vspace{5mm}
\begin{minipage}{.65\textwidth}
\begin{programSmall}
  \ccode{int[]} exchange(int[] vals, int left, int right) \\
  \redcode{ensures !exit U(left, right) send;}\\
  \lb{} \\
\ \  send(vals[3], right); \\
\ \  send(vals[0], left); \\
\ \  recv(vals[2], right); \\
\ \  recv(vals[1], left); \\
  \rb{} \\
\end{programSmall}
\end{minipage}
\begin{minipage}{.35\textwidth}
\begin{programSmall}
  \ccode{int[]} gaussElim(int[] vals) \\
  \redcode{ensures !exit U(0 .. NPROCS-1) send;}\\
  \lb{} \\
\ \   int ct = 0; \\
\ \   int x; \\
\ \   while (ct < N) \lb \\
\ \ \ \     ... \\
\ \ \ \     Allreduce(vals); \\
\ \ \ \     ... \redcode{//\textit{modify x}}\\
\ \ \ \     Bcast(vals, x); \\
\ \ \ \     ... \\
\ \   \rb \\
\ \   return vals;\\
  \rb{} \\
\end{programSmall}
\end{minipage}


%%%%%%% MANAGER/WORKER
\begin{minipage}{.55\textwidth}
\begin{programSmall}
  \ccode{int[]} managerWorker1(int data, int mg, \\
  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ int workload, \\
  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ int  term) \\
  \redcode{behavior manager:} \\
  \redcode{\ \ assumes PID == mg;} \\
  \redcode{\ \ ensures recv U(0 .. NPROCS-1) exit;} \\
  \lb{} \\
\ \   int buf, ret, x, flag = 1; \\
\ \   int recved = 0; \\
\ \   int sent = NPROCS; \\
\ \   if (PID == mg) \lb  \\
\ \ \ \     bcast(data, mg);  \\
\ \ \ \     while (recved < workload) \lb  \\ 
\ \ \ \ \ \       recv(buf, any x); \\ 
\ \ \ \ \ \       ret = ret + buf; \\ 
\ \ \ \ \ \       recved = recved + 1; \\ 
\ \ \ \ \ \       if (sent < workload) \lb  \\ 
\ \ \ \ \ \ \ \         send(data, x); \\ 
\ \ \ \ \ \ \ \         sent = sent + 1; \\ 
\ \ \ \ \ \       \rb{}  else \lb  \\ 
\ \ \ \ \ \ \ \         send(term, x); \\ 
\ \ \ \ \ \       \rb  \\ 
\ \ \ \     \rb  \\ 
\ \   \rb{}  else \lb  \\ 
\ \ \ \     bcast(buf, mg); \\ 
\ \ \ \     while (flag) \lb  \\
\ \ \ \ \ \       buf = f(buf); \\ 
\ \ \ \ \ \       send(buf, mg); \\ 
\ \ \ \ \ \       recv(buf, mg); \\ 
\ \ \ \ \ \       if (buf == term) \lb  \\ 
\ \ \ \ \ \ \ \       flag = 0; \redcode{\textit{// break}} \\ 
\ \ \ \ \ \       \rb  \\ 
\ \ \ \     \rb  \\
\ \   \rb  \\ 
  \rb{} \\
\end{programSmall}
\end{minipage}
\begin{minipage}{.35\textwidth}
\begin{programSmall}
  \ccode{int[]} managerWorker2(int data, int mg, \\
  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ int workload, \\
  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ int  term) \\
  \redcode{\ \ ensures !exit U(mg) send;} \\
  \lb{} \\
\ \   int buf, ret, x, ct = 0; \\
\ \   int recved = 0; \\
\ \   int sent = NPROCS; \\
\ \   if (PID == mg) \lb  \\
\ \ \ \     bcast(data, mg);  \\
\ \ \ \     while (recved < workload) \lb  \\ 
\ \ \ \ \ \       recv(buf, any x); \\ 
\ \ \ \ \ \       ret = ret + buf; \\ 
\ \ \ \ \ \       recved = recved + 1; \\ 
\ \ \ \ \ \       if (sent < workload) \lb  \\ 
\ \ \ \ \ \ \ \         send(data, x); \\ 
\ \ \ \ \ \ \ \         sent = sent + 1; \\ 
\ \ \ \ \ \       \rb{} \\
\ \ \ \     \rb  \\ 
\ \ \ \     while (ct < NPROCS) \lb{} \\
\ \ \ \ \ \  if (ct != mg) \lb{} \\
\ \ \ \ \ \ \ \  send(term, ct); \\
\ \ \ \ \ \  \rb{}\\
\ \ \ \ \ \  ct = ct + 1; \\
\ \ \ \ \rb{}\\

\ \   \rb{}  else \lb  \\ 
\ \ \ \     bcast(buf, mg); \\ 
\ \ \ \     while (!ct) \lb  \\
\ \ \ \ \ \       buf = f(buf); \\ 
\ \ \ \ \ \       send(buf, mg); \\ 
\ \ \ \ \ \       recv(buf, mg); \\ 
\ \ \ \ \ \       if (buf == term) \lb  \\ 
\ \ \ \ \ \ \ \       ct = 1; \redcode{\textit{// break}} \\ 
\ \ \ \ \ \       \rb  \\ 
\ \ \ \     \rb  \\
\ \   \rb  \\ 
  \rb{} \\
\end{programSmall}
\end{minipage}