From: Mathieu Desnoyers Date: Fri, 8 May 2009 18:18:03 +0000 (-0400) Subject: Add no sync_core() test to ooo two writes model X-Git-Tag: v0.1~248 X-Git-Url: https://git.lttng.org./?a=commitdiff_plain;h=4b8839f157982c717e307a2045428d3582185b11;p=urcu.git Add no sync_core() test to ooo two writes model Signed-off-by: Mathieu Desnoyers --- 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