From a9227ee907160443d0e4b1639b274ab9278d92fa Mon Sep 17 00:00:00 2001 From: Mathieu Desnoyers Date: Mon, 8 Oct 2012 17:30:57 -0400 Subject: [PATCH] spinlock model: Simplify state-space Remove useless busy-looping, useless in Promela. Same semantic as the new code: Quoting Michel Dagenais : > http://spinroot.com/spin/Man/condition.html > In Promela , a standalone expression is a valid statement. Execution > of a condition statement is blocked until the expression evaluates to > a non-zero value (or, equivalently, to the boolean value true ). > > http://spinroot.com/spin/Man/separators.html > The semicolon and the arrow are equivalent statement separators in > Promela. The convention is to reserve the use of the arrow separator > to follow condition statements. The arrow symbol can thus be used to > visually identify those points in the code where execution could > block. Signed-off-by: Mathieu Desnoyers --- spinlock/mem.spin | 15 ++------------- 1 file changed, 2 insertions(+), 13 deletions(-) diff --git a/spinlock/mem.spin b/spinlock/mem.spin index 9e87809..072d4d2 100644 --- a/spinlock/mem.spin +++ b/spinlock/mem.spin @@ -21,17 +21,7 @@ byte refcount = 0; inline spin_lock(lock) { - do - :: 1 -> atomic { - if - :: (lock) -> - skip; - :: else -> - lock = 1; - break; - fi; - } - od; + atomic{ !lock -> lock = 1} } inline spin_unlock(lock) @@ -42,8 +32,7 @@ inline spin_unlock(lock) proctype proc_X() { do - :: 1 -> - spin_lock(lock); + :: spin_lock(lock); refcount = refcount + 1; refcount = refcount - 1; spin_unlock(lock); -- 2.34.1