0 | module Profile.Runner
  1 |
  2 | import Data.Refined.Integer
  3 | import Data.String
  4 | import Text.Printf
  5 | import Profile.Statistics
  6 | import Profile.Types
  7 |
  8 | %default total
  9 |
 10 | %foreign "scheme,chez:(lambda () (collect (collect-maximum-generation)))"
 11 |          "javascript:lambda:(w) => {}"
 12 | prim__collect : PrimIO ()
 13 |
 14 | unitFor : Integer -> String
 15 | unitFor 0 = "fs"
 16 | unitFor 1 = "ps"
 17 | unitFor 2 = "ns"
 18 | unitFor 3 = "μs"
 19 | unitFor 4 = "ms"
 20 | unitFor 5 = " s"
 21 | unitFor _ = "s"
 22 |
 23 | nonSec : (sig,exp : Integer) -> String -> String
 24 | nonSec sig exp s =
 25 |   let (factor,pad) :=
 26 |         case exp `mod` 3 of
 27 |           0 => (1000, S 2)
 28 |           1 => (100, S 1)
 29 |           _ => (10, S Z)
 30 |       pre  := show $ sig `div` factor
 31 |       post := padLeft pad '0' . show $ sig `mod` factor
 32 |    in "\{pre}.\{post} \{s}"
 33 |
 34 | printPos : Integer -> String
 35 | printPos n = case lte 1000 n of
 36 |   Nothing0 => padLeft 8 ' ' "\{show n} as"
 37 |   Just0 x  =>
 38 |     let (n',exp) := significant n 4 @{weak [0,1000,n]}
 39 |         exp'     := cast {to = Integer} exp
 40 |      in case unitFor (exp' `div` 3) of
 41 |           "s" => case exp `minus` 18 of
 42 |             0 => "\{show n'} s"
 43 |             e => "\{show n'}e\{show e} s"
 44 |           u   => nonSec n' exp' u
 45 |
 46 | printAtto : AttoSecondsPerRun -> String
 47 | printAtto (MkScalar v) = if v < 0 then "-" ++ printPos v else printPos v
 48 |
 49 | -- an exponentially growing series of numbers of repetitions
 50 | runs : List Pos
 51 | runs = go 600 [< 1] 1 1.0
 52 |
 53 |   where
 54 |     go : Nat -> SnocList Pos -> Pos -> Double -> List Pos
 55 |     go 0     sx p x = sx <>> Nil
 56 |     go (S k) sx p x =
 57 |       let nx       = x * 1.05
 58 |           n2@(S _) = cast nx | 0 => go k sx p nx
 59 |           p2       = MkPos n2
 60 |        in go k (if p2.val > p.val then sx :< p2 else sx) p2 nx
 61 |
 62 | -- runs a benchmark once with the given number of
 63 | -- iterations
 64 | run : Pos -> Benchmarkable err -> IO (Either err Measured)
 65 | run p (MkBenchmarkable alloc clean go cpuonly) = do
 66 |   env      <- alloc p
 67 |   fromPrim prim__collect
 68 |   start    <- clockTime Monotonic
 69 |   startCPU <- clockTime Process
 70 |   res      <- go env p
 71 |   stopCPU  <- clockTime Process
 72 |   stop     <- clockTime Monotonic
 73 |   clean p env
 74 |
 75 |   let tot  := timeDelta start stop
 76 |       cpu  := timeDelta startCPU stopCPU
 77 |       runs := the Runs $ MkScalar $ cast p.val
 78 |       meas :=
 79 |         MkMeasured
 80 |           { iterations = runs
 81 |           , startTime  = start
 82 |           , stopTime   = stop
 83 |           , totalTime  = tot
 84 |           , avrgTime   = tot `div` runs
 85 |           , cpuTime    = cpu
 86 |           , avrgCPU    = cpu `div` runs
 87 |           , cpuOnly    = cpuonly
 88 |           }
 89 |   case res of
 90 |     Left err => pure (Left err)
 91 |     Right v  => pure (Right meas)
 92 |
 93 | -- 30 ms
 94 | threshold : AttoSeconds
 95 | threshold = fromMilliSeconds 30
 96 |
 97 | -- 300 ms
 98 | threshold10 : AttoSeconds
 99 | threshold10 = fromMilliSeconds 300
100 |
101 | ||| Run a benchmark with an increasing number of
102 | ||| iterations until at least the given time limit
103 | ||| has passed.
104 | export
105 | runBenchmark : (timeLimit : AttoSeconds)
106 |              -> Benchmarkable err
107 |              -> IO (Either err $ List Measured)
108 | runBenchmark timeLimit b = do
109 |   startTime <- clockTime Monotonic
110 |   fromPrim $ go Lin runs startTime 0 0
111 |
112 |   where
113 |     go :
114 |          SnocList Measured
115 |       -> List Pos
116 |       -> (startTime     : Clock Monotonic)
117 |       -> (overThreshold : AttoSeconds)
118 |       -> (nruns         : Nat)
119 |       -> PrimIO (Either err $ List Measured)
120 |     go sr []        st ot nr w = MkIORes (Right $ sr <>> Nil) w
121 |     go sr (p :: ps) st ot nr w =
122 |       let MkIORes (Right r) w2 := toPrim (run p b) w
123 |             | MkIORes (Left err) w2 => MkIORes (Left err) w2
124 |           diffThreshold := max 0 $ r.totalTime `minus` threshold
125 |           overThreshold := ot `plus` diffThreshold
126 |           tot           := fromClock $ timeDifference r.stopTime st
127 |           done          :=
128 |             tot           >= timeLimit   &&
129 |             overThreshold >= threshold10 &&
130 |             nr            >= 4
131 |
132 |        in if done then MkIORes (Right (sr <>> [r])) w2
133 |           else go (sr :< r) ps st overThreshold (S nr) w2
134 |
135 | detailStats : Nat -> String -> Stats -> String
136 | detailStats k name stats = """
137 |   # \{show k}: \{name}
138 |     time per run : \{printAtto stats.slope}
139 |     mean         : \{printAtto stats.mean}
140 |     r2           : \{show stats.r2}
141 |
142 |
143 |   """
144 |
145 | tableStats : Nat -> String -> Stats -> String
146 | tableStats k name stats =
147 |   let nm   := padRight 50 ' ' name
148 |       tpr  := padLeft 10 ' ' $ printAtto stats.slope
149 |       mean := padLeft 10 ' ' $ printAtto stats.mean
150 |       r2   := pack $ take 5 $ unpack $ show stats.r2
151 |    in "\{nm} \{tpr} \{mean} \{r2}"
152 |
153 | showStats : Format -> Nat -> String -> Stats -> String
154 | showStats Table   = tableStats
155 | showStats Details = detailStats
156 |
157 | runAndPrint :
158 |      Format
159 |   -> Nat
160 |   -> String
161 |   -> Benchmarkable err
162 |   -> IO (Either err ())
163 | runAndPrint format k name b = do
164 |   Right (h :: t) <- runBenchmark (fromSeconds 1) b
165 |     | Right [] => pure (Right ())
166 |     | Left err => pure (Left err)
167 |
168 |   putStrLn (showStats format k name $ regr (h :: fromList t))
169 |   pure (Right ())
170 |
171 | for :
172 |      (String -> Bool)
173 |   -> Benchmark err
174 |   -> (Nat -> String -> Benchmarkable err -> IO (Either err ()))
175 |   -> IO (Either err ())
176 | for select b f = ignore <$> fromPrim (go 1 "" b)
177 |
178 |   where
179 |     many : Nat -> String -> List (Benchmark err) -> PrimIO (Either err Nat)
180 |
181 |     go : Nat -> String -> Benchmark err -> PrimIO (Either err Nat)
182 |     go k s (Single name bench) w =
183 |       let s' := addPrefix s name
184 |        in if select s'
185 |             then
186 |               let MkIORes (Right _) w2 := toPrim (f k s' bench) w
187 |                     | MkIORes (Left err) w2 => MkIORes (Left err) w2
188 |                in MkIORes (Right $ S k) w2
189 |             else MkIORes (Right k) w
190 |     go k s (Group name benchs) w = many k (addPrefix s name) benchs w
191 |
192 |     many k s [] w        = MkIORes (Right k) w
193 |     many k s (b :: bs) w =
194 |       let MkIORes (Right k2) w2 = go k s b w
195 |             | MkIORes (Left err) w2 => MkIORes (Left err) w2
196 |        in many k2 s bs w2
197 |
198 | export
199 | runDefault :
200 |      (String -> Bool)
201 |   -> Format
202 |   -> (err -> String)
203 |   -> Benchmark err
204 |   -> IO ()
205 | runDefault select format showErr b = do
206 |   Left err <- for select b (runAndPrint format)
207 |     | Right () => pure ()
208 |   putStrLn (showErr err)
209 |