From 1920021f41c26975abd10371dbcadfa2c602a8e2 Mon Sep 17 00:00:00 2001
From: Justin Loew <jloloew@gmail.com>
Date: Thu, 22 Mar 2018 16:30:54 -0500
Subject: [PATCH] Attempt to check for fairness (not currently working)
---
node-preds.maude | 28 +++++++++++++++++++++++++++-
test-node-preds.maude | 11 +++++++++--
2 files changed, 36 insertions(+), 3 deletions(-)
diff --git a/node-preds.maude b/node-preds.maude
index c0ef36d..891c252 100644
--- a/node-preds.maude
+++ b/node-preds.maude
@@ -32,15 +32,41 @@ omod CHECK-NODE-SYSTEM{N :: NZNAT#} is
op inCritSec : Nat/{N} -> Prop .
op twoInCritSec : -> Prop .
op hasUnsentMessages : -> Prop .
+ op canUndergoFurtherTransitions : -> Prop .
+ op isExhausted : -> Formula .
vars N M : Oid . vars A B : AttributeSet . var C : Configuration .
- var I : Nat .
+ vars I J K : Nat . var Q : TaskQueue .
eq < N : Node | mode : Queued, A > C |= isQueued(N) = true .
eq < N : Node | mode : CritSec, A > C |= inCritSec(N) = true .
eq < N : Node | mode : CritSec, A >
< M : Node | mode : CritSec, B > C |= twoInCritSec = true .
eq < N : Node | stimuli : s(I), A > C |= hasUnsentMessages = true .
+
+ eq < N : Node | mode : Queued, A > C |= canUndergoFurtherTransitions = true .
+ ceq < N : Node | runQueue : Q, A > C |= canUndergoFurtherTransitions = true if count(Q) > 0 .
+ ceq < N : Node | ackQueue : Q, A > C |= canUndergoFurtherTransitions = true if count(Q) > 0 .
+ eq < N : Node | mode : Queued, A > C |= canUndergoFurtherTransitions = true .
+ eq < N : Node | mode : CritSec, A > C |= canUndergoFurtherTransitions = true .
+ eq < N : Node | stimuli : s(I), A > C |= canUndergoFurtherTransitions = true .
+ eq < N : Node | numPendingAcks : s(I), A > C |= canUndergoFurtherTransitions = true .
+ eq isExhausted = [] ~ canUndergoFurtherTransitions .
+
+ op isUnfair : -> Formula .
+ op isUnfairAux : Nat/{N} Nat/{N} -> Formula .
+ op isUnfairPair : Oid Oid -> Formula .
+ op isUnfairPre : Oid Oid -> Prop .
+
+ eq isUnfair = isUnfairAux(#, #) .
+ eq isUnfairAux([0], [0]) = False .
+ eq isUnfairAux([s(I)], [0]) = isUnfairPair([s(I)], [0]) \/ isUnfairAux([I], [#]) .
+ eq isUnfairAux([I], [s(J)]) = isUnfairPair([I], [s(J)]) \/ isUnfairAux([I], [J]) .
+ eq isUnfairPair(M, N) =
+ isUnfairPre(M, N) -> ~ ((~ inCritSec(N)) U inCritSec(M)) [owise] .
+ eq < M : Node | mode : Queued, A >
+ < N : Node | mode : Idle, B > C
+ |= isUnfairPre(M, N) = true .
endom
--- Future Invariants:
diff --git a/test-node-preds.maude b/test-node-preds.maude
index 250ee6d..25d330e 100644
--- a/test-node-preds.maude
+++ b/test-node-preds.maude
@@ -4,6 +4,11 @@ view 4 from NZNAT# to NAT is
op # to term 4 .
endv
+--- Kshemkalyani and Singhal (p. 6) lists the requirements of a mutual exclusion algorithm:
+--- * Safety Property: At any instant, only one process can execute the critical section.
+--- * Liveness Property: This property states the absence of deadlock and starvation. Two or more sites should not endlessly wait for messages which will never arrive.
+--- * Fairness: Each process gets a fair chance to execute the CS. Fairness property generally means the CS execution requests are executed in the order of their arrival (time is determined by a logical clock) in the system.
+
--- Check the mutual exclusion property
red modelCheck(init, []~ twoInCritSec) .
--- Expected: true
@@ -13,5 +18,7 @@ red modelCheck(init, []~ twoInCritSec) .
red modelCheck(init, <>[]~ hasUnsentMessages) .
--- Expected: true
---- Check for another watered-down version of strong liveness.
-red modelCheck(init, []()) .
+--- Check for fairness.
+red modelCheck(init, (<> isExhausted) -> [] ~ isUnfair) .
+---red modelCheck(init, (isUnfair_Pre(N:Oid, I:Nat, M:Oid, J:Nat) -> <> isUnfair_Post(N:Oid, I:Nat, M:Oid, J:Nat))) .
+--- Expected: true
--
GitLab