diff --git a/src/ldfi2/app/Main.hs b/src/ldfi2/app/Main.hs index d0b5e061..9dffc77a 100644 --- a/src/ldfi2/app/Main.hs +++ b/src/ldfi2/app/Main.hs @@ -7,7 +7,7 @@ module Main where import qualified Data.Text.IO as T import qualified Ldfi -import Ldfi.FailureSpec (FailureSpec(FailureSpec)) +import Ldfi.FailureSpec (FailureSpec (FailureSpec)) import qualified Ldfi.GitHash as Git import Ldfi.Sat (z3Solver) import Ldfi.Storage @@ -23,6 +23,7 @@ data Config = Config endOfFiniteFailures :: Maybe Int "The logical time after which we can't generate faults", maxCrashes :: Maybe Int "The number of crashes we are allowed to generate", endOfTime :: Maybe Int "NOT USED", + limitNumberOfFaults :: Maybe Int "Set a limit to the number of faults generated", version :: Bool "Print the git commit this binary was built from" } deriving (Generic, Show) @@ -38,7 +39,7 @@ go :: Config -> IO () -> IO () go cfg help | unHelpful $ version cfg = putStrLn Git.version | otherwise = - let mFailSpec = makeFailureSpec (unHelpful $ endOfFiniteFailures cfg) (unHelpful $ maxCrashes cfg) (unHelpful $ endOfTime cfg) + let mFailSpec = makeFailureSpec (unHelpful $ endOfFiniteFailures cfg) (unHelpful $ maxCrashes cfg) (unHelpful $ endOfTime cfg) (unHelpful $ limitNumberOfFaults cfg) in case (unHelpful $ testId cfg, mFailSpec) of (Just tid, Just failSpec) -> do let testInformation = TestInformation tid (unHelpful $ failedRunId cfg) @@ -46,7 +47,7 @@ go cfg help T.putStrLn json (_, _) -> help -makeFailureSpec :: Maybe Int -> Maybe Int -> Maybe Int -> Maybe FailureSpec -makeFailureSpec (Just eof) (Just crashes) (Just eot) = - Just (FailureSpec (toEnum eof) (toEnum crashes) (toEnum eot)) -makeFailureSpec _ _ _ = Nothing +makeFailureSpec :: Maybe Int -> Maybe Int -> Maybe Int -> Maybe Int -> Maybe FailureSpec +makeFailureSpec (Just eof) (Just crashes) (Just eot) limitFailures = + Just (FailureSpec (toEnum eof) (toEnum crashes) (toEnum eot) limitFailures) +makeFailureSpec _ _ _ _ = Nothing diff --git a/src/ldfi2/src/Ldfi.hs b/src/ldfi2/src/Ldfi.hs index a917f8b8..84c1cc46 100644 --- a/src/ldfi2/src/Ldfi.hs +++ b/src/ldfi2/src/Ldfi.hs @@ -6,6 +6,7 @@ module Ldfi where import qualified Data.Aeson as Aeson import qualified Data.ByteString.Lazy as BSL +import Data.Map (Map) import qualified Data.Map as Map import Data.Set (Set) import qualified Data.Set as Set @@ -43,12 +44,12 @@ affects (Crash n a) (Event s sa r ra) = -- failureSemantic computes a formula s.t for each event either (xor) the event -- is true or one of the failures that affect it is true failureSemantic :: Set Event -> Set Fault -> LDFIFormula -failureSemantic events failures = +failureSemantic events faults = And [ Var (EventVar event) :+ Or [ Var (FaultVar failure) - | failure <- Set.toList failures, + | failure <- Set.toList faults, failure `affects` event ] | event <- Set.toList events @@ -102,22 +103,27 @@ enumerateAllFaults events fs = Set.unions (Set.map possibleFailure events) -- * If we introduce faults the corresponding events are false (`failureSemantic`) -- * We don't intruduce faults that violates the failure spec (`failureSpecConstaint`) -- * The lineage graph from traces are not satisfied (`Neg lineage`) -ldfi :: FailureSpec -> [Trace] -> [Failures] -> FormulaF String -ldfi fs ts failures = +ldfi :: FailureSpec -> Map RunId Trace -> Failures -> FormulaF String +ldfi failureSpec tracesByRuns failures = fmap show $ simplify $ - And - [ failureSemantic allEvents allFaults, - failureSpecConstraint fs allEvents allFaults, - Neg (lineage ts), - And - [ Neg $ And $ map (Var . FaultVar) faults - | faults <- failures - ] - ] + And $ + addLimit + [ failureSemantic allEvents allFaults, + failureSpecConstraint failureSpec allEvents allFaults, + Neg (lineage traces), + And + [ Neg $ And $ map (Var . FaultVar) faults + | faults <- fFaultsFromFailedRuns failures + ] + ] where - allEvents = Set.unions (map Set.fromList ts) - allFaults = enumerateAllFaults allEvents fs + addLimit xs = case numberOfFaultLimit failureSpec of + Nothing -> xs + Just l -> AtMost [FaultVar $ f | f <- Set.toList allFaults] l : xs + traces = Map.elems tracesByRuns + allEvents = Set.unions (map Set.fromList traces) + allFaults = enumerateAllFaults allEvents failureSpec ------------------------------------------------------------------------ @@ -136,7 +142,7 @@ marshalFaults = TE.decodeUtf8 . BSL.toStrict . Aeson.encode . MF.Faults . map co where convert :: Fault -> MF.Fault convert (Crash f a) = MF.Crash f a - convert (Omission (f,t) a) = MF.Omission f t a + convert (Omission (f, t) a) = MF.Omission f t a run :: Monad m => Storage m -> Solver m -> TestInformation -> FailureSpec -> m [Fault] run Storage {load, loadFailures} Solver {solve} testInformation failureSpec = do diff --git a/src/ldfi2/src/Ldfi/FailureSpec.hs b/src/ldfi2/src/Ldfi/FailureSpec.hs index dcbb7930..cb3f14c3 100644 --- a/src/ldfi2/src/Ldfi/FailureSpec.hs +++ b/src/ldfi2/src/Ldfi/FailureSpec.hs @@ -13,5 +13,7 @@ data FailureSpec = FailureSpec -- | The maximum amount of crashes allowed. maxCrashes :: Natural, -- | When the test stops (a.k.a. EOT). - endOfTime :: Time + endOfTime :: Time, + -- | Potential max limit of number of faults + numberOfFaultLimit :: Maybe Int } diff --git a/src/ldfi2/src/Ldfi/Marshal/Faults.hs b/src/ldfi2/src/Ldfi/Marshal/Faults.hs index 9396d071..fd929f29 100644 --- a/src/ldfi2/src/Ldfi/Marshal/Faults.hs +++ b/src/ldfi2/src/Ldfi/Marshal/Faults.hs @@ -1,4 +1,5 @@ {-# LANGUAGE DeriveGeneric #-} + module Ldfi.Marshal.Faults where import Data.Aeson @@ -8,21 +9,23 @@ import GHC.Natural (Natural) data Fault = Omission - { from :: String, - to :: String, - at :: Natural - } + { from :: String, + to :: String, + at :: Natural + } | Crash - { from :: String, - at :: Natural - } + { from :: String, + at :: Natural + } deriving (Generic, Show) customOptions :: Options -customOptions = defaultOptions - { sumEncoding = defaultTaggedObject { tagFieldName = "kind"}, - constructorTagModifier = map toLower - } +customOptions = + defaultOptions + { sumEncoding = defaultTaggedObject {tagFieldName = "kind"}, + constructorTagModifier = map toLower + } + instance FromJSON Fault where parseJSON = genericParseJSON customOptions @@ -31,7 +34,7 @@ instance ToJSON Fault where toEncoding = genericToEncoding customOptions data Faults = Faults - { faults :: [Fault]} + {faults :: [Fault]} deriving (Generic, Show) instance ToJSON Faults diff --git a/src/ldfi2/src/Ldfi/Prop.hs b/src/ldfi2/src/Ldfi/Prop.hs index 5f0c5d21..9b760d36 100644 --- a/src/ldfi2/src/Ldfi/Prop.hs +++ b/src/ldfi2/src/Ldfi/Prop.hs @@ -20,10 +20,10 @@ data FormulaF var | FormulaF var :|| FormulaF var | FormulaF var :+ FormulaF var | FormulaF var :-> FormulaF var + | FormulaF var :<-> FormulaF var | And [FormulaF var] | Or [FormulaF var] | Neg (FormulaF var) - | FormulaF var :<-> FormulaF var | AtMost [var] Int | TT | FF @@ -37,13 +37,14 @@ genFormula env 0 = QC.oneof [ pure TT, pure FF, - Var <$> QC.elements env + Var <$> QC.elements env, + AtMost <$> QC.listOf1 (QC.elements env) <*> QC.arbitrarySizedNatural ] genFormula env size = QC.oneof [ genFormula env 0, Neg <$> genFormula env (size - 1), - QC.elements [(:&&), (:||), (:+), (:<->)] <*> genFormula env (size `div` 2) <*> genFormula env (size `div` 2), + QC.elements [(:&&), (:||), (:+), (:<->), (:->)] <*> genFormula env (size `div` 2) <*> genFormula env (size `div` 2), do n <- QC.choose (0, size `div` 2) QC.elements [And, Or] <*> QC.vectorOf n (genFormula env (size `div` 4)) @@ -57,6 +58,14 @@ instance QC.Arbitrary v => QC.Arbitrary (FormulaF v) where getVars :: Ord var => FormulaF var -> Set var getVars = foldMap Set.singleton +isTT :: FormulaF var -> Bool +isTT TT = True +isTT _ = False + +isFF :: FormulaF var -> Bool +isFF FF = True +isFF _ = False + simplify1 :: FormulaF var -> FormulaF var simplify1 (TT :&& r) = simplify1 r simplify1 (l :&& r) = simplify1 l :&& simplify1 r @@ -65,12 +74,23 @@ simplify1 (_l :|| TT) = TT simplify1 (l :|| r) = simplify1 l :|| simplify1 r simplify1 (And []) = TT simplify1 (And [f]) = f -simplify1 (And fs) = And (map simplify1 fs) +simplify1 (And fs) + | not (null [() | FF <- fs]) = FF + | otherwise = And (map simplify1 $ filter (not . isTT) fs) simplify1 (Or []) = FF simplify1 (Or [f]) = f -simplify1 (Or fs) = Or (map simplify1 fs) +simplify1 (Or fs) + | not (null [()| TT <- fs]) = TT + | otherwise = Or (map simplify1 $ filter (not . isFF) fs) +simplify1 (Neg FF) = TT +simplify1 (Neg TT) = FF +simplify1 (Neg (Neg f)) = f simplify1 (Neg f) = Neg (simplify1 f) simplify1 (l :<-> r) = simplify1 l :<-> simplify1 r +simplify1 (TT :-> f) = simplify1 f +simplify1 (FF :-> _) = TT +simplify1 (f :-> FF) = Neg $ simplify1 f +simplify1 (_ :-> TT) = TT simplify1 (l :-> r) = simplify1 l :-> simplify1 r simplify1 (l :+ r) = simplify1 l :+ simplify1 r simplify1 f@(AtMost {}) = f diff --git a/src/ldfi2/src/Ldfi/Sat.hs b/src/ldfi2/src/Ldfi/Sat.hs index 47d562f6..47351f25 100644 --- a/src/ldfi2/src/Ldfi/Sat.hs +++ b/src/ldfi2/src/Ldfi/Sat.hs @@ -58,31 +58,31 @@ z3SolveAll limit f = do a <- translate env f assert a go 0 [] vs vs' - where - limitReached :: Int -> Bool - limitReached n = case limit of - Nothing -> False - Just k -> n >= k + where + limitReached :: Int -> Bool + limitReached n = case limit of + Nothing -> False + Just k -> n >= k - go :: MonadZ3 z3 => Int -> [Solution] -> [String] -> [AST] -> z3 [Solution] - go n acc vs vs' - | limitReached n = return (reverse acc) - | otherwise = do - (result, mModel) <- getModel - case result of - Undef -> error "impossible" - Unsat -> return (reverse acc) - Sat -> case mModel of - Nothing -> error "impossible" -- TODO(stevan): steal Agda's __IMPOSSIBLE__? - Just model -> do - mbs <- mapM (evalBool model) vs' - let bs = map (maybe (error "impossible") id) mbs - bs' <- - mapM - (\(ix, b) -> mkNot =<< mkEq (vs' !! ix) =<< mkBool b) - (zip [0 .. length bs - 1] bs) - assert =<< mkOr bs' - go (succ n) (Solution (Map.fromList (zip vs bs)) : acc) vs vs' + go :: MonadZ3 z3 => Int -> [Solution] -> [String] -> [AST] -> z3 [Solution] + go n acc vs vs' + | limitReached n = return (reverse acc) + | otherwise = do + (result, mModel) <- getModel + case result of + Undef -> error "impossible" + Unsat -> return (reverse acc) + Sat -> case mModel of + Nothing -> error "impossible" -- TODO(stevan): steal Agda's __IMPOSSIBLE__? + Just model -> do + mbs <- mapM (evalBool model) vs' + let bs = map (maybe (error "impossible") id) mbs + bs' <- + mapM + (\(ix, b) -> mkNot =<< mkEq (vs' !! ix) =<< mkBool b) + (zip [0 .. length bs - 1] bs) + assert =<< mkOr bs' + go (succ n) (Solution (Map.fromList (zip vs bs)) : acc) vs vs' z3Solver :: Solver IO z3Solver = Solver z3Solve diff --git a/src/ldfi2/src/Ldfi/Storage.hs b/src/ldfi2/src/Ldfi/Storage.hs index 62daaad2..e907fdf4 100644 --- a/src/ldfi2/src/Ldfi/Storage.hs +++ b/src/ldfi2/src/Ldfi/Storage.hs @@ -3,10 +3,14 @@ module Ldfi.Storage where +import Control.Arrow (second) import Control.Exception import Data.Aeson (decode) import qualified Data.Binary.Builder as BB import Data.List (groupBy, intercalate) +import Data.Map (Map) +import qualified Data.Map as Map +import Data.Set (Set) import qualified Data.Set as Set import Data.Text (Text) import qualified Data.Text as Text @@ -27,7 +31,10 @@ type RunId = Int data Fault = Crash Node Time | Omission Edge Time deriving (Eq, Ord, Read, Show) -type Failures = [Fault] +data Failures = Failures + { fFaultsFromFailedRuns :: [[Fault]], + fFaultsPerRun :: Map RunId [Fault] + } data LdfiEvent = LdfiEvent { leTestId :: TestId, @@ -43,16 +50,23 @@ data TestInformation = TestInformation } data Storage m = Storage - { load :: TestInformation -> m [Trace], - loadFailures :: TestInformation -> m [Failures], + { load :: TestInformation -> m (Map RunId Trace), + loadFailures :: TestInformation -> m Failures, store :: LdfiEvent -> m () } +emptyFailures :: Failures +emptyFailures = + Failures + { fFaultsFromFailedRuns = [], + fFaultsPerRun = Map.empty + } + mockStorage :: Monad m => [Trace] -> Storage m mockStorage ts = Storage - { load = const (return ts), - loadFailures = const (return []), + { load = const (return $ Map.fromList $ zip [0 ..] ts), + loadFailures = const (return emptyFailures), store = const (return ()) } @@ -80,13 +94,12 @@ instance FromRow NetworkTraceEvent where sqliteShowSequence :: [Int] -> String sqliteShowSequence xs = "(" ++ intercalate ", " (map show xs) ++ ")" -sqliteLoad :: TestInformation -> IO [Trace] +sqliteLoad :: TestInformation -> IO (Map RunId Trace) sqliteLoad testInformation = do path <- getDbPath conn <- open path - let - testId = tiTestId testInformation - failedRuns = Set.fromList $ tiFailedRuns testInformation + let testId = tiTestId testInformation + failedRuns = Set.fromList $ tiFailedRuns testInformation r <- queryNamed conn @@ -99,36 +112,45 @@ sqliteLoad testInformation = do \ ORDER BY run_id ASC" [":testId" := testId] :: IO [NetworkTraceEvent] - return (historyToTrace (groupBy (\e1 e2 -> nteRunId e1 == nteRunId e2) . filter (not . flip Set.member failedRuns . nteRunId) $ r)) + return (Map.fromList . map prepareToMap . groupBy (\e1 e2 -> nteRunId e1 == nteRunId e2) . filter (not . flip Set.member failedRuns . nteRunId) $ r) where - historyToTrace :: [[NetworkTraceEvent]] -> [Trace] - historyToTrace = map (map go) + prepareToMap :: [NetworkTraceEvent] -> (RunId, Trace) + prepareToMap [] = error "impossible" + prepareToMap xs@(h : _) = (nteRunId h, historyToTrace xs) + + historyToTrace :: [NetworkTraceEvent] -> Trace + historyToTrace = map go where go :: NetworkTraceEvent -> Event go (NetworkTraceEvent _runId sender receiver recvAt sentAt) = Event sender (toEnum sentAt) receiver (toEnum recvAt) -sqliteLoadFailure :: TestInformation -> IO [Failures] +sqliteLoadFailure :: TestInformation -> IO Failures sqliteLoadFailure testInformation = do path <- getDbPath conn <- open path - let - testId = tiTestId testInformation - failedRuns = Set.fromList $ tiFailedRuns testInformation + let testId = tiTestId testInformation + failedRuns = Set.fromList $ tiFailedRuns testInformation r <- queryNamed conn "SELECT run_id, faults FROM run_info WHERE test_id = :testId" [":testId" := testId] :: IO [(RunId, Text)] - return . map (parse . snd) . filter (flip Set.member failedRuns . fst) $ r + return . toFailures failedRuns . map (second parse) $ r where - parse :: Text -> Failures + toFailures :: Set RunId -> [(Int, [Fault])] -> Failures + toFailures failedRuns xs = + Failures + { fFaultsFromFailedRuns = map snd . filter (flip Set.member failedRuns . fst) $ xs, + fFaultsPerRun = Map.fromList xs + } + parse :: Text -> [Fault] parse s = case decode (BB.toLazyByteString $ TextE.encodeUtf8Builder s) of Nothing -> error $ "Unable to parse faults: " ++ Text.unpack s - Just x -> map convert x + Just x -> map convert x convert :: MF.Fault -> Fault - convert (MF.Omission f t a) = Omission (f,t) a + convert (MF.Omission f t a) = Omission (f, t) a convert (MF.Crash f a) = Crash f a -- TODO(stevan): What exactly do we need to store? Previous faults are no longer diff --git a/src/ldfi2/test/Driver.hs b/src/ldfi2/test/Driver.hs index 24b6bd73..e4cf3c10 100644 --- a/src/ldfi2/test/Driver.hs +++ b/src/ldfi2/test/Driver.hs @@ -1 +1,3 @@ {-# OPTIONS_GHC -F -pgmF tasty-discover -optF --generated-module=Driver #-} + +module Driver where diff --git a/src/ldfi2/test/LdfiTest.hs b/src/ldfi2/test/LdfiTest.hs index c3422446..89addc3e 100644 --- a/src/ldfi2/test/LdfiTest.hs +++ b/src/ldfi2/test/LdfiTest.hs @@ -17,7 +17,8 @@ emptyFailureSpec = FailureSpec { endOfFiniteFailures = 0, maxCrashes = 0, - endOfTime = 0 + endOfTime = 0, + numberOfFaultLimit = Nothing } data WasSame = Same | NotSame String @@ -117,7 +118,8 @@ broadcastFailureSpec = FailureSpec { endOfFiniteFailures = 3, maxCrashes = 1, - endOfTime = 5 + endOfTime = 5, + numberOfFaultLimit = Nothing } -- TODO(stevan): This seems wrong, should be `Omission "A" "B" 1` or `Omission diff --git a/src/lib/ldfi.go b/src/lib/ldfi.go index 9c03d81a..cb2c74ed 100644 --- a/src/lib/ldfi.go +++ b/src/lib/ldfi.go @@ -11,9 +11,10 @@ import ( ) type FailSpec struct { - EFF int // End (time) of finite failures. - Crashes int // Max amount of node (permanent) crashes. - EOT int // End of time, for the test. + EFF int // End (time) of finite failures. + Crashes int // Max amount of node (permanent) crashes. + EOT int // End of time, for the test. + LimitFaults int // Have a limit of how many faults may be generated, 0 is no limit } type Fault struct { @@ -79,6 +80,10 @@ func Ldfi(testId TestId, failedRunIds []RunId, fail FailSpec) Faults { "--testId", strconv.Itoa(testId.TestId), "--endOfTime", strconv.Itoa(0), // not used } + if fail.LimitFaults > 0 { + args = append(args, "--limitNumberOfFaults") + args = append(args, strconv.Itoa(fail.LimitFaults)) + } for _, r := range failedRunIds { args = append(args, "--failedRunId") args = append(args, strconv.Itoa(r.RunId))