definitions.tex

%!TEX root = dissertation.tex

\usepackage{stackrel}

%% types

\newcommand{\setlocations}{\ensuremath{\mathbb{L}}}
\newcommand{\setvalues}{\ensuremath{\mathbb{V}}}
\newcommand{\setintegers}{\ensuremath{\mathbb{Z}}}
\newcommand{\setnaturals}{\ensuremath{\mathbb{N}}}
\newcommand{\setpositives}{\ensuremath{\mathbb{N}^+}}
\newcommand{\setidentifiers}{\ensuremath{\mathbb{I}}}
\newcommand{\setbooleans}{\ensuremath{\mathbb{B}}}
\newcommand{\setprocessors}{\ensuremath{\mathbb{P}}}

%% abbreviations

\newcommand{\setstacks}{\ensuremath{\mathbf{Stack}}}
\newcommand{\setheaps}{\ensuremath{\mathbf{Heap}}}
\newcommand{\setbuffers}{\ensuremath{\mathbf{Buf}}}
\newcommand{\setshares}{\ensuremath{\mathbf{Share}}}
\newcommand{\setperms}{\ensuremath{\mathbf{Perm}}}
\newcommand{\setastates}{\ensuremath{\mathit{\Sigma}}}
\newcommand{\setstates}{\ensuremath{\mathbf{State}}}
\newcommand{\setmodels}{\ensuremath{\mathbf{Model}}}
\newcommand{\setmemorysystems}{\ensuremath{\mathbf{Mem}}}
\newcommand{\setpstates}{\ensuremath{\Pi}}
\newcommand{\setmpstates}{\ensuremath{\mathbf{MPState}}}
\newcommand{\setresolvers}{\ensuremath{\mathbf{Resolver}}}
\newcommand{\setconfigurations}{\ensuremath{\mathbf{Config}}}
\newcommand{\setmconfigurations}{\ensuremath{\mathbf{MConfig}}}
\newcommand{\setassertions}{\ensuremath{\mathbf{Asrt}}}

%% operators 

\DeclareMathOperator{\op}{\mathit{op}}
\DeclareMathOperator{\opskip}{\mathsf{skip}}
\DeclareMathOperator{\opfence}{\mathsf{fence}}
\DeclareMathOperator{\opassume}{\mathsf{assume}}
\DeclareMathOperator{\opassert}{\mathsf{assert}}
\DeclareMathOperator{\opassign}{:\!=}
\DeclareMathOperator{\opequals}{=}
\DeclareMathOperator{\opseq}{;}
\DeclareMathOperator{\opchoice}{+}
\DeclareMathOperator{\oppar}{|\!|}
\DeclareMathOperator{\oploop}{\ast}
\DeclareMathOperator{\oplock}{\mathsf{lock}}
\DeclareMathOperator{\opunlock}{\mathsf{unlock}}
\DeclareMathOperator{\opcons}{\mathsf{cons}}
\DeclareMathOperator{\opnew}{\mathsf{new}}
\DeclareMathOperator{\opalloc}{\mathsf{alloc}}
\DeclareMathOperator{\opdispose}{\mathsf{free}}
\DeclareMathOperator{\opif}{\mathsf{if\,}}
\DeclareMathOperator{\opthen}{\mathsf{\,then\,}}
\DeclareMathOperator{\opelse}{\mathsf{\,else}}
\DeclareMathOperator{\opwhile}{\mathsf{while\,}}
\DeclareMathOperator{\opdo}{\mathsf{\,do\,}}
\DeclareMathOperator{\oplocal}{\mathsf{local\,}}
\DeclareMathOperator{\opin}{\mathsf{\,in\,}}
\DeclareMathOperator{\opresource}{\mathsf{resource\,}}
\DeclareMathOperator{\opwith}{\mathsf{with\,}}
\DeclareMathOperator{\opwhen}{\mathsf{\,when\,}}
\DeclareMathOperator{\nil}{\emptyset}
\DeclareMathOperator{\compat}{\smile}


%% primitive commands

