From: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
Date: Fri, 29 May 2009 14:59:29 +0000 (-0400)
Subject: Configuration for remote barrier formal verif run
X-Git-Tag: v0.1~204
X-Git-Url: https://git.lttng.org./?a=commitdiff_plain;h=e5b00154b490ea239a68244ed245cb888e8eed41;p=userspace-rcu.git

Configuration for remote barrier formal verif run

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
---

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