add optimisation performance comparison

Author: Atticus Kuhn

OptimisationPerformanceComparison.lean

@@ -0,0 +1,208 @@
+import PartIiProject.Bench.Common
+import PartIiProject.Bench.Table
+import PartIiProject.Optimisations
+import PartIiProject.SyntaxSDQLProg
+import Lean
+import Std
+
+open PartIiProject
+open PartIiProject.Optimisations
+open System
+
+namespace OptimisationPerformanceComparison
+
+def outDir : FilePath := FilePath.mk ".sdql-opt-perf-out"
+def runtimeSrc : FilePath := FilePath.mk "sdql_runtime.rs"
+
+def iters : Nat := 3
+def dictN : Int := 200000
+def memoN : Int := 100000
+def memoM : Int := 1000
+
+unsafe structure BenchCase where
+  name : String
+  prog : SProg2
+  opts : List Optimisation
+  env : List (String × String) := []
+
+structure Reading where
+  name : String
+  unoptMs : Nat
+  optMs : Nat
+
+def meanNat (xs : List Nat) : Nat :=
+  match xs with
+  | [] => 0
+  | _ =>
+      let total := xs.foldl (fun s x => s + x) 0
+      total / xs.length
+
+def timeBinaryAvgMs (binPath : FilePath) (iters : Nat) (env : List (String × String)) :
+    IO (Except String Nat) := do
+  if iters == 0 then
+    return .error "iters must be > 0"
+  let mut acc : List Nat := []
+  for _ in [0:iters] do
+    match ← PartIiProject.Bench.timeBinaryMs binPath env with
+    | .ok ms => acc := ms :: acc
+    | .error e => return .error e
+  return .ok (meanNat acc)
+
+unsafe def runCase (b : BenchCase) : IO (Except String Reading) := do
+  let baseCp := ToCore2.trProg2 b.prog
+  let optTerm := applyOptimisationsLoc b.opts baseCp.term
+  let optCp : Prog2 := { baseCp with term := optTerm }
+
+  let unoptBin ←
+    match ← PartIiProject.Bench.compileProg2ToBin outDir runtimeSrc s!"{b.name}_unopt" baseCp with
+    | .ok p => pure p
+    | .error e => return .error s!"Unoptimised compile failed:\n{e}"
+
+  let optBin ←
+    match ← PartIiProject.Bench.compileProg2ToBin outDir runtimeSrc s!"{b.name}_opt" optCp with
+    | .ok p => pure p
+    | .error e => return .error s!"Optimised compile failed:\n{e}"
+
+  let unoptMs ←
+    match ← timeBinaryAvgMs unoptBin iters b.env with
+    | .ok ms => pure ms
+    | .error e => return .error s!"Unoptimised run failed:\n{e}"
+
+  let optMs ←
+    match ← timeBinaryAvgMs optBin iters b.env with
+    | .ok ms => pure ms
+    | .error e => return .error s!"Optimised run failed:\n{e}"
+
+  return .ok { name := b.name, unoptMs := unoptMs, optMs := optMs }
+
+unsafe def p_vertical_loop_fusion_key_map : SProg2 :=
+  [SDQLProg2 { { int -> int } }|
+    let dictN = 200000 in
+    let d = sum( <i, _> <- range(dictN) ) { i -> i } in
+    let y = sum( <x, x_v> <- d ) { x + 1 -> x_v } in
+    sum( <x, x_v> <- y ) { x + 2 -> x_v }
+  ]
+
+unsafe def p_vertical_loop_fusion_value_map : SProg2 :=
+  [SDQLProg2 { { int -> int } }|
+    let dictN = 200000 in
+    let d = sum( <i, _> <- range(dictN) ) { i -> i } in
+    let y = sum( <x, x_v> <- d ) { x -> x_v + 1 } in
+    sum( <x, x_v> <- y ) { x -> x_v + 2 }
+  ]
+
+unsafe def p_horizontal_loop_fusion : SProg2 :=
+  [SDQLProg2 { int }|
+    let dictN = 200000 in
+    let d = sum( <i, _> <- range(dictN) ) { i -> i } in
+    let y1 = sum( <_, v> <- d ) v in
+    let y2 = sum( <_, v> <- d ) (v + 1) in
+    y1 + y2
+  ]
+
+unsafe def p_loop_factorization_left : SProg2 :=
+  [SDQLProg2 { int }|
+    let dictN = 200000 in
+    let d = sum( <i, _> <- range(dictN) ) { i -> i } in
+    sum( <_, v> <- d ) (2 * v)
+  ]
+
+unsafe def p_loop_factorization_right : SProg2 :=
+  [SDQLProg2 { int }|
+    let dictN = 200000 in
+    let d = sum( <i, _> <- range(dictN) ) { i -> i } in
+    sum( <_, v> <- d ) (v * 2)
+  ]
+
+unsafe def p_loop_invariant_code_motion : SProg2 :=
+  [SDQLProg2 { int }|
+    let dictN = 200000 in
+    let d = sum( <i, _> <- range(dictN) ) { i -> i } in
+    sum( <_, v> <- d ) (let y = 5 in v + y)
+  ]
+
+-- Memoization lookup + hoisting: without hoisting this is not a win; include code motion.
+unsafe def p_loop_memoization_lookup : SProg2 :=
+  [SDQLProg2 { int }|
+    let memoN = 100000 in
+    let memoM = 1000 in
+    let d = sum( <i, _> <- range(memoN) ) { i -> i } in
+    sum( <i, _> <- range(memoM) ) (sum( <k, v> <- d ) (if k == i then v))
+  ]
+
+-- Partition + hoisting: then-branch depends on `i`, so lookup-memoization cannot hoist `f`.
+unsafe def p_loop_memoization_partition : SProg2 :=
+  [SDQLProg2 { int }|
+    let memoN = 100000 in
+    let memoM = 1000 in
+    let d = sum( <i, _> <- range(memoN) ) { i -> i } in
+    sum( <i, _> <- range(memoM) ) (sum( <k, v> <- d ) (if k == i then v + i))
+  ]
+
+unsafe def mkCases : List BenchCase :=
+  [ { name := "vertical_loop_fusion_key_map"
+      prog := p_vertical_loop_fusion_key_map
+      opts := [verticalLoopFusionKeyMap2, verticalLoopFusionValueMap2]
+    }
+  , { name := "vertical_loop_fusion_value_map"
+      prog := p_vertical_loop_fusion_value_map
+      opts := [verticalLoopFusionKeyMap2, verticalLoopFusionValueMap2]
+    }
+  , { name := "horizontal_loop_fusion"
+      prog := p_horizontal_loop_fusion
+      opts := [horizontalLoopFusion2]
+    }
+  , { name := "loop_factorization_left"
+      prog := p_loop_factorization_left
+      opts := [loopFactorizationLeft2]
+    }
+  , { name := "loop_factorization_right"
+      prog := p_loop_factorization_right
+      opts := [loopFactorizationRight2]
+    }
+  , { name := "loop_invariant_code_motion"
+      prog := p_loop_invariant_code_motion
+      opts := [loopInvariantCodeMotion2]
+    }
+  , { name := "loop_memoization_lookup"
+      prog := p_loop_memoization_lookup
+      opts := [loopMemoizationLookup2, loopInvariantCodeMotion2]
+    }
+  , { name := "loop_memoization_partition"
+      prog := p_loop_memoization_partition
+      opts := [loopMemoizationPartition2, loopInvariantCodeMotion2]
+    }
+  ]
+
+unsafe def main (_args : List String) : IO UInt32 := do
+  if (← outDir.pathExists) then
+    IO.FS.removeDirAll outDir
+  IO.FS.createDirAll outDir
+
+  let mut readings : List Reading := []
+  let mut failures : List (String × String) := []
+
+  for b in mkCases do
+    match ← runCase b with
+    | .ok r => readings := readings.concat r
+    | .error e => failures := failures.concat (b.name, e)
+
+  PartIiProject.Bench.printMsComparisonTable
+    s!"SDQL optimisation performance comparison (mean of {iters} run(s); wall-clock ms)"
+    "unopt" "opt" "opt/unopt"
+    (readings.map fun r =>
+      { name := r.name, leftMs := r.unoptMs, rightMs := r.optMs })
+    (preamble := [s!"Params: dictN={dictN}, memoN={memoN}, memoM={memoM}"])
+
+  if !failures.isEmpty then
+    IO.eprintln ""
+    IO.eprintln "Failures:"
+    for (nm, err) in failures do
+      IO.eprintln s!"- {nm}: {err}"
+    return 1
+  return 0
+
+end OptimisationPerformanceComparison
+
+unsafe def main (args : List String) : IO UInt32 :=
+  OptimisationPerformanceComparison.main args

