| Copyright | (c) Levent Erkok |
|---|---|
| License | BSD3 |
| Maintainer | erkokl@gmail.com |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Documentation.SBV.Examples.Lists.BoundedMutex
Description
Proves a simple mutex algorithm correct up to a given bound.
Synopsis
- data State
- cv2State :: String -> [CV] -> State
- _undefiner_State :: a
- type SState = SBV State
- sIdle :: SBV State
- sReady :: SBV State
- sCritical :: SBV State
- isIdle :: SBV State -> SBool
- isReady :: SBV State -> SBool
- isCritical :: SBV State -> SBool
- sCaseState :: Mergeable result => SBV State -> result -> result -> result -> result
- mutex :: [SState] -> [SState] -> SBool
- validSequence :: Integer -> [SInteger] -> [SState] -> SBool
- validTurns :: [SInteger] -> [SState] -> [SState] -> SBool
- checkMutex :: Int -> IO ()
- notFair :: Int -> IO ()
Documentation
Each agent can be in one of the three states
Instances
_undefiner_State :: a Source #
Autogenerated definition to avoid unused-variable warnings from GHC.
sCaseState :: Mergeable result => SBV State -> result -> result -> result -> result Source #
Case analyzer for the type State.
mutex :: [SState] -> [SState] -> SBool Source #
The mutex property holds for two sequences of state transitions, if they are not in their critical section at the same time.
validTurns :: [SInteger] -> [SState] -> [SState] -> SBool Source #
The mutex algorithm, coded implicitly as an assignment to turns. Turns start at 1, and at each stage is either
1 or 2; giving preference to that process. The only condition is that if either process is in its critical
section, then the turn value stays the same. Note that this is sufficient to satisfy safety (i.e., mutual
exclusion), though it does not guarantee liveness.
checkMutex :: Int -> IO () Source #
Check that we have the mutex property so long as validSequence and validTurns holds; i.e.,
so long as both the agents and the arbiter act according to the rules. The check is bounded up-to-the
given concrete bound; so this is an example of a bounded-model-checking style proof. We have:
>>>checkMutex 20All is good!
notFair :: Int -> IO () Source #
Our algorithm is correct, but it is not fair. It does not guarantee that a process that wants to enter its critical-section will always do so eventually. Demonstrate this by trying to show a bounded trace of length 10, such that the second process is ready but never transitions to critical. We have:
>>>notFair 10Fairness is violated at bound: 10 P1: [Idle,Idle,Ready,Critical,Idle,Ready,Critical,Critical,Idle,Ready] P2: [Idle,Ready,Ready,Ready,Ready,Ready,Ready,Ready,Ready,Ready] Ts: [1,1,1,1,1,1,1,1,1,1]
As expected, P2 gets ready but never goes critical since the arbiter keeps picking P1 unfairly. (You might get a different trace depending on what z3 happens to produce!)
Exercise for the reader: Change the validTurns function so that it alternates the turns
from the previous value if neither process is in critical. Show that this makes the notFair
function below no longer exhibits the issue. Is this sufficient? Concurrent programming is tricky!