% Standard Latex definitions.

% HORIZONTAL MARGINS
% Left margin 1 inch (0 + 1)
\setlength{\oddsidemargin}{0in}
% Text width 6.5 inch (so right margin 1 inch).
\setlength{\textwidth}{6.5in}
% ----------------
% VERTICAL MARGINS
% Top margin 0.5 inch (-0.5 + 1)
\setlength{\topmargin}{-0.5in}
% Head height 0.25 inch (where page headers go)
\setlength{\headheight}{0.25in}
% Head separation 0.25 inch (between header and top line of text)
\setlength{\headsep}{0.25in}
% Text height 9 inch (so bottom margin 1 in)
\setlength{\textheight}{9in}
% ----------------
% PARAGRAPH INDENTATION
\setlength{\parindent}{0in}
% SPACE BETWEEN PARAGRAPHS
\setlength{\parskip}{\medskipamount}
% LINE SPACING
%\setlength{\baselineskip}{16pt}
% ----------------
% STRUTS
% HORIZONTAL STRUT.  One argument (width).
\newcommand{\hstrut}[1]{\hspace*{#1}}
% VERTICAL STRUT. Two arguments (offset from baseline, height).
\newcommand{\vstrut}[2]{\rule[#1]{0in}{#2}}
% ----------------
% HORIZONTAL LINE ACROSS PAGE:
\newcommand{\hdivider}{\noindent\mbox{}\hrulefill\mbox{}} 
% ----------------
% EMPTY BOXES OF VARIOUS WIDTHS, FOR INDENTATION
\newcommand{\hm}{\hspace*{1em}}
\newcommand{\hmm}{\hspace*{2em}}
\newcommand{\hmmm}{\hspace*{3em}}
\newcommand{\hmmmm}{\hspace*{4em}}
% ----------------
% VARIOUS CONVENIENT WIDTHS RELATIVE TO THE TEXT WIDTH, FOR BOXES.
\newlength{\hlessmm}
\setlength{\hlessmm}{\textwidth}
\addtolength{\hlessmm}{-2em}

\newlength{\hlessmmmm}
\setlength{\hlessmmmm}{\textwidth}
\addtolength{\hlessmmmm}{-4em}
% ----------------
% ``TIGHTLIST'' ENVIRONMENT (no para space betwee items, small indent)
\newenvironment{tightlist}%
{\begin{list}{$\bullet$}{%
    \setlength{\topsep}{0in}
    \setlength{\partopsep}{0in}
    \setlength{\itemsep}{0in}
    \setlength{\parsep}{0in}
    \setlength{\leftmargin}{1.5em}
    \setlength{\rightmargin}{0in}
    \setlength{\itemindent}{0in}
}
}%
{\end{list}
}
% ----------------
% ITALICISE WORDS
\newcommand{\ie}{{\em i.e.,\/}}
\newcommand{\eg}{{\em e.g.,\/}}
\newcommand{\etc}{{\em etc.\/}}
\newcommand{\via}{{\em via\/}}
\newcommand{\vs}{{\em vs.\/}}
% ----------------
% CODE FONT (e.g. {\cf x := 0}).
\newcommand{\cf}{\tt}
% ----------------------------------------------------------------
% ID CODE DISPLAYS.
% Id code displays are enclosed between \bid and \eid.
% Most characters are taken verbatim, in typewriter font,
% Except:
%  Commands are still available (beginning with \)
%    but use $ and $ instead of { and }

\outer\def\beginid{%
  \begin{list}{$\bullet$}{%
    \spacing{1}
    \medskip
    \setlength{\topsep}{0in}
    \setlength{\partopsep}{0in}
    \setlength{\itemsep}{0in}
    \setlength{\parsep}{0in}
    \setlength{\leftmargin}{1.5em}
    \setlength{\rightmargin}{0in}
    \setlength{\itemindent}{0in}
  }\item[]
  \catcode`\{=12
  \catcode`\}=12
  \catcode`\&=12
%  \catcode`\~=12
  \catcode`\%=12
  \catcode`\_=12
  \catcode`\^=12
  \catcode`\~=1
  \catcode`\#=2
%  \catcode`\'=2
%  \catcode`\`=1
  \obeyspaces
  \obeylines \cf}

\outer\def\endid{%
  \end{list}
  }

%{\obeyspaces\gdef {\ }}

\outer\def\beginidm{% id mode with math (allow _,$)
  \begin{list}{$\bullet$}{%
    \spacing{1}
    \medskip
    \setlength{\topsep}{0in}
    \setlength{\partopsep}{0in}
    \setlength{\itemsep}{0in}
    \setlength{\parsep}{0in}
    \setlength{\leftmargin}{1.5em}
    \setlength{\rightmargin}{0in}
    \setlength{\itemindent}{0in}
  }\item[]
  \catcode`\{=12
  \catcode`\}=12
  \catcode`\&=12
%  \catcode`\~=12
  \catcode`\%=12
%  \catcode`\_=12
  \catcode`\^=12
  \catcode`\~=1
  \catcode`\#=2
%  \catcode`\'=2
%  \catcode`\`=1
  \obeyspaces
  \obeylines \cf}

\outer\def\endidm{%
  \end{list}
  }

%{\obeyspaces\gdef {\ }}

% ----------------------------------------------------------------
% LISP CODE DISPLAYS.
% Lisp code displays are enclosed between \blisp and \elisp.
% Most characters are taken verbatim, in typewriter font,
% Except:
%  Commands are still available (beginning with \)
%  Math mode is still available (beginning with $)

\outer\def\beginlisp{%
  \begin{list}{$\bullet$}{%
    \setlength{\topsep}{0in}
    \setlength{\partopsep}{0in}
    \setlength{\itemsep}{0in}
    \setlength{\parsep}{0in}
    \setlength{\leftmargin}{1.5em}
    \setlength{\rightmargin}{0in}
    \setlength{\itemindent}{0in}
  }\item[]
  \obeyspaces
  \obeylines \tt}

\outer\def\endlisp{%
  \end{list}
  }

{\obeyspaces\gdef {\ }}

% ----------------
% ILLUSTRATIONS
% This command should specify a JJ directory for ps files for illustrations.
\def\boxedillustration#1{\begin{center}
{\fbox{\psadobe{\illustrationfileprefix#1.ps}}}
\end{center}}
\def\boxedillustrationpercent#1#2{\begin{center}
{\fbox{\psadobepercent{#2}{\illustrationfileprefix#1.ps}}}
\end{center}}

% \def\psfileprefix{/jj/barth/thesis/}
%\def\illustration#1#2{
%\vbox to #2{\vfill\special{psfile=\psfileprefix#1.ps hoffset=-72 voffset=-45}}} 
%%
%% \illuswidth is used to set up boxes around illustrations.
\newlength{\illuswidth}
\setlength{\illuswidth}{\textwidth}
\addtolength{\illuswidth}{-7pt}
%
% ----------------------------------------------------------------
\newcommand{\res}{V_R}
\newtheorem{precedence}{Precedence}
\newtheorem{wfme}{WFME}
\newtheorem{lemma}{Lemma}
\newtheorem{definition}{Definition}
\newtheorem{strictness}{Strictness}
\newtheorem{atomicity}{Take Completion}
\newtheorem{fact}[theorem]{Fact}

\newcommand{\inv}[1]{\mbox{\sf Inv}\mbox{\rm (}#1\mbox{\rm )}}
\newcommand{\comp}[1]{\mbox{\sf Cmp}\mbox{\rm (}#1\mbox{\rm )}}
\newcommand{\df}[1]{\mbox{\sf Val}\mbox{\rm (}#1\mbox{\rm )}}
\newcommand{\atm}[1]{\mbox{\sf TC}\mbox{\rm (}#1\mbox{\rm )}}
\newcommand{\dv}[1]{\mbox{\sf Def}\mbox{\rm (}#1\mbox{\rm )}}


\newcommand{\state}[1]{\mbox{$\sigma$}\mbox{\rm (}#1\mbox{\rm )}}
\newcommand{\isfull}[2]{\mbox{\sf Full}(#1,#2)}
\newcommand{\tofull}[3]{\state{#1}\mbox{\sf :=}\isfull{#2}{#3}}
\newcommand{\isempty}[1]{\mbox{\sf Empty}(#1)}
\newcommand{\toempty}[2]{\state{#1}\mbox{\sf :=}\isempty{#2}}
\newcommand{\ul}[1]{\mbox{$\underline{\mbox{#1}}$}}
\newcommand{\lbl}[2]{\mbox{${\mbox{\cf #1}}_{\mbox{\rm\small\em #2}}$}}
\newcommand{\simul}{\mbox{$\equiv$}}
\newcommand{\genesis}{\inv{\mbox{$\cal P$}}}
\newcommand{\armag}{\comp{\mbox{\cal P}}}

\newcommand{\OldTake}[2]{\mbox{\sf take}_#1 : #2}
\newcommand{\OldPut}[2]{\mbox{\sf put}_#1 : #2}

\newcommand{\Take}[2]{\df{\lbl{take}{#2} \mbox{#1}}}
\newcommand{\Put}[2]{\inv{\lbl{put}{#2} \mbox{#1} \mbox{$V$}}}

\newcommand{\Fetch}[2]{\df{\lbl{fetch}{#2} \mbox{#1}}}
\newcommand{\Store}[2]{\inv{\lbl{store}{#2} \mbox{#1} \mbox{$V$}}}
\newcommand{\fby}{\rightarrow}
\newcommand{\efby}{\stackrel{+}{\fby}}
\newcommand{\cmplt}[1]{\stackrel{\star}{#1}}
\newcommand{\lno}[1]{(#1)}
\newcommand{\pst}[1]{\ul{#1}\vspace{.5ex}}
\newcommand{\becomes}{\longrightarrow}