Browse Source

Merge pull request #303 from input-output-hk/andreas/299-liquidhaskell-verification

Code verification with LiquidHaskell
bors/trying
Alexander Diemand 3 years ago committed by GitHub
parent
commit
0967131d59
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
  1. 1
      .gitignore
  2. BIN
      docs/IOHK-Monitoring.pdf
  3. 3
      docs/references.fmt
  4. 3
      iohk-monitoring/README.md
  5. 36
      iohk-monitoring/src/Cardano/BM/Configuration/Model.lhs
  6. 26
      iohk-monitoring/src/Cardano/BM/Counters.lhs
  7. 19
      iohk-monitoring/src/Cardano/BM/Counters/Dummy.lhs
  8. 66
      iohk-monitoring/src/Cardano/BM/Data/Aggregated.lhs
  9. 31
      iohk-monitoring/src/Cardano/BM/Data/LogItem.lhs
  10. 21
      iohk-monitoring/src/Cardano/BM/Data/MessageCounter.lhs
  11. 1
      iohk-monitoring/src/Cardano/BM/Data/MonitoringEval.lhs
  12. 4
      iohk-monitoring/src/Cardano/BM/Data/SubTrace.lhs
  13. 2
      iohk-monitoring/src/Cardano/BM/Observer/Monadic.lhs
  14. 224
      iohk-monitoring/src/Cardano/BM/Output/Aggregation.lhs
  15. 3
      iohk-monitoring/src/Cardano/BM/Output/EKGView.lhs
  16. 12
      iohk-monitoring/src/Cardano/BM/Output/Editor.lhs
  17. 2
      iohk-monitoring/src/Cardano/BM/Output/Log.lhs
  18. 22
      iohk-monitoring/src/Cardano/BM/Output/Monitoring.lhs
  19. 28
      iohk-monitoring/src/Cardano/BM/Output/Switchboard.lhs
  20. 2
      iohk-monitoring/src/Cardano/BM/Tracer.lhs
  21. 55
      iohk-monitoring/test/Cardano/BM/Test/Aggregated.lhs
  22. 16
      iohk-monitoring/test/Cardano/BM/Test/Trace.lhs

1
.gitignore vendored

@ -22,6 +22,7 @@ cabal.project.local~
.HTF/
.ghc.environment.*
.DS_Store
.liquid/
docs/IOHK-Monitoring-code.idx
docs/IOHK-Monitoring-code.ilg

BIN
docs/IOHK-Monitoring.pdf

Binary file not shown.

3
docs/references.fmt

@ -47,7 +47,6 @@
%format shutdown = "\hyperref[code:shutdown]{shutdown}"
%format withTrace = "\hyperref[code:withTrace]{withTrace}"
%format Cardano.BM.Counters = "\hyperref[code:Cardano.BM.Counters]{Cardano.BM.Counters}"
%format diffTimeObserved = "\hyperref[code:diffTimeObserved]{diffTimeObserved}"
%format Cardano.BM.Counters.Common = "\hyperref[code:Cardano.BM.Counters.Common]{Cardano.BM.Counters.Common}"
%format nominalTimeToMicroseconds = "\hyperref[code:nominalTimeToMicroseconds]{nominalTimeToMicroseconds}"
%format getMonoClock = "\hyperref[code:getMonoClock]{getMonoClock}"
@ -162,13 +161,13 @@
%format toObject = "\hyperref[code:toObject]{toObject}"
%format Cardano.BM.Configuration = "\hyperref[code:Cardano.BM.Configuration]{Cardano.BM.Configuration}"
%format getOptionOrDefault = "\hyperref[code:getOptionOrDefault]{getOptionOrDefault}"
%format testSubTrace = "\hyperref[code:testSubTrace]{testSubTrace}"
%format testSeverity = "\hyperref[code:testSeverity]{testSeverity}"
%format Cardano.BM.Configuration.Model = "\hyperref[code:Cardano.BM.Configuration.Model]{Cardano.BM.Configuration.Model}"
%format Configuration = "\hyperref[code:Configuration]{Configuration}"
%format setSubTrace = "\hyperref[code:setSubTrace]{setSubTrace}"
%format toRepresentation = "\hyperref[code:toRepresentation]{toRepresentation}"
%format exportConfiguration = "\hyperref[code:exportConfiguration]{exportConfiguration}"
%format testSubTrace = "\hyperref[code:testSubTrace]{testSubTrace}"
%format Cardano.BM.Configuration.Static = "\hyperref[code:Cardano.BM.Configuration.Static]{Cardano.BM.Configuration.Static}"
%format Cardano.BM.Output.Switchboard = "\hyperref[code:Cardano.BM.Output.Switchboard]{Cardano.BM.Output.Switchboard}"
%format Switchboard = "\hyperref[code:Switchboard]{Switchboard}"

3
iohk-monitoring/README.md

@ -9,7 +9,7 @@ This framework provides logging, benchmarking and monitoring.
Documentation of the [source code and tests](docs/IOHK-Monitoring.pdf) in PDF format. Please, download the PDF file and open in external viewer. It contains links that make it easy to navigate in the source code. Those links are not active in the online viewer.
View our first presentation (2018-12-04) on this subject in [html](https://input-output-hk.github.io/iohk-monitoring-framework/pres-20181204/html/index.html)
Presentations and more documentation is available from our [docs](https://input-output-hk.github.io/iohk-monitoring-framework/) section.
## module dependencies
@ -36,3 +36,4 @@ These showcase the usage of this framework in an application. The *complex* exam
* `cabal new-build` and `cabal new-test`
* `ghcid -c "cabal new-repl"` watches for file changes and recompiles them immediately
* `liquid --ghc-option=-XOverloadedStrings --prune-unsorted src/Cardano/BM/*.lhs` verify top modules in iohk-monitoring using LiquidHaskell

36
iohk-monitoring/src/Cardano/BM/Configuration/Model.lhs

@ -8,6 +8,8 @@
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-@ LIQUID "--max-case-expand=4" @-}
#if defined(linux_HOST_OS)
#define LINUX
#endif
@ -72,7 +74,7 @@ import Cardano.BM.Data.AggregatedKind (AggregatedKind(..))
import Cardano.BM.Data.BackendKind
import qualified Cardano.BM.Data.Configuration as R
import Cardano.BM.Data.LogItem (LogObject (..), LoggerName, LOContent (..), severity)
import Cardano.BM.Data.MonitoringEval (MEvAction, MEvExpr, MEvPreCond)
import Cardano.BM.Data.MonitoringEval (MEvExpr, MEvPreCond, MEvAction)
import Cardano.BM.Data.Output (ScribeDefinition (..), ScribeId,
ScribeKind (..))
import Cardano.BM.Data.Rotation (RotationParameters (..))
@ -193,29 +195,21 @@ getScribes configuration name = do
(updateCache, scribes) <- do
let defs = cgDefScribes cg
let mapscribes = cgMapScribe cg
let find_s lname = case HM.lookup lname mapscribes of
Nothing ->
case dropToDot lname of
Nothing -> defs
Just lname' -> find_s lname'
let find_s [] = defs
find_s lnames = case HM.lookup (T.intercalate "." lnames) mapscribes of
Nothing -> find_s (init lnames)
Just os -> os
let outs = HM.lookup name (cgMapScribeCache cg)
-- look if scribes are already cached
return $ case outs of
-- if no cached scribes found; search the appropriate scribes that
-- they must inherit and update the cached map
Nothing -> (True, find_s name)
Nothing -> (True, find_s $ T.split (=='.') name)
Just os -> (False, os)
when updateCache $ setCachedScribes configuration name $ Just scribes
return scribes
dropToDot :: Text -> Maybe Text
dropToDot ts = dropToDot' (T.breakOnEnd "." ts)
where
dropToDot' (_,"") = Nothing
dropToDot' (name',_) = Just $ T.dropWhileEnd (=='.') name'
getCachedScribes :: Configuration -> LoggerName -> IO (Maybe [ScribeId])
getCachedScribes configuration name = do
cg <- readMVar $ getCG configuration
@ -617,16 +611,14 @@ the evaluation of the filters return |True|.
\begin{code}
findRootSubTrace :: Configuration -> LoggerName -> IO (Maybe SubTrace)
findRootSubTrace config loggername = do
findRootSubTrace config loggername =
-- Try to find SubTrace by provided name.
findSubTrace config loggername >>= \case
Just subtrace -> return $ Just subtrace -- Ok, found, provide it as it is.
Nothing ->
-- We didn't find it, so drop the child (from the right side)
-- and try to find it again.
case dropToDot loggername of
Nothing -> return Nothing -- was at root
Just parentName -> findRootSubTrace config parentName
let find_s :: [Text] -> IO (Maybe SubTrace)
find_s [] = return Nothing
find_s lnames = findSubTrace config (T.intercalate "." lnames) >>= \case
Just subtrace -> return $ Just subtrace
Nothing -> find_s (init lnames)
in find_s $ T.split (=='.') loggername
testSubTrace :: Configuration -> LoggerName -> LogObject a -> IO (Maybe (LogObject a))
testSubTrace config loggername lo = do

