Remove unsupported concurrency metrics

3 files changed, 52 insertions, 51 deletions

diff --git a/source/Api.hs b/source/Api.hs
index 6d88b7a..7e76c02 100644
--- a/source/Api.hs
+++ b/source/Api.hs
@@ -399,7 +399,7 @@ data VerificationReport = VerificationReport
     }
     deriving (Show, Eq)
 
--- | Invocation-local observation of the sequential verification pipeline.
+-- | Invocation-local observation of the verification pipeline.
 --
 -- Durations use the monotonic clock and are never part of fact authority or
 -- deterministic verification results.
@@ -415,7 +415,6 @@ data VerificationMeasurements = VerificationMeasurements
     , verificationMaximumLiveModuleCheckers :: !Int
     , verificationMaximumLiveVampireProcesses :: !Int
     , verificationMaximumReadyModuleCount :: !Int
-    , verificationReadyModuleWaitNanoseconds :: !Word64
     , verificationObligationBatchCount :: !Int
     , verificationPreparedObligationCount :: !Int
     , verificationMaximumObligationBatchSize :: !Int
@@ -438,7 +437,6 @@ data VerificationObservation = VerificationObservation
     , observedMaximumLiveModuleCheckers :: !Int
     , observedMaximumLiveVampireProcesses :: !Int
     , observedMaximumReadyModuleCount :: !Int
-    , observedReadyModuleWaitNanoseconds :: !Word64
     , observedObligationBatchCount :: !Int
     , observedPreparedObligationCount :: !Int
     , observedMaximumObligationBatchSize :: !Int
@@ -461,7 +459,6 @@ initialVerificationObservation =
         , observedMaximumLiveModuleCheckers = 0
         , observedMaximumLiveVampireProcesses = 0
         , observedMaximumReadyModuleCount = 0
-        , observedReadyModuleWaitNanoseconds = 0
         , observedObligationBatchCount = 0
         , observedPreparedObligationCount = 0
         , observedMaximumObligationBatchSize = 0
@@ -1635,8 +1632,6 @@ finalizeVerificationMeasurements
             observedMaximumLiveVampireProcesses observation
         , verificationMaximumReadyModuleCount =
             observedMaximumReadyModuleCount observation
-        , verificationReadyModuleWaitNanoseconds =
-            observedReadyModuleWaitNanoseconds observation
         , verificationObligationBatchCount =
             observedObligationBatchCount observation
         , verificationPreparedObligationCount =
@@ -1763,21 +1758,9 @@ renderVerificationMeasurements measurements =
             <> renderNanoseconds
                 (verificationVampireExecutionNanoseconds
                     measurements)
-        , "vampire_idle_ms="
-            <> renderNanoseconds
-                (verificationVampireIdleNanoseconds
-                    measurements)
-        , "vampire_utilization_permille="
-            <> renderIntegral
-                (verificationVampireUtilizationPermille
-                    measurements)
         , "max_ready_modules=" <> renderIntegral
             (verificationMaximumReadyModuleCount
                 measurements)
