+ /*
+ * 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 */
+