Skip to content

GitLab

Commit 6766aa25 authored by Glen Mével's avatar Glen Mével
Browse files

improve spacing 

  - define large-spacing variants of the logical connectives
  - rename \ISep to \isepV, improve its aspect
  - fix dirty spacing in various macros (avoid relative spacing such as \, or \!)
  - better use of mathpar
parent ca2aae20
Hide whitespace changes
Inline Side-by-side
papers/icfp2021/figure-pipeline-inv.tex
View file @ 6766aa25
......@@ -23,7 +23,7 @@
\pipelineInv R
& \eqdef
& \Exists \queue, \gqueue, \gcurf, \gcurg. \queueInv \isep \knowInv{}{\pipelineInvInner R}
& \Exists \queue, \gqueue, \gcurf, \gcurg. \queueInv \ISEP \knowInv{}{\pipelineInvInner R}
\\
......@@ -36,14 +36,14 @@
\left\{\begin{array}{l}
\Exists \curf, \curg, \tview, \hview, \yElemViewListInv<\curg><\curf>*[].
\\ \quad \ISep{%
\\ \quad \isepV{%
\curg \leq \curf
\isep \ownGhost \gcurf {\authfull \curf}
\isep \ownGhost \gcurg {\authfull \curg}
\ISEP \ownGhost \gcurf {\authfull \curf}
\ISEP \ownGhost \gcurg {\authfull \curg}
\cr \isQueue \tview \hview {\yElemViewListInv<\curg><\curf>}
\cr \displaystyle\Sep_{\curg \leq \idx < \curf}
\left(\wpre {g\;\yElem_\idx} {\Lam z. R\;\idx\;z}\right) \opat \view_\idx
}%end of the main \ISep of the invariant
}%end of the main \isepV of the invariant
\end{array}\right.% end of the definition of \queueInvInner
%}% end of \multicolumn
......@@ -54,9 +54,9 @@
\pipelineF R \curf \refXArray \xElemList
& \eqdef
& \ISep{%
& \isepV{%
\curf \leq \nbelems
\isep \ownGhost \gcurf {\authfull \curf}
\ISEP \ownGhost \gcurf {\authfull \curf}
\cr \arraypointstoNA \refXArray \xElemList
\cr \displaystyle\Sep_{\curf \leq \idx < \nbelems}
\wpre {f\;x_\idx} {\Lam y. \wpre {g\;y} {\Lam z. R\;\idx\;z}}
......@@ -68,9 +68,9 @@
\pipelineG R \curg \refZArray \zElemList
& \eqdef
& \ISep{%
& \isepV{%
\curg \leq \nbelems
\isep \ownGhost \gcurg {\authfull \curg}
\ISEP \ownGhost \gcurg {\authfull \curg}
\cr \arraypointstoNA \refZArray \zElemList
\cr \displaystyle\Sep_{0 \leq \idx < \curg}
R\;\idx\;z_\idx
......
papers/icfp2021/figure-pipeline-spec.tex
View file @ 6766aa25
......@@ -4,16 +4,16 @@
\hoareV
{\hphantom{\Lam \refZArray. \Exists \zElemList*[].}
\haslength \refXArray \nbelems
\isep \arraypointstoNA \refXArray \xElemList
\isep \displaystyle\Sep_{0 \leq \idx < \nbelems}
\ISEP \arraypointstoNA \refXArray \xElemList
\ISEP \displaystyle\Sep_{0 \leq \idx < \nbelems}
%\hoare {} {f\;x_\idx} {\Lam y. \hoare {} {g\;y} {\Lam z. R\;\idx\;z}\vphantom{\displaystyle\sum}}
\wpre {f\;x_\idx} {\Lam y. \wpre {g\;y} {\Lam z. R\;\idx\;z}}
}
{\pipeline\;g\;f\;\refXArray}
{\Lam \refZArray. \Exists \zElemList*[].
\haslength \refZArray \nbelems
\isep \arraypointstoNA \refZArray \zElemList
\isep \displaystyle\Sep_{0 \leq \idx < \nbelems} R\;\idx\;z_\idx
\ISEP \arraypointstoNA \refZArray \zElemList
\ISEP \displaystyle\Sep_{0 \leq \idx < \nbelems} R\;\idx\;z_\idx
}
\end{array}\]
......
papers/icfp2021/figure-queue-inv.tex
View file @ 6766aa25
......@@ -63,7 +63,7 @@
\left\{\begin{array}{l}
\Exists \reftail, \refhead, \refstatuses, \refelements.
\\ \Exists \tail, \tview, \head, \hview, \elemViewListInv<\tail><\head>*[], \statusViewList*[].
\\ \quad \ISep{%
\\ \quad \isepV{%
% pure assertions:
\queue = \Tuple{\reftail, \refhead, \refstatuses, \refelements}
\cr 0 \le \tail \le \head \le \tail + \capacity
......@@ -117,7 +117,7 @@
% cell being filled with a value by an enqueuer:
\status_{\modcap\idx} = 2\idx
\end{array}% end of array used to align the two big-stars
}%end of the main \ISep of the invariant
}%end of the main \isepV of the invariant
\end{array}\right.% end of the definition of \queueInvInner
}% end of \multicolumn
......@@ -128,7 +128,7 @@
\emptyCell \idx {\pair\status\sview}
& \eqdef
& \ISep{%
& \isepV{%
\status = 2(\idx + \capacity)
\cr (\nthpointstoNA\refelements{\modcap\idx}-) \opat \sview
\cr \tokenR\idx
......@@ -140,7 +140,7 @@
\fullCell \idx {\pair\status\sview} {\pair\elem\eview}
& \eqdef
& \ISep{%
& \isepV{%
\status = 2\idx + 1
\cr (\nthpointstoNA\refelements{\modcap\idx}{\elem}) \opat \sview
\cr \tokenW\idx{\pair\elem\eview}
......
papers/icfp2021/figure-queue-spec-sc.tex
View file @ 6766aa25
%\begin{figure}
\begin{mathpar}
%
\infer{~}{\persistent{\queueInv}}
\qquad
\infer{~}{\persistent{\queueInv}}
\and
\hoareV
{\TRUE}
{\make~\Unit}
{\Lam \queue. \queueInv \isep \isQueueSC {[]}}
{\Lam \queue. \queueInv \ISEP \isQueueSC {[]}}
\\
\infer{\queueInv}{%
\lahoareV
......@@ -15,15 +14,14 @@
{\enqueue~\queue~\elem}
{\Lam \Unit. \isQueueSC {\elemListSnoc \elemList \elem}}
}
\quad
\and
\infer{\queueInv}{%
\lahoareV
<\nbelems, \elemList*[]>
{\isQueueSC \elemList}
{\dequeue~\queue}
{\Lam \elem. 1 \leq \nbelems \isep \elem = \elem_0 \isep \isQueueSC {\elemList<1>*}}
{\Lam \elem. 1 \leq \nbelems \ISEP \elem = \elem_0 \ISEP \isQueueSC {\elemList<1>*}}
}
%
\end{mathpar}
\Description{A specification of the ``queue'' data structure in a sequentially consistent model.}
\caption{A specification of the ``queue'' data structure in a sequentially consistent memory model}
......
papers/icfp2021/figure-queue-spec-seq.tex
View file @ 6766aa25
%\begin{figure}
\begin{mathpar}
%
\hoareV
{\TRUE}
{\make~\Unit}
......@@ -10,12 +9,11 @@
{\isQueueSEQ \elemList}
{\enqueue~\queue~\elem}
{\Lam \Unit. \isQueueSEQ {\elemListSnoc \elemList \elem}}
\and
\hoareV
{\isQueueSEQ \elemList}
{\dequeue~\queue}
{\Lam \elem. 1 \leq \nbelems \isep \elem = \elem_0 \isep \isQueueSEQ {\elemList<1>*}}
%
{\Lam \elem. 1 \leq \nbelems \ISEP \elem = \elem_0 \ISEP \isQueueSEQ {\elemList<1>*}}
\end{mathpar}
\Description{A specification of the ``queue'' data structure in a sequential setting.}
\caption{A specification of the ``queue'' data structure in a sequential setting}
......
papers/icfp2021/figure-queue-spec-weak.tex
View file @ 6766aa25
......@@ -4,7 +4,8 @@
% inside text width:
\thinmuskip = 0mu
\medmuskip = 0mu
\thickmuskip = 3mu
\thickmuskip = 2mu
\verythickmuskip = 9mu
\begin{mathpar}
\infer{~}{\persistent{\queueInv}}
......@@ -16,7 +17,7 @@
{\make~\Unit}
{\Lam \queue. \Exists \gqueue.
\queueInv
\isep \isQueue {\view_0} {\view_0} {[]}
\ISEP \isQueue {\view_0} {\view_0} {[]}
}
\and
\infer{\queueInv}{%
......@@ -26,12 +27,12 @@
\\ \hphantom{\Lam\Unit.}
\isQueue \tview {\hphantom(\hview\hphantom{{}\viewjoin\view)}} \elemViewList
\hphantom{, \pair\elem\view}
\isep \seen\view
\ISEP \seen\view
\end{array}}
{\enqueue~\queue~\elem}
{\Lam \Unit.
\isQueue \tview {(\hview \sqcup \view)} {\elemListSnoc \elemViewList {\pair\elem\view}}
\isep \seen\hview
\ISEP \seen\hview
}
}
\and
......@@ -41,15 +42,15 @@
\lahoarebinder{\tview, \hview, \nbelems, \elemViewList*[]}
\\ \hphantom{\Lam\elem.}
\isQueue {\hphantom(\tview\hphantom{{}\viewjoin\view)}} \hview \elemViewList
\isep \seen\view
\ISEP \seen\view
\end{array}}
{\dequeue~\queue}
{\Lam \elem.
\isQueue {(\tview \sqcup \view)} \hview {\elemViewList<1>*}
\isep \seen \tview
\isep \seen \eview_0
\isep 1 \leq \nbelems
\isep \elem = \elem_0
\ISEP \seen \tview
\ISEP \seen \eview_0
\ISEP 1 \leq \nbelems
\ISEP \elem = \elem_0
}
}
\and
......@@ -57,10 +58,10 @@
\lahoareV
{\begin{array}{@{}l@{}}
\lahoarebinder{\tview, \hview, \nbelems, \elemViewList*[]}
\\ \hspace{2.9em}
\\ \hspace{2.57em}
\isQueue \tview {\hphantom(\hview\hphantom{{}\viewjoin\view)}} \elemViewList
\hphantom{, \pair\elem\view}
\isep \seen\view
\ISEP \seen\view
\end{array}}
{\tryenqueue~\queue~\elem}
{\Lam \boolval.
......@@ -68,7 +69,7 @@
{\False}{\isQueue \tview {\hphantom(\hview\hphantom{{}\viewjoin\view)}} \elemViewList}
{\True }{%
\isQueue \tview {(\hview \sqcup \view)} {\elemListSnoc \elemViewList {\pair\elem\view}}
\isep \seen\hview
\ISEP \seen\hview
}
}
}
......@@ -77,9 +78,9 @@
\lahoareV
{\begin{array}{@{}l@{}}
\lahoarebinder{\tview, \hview, \nbelems, \elemViewList*[]}
\\ \hspace{3.13em}
\\ \hspace{2.8em}
\isQueue {\hphantom(\tview\hphantom{{}\viewjoin\view)}} \hview \elemViewList
\isep \seen\view
\ISEP \seen\view
\end{array}}
{\trydequeue~\queue}
{\Lam \elemopt.
......@@ -89,9 +90,9 @@
}
{\Some{\elem_0}}{%
\isQueue {(\tview \sqcup \view)} \hview {\elemViewList<1>*}
\isep \seen \tview
\isep \seen \eview_0
\isep 1 \leq \nbelems
\ISEP \seen \tview
\ISEP \seen \eview_0
\ISEP 1 \leq \nbelems
}
}
}
......
papers/icfp2021/notations.tex
View file @ 6766aa25
......@@ -22,6 +22,9 @@
\colorlet{glen}{orange}
% \newcommand{\glen}[1]{\textcolor{glen}{---glen: #1}}
% ------------------------------------------------------------------------------
% Generic macros.
% Text subscript and superscript.
\newcommand{\sub}[1]{\TextOrMath{\textsubscript{#1}}{_\text{\normalfont {#1}}}}
\newcommand{\super}[1]{\TextOrMath{\textsuperscript{#1}}{^\text{\normalfont {#1}}}}
......@@ -36,6 +39,19 @@
% Tentative definition.
\newcommand{\tryeqdef}{\ensuremath{\mathrel{\stackrel{?}{=}}}}
% Large-spacing versions of logical connectives (by default they are spaced as
% binary operators, which is incorrect and hard to read when combining atomic
% formulas which are themselves relations).
\newmuskip \verythickmuskip
\newcommand \verythickspace {\mskip\verythickmuskip}
\verythickmuskip = 2\thickmuskip % default spacing
% \mathlop intends to resemble \mathbin and the like, but it is not as smart:
\newcommand \mathlop[1] {\verythickspace\mathord{#1}\verythickspace}
% common logical connectives:
\newcommand \LAND {\mathlop{\land}}
\newcommand \LOR {\mathlop{\lor}}
\newcommand \IMPLIES {\mathlop{\Longrightarrow}}
\makeatletter
% An anonymous command, to give to higher-order commands.
......@@ -276,14 +292,15 @@
% Notations of the logic.
% separating conjunction (not defined by iris.sty):
\newcommand{\isep}{\,\mathrel{*}\,}
% large separating conjunction:
\newcommand{\ISEP}{\scalebox{1.7}{\raisebox{-0.3ex}{$\ast$}}\!}
\newcommand{\isep}{\mathbin{\ast}}
\newcommand{\ISEP}{\mathlop{\ast}}
\newcommand{\WAND}{\mathlop{\wand}}
% NOTE: iris.sty defines the “big” (subscriptable) separating conjunction as \Sep.
% large separating conjunction in an array:
% (left brace on the left side)
% (using \cr inside to separate lines)
\newcommand{\ISep}[1]{%
\ISEP
\newcommand{\isepV}[1]{%
\scalebox{1.7}{\raisebox{-0.2ex}{\(\ast\)}}\hspace{-0.7ex}
\left\{\begin{array}{@{\,}l@{}}
#1
\end{array}\right.
......@@ -298,32 +315,26 @@
\def\Exists #1.{\exists#1.\spac}%
% pattern-matching / case distinction:
%\newcommand{\matchwith}[5]{%
% \mathrm{match}\;#1\;\mathrm{with}
% \left[\begin{array}{@{\,}l@{{}\rightarrow{}}l@{}}
% #2 & #3 \\
% #4 & #5
% \end{array}\right.
%}
\newcommand{\matchwith}[5]{%
\left[\begin{array}{@{\,}ll@{}}
#3 & \text{if }#1 = #2 \\
#5 & \text{if }#1 = #4
\mathrm{match}\;#1\;\mathrm{with}
\left[\begin{array}{@{\,}l@{{}\rightarrow{}}l@{}}
#2 & #3 \\
#4 & #5
\end{array}\right.
}
\newcommand{\matchwithnobinder}[5]{%
\mathord\lor
\mathord{\lor}
\left[\begin{array}{@{\,}l@{}l@{}}
#3 &{}\isep #1 = #2 \\
#5 &{}\isep #1 = #4
#3 &\ISEP #1 = #2 \\
#5 &\ISEP #1 = #4
\end{array}\right.
}
% the “valid view” predicate:
\newcommand{\valid}[1]{\mathit{valid}\,#1}
\newcommand{\valid}[1]{\mathop{\mathit{valid}}#1}
% the “seen” predicate:
\newcommand{\seen}{\mathop\uparrow\!\!\:}
\newcommand{\seen}{\mathop{\uparrow}}
%\newcommand{\seen}{\mathop{\text{\eye}}} % requires package <dingbat>
% \let\checkmark\undefined
% \usepackage{dingbat}
......@@ -519,7 +530,7 @@
% weakest precondition:
\newcommand{\WPname}{\mathsf{wp}}
\newcommand{\WP}[2]{\WPname~{#1}~\left\{{#2}\right\}}
\newcommand{\WP}[2]{\WPname\;{#1}\;\left\{{#2}\right\}}
% a logically atomic Hoare triple (adapted from iris.sty):
% in Iris literature the binder is simply denoted as "x." with no ∀ symbol:
......@@ -781,8 +792,7 @@
\newcommand{\offset}{\ensuremath{i}}
\newcommand{\queue}{\ensuremath{q}}
\newcommand{\boolval}{\ensuremath{b}}
%\newcommand{\elemopt}{\ensuremath{v^{\!?}}}
\newcommand{\elemopt}{\ensuremath{v^{\!\!\:\raisebox{-0.3ex}{\scriptsize?}}}}
\newcommand{\elemopt}{\ensuremath{v^{\hspace{-0.2ex}\raisebox{-0.3ex}{\scriptsize?}}}}
\newcommand{\elem}{\ensuremath{v}}
\newcommand{\status}{\ensuremath{s}}
\newcommand{\tail}{\ensuremath{t}}
......@@ -797,10 +807,6 @@
\newcommand{\tview}{\mathcal{T}}
\newcommand{\hview}{\mathcal{H}}
\newcommand{\eview}{\mathcal{V}}
%\newcommand{\elemViewList}{\ensuremath{v\!\view\!s}}
%\newcommand{\statusViewList}{\ensuremath{s\!\view\!s}}
%\newcommand{\elemViewList}{\ensuremath{\mathbf{v{\hskip -0.15em}V}}}
%\newcommand{\statusViewList}{\ensuremath{\mathbf{s{\hskip -0.15em}V}}}
%\newcommand{\elemListSnoc}[2]{\left(#1{} + [ #2 ]\right)}
% since we are writing lists in extenso, we can use a neater notation:
......
papers/icfp2021/queue-proof.tex
View file @ 6766aa25
......@@ -206,7 +206,7 @@ such that the inclusion order~$(\mincl_M)$ has the following implication:
\infer{%
\pair\status\sview \mincl_M \pair{\status'}{\sview'}
}{%
\status \leq \status' \land (\status = \status' \implies \sview \viewgeq \sview')
\status \leq \status' \LAND (\status = \status' \IMPLIES \sview \viewgeq \sview')
}
%
\end{mathpar}
......@@ -258,9 +258,9 @@ we get the following:
%
\infer{%
\monoWitness{\offset}{\pair\status\sview}
\isep \ownGhost\gmonos{\mapsingleton \offset {\authfull \pair{\status'}{\sview'}}}
\ISEP \ownGhost\gmonos{\mapsingleton \offset {\authfull \pair{\status'}{\sview'}}}
}{%
\status \leq \status' \land (\status = \status'\implies \sview \viewgeq \sview')
\status \leq \status' \LAND (\status = \status' \IMPLIES \sview \viewgeq \sview')
}
%
\end{mathpar}
......@@ -330,7 +330,7 @@ With all this said, a first attempt at representing the buffer might be as follo
% invariant (inner) (wrong):
\queueInvInner
& \tryeqdef
& \ISep{\begin{array}{c@{}l}
& \isepV{\begin{array}{c@{}l}
\vdots
\\
\\ \displaystyle\Sep_{\head-\capacity \leq \idx < \tail}&
......@@ -345,7 +345,7 @@ With all this said, a first attempt at representing the buffer might be as follo
\emptyCell \idx {\pair\status\sview}
& \tryeqdef
& \status = 2(\idx + \capacity)
\isep (\nthpointstoNA\refelements{\modcap\idx}-) \opat \sview
\ISEP (\nthpointstoNA\refelements{\modcap\idx}-) \opat \sview
\\
......@@ -353,8 +353,8 @@ With all this said, a first attempt at representing the buffer might be as follo
\fullCell \idx {\pair\status\sview} {\pair\elem\eview}
& \tryeqdef
& \status = 2\idx + 1 \hphantom{()\,}
\isep (\nthpointstoNA\refelements{\modcap\idx}{\elem}) \opat \sview
\isep \eview \viewleq \sview
\ISEP (\nthpointstoNA\refelements{\modcap\idx}{\elem}) \opat \sview
\ISEP \eview \viewleq \sview
\end{array}\]
......@@ -479,7 +479,7 @@ Read~tokens and write~tokens are then defined as shown in~\fref{fig:queue:inv}.
%\begin{mathpar}%
%%
% \infer{%
% \tokenR \idx \isep ...
% \tokenR \idx \ISEP ...
% }{%
% \head-\capacity \leq \idx < \tail
% }
......@@ -515,18 +515,18 @@ capture the essence of logical atomicity, and to understand our proof, is:
\delimiterfactor = 1200
\Forall \predB,
\left[ \mu U.\spac \pvs \Exists x.
P \isep (\laabort P U \land \lacommit \pred \predB)
P \ISEP (\laabort P U \LAND \lacommit \pred \predB)
\right]
\wand
\WAND
\wpre e \predB
\\
\laabort P U
&\eqdef&
\hphantom{\Forall v.} P \hphantom{\;v} \wand\pvs U
\hphantom{\Forall v.} P \hphantom{\;v} \WAND\pvs U
\\
\lacommit \pred \predB
&\eqdef&
\Forall v. \pred\;v \wand\pvs \predB\;v
\Forall v. \pred\;v \WAND\pvs \predB\;v
\end{array}\]%
% JH : cette définition est incorrecte pour un "détail" important : comme elle ne mentionne pas les masques, on ne voit pas que le commit/abort doit avoir lieu de manière atomique. C'est important, parcqu'on a beaucoup dit plus haut que ça permettait d'ouvrir des invariants.
% Pas le temps de corriger ça pour la soumission, mais je laisse ce TODO pour la version finale.
......@@ -600,7 +600,7 @@ the definition of $\queueInv$, we ought to prove the following assertion:
\\ \hspace{2.9em}
\isQueue \tview {\hphantom(\hview\hphantom{{}\viewjoin\view)}} \elemViewList
\hphantom{, \pair\elem\view}
\isep \seen\view
\ISEP \seen\view
\end{array}}
{\tryenqueue~\queue~\elem}
{\Lam \boolval.
......@@ -608,7 +608,7 @@ the definition of $\queueInv$, we ought to prove the following assertion:
{\False}{\isQueue \tview {\hphantom(\hview\hphantom{{}\viewjoin\view)}} \elemViewList}
{\True }{%
\isQueue \tview {(\hview \sqcup \view)} {\elemListSnoc \elemViewList {\pair\elem\view}}
\isep \seen\hview
\ISEP \seen\hview
}
}
}
......@@ -764,7 +764,7 @@ We then switch to the left branch, by constituting the assertion:
\[%
\fullCell \idx {\pair{\status^2}{\sview^2}} {\pair\elem\eview}
\iequiv
\ISep{%
\isepV{%
\status^2 = 2\idx + 1
\cr (\nthpointstoNA\refelements{\modcap\idx}{\elem}) \opat \sview^2
\cr \tokenW\idx{\pair\elem\eview}
......
papers/icfp2021/queue-spec-sc.tex
View file @ 6766aa25
......@@ -77,7 +77,7 @@ because it is an atomic instruction.
}{%
\Forall x. \hoare {P} {e} {Q}
}
\and
\infer[LAInv]{% using the rule names from \cite{iris-15}
\lahoare <x> {\later I \isep P} {e} {\later I \isep Q}
}{%
......@@ -179,9 +179,9 @@ where the boxed assertion is an Iris invariant:
\[
\isQueuePers\Phi
\;\eqdef\;
\Exists\gqueue. \ISep{%
\Exists\gqueue. \isepV{%
\queueInv
\\ \knowInv{}{\Exists \nbelems, \elemList*[]. \isQueueSC\elemList \isep \Phi\,\nthElem{0} \isep \cdots \isep \Phi\,\nthElem{\nbelems-1}}
\\ \knowInv{}{\Exists \nbelems, \elemList*[]. \isQueueSC\elemList \ISEP \Phi\,\nthElem{0} \ISEP \cdots \ISEP \Phi\,\nthElem{\nbelems-1}}
}
\]
......
papers/icfp2021/queue-spec-seq.tex
View file @ 6766aa25
......@@ -21,7 +21,7 @@ predicate cannot be duplicated; we say that it is \emph{exclusive}.
The operations of the queue admit a simple sequential specification which is
presented in~\fref{fig:queue:spec:seq}. We use the standard Hoare
triple notation, with a partial correctness meaning.
The asterisk~$(\ast)$ is the separating conjunction.
The asterisk~$(\mathord{\isep})$ is the separating conjunction.
\begin{itemize}
\item
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment