Commit 2bd78763 authored by Glen Mével's avatar Glen Mével
Browse files

make is not logically atomic; notation for binder of logically atomic triples

parent 9155f05b
%\begin{figure}
\begin{mathpar}
%
\lahoareV
\hoareV
{\TRUE}
{\make~\Unit}
{\Lam \queue. \queueInv \isep \isQueueSC {[]} \isep \persistent{\queueInv}}
\\
\infer{\queueInv}{\;\;\;%
\lahoareV
{\Forall \nbelems, \elemList*[]. \isQueueSC \elemList}
<\nbelems, \elemList*[]>
{\isQueueSC \elemList}
{\enqueue~\queue~\elem}
{\Lam \Unit. \isQueueSC {\elemListSnoc \elemList \elem}}
\;\;\;}
\quad
\infer{\queueInv}{\;\;\;%
\lahoareV
{\Forall \nbelems, \elemList*[]. \isQueueSC \elemList}
<\nbelems, \elemList*[]>
{\isQueueSC \elemList}
{\dequeue~\queue}
{\Lam \elem. 1 \leq \nbelems \isep \elem = \elem_0 \isep \isQueueSC {\elemList<1>*}}
\;\;\;}
......
%\begin{figure}
\begin{mathpar}
%
\lahoareV
\hoareV
{\TRUE}
{\make~\Unit}
{\Lam \queue. \isQueueSEQ {[]}}
......
......@@ -13,7 +13,8 @@
\\\\\\
\lahoareV
{\begin{array}{@{}l@{}}\Forall \tview, \hview, \nbelems, \elemViewList*[].
{\begin{array}{@{}l@{}}
\lahoarebinder{\tview, \hview, \nbelems, \elemViewList*[]}
\\ \hphantom{\Lam\Unit.}
\isQueue \tview {\hphantom(\hview\hphantom{{}\viewjoin\view)}} \elemViewList
\hphantom{, \pair\elem\view}
......@@ -28,7 +29,8 @@
\\\\\\
\lahoareV
{\begin{array}{@{}l@{}}\Forall \tview, \hview, \nbelems, \elemViewList*[].
{\begin{array}{@{}l@{}}
\lahoarebinder{\tview, \hview, \nbelems, \elemViewList*[]}
\\ \hphantom{\Lam\elem.}
\isQueue {\hphantom(\tview\hphantom{{}\viewjoin\view)}} \hview \elemViewList
\isep \seen\view
......@@ -51,7 +53,8 @@
\\\\\\
\lahoareV
{\begin{array}{@{}l@{}}\Forall \tview, \hview, \nbelems, \elemViewList*[].
{\begin{array}{@{}l@{}}
\lahoarebinder{\tview, \hview, \nbelems, \elemViewList*[]}
\\ \hspace{2.9em}
\isQueue \tview {\hphantom(\hview\hphantom{{}\viewjoin\view)}} \elemViewList
\hphantom{, \pair\elem\view}
......@@ -70,7 +73,8 @@
\\\\\\
\lahoareV
{\begin{array}{@{}l@{}}\Forall \tview, \hview, \nbelems, \elemViewList*[].
{\begin{array}{@{}l@{}}
\lahoarebinder{\tview, \hview, \nbelems, \elemViewList*[]}
\\ \hspace{3.13em}
\isQueue {\hphantom(\tview\hphantom{{}\viewjoin\view)}} \hview \elemViewList
\isep \seen\view
......
......@@ -490,16 +490,22 @@
\newcommand{\WP}[2]{\WPname~{#1}~\left\{{#2}\right\}}
% a logically atomic Hoare triple (adapted from iris.sty):
% USAGE: \lahoare {pre} {c} {post} [mask]
\NewDocumentCommand \lahoare {m m m O{}}{%
\anglebracket{#1}\spac{#2}\spac\anglebracket{#3}_{#4}%
% in Iris literature the binder is simply denoted as "x." with no ∀ symbol:
\NewDocumentCommand \lahoarebinder {m} {%
\IfNoValueTF{#1} {} {#1.\spac}
}
% USAGE: \lahoareV [vertical alignment] {pre} {c} {post} [mask]
\NewDocumentCommand \lahoareV {O{c} m m m O{}} {{%
% USAGE: \lahoare <binder> {pre} {c} {post} [mask]
\NewDocumentCommand \lahoare {d<> m m m O{}}{%
\anglebracket{\lahoarebinder{#1}#2}
\spac{#3}\spac
\anglebracket{#4}_{#5}%
}
% USAGE: \lahoareV [vertical alignment] <binder> {pre} {c} {post} [mask]
\NewDocumentCommand \lahoareV {O{c} d<> m m m O{}} {{%
\begin{aligned}[#1]
& \anglebracket{#2} \\
& \quad {#3} \\
& {\anglebracket{#4}}_{#5}
& \anglebracket{\lahoarebinder{#2}#3} \\
& \quad {#4} \\
& {\anglebracket{#5}}_{#6}
\end{aligned}%
}}
......@@ -508,11 +514,11 @@
%\newcommand{\HoareRule}[4][]{%
% \tripleinfer[#1]{#2}{#3}{#4}%
%}
%\NewDocumentCommand \LAHoareRule {O{} m m m O{}} {%
%\NewDocumentCommand \LAHoareRule {O{} d<> m m m O{}} {%
% \tripleinfer[#1]
% {\anglebracket{#2}}
% {#3}
% {{\anglebracket{#4}}_{#5}}
% {\anglebracket{\IfNoValueTF{#2}{}{#2.\spac}#3}}
% {#4}
% {{\anglebracket{#5}}_{#6}}
%}
\makeatletter
\newlength\Hoare@widthPrePost%
......@@ -527,15 +533,16 @@
& {\curlybracket{\makebox[\Hoare@widthPrePost][l]{\(\vphantom{\displaystyle\sum}#4\)}}}_{#5}
\end{aligned}
}}
\NewDocumentCommand \LAHoareRule {O{c} m m m O{}} {{%
\NewDocumentCommand \LAHoareRule {O{c} d<> m m m O{}} {{%
\newcommand \Hoare@pre {\lahoarebinder{#2}#3}%
% compute the max of the widths of Pre and Post:
\settowidth\Hoare@widthPrePost{\vbox{\hbox{\(#2\)}\hbox{\(#4\)}}}%
\settowidth\Hoare@widthPrePost{\vbox{\hbox{\(\Hoare@pre\)}\hbox{\(#5\)}}}%
\begin{aligned}[#1]
& {\anglebracket{\makebox[\Hoare@widthPrePost][l]{\(\vphantom{\displaystyle\sum}#2\)}}} \\
& {\anglebracket{\makebox[\Hoare@widthPrePost][l]{\(\vphantom{\displaystyle\sum}\Hoare@pre\)}}} \\
\hline
& \vphantom\sum \quad {#3} \\
& \vphantom\sum \quad {#4} \\
\hline
& {\anglebracket{\makebox[\Hoare@widthPrePost][l]{\(\vphantom{\displaystyle\sum}#4\)}}}_{#5}
& {\anglebracket{\makebox[\Hoare@widthPrePost][l]{\(\vphantom{\displaystyle\sum}#5\)}}}_{#6}
\end{aligned}
}}
\makeatother
......
......@@ -177,15 +177,15 @@ This linearization point being atomic, it allows the opening of invariants just
\begin{mathpar}
%
\infer{%
\lahoare {\Forall x. P} {e} {Q}
\lahoare <x> {P} {e} {Q}
}{%
\Forall x. \hoare {P} {e} {Q}
}
\infer{%
\lahoare {\Forall x. I \isep P} {e} {I \isep Q}
\lahoare <x> {I \isep P} {e} {I \isep Q}
}{%
\knowInv{}{I} \vdash \lahoare {\Forall x. P} {e} {Q}
\knowInv{}{I} \vdash \lahoare <x> {P} {e} {Q}
}
%
\end{mathpar}
......@@ -201,8 +201,7 @@ in~\fref{fig:queue:specsc}.
It closely resembles that of the sequential setting (\fref{fig:queue:specseq}).
The first difference that can be seen is the use of angle brackets $\anglebracket{\ldots}$ denoting logically atomic triples instead of curly brackets $\curlybracket{\ldots}$ for ordinary Hoare triples.
Another difference is the presence of embedded universal quantifiers ($\forall \nbelems, \elemList*[] {.}$) in the syntax of logically atomic triples.
% TODO: in Iris literature the binder is simply denoted as "x." with no ∀ symbol.
Another difference is the presence of embedded universal quantifiers ($\lahoarebinder{\nbelems, \elemList*[]}$) in the syntax of logically atomic triples.
These additional bindings address a subtlety of logical atomicity: indeed, recall that the precondition and the postcondition are to be interpreted at the linearization point.
However, the state of the shared queue is not known in advance by the client when calling the functions $\enqueue$ and $\dequeue$: instead, both the preconditions and the postconditions need to be parameterized by said shared state.
Said otherwise, since we do not know in advance when executing a program fragment the state of the shared resource at the linearization point, a logically atomic triple provides a \emph{familly} of pre/postcondition pairs covering all the possible shared states at the linearization point.
......
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