X-Git-Url: http://git.liburcu.org/?p=urcu.git;a=blobdiff_plain;f=urcu.c;h=efbb4b7890a71524fa8264877f3da63565291591;hp=8fd6195662d33a996467fe78a065cacf7d739b01;hb=67c2d80b2b808fe7a6d6d0660ca81c919a81010b;hpb=ebb22fff4a06b0661b55726ad332c4c53f6603fe

diff --git a/urcu.c b/urcu.c
index 8fd6195..efbb4b7 100644
--- 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.
 	 */