-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Lists.BoundedMutex
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Demonstrates use of bounded list utilities, proving a simple
-- mutex algorithm correct up to given bounds.
-----------------------------------------------------------------------------

{-# LANGUAGE DeriveAnyClass      #-}
{-# LANGUAGE DeriveDataTypeable  #-}
{-# LANGUAGE OverloadedLists     #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving  #-}
{-# LANGUAGE TemplateHaskell     #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.Lists.BoundedMutex where

import Data.SBV
import Data.SBV.Control

import Data.SBV.List ((.!!))
import qualified Data.SBV.List              as L
import qualified Data.SBV.Tools.BoundedList as L

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

-- | Make 'State' a symbolic enumeration
mkSymbolicEnumeration ''State

-- | The type synonym 'SState' is mnemonic for symbolic state.
type SState = SBV State

-- | Symbolic version of 'Idle'
idle :: SState
idle :: SBV State
idle = State -> SBV State
forall a. SymVal a => a -> SBV a
literal State
Idle

-- | Symbolic version of 'Ready'
ready :: SState
ready :: SBV State
ready = State -> SBV State
forall a. SymVal a => a -> SBV a
literal State
Ready

-- | Symbolic version of 'Critical'
critical :: SState
critical :: SBV State
critical = State -> SBV State
forall a. SymVal a => a -> SBV a
literal State
Critical

-- | 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.
mutex :: Int -> SList State -> SList State -> SBool
mutex :: Int -> SList State -> SList State -> SBool
mutex i :: Int
i p1s :: SList State
p1s p2s :: SList State
p2s = Int -> SList Bool -> SBool
L.band Int
i (SList Bool -> SBool) -> SList Bool -> SBool
forall a b. (a -> b) -> a -> b
$ Int
-> (SBV State -> SBV State -> SBool)
-> SList State
-> SList State
-> SList Bool
forall a b c.
(SymVal a, SymVal b, SymVal c) =>
Int -> (SBV a -> SBV b -> SBV c) -> SList a -> SList b -> SList c
L.bzipWith Int
i (\p1 :: SBV State
p1 p2 :: SBV State
p2 -> SBV State
p1 SBV State -> SBV State -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SBV State
critical SBool -> SBool -> SBool
.|| SBV State
p2 SBV State -> SBV State -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SBV State
critical) SList State
p1s SList State
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 :: Int -> Integer -> SList Integer -> SList State -> SBool
validSequence :: Int -> Integer -> SList Integer -> SList State -> SBool
validSequence b :: Int
b me :: Integer
me pturns :: SList Integer
pturns proc :: SList State
proc = [SBool] -> SBool
sAnd [ SList State -> SInteger
forall a. SymVal a => SList a -> SInteger
L.length SList State
proc SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Int -> SInteger
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
b
                                      , SBV State
idle SBV State -> SBV State -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList State -> SBV State
forall a. SymVal a => SList a -> SBV a
L.head SList State
proc
                                      , Int -> SList Integer -> SList State -> SBV State -> SBool
forall t.
(Eq t, Num t) =>
t -> SList Integer -> SList State -> SBV State -> SBool
check Int
b SList Integer
pturns SList State
proc SBV State
idle
                                      ]
   where check :: t -> SList Integer -> SList State -> SBV State -> SBool
check 0 _  _  _    = SBool
sTrue
         check i :: t
i ts :: SList Integer
ts ps :: SList State
ps prev :: SBV State
prev = let (cur :: SBV State
cur,  rest :: SList State
rest)  = SList State -> (SBV State, SList State)
forall a. SymVal a => SList a -> (SBV a, SList a)
L.uncons SList State
ps
                                  (turn :: SInteger
turn, turns :: SList Integer
turns) = SList Integer -> (SInteger, SList Integer)
forall a. SymVal a => SList a -> (SBV a, SList a)
L.uncons SList Integer
ts
                                  ok :: SBool
ok   = SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV State
prev SBV State -> SBV State -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV State
idle)                          (SBV State
cur SBV State -> [SBV State] -> SBool
forall a. EqSymbolic a => a -> [a] -> SBool
`sElem` [Item [SBV State]
SBV State
idle, Item [SBV State]
SBV State
ready])
                                       (SBool -> SBool) -> SBool -> SBool
forall a b. (a -> b) -> a -> b
$ SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV State
prev SBV State -> SBV State -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV State
ready SBool -> SBool -> SBool
.&& SInteger
turn SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Integer -> SInteger
forall a. SymVal a => a -> SBV a
literal Integer
me) (SBV State
cur SBV State -> [SBV State] -> SBool
forall a. EqSymbolic a => a -> [a] -> SBool
`sElem` [Item [SBV State]
SBV State
critical])
                                       (SBool -> SBool) -> SBool -> SBool
forall a b. (a -> b) -> a -> b
$ SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV State
prev SBV State -> SBV State -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV State
critical)                      (SBV State
cur SBV State -> [SBV State] -> SBool
forall a. EqSymbolic a => a -> [a] -> SBool
`sElem` [Item [SBV State]
SBV State
critical, Item [SBV State]
SBV State
idle])
                                                                                      (SBV State
cur SBV State -> [SBV State] -> SBool
forall a. EqSymbolic a => a -> [a] -> SBool
`sElem` [Item [SBV State]
SBV State
prev])
                              in SBool
ok SBool -> SBool -> SBool
.&& t -> SList Integer -> SList State -> SBV State -> SBool
check (t
it -> t -> t
forall a. Num a => a -> a -> a
-1) SList Integer
turns SList State
rest SBV State
cur

-- | 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.
validTurns :: Int -> SList Integer -> SList State -> SList State -> SBool
validTurns :: Int -> SList Integer -> SList State -> SList State -> SBool
validTurns b :: Int
b turns :: SList Integer
turns process1 :: SList State
process1 process2 :: SList State
process2 = [SBool] -> SBool
sAnd [ SList Integer -> SInteger
forall a. SymVal a => SList a -> SInteger
L.length SList Integer
turns SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Int -> SInteger
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
b
                                            , 1 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList Integer -> SInteger
forall a. SymVal a => SList a -> SBV a
L.head SList Integer
turns
                                            , Int
-> SList Integer -> SList State -> SList State -> SInteger -> SBool
forall a t.
(Ord a, Num t, Num a, Eq t, SymVal a) =>
t -> SList a -> SList State -> SList State -> SBV a -> SBool
check Int
b SList Integer
turns SList State
process1 SList State
process2 1
                                            ]
   where check :: t -> SList a -> SList State -> SList State -> SBV a -> SBool
check 0 _  _     _     _    = SBool
sTrue
         check i :: t
i ts :: SList a
ts proc1 :: SList State
proc1 proc2 :: SList State
proc2 prev :: SBV a
prev =   SBV a
cur SBV a -> [SBV a] -> SBool
forall a. EqSymbolic a => a -> [a] -> SBool
`sElem` [1, 2]
                                     SBool -> SBool -> SBool
.&& (SBV State
p1 SBV State -> SBV State -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV State
critical SBool -> SBool -> SBool
.|| SBV State
p2 SBV State -> SBV State -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV State
critical SBool -> SBool -> SBool
.=> SBV a
cur SBV a -> SBV a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV a
prev)
                                     SBool -> SBool -> SBool
.&& t -> SList a -> SList State -> SList State -> SBV a -> SBool
check (t
it -> t -> t
forall a. Num a => a -> a -> a
-1) SList a
rest SList State
p1s SList State
p2s SBV a
cur
            where (cur :: SBV a
cur, rest :: SList a
rest) = SList a -> (SBV a, SList a)
forall a. SymVal a => SList a -> (SBV a, SList a)
L.uncons SList a
ts
                  (p1 :: SBV State
p1,  p1s :: SList State
p1s)  = SList State -> (SBV State, SList State)
forall a. SymVal a => SList a -> (SBV a, SList a)
L.uncons SList State
proc1
                  (p2 :: SBV State
p2,  p2s :: SList State
p2s)  = SList State -> (SBV State, SList State)
forall a. SymVal a => SList a -> (SBV a, SList a)
L.uncons SList State
proc2

-- | 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 :: Int -> IO ()
checkMutex b :: Int
b = Symbolic () -> IO ()
forall a. Symbolic a -> IO a
runSMT (Symbolic () -> IO ()) -> Symbolic () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
                  SList State
p1    :: SList State   <- String -> Symbolic (SList State)
forall a. SymVal a => String -> Symbolic (SList a)
sList "p1"
                  SList State
p2    :: SList State   <- String -> Symbolic (SList State)
forall a. SymVal a => String -> Symbolic (SList a)
sList "p2"
                  SList Integer
turns :: SList Integer <- String -> Symbolic (SList Integer)
forall a. SymVal a => String -> Symbolic (SList a)
sList "turns"

                  -- Ensure that both sequences and the turns are valid
                  SBool -> Symbolic ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ Int -> Integer -> SList Integer -> SList State -> SBool
validSequence Int
b 1 SList Integer
turns SList State
p1
                  SBool -> Symbolic ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ Int -> Integer -> SList Integer -> SList State -> SBool
validSequence Int
b 2 SList Integer
turns SList State
p2
                  SBool -> Symbolic ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ Int -> SList Integer -> SList State -> SList State -> SBool
validTurns    Int
b SList Integer
turns SList State
p1 SList State
p2

                  -- Try to assert that mutex does not hold. If we get a
                  -- counter example, we would've found a violation!
                  SBool -> Symbolic ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot (SBool -> SBool) -> SBool -> SBool
forall a b. (a -> b) -> a -> b
$ Int -> SList State -> SList State -> SBool
mutex Int
b SList State
p1 SList State
p2

                  Query () -> Symbolic ()
forall a. Query a -> Symbolic a
query (Query () -> Symbolic ()) -> Query () -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ do CheckSatResult
cs <- Query CheckSatResult
checkSat
                             case CheckSatResult
cs of
                               Unk   -> String -> Query ()
forall a. HasCallStack => String -> a
error "Solver said Unknown!"
                               Unsat -> IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> (String -> IO ()) -> String -> Query ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> Query ()) -> String -> Query ()
