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


parent 20a42e6d
......@@ -102,4 +102,3 @@
% JH : TODO : serait-ce pertinent de mentionner ici la timelessness et l'objectivité de isQueue et la persistence de queueInv? Cela fait partie de la spec, à mon sens.
% GLEN: la persistance oui, la timelessness c’est peut-être trop technique ?
% TODO: a-t-on dit quelque part que tous ces triplets atomiques ont implicitement \queueInv en hypothèse ?
......@@ -122,3 +122,10 @@
title={Theorems for Free from Separation Logic Specifications},
note={Under submission at ICFP'21}
\ No newline at end of file
......@@ -572,7 +572,8 @@ deduced from the two previous by an obvious induction; and the proof of \make is
simply a matter of initializing the ghost state.
Being absolutely formal is not a goal of this text. The interested reader may
find these proofs, conducted in the Coq proof assistant, in~\cite{TODO}.
find these proofs, conducted in the Coq proof assistant, in the appendix of the present submission.
% TODO : la dernière phrase poru la version finale
Recalling here the specification in~\fref{fig:queue:spec:weak}, and unfolding
the definition of $\queueInv$, we ought to prove the following assertion:
......@@ -60,7 +60,6 @@ When using this concept, instead of using ordinary Hoare triples, we use \emph{l
This kind of triples are like Hoare triples: they specify a program fragment, have a precondition and a postcondition.
The core difference is that they allow opening invariants around the triple: in a sense, when a function is specified using logically atomic triples, one states that said function behaves just like if it were atomic.
The definition of logically atomic triples is further discussed in~\sref{sec:queue:proof:la}
% TODO : référencer la section
and given with detail in previous work~\cite[\S7]{jung-slides-2019,iris-15}.
In order to get a good intuition, let us consider an approximated definition of that concept: a logically atomic triple $\lahoare{P}{e}{Q}$ states, roughly, that the expression $e$ contains a linearization point which has $P$ as a precondition and $Q$ as a postcondition.
This linearization point being atomic, it allows the opening of invariants just like atomic instructions.
......@@ -127,7 +127,7 @@ Hence, we give fewer guarantees than a sequential queue guarded by a lock.
% sinon ça reste vague, je trouve
Interestingly, \hlog{} is able to express this subtle difference between the behavior of our library and that of lock-based implementation: the full specification under weak memory is shown in~\fref{fig:queue:spec:weak}.
It extends the previous specification (\fref{fig:queue:spec:sc}) with views, capturing the mentioned happens-before relationships as follows.
It extends the previous specification (\fref{fig:queue:spec:sc}) with views: to simplify notation, we left the premise $\queueInv$ implicit for all logically atomic specifications. The mentioned happens-before relationships are captured as follows.
......@@ -5,8 +5,10 @@ The verification of fine-grained concurrent data structures is a well-studied pr
Several approaches were tried, targeting various verification frameworks, various data structures in different contexts.
The notion of \emph{linearizability} is central for specifying such libraries.
\citet{dongol2015verifying} gave a survey of the different techniques used for linearizability of concurrent libraries at that time.
%TODO : corriger l'netrée biblio de l'article d'Armaël
Of particular interest in the context of separation logic is the technique of \emph{logical tomicity}, which has been recently proved to be equivalent to linearizability~\cite{gueneau2021theorems}.
This concept has been developped through several iterations
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