[[PATCH URCU formal]] Restructure urcu_updater() to moreaccurately reflect actual failure scenario.

[Paul E. McKenney]

Restructure urcu_updater() to more accurately reflect actual failure
scenario.

This allows an easier transformation to force failure -- simple #ifdef
out the second counter flip out of urcu_updater()'s model of
"current synchronize_rcu()".

Signed-off-by: Paul E. McKenney <paulmck@xxxxxxxxxxxxxxxxxx>
---
 formal-model/urcu.spin |   41 +++++++++++++++++++++++++++++++----------
 1 files changed, 31 insertions(+), 10 deletions(-)

diff --git a/formal-model/urcu.spin b/formal-model/urcu.spin
index eea18e8..3e18457 100644
--- a/formal-model/urcu.spin
+++ b/formal-model/urcu.spin
@@ -187,10 +187,38 @@ proctype urcu_reader()
 
 proctype urcu_updater()
 {
+	/* prior synchronize_rcu(), second counter flip. */
+	need_mb = 1;
+	do
+	:: need_mb == 1 -> skip;
+	:: need_mb == 0 -> break;
+	od;
+	urcu_gp_ctr = urcu_gp_ctr + RCU_GP_CTR_BIT;
+	need_mb = 1;
+	do
+	:: need_mb == 1 -> skip;
+	:: need_mb == 0 -> break;
+	od;
+	do
+	:: 1 ->
+		if
+		:: (urcu_active_readers & RCU_GP_CTR_NEST_MASK) != 0 &&
+		   (urcu_active_readers & ~RCU_GP_CTR_NEST_MASK) !=
+		   (urcu_gp_ctr & ~RCU_GP_CTR_NEST_MASK) ->
+			skip;
+		:: else -> break;
+		fi;
+	od;
+	need_mb = 1;
+	do
+	:: need_mb == 1 -> skip;
+	:: need_mb == 0 -> break;
+	od;
+
 	/* Removal statement, e.g., list_del_rcu(). */
 	removed = 1;
 
-	/* synchronize_rcu(), first counter flip. */
+	/* current synchronize_rcu(), first counter flip. */
 	need_mb = 1;
 	do
 	:: need_mb == 1 -> skip;
@@ -204,15 +232,13 @@ proctype urcu_updater()
 	od;
 	do
 	:: 1 ->
-		printf("urcu_gp_ctr=%x urcu_active_readers=%x\n", urcu_gp_ctr, urcu_active_readers);
-		printf("urcu_gp_ctr&0x7f=%x urcu_active_readers&0x7f=%x\n", urcu_gp_ctr & ~RCU_GP_CTR_NEST_MASK, urcu_active_readers & ~RCU_GP_CTR_NEST_MASK);
 		if
 		:: (urcu_active_readers & RCU_GP_CTR_NEST_MASK) != 0 &&
 		   (urcu_active_readers & ~RCU_GP_CTR_NEST_MASK) !=
 		   (urcu_gp_ctr & ~RCU_GP_CTR_NEST_MASK) ->
 			skip;
 		:: else -> break;
-		fi
+		fi;
 	od;
 	need_mb = 1;
 	do
@@ -220,10 +246,7 @@ proctype urcu_updater()
 	:: need_mb == 0 -> break;
 	od;
 
-	/* Erroneous removal statement, e.g., list_del_rcu(). */
-	/* removed = 1; */
-
-	/* synchronize_rcu(), second counter flip. */
+	/* current synchronize_rcu(), second counter flip. */
 	need_mb = 1;
 	do
 	:: need_mb == 1 -> skip;
@@ -237,8 +260,6 @@ proctype urcu_updater()
 	od;
 	do
 	:: 1 ->
-		printf("urcu_gp_ctr=%x urcu_active_readers=%x\n", urcu_gp_ctr, urcu_active_readers);
-		printf("urcu_gp_ctr&0x7f=%x urcu_active_readers&0x7f=%x\n", urcu_gp_ctr & ~RCU_GP_CTR_NEST_MASK, urcu_active_readers & ~RCU_GP_CTR_NEST_MASK);
 		if
 		:: (urcu_active_readers & RCU_GP_CTR_NEST_MASK) != 0 &&
 		   (urcu_active_readers & ~RCU_GP_CTR_NEST_MASK) !=
-- 
1.5.2.5

--
To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
the body of a message to majordomo@xxxxxxxxxxxxxxx
More majordomo info at  http://vger.kernel.org/majordomo-info.html
Please read the FAQ at  http://www.tux.org/lkml/