Copyright | (c) Levent Erkok |
---|---|
License | BSD3 |
Maintainer | erkokl@gmail.com |
Stability | experimental |
Safe Haskell | None |
Language | Haskell2010 |
Demonstrates use of bounded list utilities, proving a simple mutex algorithm correct up to given bounds.
Synopsis
- data State
- type SState = SBV State
- idle :: SState
- ready :: SState
- critical :: SState
- mutex :: Int -> SList State -> SList State -> SBool
- validSequence :: Int -> Integer -> SList Integer -> SList State -> SBool
- validTurns :: Int -> SList Integer -> SList State -> SList State -> SBool
- checkMutex :: Int -> IO ()
Documentation
Each agent can be in one of the three states
Instances
mutex :: Int -> SList State -> SList State -> SBool Source #
A bounded mutex property holds for two sequences of state transitions, if they are not in their critical section at the same time up to that given bound.
validTurns :: Int -> SList Integer -> SList State -> SList State -> SBool Source #
The mutex algorithm, coded implicity 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 20
All is good!