feat(ase): automated timing benchmark

analyses/simpleactor/app/ASE/Benchmark.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE DeriveGeneric #-}
 -- | Benchmarks for the ASE paper
 module ASE.Benchmark where
 
@@ -13,9 +14,42 @@ import qualified Analysis.ASE.WidenedStates as SmallStepWidened
 -- Haskell-related
 import Control.DeepSeq
 import Control.Monad
-import Data.Map (Map) 
-import qualified Data.Map as Map
+import GHC.Generics
+import RIO hiding (hFlush)
 
+-- Files
+import System.FilePath.Posix
+import GHC.IO.Handle
+
+-- Time related
+import Data.Time
+import Data.Time.Clock.System
+import Data.Time.Format.ISO8601
+
+
+-- Command line parsing imports
+import Options.Applicative
+
+
+------------------------------------------------------------
+-- Command-line interface
+------------------------------------------------------------
+
+newtype BenchmarkOptions = BenchmarkOptions {
+      outputFilename :: String
+   } deriving (Show, Ord, Eq)
+
+benchmarkOptions :: Parser BenchmarkOptions 
+benchmarkOptions = BenchmarkOptions <$> strOption ( long "file" <> short 'f' <> help "Output filename" )
+
+benchmarkCmd :: BenchmarkOptions -> IO () 
+benchmarkCmd (BenchmarkOptions { .. }) = runTimeBenchmarks benchmarkPrograms outputFilename
+
+------------------------------------------------------------
+-- Benchmark programs
+------------------------------------------------------------
+
+benchmarkPrograms :: [String]
 benchmarkPrograms = [
       "games_snake.rkt",
       "games_tetris.rkt",
@@ -54,41 +88,91 @@ benchmarkPrograms = [
       "softy_tak.rkt"
    ]
 
-{-
 -- | Loads a program from disk, translates it to a simpler form amenable for verification, parses and compiles it
 loadProgram :: String -> IO Exp
 loadProgram = readFile >=> translate >=> return . either (error . ("error while parsing" ++)) id . parseFromString
 
+------------------------------------------------------------
+-- Timing
+------------------------------------------------------------
+
+-- | Get the current time in nanoseconds
+getTime :: IO Integer
+getTime = do
+   currentTime <- getSystemTime
+   return $ fromIntegral (systemSeconds currentTime) * 1000 * 1000 * 10000 + fromIntegral (systemNanoseconds currentTime)
+
+-- | The total of iterations to run the benchmark for
+totalIterations :: Integer
+totalIterations = 20
+
+time :: NFData a => IO a -> IO (a, Integer)
+time act = do
+   start <- getTime
+   v <- act
+   end <- v `deepseq` getTime
+   return (v, start - end)
+
+------------------------------------------------------------
+-- Analysis results and configurations
+------------------------------------------------------------
+
 -- | A polymorphic analysis result, no information about this 
 -- analysis result is known, except that it can be inspected 
 -- and evaluated using `deepseq`.
-data AnalysisResult where  
-   AnalysisResult :: NFData a => a -> AnalysisResult
+data AnalysisResult where
+   AnalysisResult :: (NFData a) => a -> AnalysisResult
+
+instance NFData AnalysisResult where
+   rnf (AnalysisResult a) = rnf a
 
 analysisConfigurations :: [(String, Exp -> IO AnalysisResult)]
 analysisConfigurations = concatMap (\k -> [
       ("smallstep, k = " ++ show k, fmap AnalysisResult . SmallStep.analyze k),
       ("widened per state, k = " ++ show k, fmap AnalysisResult . SmallStepWidened.analyze k)
    ]) [1..5]
 
--- | The total of iterations to run the benchmark for
-totalIterations :: Int
-totalIterations = 20
 
-time :: IO () -> IO Integer 
-time act = do 
-   start <- getTime
-   v <- act
-   v `deepseq` getTime
+-- | The result of running a single benchmark once
+data Result = Result {
+      benchmarkName :: String,
+      benchmarkIteration :: Integer,
+      benchmarkAnalysisResult :: AnalysisResult,
+      benchmarkTime :: Integer
+   } deriving (Generic)
+
+instance NFData Result
+
+-- | Write a single result to a file
+writeToFile :: Handle -- ^ the file handle to write the output to, gets flushed after writing
+            -> String -- ^ name of the program to write the result for
+            -> Result -- ^ the result to write to the file
+            -> IO ()
+writeToFile hdl programName (Result { .. }) = do
+   hPutStr hdl programName >> hPutStr hdl ";"
+   hPutStr hdl benchmarkName >> hPutStr hdl ";"
+   hPutStr hdl (show benchmarkIteration) >> hPutStr hdl ";"
+   hPutStr hdl (show benchmarkTime) >> hPutChar hdl '\n'
+   hFlush hdl
+
+-- | Open an output file suffixed with the timestamp
+openTimestamped :: FilePath -> IO Handle
+openTimestamped path = do
+      currentTime <- getCurrentTime
+      let formattedTime = iso8601Show currentTime
+      let filename = addExtension (base ++ formattedTime) extension
+      openFile filename WriteMode
+   where (base, extension) = splitExtension path
 
 -- | Run the timing benchmarks over the set of programs
-benchmarkTime :: [String] -- ^ the programs to run the benchmark on
-              -> String   -- ^ the name of the file to output the benchmark results to 
-              -> IO ()
-benchmarkTime = run
-   where runSingle (name, runner) program = do 
-            exp <- loadProgram program
-            results <- mapM (\i -> time (runner exp) >>= (\time -> (name, i, time))) [0..totalIterations]
-            results `deepseq` (return results)
-
--}
+runTimeBenchmarks :: [String] -- ^ the programs to run the benchmark on
+                  -> String   -- ^ the name of the file to output the benchmark results to 
+                  -> IO ()
+runTimeBenchmarks benchmarks outputFilename = do
+      outputHandle <- openTimestamped outputFilename
+      mapM_ (\(runner,filename) -> runSingle runner filename >>= mapM (writeToFile outputHandle filename)) benchmarkWithConfigurations
+   where runSingle (name, runner) program = do
+            expr <- loadProgram program
+            results <- mapM (\i -> time (runner expr) <&> uncurry (Result name i)) [0..totalIterations]
+            results `deepseq` return results
+         benchmarkWithConfigurations = [ (runner, benchmark) | runner <- analysisConfigurations, benchmark <- benchmarks ]

analyses/simpleactor/app/Main.hs

@@ -23,6 +23,7 @@ import qualified Analysis.ASE.Common as ASE
 import qualified Analysis.ASE.WidenedStates as SmallStepWidened
 import System.IO
 import Control.Monad
+import ASE.Benchmark
 
 ------------------------------------------------------------
 -- Command-line arguments
@@ -52,7 +53,8 @@ commandParser =
     (   command "smallstep" (info (smallstepCmd <$> inputOptions) (progDesc "Analyze a program using the ASE in small-step"))
     <>  command "analyze" (info (analyzeCmd <$> inputOptions) (progDesc "Analyze a program"))
     <>  command "eval"    (info (interpret <$> inputOptions) (progDesc "Run a program"))
-    <>  command "smallstepw" (info (smallstepWideningCmd <$> inputOptions) (progDesc "Analyze a program using ASE in small-step, widened version")))
+    <>  command "smallstepw" (info (smallstepWideningCmd <$> inputOptions) (progDesc "Analyze a program using ASE in small-step, widened version"))
+    <>  command "asebenchmark" (info (benchmarkCmd <$> benchmarkOptions) (progDesc "Benchmark ASE programs in all configurations")))
 
 
 ------------------------------------------------------------

analyses/simpleactor/interpreter.cabal

@@ -120,6 +120,7 @@ executable interpreter-exe
       base >=4.7 && <5
     , containers
     , deepseq
+    , filepath
     , hspec
     , hspec-contrib
     , interpreter
@@ -128,6 +129,7 @@ executable interpreter-exe
     , maf2-syntax
     , optparse-applicative
     , rio
+    , time
   default-language: Haskell2010
 
 test-suite interpreter-test

analyses/simpleactor/package.yaml

@@ -89,6 +89,8 @@ executables:
     - maf2-syntax
     - maf2-domains
     - maf2-analysis
+    - filepath
+    - time
 
 tests:
   interpreter-test: