Commit 295a0eda authored by POTTIER Francois's avatar POTTIER Francois
Browse files

Citations of the Cosmo paper.

parent 5afbfaad
...@@ -10,8 +10,9 @@ ...@@ -10,8 +10,9 @@
The syntax of (an idealized fragment of) \mocaml{} is presented The syntax of (an idealized fragment of) \mocaml{} is presented
in~\fref{fig:syntax}. It is equipped with a standard call-by-value, in~\fref{fig:syntax}. It is equipped with a standard call-by-value,
left-to-right evaluation. The parts of interest are the memory operations. left-to-right evaluation. The parts of interest are the memory operations.
Their semantics have been described in~[Cosmo]; however, in the present paper, Their semantics have been described in our earlier paper~\citecosmo;
each location now stores an \emph{array} of values, whose cells act as independent however, in the present paper,
each location stores an \emph{array} of values, whose cells act as independent
memory cells with respect to the memory model. memory cells with respect to the memory model.
% %
Cells are rigidly ascribed an access mode~$\accmode$, which is either Cells are rigidly ascribed an access mode~$\accmode$, which is either
......
...@@ -11,6 +11,7 @@ ...@@ -11,6 +11,7 @@
% The base logic and the derived logic. % The base logic and the derived logic.
\newcommand{\llog}{BaseCosmo\xspace} \newcommand{\llog}{BaseCosmo\xspace}
\newcommand{\hlog}{Cosmo\xspace} \newcommand{\hlog}{Cosmo\xspace}
\newcommand{\citecosmo}{\cite{mevel-jourdan-pottier-20}\xspace}
% Lambda-calculus. % Lambda-calculus.
\newcommand{\lc}{$\lambda$-calculus\xspace} \newcommand{\lc}{$\lambda$-calculus\xspace}
......
...@@ -190,8 +190,8 @@ Then, for proving the weaker specification of $\enqueue$ and $\dequeue$, one sim ...@@ -190,8 +190,8 @@ Then, for proving the weaker specification of $\enqueue$ and $\dequeue$, one sim
Up to now, we ignored the weakly consistent behavior of the semantics of \mocaml{}. Up to now, we ignored the weakly consistent behavior of the semantics of \mocaml{}.
In this section, we lift this restriction, and propose a more precise specification for our concurrent queue implementation, which takes into account this aspect. In this section, we lift this restriction, and propose a more precise specification for our concurrent queue implementation, which takes into account this aspect.
We will use the separation logic Cosmo~\cite{TODO}% TODO We will use the separation logic Cosmo~\citecosmo:
: this framework has been designed on top of Iris in order to provide a powerful proof framework for the weak memory model of \mocaml{}. this framework has been designed on top of Iris in order to provide a powerful proof framework for the weak memory model of \mocaml{}.
Because Cosmo is based on Iris, logically atomic triples can also be defined in this logic. Because Cosmo is based on Iris, logically atomic triples can also be defined in this logic.
In fact, the specification shown in~\fref{fig:queue:specsc} still applies. In fact, the specification shown in~\fref{fig:queue:specsc} still applies.
......
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