26
iohk-monitoring/src/Cardano/BM/Counters.lhs

@ -16,7 +16,6 @@ Currently, we mainly support |Linux| with its 'proc' filesystem.
module Cardano.BM.Counters
(
Platform.readCounters
, diffTimeObserved
, getMonoClock
) where
@ -27,30 +26,5 @@ import qualified Cardano.BM.Counters.Dummy as Platform
#endif
import Cardano.BM.Counters.Common (getMonoClock)
import Cardano.BM.Data.Aggregated (Measurable (..))
import Cardano.BM.Data.Counter
\end{code}
\subsubsection{Calculate difference between clocks}\label{code:diffTimeObserved}\index{diffTimeObserved}
\begin{code}
diffTimeObserved :: CounterState -> CounterState -> Measurable
diffTimeObserved (CounterState id0 startCounters) (CounterState id1 endCounters) =
let
startTime = getMonotonicTime startCounters
endTime = getMonotonicTime endCounters
in
if (id0 == id1)
then endTime - startTime
else error "these clocks are not from the same experiment"
where
getMonotonicTime counters = case (filter isMonotonicClockCounter counters) of
[(Counter MonotonicClockTime _ mus)] -> mus
_ -> error "A time measurement is missing!"
isMonotonicClockCounter :: Counter -> Bool
isMonotonicClockCounter = (MonotonicClockTime ==) . cType
\end{code}

19
iohk-monitoring/src/Cardano/BM/Counters/Dummy.lhs

@ -16,7 +16,6 @@ module Cardano.BM.Counters.Dummy
) where
#ifdef ENABLE_OBSERVABLES
import Data.Foldable (foldrM)
import Cardano.BM.Counters.Common (getMonoClock, readRTSStats)
import Cardano.BM.Data.Observable
#endif
@ -34,16 +33,16 @@ readCounters (TeeTrace _) = return []
readCounters (FilterTrace _) = return []
readCounters UntimedTrace = return []
readCounters DropOpening = return []
readCounters (SetSeverity _) = return []
#ifdef ENABLE_OBSERVABLES
readCounters (ObservableTrace tts) = foldrM (\(sel, fun) a ->
if any (== sel) tts
then (fun >>= \xs -> return $ a ++ xs)
else return a) [] selectors
where
selectors = [ (MonotonicClock, getMonoClock)
, (GhcRtsStats, readRTSStats)
]
readCounters (ObservableTrace tts) = readCounters' tts []
readCounters' :: [ObservableInstance] -> [Counter] -> IO [Counter]
readCounters' [] acc = return acc
readCounters' (MonotonicClock : r) acc = getMonoClock >>= \xs -> readCounters' r $ acc ++ xs
readCounters' (GhcRtsStats : r) acc = readRTSStats >>= \xs -> readCounters' r $ acc ++ xs
readCounters' (_ : r) acc = readCounters' r acc
#else
readCounters (ObservableTrace _) = return []
#endif
\end{code}
\end{code}

66
iohk-monitoring/src/Cardano/BM/Data/Aggregated.lhs

