+ WRITE_DATA) ->
+ ooo_mem(i);
+ cur_data = (cur_data + 1) % SLAB_SIZE;
+ WRITE_CACHED_VAR(rcu_data[cur_data], WINE);
+ PRODUCE_TOKENS(proc_urcu_writer, WRITE_DATA);
+
+
+ :: CONSUME_TOKENS(proc_urcu_writer,
+ WRITE_DATA,
+ WRITE_PROC_WMB) ->
+ smp_wmb(i);
+ PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_WMB);
+
+ :: CONSUME_TOKENS(proc_urcu_writer,
+ WRITE_PROC_WMB,
+ WRITE_XCHG_PTR) ->
+ /* rcu_xchg_pointer() */
+ atomic {
+ old_data = READ_CACHED_VAR(rcu_ptr);
+ WRITE_CACHED_VAR(rcu_ptr, cur_data);
+ }
+ PRODUCE_TOKENS(proc_urcu_writer, WRITE_XCHG_PTR);
+
+ :: CONSUME_TOKENS(proc_urcu_writer,
+ WRITE_DATA | WRITE_PROC_WMB | WRITE_XCHG_PTR,