 MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

ICFP21 paper: minor text improvements

parent 5defc6d1
 ... ... @@ -473,13 +473,13 @@ The assertion $\wpre e \predB$ is the weakest precondition for program~$e$ and postcondition~$\predB$ (in Iris, Hoare triples are syntactic sugar for weakest preconditions). The goal of a logically atomic triple is to give the specification of a non-atomic term $e$ \emph{as if it were atomic}. In practice, this means that we ask the proof of $e$ to access the precondition and turn it into the postcondition in \emph{one atomic step} only\footnote{In the full definition of logically atomic triples, it is actually possible to atomically access the precondition without turning it into the postcondition before the final commit. This is not needed for our proof, and out of the scope of this paper.}, which actually corresponds to the commit point of this logically atomic operation. That is, if $e$ satisfies the triple $\lahoare{P}{e}{\pred}$, then it can perform several steps of computation, but as soon as it accesses the resource $P$, it must return the resource~$\pred$ in the same step of computation. Once it has returned $\pred$, then $e$ can perform further computation steps without accessing either $P$ or $\pred$. As explained in \sref{sec:queue:spec:sc}, thanks to this constraint, the client of this specification is allowed to open an invariant around $e$, as if $e$ were atomic. The purpose of a logically atomic triple is to give a specification to a non-atomic program $e$ \emph{as if it were atomic}. In practice, we require that the proof of $e$ accesses the precondition and turns it into the postcondition in \emph{one atomic step} only, which we call the commit point of this logically atomic program. That is, if $e$ satisfies the triple $\lahoare{P}{e}{\pred}$, then it can perform several steps of computation but, as soon as it accesses the resource~$P$, it must return the resource~$\pred$ in the same step of computation.\footnote{The full definition of logically atomic triples allows to access the precondition atomically before the commit point, hence without turning it into the postcondition. This is called \emph{aborting}; it is not needed in our proof, and out of the scope of this paper.} Once it has done so, $e$ can perform further computation steps but $P$ is not available anymore. As explained in \sref{sec:queue:spec:sc}, thanks to this constraint, the client of this specification can open invariants around $e$ as if $e$ were atomic. In order to capture this atomicity requirement, we ask the proof of the logically atomic triple for $e$ to be valid for any postcondition $\predB$ chosen by the client. To capture this atomicity requirement, we ask the proof of the logically atomic triple for $e$ to be valid for any postcondition $\predB$ chosen by the client. Given that $\predB$ is arbitrary, the only means of establishing this postcondition is to use the premise $\pvs[\top][\emptyset] \Exists x. P \ISEP (\Forall v. \pred\;v \WAND\pvs[\emptyset][\top] \predB\;v)$, which is known as an \emph{atomic update}. When desired, this atomic update gives access to the precondition~$P$ for some value of $x$, and, in exchange for the postcondition $\pred$ of the logically atomic triple, it returns the resource $\predB$, which can then be used to finish the proof. 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. ... ...
 ... ... @@ -155,7 +155,7 @@ a dequeuer to an enqueuer.% This is not entirely true: the implementation shown in \sref{sec:queue:impl} does create a happens-before relationship from the dequeuer of rank~$\idx$ to the enqueuer of rank~$\idx+\capacity$ (hence also to all enqueuers of subsequent ranks). We choose to not reveal this in the specification, since the specification hides the constant~$\capacity$. We choose to not reveal this in the specification, since the constant~$\capacity$ is an implementation detail. } % Hence, it provides fewer guarantees than a sequential queue guarded by a lock. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!