-#ifndef NO_RMB
- smp_rmb();
- ooo_mem();
-#endif
- read_two = READ_CACHED_VAR(alpha);
- ooo_mem();
- // test : [] (read_one == 0 -> read_two != 0)
- // test : [] (read_two == 0 -> read_one != 0)
- assert(!(read_one == 0 && read_two == 0));
+
+ do
+ :: CONSUME_TOKENS(proc_two_produced,
+ P2_PROD_NONE, P2_WRITE_ONE) ->
+ ooo_mem();
+ WRITE_CACHED_VAR(alpha, 1);
+ ooo_mem();
+ PRODUCE_TOKENS(proc_two_produced, P2_WRITE_ONE);
+ :: CONSUME_TOKENS(proc_two_produced,
+ P2_WRITE_ONE, P2_WMB) ->
+ smp_wmb();
+ PRODUCE_TOKENS(proc_two_produced, P2_WMB);
+ :: CONSUME_TOKENS(proc_two_produced,
+ P2_WMB, P2_WRITE_TWO) ->
+ ooo_mem();
+ WRITE_CACHED_VAR(beta, 1);
+ ooo_mem();
+ PRODUCE_TOKENS(proc_two_produced, P2_WRITE_TWO);
+ :: CONSUME_TOKENS(proc_two_produced,
+ P2_PROD_NONE | P2_WRITE_ONE
+ | P2_WMB | P2_WRITE_TWO, 0) ->
+ break;
+ od;
+
+ //CLEAR_TOKENS(proc_two_produced,
+ // P2_PROD_NONE | P2_WRITE_ONE | P2_WMB | P2_WRITE_TWO);