X-Git-Url: https://git.lttng.org/?p=urcu.git;a=blobdiff_plain;f=formal-model%2Furcu%2Furcu.spin;h=5ac2f02dd9d80c3abd8d08f2b20136dd9a604635;hp=7f94d3b10232b7ff91520852a65d7236238f5385;hb=710b09b7ba5203ea868240c1746d0ac0fc65f884;hpb=2ba2a48d02164a7f51fbd1686173080240579002

diff --git a/formal-model/urcu/urcu.spin b/formal-model/urcu/urcu.spin
index 7f94d3b..5ac2f02 100644
--- a/formal-model/urcu/urcu.spin
+++ b/formal-model/urcu/urcu.spin
@@ -225,11 +225,16 @@ active [NR_WRITERS] proctype urcu_writer()
 	ooo_mem(i);
 
 	do
-	:: write_lock == 0 ->
-		write_lock = 1;
-		break;
-	:: else ->
-		skip;
+	:: 1 ->
+		atomic {
+			if
+			:: write_lock == 0 ->
+				write_lock = 1;
+				break;
+			:: else ->
+				skip;
+			fi;
+		}
 	od;
 	smp_mb(i);
 	ooo_mem(i);
@@ -251,11 +256,11 @@ active [NR_WRITERS] proctype urcu_writer()
 #endif
 	ooo_mem(i);
 	smp_mb(i);
-	/* free-up step, e.g., kfree(). */
 	ooo_mem(i);
+	write_lock = 0;
+	/* free-up step, e.g., kfree(). */
 	atomic {
 		last_free_gen = old_gen;
 		free_done = 1;
-		write_lock = 0;
 	}
 }