Warn when productivity is low (#2005)

* Warn when productivity is low

* Stylish

* Use logger

* Lint

* Add Kore.Log.WarnIfLowProductivity

* Refactoring: factor out calculations for clarity

Co-authored-by: ana-pantilie <ana.pantilie95@gmail.com>

Author: andreiburdusa

kore/app/exec/Main.hs

@@ -127,6 +127,9 @@ import Kore.Log
 import Kore.Log.ErrorException
     ( errorException
     )
+import Kore.Log.WarnIfLowProductivity
+    ( warnIfLowProductivity
+    )
 import qualified Kore.ModelChecker.Bounded as Bounded
     ( CheckResult (..)
     )
@@ -573,7 +576,7 @@ mainWithOptions execOptions = do
     exitCode <-
         withBugReport Main.exeName bugReport $ \tmpDir -> do
             writeOptionsAndKoreFiles tmpDir execOptions
-            go
+            go <* warnIfLowProductivity
                 & handle handleWithConfiguration
                 & handle handleSomeException
                 & runKoreLog tmpDir koreLogOptions

kore/app/repl/Main.hs

@@ -56,6 +56,9 @@ import Kore.Log
 import Kore.Log.KoreLogOptions
     ( parseKoreLogOptions
     )
+import Kore.Log.WarnIfLowProductivity
+    ( warnIfLowProductivity
+    )
 import Kore.Repl.Data
 import Kore.Step.SMT.Lemma
 import Kore.Syntax.Module
@@ -271,6 +274,7 @@ mainWithOptions
                         mainModuleName
                         koreLogOptions
 
+                warnIfLowProductivity
                 pure ExitSuccess
     exitWith exitCode
   where

kore/src/Kore/Log/Registry.hs

@@ -95,6 +95,9 @@ import Kore.Log.InfoReachability
 import Kore.Log.WarnFunctionWithoutEvaluators
     ( WarnFunctionWithoutEvaluators
     )
+import Kore.Log.WarnIfLowProductivity
+    ( WarnIfLowProductivity
+    )
 import Kore.Log.WarnStuckProofState
     ( WarnStuckProofState
     )
@@ -148,6 +151,7 @@ entryHelpDocs :: [Pretty.Doc ()]
     , mk $ Proxy @WarnFunctionWithoutEvaluators
     , mk $ Proxy @WarnSymbolSMTRepresentation
     , mk $ Proxy @WarnStuckProofState
+    , mk $ Proxy @WarnIfLowProductivity
     , mk $ Proxy @DebugEvaluateCondition
     , mk $ Proxy @ErrorException
     , mk $ Proxy @ErrorRewriteLoop

kore/src/Kore/Log/WarnIfLowProductivity.hs

@@ -0,0 +1,44 @@
+{- |
+Copyright   : (c) Runtime Verification, 2020
+License     : NCSA
+
+-}
+
+module Kore.Log.WarnIfLowProductivity
+    ( WarnIfLowProductivity (..)
+    , warnIfLowProductivity
+    )where
+
+import Prelude.Kore
+
+import Log
+import Numeric.Natural
+import Pretty
+    ( Pretty
+    )
+import qualified Pretty
+import Stats
+
+newtype WarnIfLowProductivity =
+    WarnIfLowProductivity { productivityPercent :: Natural }
+    deriving Show
+
+instance Pretty WarnIfLowProductivity where
+    pretty (WarnIfLowProductivity productivityPercent) =
+        Pretty.hsep
+            [ "Warning! Poor performance: productivity dropped to aprox."
+            , Pretty.pretty productivityPercent <> "%"
+            ]
+
+instance Entry WarnIfLowProductivity where
+    entrySeverity _ = Warning
+    helpDoc _ = "warn when productivty (MUT time / Total time) drops below 90%"
+
+warnIfLowProductivity :: MonadLog log => MonadIO log => log ()
+warnIfLowProductivity = do
+    Stats { gc_cpu_ns, cpu_ns } <- liftIO getStats
+    let gcTimeOver10Percent = gc_cpu_ns * 10 > cpu_ns
+        gcPercentage = gc_cpu_ns * 100 `div` cpu_ns
+        productivity = 100 - gcPercentage & fromIntegral
+    when gcTimeOver10Percent . logEntry
+        $ WarnIfLowProductivity productivity