From e5b00154b490ea239a68244ed245cb888e8eed41 Mon Sep 17 00:00:00 2001 From: Mathieu Desnoyers Date: Fri, 29 May 2009 10:59:29 -0400 Subject: [PATCH] Configuration for remote barrier formal verif run Signed-off-by: Mathieu Desnoyers --- formal-model/urcu-controldataflow/DEFINES | 2 +- formal-model/urcu-controldataflow/urcu.spin | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/formal-model/urcu-controldataflow/DEFINES b/formal-model/urcu-controldataflow/DEFINES index 929f5a1..980fad6 100644 --- a/formal-model/urcu-controldataflow/DEFINES +++ b/formal-model/urcu-controldataflow/DEFINES @@ -11,4 +11,4 @@ #define RCU_GP_CTR_NEST_MASK (RCU_GP_CTR_BIT - 1) //disabled -//#define REMOTE_BARRIERS +#define REMOTE_BARRIERS diff --git a/formal-model/urcu-controldataflow/urcu.spin b/formal-model/urcu-controldataflow/urcu.spin index 12f841c..3751868 100644 --- a/formal-model/urcu-controldataflow/urcu.spin +++ b/formal-model/urcu-controldataflow/urcu.spin @@ -927,7 +927,7 @@ active proctype urcu_writer() assert(get_pid() < NR_PROCS); do - :: (loop_nr < 4) -> + :: (loop_nr < 3) -> #ifdef WRITER_PROGRESS progress_writer1: #endif -- 2.34.1