Add clock vectors

[bartoszmodelski]

The core of DSCheck is closely following the design introduced in the DPOR paper, except for clock vectors, which are missing. This PR adds them.

Motivation

We want to be able to track happens before relationship as it is critical to an efficient search. For example, consider the following program:

Thread A 
a1: write x=1
a2: write y=2 

Thread B 
b1: write y=1 
b2: write x=2 

If we were to do a full search, we'd explore 6 traces:

a1 a2 b1 b2 
a1 b1 a2 b2 
a1 b1 b2 a2 
b1 b2 a2 a2
b1 a1 b2 a2 
b1 a1 a2 b2 

But many of these trace are redundant as far as the terminal state is concerned. For example, consider: a1 b1 a2 b2. Reordering of either the first two or the last two transitions leads to the same result (x=2, y=2). In fact, the only three possible terminal states are (x=1, y=2), (y=1, x=2), (x=2, y=2) and as long as these are covered, so are all possible realizations.

Results

There's a significant improvement on tests with multiple variables:

• Artificial test. Number of traces goes down from 31 to 5.
• Michael-Scott queue. The runtime on tests with 4 items goes down from 0.2 s to ~0.001 s. Eyeballing it, previously adding a single item increased the runtime 7-fold, while now it doubles it.

There's a 10-15% slowdown on test_list, which has all threads focus on a single variable, due to cost of extra accounting. If we don't find any further optimizations here in the future, we can always add a flag for fast-path here.

test_naive_counter is too small to be affected.

Design

I followed the section 4.2 and figure 5 in DPOR paper. It was not that trivial due to sheer amount of notation but it should be easier to verify than to translate for the first time.

I think the best resource is the paper itself. In part because I'm not an expert in this area, and another pair of eyes looking at this could potentially discover things I've missed (even in terms of building understanding). Having said that, I'm super happy to jump on a call or try to explain more here.

I'd recommend a quick read of sections 1-3, and spending more time on section 4. The paper explains vector clocks but I've supported myself with Martin Kleppmann's excellent short lecture on them.