Commit f8223f23 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

refer to rules about LA triples.

parent 52458383
......@@ -60,8 +60,10 @@ 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.
The core difference is that 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 \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}.
......@@ -70,6 +72,7 @@ a logically atomic triple $\lahoare{P}{e}{Q}$ states, roughly, that the expressi
The triple then allows the opening of invariants around that commit point
because it is an atomic instruction.
%
\begin{figure}
\begin{mathpar}
%
\infer[LAHoare]{% using the rule names from \cite{iris-15}
......@@ -85,6 +88,10 @@ because it is an atomic instruction.
}
%
\end{mathpar}
\Description{Selected rules for logically atomic triples.}
\caption{Selected rules for logically atomic triples}
\label{fig:latriples}
\end{figure}
% TODO: faire référence aux règles ci-dessus dans le texte.
% => JH
......
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