From: Mathieu Desnoyers Date: Wed, 13 May 2009 18:09:34 +0000 (-0400) Subject: Use sync_core() in the write side to match current formal verif model X-Git-Tag: v0.1~225 X-Git-Url: http://git.liburcu.org/?p=urcu.git;a=commitdiff_plain;h=67c2d80b2b808fe7a6d6d0660ca81c919a81010b 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 --- 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. */