Commit f91388c3 authored by Klaus Aehlig's avatar Klaus Aehlig
Browse files

Tests specifying safeUpdateLocksWaiting



Add tests that verify the defining properties of safeUpdateLocksWaiting.

1.) If the state contains no pending request by the requester, then
    updateLocksWaiting and safeUpdateLocksWaiting coincide.

2.) safeUpdateLocksWaiting is idempotent on all states.
Signed-off-by: default avatarKlaus Aehlig <aehlig@google.com>
Reviewed-by: default avatarPetr Pudlak <pudlak@google.com>
parent e01d84a1
......@@ -310,6 +310,46 @@ prop_SimulateUpdateLocksWaiting =
, extRepr finState == extRepr finState'
]
-- | Verify that if a requestor has no pending requests, `safeUpdateWaiting`
-- conincides with `updateLocksWaiting`.
prop_SafeUpdateWaitingCorrect :: Property
prop_SafeUpdateWaitingCorrect =
forAll (arbitrary :: Gen TestOwner) $ \owner ->
forAll ((arbitrary :: Gen (LockWaiting TestLock TestOwner Integer))
`suchThat` (not . hasPendingRequest owner)) $ \state ->
forAll (arbitrary :: Gen Integer) $ \prio ->
forAll (arbitrary :: Gen [LockRequest TestLock]) $ \req ->
let (state', answer') = updateLocksWaiting prio owner req state
(state'', answer'') = safeUpdateLocksWaiting prio owner req state
in conjoin [ printTestCase ("safeUpdateLocksWaiting gave different answer: "
++ show answer' ++ " /= " ++ show answer'')
$ answer' == answer''
, printTestCase ("safeUpdateLocksWaiting gave different states\
\ after answer " ++ show answer' ++ ": "
++ show (extRepr state') ++ " /= "
++ show (extRepr state''))
$ extRepr state' == extRepr state''
]
-- | Verify that `safeUpdateLocksWaiting` is idempotent, that in the repetition
-- no notifications are done.
prop_SafeUpdateWaitingIdempotent :: Property
prop_SafeUpdateWaitingIdempotent =
forAll (arbitrary :: Gen (LockWaiting TestLock TestOwner Integer)) $ \state ->
forAll (arbitrary :: Gen TestOwner) $ \owner ->
forAll (arbitrary :: Gen Integer) $ \prio ->
forAll (arbitrary :: Gen [LockRequest TestLock]) $ \req ->
let (state', (answer', _)) = safeUpdateLocksWaiting prio owner req state
(state'', (answer'', nfy)) = safeUpdateLocksWaiting prio owner req state'
in conjoin [ printTestCase ("repeated safeUpdateLocks waiting gave different\
\ answers: " ++ show answer' ++ " /= "
++ show answer'') $ answer' == answer''
, printTestCase "safeUpdateLocksWaiting not idempotent"
$ extRepr state' == extRepr state''
, printTestCase ("notifications (" ++ show nfy ++ ") on replay")
$ S.null nfy
]
-- | Verify that for LockWaiting we have readJSON . showJSON is extensionally
-- equivalent to Ok.
prop_ReadShow :: Property
......@@ -374,6 +414,8 @@ testSuite "Locking/Waiting"
, 'prop_SimulateUpdateLocks
, 'prop_SimulateUpdateLocksWaiting
, 'prop_ReadShow
, 'prop_SafeUpdateWaitingCorrect
, 'prop_SafeUpdateWaitingIdempotent
, 'prop_OpportunisticMonotone
, 'prop_OpportunisticAnswer
]
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment