Add running time printer and statistics for Laurel passes#938
Add running time printer and statistics for Laurel passes#938aqjune-aws wants to merge 11 commits intomainfrom
Conversation
|
This pull request was written by an internal request for collecting measures useful for observing how behaviors of passes change on benchmarks after Strata is updated. I relied on an agent to figure out which numbers to report. |
| { name := "EliminateValueReturns" | ||
| run := fun p _m => | ||
| let (p', diags) := eliminateValueReturnsTransform p | ||
| (p', diags.toList, {}) }, |
There was a problem hiding this comment.
EliminateValueReturns is the only pass that doesn't return Statistics from its underlying function — the pipeline wrapper supplies {}. For consistency, consider adding a Statistics return to eliminateValueReturnsTransform (even if it's just counting procedures processed), or at least leave a -- TODO here explaining why it's omitted.
There was a problem hiding this comment.
To avoid conflicts with updates in other Laurel passes, I left stats in eliminateHoles and inferHoleTypes only.
| /-- Human-readable name, used for profiling and file emission. -/ | ||
| name : String | ||
| /-- How many times `resolve` should be run after the pass. -/ | ||
| resolvesAfter : Nat := 0 |
There was a problem hiding this comment.
Can this be more than 1 ? Why not use a bool?
There was a problem hiding this comment.
It seems there were two resolve invocations after the previous modifiesClausesTransform call. Or should one of these be removed?
let (program, modifiesDiags) := modifiesClausesTransform model program
let result := resolve program (some model)
let (program, model) := (result.program, result.model)
let result := resolve program (some model)
let (program, model) := (result.program, result.model)
There was a problem hiding this comment.
One should be removed. The bool can be named something like introducesUnresolvedAstNodes: Bool or requiresReresolving: Bool
| | .staticProcedure proc => some (proc.inputs.map (·.type)) | ||
| | _ => none | ||
|
|
||
| inductive InferHoleTypesStats where |
There was a problem hiding this comment.
Is this useful? It looks a bit like a showcase for collecting data.
There was a problem hiding this comment.
I think this can be (somewhat?) useful because it is good to have an idea about how many annotated/unannotated holes there are in benchmarks.
There was a problem hiding this comment.
What what you do with that information?
| { program with staticProcedures := finalState.generatedFunctions ++ procs } | ||
| let stats := ({} : Statistics) | ||
| |>.increment s!"{ElimHoleStats.holesEliminated}" finalState.counter | ||
| |>.increment s!"{ElimHoleStats.functionsGenerated}" finalState.generatedFunctions.length |
There was a problem hiding this comment.
Nit: by construction each eliminated hole produces exactly one generated function, so functionsGenerated == holesEliminated should always hold. Consider stating that as an assert (or at minimum a comment) so a future change that breaks the 1-to-1 relationship is caught early.
There was a problem hiding this comment.
Good catch, thank you.
| let (program', diags, stats) ← profileStep options.profile s!" {pass.name}" do | ||
| pure (pass.run program model) | ||
| program := program' | ||
| allDiags := allDiags ++ diags |
There was a problem hiding this comment.
Soft note: allDiags := allDiags ++ diags is left-nested List append inside the loop (O(n) per iteration). With 11 passes and typically small diagnostic lists this is fine, but if diagnostic counts grow consider switching to Array accumulation with Array.append.
There was a problem hiding this comment.
Yes, diags will be pretty small. :) It would be fine.
|
|
||
| public import Strata.Languages.Laurel.MapStmtExpr | ||
| public import Strata.Languages.Laurel.Resolution | ||
| public import Strata.Util.Statistics |
| (keepAllFilesPrefix := keepPrefix) (profile := profile) | ||
|
|
||
| if profile && !laurelPassStats.data.isEmpty then | ||
| let _ ← (IO.println laurelPassStats.format |>.toBaseIO) |
There was a problem hiding this comment.
| let _ ← (IO.println laurelPassStats.format |>.toBaseIO) | |
| IO.println laurelPassStats.format |
5 participants
This pull request
profileSteputility function in Strata) and statistics for Laurel passes--profileis given#in front ofderive_prefixed_toStringwhich was promised in Collect Statistics for the Core pipeline #870 (comment) .By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.