forall a b. (a -> b) -> a -> b
$ "All is good!"
                               Sat   -> do IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> (String -> IO ()) -> String -> Query ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> Query ()) -> String -> Query ()
forall a b. (a -> b) -> a -> b
$ "Violation detected!"
                                           do [State]
p1V <- SList State -> Query [State]
forall a. SymVal a => SBV a -> Query a
getValue SList State
p1
                                              [State]
p2V <- SList State -> Query [State]
forall a. SymVal a => SBV a -> Query a
getValue SList State
p2
                                              [Integer]
ts  <- SList Integer -> Query [Integer]
forall a. SymVal a => SBV a -> Query a
getValue SList Integer
turns

                                              IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> (String -> IO ()) -> String -> Query ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> Query ()) -> String -> Query ()
forall a b. (a -> b) -> a -> b
$ "P1: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [State] -> String
forall a. Show a => a -> String
show [State]
p1V
                                              IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> (String -> IO ()) -> String -> Query ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> Query ()) -> String -> Query ()
forall a b. (a -> b) -> a -> b
$ "P2: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [State] -> String
forall a. Show a => a -> String
show [State]
p2V
                                              IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> (String -> IO ()) -> String -> Query ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> Query ()) -> String -> Query ()
forall a b. (a -> b) -> a -> b
$ "Ts: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Integer] -> String
forall a. Show a => a -> String
show [Integer]
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:
--
-- > 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!
notFair :: Int -> IO ()
notFair :: Int -> IO ()
notFair b :: Int
b = Symbolic () -> IO ()
forall a. Symbolic a -> IO a
runSMT (Symbolic () -> IO ()) -> Symbolic () -> IO ()
forall a b. (a -> b) -> a -> b
$ do SList State
p1    :: SList State   <- String -> Symbolic (SList State)
forall a. SymVal a => String -> Symbolic (SList a)
sList "p1"
                        SList State