PartIiProject/Bench/Common.lean

@@ -0,0 +1,113 @@
+import PartIiProject.CodegenRust
+import PartIiProject.SyntaxSDQLProg
+import Lean
+import Std
+
+open PartIiProject
+open System
+
+namespace PartIiProject.Bench
+
+def writeFile (p : FilePath) (s : String) : IO Unit :=
+  IO.FS.writeFile p s
+
+def copyFile (src dst : FilePath) : IO Unit := do
+  let contents ← IO.FS.readFile src
+  IO.FS.writeFile dst contents
+
+def absPath (p : FilePath) : IO FilePath := do
+  let cwd ← IO.currentDir
+  pure (cwd / p)
+
+def runProc (cmd : String) (args : Array String) (cwd? : Option FilePath := none)
+    (envVars : List (String × String) := []) : IO (Nat × String × String) := do
+  let env : Array (String × Option String) := envVars.toArray.map (fun (k, v) => (k, some v))
+  let out ← IO.Process.output { cmd := cmd, args := args, cwd := cwd?, env := env, inheritEnv := Bool.true }
+  return (out.exitCode.toNat, out.stdout, out.stderr)
+
+def runProcDiscardStdout (cmd : String) (args : Array String) (cwd? : Option FilePath := none)
+    (envVars : List (String × String) := []) : IO (Nat × String) := do
+  let env : Array (String × Option String) := envVars.toArray.map (fun (k, v) => (k, some v))
+  let child ← IO.Process.spawn {
+    cmd := cmd,
+    args := args,
+    cwd := cwd?,
+    env := env,
+    inheritEnv := Bool.true,
+    stdout := .null,
+    stderr := .piped,
+  }
+  let code := (← child.wait).toNat
+  let err ← child.stderr.readToEnd
+  return (code, err)
+
+def runTimedMs (cmd : String) (args : Array String) (cwd? : Option FilePath := none)
+    (envVars : List (String × String) := []) : IO (Nat × Nat) := do
+  let env : Array (String × Option String) := envVars.toArray.map (fun (k, v) => (k, some v))
+  let start ← IO.monoMsNow
+  let child ← IO.Process.spawn {
+    cmd := cmd,
+    args := args,
+    cwd := cwd?,
+    env := env,
+    stdout := .null,
+    stderr := .null,
+  }
+  let code := (← child.wait).toNat
+  let stop ← IO.monoMsNow
+  return (code, stop - start)
+
+def compileRust (rsPath binPath : FilePath) : IO (Except String Unit) := do
+  let (code, _out, err) ← runProc "rustc"
+    #["-O", "-C", "target-cpu=native", "-o", binPath.toString, rsPath.toString]
+  if code != 0 then
+    return .error err
+  return .ok ()
+
+def copyRuntime (runtimeSrc outDir : FilePath) : IO Unit := do
+  IO.FS.createDirAll outDir
+  copyFile runtimeSrc (outDir / "sdql_runtime.rs")
+
+unsafe def compileProg2ToBin (outDir runtimeSrc : FilePath) (name : String) (cp : Prog2) :
+    IO (Except String FilePath) := do
+  copyRuntime runtimeSrc outDir
+  let rs := PartIiProject.renderRustProg2Shown cp
+  let rsPath := outDir / s!"{name}.rs"
+  let binPath := outDir / s!"{name}.bin"
+  writeFile rsPath rs
+  match ← compileRust rsPath binPath with
+  | .ok () => return .ok binPath
+  | .error err => return .error err
+
+unsafe def compileSProg2ToBin (outDir runtimeSrc : FilePath) (name : String) (sp : SProg2) :
+    IO (Except String FilePath) := do
+  compileProg2ToBin outDir runtimeSrc name (ToCore2.trProg2 sp)
+
+def timeBinaryMs (binPath : FilePath) (envVars : List (String × String) := []) : IO (Except String Nat) := do
+  let (code, ms) ← runTimedMs binPath.toString #[] (cwd? := none) (envVars := envVars)
+  if code != 0 then
+    return .error s!"Non-zero exit code {code} for {binPath.toString}"
+  return .ok ms
+
+def padLeft (width : Nat) (s : String) : String :=
+  if s.length >= width then s else String.mk (List.replicate (width - s.length) ' ') ++ s
+
+def padRight (width : Nat) (s : String) : String :=
+  if s.length >= width then s else s ++ String.mk (List.replicate (width - s.length) ' ')
+
+def pad3 (n : Nat) : String :=
+  let s := toString n
+  if s.length >= 3 then s else String.mk (List.replicate (3 - s.length) '0') ++ s
+
+def ratioMilli (numer denom : Nat) : Nat :=
+  if denom == 0 then 0 else (numer * 1000) / denom
+
+def ratioString (numer denom : Nat) : String :=
+  if denom == 0 then "n/a"
+  else
+    let rm := ratioMilli numer denom
+    let whole := rm / 1000
+    let frac := rm % 1000
+    s!"{whole}.{pad3 frac}×"
+
+end PartIiProject.Bench

