Linearizibility issues

[b-mezei]

I have used the model checker GenMC to try and verify some data structures in the library. Specifically, I tried to check for the linearizibility of the data structures using the tool RELINCHE. With the help of the tool, I have found a few issues in some structures that prevent them from being linearizable, and under the C++ weak memory model, allow accessing and dereferencing unallocated memory.

1. Intrusive Michael & Scott's queue:
   If a thread enqueues, then two threads dequeue after each other, the second dequeue thread isn't synchronized properly. The first dequeue operation advances the head with acquire ordering:
   if ( m_pHead.compare_exchange_strong( h, pNext, memory_model::memory_order_acquire, atomics::memory_order_relaxed ))
   This means that when the second dequeue tries to load the head, again with acquire ordering (during the hazard pointer protect operation), and access its m_pNext field, the memory model doesn't guarantee that that field has been initialized at that point, as the synchronization is insufficient. A fix would be to change the ordering to release in this line.

2. Intrusive optimistic queue:
   There is a very similar issue with this data structure. It occurs again when a thread enqueues, then two threads dequeue. The synchronization issue is virtually the same, the second dequeue isn't synchronized sufficiently with the first, so it is allowed to access uninitialized memory.
   if ( m_pHead.compare_exchange_weak( pHead, pFirstNodePrev, memory_model::memory_order_acquire, atomics::memory_order_relaxed )) {
   A fix would be to change the ordering to release in this line.

The two proposed changes would make the data structures linearizable. As a side node, the Treiber stack and Moir queue data structures are linearizable, provably so with the tool.

[TomlyYang]

这是来自QQ邮箱的假期自动回复邮件。   您好，我最近正在休假中，无法亲自回复您的邮件。我将在假期结束后，尽快给您回复。