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 fce9cbc1 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

misc changes in section 4

parent bf3174ee
......@@ -33,9 +33,9 @@ operation of the CMRA:
\).
In \hlog, ghost state is objective, as it is independent from the physical state
of the memory.%
\footnote{%
In fact, the physical memory is itself encoded as a piece of ghost state.
}
%% \footnote{%
%% In fact, the physical memory is itself encoded as a piece of ghost state.
%% }
Ghost state can be coupled with invariants such as the ones presented in \sref{sec:queue:spec:sc} to describe protocols that threads must follow to access shared resources.
......@@ -153,12 +153,12 @@ $\ownGhost \gmonos {\mapsingleton\offset{\authfull \pair\status\sview}}$
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$.
The first assertion, owned by the invariant of the queue is connected by the invariant to the value-view pair stored in the status cell.
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.
The second assertion $\monoWitness \offset {\pair\status\sview}$ 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 and can be duplicated at will.
We thus have the following properties:
%
......@@ -671,7 +671,7 @@ that the invariant gives us:
\status_{\modcap{\idx-\capacity}} = 2(\idx-\capacity)+1
\]%
%
Again the second branch is absurd because the status is monotonic. Hence the slot we are claiming is available indeed.
Again the second disjunct is absurd because the status is monotonic. Hence the slot we are claiming is available indeed.
%
From this
%$\emptyCell {(\idx-\capacity)} {\nthStatusView{\modcap\idx}}$,
......@@ -726,14 +726,14 @@ The invariant then gives us for slot~$\modcap\idx$:
\status_{\modcap\idx} = 2\idx
\]%
%
The left branch would own our write~token, but we already have it and it is exclusive;
hence we are in the right branch, $\status_{\modcap\idx} = 2\idx = s^1$.
The left disjunct would own our write~token, but we already have it and it is exclusive;
hence we are in the right disjunct, $\status_{\modcap\idx} = 2\idx = s^1$.
We perform the atomic write with value~$\status^2 \eqdef 2\idx+1$ (strict
monotonicity is respected),
and since we have both $\seen\eview$ and $\seen\viewB$ in context, we can push
the view~$\sview^2 = \eview \viewjoin \viewB$ to this atomic location while
writing.
We then switch to the left branch, by constituting the assertion:
We then switch to the left disjunct, by constituting the assertion:
%
\[%
\fullCell \idx {\pair{\status^2}{\sview^2}} {\pair\elem\eview}
......
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