PartIiProject/Bench/Table.lean

@@ -0,0 +1,50 @@
+import PartIiProject.Bench.Common
+import Std
+
+namespace PartIiProject.Bench
+
+structure MsComparisonRow where
+  name : String
+  leftMs : Nat
+  rightMs : Nat
+
+def printMsComparisonTable
+    (title : String)
+    (leftLabel rightLabel ratioLabel : String)
+    (rows : List MsComparisonRow)
+    (preamble : List String := [])
+    (nameHeader : String := "case")
+    (totalLabel : String := "TOTAL")
+    (colW : Nat := 12) : IO Unit := do
+  if rows.isEmpty then
+    IO.println "No benchmarks ran."
+    return
+
+  let nameW := rows.foldl (fun w r => max w r.name.length) nameHeader.length
+
+  IO.println title
+  for l in preamble do
+    IO.println l
+
+  IO.println (padRight nameW nameHeader ++ "  " ++
+    padLeft colW leftLabel ++ "  " ++
+    padLeft colW rightLabel ++ "  " ++
+    padLeft colW ratioLabel)
+  IO.println (String.mk (List.replicate (nameW + 2 + colW*3 + 4) '-'))
+
+  for r in rows do
+    IO.println (padRight nameW r.name ++ "  " ++
+      padLeft colW s!"{r.leftMs}ms" ++ "  " ++
+      padLeft colW s!"{r.rightMs}ms" ++ "  " ++
+      padLeft colW (ratioString r.rightMs r.leftMs))
+
+  let totalLeft := rows.foldl (fun s r => s + r.leftMs) 0
+  let totalRight := rows.foldl (fun s r => s + r.rightMs) 0
+  IO.println (String.mk (List.replicate (nameW + 2 + colW*3 + 4) '-'))
+  IO.println (padRight nameW totalLabel ++ "  " ++
+    padLeft colW s!"{totalLeft}ms" ++ "  " ++
+    padLeft colW s!"{totalRight}ms" ++ "  " ++
+    padLeft colW (ratioString totalRight totalLeft))
+
+end PartIiProject.Bench
+