Use sync_core() in the write side to match current formal verif model

The formal model we currently have assumes serialized instruction execution on
the write-side. Until we extend this model to allow out-of-order instruction
execution, add equivalent synchronization in the library code.

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

diff --git a/urcu.c b/urcu.c
index 8fd6195662d33a996467fe78a065cacf7d739b01..efbb4b7890a71524fa8264877f3da63565291591 100644 (file)
--- a/urcu.c
+++ b/urcu.c
@@ -248,6 +248,14 @@ void synchronize_rcu(void)
         * Ensured by STORE_SHARED and LOAD_SHARED.
         */
 
+       /*
+        * Current RCU formal verification model assumes sequential execution of
+        * the write-side. Add core synchronization instructions. Can be removed
+        * if the formal model is extended to prove that reordering is still
+        * correct.
+        */
+       sync_core();    /* Formal model assumes serialized execution */
+
        /*
         * Wait for previous parity to be empty of readers.
         */
@@ -261,6 +269,8 @@ void synchronize_rcu(void)
         * Ensured by STORE_SHARED and LOAD_SHARED.
         */
 
+       sync_core();    /* Formal model assumes serialized execution */
+
        switch_next_urcu_qparity();     /* 1 -> 0 */
 
        /*
@@ -271,6 +281,8 @@ void synchronize_rcu(void)
         * Ensured by STORE_SHARED and LOAD_SHARED.
         */
 
+       sync_core();    /* Formal model assumes serialized execution */
+
        /*
         * Wait for previous parity to be empty of readers.
         */