diff --git a/crdt.cabal b/crdt.cabal --- a/crdt.cabal +++ b/crdt.cabal @@ -1,9 +1,11 @@ --- This file has been generated from package.yaml by hpack version 0.17.1. +-- This file has been generated from package.yaml by hpack version 0.20.0. -- -- see: https://github.com/sol/hpack +-- +-- hash: db0538f8b628af11f30af67edf7178b1305f42a56a99e2fa5e60a6c941a47ce8 name: crdt -version: 4.0 +version: 4.1 synopsis: Conflict-free replicated data types description: Definitions of CmRDT and CvRDT. Implementations for some classic CRDTs. category: Distributed Systems @@ -24,9 +26,14 @@ hs-source-dirs: lib build-depends: - base >= 4.9 && < 4.11 + base >=4.9 && <4.11 + , binary + , bytestring , containers , mtl + , network-info + , safe + , time exposed-modules: CRDT.Cm CRDT.Cm.Counter @@ -43,6 +50,8 @@ CRDT.LamportClock CRDT.LWW Data.Semilattice + other-modules: + Paths_crdt default-language: Haskell2010 test-suite test @@ -51,14 +60,14 @@ hs-source-dirs: test build-depends: - base >= 4.9 && < 4.11 + QuickCheck + , base >=4.9 && <4.11 , containers - , mtl - , QuickCheck + , crdt + , quickcheck-instances , tasty - , tasty-discover >= 4.1 + , tasty-discover >=4.1 , tasty-quickcheck - , crdt other-modules: ArbitraryOrphans Cm.TwoPSet @@ -72,5 +81,5 @@ Max ORSet PNCounter - QCUtil + Paths_crdt default-language: Haskell2010 diff --git a/lib/CRDT/Cm.hs b/lib/CRDT/Cm.hs --- a/lib/CRDT/Cm.hs +++ b/lib/CRDT/Cm.hs @@ -70,6 +70,9 @@ :: Intent op ~ op => Intent op -> Payload op -> Maybe (Process op) makeOp i _ = Just $ pure i - -- | Apply an update to the payload. + -- | Apply an update to the payload (downstream). -- An invalid update must be ignored. + -- + -- TODO(Syrovetsky, 2017-12-05) There is no downstream precondition yet. + -- We must make a test for it first. apply :: op -> Payload op -> Payload op diff --git a/lib/CRDT/LamportClock.hs b/lib/CRDT/LamportClock.hs --- a/lib/CRDT/LamportClock.hs +++ b/lib/CRDT/LamportClock.hs @@ -4,6 +4,7 @@ ( Pid (..) -- * Lamport timestamp (for a single process) , LamportTime (..) + , getRealLamportTime , getTime , advance -- * Lamport clock (for a whole multi-process system) @@ -18,22 +19,33 @@ import Control.Monad.Reader (ReaderT, ask, runReaderT) import Control.Monad.State.Strict (State, evalState, modify, state) import Control.Monad.Trans (lift) -import Data.IntMap.Strict (IntMap) -import qualified Data.IntMap.Strict as IntMap +import Data.Binary (decode) +import qualified Data.ByteString.Lazy as BSL +import Data.Map.Strict (Map) +import qualified Data.Map.Strict as Map import Data.Maybe (fromMaybe) +import Data.Time (getCurrentTime) +import Data.Time.Clock.POSIX (utcTimeToPOSIXSeconds) +import Data.Word (Word64) +import Network.Info (MAC (MAC), getNetworkInterfaces, mac) +import Numeric (showHex) import Numeric.Natural (Natural) +import Safe (headDef) type LocalTime = Natural data LamportTime = LamportTime !LocalTime !Pid - deriving (Eq, Ord, Show) + deriving (Eq, Ord) +instance Show LamportTime where + show (LamportTime time (Pid pid)) = showHex time "" ++ '-' : showHex pid "" + -- | Unique process identifier -newtype Pid = Pid Int +newtype Pid = Pid Word64 deriving (Eq, Ord, Show) -- | Key is 'Pid'. Non-present value is equivalent to 0. -newtype LamportClock a = LamportClock (State (IntMap LocalTime) a) +newtype LamportClock a = LamportClock (State (Map Pid LocalTime) a) deriving (Applicative, Functor, Monad) newtype Process a = Process (ReaderT Pid LamportClock a) @@ -55,12 +67,32 @@ runProcess pid (Process action) = runReaderT action pid preIncrementAt :: Pid -> LamportClock LocalTime -preIncrementAt (Pid pid) = +preIncrementAt pid = LamportClock . state $ \m -> let - lt' = succ . fromMaybe 0 $ IntMap.lookup pid m - in (lt', IntMap.insert pid lt' m) + lt' = succ . fromMaybe 0 $ Map.lookup pid m + in (lt', Map.insert pid lt' m) advance :: LamportTime -> Process () advance (LamportTime time _) = Process $ do - Pid pid <- ask - lift . LamportClock . modify $ IntMap.insertWith max pid time + pid <- ask + lift . LamportClock . modify $ Map.insertWith max pid time + +getRealLocalTime :: IO LocalTime +getRealLocalTime = round . utcTimeToPOSIXSeconds <$> getCurrentTime + +-- TODO(cblp, 2018-01-05) monotonic +getRealLamportTime :: IO LamportTime +getRealLamportTime = + LamportTime <$> getRealLocalTime <*> (Pid . decodeMac <$> getMac) + where + + getMac :: IO MAC + getMac = + headDef (error "Can't get any non-zero MAC address of this machine") + . filter (/= minBound) + . map mac + <$> getNetworkInterfaces + + decodeMac :: MAC -> Word64 + decodeMac (MAC b5 b4 b3 b2 b1 b0) = + decode $ BSL.pack [0, 0, b5, b4, b3, b2, b1, b0] diff --git a/test/ArbitraryOrphans.hs b/test/ArbitraryOrphans.hs --- a/test/ArbitraryOrphans.hs +++ b/test/ArbitraryOrphans.hs @@ -1,21 +1,23 @@ {-# OPTIONS_GHC -Wno-orphans #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE StandaloneDeriving #-} module ArbitraryOrphans () where import Test.QuickCheck (Arbitrary (..), arbitraryBoundedEnum, elements) +import Test.QuickCheck.Gen (Gen (MkGen)) +import Test.QuickCheck.Instances () +import Test.QuickCheck.Random (mkQCGen) import CRDT.Cm.Counter (Counter (..)) import CRDT.Cm.GSet (GSet (..)) -import CRDT.Cm.TwoPSet (TwoPSet (..)) -import qualified CRDT.Cm.TwoPSet as TwoPSet -import CRDT.Cv.ORSet (ORSet (..)) +import qualified CRDT.Cm.TwoPSet as Cm import CRDT.Cv.GCounter (GCounter (..)) import CRDT.Cv.LwwElementSet (LwwElementSet (..)) -import CRDT.Cv.Max (Max (..)) +import CRDT.Cv.ORSet (ORSet (..)) import CRDT.Cv.PNCounter (PNCounter (..)) import qualified CRDT.Cv.TwoPSet as Cv import CRDT.LamportClock (LamportTime (..), Pid (..)) @@ -25,12 +27,17 @@ arbitrary = arbitraryBoundedEnum instance Arbitrary a => Arbitrary (LWW a) where - arbitrary = LWW <$> arbitrary <*> arbitrary + arbitrary = do + time <- arbitrary + value <- seeded (hash time) arbitrary + pure LWW{value, time} + where + hash (LamportTime t (Pid p)) = fromIntegral t * 997 + fromIntegral p deriving instance Arbitrary a => Arbitrary (GSet a) -instance Arbitrary a => Arbitrary (TwoPSet a) where - arbitrary = elements [TwoPSet.Add, Remove] <*> arbitrary +instance Arbitrary a => Arbitrary (Cm.TwoPSet a) where + arbitrary = elements [Cm.Add, Cm.Remove] <*> arbitrary deriving instance Arbitrary a => Arbitrary (GCounter a) @@ -38,8 +45,6 @@ deriving instance (Arbitrary a, Ord a) => Arbitrary (LwwElementSet a) -deriving instance Arbitrary a => Arbitrary (Max a) - instance Arbitrary a => Arbitrary (PNCounter a) where arbitrary = PNCounter <$> arbitrary <*> arbitrary @@ -49,3 +54,7 @@ arbitrary = LamportTime <$> arbitrary <*> arbitrary deriving instance Arbitrary Pid + +-- | Generate deterministically +seeded :: Int -> Gen a -> Gen a +seeded s (MkGen g) = MkGen $ \_ n -> g (mkQCGen s) n diff --git a/test/Cv/TwoPSet.hs b/test/Cv/TwoPSet.hs --- a/test/Cv/TwoPSet.hs +++ b/test/Cv/TwoPSet.hs @@ -24,4 +24,4 @@ prop_add_then_remove (s :: TwoPSet Char) x = not . lookup x . remove x $ add x s -test_Cv = cvrdtLaws @(TwoPSet Char) Nothing +test_Cv = cvrdtLaws @(TwoPSet Char) diff --git a/test/GCounter.hs b/test/GCounter.hs --- a/test/GCounter.hs +++ b/test/GCounter.hs @@ -11,7 +11,7 @@ import Laws (cvrdtLaws) -test_Cv = cvrdtLaws @(GCounter Int) Nothing +test_Cv = cvrdtLaws @(GCounter Int) prop_increment (counter :: GCounter Int) pid = query (increment pid counter) === succ (query counter) diff --git a/test/GSet.hs b/test/GSet.hs --- a/test/GSet.hs +++ b/test/GSet.hs @@ -12,6 +12,6 @@ prop_Cm = cmrdtLaw @(Cm.GSet Char) -test_Cv = cvrdtLaws @(Cv.GSet Char) Nothing +test_Cv = cvrdtLaws @(Cv.GSet Char) prop_add (x :: Char) = Cv.lookup x . Cv.add x diff --git a/test/LWW.hs b/test/LWW.hs --- a/test/LWW.hs +++ b/test/LWW.hs @@ -5,28 +5,23 @@ {-# LANGUAGE TypeApplications #-} module LWW - ( genUniquelyTimedLWW - , prop_Cm + ( prop_Cm , prop_assign , prop_merge_with_former , test_Cv ) where -import Control.Monad.State.Strict (StateT, lift) import Data.Semigroup ((<>)) -import Data.Set (Set) -import qualified Data.Set as Set -import Test.QuickCheck (Arbitrary, Gen, arbitrary, (===)) +import Test.QuickCheck ((===)) -import CRDT.LamportClock (LamportTime, runLamportClock, runProcess) -import CRDT.LWW (LWW (LWW), assign, initial, query) +import CRDT.LamportClock (runLamportClock, runProcess) +import CRDT.LWW (LWW, assign, initial, query) import Laws (cmrdtLaw, cvrdtLaws) -import QCUtil (genUnique) prop_Cm = cmrdtLaw @(LWW Char) -test_Cv = cvrdtLaws @(LWW Char) $ Just (genUniquelyTimedLWW, Set.empty) +test_Cv = cvrdtLaws @(LWW Char) prop_assign pid1 pid2 (formerValue :: Char) latterValue = runLamportClock $ do state1 <- runProcess pid1 $ initial formerValue @@ -38,7 +33,3 @@ state1 <- runProcess pid1 $ initial formerValue state2 <- runProcess pid2 $ assign latterValue state1 pure $ query (state1 <> state2) === latterValue - --- | Generate specified number of 'LWW' with unique timestamps -genUniquelyTimedLWW :: Arbitrary a => StateT (Set LamportTime) Gen (LWW a) -genUniquelyTimedLWW = LWW <$> lift arbitrary <*> genUnique diff --git a/test/Laws.hs b/test/Laws.hs --- a/test/Laws.hs +++ b/test/Laws.hs @@ -1,87 +1,101 @@ {-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE LambdaCase #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} module Laws ( cmrdtLaw , cvrdtLaws ) where -import Control.Monad.State.Strict (StateT, evalStateT) -import Data.Maybe (fromMaybe) +import Data.Maybe (fromMaybe, isJust) import Data.Semigroup (Semigroup, (<>)) -import Test.QuickCheck (Arbitrary (..), Gen, Property, discard, - forAll, property, (===), (==>)) +import Test.QuickCheck (Arbitrary (..), Property, counterexample, + discard, property, (.&&.), (===), (==>)) import Test.Tasty (TestTree) import Test.Tasty.QuickCheck (testProperty) import CRDT.Cm (CmRDT (..), concurrent) +import CRDT.Cm.Counter (Counter) +import CRDT.Cm.GSet (GSet) +import CRDT.Cm.TwoPSet (TwoPSet) import CRDT.Cv (CvRDT) -import CRDT.LamportClock (runLamportClock, runProcess) +import CRDT.LamportClock (Process, runLamportClock, runProcess) +import CRDT.LWW (LWW) +import qualified CRDT.LWW as LWW import Data.Semilattice (Semilattice, merge) import ArbitraryOrphans () -gen2 :: (StateT s Gen a, s) -> Gen (a, a) -gen2 (gen, start) = evalStateT ((,) <$> gen <*> gen) start - -gen3 :: (StateT s Gen a, s) -> Gen (a, a, a) -gen3 (gen, start) = evalStateT ((,,) <$> gen <*> gen <*> gen) start - -semigroupLaw - :: forall a - . (Arbitrary a, Semigroup a, Eq a, Show a) - => Maybe (Gen (a, a, a)) -> TestTree -semigroupLaw mgen = testProperty "associativity" $ associativity' mgen +semigroupLaw :: forall a. (Arbitrary a, Semigroup a, Eq a, Show a) => TestTree +semigroupLaw = testProperty "associativity" associativity where associativity x y (z :: a) = (x <> y) <> z === x <> (y <> z) - associativity' = \case - Nothing -> property associativity - Just gen -> forAll gen $ uncurry3 associativity semilatticeLaws - :: forall a s - . (Arbitrary a, Semilattice a, Eq a, Show a) - => Maybe (StateT s Gen a, s) -> [TestTree] -semilatticeLaws mgen = - [ semigroupLaw $ gen3 <$> mgen - , testProperty "commutativity" $ commutativity' $ gen2 <$> mgen + :: forall a. (Arbitrary a, Semilattice a, Eq a, Show a) => [TestTree] +semilatticeLaws = + [ semigroupLaw @a + , testProperty "commutativity" commutativity , testProperty "idempotency" idempotency ] where idempotency (x :: a) = x `merge` x === x commutativity x (y :: a) = x `merge` y === y `merge` x - commutativity' = \case - Nothing -> property commutativity - Just gen -> forAll gen $ uncurry commutativity -cvrdtLaws - :: forall a s - . (Arbitrary a, CvRDT a, Eq a, Show a) - => Maybe (StateT s Gen a, s) -> [TestTree] -cvrdtLaws = semilatticeLaws +cvrdtLaws :: forall a. (Arbitrary a, CvRDT a, Eq a, Show a) => [TestTree] +cvrdtLaws = semilatticeLaws @a +class Initialize op where + type Initial op + type Initial op = Payload op + + initialize :: Initial op -> Process (Payload op) + default initialize + :: Initial op ~ Payload op => Initial op -> Process (Payload op) + initialize = pure + +instance Initialize (Counter a) + +instance Initialize (GSet a) + +instance Initialize (LWW a) where + type Initial (LWW a) = a + initialize = LWW.initial + +instance Initialize (TwoPSet a) + -- | CmRDT law: concurrent ops commute cmrdtLaw :: forall op. ( CmRDT op , Arbitrary op, Show op - , Arbitrary (Intent op), Show (Intent op) + , Arbitrary (Intent op), Show (Intent op) , Arbitrary (Payload op), Show (Payload op) + , Initialize op + , Arbitrary (Initial op), Show (Initial op) ) => Property -cmrdtLaw = property $ \(s :: Payload op) in1 in2 pid1 pid2 -> - fromMaybe discard $ do - getOp1 <- makeOp @op in1 s - getOp2 <- makeOp @op in2 s - let (op1, op2) = - runLamportClock $ - (,) <$> runProcess pid1 getOp1 <*> runProcess pid2 getOp2 - pure $ - concurrent op1 op2 ==> - (apply op1 . apply op2) s === (apply op2 . apply op1) s +cmrdtLaw = property concurrentOpsCommute + where + concurrentOpsCommute st1 st2 seed3 in1 in2 pid1 pid2 pid3 = + let (op1, op2, state) = runLamportClock $ (,,) + <$> runProcess pid1 (makeOp @op in1 st1 `orElse` discard) + <*> runProcess pid2 (makeOp @op in2 st2 `orElse` discard) + <*> runProcess pid3 (initialize @op seed3) + in concurrent op1 op2 ==> opCommutativity (in1, op1) (in2, op2) state + opCommutativity (in1, op1) (in2, op2) state = + isJust (makeOp @op in1 state) ==> + isJust (makeOp @op in2 state) ==> + counterexample + ( show in1 ++ " must be valid after " ++ show op2 ++ + " applied to " ++ show state ) + (isJust $ makeOp @op in1 $ apply op2 state) + .&&. + (apply op1 . apply op2) state === (apply op2 . apply op1) state -uncurry3 :: (a -> b -> c -> d) -> (a, b, c) -> d -uncurry3 f (a, b, c) = f a b c +orElse :: Maybe a -> a -> a +orElse = flip fromMaybe diff --git a/test/LwwElementSet.hs b/test/LwwElementSet.hs --- a/test/LwwElementSet.hs +++ b/test/LwwElementSet.hs @@ -13,30 +13,14 @@ import Prelude hiding (lookup) -import Control.Monad (replicateM) -import Control.Monad.State.Strict (StateT, lift) -import qualified Data.Map.Strict as Map import Data.Semigroup ((<>)) -import Data.Set (Set) -import qualified Data.Set as Set -import Test.QuickCheck (Arbitrary, Gen, arbitrary) import CRDT.Cv.LwwElementSet (LwwElementSet (..), add, lookup, remove) -import CRDT.LamportClock (LamportTime, runLamportClock, runProcess) +import CRDT.LamportClock (runLamportClock, runProcess) import Laws (cvrdtLaws) -import LWW (genUniquelyTimedLWW) -test_Cv = - cvrdtLaws @(LwwElementSet Char) $ Just (genUniquelyTimedLES, Set.empty) - --- | Generate specified number of 'LWW' with unique timestamps -genUniquelyTimedLES - :: (Arbitrary a, Ord a) => StateT (Set LamportTime) Gen (LwwElementSet a) -genUniquelyTimedLES = do - values <- lift arbitrary - tags <- replicateM (length values) genUniquelyTimedLWW - pure $ LES $ Map.fromList $ zip values tags +test_Cv = cvrdtLaws @(LwwElementSet Char) prop_add (s :: LwwElementSet Char) x pid1 = runLamportClock $ do diff --git a/test/Max.hs b/test/Max.hs --- a/test/Max.hs +++ b/test/Max.hs @@ -12,6 +12,6 @@ import Laws (cvrdtLaws) -test_Cv = cvrdtLaws @(Max Char) Nothing +test_Cv = cvrdtLaws @(Max Char) prop_merge (x :: Char) y = query (initial x `merge` initial y) === max x y diff --git a/test/ORSet.hs b/test/ORSet.hs --- a/test/ORSet.hs +++ b/test/ORSet.hs @@ -14,7 +14,7 @@ import Laws (cvrdtLaws) -test_Cv = cvrdtLaws @(ORSet Int) Nothing +test_Cv = cvrdtLaws @(ORSet Int) prop_add pid (x :: Char) s = runLamportClock $ runProcess pid $ not . lookup x . remove x <$> add x s diff --git a/test/PNCounter.hs b/test/PNCounter.hs --- a/test/PNCounter.hs +++ b/test/PNCounter.hs @@ -12,7 +12,7 @@ import GCounter () import Laws (cvrdtLaws) -test_Cv = cvrdtLaws @(PNCounter Int) Nothing +test_Cv = cvrdtLaws @(PNCounter Int) prop_increment (counter :: PNCounter Int) pid = query (increment pid counter) === succ (query counter) diff --git a/test/QCUtil.hs b/test/QCUtil.hs deleted file mode 100644 --- a/test/QCUtil.hs +++ /dev/null @@ -1,15 +0,0 @@ -module QCUtil - ( genUnique - ) where - -import Control.Monad.State.Strict (StateT, get, lift, modify) -import Data.Set (Set) -import qualified Data.Set as Set -import Test.QuickCheck (Arbitrary, Gen, arbitrary, suchThat) - -genUnique :: (Arbitrary a, Ord a) => StateT (Set a) Gen a -genUnique = do - used <- get - a <- lift $ arbitrary `suchThat` (`Set.notMember` used) - modify $ Set.insert a - pure a