This module contains the basic definitions and structures for modelling costs.
module Cost where
open import Agda.Builtin.Unit using (tt) open import Function using (_∘_) open import Data.Bool using (if_then_else_) open import Data.Fin using (Fin;zero;suc) open import Data.Nat using (ℕ;zero;suc;_+_) open import Data.Nat.Properties using (+-assoc;+-identityʳ) open import Data.Nat.Show using () renaming (show to showℕ) open import Data.Integer using (ℤ;∣_∣) open import Data.Float using (Float;fromℕ;_÷_;_≤ᵇ_) renaming (show to show𝔽;_*_ to _*f_) import Data.List as L open import Data.Maybe using (Maybe;just;nothing;maybe′;fromMaybe) renaming (map to mapMaybe; _>>=_ to _>>=m_ ) open import Data.Product using () renaming (_,_ to _,,_) open import Data.String using (String;_++_;padLeft;padRight;length) open import Data.Vec using (Vec;replicate;[];_∷_;foldr) open import Algebra using (IsMonoid) open import Relation.Nullary using (yes;no) open import Relation.Binary.PropositionalEquality using (_≡_;refl;isEquivalence;cong₂) open import Text.Printf using (printf) open import Relation.Binary using (StrictTotalOrder) open import Data.Char using (_≈ᵇ_) open import Data.String.Properties using (<-strictTotalOrder-≈) open import Data.Tree.AVL.Map <-strictTotalOrder-≈ as AVL using (Map;empty;unionWith;singleton) renaming (lookup to lookupAVL) open import Utils using (_×_;_,_) open import Builtin using (Builtin;showBuiltin;builtinList;arity) open Builtin.Builtin open import Builtin.Signature using (_⊢♯) open _⊢♯ open import Builtin.Constant.AtomicType using (AtomicTyCon) open AtomicTyCon open import Cost.Base open import Cost.Size using (defaultValueMeasure) open import Cost.Model open import Cost.Raw open import Untyped.CEK using (Value;V-con)
An execution budget consist of two costs: CPU and memory costs.
record ExBudget : Set where constructor mkExBudget field ExCPU : CostingNat -- CPU usage ExMem : CostingNat -- Memory usage open ExBudget fromHExBudget : HExBudget → ExBudget fromHExBudget hb = mkExBudget (getCPUCost hb) (getMemoryCost hb)
The type for execution budget should be a Monoid.
We show that this is the case for ExBudget
.
-- unit of the monoid ε€ : ExBudget ε€ = mkExBudget 0 0 -- binary operation _∙€_ : ExBudget → ExBudget → ExBudget (mkExBudget xCPU xMem) ∙€ (mkExBudget yCPU yMem) = mkExBudget (xCPU + yCPU) (xMem + yMem) -- Note: working with `Monoid` instances would imply working in Set₁, so we avoid it -- and just state that `ExBudget` is a Monoid isMonoidExBudget : IsMonoid _≡_ _∙€_ ε€ isMonoidExBudget = record { isSemigroup = record { isMagma = record { isEquivalence = isEquivalence ; ∙-cong = λ {refl refl → refl }} ; assoc = λ x y z → cong₂ mkExBudget (+-assoc (ExCPU x) (ExCPU y) (ExCPU z)) (+-assoc (ExMem x) (ExMem y) (ExMem z)) } ; identity = (λ x → refl) ,, λ x → cong₂ mkExBudget (+-identityʳ (ExCPU x)) (+-identityʳ (ExMem x)) }
To calculate the cost of a builtin we obtain the corresponding builtin model, and run the cpu and memory model using the vector of argument sizes.
builtinCost : (b : Builtin) → BuiltinModel (arity b) → Vec Value (arity b) → ExBudget builtinCost b bc cs = mkExBudget (runModel (costingCPU bc) cs) (runModel (costingMem bc) cs)
The machine parameters for ExBudget
for a given Cost Model
CostModel = HCekMachineCosts × ModelAssignment cekMachineCostFunction : HCekMachineCosts → StepKind → ExBudget cekMachineCostFunction mc BConst = fromHExBudget (getCekConstCost mc) cekMachineCostFunction mc BVar = fromHExBudget (getCekVarCost mc) cekMachineCostFunction mc BLamAbs = fromHExBudget (getCekLamCost mc) cekMachineCostFunction mc BApply = fromHExBudget (getCekApplyCost mc) cekMachineCostFunction mc BDelay = fromHExBudget (getCekDelayCost mc) cekMachineCostFunction mc BForce = fromHExBudget (getCekForceCost mc) cekMachineCostFunction mc BBuiltin = fromHExBudget (getCekBuiltinCost mc) cekMachineCostFunction mc BConstr = fromHExBudget (getCekConstCost mc) cekMachineCostFunction mc BCase = fromHExBudget (getCekCaseCost mc) exBudgetCategoryCost : CostModel → ExBudgetCategory → ExBudget exBudgetCategoryCost (cekMc , _) (BStep x) = cekMachineCostFunction cekMc x exBudgetCategoryCost (_ , ma) (BBuiltinApp b cs) = builtinCost b (ma b) cs exBudgetCategoryCost (cekMc , _) BStartup = fromHExBudget (getCekStartupCost cekMc) machineParameters : CostModel → MachineParameters ExBudget machineParameters costmodel = record { cekMachineCost = exBudgetCategoryCost costmodel ; ε = ε€ ; _∙_ = _∙€_ ; costMonoid = isMonoidExBudget } countingReport : ExBudget → String countingReport (mkExBudget cpu mem) = "\nCPU budget: " ++ showℕ cpu ++ "\nMemory budget: " ++ showℕ mem
## Tallying budget
These functions define a type for Budgets that can record detailed cost information about nodes and builtins.
We need a map from ExBudgetCategory
into ExBudget
.
It’s not the most efficient, but the simplest thing to do is to
transform ExBudgetCategory
into a string, and use that as keys.
mkKeyFromExBudgetCategory : ExBudgetCategory → String mkKeyFromExBudgetCategory (BStep x) = "0" ++ showStepKind x mkKeyFromExBudgetCategory (BBuiltinApp x _) = "1"++ showBuiltin x mkKeyFromExBudgetCategory BStartup = "2" TallyingBudget : Set TallyingBudget = Map ExBudget × ExBudget lookup : Map ExBudget → ExBudgetCategory → ExBudget lookup m k with lookupAVL m (mkKeyFromExBudgetCategory k) ... | just x = x ... | nothing = ε€
As required, TallyingBudget
is a monoid.
--unit of TallyingBudget εT : TallyingBudget εT = empty , ε€ -- adding TallyingBudgets _∙T_ : TallyingBudget → TallyingBudget → TallyingBudget (m , x) ∙T (n , y) = unionWith u m n , (x ∙€ y) where u : ExBudget → Maybe (ExBudget) → ExBudget u x (just y) = x ∙€ y u x nothing = x -- TODO : Prove these postulates. postulate TallyingBudget-assoc : Algebra.Associative _≡_ _∙T_ postulate Tallying-budget-identityʳ : Algebra.RightIdentity _≡_ εT _∙T_ isMonoidTallyingBudget : IsMonoid _≡_ _∙T_ εT isMonoidTallyingBudget = record { isSemigroup = record { isMagma = record { isEquivalence = isEquivalence ; ∙-cong = λ {refl refl → refl }} ; assoc = TallyingBudget-assoc } ; identity = (λ x → refl) ,, Tallying-budget-identityʳ } tallyingCekMachineCost : CostModel → ExBudgetCategory → TallyingBudget tallyingCekMachineCost cm k = let spent = exBudgetCategoryCost cm k in singleton (mkKeyFromExBudgetCategory k) spent , spent tallyingMachineParameters : CostModel → MachineParameters TallyingBudget tallyingMachineParameters cm = record { cekMachineCost = tallyingCekMachineCost cm ; ε = εT ; _∙_ = _∙T_ ; costMonoid = isMonoidTallyingBudget } tallyingReport : TallyingBudget → String tallyingReport (mp , budget) = countingReport budget ++ "\n" ++ "\n" ++ printStepReport mp ++ "\n" ++ "startup " ++ budgetToString (lookup mp BStartup) ++ "\n" ++ "compute " ++ budgetToString totalComputeCost ++ "\n" -- ++ "AST nodes " ++ ++ "\n" ++ "\n\n" ++ printBuiltinReport mp ++ "\n" ++ "Total builtin costs: " ++ budgetToString totalBuiltinCosts ++ "\n" -- We would like to be able to print the following number as "%4.2f" -- but Agda's printf currently doesn't support it. ++ printf "Time spent executing builtins: %f%%\n" (fromℕ 100 *f (getCPU totalBuiltinCosts) ÷ (getCPU budget)) ++ "\n" ++ "\n" ++ "Total budget spent: " ++ budgetToString budget ++ "\n" ++ "Predicted execution time: " ++ formatTimePicoseconds (getCPU budget) where totalComputeCost totalBuiltinCosts : ExBudget totalComputeCost = L.foldr (λ x acc → (lookup mp (BStep x)) ∙€ acc) ε€ stepKindList totalBuiltinCosts = L.foldr _∙€_ ε€ (L.map (lookup mp ∘ (λ b → BBuiltinApp b (replicate (arity b) (V-con (atomic aUnit) tt)))) builtinList) getCPU : ExBudget → Float getCPU n = fromℕ (ExCPU n) budgetToString : ExBudget → String budgetToString (mkExBudget cpu mem) = padLeft ' ' 15 (showℕ cpu) ++ " " ++ padLeft ' ' 15 (showℕ mem) printStepCost : StepKind → ExBudget → String printStepCost sk budget = padRight ' ' 10 (showStepKind sk) ++ " " ++ padLeft ' ' 20 (budgetToString budget) ++ "\n" printStepReport : Map ExBudget → String printStepReport mp = L.foldr (λ s xs → printStepCost s (lookup mp (BStep s)) ++ xs) "" stepKindList printBuiltinCost : Builtin → ExBudget → String printBuiltinCost b (mkExBudget 0 0) = "" printBuiltinCost b budget = padRight ' ' 22 (showBuiltin b) ++ " " ++ budgetToString budget ++ "\n" printBuiltinReport : Map ExBudget → String printBuiltinReport mp = L.foldr (λ b xs → printBuiltinCost b (lookup mp (BBuiltinApp b (replicate (arity b) (V-con (atomic aUnit) tt)))) ++ xs) "" builtinList formatTimePicoseconds : Float → String formatTimePicoseconds t = if 1e12 ≤ᵇ t then (printf "%f s" (t ÷ 1e12)) else if 1e9 ≤ᵇ t then (printf "%f ms" (t ÷ 1e9)) else if 1e6 ≤ᵇ t then (printf "%f μs" (t ÷ 1e6)) else if 1e3 ≤ᵇ t then (printf "%f ns" (t ÷ 1e3)) else printf "%f ps" t