Learning RRD by testing common MPMC stack

[Brendon Costa]

Hi,

First of all, thanks for making this tool. I think once I understand it better it will be very useful and would like to use it to test the various lockfree data structures we have.

I am trying to learn how to use RRD on a basic MPMC lockfree stack that I have seen documented as a common tutorial in many places on the internet. I understand that this stack is probably not a very good structure to use performance wise in a lot of situations but dont want to get into that I am using it to try and understand RRD.

I am trying to make sure I understand why RRD is identifying a data race, and if this particular race is safe in my scenario and if so is there a way to silence it in RRD.

---- relevant section of results ---

[2061] 1: <0x12708c8> store, value=4294967295, in PushNode, stack.cpp(134)

[2062] 1: <0x11ff2b8> CAS succ orig=4294967295, cmp=4294967295, xchg=4294967296, order=seq_cst, in PushNode, stack.cpp(139)

[2063] 2: <0x11ff2f0> atomic load, value=4294967297, order=acquire, in PopNode, stack.cpp(99)

[2064] 2: <0x1270908> load, value=2, in PopNode, stack.cpp(113)

[2065] 2: <0x11ff2f0> CAS succ orig=4294967297, cmp=4294967297, xchg=8589934594, order=seq_cst, in PopNode, stack.cpp(116)

[2066] 2: <0x1270928> store, value=719885387, in Push, stack.cpp(149)

[2067] 2: <0x11ff2b8> atomic load, value=4294967295 [NOT CURRENT], order=acquire, in PushNode, stack.cpp(125)

[2068] 2: <0x1270908> store, value=4294967295, in PushNode, stack.cpp(134)

[2069] 2: <0x11ff2b8> CAS fail orig=4294967296, cmp=4294967295, xchg=4294967297, order=seq_cst, in PushNode, stack.cpp(139)

[2070] 2: <0x1270908> store, value=0, in PushNode, stack.cpp(134)

[2071] 3: <0x11ff2f0> atomic load, value=0 [NOT CURRENT], order=acquire, in PopNode, stack.cpp(99)

[2072] 3: <0x12708c8> load, value=0, in PopNode, stack.cpp(113)

[2073] 3: DATA RACE (data race detected), in PopNode, stack.cpp(113)

It looks like a thread (1) in "PushNode, stack.cpp(134)" can modify the nodes next_index (0x12708c8) while another thread (3) is reading the next_index (0x12708c8) in "PopNode, stack.cpp(113)". 

The key thing here is that I expect the thread in PopNode on this race to fail the next compare_exchange_weak() and so I believe this particular race is "benign".

The two relevant lines can be found in the code at the bottom, are:

* In PopNode:

next.node_index = pool[orig.node_index].next_index($);

* In PushNode:

node->next_index($) = orig.node_index;

I can silence this by making node_index *not* a rl::var object (See macro: SKIP_TRACKING_BENIGN_RACE), but am worried this is the wrong way to silence this problem. 

Is there a way to indicate to RRD that I expect a race in a specific spot, but it is safe so long as the compare_exchange fails?

Also, can you see any other issues with this stack example?

Thanks,

Brendon.

--- full example included below ---

#include "stdafx.h"

#include "../../relacy/relacy.hpp"

#include <vector>

#include <assert.h>

using namespace rl;

// Uncomment this define if you want to stop RRD tracking the Node::next_index which is known to have a benign race

//#define SKIP_TRACKING_BENIGN_RACE 1

class MPMCBoundedStack

