Commit e2e75b32 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Merge branch 'master' of gitlab.inria.fr:gmevel/cosmo

parents fce9cbc1 796452c9
......@@ -461,7 +461,7 @@ The sixth rule corresponds to step~\ref{item:token1} in the list above, where we
Likewise, the last rule corresponds to step~\ref{item:token3}, where we turn a write~token into a read~token of the same rank.
Lastly, the finite map described in the internal invariant is such that,
whenever we own a read~token (respectively a write~token) of rank~$\idx$, that rank necessarily lies in the range~$[\head-\capacity, \tail)$ (respectively $[\tail, \head)$), where $\tail$ and $\head$ are the values of $\reftail$ and $\refhead$ which are existentially quantified in the invariant.
whenever we own a read~token (respectively a write~token), the rank of this token necessarily lies in the range~$[\head-\capacity, \tail)$ (respectively $[\tail, \head)$), where $\tail$ and $\head$ are the values of $\reftail$ and $\refhead$ which are existentially quantified in the invariant.
Thanks to that property, at step~\ref{item:token4} (respectively~\ref{item:token2}), when a dequeuer (respectively an enqueuer) returns the token, it knows that the rank it has been operating on is still in the right range---in other words, that the queue has not advanced too far while the thread was working.
%To implement a token in ghost state, we again use an authority over an exclusive
......
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