Increase timestamp resolution (#3893)

This PR: - customizes the default timestamp caching mechanism provided by the `fast-logger` package, allowing finer granularity - adds `--timestamp-format` CLI argument to `booster-dev` and `kore-rpc-booster`, with two possible values: `pretty` and `nanoseconds`. `pretty` is the default. --------- Co-authored-by: Sam Balco <[email protected]>
runtimeverification · May 27, 2024 · 912cbe6 · 912cbe6
1 parent 069533c
commit 912cbe6
Show file tree

Hide file tree

Showing 5 changed files with 94 additions and 6 deletions.
diff --git a/booster/library/Booster/CLOptions.hs b/booster/library/Booster/CLOptions.hs
@@ -5,6 +5,7 @@ module Booster.CLOptions (
     CLOptions (..),
     EquationOptions (..),
     LogFormat (..),
+    TimestampFormat (..),
     clOptionsParser,
     adjustLogLevels,
     levelToContext,
@@ -40,6 +41,7 @@ data CLOptions = CLOptions
     , port :: Int
     , logLevels :: [LogLevel]
     , logTimeStamps :: Bool
+    , timeStampsFormat :: TimestampFormat
     , logFormat :: LogFormat
     , logContexts :: [ContextFilter]
     , logFile :: Maybe FilePath
@@ -63,6 +65,16 @@ instance Show LogFormat where
         Standard -> "standard"
         Json -> "json"
 
+data TimestampFormat
+    = Pretty
+    | Nanoseconds
+    deriving (Eq, Enum)
+
+instance Show TimestampFormat where
+    show = \case
+        Pretty -> "pretty"
+        Nanoseconds -> "nanoseconds"
+
 clOptionsParser :: Parser CLOptions
 clOptionsParser =
     CLOptions
@@ -104,6 +116,17 @@ clOptionsParser =
                 )
             )
         <*> switch (long "log-timestamps" <> help "Add timestamps to logs")
