Verify Basic property for lock allocation

Verify the minimal consistency property for any form
of lock handling: if a user holds an exclusive lock,
then no other user can hold the same lock (neither
exclusively, nor shared).
Signed-off-by: Klaus Aehlig <aehlig@google.com>
Reviewed-by: Petr Pudlak <pudlak@google.com>

Makefile.am

@@ -147,6 +147,7 @@ HS_DIRS = \
 	test/hs/Test/Ganeti/HTools/Backend \
 	test/hs/Test/Ganeti/Hypervisor \
 	test/hs/Test/Ganeti/Hypervisor/Xen \
+	test/hs/Test/Ganeti/Locking \
 	test/hs/Test/Ganeti/Query \
 	test/hs/Test/Ganeti/THH
 
@@ -809,6 +810,7 @@ HS_TEST_SRCS = \
 	test/hs/Test/Ganeti/JQueue.hs \
 	test/hs/Test/Ganeti/Kvmd.hs \
 	test/hs/Test/Ganeti/Luxi.hs \
+        test/hs/Test/Ganeti/Locking/Allocation.hs \
 	test/hs/Test/Ganeti/Network.hs \
 	test/hs/Test/Ganeti/Objects.hs \
 	test/hs/Test/Ganeti/OpCodes.hs \

test/hs/Test/Ganeti/Locking/Allocation.hs

+{-# LANGUAGE TemplateHaskell #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+
+{-| Tests for lock allocation.
+
+-}
+
+{-
+
+Copyright (C) 2014 Google Inc.
+
+This program is free software; you can redistribute it and/or modify
+it under the terms of the GNU General Public License as published by
+the Free Software Foundation; either version 2 of the License, or
+(at your option) any later version.
+
+This program is distributed in the hope that it will be useful, but
+WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
+General Public License for more details.
+
+You should have received a copy of the GNU General Public License
+along with this program; if not, write to the Free Software
+Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
+02110-1301, USA.
+
+-}
+
+module Test.Ganeti.Locking.Allocation (testLocking_Allocation) where
+
+import Control.Applicative
+import qualified Data.Map as M
+import qualified Data.Set as S
+
+import Test.QuickCheck
+
+import Test.Ganeti.TestHelper
+
+import Ganeti.Locking.Allocation
+
+{-
+
+Ganeti.Locking.Allocation is polymorphic in the types of locks
+and lock owners. So we can use much simpler types here than Ganeti's
+real locks and lock owners, knowning at polymorphic functions cannot
+exploit the simplicity of the types they're deling with.
+
+-}
+
+data TestOwner = TestOwner Int deriving (Ord, Eq, Show)
+
+instance Arbitrary TestOwner where
+  arbitrary = TestOwner <$> choose (0, 7)
+
+data TestLock = TestLock Int deriving (Ord, Eq, Show)
+
+instance Arbitrary TestLock where
+  arbitrary = TestLock <$> choose (0, 7)
+
+
+{-
+
+All states of a  LockAllocation can be obtained by starting from the
+empty allocation, and sequentially requesting (successfully or not)
+lock updates. So we first define what arbitrary updates sequences are.
+
+-}
+
+instance Arbitrary OwnerState where
+  arbitrary = elements [OwnShared, OwnExclusive]
+
+instance Arbitrary a => Arbitrary (LockRequest a) where
+  arbitrary = LockRequest <$> arbitrary <*> genMaybe arbitrary
+
+data UpdateRequest a b = UpdateRequest a [LockRequest b] deriving Show
+
+instance (Arbitrary a, Arbitrary b) => Arbitrary (UpdateRequest a b) where
+  arbitrary = UpdateRequest <$> arbitrary <*> arbitrary
+
+-- | Fold a sequence of update requests; all allocationscan be obtained in
+-- this way, starting from the empty allocation.
+foldUpdates :: (Ord a, Ord b, Show b)
+            => LockAllocation b a -> [UpdateRequest a b] -> LockAllocation b a
+foldUpdates = foldl (\s (UpdateRequest owner updates) ->
+                      fst $ updateLocks owner updates s)
+
+instance (Arbitrary a, Arbitrary b, Ord a, Ord b, Show a, Show b)
+          => Arbitrary (LockAllocation a b) where
+  arbitrary = foldUpdates emptyAllocation <$> arbitrary
+
+-- | Basic property of locking: the exclusive locks of one user
+-- are disjoint from any locks of any other user.
+prop_LocksDisjoint :: Property
+prop_LocksDisjoint =
+  forAll (arbitrary :: Gen (LockAllocation TestLock TestOwner)) $ \state ->
+  forAll (arbitrary :: Gen TestOwner) $ \a ->
+  forAll (arbitrary `suchThat` (/= a)) $ \b ->
+  let aExclusive = M.keysSet . M.filter (== OwnExclusive) $ listLocks  a state
+      bAll = M.keysSet $ listLocks b state
+  in printTestCase
+     (show a ++ "'s exclusive lock" ++ " is not respected by " ++ show b)
+     (S.null $ S.intersection aExclusive bAll)
+
+testSuite "Locking/Allocation"
+ [ 'prop_LocksDisjoint
+ ]

test/hs/htest.hs

@@ -56,6 +56,7 @@ import Test.Ganeti.JSON
 import Test.Ganeti.Jobs
 import Test.Ganeti.JQueue
 import Test.Ganeti.Kvmd
+import Test.Ganeti.Locking.Allocation
 import Test.Ganeti.Luxi
 import Test.Ganeti.Network
 import Test.Ganeti.Objects
@@ -121,6 +122,7 @@ allTests =
   , testJobs
   , testJQueue
   , testKvmd
+  , testLocking_Allocation
   , testLuxi
   , testNetwork
   , testObjects