Documentation.SBV.Examples.Lists.BoundedMutex

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

Documentation

data State

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

Data State

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

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

toConstr :: State -> Constr

dataTypeOf :: State -> DataType

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

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

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

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

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

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

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

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

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

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

Read State

Defined in Documentation.SBV.Examples.Lists.BoundedMutex

Methods

readsPrec :: Int -> ReadS State

readList :: ReadS [State]

readPrec :: ReadPrec State

readListPrec :: ReadPrec [State]

Show State

Defined in Documentation.SBV.Examples.Lists.BoundedMutex

Methods

showsPrec :: Int -> State -> ShowS

show :: State -> String

showList :: [State] -> ShowS

Eq State

Defined in Documentation.SBV.Examples.Lists.BoundedMutex

Methods

(==) :: State -> State -> Bool

(/=) :: State -> State -> Bool

Ord State

Defined in Documentation.SBV.Examples.Lists.BoundedMutex

Methods

compare :: State -> State -> Ordering

(<) :: State -> State -> Bool

(<=) :: State -> State -> Bool

(>) :: State -> State -> Bool

(>=) :: State -> State -> Bool

max :: State -> State -> State

min :: State -> State -> State

SymVal State

Defined in Documentation.SBV.Examples.Lists.BoundedMutex

Methods

mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV State)

literal :: State -> SBV State

fromCV :: CV -> State

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

sbvForall :: MonadSymbolic m => String -> m (SBV State)

sbvForall_ :: MonadSymbolic m => m (SBV State)

mkForallVars :: MonadSymbolic m => Int -> m [SBV State]

sbvExists :: MonadSymbolic m => String -> m (SBV State)

sbvExists_ :: MonadSymbolic m => m (SBV State)

mkExistVars :: MonadSymbolic m => Int -> m [SBV State]

free :: MonadSymbolic m => String -> m (SBV State)

free_ :: MonadSymbolic m => m (SBV State)

mkFreeVars :: MonadSymbolic m => Int -> m [SBV State]

symbolic :: MonadSymbolic m => String -> m (SBV State)

symbolics :: MonadSymbolic m => [String] -> m [SBV State]

unliteral :: SBV State -> Maybe State

isConcrete :: SBV State -> Bool

isSymbolic :: SBV State -> Bool

HasKind State

Defined in Documentation.SBV.Examples.Lists.BoundedMutex

Methods

kindOf :: State -> Kind

hasSign :: State -> Bool

intSizeOf :: State -> Int

isBoolean :: State -> Bool

isBounded :: State -> Bool

isReal :: State -> Bool

isFloat :: State -> Bool

isDouble :: State -> Bool

isRational :: State -> Bool

isFP :: State -> Bool

isUnbounded :: State -> Bool

isUserSort :: State -> Bool

isChar :: State -> Bool

isString :: State -> Bool

isList :: State -> Bool

isSet :: State -> Bool

isTuple :: State -> Bool

isMaybe :: State -> Bool

isEither :: State -> Bool

showType :: State -> String

SatModel State

Defined in Documentation.SBV.Examples.Lists.BoundedMutex

Methods

parseCVs :: [CV] -> Maybe (State, [CV])

cvtModel :: (State -> Maybe b) -> Maybe (State, [CV]) -> Maybe (b, [CV])

type SState = SBV State

Symbolic version of the type State.

sCritical :: SBV State

Symbolic version of the constructor Critical.

sReady :: SBV State

Symbolic version of the constructor Ready.

sIdle :: SBV State

Symbolic version of the constructor Idle.

mutex :: Int -> SList State -> SList State -> SBool

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

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

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 ()

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 ()

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!