Merge #3640 #3662

3640: Connection manager transition order test using IOSimPOR r=coot a=coot

This PR adds a quickcheck property test which validates order of connection manager transitions using *IOSimPOR*.  It also fixes a connection manager bug discovered thanks to the new test.

Fixes #3613.

- connection-manager-tests: test transition order
- connection-manager: don't blindly override state
- connection-manager-tests: code style


3662: Removed ST effects from IOSimPOR r=coot a=coot

ST effects are thread local, they never race with other steps.  This patch
reverts a previous fix commited in PR #3647.

Thanks for `IOSimPOR` we also found out that the transition:
`UnnegotiatedSt Inbound → TerminatingSt` should be valid, similarly to one for
outbound connections (see PR #3652, commit fbcb6aada).


Co-authored-by: Marcin Szamotulski <[email protected]>

Author: iohk-bors[bot]

io-sim/src/Control/Monad/IOSimPOR/Internal.hs

@@ -378,8 +378,7 @@ schedule thread@Thread{
 
     LiftST st k -> do
       x <- strictToLazyST st
-      let thread' = thread { threadControl = ThreadControl (k x) ctl,
-                             threadEffect  = effect <> liftSTEffect }
+      let thread' = thread { threadControl = ThreadControl (k x) ctl }
       schedule thread' simstate
 
     GetMonoTime k -> do
@@ -1463,23 +1462,16 @@ updateRaces newStep@Step{ stepThreadId = tid, stepEffect = newEffect }
           -- then any threads that it wakes up become non-concurrent also.
           let lessConcurrent = foldr Set.delete concurrent (effectWakeup newEffect) in
           if tid `elem` concurrent then
-            let theseStepsRace = isRacyThreadId tid
-                              && step `racingSteps` newStep
+            let theseStepsRace = isRacyThreadId tid && racingSteps step newStep
                 happensBefore  = step `happensBeforeStep` newStep
                 nondep' | happensBefore = nondep
                         | otherwise     = newStep : nondep
-                -- We cannot remove the 'tid' thread from the set of concurrent
-                -- threads if 'theseStepsRace'.  This was done previously in
-                -- order to record only the first race with each thread.  But
-                -- it can happen that the frist race will block a thread that
-                -- is scheduled to run until another later step unblock it
-                -- (e.g. 'modifyTMVar`).  If we remove the 'tid' from the set
-                -- of concurrent threads we can end up in a situation where
-                -- a schedule is not runnable, because the next thread to run
-                -- is still blocked (e.g. 'TMVar' is taken but not yet
-                -- released).
-                concurrent' | happensBefore = Set.delete tid lessConcurrent
-                            | otherwise     = concurrent
+                -- We will only record the first race with each thread---reversing
+                -- the first race makes the next race detectable. Thus we remove a
+                -- thread from the concurrent set after the first race.
+                concurrent' | happensBefore  = Set.delete tid lessConcurrent
+                            | theseStepsRace = Set.delete tid concurrent
+                            | otherwise      = concurrent
                 -- Here we record discovered races.
                 -- We only record a new race if we are following the default schedule,
                 -- to avoid finding the same race in different parts of the search space.

io-sim/src/Control/Monad/IOSimPOR/Types.hs

@@ -17,18 +17,17 @@ data Effect = Effect {
     effectReads  :: !(Set TVarId),
     effectWrites :: !(Set TVarId),
     effectForks  :: !(Set ThreadId),
-    effectLiftST :: !Bool,
     effectThrows :: ![ThreadId],
     effectWakeup :: ![ThreadId]
   }
   deriving (Eq, Show)
 
 instance Semigroup Effect where
-  Effect r w s b ts wu <> Effect r' w' s' b' ts' wu' =
-    Effect (r<>r') (w<>w') (s<>s') (b||b') (ts++ts') (wu++wu')
+  Effect r w s ts wu <> Effect r' w' s' ts' wu' =
+    Effect (r<>r') (w<>w') (s<>s') (ts++ts') (wu++wu')
 
 instance Monoid Effect where
-  mempty = Effect Set.empty Set.empty Set.empty False [] []
+  mempty = Effect Set.empty Set.empty Set.empty [] []
 
 -- readEffect :: SomeTVar s -> Effect
 -- readEffect r = mempty{effectReads = Set.singleton $ someTvarId r }
@@ -45,9 +44,6 @@ writeEffects rs = mempty{effectWrites = Set.fromList (map someTvarId rs)}
 forkEffect :: ThreadId -> Effect
 forkEffect tid = mempty{effectForks = Set.singleton $ tid}
 
-liftSTEffect :: Effect
-liftSTEffect = mempty{ effectLiftST = True }
-
 throwToEffect :: ThreadId -> Effect
 throwToEffect tid = mempty{ effectThrows = [tid] }
 
@@ -62,9 +58,7 @@ onlyReadEffect e = e { effectReads = effectReads mempty } == mempty
 
 racingEffects :: Effect -> Effect -> Bool
 racingEffects e e' =
-      (effectLiftST e  && racesWithLiftST e')
-   || (effectLiftST e' && racesWithLiftST e )
-   || effectThrows e `intersectsL` effectThrows e'
+      effectThrows e `intersectsL` effectThrows e'
    || effectReads  e `intersects`  effectWrites e'
    || effectWrites e `intersects`  effectReads  e'
    || effectWrites e `intersects`  effectWrites e'
@@ -74,8 +68,3 @@ racingEffects e e' =
 
     intersectsL :: Eq a => [a] -> [a] -> Bool
     intersectsL a b = not $ null $ a `List.intersect` b
-
-    racesWithLiftST eff =
-         effectLiftST eff
-      || not (Set.null (effectReads eff) && Set.null (effectWrites eff))
-