@ -18,6 +18,7 @@ module Cardano.BM.Data.Aggregated
, showUnits
, getInteger
, getDouble
, subtractMeasurable
, meanOfStats
, stdevOfStats
, stats2Text
@ -45,8 +46,8 @@ data Measurable = Microseconds {-# UNPACK #-} !Word64
| Nanoseconds {-# UNPACK #-} !Word64
| Seconds {-# UNPACK #-} !Word64
| Bytes {-# UNPACK #-} !Word64
| PureD Double
| PureI Integer
| PureD !Double
| PureI !Integer
| Severity S.Severity
deriving (Eq, Read, Generic, ToJSON)
@ -58,12 +59,12 @@ instance Ord Measurable where
compare (Seconds a) (Seconds b) = compare a b
compare (Microseconds a) (Microseconds b) = compare a b
compare (Nanoseconds a) (Nanoseconds b) = compare a b
compare (Seconds a) (Microseconds b) = compare (a * 1000000) b
compare (Seconds a) (Microseconds b) = compare (a * 1000 * 1000) b
compare (Nanoseconds a) (Microseconds b) = compare a (b * 1000)
compare (Seconds a) (Nanoseconds b) = compare (a * 1000000000) b
compare (Seconds a) (Nanoseconds b) = compare (a * 1000* 1000 * 1000) b
compare (Microseconds a) (Nanoseconds b) = compare (a * 1000) b
compare (Microseconds a) (Seconds b) = compare a (b * 1000000)
compare (Nanoseconds a) (Seconds b) = compare a (b * 1000000000)
compare (Microseconds a) (Seconds b) = compare a (b * 1000 * 1000)
compare (Nanoseconds a) (Seconds b) = compare a (b * 1000 * 1000 * 1000)
compare (Bytes a) (Bytes b) = compare a b
compare (PureD a) (PureD b) = compare a b
compare (PureI a) (PureI b) = compare a b
@ -78,7 +79,7 @@ instance Ord Measurable where
compare (Bytes a) (PureI b) | b >= 0 = compare (toInteger a) b
compare a@(PureD _) (PureI b) = compare (getInteger a) b
compare (PureI a) b@(PureD _) = compare a (getInteger b)
compare a b = error $ "cannot compare " ++ (showType a) ++ " " ++ (show a) ++ " against this value: " ++ (showType b) ++ " " ++ (show b)
compare _a _b = LT
\end{code}
@ -118,7 +119,7 @@ instance Num Measurable where
(+) (Bytes a) (Bytes b) = Bytes (a+b)
(+) (PureI a) (PureI b) = PureI (a+b)
(+) (PureD a) (PureD b) = PureD (a+b)
(+) _ _ = error "Trying to add values with different units"
(+) a _ = a
(*) (Microseconds a) (Microseconds b) = Microseconds (a*b)
(*) (Nanoseconds a) (Nanoseconds b) = Nanoseconds (a*b)
@ -126,7 +127,7 @@ instance Num Measurable where
(*) (Bytes a) (Bytes b) = Bytes (a*b)
(*) (PureI a) (PureI b) = PureI (a*b)
(*) (PureD a) (PureD b) = PureD (a*b)
(*) _ _ = error "Trying to multiply values with different units"
(*) a _ = a
abs (Microseconds a) = Microseconds (abs a)
abs (Nanoseconds a) = Nanoseconds (abs a)
@ -134,7 +135,7 @@ instance Num Measurable where
abs (Bytes a) = Bytes (abs a)
abs (PureI a) = PureI (abs a)
abs (PureD a) = PureD (abs a)
abs (Severity _) = error "cannot compute absolute value for Severity"
abs a = a
signum (Microseconds a) = Microseconds (signum a)
signum (Nanoseconds a) = Nanoseconds (signum a)
@ -142,7 +143,7 @@ instance Num Measurable where
signum (Bytes a) = Bytes (signum a)
signum (PureI a) = PureI (signum a)
signum (PureD a) = PureD (signum a)
signum (Severity _) = error "cannot compute sign of Severity"
signum a = a
negate (Microseconds a) = Microseconds (negate a)
negate (Nanoseconds a) = Nanoseconds (negate a)
@ -150,10 +151,18 @@ instance Num Measurable where
negate (Bytes a) = Bytes (negate a)
negate (PureI a) = PureI (negate a)
negate (PureD a) = PureD (negate a)
negate (Severity _) = error "cannot negate Severity"
negate a = a
fromInteger = PureI
subtractMeasurable :: Measurable -> Measurable -> Measurable
subtractMeasurable (Microseconds a) (Microseconds b) = Microseconds (a-b)
subtractMeasurable (Nanoseconds a) (Nanoseconds b) = Nanoseconds (a-b)
subtractMeasurable (Seconds a) (Seconds b) = Seconds (a-b)
subtractMeasurable (Bytes a) (Bytes b) = Bytes (a-b)
subtractMeasurable (PureI a) (PureI b) = PureI (a-b)
subtractMeasurable (PureD a) (PureD b) = PureD (a-b)
subtractMeasurable a _ = a
\end{code}
Pretty printing of |Measurable|. \index{Measurable!instance of Show}
@ -176,20 +185,11 @@ showUnits (PureI _) = ""
showUnits (PureD _) = ""
showUnits (Severity _) = ""
showType :: Measurable -> String
showType (Microseconds _) = "Microseconds"
showType (Nanoseconds _) = "Nanoseconds"
showType (Seconds _) = "Seconds"
showType (Bytes _) = "Bytes"
showType (PureI _) = "PureI"
showType (PureD _) = "PureD"
showType (Severity _) = "Severity"
-- show in S.I. units
showSI :: Measurable -> String
showSI (Microseconds a) = show (fromFloatDigits ((fromIntegral a) / (1000000::Float))) ++
showSI (Microseconds a) = show (fromFloatDigits ((fromIntegral a) / (1000::Float) / (1000::Float))) ++
showUnits (Seconds a)
showSI (Nanoseconds a) = show (fromFloatDigits ((fromIntegral a) / (1000000000::Float))) ++
showSI (Nanoseconds a) = show (fromFloatDigits ((fromIntegral a) / (1000::Float) / (1000::Float) / (1000::Float))) ++
showUnits (Seconds a)
showSI v@(Seconds a) = show a ++ showUnits v
showSI v@(Bytes a) = show a ++ showUnits v
@ -205,7 +205,7 @@ A |Stats| statistics is strictly computed.
data BaseStats = BaseStats {
fmin :: !Measurable,
fmax :: !Measurable,
fcount :: {-# UNPACK #-} !Int,
fcount :: {-# UNPACK #-} !Word64,
fsum_A :: {-# UNPACK #-} !Double,
fsum_B :: {-# UNPACK #-} !Double
} deriving (Generic, ToJSON, Show)
@ -235,9 +235,13 @@ meanOfStats = fsum_A
\begin{code}
stdevOfStats :: BaseStats -> Double
stdevOfStats s =
if fcount s < 2
then 0
else sqrt $ (fsum_B s) / (fromInteger $ fromIntegral (fcount s) - 1)
calculate (fcount s)
where
calculate :: Word64 -> Double
calculate n =
if n >= 2
then sqrt $ (fsum_B s) / (fromInteger $ fromIntegral (n - 1))
else 0
\end{code}
@ -318,7 +322,7 @@ data Aggregated = AggregatedStats Stats
instance Semigroup Aggregated where
(<>) (AggregatedStats a) (AggregatedStats b) =
AggregatedStats (a <> b)
(<>) _ _ = error "Cannot combine different objects"
(<>) a _ = a
\end{spec}
@ -337,13 +341,13 @@ singletonStats a =
, fdelta = BaseStats
{ fmin = 0
, fmax = 0
, fcount = 0
, fcount = 1
, fsum_A = 0
, fsum_B = 0 }
, ftimed = BaseStats
{ fmin = Nanoseconds 999999999999
{ fmin = Nanoseconds 0
, fmax = Nanoseconds 0
, fcount = (-1)
, fcount = 1
, fsum_A = 0
, fsum_B = 0 }
}

31
iohk-monitoring/src/Cardano/BM/Data/LogItem.lhs

@ -12,6 +12,7 @@
module Cardano.BM.Data.LogItem
( LogObject (..)
, loType
, loType2Name
, LOMeta (..), mkLOMeta
, LOContent (..)
, CommandValue (..)
@ -98,6 +99,7 @@ data MonitorAction = MonitorAlert Text
\end{code}
\label{code:LogMessage}\index{LogMessage}
\label{code:LogError}\index{LogError}
\label{code:LogValue}\index{LogValue}
\label{code:ObserveOpen}\index{ObserveOpen}
\label{code:ObserveDiff}\index{ObserveDiff}
@ -109,6 +111,7 @@ data MonitorAction = MonitorAlert Text
Payload of a |LogObject|:
\begin{code}
data LOContent a = LogMessage a
| LogError Text
| LogValue Text Measurable
| ObserveOpen CounterState
| ObserveDiff CounterState
@ -120,16 +123,24 @@ data LOContent a = LogMessage a
deriving (Generic, Show, ToJSON)
loType :: LogObject a -> Text
loType = \case
LogObject _ _ (LogMessage _) -> "LogMessage"
LogObject _ _ (LogValue _ _) -> "LogValue"
LogObject _ _ (ObserveOpen _) -> "ObserveOpen"
LogObject _ _ (ObserveDiff _) -> "ObserveDiff"
LogObject _ _ (ObserveClose _) -> "ObserveClose"
LogObject _ _ (AggregatedMessage _) -> "AggregatedMessage"
LogObject _ _ (MonitoringEffect _) -> "MonitoringEffect"
LogObject _ _ (Command _) -> "Command"
LogObject _ _ KillPill -> "KillPill"
loType (LogObject _ _ content) = loType2Name content
\end{code}
Name of a message content type
\begin{code}
loType2Name :: LOContent a -> Text
loType2Name = \case
LogMessage _ -> "LogMessage"
LogError _ -> "LogError"
LogValue _ _ -> "LogValue"
ObserveOpen _ -> "ObserveOpen"
ObserveDiff _ -> "ObserveDiff"
ObserveClose _ -> "ObserveClose"
AggregatedMessage _ -> "AggregatedMessage"
MonitoringEffect _ -> "MonitoringEffect"
Command _ -> "Command"
KillPill -> "KillPill"
\end{code}

21
iohk-monitoring/src/Cardano/BM/Data/MessageCounter.lhs

@ -5,7 +5,6 @@
%if style == newcode
\begin{code}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE LambdaCase #-}
module Cardano.BM.Data.MessageCounter
( MessageCounter (..)
@ -27,7 +26,7 @@ import Data.Word (Word64)
import Cardano.BM.Data.Aggregated (Measurable (PureI))
import Cardano.BM.Data.LogItem (LoggerName, LOContent (..),
LOMeta(..), LogObject(..), PrivacyAnnotation(Confidential),
mkLOMeta)
loType2Name, mkLOMeta)
import Cardano.BM.Data.Severity (Severity (..))
import Cardano.BM.Data.Trace
import qualified Cardano.BM.Trace as Trace
@ -51,7 +50,7 @@ Update counter for specific severity and type of message.
updateMessageCounters :: MessageCounter -> LogObject a -> MessageCounter
updateMessageCounters mc (LogObject _ meta content) =
let sev = pack $ show $ severity meta
messageType = lotype2name content
messageType = loType2Name content
increasedCounter key cmap =
case HM.lookup key cmap of
Nothing -> 1 :: Word64
@ -66,22 +65,6 @@ updateMessageCounters mc (LogObject _ meta content) =
\end{code}
Name of a message content type
\begin{code}
lotype2name :: LOContent a -> Text
lotype2name = \case
LogMessage _ -> "LogMessage"
LogValue _ _ -> "LogValue"
ObserveOpen _ -> "ObserveOpen"
ObserveDiff _ -> "ObserveDiff"
ObserveClose _ -> "ObserveClose"
AggregatedMessage _ -> "AggregatedMessage"
MonitoringEffect _ -> "MonitoringEffect"
Command _ -> "Command"
KillPill -> "KillPill"
\end{code}
\subsubsection{Reset counters}
Reset counters.
\begin{code}

1
iohk-monitoring/src/Cardano/BM/Data/MonitoringEval.lhs

@ -170,6 +170,7 @@ parseEitherAction t =
An expression is enclosed in parentheses. Either it is a negation, starting with 'Not',
or a binary operand like 'And', 'Or', or a comparison of a named variable.
\begin{code}
{-@ lazy parseExpr @-}
parseExpr :: P.Parser MEvExpr
parseExpr = do
openPar

4
iohk-monitoring/src/Cardano/BM/Data/SubTrace.lhs

@ -17,7 +17,7 @@ module Cardano.BM.Data.SubTrace
where
import Data.Aeson (FromJSON (..), ToJSON (..), Value (..), (.:), (.=), object, withObject)
import Data.Text (Text)
import Data.Text (Text, unpack)
import Cardano.BM.Data.LogItem (LoggerName)
import Cardano.BM.Data.Observable
@ -69,7 +69,7 @@ instance FromJSON SubTrace where
"DropOpening" -> return $ DropOpening
"ObservableTrace" -> ObservableTrace <$> o .: "contents"
"SetSeverity" -> SetSeverity <$> o .: "contents"
_ -> error "cannot parse such an expression!"
other -> fail $ "unexpected subtrace: " ++ (unpack other)
instance ToJSON SubTrace where
toJSON Neutral = object ["subtrace" .= String "Neutral" ]

2
iohk-monitoring/src/Cardano/BM/Observer/Monadic.lhs

@ -7,6 +7,8 @@
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-@ LIQUID "--prune-unsorted" @-}
module Cardano.BM.Observer.Monadic
(
bracketObserveIO

224
iohk-monitoring/src/Cardano/BM/Output/Aggregation.lhs

@ -4,9 +4,12 @@
%if style == newcode
\begin{code}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-@ embed GHC.Natural.Natural as int @-}
module Cardano.BM.Output.Aggregation
(
Aggregation
@ -28,7 +31,7 @@ import qualified Data.HashMap.Strict as HM
import Data.Text (Text, pack)
import qualified Data.Text.IO as TIO
import Data.Time.Calendar (toModifiedJulianDay)
import Data.Time.Clock (UTCTime (..), getCurrentTime)
import Data.Time.Clock (UTCTime (..), diffTimeToPicoseconds, getCurrentTime)
import Data.Word (Word64)
import GHC.Clock (getMonotonicTimeNSec)
import System.IO (stderr)
@ -36,7 +39,7 @@ import System.IO (stderr)
import Cardano.BM.Configuration.Model (Configuration, getAggregatedKind)
import Cardano.BM.Data.Aggregated (Aggregated (..), BaseStats (..),
EWMA (..), Measurable (..), Stats (..), getDouble,
singletonStats)
getInteger, singletonStats, subtractMeasurable)
import Cardano.BM.Data.AggregatedKind (AggregatedKind (..))
import Cardano.BM.Data.Backend
import Cardano.BM.Data.Counter (Counter (..), CounterState (..),
@ -78,7 +81,7 @@ type Timestamp = Word64
data AggregatedExpanded = AggregatedExpanded
{ aeAggregated :: !Aggregated
, aeResetAfter :: !(Maybe Int)
, aeResetAfter :: !(Maybe Word64)
, aeLastSent :: {-# UNPACK #-} !Timestamp
}
@ -107,7 +110,7 @@ instance IsEffectuator Aggregation a where
instance IsBackend Aggregation a where
typeof _ = AggregationBK
realize _ = error "Aggregation cannot be instantiated by 'realize'"
realize _ = fail "Aggregation cannot be instantiated by 'realize'"
realizefrom config trace _ = do
aggref <- newEmptyMVar
@ -158,11 +161,12 @@ spawnDispatcher conf aggMap aggregationQueue basetrace = do
Async.async $ qProc trace countersMVar aggMap
where
{-@ lazy qProc @-}
qProc trace counters aggregatedMap = do
maybeItem <- atomically $ TBQ.readTBQueue aggregationQueue
case maybeItem of
Just (lo@(LogObject logname lm _)) -> do
(updatedMap, aggregations) <- update lo aggregatedMap
(updatedMap, aggregations) <- update lo aggregatedMap trace
unless (null aggregations) $
sendAggregated trace (LogObject logname lm (AggregatedMessage aggregations))
-- increase the counter for the specific severity and message type
@ -170,81 +174,107 @@ spawnDispatcher conf aggMap aggregationQueue basetrace = do
qProc trace counters updatedMap
Nothing -> return ()
createNupdate :: Text -> Measurable -> LOMeta -> AggregationMap -> IO (Either Text Aggregated)
createNupdate name value lme agmap = do
case HM.lookup name agmap of
Nothing -> do
-- if Aggregated does not exist; initialize it.
aggregatedKind <- getAggregatedKind conf name
case aggregatedKind of
StatsAK -> return $ singletonStats value
StatsAK -> return $ Right $ singletonStats value
EwmaAK aEWMA -> do
let initEWMA = EmptyEWMA aEWMA
return $ AggregatedEWMA $ ewma initEWMA value
return $ AggregatedEWMA <$> ewma initEWMA value
Just a -> return $ updateAggregation value (aeAggregated a) lme (aeResetAfter a)
update :: LogObject a
-> AggregationMap
-> Trace.Trace IO a
-> IO (AggregationMap, [(Text, Aggregated)])
update (LogObject logname lme (LogValue iname value)) agmap = do
update (LogObject logname lme (LogValue iname value)) agmap trace = do
let fullname = logname <> "." <> iname
aggregated <- createNupdate fullname value lme agmap
now <- getMonotonicTimeNSec
let aggregatedX = AggregatedExpanded {
aeAggregated = aggregated
, aeResetAfter = Nothing
, aeLastSent = now
}
namedAggregated = [(iname, aeAggregated aggregatedX)]
updatedMap = HM.alter (const $ Just $ aggregatedX) fullname agmap
return (updatedMap, namedAggregated)
update (LogObject logname lme (ObserveDiff counterState)) agmap =
updateCounters (csCounters counterState) lme (logname, "diff") agmap []
update (LogObject logname lme (ObserveOpen counterState)) agmap =
updateCounters (csCounters counterState) lme (logname, "open") agmap []
update (LogObject logname lme (ObserveClose counterState)) agmap =
updateCounters (csCounters counterState) lme (logname, "close") agmap []
update (LogObject logname lme (LogMessage _)) agmap = do
eitherAggregated <- createNupdate fullname value lme agmap
case eitherAggregated of
Right aggregated -> do
now <- getMonotonicTimeNSec
let aggregatedX = AggregatedExpanded {
aeAggregated = aggregated
, aeResetAfter = Nothing
, aeLastSent = now
}
namedAggregated = [(iname, aeAggregated aggregatedX)]
updatedMap = HM.alter (const $ Just $ aggregatedX) fullname agmap
return (updatedMap, namedAggregated)
Left w -> do
trace' <- Trace.appendName "update" trace
Trace.traceNamedObject trace' =<<
(,) <$> liftIO (mkLOMeta Warning Public)
<*> pure (LogError w)
return (agmap, [])
update (LogObject logname lme (ObserveDiff counterState)) agmap trace =
updateCounters (csCounters counterState) lme (logname, "diff") agmap [] trace
update (LogObject logname lme (ObserveOpen counterState)) agmap trace =
updateCounters (csCounters counterState) lme (logname, "open") agmap [] trace
update (LogObject logname lme (ObserveClose counterState)) agmap trace =
updateCounters (csCounters counterState) lme (logname, "close") agmap [] trace
update (LogObject logname lme (LogMessage _)) agmap trace = do
let iname = pack $ show (severity lme)
let fullname = logname <> "." <> iname
aggregated <- createNupdate fullname (PureI 0) lme agmap
now <- getMonotonicTimeNSec
let aggregatedX = AggregatedExpanded {
aeAggregated = aggregated
, aeResetAfter = Nothing
, aeLastSent = now
}
namedAggregated = [(iname, aeAggregated aggregatedX)]
updatedMap = HM.alter (const $ Just $ aggregatedX) fullname agmap
return (updatedMap, namedAggregated)
eitherAggregated <- createNupdate fullname (PureI 0) lme agmap
case eitherAggregated of
Right aggregated -> do
now <- getMonotonicTimeNSec
let aggregatedX = AggregatedExpanded {
aeAggregated = aggregated
, aeResetAfter = Nothing
, aeLastSent = now
}
namedAggregated = [(iname, aeAggregated aggregatedX)]
updatedMap = HM.alter (const $ Just $ aggregatedX) fullname agmap
return (updatedMap, namedAggregated)
Left w -> do
trace' <- Trace.appendName "update" trace
Trace.traceNamedObject trace' =<<
(,) <$> liftIO (mkLOMeta Warning Public)
<*> pure (LogError w)
return (agmap, [])
-- everything else
update _ agmap = return (agmap, [])
update _ agmap _ = return (agmap, [])
updateCounters :: [Counter]
-> LOMeta
-> (LoggerName,LoggerName)
-> AggregationMap
-> [(Text, Aggregated)]
-> Trace.Trace IO a
-> IO (AggregationMap, [(Text, Aggregated)])
updateCounters [] _ _ aggrMap aggs = return $ (aggrMap, aggs)
updateCounters (counter : cs) lme (logname, msgname) aggrMap aggs = do
updateCounters [] _ _ aggrMap aggs _ = return $ (aggrMap, aggs)
updateCounters (counter : cs) lme (logname, msgname) aggrMap aggs trace = do
let name = cName counter
subname = msgname <> "." <> (nameCounter counter) <> "." <> name
fullname = logname <> "." <> subname
value = cValue counter
aggregated <- createNupdate fullname value lme aggrMap
now <- getMonotonicTimeNSec
let aggregatedX = AggregatedExpanded {
aeAggregated = aggregated
, aeResetAfter = Nothing
, aeLastSent = now
}
namedAggregated = (subname, aggregated)
updatedMap = HM.alter (const $ Just $ aggregatedX) fullname aggrMap
updateCounters cs lme (logname, msgname) updatedMap (namedAggregated : aggs)
eitherAggregated <- createNupdate fullname value lme aggrMap
case eitherAggregated of
Right aggregated -> do
now <- getMonotonicTimeNSec
let aggregatedX = AggregatedExpanded {
aeAggregated = aggregated
, aeResetAfter = Nothing
, aeLastSent = now
}
namedAggregated = (subname, aggregated)
updatedMap = HM.alter (const $ Just $ aggregatedX) fullname aggrMap
updateCounters cs lme (logname, msgname) updatedMap (namedAggregated : aggs) trace
Left w -> do
trace' <- Trace.appendName "updateCounters" trace
Trace.traceNamedObject trace' =<<
(,) <$> liftIO (mkLOMeta Warning Public)
<*> pure (LogError w)
updateCounters cs lme (logname, msgname) aggrMap aggs trace
sendAggregated :: Trace.Trace IO a -> LogObject a -> IO ()
sendAggregated trace (LogObject logname meta v@(AggregatedMessage _)) = do
@ -263,50 +293,62 @@ We use Welford's online algorithm to update the estimation of mean and variance
(see \url{https://en.wikipedia.org/wiki/Algorithms_for_calculating_variance#Welford's_Online_algorithm})
\begin{code}
updateAggregation :: Measurable -> Aggregated -> LOMeta -> Maybe Int -> Aggregated
updateAggregation :: Measurable -> Aggregated -> LOMeta -> Maybe Word64 -> Either Text Aggregated
updateAggregation v (AggregatedStats s) lme resetAfter =
let count = fcount (fbasic s)
reset = maybe False (count >=) resetAfter
in
if reset
then
singletonStats v
Right $ singletonStats v
else
AggregatedStats $! Stats { flast = v
, fold = mkTimestamp
, fbasic = updateBaseStats (count >= 1) v (fbasic s)
, fdelta = updateBaseStats (count >= 2) (v - flast s) (fdelta s)
, ftimed = updateBaseStats (count >= 2) (mkTimestamp - fold s) (ftimed s)
}
Right $ AggregatedStats $! Stats { flast = v
, fold = mkTimestamp
, fbasic = updateBaseStats 1 v (fbasic s)
, fdelta = updateBaseStats 2 deltav (fdelta s)
, ftimed = updateBaseStats 2 timediff (ftimed s)
}
where
deltav = subtractMeasurable v (flast s)
mkTimestamp = utc2ns (tstamp lme)
timediff = Nanoseconds $ fromInteger $ (getInteger mkTimestamp) - (getInteger $ fold s)
utc2ns (UTCTime days secs) =
let yearsecs :: Rational
yearsecs = 365 * 24 * 3600
rdays,rsecs :: Rational
rdays = toRational $ toModifiedJulianDay days
rsecs = toRational secs
s2ns = 1000000000
let daysecs = 24 * 3600
rdays,rsecs :: Integer
rdays = toModifiedJulianDay days
rsecs = diffTimeToPicoseconds secs `div` 1000
s2ns = 1000*1000*1000
ns = rsecs + s2ns * rdays * daysecs
in
Nanoseconds $ round $ (fromRational $ s2ns * rsecs + rdays * yearsecs :: Double)
updateAggregation v (AggregatedEWMA e) _ _ = AggregatedEWMA $! ewma e v
updateBaseStats :: Bool -> Measurable -> BaseStats -> BaseStats
updateBaseStats False _ s = s {fcount = fcount s + 1}
updateBaseStats True v s =
let newcount = fcount s + 1
newvalue = getDouble v
delta = newvalue - fsum_A s
dincr = (delta / fromIntegral newcount)
delta2 = newvalue - fsum_A s - dincr
Nanoseconds $ fromInteger ns
updateAggregation v (AggregatedEWMA e) _ _ =
let !eitherAvg = ewma e v
in
BaseStats { fmin = min (fmin s) v
, fmax = max v (fmax s)
, fcount = newcount
, fsum_A = fsum_A s + dincr
, fsum_B = fsum_B s + (delta * delta2)
}
AggregatedEWMA <$> eitherAvg
updateBaseStats :: Word64 -> Measurable -> BaseStats -> BaseStats
updateBaseStats startAt v s =
let newcount = fcount s + 1 in
if (startAt > newcount)
then s {fcount = fcount s + 1}
else
let newcountRel = newcount - startAt + 1
newvalue = getDouble v
delta = newvalue - fsum_A s
dincr = (delta / fromIntegral newcountRel)
delta2 = newvalue - fsum_A s - dincr
(minim, maxim) =
if startAt == newcount
then (v, v)
else (min v (fmin s), max v (fmax s))
in
BaseStats { fmin = minim
, fmax = maxim
, fcount = newcount
, fsum_A = fsum_A s + dincr
, fsum_B = fsum_B s + (delta * delta2)
}
\end{code}
@ -325,18 +367,18 @@ $$
The pattern matching below ensures that the |EWMA| will start with the first value passed in,
and will not change type, once determined.
\begin{code}
ewma :: EWMA -> Measurable -> EWMA
ewma (EmptyEWMA a) v = EWMA a v
ewma :: EWMA -> Measurable -> Either Text EWMA
ewma (EmptyEWMA a) v = Right $ EWMA a v
ewma (EWMA a s@(Microseconds _)) y@(Microseconds _) =
EWMA a $ Microseconds $ round $ a * (getDouble y) + (1 - a) * (getDouble s)
Right $ EWMA a $ Microseconds $ round $ a * (getDouble y) + (1 - a) * (getDouble s)
ewma (EWMA a s@(Seconds _)) y@(Seconds _) =
EWMA a $ Seconds $ round $ a * (getDouble y) + (1 - a) * (getDouble s)
Right $ EWMA a $ Seconds $ round $ a * (getDouble y) + (1 - a) * (getDouble s)
ewma (EWMA a s@(Bytes _)) y@(Bytes _) =
EWMA a $ Bytes $ round $ a * (getDouble y) + (1 - a) * (getDouble s)
Right $ EWMA a $ Bytes $ round $ a * (getDouble y) + (1 - a) * (getDouble s)
ewma (EWMA a (PureI s)) (PureI y) =
EWMA a $ PureI $ round $ a * (fromInteger y) + (1 - a) * (fromInteger s)
Right $ EWMA a $ PureI $ round $ a * (fromInteger y) + (1 - a) * (fromInteger s)
ewma (EWMA a (PureD s)) (PureD y) =
EWMA a $ PureD $ a * y + (1 - a) * s
ewma _ _ = error "Cannot average on values of different type"
Right $ EWMA a $ PureD $ a * y + (1 - a) * s
ewma _ _ = Left "EWMA: Cannot compute average on values of different types"
\end{code}

3
iohk-monitoring/src/Cardano/BM/Output/EKGView.lhs

@ -192,7 +192,7 @@ instance IsEffectuator EKGView a where
instance ToObject a => IsBackend EKGView a where
typeof _ = EKGViewBK
realize _ = error "EKGView cannot be instantiated by 'realize'"
realize _ = fail "EKGView cannot be instantiated by 'realize'"
realizefrom config sbtrace _ = do
evref <- newEmptyMVar
@ -247,6 +247,7 @@ spawnDispatcher config evqueue sbtrace ekgtrace = do
Async.async $ qProc countersMVar
where
{-@ lazy qProc @-}
qProc :: MVar MessageCounter -> IO ()
qProc counters = do
maybeItem <- atomically $ TBQ.readTBQueue evqueue

12
iohk-monitoring/src/Cardano/BM/Output/Editor.lhs

@ -21,12 +21,12 @@ import qualified Control.Concurrent.Async as Async
import Control.Concurrent.MVar (MVar, newEmptyMVar, putMVar, readMVar, withMVar)
import Control.Exception.Safe (SomeException, catch)
import Control.Monad (void, when, forM_)
import Data.Aeson.Text (encodeToLazyText)
import Data.Aeson (encode)
import qualified Data.ByteString.Lazy.Char8 as BS8
import qualified Data.HashMap.Strict as HM
import Data.List (delete)
import Data.Text (pack, unpack)
import qualified Data.Text.IO as TIO
import qualified Data.Text.Lazy as TL
import Data.Time (getCurrentTime)
import Data.Time.Format (defaultTimeLocale, formatTime)
import Safe (readMay)
@ -73,7 +73,7 @@ type EditorMVar a = MVar (EditorInternal a)
newtype Editor a = Editor
{ getEd :: EditorMVar a }
data ToObject a => EditorInternal a = EditorInternal
data {-ToObject a =>-} EditorInternal a = EditorInternal
{ edSBtrace :: Trace IO a
, edThread :: Async.Async ()
, edBuffer :: LogBuffer a
@ -88,13 +88,13 @@ data ToObject a => EditorInternal a = EditorInternal
instance ToObject a => IsBackend Editor a where
typeof _ = EditorBK
realize _ = error "Editor cannot be instantiated by 'realize'"
realize _ = fail "Editor cannot be instantiated by 'realize'"
realizefrom config sbtrace _ = do
gref <- newEmptyMVar
let gui = Editor gref
port <- getGUIport config
when (port <= 0) $ error "cannot create GUI"
when (port <= 0) $ fail "cannot create GUI"
-- local |LogBuffer|
logbuf :: Cardano.BM.Output.LogBuffer.LogBuffer a <- Cardano.BM.Output.LogBuffer.realize config
@ -211,7 +211,7 @@ prepare editor config window = void $ do
let mkSimpleRow :: ToObject a => LoggerName -> LogObject a -> UI Element
mkSimpleRow n lo@(LogObject _lonm _lometa _lov) = UI.tr #. "itemrow" #+
[ UI.td #+ [ string (unpack n) ]
, UI.td #+ [ string $ unpack $ TL.toStrict (encodeToLazyText (toObject lo)) ]
, UI.td #+ [ string $ BS8.unpack $ {-TL.toStrict-} encode (toObject lo) ]
]
let mkTableRow :: Show t => Cmd -> LoggerName -> t -> UI Element
mkTableRow cmd n v = UI.tr #. "itemrow" #+

2
iohk-monitoring/src/Cardano/BM/Output/Log.lhs

@ -294,6 +294,8 @@ passN backend katip (LogObject loname lometa loitem) = do
Nothing -> ("", Just loitem)
in
(severity lometa, text, maylo)
(LogError text) ->
(severity lometa, text, Nothing)
(ObserveDiff _) ->
let text = TL.toStrict (encodeToLazyText (toObject loitem))
in

22
iohk-monitoring/src/Cardano/BM/Output/Monitoring.lhs

@ -9,6 +9,9 @@
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-@ embed Ratio * as int @-}
{-@ embed GHC.Natural.Natural as int @-}
module Cardano.BM.Output.Monitoring
(
Monitor
@ -26,7 +29,7 @@ import qualified Data.HashMap.Strict as HM
import Data.Text (pack)
import qualified Data.Text.IO as TIO
import Data.Time.Calendar (toModifiedJulianDay)
import Data.Time.Clock (UTCTime (..), getCurrentTime)
import Data.Time.Clock (UTCTime (..), diffTimeToPicoseconds, getCurrentTime)
import GHC.Clock (getMonotonicTimeNSec)
import System.IO (stderr)
@ -90,7 +93,7 @@ instance IsEffectuator Monitor a where
instance IsBackend Monitor a where
typeof _ = MonitoringBK
realize _ = error "Monitoring cannot be instantiated by 'realize'"
realize _ = fail "Monitoring cannot be instantiated by 'realize'"
realizefrom config sbtrace _ = do
monref <- newEmptyMVar
@ -129,6 +132,7 @@ spawnDispatcher mqueue config sbtrace = do
Warning -- Debug
Async.async (initMap >>= qProc countersMVar)
where
{-@ lazy qProc @-}
qProc counters state = do
maybeItem <- atomically $ TBQ.readTBQueue mqueue
case maybeItem of
@ -174,14 +178,14 @@ evalMonitoringAction sbtrace mmap logObj@(LogObject logname _ _) = do
else return mmap
where
utc2ns (UTCTime days secs) =
let yearsecs :: Rational
yearsecs = 365 * 24 * 3600
rdays,rsecs :: Rational
rdays = toRational $ toModifiedJulianDay days
rsecs = toRational secs
s2ns = 1000000000
let daysecs = 24 * 3600
rdays,rsecs :: Integer
rdays = toModifiedJulianDay days
rsecs = diffTimeToPicoseconds secs `div` 1000
s2ns = 1000*1000*1000
ns = rsecs + s2ns * rdays * daysecs
in
Nanoseconds $ round $ (fromRational $ s2ns * rsecs + rdays * yearsecs :: Double)
Nanoseconds $ fromInteger ns
updateEnv env (LogObject _ _ (ObserveOpen _)) = env
updateEnv env (LogObject _ _ (ObserveDiff _)) = env
updateEnv env (LogObject _ _ (ObserveClose _)) = env

28
iohk-monitoring/src/Cardano/BM/Output/Switchboard.lhs

@ -29,8 +29,8 @@ import Control.Concurrent.MVar (MVar, newEmptyMVar, newMVar,
import Control.Concurrent.STM (TVar, atomically, modifyTVar, retry)
import qualified Control.Concurrent.STM.TBQueue as TBQ
import Control.Exception.Safe (throwM)
import Control.Monad (forM, forM_, when, void)
import Data.Maybe (catMaybes, fromMaybe)
import Control.Monad (forM_, when, void)
import Data.Maybe (fromMaybe)
import qualified Data.Text.IO as TIO
import Data.Time.Clock (getCurrentTime)
import System.IO (stderr)
@ -137,18 +137,6 @@ instance IsEffectuator Switchboard a where
\end{code}
\begin{spec}
instead of 'writequeue ...':
evalMonitoringAction config item >>=
mapM_ (writequeue (sbQueue sb))
evalMonitoringAction :: Configuration -> LogObject a -> m [LogObject a]
evalMonitoringAction c item = return [item]
-- let action = LogObject { loName=(loName item) <> ".action", loContent=LogMessage ... }
-- return (action : item)
\end{spec}
\subsubsection{|Switchboard| implements |Backend| functions}\index{Switchboard!instance of IsBackend}
|Switchboard| is an |IsBackend|
@ -292,12 +280,16 @@ setupBackends :: ToObject a
-> Configuration
-> Switchboard a
-> IO [(BackendKind, Backend a)]
setupBackends bes c sb = catMaybes <$>
forM bes (\bk -> do { setupBackend' bk c sb >>= \case Nothing -> return Nothing
Just be -> return $ Just (bk, be) })
setupBackends bes c sb = setupBackendsAcc bes []
where
setupBackendsAcc [] acc = return acc
setupBackendsAcc (bk : r) acc = do
setupBackend' bk c sb >>= \case
Nothing -> setupBackendsAcc r acc
Just be -> setupBackendsAcc r ((bk,be) : acc)
setupBackend' :: ToObject a => BackendKind -> Configuration -> Switchboard a -> IO (Maybe (Backend a))
setupBackend' SwitchboardBK _ _ = error "cannot instantiate a further Switchboard"
setupBackend' SwitchboardBK _ _ = fail "cannot instantiate a further Switchboard"
#ifdef ENABLE_MONITORING
setupBackend' MonitoringBK c sb = do
let basetrace = mainTraceConditionally c sb

2
iohk-monitoring/src/Cardano/BM/Tracer.lhs

@ -10,6 +10,8 @@
{-# LANGUAGE FlexibleInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-@ LIQUID "--prune-unsorted" @-}
module Cardano.BM.Tracer
(
Tracer (..)

55
iohk-monitoring/test/Cardano/BM/Test/Aggregated.lhs

@ -73,11 +73,13 @@ lometa = unsafePerformIO $ mkLOMeta Debug Public
prop_Aggregation_comm :: Integer -> Integer -> Aggregated -> Property
prop_Aggregation_comm v1 v2 ag =
let AggregatedStats stats1 = updateAggregation (PureI v1) (updateAggregation (PureI v2) ag lometa Nothing) lometa Nothing
AggregatedStats stats2 = updateAggregation (PureI v2) (updateAggregation (PureI v1) ag lometa Nothing) lometa Nothing
let Right agg2 = updateAggregation (PureI v2) ag lometa Nothing
Right agg1 = updateAggregation (PureI v1) ag lometa Nothing
Right (AggregatedStats stats21) = updateAggregation (PureI v1) agg2 lometa Nothing
Right (AggregatedStats stats12) = updateAggregation (PureI v2) agg1 lometa Nothing
in
fbasic stats1 === fbasic stats2 .&&.
(v1 == v2) `implies` (flast stats1 === flast stats2)
fbasic stats21 === fbasic stats12 .&&.
(v1 == v2) `implies` (flast stats21 === flast stats12)
-- implication: if p1 is true, then return p2; otherwise true
implies :: Bool -> Property -> Property
@ -90,30 +92,31 @@ implies p1 p2 = property (not p1) .||. p2
unitAggregationInitialMinus1 :: Assertion
unitAggregationInitialMinus1 = do
let AggregatedStats stats1 = updateAggregation (-1) firstStateAggregatedStats lometa Nothing
let Right (AggregatedStats stats1) = updateAggregation (-1) firstStateAggregatedStats lometa Nothing
flast stats1 @?= (-1)
(fbasic stats1) @?= BaseStats (-1) 0 2 (-0.5) 0.5
(fdelta stats1) @?= BaseStats 0 0 1 0 0
-- AggregatedStats (Stats (-1) 0 (BaseStats (-1) 0 2 (-0.5) 0.5) (BaseStats 0 0 1 0 0) (BaseStats 0 0 1 0 0))
(fdelta stats1) @?= BaseStats (-1) (-1) 2 (-1) 0
-- AggregatedStats (Stats (-1) x (BaseStats (-1) 0 2 (-0.5) 0.5) (BaseStats (-1) (-1) 2 (-1) 0) (BaseStats x x 2 x 0))
unitAggregationInitialPlus1 :: Assertion
unitAggregationInitialPlus1 = do
let AggregatedStats stats1 = updateAggregation 1 firstStateAggregatedStats lometa Nothing
let Right (AggregatedStats stats1) = updateAggregation 1 firstStateAggregatedStats lometa Nothing
flast stats1 @?= 1
(fbasic stats1) @?= BaseStats 0 1 2 0.5 0.5
(fdelta stats1) @?= BaseStats 0 0 1 0 0
-- AggregatedStats (Stats 1 0 (BaseStats 0 1 2 0.5 0.5) (BaseStats 0 0 1 0 0) (BaseStats 0 0 1 0 0))
(fdelta stats1) @?= BaseStats 1 1 2 1 0
-- AggregatedStats (Stats 1 x (BaseStats 0 1 2 0.5 0.5) (BaseStats 1 1 2 1 0) (BaseStats x x 2 x 0))
unitAggregationInitialZero :: Assertion
unitAggregationInitialZero = do
let AggregatedStats stats1 = updateAggregation 0 firstStateAggregatedStats lometa Nothing
let Right (AggregatedStats stats1) = updateAggregation 0 firstStateAggregatedStats lometa Nothing
flast stats1 @?= 0
(fbasic stats1) @?= BaseStats 0 0 2 0 0
(fdelta stats1) @?= BaseStats 0 0 1 0 0
-- AggregatedStats (Stats 0 0 (BaseStats 0 0 2 0 0) (BaseStats 0 0 1 0 0) (BaseStats 0 0 1 0 0))
(fdelta stats1) @?= BaseStats 0 0 2 0 0
-- AggregatedStats (Stats 0 x (BaseStats 0 0 2 0 0) (BaseStats 0 0 2 0 0) (BaseStats x x 2 x 0))
unitAggregationInitialPlus1Minus1 :: Assertion
unitAggregationInitialPlus1Minus1 = do
let AggregatedStats stats1 = updateAggregation (PureI (-1)) (updateAggregation (PureI 1) firstStateAggregatedStats lometa Nothing) lometa Nothing
let Right agg1 = updateAggregation (PureI 1) firstStateAggregatedStats lometa Nothing
Right (AggregatedStats stats1) = updateAggregation (PureI (-1)) agg1 lometa Nothing
(fbasic stats1) @?= BaseStats (PureI (-1)) (PureI 1) 3 0.0 2.0
(fdelta stats1) @?= BaseStats (PureI (-2)) (PureI 0) 2 (-1.0) 2.0
(fdelta stats1) @?= BaseStats (PureI (-2)) (PureI 1) 3 (-0.5) 4.5
unitAggregationStepwise :: Assertion
unitAggregationStepwise = do
@ -121,24 +124,24 @@ unitAggregationStepwise = do
-- putStrLn (show stats0)
threadDelay 50000 -- 0.05 s
t1 <- mkLOMeta Debug Public
stats1 <- pure $ updateAggregation (Bytes 5000) stats0 t1 Nothing
Right stats1 <- pure $ updateAggregation (Bytes 5000) stats0 t1 Nothing
-- putStrLn (show stats1)
-- showTimedMean stats1
threadDelay 50000 -- 0.05 s
t2 <- mkLOMeta Debug Public
stats2 <- pure $ updateAggregation (Bytes 1000) stats1 t2 Nothing
Right stats2 <- pure $ updateAggregation (Bytes 1000) stats1 t2 Nothing
-- putStrLn (show stats2)
-- showTimedMean stats2
checkTimedMean stats2
threadDelay 50000 -- 0.05 s
t3 <- mkLOMeta Debug Public
stats3 <- pure $ updateAggregation (Bytes 3000) stats2 t3 Nothing
Right stats3 <- pure $ updateAggregation (Bytes 3000) stats2 t3 Nothing
-- putStrLn (show stats3)
-- showTimedMean stats3
checkTimedMean stats3
threadDelay 50000 -- 0.05 s
t4 <- mkLOMeta Debug Public
stats4 <- pure $ updateAggregation (Bytes 1000) stats3 t4 Nothing
Right stats4 <- pure $ updateAggregation (Bytes 1000) stats3 t4 Nothing
-- putStrLn (show stats4)
-- showTimedMean stats4
checkTimedMean stats4
@ -154,14 +157,22 @@ unitAggregationStepwise = do
commented out:
\begin{spec}
showTimedMean (AggregatedEWMA _) = return ()
showTimedMean (AggregatedStats s) = putStrLn $ "mean = " ++ show (meanOfStats (ftimed s)) ++ showUnits (fmin (ftimed s))
showTimedMean (AggregatedStats s) = putStrLn $ "mean = " ++ show (meanOfStats (ftimed s))
++ showUnits (fmin (ftimed s))
\end{spec}
\begin{code}
firstStateAggregatedStats :: Aggregated
firstStateAggregatedStats = AggregatedStats (Stats z z (BaseStats z z 1 0 0) (BaseStats z z 0 0 0) (BaseStats z z 0 0 0))
firstStateAggregatedStats = AggregatedStats $
Stats
z
z'
(BaseStats z z 1 0 0)
(BaseStats z z 1 0 0)
(BaseStats z' z' 1 0 0)
where
z = PureI 0
z = PureI 0
z' = Nanoseconds 0
\end{code}

16
iohk-monitoring/test/Cardano/BM/Test/Trace.lhs

@ -47,7 +47,7 @@ import Cardano.BM.Data.Severity
import Cardano.BM.Data.SubTrace
import Cardano.BM.Output.Switchboard (MockSwitchboard (..))
#ifdef ENABLE_OBSERVABLES
import Cardano.BM.Counters (diffTimeObserved, getMonoClock)
import Cardano.BM.Counters (getMonoClock)
import Cardano.BM.Data.Aggregated
import Cardano.BM.Data.Counter
import qualified Cardano.BM.Observer.Monadic as MonadicObserver
@ -212,6 +212,20 @@ runTimedAction cfg logTrace name reps = do
_ <- MonadicObserver.bracketObserveIO cfg trace Debug name action
return ()
action = return $ forM [1::Int ..100] $ \x -> [x] ++ (init $ reverse [1::Int ..10000])
diffTimeObserved :: CounterState -> CounterState -> Measurable
diffTimeObserved (CounterState id0 startCounters) (CounterState id1 endCounters) =
let
startTime = getMonotonicTime startCounters
endTime = getMonotonicTime endCounters
in
if (id0 == id1)
then endTime - startTime
else error "these clocks are not from the same experiment"
getMonotonicTime counters = case (filter isMonotonicClockCounter counters) of
[(Counter MonotonicClockTime _ mus)] -> mus
_ -> error "A time measurement is missing!"
isMonotonicClockCounter :: Counter -> Bool
isMonotonicClockCounter = (MonotonicClockTime ==) . cType
timingObservableVsUntimed :: Assertion
timingObservableVsUntimed = do

Loading…
Cancel
Save