PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_MB);
:: CONSUME_TOKENS(proc_urcu_writer, WRITE_PROC_ALL_TOKENS, 0) ->
CLEAR_TOKENS(proc_urcu_writer, WRITE_PROC_ALL_TOKENS_CLEAR);
break;
PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_MB);
:: CONSUME_TOKENS(proc_urcu_writer, WRITE_PROC_ALL_TOKENS, 0) ->
CLEAR_TOKENS(proc_urcu_writer, WRITE_PROC_ALL_TOKENS_CLEAR);
break;