p2    :: SList State   <- String -> Symbolic (SList State)
forall a. SymVal a => String -> Symbolic (SList a)
sList "p2"
                        SList Integer
turns :: SList Integer <- String -> Symbolic (SList Integer)
forall a. SymVal a => String -> Symbolic (SList a)
sList "turns"

                        -- Ensure that both sequences and the turns are valid
                        SBool -> Symbolic ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ Int -> Integer -> SList Integer -> SList State -> SBool
validSequence Int
b 1 SList Integer
turns SList State
p1
                        SBool -> Symbolic ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ Int -> Integer -> SList Integer -> SList State -> SBool
validSequence Int
b 2 SList Integer
turns SList State
p2
                        SBool -> Symbolic ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ Int -> SList Integer -> SList State -> SList State -> SBool
validTurns    Int
b SList Integer
turns SList State
p1 SList State
p2

                        -- Ensure that the second process becomes ready in the second cycle:
                        SBool -> Symbolic ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ SList State
p2 SList State -> SInteger -> SBV State
forall a. SymVal a => SList a -> SInteger -> SBV a
.!! 1 SBV State -> SBV State -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV State
ready

                        -- Find a trace where p2 never goes critical
                        -- counter example, we would've found a violation!
                        SBool -> Symbolic ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> Symbolic ()) -> SBool -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot (SBool -> SBool) -> SBool -> SBool
