X-Git-Url: http://git.liburcu.org/?a=blobdiff_plain;f=formal-model%2Fooomem-two-writes%2Fmem.spin;h=828ff4a5d9245e51c3ba529af0ff4c0189caefc8;hb=4b8839f157982c717e307a2045428d3582185b11;hp=4892c5ec333249b74d3b8beab5ff5bee40a268b1;hpb=03c9e0f3f9c72b36b9da30ad4b6ecb055fb6adff;p=urcu.git

diff --git a/formal-model/ooomem-two-writes/mem.spin b/formal-model/ooomem-two-writes/mem.spin
index 4892c5e..828ff4a 100644
--- a/formal-model/ooomem-two-writes/mem.spin
+++ b/formal-model/ooomem-two-writes/mem.spin
@@ -184,6 +184,9 @@ active proctype test_proc_one()
 #ifdef NO_RMB
 	PRODUCE_TOKENS(proc_one_produced, P1_RMB);
 #endif
+#ifdef NO_SYNC
+	PRODUCE_TOKENS(proc_one_produced, P1_SYNC_CORE);
+#endif
 
 	do
 	:: CONSUME_TOKENS(proc_one_produced, P1_PROD_NONE, P1_WRITE) ->
@@ -231,6 +234,9 @@ active proctype test_proc_two()
 #ifdef NO_RMB
 	PRODUCE_TOKENS(proc_two_produced, P2_RMB);
 #endif
+#ifdef NO_SYNC
+	PRODUCE_TOKENS(proc_two_produced, P2_SYNC_CORE);
+#endif
 
 	do
 	:: CONSUME_TOKENS(proc_two_produced, P2_PROD_NONE, P2_WRITE) ->