{

public:

typedef int Data;

struct Node

{

Node(unsigned long index_in, unsigned long next_index_in)

: index(index_in)

, next_index(next_index_in)

, data(0)

{

}

const unsigned long index;

#ifdef SKIP_TRACKING_BENIGN_RACE

unsigned long next_index;

#else

rl::var<unsigned long> next_index;

#endif

rl::var<Data> data;

Node(const Node& rhs) = default;

private:

Node& operator=(const Node& rhs);

};

static const unsigned long INVALID_INDEX = 0xFFFFFFFFU;

struct Head

{

typedef unsigned long long Combined;

unsigned long write_sequence;

unsigned long node_index;

Combined GetCombined() const

{

Combined combined = ((Combined)write_sequence << 32) & 0xFFFFFFFF00000000ULL;

combined |= (node_index & 0xFFFFFFFFULL);

return combined;

}

void SetCombined(Combined combined)

{

node_index = combined & 0xFFFFFFFFULL;

write_sequence = (combined >> 32) & 0xFFFFFFFFULL;

}

};

static const size_t MAX_SIZE = 1024;

std::vector<Node> pool;

atomic<Head::Combined> head;

atomic<Head::Combined> unalloced;

MPMCBoundedStack()

{

// NOTE: Not using RRD ($) in constructor as I dont think it is required

//assert(head.is_lock_free());

//assert(unalloced.is_lock_free());

Head init_head;

init_head.write_sequence = 0;

init_head.node_index = INVALID_INDEX;

head.store(init_head.GetCombined(), memory_order_release);

pool.reserve(MAX_SIZE);

for (size_t i = 0; i < MAX_SIZE; i++)

{

unsigned int next = i + 1;

if (i == MAX_SIZE - 1)

next = INVALID_INDEX;

pool.push_back(Node(i, next));

}

Head init_unalloced;

init_unalloced.write_sequence = 0;

init_unalloced.node_index = 0;

unalloced.store(init_unalloced.GetCombined(), memory_order_release);

}

Node* PopNode(atomic<Head::Combined>& list)

{

Head next;

Head::Combined orig_combined = list($).load(mo_acquire);

Head orig;

do

{

orig.SetCombined(orig_combined);

if (orig.node_index == INVALID_INDEX)

return NULL;  // empty stack

next.write_sequence = orig.write_sequence + 1;

#ifdef SKIP_TRACKING_BENIGN_RACE

next.node_index = pool[orig.node_index].next_index;

#else

next.node_index = pool[orig.node_index].next_index($);

#endif

} while (!list($).compare_exchange_weak(orig_combined, next.GetCombined(), rl::mo_seq_cst));

return &pool[orig.node_index];

}

void PushNode(atomic<Head::Combined>& list, Node *node)

{

Head next;

Head::Combined orig_combined = list($).load(mo_acquire);

Head orig;

do

{

orig.SetCombined(orig_combined);

#ifdef SKIP_TRACKING_BENIGN_RACE

node->next_index = orig.node_index;

#else

node->next_index($) = orig.node_index;

#endif

next.write_sequence = orig.write_sequence + 1;

next.node_index = node->index;

} while (!list($).compare_exchange_weak(orig_combined, next.GetCombined(), rl::mo_seq_cst));

}

bool Push(const Data& data)

{

Node* node = PopNode(unalloced);

if (node == NULL)

return false;

node->data($) = data;

PushNode(head, node);

return true;

}

bool Pop(Data& data)

{

Node* node = PopNode(head);

if (node == NULL)

return false;

data = node->data($);

PushNode(unalloced, node);

return true;

}

};

struct MPMCBoundedStack_test : rl::test_suite<MPMCBoundedStack_test, 4>

{

MPMCBoundedStack s_;

int produced_count_;

int consumed_count_;

void before()

{

produced_count_ = 0;

consumed_count_ = 0;

}

void after()

{

typedef rl::test_suite<MPMCBoundedStack_test, 4> base_t;

RL_ASSERT(consumed_count_ == produced_count_);

//RL_ASSERT(base_t::params::thread_count == consumed_count_);

}

void thread(unsigned /*index*/)

{

if (s_.Push(rand() + 1))

{

produced_count_ += 1;

int data;

bool result = s_.Pop(data);

RL_ASSERT(result);

RL_ASSERT(data);

consumed_count_ += 1;

}

}

};

int main()

{

rl::simulate<MPMCBoundedStack_test>();

return 0;

}

[Dmitry Vyukov]

Hi Brendon,

There is no such thing as "benign data race" in C/C++. The standards
make it very clear. E.g. C++ says:
1.10/21:
Any such data race results in undefined behavior.

So this is not about "silencing" Relacy. This is about fixing a bug in
your code.

Next should be an atomic variable if it is a subject to data races otherwise.

See e.g. https://software.intel.com/en-us/blogs/2013/01/06/benign-data-races-what-could-possibly-go-wrong
for what can go wrong with such seemingly "benign" races.

> --
> You received this message because you are subscribed to the Google Groups
> "Relacy Race Detector" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to relacy+un...@googlegroups.com.
> To post to this group, send email to rel...@googlegroups.com.
> Visit this group at https://groups.google.com/group/relacy.
> For more options, visit https://groups.google.com/d/optout.



--
Dmitry Vyukov

All about lockfree/waitfree algorithms, multicore, scalability,
parallel computing and related topics:
http://www.1024cores.net