sbv-14.1: Documentation/SBV/Examples/Lists/BoundedMutex.hs
-----------------------------------------------------------------------------
-- |
-- Module : Documentation.SBV.Examples.Lists.BoundedMutex
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Proves a simple mutex algorithm correct up to a given bound.
-----------------------------------------------------------------------------
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.Lists.BoundedMutex where
import Data.SBV
import Data.SBV.Control
-- | Each agent can be in one of the three states
data State = Idle -- ^ Regular work
| Ready -- ^ Intention to enter critical state
| Critical -- ^ In the critical state
deriving Show
-- | Make 'State' a symbolic enumeration
mkSymbolic [''State]
-- | The mutex property holds for two sequences of state transitions, if they are not in
-- their critical section at the same time.
mutex :: [SState] -> [SState] -> SBool
mutex p1s p2s = sAnd $ zipWith (\p1 p2 -> p1 ./= sCritical .|| p2 ./= sCritical) p1s p2s
-- | 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.
validSequence :: Integer -> [SInteger] -> [SState] -> SBool
validSequence _ [] _ = sTrue
validSequence _ _ [] = sTrue
validSequence me pturns procs@(p:_) = sAnd [ sIdle .== p
, check pturns procs sIdle
]
where check [] _ _ = sTrue
check _ [] _ = sTrue
check (turn:turns) (cur:rest) prev = ok .&& check turns rest cur
where ok = ite (prev .== sIdle) (cur `sElem` [sIdle, sReady])
$ ite (prev .== sReady .&& turn .== literal me) (cur `sElem` [sCritical])
$ ite (prev .== sCritical) (cur `sElem` [sCritical, sIdle])
(cur `sElem` [prev])
-- | 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.
validTurns :: [SInteger] -> [SState] -> [SState] -> SBool
validTurns [] _ _ = sTrue
validTurns turns@(firstTurn : _) process1 process2 = firstTurn .== 1 .&& check (zip3 turns process1 process2) 1
where check [] _ = sTrue
check ((cur, p1, p2) : rest) prev = cur `sElem` map literal [1, 2]
.&& (p1 .== sCritical .|| p2 .== sCritical .=> cur .== prev)
.&& check rest cur
-- | 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!
checkMutex :: Int -> IO ()
checkMutex b = runSMT $ do
p1 :: [SState] <- mapM (\i -> free ("p1_" ++ show i)) [1 .. b]
p2 :: [SState] <- mapM (\i -> free ("p2_" ++ show i)) [1 .. b]
turns :: [SInteger] <- mapM (\i -> free ("t_" ++ show i)) [1 .. b]
-- Ensure that both sequences and the turns are valid
constrain $ validSequence 1 turns p1
constrain $ validSequence 2 turns p2
constrain $ validTurns turns p1 p2
-- Try to assert that mutex does not hold. If we get a
-- counter example, we would've found a violation!
constrain $ sNot $ mutex p1 p2
query $ do cs <- checkSat
case cs of
Unk -> error "Solver said Unknown!"
DSat{} -> error "Solver said delta-satisfiable!"
Unsat -> io . putStrLn $ "All is good!"
Sat -> do io . putStrLn $ "Violation detected!"
do p1V <- mapM getValue p1
p2V <- mapM getValue p2
ts <- mapM getValue turns
io . putStrLn $ "P1: " ++ show p1V
io . putStrLn $ "P2: " ++ show p2V
io . putStrLn $ "Ts: " ++ show ts
-- | 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 10
-- Fairness is violated at bound: 10
-- P1: [Idle,Idle,Idle,Idle,Ready,Critical,Idle,Ready,Critical,Critical]
-- 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!
notFair :: Int -> IO ()
notFair b = runSMT $ do p1 :: [SState] <- mapM (\i -> free ("p1_" ++ show i)) [1 .. b]
p2 :: [SState] <- mapM (\i -> free ("p2_" ++ show i)) [1 .. b]
turns :: [SInteger] <- mapM (\i -> free ("t_" ++ show i)) [1 .. b]
-- Ensure that both sequences and the turns are valid
constrain $ validSequence 1 turns p1
constrain $ validSequence 2 turns p2
constrain $ validTurns turns p1 p2
-- Ensure that the second process becomes ready in the second cycle:
constrain $ p2 !! 1 .== sReady
-- Find a trace where p2 never goes critical
-- counter example, we would've found a violation!
constrain $ sNot $ sCritical `sElem` p2
query $ do cs <- checkSat
case cs of
Unk -> error "Solver said Unknown!"
DSat{} -> error "Solver said delta-satisfiable!"
Unsat -> error "Solver couldn't find a violating trace!"
Sat -> do io . putStrLn $ "Fairness is violated at bound: " ++ show b
do p1V <- mapM getValue p1
p2V <- mapM getValue p2
ts <- mapM getValue turns
io . putStrLn $ "P1: " ++ show p1V
io . putStrLn $ "P2: " ++ show p2V
io . putStrLn $ "Ts: " ++ show ts
{- HLint ignore module "Reduce duplication" -}