Commit 710a0416 authored by POTTIER Francois's avatar POTTIER Francois
Browse files

A comment on my view of linearizability.

parent a19b1f11
......@@ -16,6 +16,32 @@ Indeed, as we explained in~\sref{sec:queue:spec:sc}, that specification is desig
But, in \hlog{}, invariants are restricted to a special class of assertions, called \emph{objective} assertions.
As a result, the specification shown in~\fref{fig:queue:specsc} is useful in a weakly consistent context only if the representation predicate $\isQueueSC\elemList$ is objective.
% FP voilà les grandes lignes de ce que je dirais sur la linéarisabilité:
% linearizability is a (complex) technical criterion
% that is defined only in an SC setting
% (because it assumes, as its starting point, that
% we have a *totally ordered* trace of call and
% return events),
% so one must be careful not to use this word in a weak-memory setting,
% unless one has defined its meaning (possible citation of Smith, Winter, and Colvin, 2018).
% In an SC setting, the purpose of linearizability is to imply a refinement relation:
% "the fine-grained concurrent data structure
% behaves like coarse-grained data structure,
% that is, a sequential data structure guarded by a lock".
% Here, even though our concurrent queue has "linearizable
% internal state" in a certain sense (there exists only one
% instance of the predicate $\isQueueSC\elemList$, which
% at every time keeps track of "the current logical state"
% of the queue), it does \emph{not} quite behave like a
% coarse-grained data structure,
% because it imposes fewer \emph{happens-before}
% relationships between accesses. Indeed, all accesses to a lock are totally ordered
% by \emph{happens-before}, whereas our data structure guarantees
% the existence of \emph{happens-before} relationships between
% some, but not all, pairs of operations.
Hence, the first addition in our specification to take into account weakly consistent behaviors is the objectiveness of $\isQueueSC\elemList$.
This corresponds to asserting that the use of atomic accesses in the concurrent queue library is sufficient to maintain its linearizability.
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