Commit 58e173a5 authored by Klaus Aehlig's avatar Klaus Aehlig
Browse files

Verify the answer of opportunistic lock union



Verify that the result set of the opportunistic lock
union is correct.
- If a lock is mentioned in the result set, the request
  must have been granted.
- If it is not mentioned, the owner state must be unchanged.
Signed-off-by: default avatarKlaus Aehlig <aehlig@google.com>
Reviewed-by: default avatarPetr Pudlak <pudlak@google.com>
parent 11a498d5
......@@ -304,6 +304,36 @@ prop_OpportunisticMonotone =
. flip all oldLocks $ \lock ->
M.lookup lock newOwned >= M.lookup lock oldOwned
-- | Verify the result list of the opportunistic union: if a lock is not in
-- the result that, than its state has not changed, and if it is, it is as
-- requested. The latter property is tested in that liberal way, so that we
-- really can take arbitrary requests, including those that require both, shared
-- and exlusive state for the same lock.
prop_OpportunisticAnswer :: Property
prop_OpportunisticAnswer =
forAll (arbitrary :: Gen (LockWaiting TestLock TestOwner Integer)) $ \state ->
forAll (arbitrary :: Gen TestOwner) $ \a ->
forAll ((choose (1,3) >>= vector) :: Gen [(TestLock, L.OwnerState)]) $ \req ->
let (state', (result, _)) = opportunisticLockUnion a req state
oldOwned = listLocks a $ getAllocation state
newOwned = listLocks a $ getAllocation state'
involvedLocks = M.keys oldOwned ++ map fst req
in conjoin [ printTestCase ("Locks not in the answer set " ++ show result
++ " may not be changed, but found "
++ show state')
. flip all involvedLocks $ \lock ->
(lock `elem` result)
|| (M.lookup lock oldOwned == M.lookup lock newOwned)
, printTestCase ("Locks not in the answer set " ++ show result
++ " must be as requested, but found "
++ show state')
. flip all involvedLocks $ \lock ->
notElem lock result
|| maybe False (flip elem req . (,) lock)
(M.lookup lock newOwned)
]
testSuite "Locking/Waiting"
[ 'prop_NoActionWithPendingRequests
, 'prop_WaitingRequestsGetPending
......@@ -317,4 +347,5 @@ testSuite "Locking/Waiting"
, 'prop_SimulateUpdateLocksWaiting
, 'prop_ReadShow
, '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