Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

Commit 33de50cd authored by POTTIER Francois's avatar POTTIER Francois
Browse files

Minor fixes.

parent 38944cdb
......@@ -135,7 +135,7 @@ We now explain the other two pieces of ghost state.
The purpose of the ghost variable~$\gmonos$ is to reflect the fact that statuses
are monotonic.
%
More precisely, they are \emph{strictly} monotonic: every write to a status cell necessarily increases its value. As a consequence, as long as the value of a status cell has not increased, we know that no write happened to it and, in particular, that the view that it stores has not augmented either.
More precisely, they are \emph{strictly} monotonic: every write to a status cell necessarily increases its value. As a consequence, as long as the value of a status cell has not increased, we know that no write happened to it and, in particular, that the view that it stores has not increased either.
%
In other words, we have the monotonicity of the value-view pair stored in a status cell, for the lexicographic order where the order on views is reversed:
%
......@@ -156,8 +156,8 @@ and $\monoWitness \offset {\pair\status\sview}$,
connected via a ghost variable~$\gmonos$.
%
The first assertion, owned by the invariant of the queue, implies that the value-view pair stored in the status cell is exactly $\pair\status\sview$.
In addition, it is exclusive: for any offset~$\offset$, not two assertions
of the form $\ownGhost \gmonos {\mapsingleton\offset{\authfull -}}$ can hold simultaneously.
In addition, it is exclusive: for any offset~$\offset$, two assertions
of the form $\ownGhost \gmonos {\mapsingleton\offset{\authfull -}}$ cannot hold simultaneously.
%
The second assertion means that the value-view pair stored in the status cell is at least $\pair\status\sview$.
Importantly, a witness assertion is persistent: once it has been established, it remains true forever.
......@@ -188,7 +188,7 @@ We thus have the following properties:
%
The first property is the persistency just mentioned. The second property is the fact that a witness gives a lower bound on what the status cell currently stores.
%
The last property asserts that we can update a status cell to any larger or equal contents, and obtain a witness for that contents.
The last property asserts that we can update a status cell to any larger or equal content, and obtain a witness for that content.
We achieve these properties by constructing an adequate CMRA for the values taken by the ghost variable~$\gmonos$. Again, we will not explain standard Iris constructs here, except for one point.
%
......
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