sbv-7.13: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | None
Language | Haskell2010

Documentation.SBV.Examples.Lists.BoundedMutex

Description

Demonstrates use of bounded list utilities, proving a simple mutex algorithm correct up to given bounds.

Synopsis

- data State
  - = Idle
  - | Ready
  - | Critical
- 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 ()
- notFair :: Int -> IO ()

# Documentation

data State Source #

Each agent can be in one of the three states

Constructors

Idle | Regular work
Ready | Intention to enter critical state
Critical | In the critical state

Instances

Eq State Source # |
Instance details Defined in Documentation.SBV.Examples.Lists.BoundedMutex Methods (==) :: State -> State -> Bool Source # (/=) :: State -> State -> Bool Source #
Data State Source # |

Instance details

Defined in Documentation.SBV.Examples.Lists.BoundedMutex

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> State -> c State Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c State Source #

toConstr :: State -> Constr Source #

dataTypeOf :: State -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c State) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c State) Source #

gmapT :: (forall b. Data b => b -> b) -> State -> State Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> State -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> State -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> State -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> State -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> State -> m State Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> State -> m State Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> State -> m State Source #

Ord State Source # |
Instance details Defined in Documentation.SBV.Examples.Lists.BoundedMutex Methods compare :: State -> State -> Ordering Source # (<) :: State -> State -> Bool Source # (<=) :: State -> State -> Bool Source # (>) :: State -> State -> Bool Source # (>=) :: State -> State -> Bool Source # max :: State -> State -> State Source # min :: State -> State -> State Source #
Read State Source # |
Instance details Defined in Documentation.SBV.Examples.Lists.BoundedMutex Methods readsPrec :: Int -> ReadS State Source # readList :: ReadS [State] Source # readPrec :: ReadPrec State Source # readListPrec :: ReadPrec [State] Source #
Show State Source # |
Instance details Defined in Documentation.SBV.Examples.Lists.BoundedMutex Methods showsPrec :: Int -> State -> ShowS Source # show :: State -> String Source # showList :: [State] -> ShowS Source #
HasKind State Source # |

Instance details

Defined in Documentation.SBV.Examples.Lists.BoundedMutex

Methods

kindOf :: State -> Kind Source #

hasSign :: State -> Bool Source #

intSizeOf :: State -> Int Source #

isBoolean :: State -> Bool Source #

isBounded :: State -> Bool Source #

isReal :: State -> Bool Source #

isFloat :: State -> Bool Source #

isDouble :: State -> Bool Source #

isInteger :: State -> Bool Source #

isUninterpreted :: State -> Bool Source #

isChar :: State -> Bool Source #

isString :: State -> Bool Source #

isList :: State -> Bool Source #

showType :: State -> String Source #

SymWord State Source # |

Instance details

Defined in Documentation.SBV.Examples.Lists.BoundedMutex

Methods

forall :: String -> Symbolic (SBV State) Source #

forall_ :: Symbolic (SBV State) Source #

mkForallVars :: Int -> Symbolic [SBV State] Source #

exists :: String -> Symbolic (SBV State) Source #

exists_ :: Symbolic (SBV State) Source #

mkExistVars :: Int -> Symbolic [SBV State] Source #

free :: String -> Symbolic (SBV State) Source #

free_ :: Symbolic (SBV State) Source #

mkFreeVars :: Int -> Symbolic [SBV State] Source #

symbolic :: String -> Symbolic (SBV State) Source #

symbolics :: [String] -> Symbolic [SBV State] Source #

literal :: State -> SBV State Source #

unliteral :: SBV State -> Maybe State Source #

fromCW :: CW -> State Source #

isConcrete :: SBV State -> Bool Source #

isSymbolic :: SBV State -> Bool Source #

isConcretely :: SBV State -> (State -> Bool) -> Bool Source #

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV State) Source #

SatModel State Source # | Make `State` a symbolic enumeration
Instance details Defined in Documentation.SBV.Examples.Lists.BoundedMutex Methods parseCWs :: [CW] -> Maybe (State, [CW]) Source # cvtModel :: (State -> Maybe b) -> Maybe (State, [CW]) -> Maybe (b, [CW]) Source #
SMTValue State Source # |
Instance details Defined in Documentation.SBV.Examples.Lists.BoundedMutex Methods sexprToVal :: SExpr -> Maybe State Source #

type SState = SBV State Source #

The type synonym `SState` is mnemonic for symbolic state.

idle :: SState Source #

Symbolic version of `Idle`

ready :: SState Source #

Symbolic version of `Ready`

critical :: SState Source #

Symbolic version of `Critical`

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.

validSequence :: Int -> Integer -> SList Integer -> SList State -> SBool Source #

A sequence is valid upto a bound if it starts at `Idle`, and follows the mutex rules. That is:

- From `Idle` it can switch to `Ready` or stay `Idle`
- From `Ready` it can switch to `Critical` if it's its turn
- From `Critical` it can either stay in `Critical` or go back to `Idle`

The variable `me` identifies the agent id.

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!

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:

    ghci> notFair 10
    Fairness is violated at bound: 10
    P1: [Idle,Idle,Ready,Critical,Idle,Idle,Ready,Critical,Idle,Idle]
    P2: [Idle,Ready,Ready,Ready,Ready,Ready,Ready,Ready,Ready,Ready]
    Ts: [1,2,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!