Commit 49d57a97 by Glen Mével

### more work on impl

  - try introducing some invariants more precisely, to make the
explanation of the code easier
- address JH’s remark about order of writes
parent 2a53c3d2
 ... ... @@ -95,7 +95,18 @@ The status encodes this information in a single integer, as follows: \end{itemize}% Let~\head\ and~\tail\ be the value of references \refhead and \reftail, respectively. We say that the buffer is \emph{full} when slot~$\modcap\head$ has respectively. % At any time, the ranks of items that are stored (or in the process of being stored) in the queue range from~\tail\ included to~\head\ excluded. As will be verified when we will be proving the correctness of the implementation, an invariant property of the queue is: % $0 \leq \tail \leq \head \leq \tail+\capacity$ We say that the buffer is \emph{full} when slot~$\modcap\head$ has a status less than $2\head$; in other words, the next slot at which to enqueue is still in use for a rank less than~\head\ % ... ... @@ -115,18 +126,94 @@ or it has status $2\tail$ and is available for a future item of rank~\tail). % This implies that $\head = \tail$. \subsubsection{Some invariants of the queue} Once the queue has been created, the reference~\refhead is only accessed from function~\tryenqueue. The only place where it is modified is the compare-and-set operation in this function, which attempts to increment it by one, using a compare-and-set operation. Hence this counter is strictly monotonic, and we can regard a successful incrementation from~\head\ to~$\head+1$ as uniquely attributing rank~\head\ to the candidate enqueuer. Only then it is allowed to write into slot~$\modcap\head$. Similarly, \reftail is only accessed from function~\trydequeue, is strictly monotonic, and a successful incrementation from~\tail\ to~$\tail+1$ uniquely attributes rank~\tail\ to the candidate dequeuer. Only then it is allowed to write into slot~$\modcap\tail$. The status of a given slot is strictly monotonic too. Indeed, there are two places where it is updated: either a successful enqueuer makes it odd after having read that it was even, or a successful dequeuer makes it even after having read that it was odd. % As an enqueuer, when we write $2\head+1$, no other enqueuer updated the status since we read it to be $2\head$, because only us have been attributed rank~\head. In particular, it remained even, so no dequeuer tried to obtain rank~\head\ and update the status of slot~$\modcap\head$. Hence, the status is still $2\head$ when we overwrite it with $2\head+1$. % Symmetrically, the status is still $2\tail+1$ when a dequeuer overwrites it with $2(\tail+\capacity)$. % GLEN: difficile d’expliquer un invariant comme ça, c’est forcément cyclique… \subsubsection{Explanation of the code} The function~\enqueue repeatedly calls \tryenqueue until it succeeds; the latter can fail either because the buffer is full or because of a competing enqueuer.% % \footnote{\label{fn:distinguishfail}% We currently do not distinguish between these two causes, but this is feasible. } When calling \tryenqueue, we start by reading the current value~\head\ of the reference~\refhead. To check that slot~$\modcap\head$ is available for rank~\head, we read its status. % If it differs from~$2\head$, we fail % (to be more precise, a status less than~$2\head$ indicates that the buffer is full; a status greater than~$2\head$ indicates interference from other threads and, as explained later, this interference implies a competing enqueuer being attributed rank~\head\ before we have). If the status is $2\head$, then we try to increment \refhead from~\head\ to~$\head+1$. % If the CAS fails, we fail (it is again because of a competing enqueuer). If the CAS succeeds, then we are attributed rank~\head\ and can proceed to inserting an item into slot~$\modcap\head$. As explained early, its status has not changed since we read it: the slot is still available. % We write the new item, then we update the status accordingly. This update must come last, as it serves as a signal that the slot is now occupied with an item and ready for dequeuers. %Notice that, under weak memory, the order of these two writes matters: the %atomic write to \refstatuses must propagate the information that the nonatomic %write to \refelements has taken place. Thus, a thread which dequeues this item %(after reading its status) is certain to read a correct value from the array %\refelements. This is a typical release/acquire idiom. % TODO : JH : Ok, mais c'est aussi nécessaire dasn un modèle SC, puisque l'écriture du statut correspond au relacheemnt du lock : si on s'amusait à remplir la cellule après écrire dasn statut, alors le dequeuer pourrait commencer à lire le contenu de la cellule avant que celle-ci ait été remplie, non ? Pour moi, c'est une meilleure justification pour l'odre des opérations. Les questions de mémoire faible sont plus subtiles et nécessitent d'avoir compris un peu la spec. Similarly, \dequeue repeatedly calls \trydequeue untils it succeeds; the latter can fail either because the buffer is empty or because of a competing dequeuer.% the latter works analogously to \tryenqueue,% % \footnote{% Overwriting the extracted value with a unit value~$\Unit$ is unnecessary for functional correctness but, as mentioned in~\fnref{fn:memleak}, it prevents memory leaks. } % and can fail either because the buffer is empty or because of a competing dequeuer.% % \footref{fn:distinguishfail} \subsubsection{Interactions between threads} %A noteworthy feature of this implementation is that the head and tail are %independent of each other, so that an enqueuer and a dequeuer never race %against each other. This is why the data structure does not guarantee any ... ... @@ -189,7 +276,7 @@ Possible situations are: in that case, the dequeuer continues unaffected; the candidate enqueuer fails, but the existence of a dequeuer for a rank at least \idx\ implies that another enqueuer has been attributed rank~\idx\ before the candidate enqueuer, hence we can connect its failure to the before the candidate enqueuer, hence we can connect its failure to competition with that other enqueuer; \item symmetrically, a enqueuer enqueuing an item of rank~$\idx + r\capacity$ ... ... @@ -200,55 +287,8 @@ Possible situations are: the candidate dequeuer fails, but the existence of a enqueuer for a rank at least $\idx+\capacity$ implies that another dequeuer has been attributed rank~\idx\ before the candidate dequeuer, hence we can connect its failure to the competition with that other dequeuer; to competition with that other dequeuer; \end{itemize}% \subsubsection{Explanation of \tryenqueue and \trydequeue} When calling \tryenqueue, we start by reading the current value~\head\ of the reference~\refhead. To check that slot~$\modcap\head$ is available for rank~\head, we read its status. % If it differs from~$2\head$, we fail % (a status less than~$2\head$ indicates that the buffer is full; %a status greater than~$2\head$ indicates that the slot has been filled, then %possibly emptied, possibly several times, since we read \refhead: that is, we %have lost a race against other enqueuers). a status greater than~$2\head$ indicates that someone has increased the status since we read \refhead, and as explained further on, only an enqueuer that has been attributed rank~\head\ before we have is permitted to do so). If the status is $2\head$, then we try to increment the atomic counter~\refhead from~\head\ to~$\head+1$, using a compare-and-set operation. % Note that this is the only place in the implementation where \refhead is modified, hence that counter is monotonic. % If the CAS fails, it is again because of a competing enqueuer; in that case, we fail. If the CAS succeeds, then no other enqueuer can successfully perform the same increment, so we can regard this achievement as attributing us rank~\head, and giving us an unique permission to write an item into slot~$\modcap\head$. No one else has got that permission since we initially read \refhead, so this slot’s status has not changed: it is still available. % We write the new item, then update the status accordingly. Notice that, under weak memory, the order of these two writes matters: the atomic write to \refstatuses must propagate the information that the nonatomic write to \refelements has taken place. Thus, a thread which dequeues this item (after reading its status) is certain to read a correct value from the array \refelements. This is a typical release/acquire idiom. % TODO : JH : Ok, mais c'est aussi nécessaire dasn un modèle SC, puisque l'écriture du statut correspond au relacheemnt du lock : si on s'amusait à remplir la cellule après écrire dasn statut, alors le dequeuer pourrait commencer à lire le contenu de la cellule avant que celle-ci ait été remplie, non ? Pour moi, c'est une meilleure justification pour l'odre des opérations. Les questions de mémoire faible sont plus subtiles et nécessitent d'avoir compris un peu la spec. The function~\trydequeue works analogously.% % \footnote{% Overwriting the extracted value with a unit value~$\Unit$ is unnecessary for functional correctness but, as mentioned in~\fnref{fn:memleak}, it prevents memory leaks. } Hence competition happens only between enqueuers, or between dequeuers.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!