From 67c2d80b2b808fe7a6d6d0660ca81c919a81010b Mon Sep 17 00:00:00 2001 From: Mathieu Desnoyers Date: Wed, 13 May 2009 14:09:34 -0400 Subject: [PATCH] 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 --- urcu.c | 12 ++++++++++++ 1 file changed, 12 insertions(+) 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. */ -- 2.34.1