Add extended urcu model with ooo mem and instruction scheduling

Add extended urcu model with ooo mem and instruction scheduling

Here is the new model I worked on for the past weeks. It models :

- out-of-order memory accesses.
- instruction scheduling by the CPU on the write and read sides.

The model as committed in the repository at

formal-model/urcu-controldataflow

models the urcu with memory barriers on the read-side. It works exactly
as expected. mb() on the read-side is enabled when we have this in
the DEFINES file :

//#define REMOTE_BARRIERS   (commented out)

To run all tests, just fire :

make
(with spin 5.1.7 here. 5.2.0 has a bug with arrays of size 1)

Verification summary
asserts.log:State-vector 64 byte, depth reached 2801, errors: 0
urcu_free.log:State-vector 88 byte, depth reached 3302, errors: 0
urcu_free_no_mb.log:State-vector 88 byte, depth reached 24407, errors: 1
urcu_free_single_flip.log:State-vector 88 byte, depth reached 2904, errors: 1
urcu_progress_reader.log:State-vector 80 byte, depth reached 3353, errors: 0
urcu_progress_writer_error.log:State-vector 80 byte, depth reached 8035, errors: 1
urcu_progress_writer.log:State-vector 80 byte, depth reached 3348, errors: 0

However, I still have a problem modeling the signal-based barriers.

(remove comment from the define)

make urcu_free_single_flip should generate an error (just like it does
with the reader-mb() case), but it does not. I think it's caused by
added serialization due to the writer waiting on the reader barriers.

Normally, this model should behave similarly to yours : it should honor
the barrier requests before each read-side instruction IIF the
instruction execution order is in program order.

I'm pretty sure I missed something obvious, but I think it's time I
share the model I have with you so you might help me spot what I missed.
It may be as simple as an incorrect instruction scheduling dependency
too.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>