From f321bf383dd9b5940b31e4db6c9e18a5abaa0213 Mon Sep 17 00:00:00 2001 From: "Paul E. McKenney" Date: Thu, 12 Feb 2009 13:25:05 -0500 Subject: [PATCH] Fix formal model nesting Also, the original model I sent out has a minor bug that prevents it from fully modeling the nested-read-side case. The patch below fixes this. Signed-off-by: Paul E. McKenney Signed-off-by: Mathieu Desnoyers --- formal-model/urcu.spin | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/formal-model/urcu.spin b/formal-model/urcu.spin index e5bfff3..611464b 100644 --- a/formal-model/urcu.spin +++ b/formal-model/urcu.spin @@ -124,9 +124,13 @@ proctype urcu_reader() break; :: tmp < 4 && reader_progress[tmp] != 0 -> tmp = tmp + 1; - :: tmp >= 4 -> + :: tmp >= 4 && + reader_progress[0] == reader_progress[3] -> done = 1; break; + :: tmp >= 4 && + reader_progress[0] != reader_progress[3] -> + break; od; do :: tmp < 4 && reader_progress[tmp] == 0 -> -- 2.34.1