-        , "ready_wait_sum_ms="
-            <> renderNanoseconds
-                (verificationReadyModuleWaitNanoseconds
-                    measurements)
         , "total_ms="
             <> renderNanoseconds
                 (verificationInvocationNanoseconds
@@ -1787,35 +1770,6 @@ renderVerificationMeasurements measurements =
     parseMeasurements =
         verificationParseMeasurements measurements
 
-verificationVampireIdleNanoseconds
-    :: VerificationMeasurements
-    -> Word64
-verificationVampireIdleNanoseconds measurements =
-    checking - min checking execution
-  where
-    checking =
-        verificationCheckingNanoseconds measurements
-    execution =
-        verificationVampireExecutionNanoseconds
-            measurements
-
-verificationVampireUtilizationPermille
-    :: VerificationMeasurements
-    -> Word64
-verificationVampireUtilizationPermille measurements
-    | checking == 0 =
-        0
-    | otherwise =
-        min
-            1000
-            (execution * 1000 `div` checking)
-  where
-    checking =
-        verificationCheckingNanoseconds measurements
-    execution =
-        verificationVampireExecutionNanoseconds
-            measurements
-
 renderNanoseconds :: Word64 -> Text
 renderNanoseconds nanoseconds =
     renderIntegral (nanoseconds `div` 1000000)
diff --git a/source/Test/Unit/Module.hs b/source/Test/Unit/Module.hs
index 27110a5..35256e0 100644
--- a/source/Test/Unit/Module.hs
+++ b/source/Test/Unit/Module.hs
@@ -69,6 +69,7 @@ import Data.Set qualified as Set
 import Data.Vector qualified as Vector
 import System.Directory
     ( createDirectoryIfMissing
+    , doesFileExist
     , getCurrentDirectory
     , getPermissions
     , setOwnerExecutable
@@ -4975,6 +4976,9 @@ selectsConcurrentModuleFailureDeterministically = do
                 pure measurements
             runCase label jobsAmount = do
                 let storePath = root Posix.</> (label <> ".sqlite")
+                    processLock = root Posix.</> (label <> ".process-lock")
+                    processStarted =
+                        root Posix.</> (label <> ".process-started")
                 writeAcceptedFixtureVampire executable
                 (_startup, store) <-
                     Store.openStore storePath (Identity.theoryId foundation)
@@ -4994,6 +4998,11 @@ selectsConcurrentModuleFailureDeterministically = do
                     writeFile executable
                         (unlines
                             [ "#!/bin/sh"
+                            , "while ! mkdir \"" <> processLock
+                                <> "\" 2>/dev/null; do sleep 0.01; done"
+                            , "trap 'rmdir \"" <> processLock
+                                <> "\"' EXIT"
+                            , ": > \"" <> processStarted <> "\""
                             , "cat >/dev/null"
                             , "printf '%s\\n' '% SZS status CounterSatisfiable for concurrent-fixture'"
                             ])
@@ -5008,9 +5017,12 @@ selectsConcurrentModuleFailureDeterministically = do
                                         (\positions ->
                                             (position : positions, ()))
                                     when
-                                        (Provers.workPositionModuleOrdinal
-                                            position == 1)
-                                        (threadDelay 200000))
+                                        (jobsAmount > 1
+                                            && Provers.workPositionModuleOrdinal
+                                                position == 1)
+                                        (waitForFileSignal
+                                            "later module process"
+                                            processStarted))
                     jobs <- select jobsAmount
                     (result, measurements) <-
                         runNoLoggingT
@@ -5043,6 +5055,23 @@ selectsConcurrentModuleFailureDeterministically = do
             1
             (Api.verificationMaximumLiveVampireProcesses sequential)
 
+waitForFileSignal :: String -> FilePath -> Assertion
+waitForFileSignal label path = do
+    guarded <- Timeout.timeout 10000000 loop
+    case guarded of
+        Just () ->
+            pure ()
+        Nothing ->
+            assertFailure (label <> " was not observed")
+  where
+    loop = do
+        exists <- doesFileExist path
+        if exists
+            then pure ()
+            else do
+                threadDelay 10000
+                loop
+
 schedulesDiamondAfterSealedImports :: Assertion
 schedulesDiamondAfterSealedImports = do
     foundation <- expectRight Foundation.checkedFoundation
diff --git a/source/Test/Unit/Provers.hs b/source/Test/Unit/Provers.hs
index 62dccdd..22a6b5b 100644
--- a/source/Test/Unit/Provers.hs
+++ b/source/Test/Unit/Provers.hs
@@ -172,7 +172,7 @@ vampireExecutorTests =
                                                 (workPosition 2 1)
                                                 prepared))
                                         \queued -> do
-                                            threadDelay 20000
+                                            waitForSubmittedCount executor 2
                                             cancel queued
                                             cancel running
                                     observed <- vampireExecutorObservation
@@ -565,6 +565,24 @@ waitForProcessIds path = do
                 threadDelay 10000
                 loop
 
+waitForSubmittedCount :: VampireExecutor -> Int -> Assertion
+waitForSubmittedCount executor expected = do
+    guarded <- Timeout.timeout 10000000 loop
+    case guarded of
+        Just () ->
+            pure ()
+        Nothing ->
+            assertFailure
+                ("executor did not submit " <> show expected <> " requests")
+  where
+    loop = do
+        observed <- vampireExecutorObservation executor
+        if vampireExecutorSubmittedCount observed >= expected
+            then pure ()
+            else do
+                threadDelay 10000
+                loop
+
 assertProcessesGone :: [ProcessID] -> Assertion
 assertProcessesGone processIds = do
     guarded <- Timeout.timeout 10000000 loop