summary |
shortlog |
log |
commit | commitdiff |
tree
raw |
patch |
inline | side by side (from parent 1:
ebb22ff)
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>
* Ensured by STORE_SHARED and LOAD_SHARED.
*/
* 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.
*/
/*
* Wait for previous parity to be empty of readers.
*/
* Ensured by STORE_SHARED and LOAD_SHARED.
*/
* Ensured by STORE_SHARED and LOAD_SHARED.
*/
+ sync_core(); /* Formal model assumes serialized execution */
+
switch_next_urcu_qparity(); /* 1 -> 0 */
/*
switch_next_urcu_qparity(); /* 1 -> 0 */
/*
* Ensured by STORE_SHARED and LOAD_SHARED.
*/
* Ensured by STORE_SHARED and LOAD_SHARED.
*/
+ sync_core(); /* Formal model assumes serialized execution */
+
/*
* Wait for previous parity to be empty of readers.
*/
/*
* Wait for previous parity to be empty of readers.
*/