From: Mathieu Desnoyers Date: Tue, 19 May 2009 22:07:08 +0000 (-0400) Subject: Add extended urcu model with ooo mem and instruction scheduling X-Git-Tag: v0.1~216 X-Git-Url: https://git.lttng.org/?a=commitdiff_plain;h=551ac1a376f4d1e97b9026aa7436fbd0de6a5218;hp=551ac1a376f4d1e97b9026aa7436fbd0de6a5218;p=urcu.git 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 ---