Skip to content

Commit

Permalink
310 add optional timing to logs (#314)
Browse files Browse the repository at this point in the history 
Follows #3658
(merged, this PR updates the dependency).

Whe using `kore-rpc-booster`, all timing logs of the internal calls are
retained, and a single untagged log entry is added to indicate the
overall processing time.

Fixes #310
  • Loading branch information
@jberthold
jberthold committed Apr 10, 2024
1 parent 5d41135 commit 21db01e
Show file tree
Hide file tree
Showing 14 changed files with 309 additions and 76 deletions.
4 changes: 2 additions & 2 deletions booster/cabal.project
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ source-repository-package
source-repository-package
type: git
location: https://github.com/runtimeverification/haskell-backend.git
tag: 85b5d086840a0f1e89499f086b50d7258598fc8b
--sha256: sha256-56L7b7ZT+0UmUcuzQDmBH6naqkZm3l+9PCZuyoeTX2s=
tag: 63397c713d21322434d572281c1407d929a1189e
--sha256: sha256-HNxCf7HokEI9EHSXR4lJ2nw9yBj16iQm4/NyLKZfhOQ=
subdir: kore kore-rpc-types

2 changes: 1 addition & 1 deletion booster/deps/haskell-backend_release
View file
Original file line number Diff line number Diff line change
@@ -1 +1 @@
85b5d086840a0f1e89499f086b50d7258598fc8b
63397c713d21322434d572281c1407d929a1189e
6 changes: 3 additions & 3 deletions booster/flake.lock
View file

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

97 changes: 67 additions & 30 deletions booster/library/Booster/JsonRpc.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,16 +20,20 @@ import Control.Monad.IO.Class
import Control.Monad.Logger.CallStack (LogLevel (LevelError), MonadLoggerIO)
import Control.Monad.Logger.CallStack qualified as Log
import Control.Monad.Trans.Except (runExcept, throwE)
import Data.Bifunctor (second)
import Data.Conduit.Network (serverSettings)
import Data.Foldable
import Data.List (singleton)
import Data.Map.Strict (Map)
import Data.Map.Strict qualified as Map
import Data.Maybe (catMaybes, fromMaybe, isJust, mapMaybe)
import Data.Sequence (Seq)
import Data.Text (Text, pack)
import Data.Text qualified as Text
import Data.Text.Encoding qualified as Text
import GHC.Records
import Numeric.Natural
import System.Clock (Clock (Monotonic), diffTimeSpec, getTime, toNanoSecs)

import Booster.Definition.Attributes.Base (getUniqueId, uniqueId)
import Booster.Definition.Base (KoreDefinition (..))
Expand All @@ -55,8 +59,6 @@ import Booster.Syntax.Json.Internalise (
import Booster.Syntax.ParsedKore (parseKoreModule)
import Booster.Syntax.ParsedKore.Base
import Booster.Syntax.ParsedKore.Internalise (DefinitionError (..), addToDefinitions)
import Data.List (singleton)
import Data.Sequence (Seq)
import Kore.JsonRpc.Error qualified as RpcError
import Kore.JsonRpc.Server
import Kore.JsonRpc.Types qualified as RpcTypes
Expand All @@ -76,6 +78,7 @@ respond stateVar =
| isJust req.movingAverageStepTimeout ->
pure $ Left $ RpcError.unsupportedOption ("moving-average-step-timeout" :: String)
RpcTypes.Execute req -> withContext req._module $ \(def, mLlvmLibrary) -> do
start <- liftIO $ getTime Monotonic
-- internalise given constrained term
let internalised = runExcept $ internalisePattern DisallowAlias CheckSubsorts Nothing def req.state.term

Expand All @@ -95,7 +98,15 @@ respond stateVar =
, req.logSuccessfulSimplifications
, req.logFailedSimplifications
]
execResponse req <$> performRewrite doTracing def mLlvmLibrary mbDepth cutPoints terminals pat
result <- performRewrite doTracing def mLlvmLibrary mbDepth cutPoints terminals pat
stop <- liftIO $ getTime Monotonic
let duration =
if fromMaybe False req.logTiming
then
Just $
fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1e9
else Nothing
pure $ execResponse duration req result
RpcTypes.AddModule req -> do
-- block other request executions while modifying the server state
state <- liftIO $ takeMVar stateVar
Expand Down Expand Up @@ -126,25 +137,34 @@ respond stateVar =
"Added a new module. Now in scope: " <> Text.intercalate ", " (Map.keys newDefinitions)
pure $ Right $ RpcTypes.AddModule ()
RpcTypes.Simplify req -> withContext req._module $ \(def, mLlvmLibrary) -> do
start <- liftIO $ getTime Monotonic
let internalised =
runExcept $ internaliseTermOrPredicate DisallowAlias CheckSubsorts Nothing def req.state.term
let mkTraces
| all not . catMaybes $
[req.logSuccessfulSimplifications, req.logFailedSimplifications] =
const Nothing
| otherwise =
let mkEquationTraces
| doTracing =
Just
. mapMaybe
( mkLogEquationTrace
(fromMaybe False req.logSuccessfulSimplifications, fromMaybe False req.logFailedSimplifications)
( fromMaybe False req.logSuccessfulSimplifications
, fromMaybe False req.logFailedSimplifications
)
)
| otherwise =
const Nothing
mkTraces duration traceData
| Just True <- req.logTiming =
Just $
[ProcessingTime (Just Booster) duration]
<> fromMaybe [] (mkEquationTraces traceData)
| otherwise =
mkEquationTraces traceData
doTracing =
any
(fromMaybe False)
[ req.logSuccessfulSimplifications
, req.logFailedSimplifications
]
case internalised of
result <- case internalised of
Left patternErrors -> do
Log.logError $ "Error internalising cterm: " <> Text.pack (show patternErrors)
pure $ Left $ RpcError.backendError RpcError.CouldNotVerifyPattern patternErrors
Expand All @@ -158,18 +178,20 @@ respond stateVar =
predicate = fromMaybe (KoreJson.KJTop tSort) mbPredicate
substitution = fromMaybe (KoreJson.KJTop tSort) mbSubstitution
result = KoreJson.KJAnd tSort (KoreJson.KJAnd tSort term predicate) substitution
pure . Right . RpcTypes.Simplify $
RpcTypes.SimplifyResult
{ state = addHeader result
, logs = mkTraces patternTraces
}
-- pure . Right . RpcTypes.Simplify $
-- RpcTypes.SimplifyResult
-- { state = addHeader result
-- , logs = mkTraces patternTraces
-- }
pure $ Right (addHeader result, patternTraces)
(Left ApplyEquations.SideConditionsFalse{}, patternTraces) -> do
let tSort = fromMaybe (error "unknown sort") $ sortOfJson req.state.term
pure . Right . RpcTypes.Simplify $
RpcTypes.SimplifyResult
{ state = addHeader $ KoreJson.KJBottom tSort
, logs = mkTraces patternTraces
}
-- pure . Right . RpcTypes.Simplify $
-- RpcTypes.SimplifyResult
-- { state = addHeader $ KoreJson.KJBottom tSort
-- , logs = mkTraces patternTraces
-- }
pure $ Right (addHeader $ KoreJson.KJBottom tSort, patternTraces)
(Left (ApplyEquations.EquationLoop terms), _traces) ->
pure . Left . RpcError.backendError RpcError.Aborted $ map externaliseTerm terms -- FIXME
(Left other, _traces) ->
Expand All @@ -183,13 +205,22 @@ respond stateVar =
fromMaybe (error "not a predicate") $
sortOfJson req.state.term
result = externalisePredicate predicateSort newPred
pure . Right . RpcTypes.Simplify $
RpcTypes.SimplifyResult
{ state = addHeader result
, logs = mkTraces traces
}
-- pure . Right . RpcTypes.Simplify $
-- RpcTypes.SimplifyResult
-- { state = addHeader result
-- , logs = mkTraces traces
-- }
pure $ Right (addHeader result, traces)
(Left something, _traces) ->
pure . Left . RpcError.backendError RpcError.Aborted $ show something -- FIXME
stop <- liftIO $ getTime Monotonic

let duration =
fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1e9
mkSimplifyResponse state traceData =
RpcTypes.Simplify
RpcTypes.SimplifyResult{state, logs = mkTraces duration traceData}
pure $ second (uncurry mkSimplifyResponse) result

-- this case is only reachable if the cancel appeared as part of a batch request
RpcTypes.Cancel -> pure $ Left RpcError.cancelUnsupportedInBatchMode
Expand Down Expand Up @@ -253,10 +284,11 @@ execStateToKoreJson RpcTypes.ExecuteState{term = t, substitution, predicate} =
}

