@@ -50,9 +50,9 @@ Then, when one of the threads needs to access the shared resource, it can

operation on the shared state, reestablish the invariant, and finally close it.

%

However, to ensure soundness in the face of concurrency, the use of invariants

in Iris obeys a strict constraint: they can remain open during at most a single

in Iris obeys a strict constraint: they can remain open during at most one

step of execution. Unfortunately, $\enqueue$ and $\dequeue$ are complex

operations which, \emph{a~priori}, take more than one step of execution. Hence a client

operations which, \emph{a~priori}, take several steps. Hence a client

would be unable to open their invariant around the triples shown

in~\fref{fig:queue:spec:seq}.

Yet these operations are ``atomic'' in some empirical sense.

...

...

@@ -60,16 +60,17 @@ 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}.

Just like ordinary triples, they specify a program fragment with a precondition and a postcondition.

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.

%

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 on that concept:

a logically atomic triple $\lahoare{P}{e}{Q}$ states, roughly, that the expression $e$ contains a commit point which has $P$ as a precondition and $Q$ as a postcondition.

The triple then allows the opening of invariants around that commit point

because it is an atomic instruction.

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.

Because it is atomic, invariants can be opened around that commit point.