@@ -444,7 +444,7 @@ When desired, this atomic update gives access to the precondition~$P$ for some v
Crucially, the \emph{masks}$\emptyset$ and $\top$ annotating the \emph{fancy updates}$\pvs[\top][\emptyset]$ and $\pvs[\emptyset][\top]$ require that the atomic update be used during one atomic step only, as required.
Using the invariant rules of Iris~\cite{iris}, it is easy to show that atomic updates can be used to open and close invariants.
The rule \RULE{LAInv} follows as a corollary, and \RULE{LAHoare} is immediate.
Rule~\rulelainv follows as a corollary, rule~\rulelahoare is immediate.
@@ -59,41 +59,22 @@ Yet these operations are ``atomic'' in some empirical sense.
The concept of logical atomicity~\cite[\S7]{jacobs2011expressive,jung-slides-2019,iris-15} aims at addressing that difficulty.
To use it, we substitute ordinary Hoare triples with \emph{logically atomic triples}.
Two important reasoning rules for logically atomic triples are given in \fref{fig:latriples}.%
Two important reasoning rules for logically atomic triples are given in \fref{fig:hlog:latriples}.%
\footnote{%
Following Iris notations, $\knowInv{}{I}$ is an invariant whose content is the assertion~$I$, and $\later$ is a step-indexing modality, a technicality of Iris that we can ignore in this paper.
}
A logically atomic triple is denoted with angle brackets~$\anglebracket{\ldots}$.
Just like an ordinary triple, it specifies a program fragment with a precondition and a postcondition.
In fact, as witnessed by rule \RULE{LAHoare}, one can deduce an ordinary Hoare triple from a logically atomic triple.
The core difference is that, thanks to rule \RULE{LAInv}, invariants can be opened around a logically atomic triple, regardless of the number of execution steps of the program fragment: in a sense, when a function is specified using a logically atomic triple, one states that said function behaves as if it were atomic.
In fact, as witnessed by rule \rulelahoare, one can deduce an ordinary Hoare triple from a logically atomic triple.
The core difference is that, thanks to rule \rulelainv, invariants can be opened around a logically atomic triple, regardless of the number of execution steps of the program fragment: in a sense, when a function is specified using a logically atomic triple, one states that said function behaves as if it were atomic.
%
The definition of logically atomic triples is further discussed in~\sref{sec:queue:proof:la}
and given with detail in previous work~\cite[\S7]{jung-slides-2019,iris-15}.
We now try to give an intuition of that concept:
a logically atomic triple $\lahoare{P}{e}{Q}$ states, roughly, that the expression$e$ contains an atomic instruction, called the \emph{commit point}, which has $P$ as a precondition and $Q$ as a postcondition.
a logically atomic triple $\lahoare{P}{e}{Q}$ states, roughly, that the expression~$e$ contains an atomic instruction, called the \emph{commit point}, which has $P$ as a precondition and $Q$ as a postcondition.
Because it is atomic, invariants can be opened around that commit point.
%
\begin{figure}
\begin{mathpar}
%
\infer[LAHoare]{% using the rule names from \cite{iris-15}
\lahoare <x> {P}{e}{Q}
}{%
\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}
}{%
\knowInv{}{I}\vdash\lahoare <x> {P}{e}{Q}
}
%
\end{mathpar}
\Description{Selected rules for logically atomic triples.}
\caption{Selected rules for logically atomic triples}
\label{fig:latriples}
\end{figure}
\input{figure-hlog-latriples}
Using logically atomic triples, the specification can be written as shown