Add no sync_core() test to ooo two writes model

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>

diff --git a/formal-model/ooomem-two-writes/mem.spin b/formal-model/ooomem-two-writes/mem.spin
index 4892c5ec333249b74d3b8beab5ff5bee40a268b1..828ff4a5d9245e51c3ba529af0ff4c0189caefc8 100644 (file)
--- 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) ->

diff --git a/formal-model/ooomem-two-writes/read_order_no_sync.define b/formal-model/ooomem-two-writes/read_order_no_sync.define
new file mode 100644 (file)
index 0000000..0d2f8cf
--- /dev/null
+++ b/formal-model/ooomem-two-writes/read_order_no_sync.define
@@ -0,0 +1 @@
+#define NO_SYNC