% Graphics and colors... \graphicspath{{../images/}} % hyphenation...s \hyphenation{Open-MP} \definecolor{darkred}{rgb}{0.55, 0.0, 0.0} \definecolor{bistre}{rgb}{0.47, 0.27, 0.23} \definecolor{coolblack}{rgb}{0.0, 0.18, 0.39} \definecolor{Brown}{rgb}{0.59, 0.29, 0.0} % Comments... \newcommand{\mycomment}[1]{\texttt{\textcolor{darkred}{#1}}} \newcommand{\nonterm}[1]{\texttt{\textit{\textcolor{blue}{#1}}}} \newcommand{\mgcolor}[0]{bistre} \newcommand{\acslmark}{\textit{\textcolor{red}{a}}} \newcommand{\myskip}[0]{2mm} \newcommand{\powerset}{\raisebox{.15\baselineskip}{\Large\ensuremath{\wp}}} \renewcommand{\vdash}[0]{\models} % font size... \newcommand{\codesize}{\tt} % Type/font styles... \newcommand{\upsty}[1]{{\ttfamily\textcolor{Brown}{#1}}} %{\textbf{\textcolor{BlueViolet}{#1}}} \newcommand{\consty}[1]{{\ttfamily\textcolor{Bittersweet}{#1}}} \newcommand{\setsty}[1]{\textup{\textsf{\textcolor{BlueViolet}{#1}}}} \newcommand{\code}[1]{{\ttfamily #1}} % code not CIVL/C keyword \newcommand{\ccode}[1]{{\textcolor{coolblack}{\ttfamily\fontseries{b}\selectfont{}#1}}} \newcommand{\myccode}[1]{{\textcolor{blue}{\ttfamily\fontseries{b}\selectfont{}#1}}} \newcommand{\bluecode}[1]{{\ttfamily\bfseries\color{blue} #1}} \newcommand{\redcode}[1]{{\ttfamily\bfseries\color{red} #1}} \newcommand{\funsty}[1]{\ttfamily\bfseries #1} \newcommand{\typsty}[1]{{\textcolor{blue}{\ttfamily\bfseries\emph{#1}}}} \newcommand{\ct}[1]{\texttt{#1}} % Symbols... \newcommand{\civlImplies}{\Rightarrow} \newcommand{\ra}{\rightarrow} \newcommand{\B}{\mathbb{B}} \newcommand{\N}{\mathbb{N}} \newcommand{\lb}{\texttt{\char`\{}} \newcommand{\rb}{\texttt{\char`\}}} \newcommand{\civlU}{\texttt{\char`\_}} \newcommand{\U}{\texttt{\char`\_}} \newcommand{\BSL}{\texttt{\char`\\}} %\newcommand{\civlU}{{\ttfamily\symbol{'137}}} \newcommand{\civlUU}{\civlU\civlU} \newcommand{\biglp}{\textcolor{\mgcolor}{\big(}} \newcommand{\bigrp}{\textcolor{\mgcolor}{\big)}} \newcommand{\regxstar}{\textcolor{\mgcolor}{\textit{*}}} \newcommand{\regxplus}{\textcolor{\mgcolor}{\textit{+}}} \newcommand{\regxques}{\textcolor{\mgcolor}{\textit{?}}} \newcommand{\synxbar}{\textcolor{\mgcolor}{\mid}} \newcommand{\synxdef}{\textcolor{\mgcolor}{:=}} \newcommand{\synxdots}{\textcolor{\mgcolor}{\ldots}} % Spaces... \newcommand{\sspc}{\hspace{1mm}} % small space % Tools... \newcommand{\civl}{CIVL} \newcommand{\spin}{\textsc{Spin}} \newcommand{\mpispin}{\textsc{MPI-Spin}} \newcommand{\tass}{TASS} \newcommand{\partypes}[0]{\text{\normalsize{P}\scriptsize{AR}\normalsize{T}\scriptsize{YPES}}} \newcommand{\isp}{ISP} \newcommand{\mopper}{MOPPER} \newcommand{\promela}{Promela} % MPI primitives... % functions \newcommand{\MPISend}{\funsty{MPI\civlU{}Send}} \newcommand{\MPIRecv}{\funsty{MPI\civlU{}Recv}} \newcommand{\MPIBarrier}{\funsty{MPI\civlU{}Barrier}} \newcommand{\MPIReduce}{\funsty{MPI\civlU{}\-Reduce}} \newcommand{\MPIAllreduce}{\funsty{MPI\civlU{}Allreduce}} \newcommand{\MPIInit}{\funsty{MPI\civlU{}Init}} \newcommand{\MPIInitthread}{\funsty{MPI\civlU{}Init}\civlU{}thread} \newcommand{\MPIFinalize}{\funsty{MPI\civlU{}Finalize}} \newcommand{\MPIDup}{\funsty{MPI\civlU{}Comm\civlU{}dup}} \newcommand{\MPIFree}{\funsty{MPI\civlU{}Comm\civlU{}free}} \newcommand{\MPIWtime}{\funsty{MPI\civlU{}Wtime}} \newcommand{\MPIReducescatter}{\funsty{MPI\civlU{}Reducescatter}} \newcommand{\MPIAlltoallv}{\funsty{MPI\civlU{}Alltoallv}} \newcommand{\MPIAlltoallw}{\funsty{MPI\civlU{}Alltoallw}} \newcommand{\MPICommsize}{\funsty{MPI\civlU{}Comm\civlU{}size}} \newcommand{\MPICommrank}{\funsty{MPI\civlU{}Comm\civlU{}rank}} \newcommand{\MPIGetcount}{\funsty{MPI{\civlU}Get{\civlU}count}} \newcommand{\MPISendrecv}{\funsty{MPI{\civlU}Sendrecv}} \newcommand{\MPIBcast}{\funsty{MPI{\civlU}Bcast}} \newcommand{\MPIAllgather}{\funsty{MPI{\civlU}Allgather}} \newcommand{\MPICommdup}{\funsty{MPI{\civlU}Comm{\civlU}dup}} \newcommand{\MPICommfree}{\funsty{MPI{\civlU}Comm{\civlU}free}} \newcommand{\MPIScatter}{\funsty{MPI{\civlU}Scatter}} \newcommand{\MPIGather}{\funsty{MPI{\civlU}\-Gath\-er}} \newcommand{\MPIGatherv}{\funsty{MPI{\civlU}Gatherv}} \newcommand{\MPIScatterv}{\funsty{MPI{\civlU}Scatterv}} \newcommand{\MPIAlltoall}{\funsty{MPI{\civlU}Alltoall}} % types \newcommand{\MPIDatatype}{\typsty{MPI\civlU{}Datatype}} \newcommand{\MPIComm}{\typsty{MPI\civlU{}Comm}} \newcommand{\MPIStatus}{\typsty{MPI\civlU{}Status}} \newcommand{\MPIOp}{\typsty{MPI\civlU{}Op}} \newcommand{\MPIRequest}{\typsty{MPI\civlU{}Request}} % constants \newcommand{\MPICOMMWORLD}{\code{MPI\civlU{}COMM\civlU{}WORLD}} \newcommand{\MPIPROCNULL}{\code{MPI\civlU{}PROC\civlU{}NULL}} \newcommand{\MPIANYSOURCE}{\code{MPI\civlU{}ANY\civlU{}SOURCE}} \newcommand{\MPIANYTAG}{\code{MPI\civlU{}ANY\civlU{}TAG}} \newcommand{\MPISTATUSIGNORE}{\code{MPI\civlU{}STATUS\civlU{}IGNORE}} \newcommand{\MPIUNINIT}{\code{\civlU{}MPI\civlU{}UNINIT}} \newcommand{\MPIINIT}{\code{\civlU{}MPI\civlU{}INIT}} \newcommand{\MPIFINALIZED}{\code{\civlU{}MPI\civlU{}FINALIZED}} \newcommand{\REDUCETAG}{\code{\civlU{}REDUCE\civlU{}TAG}} % Displaying code... \newcounter{lc} % global variable for line count \DeclareRobustCommand{\showline}{% \stepcounter{lc}% {\scriptsize\makebox[1mm][r]{\textcolor{blue}{\arabic{lc}}}\hspace{.5mm}}% } \newenvironment{program}{% \linespread{1.0} \normalsize\tt\setcounter{lc}{0} \begin{tabular}{@{\showline{}\hspace{.2cm}}l@{}}% }{% \end{tabular}% } \newenvironment{programContinue}[1]{% \linespread{1.0} \normalsize\tt\setcounter{lc}{#1} \begin{tabular}{@{\showline{}\hspace{.2cm}}l@{}}% }{% \end{tabular}% } \newenvironment{programNoNum}{% \normalsize\tt\setcounter{lc}{0} \begin{tabular}{@{}l@{}}% }{% \end{tabular}% } \newenvironment{programSmall}{% \linespread{1.0} \footnotesize\tt\setcounter{lc}{0} \begin{tabular}{@{\showline{}\hspace{.2cm}}l@{}}% }{% \end{tabular}% } \newenvironment{programSuperSmall}{% \linespread{1.0} \scriptsize\tt\setcounter{lc}{0} \begin{tabular}{@{\showline{}\hspace{.2cm}}l@{}}% }{% \end{tabular}% } \newcommand{\transsep}[1]{ \vspace{-1.5mm}\par \begin{tabular}{@{}r@{}} \scriptsize\it\textcolor{blue}{#1}\\[-2.5mm] \rule{\columnwidth}{0.5pt}\\[-1.4mm] \scriptsize\it\textcolor{blue}{transformed to CIVL-C} \end{tabular} \vspace{-1.5mm}\par } \newenvironment{listing}{ \codesize\tt\setcounter{lc}{0} \begin{flushleft} }{ \end{flushleft} } \newcommand{\lno}{\showline \ } % CIVL-C keywords... \newcommand{\cckey}{\$} \newcommand{\cc}[1]{\mbox{\textcolor{blue}{\texttt{\cckey{}#1}}}} \newcommand{\cabstract}{\cc{abstract}} \newcommand{\cproc}{\cc{proc}} \newcommand{\cprocNull}{\cc{proc{\civlU}null}} \newcommand{\cself}{\cc{self}} \newcommand{\cinput}{\cc{input}} \newcommand{\coutput}{\cc{output}} \newcommand{\cspawn}{\cc{spawn}} \newcommand{\csystem}{\cc{system}} \newcommand{\catomicf}{\cc{atomic{\civlU}f}} \newcommand{\cwait}{\cc{wait}} \newcommand{\cwaitall}{\cc{waitall}} \newcommand{\cassert}{\cc{assert}} \newcommand{\ctrue}{\cc{true}} \newcommand{\cfalse}{\cc{false}} \newcommand{\cassume}{\cc{assume}} \newcommand{\catom}{\cc{atom}} \newcommand{\catomic}{\cc{atomic}} \newcommand{\cwhen}{\cc{when}} \newcommand{\cchoose}{\cc{choose}} \newcommand{\cchooseint}{\cc{choose{\civlU}int}} \newcommand{\cinvariant}{\cc{invariant}} \newcommand{\cexit}{\funsty{\$exit}} \newcommand{\cresult}{\cc{result}} \newcommand{\cat}{\texttt{@}} \newcommand{\ccollective}{\cc{collective}} \newcommand{\cequals}{\cc{equals}} \newcommand{\cfor}{\cc{for}} \newcommand{\cparfor}{\cc{parfor}} \newcommand{\cscope}{\cc{scope}} \newcommand{\cscoperoot}{\cc{root}} \newcommand{\chere}{\cc{here}} \newcommand{\cregion}{\cc{region}} \newcommand{\cmalloc}{\cc{malloc}} \newcommand{\cfree}{\cc{free}} \newcommand{\cforall}{\cc{forall}} \newcommand{\cexists}{\cc{exists}} \newcommand{\cimplies}{\ct{=>}} \newcommand{\crange}{\cc{range}} \newcommand{\cdomain}{\cc{domain}} \newcommand{\cdomainof}[1]{\cc{domain}\ct{(}#1\ct{)}} \newcommand{\clambda}{\cc{lambda}} %%% CIVL-C functions %%% \newcommand{\capply}{\funsty{\$apply}} \newcommand{\ccontains}{\funsty{\$contains}} \newcommand{\ccopy}{\funsty{\$copy}} \newcommand{\cscopeof}{\funsty{\$scopeof}} \newcommand{\cscopeparent}{\funsty{\$scope{\civlU}parent}} \newcommand{\cbundlesize}{\funsty{\$bundle{\civlU}size}} \newcommand{\cbundlepack}{\funsty{\$bundle{\civlU}pack}} \newcommand{\cbundleunpack}{\funsty{\$bundle{\civlU}unpack}} \newcommand{\cbundleunpackapply}{\funsty{\$bundle{\civlU}unpack{\civlU}apply}} \newcommand{\cmessagepack}{\funsty{\$message{\civlU}pack}} \newcommand{\cmessagesource}{\funsty{\$message{\civlU}source}} \newcommand{\cmessagetag}{\funsty{\$message{\civlU}tag}} \newcommand{\cmessagedest}{\funsty{\$message{\civlU}dest}} \newcommand{\cmessagesize}{\funsty{\$message{\civlU}size}} \newcommand{\cmessageunpack}{\funsty{\$message{\civlU}unpack}} \newcommand{\ccommsize}{\funsty{\$comm{\civlU}size}} \newcommand{\ccommplace}{\funsty{\$comm{\civlU}place}} \newcommand{\ccommseek}{\funsty{\$comm{\civlU}seek}} \newcommand{\ccommprobe}{\funsty{\$comm{\civlU}probe}} \newcommand{\ccommcreate}{\funsty{\$comm{\civlU}create}} \newcommand{\ccommdestroy}{\funsty{\$comm{\civlU}destroy}} \newcommand{\ccommenqueue}{\funsty{\$comm{\civlU}enqueue}} \newcommand{\ccommdequeue}{\funsty{\$comm{\civlU}dequeue}} \newcommand{\cgcommcreate}{\funsty{\$gcomm{\civlU}create}} \newcommand{\cgcommdestroy}{\funsty{\$gcomm{\civlU}destroy}} \newcommand{\cgcommdup}{\funsty{\$gcomm{\civlU}dup}} \newcommand{\cgbarriercreate}{\funsty{\$gbarrier{\civlU}create}} \newcommand{\cbarriercreate}{\funsty{\$barrier{\civlU}create}} \newcommand{\cbarriercall}{\funsty{\$barrier{\civlU}call}} \newcommand{\cbarrierenter}{\funsty{\$barrier{\civlU}enter}} \newcommand{\cbarrierexit}{\funsty{\$barrier{\civlU}exit}} \newcommand{\cgbarrierdestroy}{\funsty{\$gbarrier{\civlU}destroy}} \newcommand{\cbarrierdestroy}{\funsty{\$barrier{\civlU}destroy}} \newcommand{\ccollectcheck}{\funsty{\$collator{\civlU}check}} \newcommand{\cgcheckercreate}{\funsty{\$gcollator{\civlU}create}} \newcommand{\cgcheckerdestroy}{\funsty{\$gcollator{\civlU}destroy}} \newcommand{\ccheckercreate}{\funsty{\$collator{\civlU}create}} \newcommand{\ccheckerdestroy}{\funsty{\$collator{\civlU}destroy}} \newcommand{\cpointeradd}{\funsty{\$pointer{\civlU}add}} \newcommand{\cseqinit}{\funsty{\$seq{\civlU}init}} \newcommand{\cseqlen}{\funsty{\$seq{\civlU}length}} \newcommand{\cseqinsert}{\funsty{\$seq{\civlU}insert}} \newcommand{\cseqrm}{\funsty{\$seq{\civlU}remove}} \newcommand{\cseqapp}{\funsty{\$seq{\civlU}append}} \newcommand{\cnexttimecount}{\funsty{\$next{\civlU}time\civlU{}count}} \newcommand{\celaborate}{\funsty{\$elaborate}} \newcommand{\cmpisend}{\funsty{\$mpi\civlU{}send}} \newcommand{\cmpirecv}{\funsty{\$mpi\civlU{}recv}} \newcommand{\cmpisendrecv}{\funsty{\$mpi\civlU{}sendrecv}} \newcommand{\csizeofdatatype}{\funsty{sizeofDatatype}} \newcommand{\cmpicheckbuffer}{\funsty{\$mpi\civlU{}check\civlU{}buffer}} \newcommand{\cmpicreatecoroutineentry}{\funsty{\$mpi\civlU{}create\civlU{}routine\civlU{}entry}} \newcommand{\cmpidiffcoroutineentries}{\funsty{\$mpi\civlU{}diff\civlU{}coroutine\civlU{}entries}} \newcommand{\cmpireduce}{\funsty{\$mpi\civlU{}reduce}} \newcommand{\cmpicollectivesend}{\funsty{\$mpi\civlU{}collective\civlU{}send}} \newcommand{\cmpicollectiverecv}{\funsty{\$mpi\civlU{}collective\civlU{}recv}} \newcommand{\cmpibcast}{\funsty{\$mpi\civlU{}bcast}} \newcommand{\cmpigather}{\funsty{\$mpi\civlU{}gather}} \newcommand{\cmpigatherv}{\funsty{\$mpi\civlU{}gatherv}} \newcommand{\cmpiscatter}{\funsty{\$mpi\civlU{}scatter}} \newcommand{\cmpiscatterv}{\funsty{\$mpi\civlU{}scatterv}} \newcommand{\cmpipointeradd}{\funsty{\$mpi\civlU{}pointer\civlU{}add}} \newcommand{\cmpinewgcomm}{\funsty{\$mpi\civlU{}new\civlU{}gcomm}} \newcommand{\cmpigetgcomm}{\funsty{\$mpi\civlU{}get\civlU{}gcomm}} \newcommand{\cmpicommdup}{\funsty{\$mpi\civlU{}comm\civlU{}dup}} \newcommand{\cmpicommfree}{\funsty{\$mpi\civlU{}comm\civlU{}free}} \newcommand{\cmpirootscope}{\funsty{\$mpi\civlU{}root\civlU{}scope}} \newcommand{\cmpiprocscope}{\funsty{\$mpi\civlU{}proc\civlU{}scope}} \newcommand{\cmpiassertconsistbtype}{\funsty{\$mpi\civlU{}assert\civlU{}consistent\civlU{}basetype}} \newcommand{\cmpitime}{\funsty{\$mpi\civlU{}time}} \newcommand{\cmpigcommcreate}{\funsty{\$mpi\civlU{}gcomm\civlU{}create}} \newcommand{\cmpigcommdestroy}{\funsty{\$mpi\civlU{}gcomm\civlU{}destroy}} \newcommand{\cmpicommcreate}{\funsty{\$mpi\civlU{}comm\civlU{}create}} \newcommand{\cmpicommdestroy}{\funsty{\$mpi\civlU{}comm\civlU{}destroy}} \newcommand{\cmpigcomm}{\funsty{\$mpi\civlU{}gcomm}} \newcommand{\cmpicomm}{\funsty{\$mpi\civlU{}comm}} %%% CIVL-C types %%% \newcommand{\cbarrier}{\typsty{\$barrier}} \newcommand{\cgbarrier}{\typsty{\$gbarrier}} \newcommand{\cqueue}{\typsty{\$queue}} \newcommand{\cbundle}{\typsty{\$bundle}} \newcommand{\cmessage}{\typsty{\$message}} \newcommand{\ccomm}{\typsty{\$comm}} \newcommand{\cgcomm}{\typsty{\$gcomm}} \newcommand{\ccollectchecker}{\typsty{\$collator}} \newcommand{\ccollator}{\typsty{\$collator}} \newcommand{\cgcollectchecker}{\typsty{\$gcollator}} \newcommand{\ccollectrecord}{\typsty{\$collator{\civlU}entry}} \newcommand{\coperation}{\typsty{\$operation}} \newcommand{\cgcollator}{\typsty{\$gcollator}} \newcommand{\cmpistate}{\typsty{\$mpi\civlU{}state}} %%%C keywords%%% \newcommand{\typedef}{\ccode{typedef}} \newcommand{\enum}{\ccode{enum}} \newcommand{\struct}{\ccode{struct}} \newcommand{\void}{\ccode{void}} \newcommand{\inttype}{\ccode{int}} \newcommand{\cchar}{\ccode{char}} \newcommand{\cdouble}{\ccode{double}} \newcommand{\creturn}{\ccode{return}} \newcommand{\cif}{\ccode{if}} \newcommand{\sizeof}{\ccode{sizeof}} \newcommand{\bool}{\ccode{sizeof{\civlU}Bool}} \newcommand{\cconst}{\ccode{const}} \newcommand{\memset}{\ccode{memset}} \newcommand{\cmemcpy}{\ccode{memcpy}} %%%% Mini-language %%%% \newcommand{\minibarrier}{\texttt{\textcolor{pink}{barrier}}} \newcommand{\mininprocs}{\texttt{\textcolor{pink}{nprocs}}} \newcommand{\miniproc}{\texttt{\textcolor{pink}{proc}}} \newcommand{\minipid}{\texttt{\textcolor{pink}{pid}}} \newcommand{\minisend}[2]{\texttt{\textcolor{pink}{send} #1 \textcolor{pink}{to} #2}} \newcommand{\minirecv}[2]{\texttt{\textcolor{pink}{recv} #1 \textcolor{pink}{from} #2}} \newcommand{\miniwildcard}[1]{\texttt{\textcolor{pink}{any} #1}} \newcommand{\miniassert}[1]{\texttt{\textcolor{pink}{assert #1}}} \newcommand{\minireturn}{\texttt{\textcolor{pink}{return}}} \newcommand{\miniwhile}{\texttt{\textcolor{pink}{while}}} \newcommand{\miniif}{\texttt{\textcolor{pink}{if}}} \newcommand{\minielse}{\texttt{\textcolor{pink}{else}}} %%%% propertes %%%% %\newcommand{\prop}[1]{\textbf{F\textsf{#1}}} \newcommand{\prop}[1]{\textsf{#1}} %%%% variables %%%% \newcommand{\NP}{\texttt{NP}} %%%% chapter symbol %%%% \newcommand{\Chp}{Chapter } %%%% MINIMP %%%% \newcommand{\send}[2]{\ccode{send} #1 \ccode{to} #2} \newcommand{\recv}[2]{\ccode{recv} #1 \ccode{from} #2} \newcommand{\recvany}[2]{\ccode{recv} #1 \ccode{from any} #2} %%%%%%%%%%%%%% %%%% notations %%%% \newcommand{\enque}[2]{\mymath{#1\texttt{!}#2}} \newcommand{\deque}[2]{\mymath{#1\texttt{?}#2}} \newcommand{\lco}{\langle} \newcommand{\rco}{\rangle} \newcommand{\cocond}[1]{\lco{}#1\rco{}} \newcommand{\proc}{\texttt{p}} \newcommand{\eval}{\texttt{eval}} \newcommand{\Var}{\texttt{Var}} \newcommand{\len}{\texttt{len}} \newcommand{\ttC}{\texttt{c}} \newcommand{\ttE}{\texttt{e}} \newcommand{\ttI}{\texttt{i}} \newcommand{\ttJ}{\texttt{j}} \newcommand{\ttK}{\texttt{k}} \newcommand{\ttN}{\texttt{n}} \newcommand{\model}{\mathcal{M}} \newcommand{\progseg}[3]{#1{\colon}#2~{#3}} \newcommand{\progsegs}[5]{#1{\colon}#2~{#3}\colon{}#4~{#5}} \newcommand{\vocab}{\mathcal{V}} \newcommand{\corule}{\mathcal{R}} \newcommand{\mylabel}{\mathcal{L}} \newcommand{\mytxcmt}[1]{\textcolor{red}{#1}} \newcommand{\dom}{\textsf{Val}} \newcommand{\sym}{\textsf{Sym}} \newcommand{\symexpr}{\exprv_{\dom{}\cup{}\textsf{Sym}}} \newcommand{\pathcond}{\textsf{pc}} \newcommand{\mypathcond}{\textsf{PC}} \newcommand{\myundef}{\textsf{UNDEF}} \newcommand{\domtmp}{\textsf{Val}} %\newcommand{\nprocs}[1]{\mathbb{N}^{<#1}} \newcommand{\nprocs}[1]{[#1]} \newcommand{\minimp}[0]{\textsc{MiniMP}} \newcommand{\minispec}[0]{\textsc{MiniSpec}} \newcommand{\mcalgo}[0]{\textsc{Mc}} \newcommand{\mcalgodelta}[0]{\textsc{Mc}$^\Delta$} \newcommand{\emana}[0]{\textsf{emanate}} \newcommand{\errorpaths}[0]{\leadsto^*_{\textsf{error}}} \newcommand{\mayInterfere}[0]{\textsf{mayInterfere}} %% \newcommand{\var}[0]{\textsf{Var}} \newcommand{\myprocedure}[0]{\textsf{Procedure}} \newcommand{\globvar}[0]{\textsf{Global}} \newcommand{\locvar}[0]{\textsf{locvar}} \newcommand{\stmt}[0]{\textsf{AStmt}_{\vocab}} \newcommand{\exprv}[0]{\textsf{Expr}} \newcommand{\sexprv}[0]{\textsf{SExpr}} \newcommand{\seventv}[0]{\textsf{SEvent}} \newcommand{\sabsentv}[0]{\textsf{SAbsent}} \newcommand{\bexprv}[0]{\textsf{BExpr}} \newcommand{\pexprv}[0]{\textsf{PExpr}} \newcommand{\transT}[0]{\textsf{transStmt}} \newcommand{\myskipstmt}[0]{\textsf{skip}} \newcommand{\myrettostmt}[2]{\textsf{return }#1\textsf{ to }#2} \newcommand{\myemptyguard}[0]{\textsf{empty}} \newcommand{\myallemptyguard}[0]{\textsf{allempty}} \newcommand{\myframes}[0]{\textsf{Frame}} \newcommand{\myframe}[0]{\textsf{frame}} \newcommand{\myprocStates}[0]{\textsf{ProcState}} \newcommand{\myprocState}[0]{\textsf{procState}} \newcommand{\myprocGraphFunc}[0]{\textsf{pg}} \newcommand{\mymem}[0]{\textsf{mem}} \newcommand{\mygmem}[0]{\textsf{gmem}} \newcommand{\mystack}[0]{\textsf{stack}} \newcommand{\mychan}[0]{\textsf{chan}} \newcommand{\mystate}[0]{\textsf{state}} \newcommand{\mystates}[0]{\textsf{State}} \newcommand{\mytop}[0]{\textsf{top}} \newcommand{\mytoploc}[0]{\textsf{toploc}} \newcommand{\mynp}[0]{\textsf{np}} \newcommand{\myhead}[0]{\textsf{head}} \newcommand{\mytail}[0]{\textsf{tail}} \newcommand{\myloc}[0]{\textsf{Loc}} \newcommand{\mynexts}[0]{\textsf{nexts}} \newcommand{\mysrc}[0]{\textsf{src}} \newcommand{\mydest}[0]{\textsf{dest}} \newcommand{\myproc}[0]{\textsf{proc}} \newcommand{\myact}[0]{\textsf{act}} \newcommand{\mypathtrans}[0]{\textsf{Tr}} \newcommand{\mypathstates}[0]{\textsf{St}} \newcommand{\myabsentpred}[3]{\textsf{no }#1\textsf{ after }#2\textsf{ until }#3} \newcommand{\myenter}[0]{\textsf{enter}} \newcommand{\myexit}[0]{\textsf{exit}} \newcommand{\myproj}[1]{\textsf{proj}_{#1}} \newcommand{\mypre}[0]{\textsf{pre}} \newcommand{\myaeval}[1]{\myeval{#1}^{\textsf{absent}}} \newcommand{\myseval}[1]{\myeval{#1}^{\textsf{spec}}} \newcommand{\mypeval}[3]{\textsf{pe}(#1, #2, #3)} \newcommand{\mypevaltitle}[0]{\textsf{pe}} %% actions %% acsls \newcommand{\acslold}{\ccode{\BSL{}old}} \newcommand{\acslon}{\ccode{\BSL{}on}} \newcommand{\acslforall}{\ccode{\BSL{}forall}} \newcommand{\acslexists}{\ccode{\BSL{}exists}} \newcommand{\acslresult}{\ccode{\BSL{}result}} \newcommand{\acslsend}{\ccode{\BSL{}send}} \newcommand{\acslenter}{\ccode{\BSL{}enter}} \newcommand{\acslexit}{\ccode{\BSL{}exit}} \newcommand{\acslabsent}[3]{\ccode{\BSL{}no} #1 \ccode{\BSL{}after} #2 \ccode{\BSL{}until} #3} \newcommand{\acslgamma}[3]{\acslabsent{\acslsend{(#1, #2)}}{\acslexit{(#1)}}{\acslexit{(#3)}}} \newcommand{\acslguarantee}[3]{\acslabsent{\acslsend{(#1, #2)}}{\acslenter{(#1)}}{\acslenter{(#3)}}} \newcommand{\acslwaitsfor}[2]{\acslabsent{\acslexit{(#1)}}{\acslenter{(#1)}}{\acslenter{(#2)}}} %% \newcommand{\myactskip}[0]{\textsf{skip}} \newcommand{\myactassign}[2]{#1\texttt{ = }#2} \newcommand{\myactret}[1]{\textsf{ret #1}} \newcommand{\myactretto}[1]{\textsf{assignRetTo} #1} \newcommand{\myactsend}[2]{\textsf{send(#1, #2)}} \newcommand{\myactrecv}[2]{\textsf{recv(#1, #2)}} \newcommand{\myactrefresh}[0]{\textsf{refresh}} %% end-of-actions %% %% #recvs and #sends \newcommand{\mynsends}[3]{\textsf{nsends}_{#1}(#2, #3)} \newcommand{\mynrecvs}[3]{\textsf{nrecvs}_{#1}(#2, #3)} \newcommand{\myinterfere}[2]{\textsf{interfere}_{#1}^{#2}} \newcommand{\mycspre}[2]{\textsf{preCS}({#1}, {#2})} \newcommand{\mycspost}[2]{\textsf{postCS}({#1}, {#2})} \newcommand{\myCoChanPre}[0]{\textsf{preCoChan}} \newcommand{\myCoChanPost}[0]{\textsf{postCoChan}} %% %% %% \newcommand{\tri}[0]{\textsf{tri}} \newcommand{\Tri}[0]{\textsf{Tri}} \newcommand{\ruleguarantee}{\textsf{guarantees}} \newcommand{\ruleinfer}[3]{#1\textsf{ and }#2\textsf{ infer }#3} \newcommand{\myruleinfer}[4]{#1\textsf{ and }#2\textsf{ infer$_{#4}$ } #3} \newcommand{\nosendsubset}{\textsf{noSend}} \newcommand{\rulecancels}{\textsf{cancels}} %% \newcommand{\mymath}[1]{\mathit{#1}} \newcommand{\myeval}[1]{[\![\mymath{#1}]\!]} \newcommand{\coLoc}{\mymath{coLoc}} \newcommand*{\tran}[2]{\genfrac{}{}{0pt}{}{#1}{#2}} \newcommand{\param}{\vspace{7mm}} \newcommand{\tranin}[2]{#1\textbf{\textit{ in }}#2} \newcommand{\cotriple}{\lco{}\psi,\,\Gamma{}\rco{}~\progseg{l}{C}{l'}~\lco{}\phi,\,\Upsilon{}\rco{}} \newcommand{\cotriplenoloc}{\lco{}\psi,\,\Gamma{}\rco{}~C~\lco{}\phi,\,\Upsilon{}\rco{}} \newcommand{\cotriplearg}[1]{\lco{}\psi,\,\Gamma{}\rco{}~#1~\lco{}\phi,\,\Upsilon{}\rco{}} \newcommand{\cosubtriple}[1]{\lco{}\psi_{#1},\,\Gamma_{#1}\rco{}~C_{#1}~\lco{}\phi_{#1},\,\Upsilon_{#1}\rco{}} %%%% \mycosubtriple: subscript, pre, post, progseg: \newcommand{\mycosubtriple}[4]{\lco{}{#2},\,\Gamma_{#1}\rco{}~{#4}~\lco{}{#3},\,\Upsilon_{#1}\rco{}} %%%% \newcommand{\cosubtripleloc}[3]{\lco{}\psi_{#1},\,\Gamma_{#1}\rco{}~#2{:}C_{#1}\texttt{;}#3~\lco{}\phi_{#1},\,\Upsilon_{#1}\rco{}} \newcommand{\cotripleloc}{\lco{}\psi,\,\Gamma{}\rco{}~l{:}C\texttt{;}l'~\lco{}\phi,\,\Upsilon{}\rco{}} \newcommand{\cotripleseq}[2]{\lco{}\psi,\,\Gamma{}\rco{}~C_{#1}\texttt{;}C_{#2}~\lco{}\phi,\,\Upsilon{}\rco{}} \newcommand{\cotripleseqloc}[2]{\lco{}\psi,\,\Gamma{}\rco{}~l{:}C_{#1}\texttt{;}l'{:}C_{#2}~\lco{}\phi,\,\Upsilon{}\rco{}} \newcommand{\PID}{\texttt{PID}} \newcommand{\mygamma}[3]{\BSL{}absent(\BSL{}send($#1$, $#2$), \BSL{}exit($#1$), \BSL{}exit($#3$))} \newcommand{\mywaitsfor}[2]{\BSL{}absent(\BSL{}exit($#1$), \BSL{}enter($#1$), \BSL{}enter($#2$))} \newcommand{\myguaranty}[3]{\BSL{}absent(\BSL{}send($#1$, $#2$), \BSL{}enter($#1$), \BSL{}enter($#3$))} \newcommand{\mygammaVal}[4]{absent(send($#1$, $#2$), exit$_{#4}$($#1$), exit$_{#4}$($#3$))} \newcommand{\mywaitsforVal}[4]{absent(exit$_{#4}$($#1$), enter$_{#3}$($#1$), enter$_{#3}$($#2$))} \newcommand{\myguarantyVal}[4]{absent(send($#1$, $#2$), enter$_{#4}$($#1$), enter$_{#4}$($#3$))} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \newcommand{\mygammaMPI}[2]{\BSL{}absenceof \BSL{}sendfrom($#1$, $#2$) \BSL{}after \BSL{}exit($#1$) \BSL{}until \BSL{}exit} \newcommand{\mywaitsforMPI}[1]{\BSL{}absenceof \BSL{}exit \BSL{}after \BSL{}enter \BSL{}until \BSL{}exit(#1)} \newcommand{\myguarantyMPI}[3]{\BSL{}absenceof \BSL{}sendto($#1$, $#2$) \BSL{}after \BSL{}enter \BSL{}until \BSL{}enter($#3$)} \newcommand{\mygammaCIVL}[2]{\$absent\U{}sendfrom($#1$, $#2$)} \newcommand{\mywaitsforCIVL}[1]{\$absent\U{}exit($#1$)} \newcommand{\myguarantyCIVL}[3]{\$absent\U{}sendto($#1$, $#2$, $#3$)} \newcommand{\myseqrule}[0]{ $\frac{ \cocond{\psi, \Gamma_0}~C_0~\cocond{\delta, \Upsilon_0},\, \cocond{\delta, \Gamma_1}~C_1~\cocond{\phi, \Upsilon_1} }{ \cocond{\psi, \Gamma}~C_0\texttt{;}C_1~\cocond{\phi, \Upsilon} }$ } \newcommand{\indepcond}[4]{ $#1 \vdash{} exit^{#2}_{#3} \preceq{} t_{#3} \preceq{} t_{#4} \preceq{} exit^{#2}_{#4}$ } %%%%%%%%%%%%%%%%%%%%%%%%%% Tool %%%%%%%%%%%%%%%%%%%%