Commit 0a3d8195 authored by Glen Mével's avatar Glen Mével
Browse files

rename files accordingly

parent 3fa82058
\subsection{Proof of the Specification for the Pipeline}
\label{sec:pipeline:proof}
\input{figure-pipeline-invariant}
\input{figure-pipeline-inv}
......@@ -5,7 +5,7 @@
\section{Proof of the Specification for the Ring Buffer}
\label{sec:queue:proof}
\input{figure-queue-invariant}
\input{figure-queue-inv}
% TODO: tout ceci est objectif
......
\subsection{Specification under weak memory}
\label{sec:queue:spec:weak}
\input{figure-queue-spec}
\input{figure-queue-spec-weak}
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.
......
Supports Markdown
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