forall a b. (a -> b) -> a -> b
$ Int -> SBV State -> SList State -> SBool
forall a. (Eq a, SymVal a) => Int -> SBV a -> SList a -> SBool
L.belem Int
b SBV State
critical SList State
p2

                        Query () -> Symbolic ()
forall a. Query a -> Symbolic a
query (Query () -> Symbolic ()) -> Query () -> Symbolic ()
forall a b. (a -> b) -> a -> b
$ do CheckSatResult
cs <- Query CheckSatResult
checkSat
                                   case CheckSatResult
cs of
                                     Unk   -> String -> Query ()
forall a. HasCallStack => String -> a
error "Solver said Unknown!"
                                     Unsat -> String -> Query ()
forall a. HasCallStack => String -> a
error "Solver couldn't find a violating trace!"
                                     Sat   -> do IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> (String -> IO ()) -> String -> Query ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> Query ()) -> String -> Query ()
forall a b. (a -> b) -> a -> b
$ "Fairness is violated at bound: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
b
                                                 do [State]
p1V <- SList State -> Query [State]
forall a. SymVal a => SBV a -> Query a
getValue SList State
p1
                                                    [State]
p2V <- SList State -> Query [State]
forall a. SymVal a => SBV a -> Query a
getValue SList State
p2
                                                    [Integer]
ts  <- SList Integer -> Query [Integer]
forall a. SymVal a => SBV a -> Query a
getValue SList Integer
turns

                                                    IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> (String -> IO ()) -> String -> Query ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> Query ()) -> String -> Query ()
forall a b. (a -> b) -> a -> b
$ "P1: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [State] -> String
forall a. Show a => a -> String
show [State]
p1V
                                                    IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> (String -> IO ()) -> String -> Query ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> Query ()) -> String -> Query ()
forall a b. (a -> b) -> a -> b
$ "P2: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [State] -> String
forall a. Show a => a -> String
show [State]
p2V
                                                    IO () -> Query ()
forall a. IO a -> Query a
io (IO () -> Query ()) -> (String -> IO ()) -> String -> Query ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> Query ()) -> String -> Query ()
forall a b. (a -> b) -> a -> b
$ "Ts: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Integer] -> String
forall a. Show a => a -> String
show [Integer]
ts

{-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}