\newcommand{\cskip}[0]{\ensuremath{\opskip}}
\newcommand{\cfence}[0]{\ensuremath{\opfence}}
\newcommand{\clock}[0]{\ensuremath{\oplock}}
\newcommand{\cunlock}[0]{\ensuremath{\opunlock}}
\newcommand{\cassume}[1]{\ensuremath{\opassume(#1)}}
\newcommand{\cassert}[1]{\ensuremath{\opassert(#1)}}
\newcommand{\cassign}[2]{\ensuremath{#1 \opassign #2}}
\newcommand{\cload}[2]{\ensuremath{#1 \opassign \left[ #2 \right]}}
\newcommand{\cstore}[2]{\ensuremath{\left[ #1 \right] \opassign #2}}
\newcommand{\cnew}[2]{\ensuremath{#1 \opassign \opnew(#2)}}
\newcommand{\calloc}[1]{\ensuremath{#1 \opassign \opalloc}}
\newcommand{\ccons}[3]{\ensuremath{#1 \opassign \opcons(#2, #3)}}
\newcommand{\cfree}[1]{\ensuremath{\opdispose(#1)}}

%% commands

\newcommand{\cseq}[2]{\ensuremath{#1 \opseq #2}}
\newcommand{\cchoice}[2]{\ensuremath{#1 \opchoice #2}}
\newcommand{\cpar}[2]{\ensuremath{#1 \oppar #2}}
\newcommand{\cifthenelse}[3]{\ensuremath{\opif #1 \opthen #2 \opelse #3}}
\newcommand{\cifthen}[2]{\ensuremath{\opif #1 \opthen #2}}
\newcommand{\cwhile}[2]{\ensuremath{\opwhile #1 \opdo #2}}
\newcommand{\cloop}[1]{\ensuremath{#1^{\oploop}}}
\newcommand{\clocal}[3]{\ensuremath{\oplocal #1 \opassign #2 \opin #3}}
\newcommand{\cres}[2]{\ensuremath{\opresource #1 \opin #2}}
\newcommand{\cwith}[2]{\ensuremath{\left\langle #2\right\rangle_{#1}}}
% \newcommand{\cwith}[2]{\ensuremath{\opwith #1 \opdo #2}}
\newcommand{\catomic}[1]{\ensuremath{\left\langle #1 \right\rangle}}
\newcommand{\ccas}[2]{\ensuremath{\mathsf{cas}_{#1}(#2)}}

\newcommand{\exprs}{\ensuremath{\mathbf{Expr}}}
\newcommand{\fracs}{\ensuremath{\mathbf{Frac}}}
\newcommand{\bexprs}{\ensuremath{\mathbf{BExpr}}}
\newcommand{\pcomms}{\ensuremath{\mathbf{PComm}}}
\newcommand{\comms}{\ensuremath{\mathbf{Comm}}}
\newcommand{\asserts}{\ensuremath{\mathbf{Assert}}}
\newcommand{\progs}{\ensuremath{\mathbf{Prog}}}

\newcommand{\dnexpr}[1]{\ensuremath{\mathcal{E}[\![#1]\!]}}
\newcommand{\dnshare}[1]{\ensuremath{\mathcal{S}[\![#1]\!]}}
\newcommand{\dnbexpr}[1]{\ensuremath{\mathcal{B}[\![#1]\!]}}
\newcommand{\dnpcomm}[1]{\ensuremath{\mathcal{P}[\![#1]\!]}}
\newcommand{\dna}[1]{\ensuremath{\mathcal{A}[\![#1]\!]}}
\newcommand{\dnfrac}[1]{\ensuremath{\mathcal{F}[\![#1]\!]}}

\newcommand{\sflush}[1]{\ensuremath{\mathit{flush}(#1)}}
\newcommand{\speek}[2]{\ensuremath{\mathit{peek}_{#1}(#2)}}
\newcommand{\sval}[1]{\ensuremath{\mathit{val}(#1)}}
\newcommand{\spush}[3]{\ensuremath{\mathit{push}_{#1}^{#2}(#3)}}
\newcommand{\alloc}[1]{\ensuremath{\mathit{alloc}(#1)}}
\newcommand{\allocat}[2]{\ensuremath{\mathit{alloc}_{#1}(#2)}}
\newcommand{\owned}[1]{\ensuremath{\mathit{owned}(#1)}}
\newcommand{\full}[1]{\ensuremath{\mathit{full}(#1)}}

\newcommand{\step}{\ensuremath{\rightarrow}}
\newcommand{\rtstep}{\ensuremath{\stackrel{\ast}{\rightarrow}}}
\newcommand{\nostep}{\ensuremath{\nrightarrow}}
\newcommand{\pstep}[1]{\ensuremath{\underset{#1}{\rightarrow}}}
\newcommand{\taustep}{\pstep{\tau}}
\newcommand{\modstep}{\pstep{\widehat{\tau}}}

\newcommand{\fv}[1]{\ensuremath{\mathrm{fv}(#1)}}
\renewcommand{\mod}[1]{\ensuremath{\mathrm{mod}(#1)}}

\newcommand{\bexpt}{\ensuremath{\mathbf{true}}}
\newcommand{\bexpf}{\ensuremath{\mathbf{false}}}


\newcommand{\spec}[4]{\ensuremath{#1\,\vdash\,\set{#2}\;#3\;\set{#4}}}
\newcommand{\truespec}[4]{\ensuremath{#1\,\models\,\set{#2}\;#3\;\set{#4}}}
\newcommand{\proofof}[1]{\ensuremath{\overline{#1}}}
\newcommand{\andif}{\ensuremath{\text{\;\;\;and\;\;\;}}}
\newcommand{\htriple}[3]{\ensuremath{\set{#1}\;#2\;\set{#3}}}
\newcommand{\triple}[3]{\ensuremath{\vdash\,\set{#1}\;#2\;\set{#3}}}
\newcommand{\truetriple}[3]{\ensuremath{\models\,\set{#1}\;#2\;\set{#3}}}

\newcommand{\safe}[2]{\ensuremath{\mathit{safe}_{#1}(#2)}}

\newcommand{\defined}[1]{\ensuremath{\mathsf{def}(#1)}}

\newcommand{\abort}{\ensuremath{\zorch}}

\newcommand{\live}[1]{\ensuremath{\mathit{live}(#1)}}

\newcommand{\femp}{\ensuremath{\mathbf{emp}}}
\newcommand{\fbar}[1]{\ensuremath{\mathbf{bar}_{#1}}}
\newcommand{\flock}[1]{\ensuremath{\mathbf{lock}_{#1}}}
\newcommand{\fexp}[1]{\ensuremath{\mathbf{exp}({#1})}}
\newcommand{\ftop}[1]{\ensuremath{\mathbf{top}_{#1}}}
%\newcommand{\fwrite}[1]{\ensuremath{\!\stackrel{#1}{\leadsto}\!}}
\newcommand{\fwrite}[1]{\ensuremath{\!\leadsto_{#1}\!}}
\newcommand{\fwrote}[1]{\ensuremath{\rightarrowtail_{#1}}}
\newcommand{\fpointsto}{\ensuremath{\!\mapsto\!}}
\newcommand{\fiter}[1]{\ensuremath{#1^{\ast}}}

\newcommand{\gensym}{\bullet}
\newcommand{\sepsym}{\ast}
\newcommand{\seqsym}{\vartriangleleft}
\newcommand{\sseqsym}{\blacktriangleleft}
\newcommand{\hashsym}{\#}

\DeclareMathOperator{\fhash}{\,\#\,}
\DeclareMathOperator{\fsep}{\,\ast\,}
\DeclareMathOperator{\fseq}{\,\vartriangleleft\,}
\DeclareMathOperator{\fsseq}{\,\blacktriangleleft\,}
\DeclareMathOperator{\fseqc}{\,\vartriangleright\,}
\DeclareMathOperator{\fsseqc}{\,\blacktriangleright\,}
\DeclareMathOperator{\fsepi}{\,\relbar\!\!\!\ast\,}
\DeclareMathOperator{\fseqli}{\,\relbar\!\vartriangleleft\,}
\DeclareMathOperator{\fseqri}{\,\vartriangleleft\!\relbar\,}
\DeclareMathOperator{\fsepic}{\,\ast\!\!\!\relbar\,}
\DeclareMathOperator{\fseqlic}{\,\vartriangleright\!\relbar\,}
\DeclareMathOperator{\fseqric}{\,\relbar\!\vartriangleright\,}
\DeclareMathOperator{\fgen}{\bullet}


\DeclareMathOperator{\shash}{\,\widetilde{\#}\,}
\DeclareMathOperator{\ssep}{\,\widetilde{\ast}\,}
\DeclareMathOperator{\sseq}{\,\widetilde{\vartriangleleft}\,}
\DeclareMathOperator{\ssseq}{\,\widetilde{\blacktriangleleft}\,}
\DeclareMathOperator{\sseqc}{\,\widetilde{\vartriangleright}\,}
\DeclareMathOperator{\ssseqc}{\,\widetilde{\blacktriangleright}\,}
\DeclareMathOperator{\ssepi}{\,\widetilde{\relbar\!\!\ast}\,}
\DeclareMathOperator{\sseqli}{\,\widetilde{\relbar\!\vartriangleleft}\,}
\DeclareMathOperator{\sseqri}{\,\widetilde{\vartriangleleft\!\relbar}\,}
\DeclareMathOperator{\ssepic}{\,\widetilde{\ast\!\!\relbar}\,}
\DeclareMathOperator{\sseqlic}{\,\widetilde{\vartriangleright\!\relbar}\,}
\DeclareMathOperator{\sseqric}{\,\widetilde{\relbar\!\vartriangleright}\,}
\DeclareMathOperator{\sgen}{\widetilde{\bullet}}

\DeclareMathOperator{\mhash}{\,\widehat{\#}\,}
\DeclareMathOperator{\msep}{\,\widehat{\ast}\,}
\DeclareMathOperator{\mseq}{\,\widehat{\vartriangleleft}\,}
\DeclareMathOperator{\msseq}{\,\widehat{\blacktriangleleft}\,}
\DeclareMathOperator{\mseqc}{\,\widehat{\vartriangleright}\,}
\DeclareMathOperator{\msseqc}{\,\widehat{\blacktriangleright}\,}
\DeclareMathOperator{\msepi}{\,\widehat{\relbar\!\!\ast}\,}
\DeclareMathOperator{\mseqli}{\,\widehat{\relbar\!\vartriangleleft}\,}
\DeclareMathOperator{\mseqri}{\,\widehat{\vartriangleleft\!\relbar}\,}
\DeclareMathOperator{\msepic}{\,\widehat{\ast\!\!\relbar}\,}
\DeclareMathOperator{\mseqlic}{\,\widehat{\vartriangleright\!\relbar}\,}
\DeclareMathOperator{\mseqric}{\,\widehat{\relbar\!\vartriangleright}\,}
\DeclareMathOperator{\mgen}{\widehat{\bullet}}


\newcommand{\amod}{\ensuremath{\mathcal{M}}}



\newcommand{\fbaru}{\ensuremath{\mathbf{bar}}}
\newcommand{\fwriteu}{\ensuremath{\!\leadsto\!}}

\newcommand{\pred}[1]{\ensuremath{[\![#1]\!]}}
\newcommand{\locked}[1]{\ensuremath{\mathit{locked}(#1)}}
\newcommand{\taurefines}{\ensuremath{\preceq}}
\newcommand{\modrefines}{\ensuremath{\leq}}
\newcommand{\lockcomplete}[1]{\ensuremath{\text{\textit{lock-complete}}(#1)}}
\newcommand{\stable}[1]{\ensuremath{\mathit{stable}(#1)}}
\newcommand{\stcong}[1]{\ensuremath{\sim_{#1}}}