+        <*> option
+            (eitherReader readTimeStampFormat)
+            ( metavar "TIMESTAMPFORMAT"
+                <> value Pretty
+                <> long "timestamp-format"
+                <> help
+                    ( "Format to output log timestamps in. Available formats: "
+                        <> intercalate ", " (map show $ enumFrom (toEnum @TimestampFormat 0))
+                    )
+                <> showDefault
+            )
         <*> option
             (eitherReader readLogFormat)
             ( metavar "LOGFORMAT"
@@ -178,6 +201,12 @@ clOptionsParser =
         "json" -> Right Json
         other -> Left $ other <> ": Unsupported log format"
 
+    readTimeStampFormat :: String -> Either String TimestampFormat
+    readTimeStampFormat = \case
+        "pretty" -> Right Pretty
+        "nanoseconds" -> Right Nanoseconds
+        other -> Left $ other <> ": Unsupported timestamp format"
+
     readCellName :: String -> Either String Text
     readCellName input
         | null input =

diff --git a/booster/library/Booster/Util.hs b/booster/library/Booster/Util.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE DeriveLift #-}
+{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE PolyKinds #-}
 
 module Booster.Util (
@@ -11,18 +12,25 @@ module Booster.Util (
     constructorName,
     handleOutput,
     withFastLogger,
+    newTimeCache,
+    pattern PrettyTimestamps,
+    pattern NoPrettyTimestamps,
 ) where
 
+import Control.AutoUpdate (defaultUpdateSettings, mkAutoUpdate, updateAction, updateFreq)
 import Control.DeepSeq (NFData (..))
 import Control.Exception (bracket, catch, throwIO)
 import Control.Monad.Logger.CallStack qualified as Log
 import Data.ByteString (ByteString)
 import Data.ByteString.Char8 qualified as BS
+import Data.Coerce (coerce)
 import Data.Data
 import Data.Either (fromRight)
 import Data.Hashable (Hashable)
 import Data.Map qualified as Map
 import Data.Maybe (fromMaybe)
+import Data.Time.Clock.System (SystemTime (..), getSystemTime, systemToUTCTime)
+import Data.Time.Format
 import GHC.Generics (Generic)
 import Language.Haskell.TH.Syntax (Lift)
 import System.Directory (removeFile)
@@ -163,3 +171,35 @@ withFastLogger mFormattedTime (Just fp) log' =
         handleExists e
             | isDoesNotExistError e = return ()
             | otherwise = throwIO e
+
+{- |  Make 'IO' action which get cached formatted local time.
+Use this to avoid the cost of frequently time formatting by caching an
+auto updating formatted time, this cache update every 100 microseconds.
+
+Borrowed almost verbatim from the fast-logger package: https://hackage.haskell.org/package/fast-logger-3.2.3/docs/src/System.Log.FastLogger.Date.html#newTimeCache, but the timestamp resolution and the actions to get and format the time are tweaked.
+-}
+newTimeCache :: Flag "PrettyTimestamp" -> IO (IO FormattedTime)
+newTimeCache prettyTimestamp =
+    mkAutoUpdate
+        defaultUpdateSettings{updateFreq = 100}
+            { updateAction = formatSystemTime prettyTimestamp <$> getSystemTime
+            }
+
+pattern PrettyTimestamps, NoPrettyTimestamps :: Flag "PrettyTimestamp"
+pattern PrettyTimestamps = Flag True
+pattern NoPrettyTimestamps = Flag False
+
+-- | Format time either as a human-readable date and time or as nanoseconds
+formatSystemTime :: Flag "PrettyTimestamp" -> SystemTime -> ByteString
+formatSystemTime prettyTimestamp =
+    let formatString = BS.unpack "%Y-%m-%dT%H:%M:%S.%6Q"
+        formatter =
+            if coerce prettyTimestamp
+                then formatTime defaultTimeLocale formatString . systemToUTCTime
+                else show . toNanoSeconds
+     in BS.pack . formatter
+  where
+    toNanoSeconds :: SystemTime -> Integer
+    toNanoSeconds MkSystemTime{systemSeconds, systemNanoseconds} =
+        fromIntegral @_ @Integer systemSeconds * (10 :: Integer) ^ (9 :: Integer)
+            + fromIntegral @_ @Integer systemNanoseconds
diff --git a/booster/package.yaml b/booster/package.yaml
@@ -60,6 +60,7 @@ library:
   - aeson-pretty
   - array
   - attoparsec
+  - auto-update
   - base
   - binary
   - bytestring
@@ -98,6 +99,7 @@ library:
   - text
   - transformers
   - unix
+  - time
   - unliftio
   - unordered-containers
   source-dirs: library

diff --git a/booster/tools/booster/Server.hs b/booster/tools/booster/Server.hs
@@ -48,7 +48,6 @@ import System.Clock (
 import System.Environment qualified as Env
 import System.Exit
 import System.IO (hPutStrLn, stderr)
-import System.Log.FastLogger (newTimeCache)
 
 import Booster.CLOptions
 import Booster.Definition.Attributes.Base (
@@ -134,6 +133,7 @@ main = do
                     , logLevels
                     , logFormat
                     , logTimeStamps
+                    , timeStampsFormat
                     , logContexts
                     , logFile
                     , smtOptions
@@ -161,8 +161,12 @@ main = do
             lvl `elem` customLevels
                 || lvl >= logLevel && lvl <= LevelError
         koreSolverOptions = translateSMTOpts smtOptions
+        timestampFlag = case timeStampsFormat of
+            Pretty -> Booster.PrettyTimestamps
+            Nanoseconds -> Booster.NoPrettyTimestamps
 
-    mTimeCache <- if logTimeStamps then Just <$> (newTimeCache "%Y-%m-%d %T") else pure Nothing
+    mTimeCache <-
+        if logTimeStamps then Just <$> Booster.newTimeCache timestampFlag else pure Nothing
 
     Booster.withFastLogger mTimeCache logFile $ \stderrLogger mFileLogger -> do
         flip runLoggingT (handleOutput stderrLogger) . Logger.filterLogger levelFilter $ do

diff --git a/dev-tools/booster-dev/Server.hs b/dev-tools/booster-dev/Server.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE PatternSynonyms #-}
+
 {- |
 Copyright   : (c) Runtime Verification, 2022
 License     : BSD-3-Clause
@@ -19,7 +21,6 @@ import Data.Maybe (fromMaybe, isNothing)
 import Data.Text (Text, unpack)
 import Data.Text.Encoding qualified as Text
 import Options.Applicative
-import System.Log.FastLogger (newTimeCache)
 
 import Booster.CLOptions
 import Booster.Definition.Base (KoreDefinition (..))
@@ -33,7 +34,13 @@ import Booster.Log.Context qualified as Booster.Log
 import Booster.SMT.Interface qualified as SMT
 import Booster.Syntax.ParsedKore (loadDefinition)
 import Booster.Trace
-import Booster.Util (handleOutput, withFastLogger)
+import Booster.Util (
+    handleOutput,
+    newTimeCache,
+    withFastLogger,
+    pattern NoPrettyTimestamps,
+    pattern PrettyTimestamps,
+ )
 import Kore.JsonRpc.Error qualified as RpcError
 import Kore.JsonRpc.Server
 
@@ -47,6 +54,7 @@ main = do
             , logLevels
             , logContexts
             , logTimeStamps
+            , timeStampsFormat
             , logFormat
             , llvmLibraryFile
             , smtOptions
@@ -88,6 +96,7 @@ main = do
             (adjustLogLevels logLevels)
             logContexts
             logTimeStamps
+            timeStampsFormat
             logFormat
   where
     withLlvmLib libFile m = case libFile of
@@ -117,11 +126,15 @@ runServer ::
     (LogLevel, [LogLevel]) ->
     [Booster.Log.ContextFilter] ->
     Bool ->
+    TimestampFormat ->
     LogFormat ->
     IO ()
-runServer port definitions defaultMain mLlvmLibrary logFile mSMTOptions (logLevel, customLevels) logContexts logTimeStamps logFormat =
+runServer port definitions defaultMain mLlvmLibrary logFile mSMTOptions (logLevel, customLevels) logContexts logTimeStamps timeStampsFormat logFormat =
     do
-        mTimeCache <- if logTimeStamps then Just <$> (newTimeCache "%Y-%m-%d %T") else pure Nothing
+        let timestampFlag = case timeStampsFormat of
+                Pretty -> PrettyTimestamps
+                Nanoseconds -> NoPrettyTimestamps
+        mTimeCache <- if logTimeStamps then Just <$> newTimeCache timestampFlag else pure Nothing
 
         withFastLogger mTimeCache logFile $ \stderrLogger mFileLogger -> do
             let boosterContextLogger = case logFormat of