execResponse ::
Maybe Double ->
RpcTypes.ExecuteRequest ->
(Natural, Seq (RewriteTrace Pattern), RewriteResult Pattern) ->
Either ErrorObj (RpcTypes.API 'RpcTypes.Res)
execResponse req (d, traces, rr) = case rr of
execResponse mbDuration req (d, traces, rr) = case rr of
RewriteBranch p nexts ->
Right $
RpcTypes.Execute
Expand Down Expand Up @@ -342,17 +374,22 @@ execResponse req (d, traces, rr) = case rr of
depth = RpcTypes.Depth d

logs =
let ls =
let traceLogs =
fmap concat
. mapM
( mkLogRewriteTrace
(logSuccessfulRewrites, logFailedRewrites)
(logSuccessfulSimplifications, logFailedSimplifications)
)
$ toList traces
in case ls of
Just [] -> Nothing
xs -> xs
timingLog =
fmap (ProcessingTime $ Just Booster) mbDuration
in case (timingLog, traceLogs) of
(Nothing, Nothing) -> Nothing
(Nothing, Just []) -> Nothing
(Nothing, Just xs@(_ : _)) -> Just xs
(Just t, Nothing) -> Just [t]
(Just t, Just xs) -> Just (t : xs)

toExecState :: Pattern -> RpcTypes.ExecuteState
toExecState pat =
Expand Down
1 change: 1 addition & 0 deletions booster/package.yaml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,6 +65,7 @@ library:
- binary
- bytestring
- casing
- clock
- conduit
- conduit-extra
- containers
Expand Down
2 changes: 1 addition & 1 deletion booster/stack.yaml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ extra-deps:
- typerep-map-0.5.0.0
- monad-validate-1.2.0.1
- git: https://github.com/runtimeverification/haskell-backend.git
commit: 85b5d086840a0f1e89499f086b50d7258598fc8b
commit: 63397c713d21322434d572281c1407d929a1189e
subdirs:
- kore
- kore-rpc-types
Expand Down
12 changes: 6 additions & 6 deletions booster/stack.yaml.lock
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,29 +40,29 @@ packages:
original:
hackage: monad-validate-1.2.0.1
- completed:
commit: 85b5d086840a0f1e89499f086b50d7258598fc8b
commit: 63397c713d21322434d572281c1407d929a1189e
git: https://github.com/runtimeverification/haskell-backend.git
name: kore
pantry-tree:
sha256: 1fda20503a0dd9bf48a2f58ba5d228ce41d01bb72fcaa9f540b73c25292bdee8
sha256: 2e2db238551273ea69abe9022c8d05ee38a73a9653224ab872639b2ffdd13568
size: 44548
subdir: kore
version: 0.60.0.0
original:
commit: 85b5d086840a0f1e89499f086b50d7258598fc8b
commit: 63397c713d21322434d572281c1407d929a1189e
git: https://github.com/runtimeverification/haskell-backend.git
subdir: kore
- completed:
commit: 85b5d086840a0f1e89499f086b50d7258598fc8b
commit: 63397c713d21322434d572281c1407d929a1189e
git: https://github.com/runtimeverification/haskell-backend.git
name: kore-rpc-types
pantry-tree:
sha256: 08a4f20aa4664371edf1e5ca0925fdb7a704704c55fc5615b92c01f9f1d1a8dd
sha256: 3033d5c31dc212c776c9eeccd473aa0fe19c4c8c97e5a84e9719276b839f43ce
size: 475
subdir: kore-rpc-types
version: 0.60.0.0
original:
commit: 85b5d086840a0f1e89499f086b50d7258598fc8b
commit: 63397c713d21322434d572281c1407d929a1189e
git: https://github.com/runtimeverification/haskell-backend.git
subdir: kore-rpc-types
snapshots:
Expand Down
1 change: 1 addition & 0 deletions booster/test/rpc-integration/resources/logTiming.kore
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
a-to-f.kore
6 changes: 5 additions & 1 deletion booster/test/rpc-integration/runDirectoryTest.sh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -70,7 +70,11 @@ echo "Server PID ${server_pid}"

sleep 5

if [ -d $dir ]; then
if [ -d $dir ] && [ -f "${dir}/test.sh" ]; then
echo "shell-scripted test, running $dir/testsh as-is"
. ./${dir}/test.sh
elif [ -d $dir ]; then
echo "Directory test"
for test in $( ls $dir/state-*.{execute,send,simplify,add-module,get-model} 2>/dev/null ); do
tmp=${test#$dir/state-}
testname=${tmp%.*}
Expand Down
Loading

0 comments on commit 21db01e

Please sign in to comment.