linux-kernel - [[PATCH URCU formal]] Restructure urcu_updater() to more accurately reflect actual failure scenario.

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [thread-next>] [day] [month] [year] [list]

Message-ID: <20090220015747.GA19488@linux.vnet.ibm.com>
Date:	Thu, 19 Feb 2009 17:57:47 -0800
From:	"Paul E. McKenney" <paulmck@...ux.vnet.ibm.com>
To:	ltt-dev@...ts.casi.polymtl.ca
Cc:	compudj@...stal.dyndns.org, bert.wesarg@...glemail.com,
	bob@...son.ibm.com, linux-kernel@...r.kernel.org
Subject: [[PATCH URCU formal]] Restructure urcu_updater() to more
	accurately reflect actual failure scenario.

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@...ux.vnet.ibm.com>
---
 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@...r.kernel.org
More majordomo info at  http://vger.kernel.org/majordomo-info.html
Please read the FAQ at  http://www.tux.org/lkml/