Re: [PATCH master 5/6] Verify that opportunistic union only adds to the locks held

[Petr Pudlák]

On Thu, Feb 20, 2014 at 5:02 PM, Klaus Aehlig <aeh...@google.com> wrote:

> Add a test verifying that by opportunistic union the set of locks
> held, and the level at which the locks are held, only increases.
>
> Signed-off-by: Klaus Aehlig <aeh...@google.com>
> ---
>  test/hs/Test/Ganeti/Locking/Allocation.hs | 15 +++++++++++++++
>  1 file changed, 15 insertions(+)
>
> diff --git a/test/hs/Test/Ganeti/Locking/Allocation.hs
> b/test/hs/Test/Ganeti/Locking/Allocation.hs
> index 257d281..0e3ba17 100644
> --- a/test/hs/Test/Ganeti/Locking/Allocation.hs
> +++ b/test/hs/Test/Ganeti/Locking/Allocation.hs
> @@ -257,6 +257,20 @@ prop_BlockNecessary =
>          . F.foldl freeLocks state
>          $ S.filter (/= blocker) blockers
>
> +-- | Verify that opportunistic union only increases the locks held.
> +prop_OpportunisticMonotone :: Property
> +prop_OpportunisticMonotone =
> +  forAll (arbitrary :: Gen (LockAllocation TestLock TestOwner)) $ \state
> ->
> +  forAll (arbitrary :: Gen TestOwner) $ \a ->
> +  forAll ((choose (1,3) >>= vector) :: Gen [(TestLock, OwnerState)]) $
> \req ->
> +  let (state', _) = opportunisticLockUnion a req state
> +      oldOwned = listLocks a state
> +      oldLocks = M.keys oldOwned
> +      newOwned = listLocks a state'
> +  in printTestCase "Opportunistic union may only increase the set of
> locks held"
> +     . flip all oldLocks $ \lock ->
> +       (>=) (M.lookup lock newOwned) (M.lookup lock oldOwned)
>

I'd suggest just

       M.lookup lock newOwned >= M.lookup lock oldOwned



> +
>  testSuite "Locking/Allocation"
>   [ 'prop_LocksDisjoint
>   , 'prop_LockImplicationX
> @@ -266,4 +280,5 @@ testSuite "Locking/Allocation"
>   , 'prop_LockReleaseSucceeds
>   , 'prop_BlockSufficient
>   , 'prop_BlockNecessary
> + , 'prop_OpportunisticMonotone
>   ]
> --
> 1.9.0.rc1.175.g0b1dcb5
>
>
Otherwise LGTM, no need to resend.