feat(ldfi2): Make events have a sent field, so we can be better at ge…

…nerating crashes

src/ldfi2/src/Ldfi.hs

@@ -4,8 +4,6 @@
 
 module Ldfi where
 
-import Data.IntMap (IntMap)
-import qualified Data.IntMap as IntMap
 import qualified Data.Map as Map
 import Data.Set (Set)
 import qualified Data.Set as Set
@@ -36,8 +34,9 @@ lineage ts =
   Or [ makeVars t | t <- map (foldMap $ Set.singleton . EventVar) ts ]
 
 affects :: Fault -> Event -> Bool
-affects (Omission (f, t) a) (Event f' t' a') = f == f' && t == t' && a == a'
-affects (Crash n a) (Event _ n' a') = n == n' && a <= a'
+affects (Omission (s, r) ra) (Event s' _ r' ra') = s == s' && r == r' && ra == ra'
+affects (Crash n a) (Event s sa r ra) =
+    (n == s && a <= sa) || (n == r && a <= ra)
    -- we should be able to be smarter if we knew when something was sent, then
    -- we could also count for the sender..
 
@@ -54,12 +53,17 @@ failureSemantic events failures = And
 -- failureSpecConstraint is the formula that makes sure we are following the
 -- Failure Specification. Although we will never generate any faults that occur
 -- later than eff, so we don't have to check that here
-failureSpecConstraint :: FailureSpec -> Set Fault -> LDFIFormula
-failureSpecConstraint fs faults
+failureSpecConstraint :: FailureSpec -> Set Event -> Set Fault -> LDFIFormula
+failureSpecConstraint fs events faults
   | null crashes = TT
-  | otherwise    = AtMost crashes (Nat.naturalToInt $ maxCrashes fs)
+  | otherwise    = And (AtMost crashVars (Nat.naturalToInt $ maxCrashes fs) : crashConditions)
   where
-    crashes = [ FaultVar c | c@(Crash _ _) <- Set.toList faults ]
+    crashes = [ c | c@(Crash _ _) <- Set.toList faults ]
+    crashVars = map FaultVar crashes
+    crashConditions = [ Var (FaultVar c) :-> Or [ Var (EventVar e)
+                                          | e@(Event s sa _ _) <- Set.toList events
+                                          , s == n && sa < t]
+                      | c@(Crash n t) <- crashes]
 
 -- enumerateAllFaults will generate the interesting faults that could affect the
 -- set of events. But since it is pointless to generate a fault that is later
@@ -77,23 +81,10 @@ enumerateAllFaults events fs = Set.unions (Set.map possibleFailure events)
     eff :: Time
     eff = endOfFiniteFailures fs
 
-    activeNodesAt :: IntMap (Set Node)
-    activeNodesAt = IntMap.fromListWith (<>)
-      [ (fromEnum at, Set.singleton from)
-      | Event from _to at <- Set.toList events
-      ]
-
-    beenActive :: Node -> Time -> Bool
-    beenActive n t = case IntMap.lookup (fromEnum t) activeNodesAt of
-      Nothing -> False
-      Just ns -> Set.member n ns
-
     possibleFailure :: Event -> Set Fault
-    possibleFailure (Event f t a)
-      | eff < a   = Set.singleton (Crash t eff)
-      | otherwise = Set.fromList ([Omission (f, t) a] ++
-                                  -- Only crash nodes that have sent something.
-                                  if beenActive t a then [Crash t a] else [])
+    possibleFailure (Event s sa r ra)
+      | eff < ra  = Set.fromList [Crash s eff , Crash r eff]
+      | otherwise = Set.fromList [Omission (s, r) ra, Crash s sa, Crash r ra]
 
 -- ldfi will produce a formula that if solved will give you:
 -- * Which faults to introduce
@@ -105,7 +96,7 @@ enumerateAllFaults events fs = Set.unions (Set.map possibleFailure events)
 ldfi :: FailureSpec -> [Trace] -> FormulaF String
 ldfi fs ts = fmap show $ simplify $ And
   [ failureSemantic allEvents allFaults
-  , failureSpecConstraint fs allFaults
+  , failureSpecConstraint fs allEvents allFaults
   , Neg (lineage ts)
   ]
   where

src/ldfi2/src/Ldfi/Prop.hs

@@ -16,6 +16,7 @@ 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)
@@ -66,6 +67,7 @@ simplify1 (Or [f])      = f
 simplify1 (Or fs)       = Or (map simplify1 fs)
 simplify1 (Neg f)       = Neg (simplify1 f)
 simplify1 (l :<-> r)    = simplify1 l :<-> simplify1 r
+simplify1 (l :-> r)     = simplify1 l :-> simplify1 r
 simplify1 (l :+ r)      = simplify1 l :+ simplify1 r
 simplify1 f@(AtMost {}) = f
 simplify1 f@TT          = f

src/ldfi2/src/Ldfi/Sat.hs

@@ -29,6 +29,7 @@ translate env f0 = case f0 of
   Or fs       -> mkOr  =<< mapM (translate env) fs
   Neg f       -> mkNot =<< translate env f
   l :<-> r    -> liftFun env l r mkIff
+  l :-> r     -> liftFun env l r mkImplies
   TT          -> mkTrue
   FF          -> mkFalse
   Var v       -> return (env Map.! v)

src/ldfi2/src/Ldfi/Storage.hs

@@ -77,8 +77,8 @@ sqliteLoad testId = do
     historyToTrace = map (map go)
       where
         go :: NetworkTraceEvent -> Event
-        go (NetworkTraceEvent _runId sender receiver received _sent) =
-          Event sender receiver (toEnum received)
+        go (NetworkTraceEvent _runId sender receiver recvAt sentAt) =
+          Event sender (toEnum sentAt) receiver (toEnum recvAt)
 
 -- TODO(stevan): What exactly do we need to store? Previous faults are no longer
 -- interesting.

src/ldfi2/src/Ldfi/Traces.hs

@@ -10,9 +10,10 @@ import GHC.Natural
 type Trace = [Event]
 
 data Event = Event
-  { from :: Node
-  , to   :: Node
-  , at   :: Time
+  { from  :: Node
+  , sent  :: Time
+  , to    :: Node
+  , recv  :: Time
   }
   deriving (Eq, Ord, Read, Show)
 

src/ldfi2/test/LdfiTest.hs

@@ -71,14 +71,14 @@ unit_z3_same_neq = do
 -- suggest failing S1 or S2 or both without also suggesting failing C."
 cacheTraces :: [Trace]
 cacheTraces =
-  [ [Event "A" "B" 0, Event "A" "C" 1]
-  , [Event "A" "B" 0, Event "A" "R" 1, Event "R" "S1" 2, Event "R" "S2" 3]
+  [ [Event "A" 0 "B" 0, Event "A" 1 "C" 1]
+  , [Event "A" 0 "B" 0, Event "A" 1 "R" 1, Event "R" 2 "S1" 2, Event "R" 3 "S2" 3]
   ]
 
 unit_cache_lineage :: Assertion
 unit_cache_lineage =
     (fmap show $ simplify $ lineage cacheTraces) `shouldBe`
-    (var "A" "B" 0 :&& (var "A" "C" 1 :|| And [var "A" "R" 1, var "R" "S1" 2, var "R" "S2" 3]))
+    (var "A" 0 "B" 0 :&& (var "A" 1 "C" 1 :|| And [var "A" 1 "R" 1, var "R" 2 "S1" 2, var "R" 3 "S2" 3]))
   where
 
 dummyTestId :: TestId
@@ -89,22 +89,22 @@ unit_cacheFailures = do
   fs <- run (mockStorage cacheTraces) z3Solver dummyTestId emptyFailureSpec
   fs @?= [ Omission ("A", "B") 0 ]
 
-var :: Node -> Node -> Time -> Formula
-var f t a = Var (show $ EventVar (Event f t a))
+var :: Node -> Time -> Node -> Time -> Formula
+var f ft t tt = Var (show $ EventVar (Event f ft t tt))
 
 ------------------------------------------------------------------------
 
 -- Node A broadcasts to node B and C without retry. Node B getting the
 -- message constitutes a successful outcome.
 broadcast1Traces :: [Trace]
-broadcast1Traces = [ [Event "A" "B" 1, Event "A" "C" 1]
-                   , [Event "A" "B" 1]
+broadcast1Traces = [ [Event "A" 0 "B" 1, Event "A" 0 "C" 1]
+                   , [Event "A" 0 "B" 1]
                    ]
 
 unit_broadcast1 :: Assertion
 unit_broadcast1 =
   (fmap show $ simplify $ lineage broadcast1Traces) `shouldBe`
-  (And [var "A" "B" 1])
+  (And [var "A" 0 "B" 1])
 
 broadcastFailureSpec :: FailureSpec
 broadcastFailureSpec = FailureSpec
@@ -123,32 +123,31 @@ unit_broadcast1Run1 = do
 unit_broadcast1Run2 :: Assertion
 unit_broadcast1Run2 = do
   fs <- run (mockStorage (take 2 broadcast1Traces)) z3Solver dummyTestId broadcastFailureSpec
-  fs @?= [ Omission ("A", "B") 1 ] -- Minimal counterexample.
+  fs @?= [ Omission ("A", "B") 1, Omission ("A", "C") 1 ] -- Minimal counterexample.
 
 ------------------------------------------------------------------------
 
 -- Node A broadcasts to node B and C with retry. Node B getting the
 -- message constitutes a successful outcome.
 broadcast2Traces :: [Trace]
-broadcast2Traces = [ [Event "A" "B" 1, Event "A" "C" 1]
-                   , [Event "A" "B" 1]
-                   , [Event "A" "B" 2, Event "A" "C" 1]
-                   , [Event "A" "B" 4]
+broadcast2Traces = [ [Event "A" 0 "B" 1, Event "A" 0 "C" 1]
+                   , [Event "A" 0 "B" 1]
+                   , [Event "A" 1 "B" 2, Event "A" 0 "C" 1]
+                   , [Event "A" 3 "B" 4]
                    ]
 
 -- Lets assume that run 1 and 2 were the same as in broadcast1.
 unit_broadcast2Run3 :: Assertion
 unit_broadcast2Run3 = do
   fs <- run (mockStorage (take 3 broadcast2Traces)) z3Solver dummyTestId broadcastFailureSpec
-  fs @?= [Omission ("A", "B") 1, Omission ("A", "B") 2]
+  fs @?= [ Crash "A" 1, Omission ("A", "B") 1]
 
 unit_broadcast2Run4 :: Assertion
 unit_broadcast2Run4 = do
   fs <- run (mockStorage (take 4 broadcast2Traces)) z3Solver dummyTestId broadcastFailureSpec
   fs @?=
-    [ Crash "B" 3
+    [ Crash "A" 1
     , Omission ("A", "B") 1
-    , Omission ("A", "B") 2
     ] -- Minimal counterexample.
 
 ------------------------------------------------------------------------