From 4b8839f157982c717e307a2045428d3582185b11 Mon Sep 17 00:00:00 2001 From: Mathieu Desnoyers Date: Fri, 8 May 2009 14:18:03 -0400 Subject: [PATCH] Add no sync_core() test to ooo two writes model Signed-off-by: Mathieu Desnoyers --- formal-model/ooomem-two-writes/mem.spin | 6 ++++++ formal-model/ooomem-two-writes/read_order_no_sync.define | 1 + 2 files changed, 7 insertions(+) create mode 100644 formal-model/ooomem-two-writes/read_order_no_sync.define 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) -> 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 index 0000000..0d2f8cf --- /dev/null +++ b/formal-model/ooomem-two-writes/read_order_no_sync.define @@ -0,0 +1 @@ +#define NO_SYNC -- 2.34.1