%%%%% 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}