feat: add latest run from yday

1-runs/.gitignore

@@ -1,2 +1 @@
-*.csv
 

1-runs/run-2023-03-29---20-19---tcg40/README

@@ -0,0 +1,2 @@
+- Run stage2 normally, then time the compile of stage3. Also track file sizes to compare between baseline and reused compiler.
+

1-runs/run-2023-03-29---20-19---tcg40/ResetReuse.baseline.lean.in

@@ -0,0 +1,161 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Compiler.IR.Basic
+import Lean.Compiler.IR.LiveVars
+import Lean.Compiler.IR.Format
+
+
+namespace Lean.IR.ResetReuse
+/-! Remark: the insertResetReuse transformation is applied before we have
+   inserted `inc/dec` instructions, and performed lower level optimizations
+   that introduce the instructions `release` and `set`. -/
+
+/-! Remark: the functions `S`, `D` and `R` defined here implement the
+  corresponding functions in the paper "Counting Immutable Beans"
+
+  Here are the main differences:
+  - We use the State monad to manage the generation of fresh variable names.
+  - Support for join points, and `uset` and `sset` instructions for unboxed data.
+  - `D` uses the auxiliary function `Dmain`.
+  - `Dmain` returns a pair `(b, found)` to avoid quadratic behavior when checking
+    the last occurrence of the variable `x`.
+  - Because we have join points in the actual implementation, a variable may be live even if it
+    does not occur in a function body. See example at `livevars.lean`.
+-/
+
+private def mayReuse (c₁ c₂ : CtorInfo) : Bool :=
+  c₁.size == c₂.size && c₁.usize == c₂.usize && c₁.ssize == c₂.ssize &&
+  /- The following condition is a heuristic.
+     We don't want to reuse cells from different types even when they are compatible
+     because it produces counterintuitive behavior. -/
+  (c₁.name.getPrefix == c₂.name.getPrefix)
+
+private partial def S (w : VarId) (c : CtorInfo) : FnBody → FnBody
+  | FnBody.vdecl x t v@(Expr.ctor c' ys) b   =>
+    if mayReuse c c' then
+      let updtCidx := c.cidx != c'.cidx
+      FnBody.vdecl x t (Expr.reuse w c' updtCidx ys) b
+    else
+      FnBody.vdecl x t v (S w c b)
+  | FnBody.jdecl j ys v b   =>
+    let v' := S w c v
+    if v == v' then FnBody.jdecl j ys v (S w c b)
+    else FnBody.jdecl j ys v' b
+  | FnBody.case tid x xType alts    => FnBody.case tid x xType <| alts.map fun alt => alt.modifyBody (S w c)
+  | b =>
+    if b.isTerminal then b
+    else let
+      (instr, b) := b.split
+      instr.setBody (S w c b)
+
+/-- We use `Context` to track join points in scope. -/
+abbrev M := ReaderT LocalContext (StateT Index Id)
+
+private def mkFresh : M VarId := do
+  let idx ← getModify (fun n => n + 1)
+  pure { idx := idx }
+
+private def tryS (x : VarId) (c : CtorInfo) (b : FnBody) : M FnBody := do
+  let w ← mkFresh
+  let b' := S w c b
+  if b == b' then pure b
+  else pure $ FnBody.vdecl w IRType.object (Expr.reset c.size x) b'
+
+private def Dfinalize (x : VarId) (c : CtorInfo) : FnBody × Bool → M FnBody
+  | (b, true)  => pure b
+  | (b, false) => tryS x c b
+
+private def argsContainsVar (ys : Array Arg) (x : VarId) : Bool :=
+  ys.any fun arg => match arg with
+    | Arg.var y => x == y
+    | _         => false
+
+private def isCtorUsing (b : FnBody) (x : VarId) : Bool :=
+  match b with
+  | (FnBody.vdecl _ _ (Expr.ctor _ ys) _) => argsContainsVar ys x
+  | _ => false
+
+/-- Given `Dmain b`, the resulting pair `(new_b, flag)` contains the new body `new_b`,
+   and `flag == true` if `x` is live in `b`.
+
+   Note that, in the function `D` defined in the paper, for each `let x := e; F`,
+   `D` checks whether `x` is live in `F` or not. This is great for clarity but it
+   is expensive: `O(n^2)` where `n` is the size of the function body. -/
+private partial def Dmain (x : VarId) (c : CtorInfo) : FnBody → M (FnBody × Bool)
+  | e@(FnBody.case tid y yType alts) => do
+    let ctx ← read
+    if e.hasLiveVar ctx x then do
+      /- If `x` is live in `e`, we recursively process each branch. -/
+      let alts ← alts.mapM fun alt => alt.mmodifyBody fun b => Dmain x c b >>= Dfinalize x c
+      pure (FnBody.case tid y yType alts, true)
+    else pure (e, false)
+  | FnBody.jdecl j ys v b   => do
+    let (b, found) ← withReader (fun ctx => ctx.addJP j ys v) (Dmain x c b)
+    let (v, _ /- found' -/) ← Dmain x c v
+    /- If `found' == true`, then `Dmain b` must also have returned `(b, true)` since
+       we assume the IR does not have dead join points. So, if `x` is live in `j` (i.e., `v`),
+       then it must also live in `b` since `j` is reachable from `b` with a `jmp`.
+       On the other hand, `x` may be live in `b` but dead in `j` (i.e., `v`). -/
+    pure (FnBody.jdecl j ys v b, found)
+  | e => do
+    let ctx ← read
+    if e.isTerminal then
+      pure (e, e.hasLiveVar ctx x)
+    else do
+      let (instr, b) := e.split
+      if isCtorUsing instr x then
+        /- If the scrutinee `x` (the one that is providing memory) is being
+           stored in a constructor, then reuse will probably not be able to reuse memory at runtime.
+           It may work only if the new cell is consumed, but we ignore this case. -/
+        pure (e, true)
+      else
+        let (b, found) ← Dmain x c b
+        /- Remark: it is fine to use `hasFreeVar` instead of `hasLiveVar`
+           since `instr` is not a `FnBody.jmp` (it is not a terminal) nor it is a `FnBody.jdecl`. -/
+        if found || !instr.hasFreeVar x then
+          pure (instr.setBody b, found)
+        else
+          let b ← tryS x c b
+          pure (instr.setBody b, true)
+
+private def D (x : VarId) (c : CtorInfo) (b : FnBody) : M FnBody :=
+  Dmain x c b >>= Dfinalize x c
+
+partial def R : FnBody → M FnBody
+  | FnBody.case tid x xType alts   => do
+      let alts ← alts.mapM fun alt => do
+        let alt ← alt.mmodifyBody R
+        match alt with
+        | Alt.ctor c b =>
+          if c.isScalar then pure alt
+          else Alt.ctor c <$> D x c b
+        | _            => pure alt
+      pure $ FnBody.case tid x xType alts
+  | FnBody.jdecl j ys v b   => do
+    let v ← R v
+    let b ← withReader (fun ctx => ctx.addJP j ys v) (R b)
+    pure $ FnBody.jdecl j ys v b
+  | e => do
+    if e.isTerminal then pure e
+    else do
+      let (instr, b) := e.split
+      let b ← R b
+      pure (instr.setBody b)
+
+end ResetReuse
+
+open ResetReuse
+
+def Decl.insertResetReuse (d : Decl) : Decl :=
+  match d with
+  | .fdecl (body := b) ..=>
+    let nextIndex := d.maxIndex + 1
+    let bNew      := (R b {}).run' nextIndex
+    d.updateBody! bNew
+  | other => other
+
+end Lean.IR

1-runs/run-2023-03-29---20-19---tcg40/ResetReuse.research.lean.in

@@ -0,0 +1,157 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Compiler.IR.Basic
+import Lean.Compiler.IR.LiveVars
+import Lean.Compiler.IR.Format
+
+
+namespace Lean.IR.ResetReuse
+/-! Remark: the insertResetReuse transformation is applied before we have
+   inserted `inc/dec` instructions, and performed lower level optimizations
+   that introduce the instructions `release` and `set`. -/
+
+/-! Remark: the functions `S`, `D` and `R` defined here implement the
+  corresponding functions in the paper "Counting Immutable Beans"
+
+  Here are the main differences:
+  - We use the State monad to manage the generation of fresh variable names.
+  - Support for join points, and `uset` and `sset` instructions for unboxed data.
+  - `D` uses the auxiliary function `Dmain`.
+  - `Dmain` returns a pair `(b, found)` to avoid quadratic behavior when checking
+    the last occurrence of the variable `x`.
+  - Because we have join points in the actual implementation, a variable may be live even if it
+    does not occur in a function body. See example at `livevars.lean`.
+-/
+
+private def mayReuse (c₁ c₂ : CtorInfo) : Bool :=
+  c₁.size == c₂.size && c₁.usize == c₂.usize && c₁.ssize == c₂.ssize
+
+private partial def S (w : VarId) (c : CtorInfo) : FnBody → FnBody
+  | FnBody.vdecl x t v@(Expr.ctor c' ys) b   =>
+    if mayReuse c c' then
+      let updtCidx := c.cidx != c'.cidx
+      FnBody.vdecl x t (Expr.reuse w c' updtCidx ys) b
+    else
+      FnBody.vdecl x t v (S w c b)
+  | FnBody.jdecl j ys v b   =>
+    let v' := S w c v
+    if v == v' then FnBody.jdecl j ys v (S w c b)
+    else FnBody.jdecl j ys v' b
+  | FnBody.case tid x xType alts    => FnBody.case tid x xType <| alts.map fun alt => alt.modifyBody (S w c)
+  | b =>
+    if b.isTerminal then b
+    else let
+      (instr, b) := b.split
+      instr.setBody (S w c b)
+
+/-- We use `Context` to track join points in scope. -/
+abbrev M := ReaderT LocalContext (StateT Index Id)
+
+private def mkFresh : M VarId := do
+  let idx ← getModify (fun n => n + 1)
+  pure { idx := idx }
+
+private def tryS (x : VarId) (c : CtorInfo) (b : FnBody) : M FnBody := do
+  let w ← mkFresh
+  let b' := S w c b
+  if b == b' then pure b
+  else pure $ FnBody.vdecl w IRType.object (Expr.reset c.size x) b'
+
+private def Dfinalize (x : VarId) (c : CtorInfo) : FnBody × Bool → M FnBody
+  | (b, true)  => pure b
+  | (b, false) => tryS x c b
+
+private def argsContainsVar (ys : Array Arg) (x : VarId) : Bool :=
+  ys.any fun arg => match arg with
+    | Arg.var y => x == y
+    | _         => false
+
+private def isCtorUsing (b : FnBody) (x : VarId) : Bool :=
+  match b with
+  | (FnBody.vdecl _ _ (Expr.ctor _ ys) _) => argsContainsVar ys x
+  | _ => false
+
+/-- Given `Dmain b`, the resulting pair `(new_b, flag)` contains the new body `new_b`,
+   and `flag == true` if `x` is live in `b`.
+
+   Note that, in the function `D` defined in the paper, for each `let x := e; F`,
+   `D` checks whether `x` is live in `F` or not. This is great for clarity but it
+   is expensive: `O(n^2)` where `n` is the size of the function body. -/
+private partial def Dmain (x : VarId) (c : CtorInfo) : FnBody → M (FnBody × Bool)
+  | e@(FnBody.case tid y yType alts) => do
+    let ctx ← read
+    if e.hasLiveVar ctx x then do
+      /- If `x` is live in `e`, we recursively process each branch. -/
+      let alts ← alts.mapM fun alt => alt.mmodifyBody fun b => Dmain x c b >>= Dfinalize x c
+      pure (FnBody.case tid y yType alts, true)
+    else pure (e, false)
+  | FnBody.jdecl j ys v b   => do
+    let (b, found) ← withReader (fun ctx => ctx.addJP j ys v) (Dmain x c b)
+    let (v, _ /- found' -/) ← Dmain x c v
+    /- If `found' == true`, then `Dmain b` must also have returned `(b, true)` since
+       we assume the IR does not have dead join points. So, if `x` is live in `j` (i.e., `v`),
+       then it must also live in `b` since `j` is reachable from `b` with a `jmp`.
+       On the other hand, `x` may be live in `b` but dead in `j` (i.e., `v`). -/
+    pure (FnBody.jdecl j ys v b, found)
+  | e => do
+    let ctx ← read
+    if e.isTerminal then
+      pure (e, e.hasLiveVar ctx x)
+    else do
+      let (instr, b) := e.split
+      if isCtorUsing instr x then
+        /- If the scrutinee `x` (the one that is providing memory) is being
+           stored in a constructor, then reuse will probably not be able to reuse memory at runtime.
+           It may work only if the new cell is consumed, but we ignore this case. -/
+        pure (e, true)
+      else
+        let (b, found) ← Dmain x c b
+        /- Remark: it is fine to use `hasFreeVar` instead of `hasLiveVar`
+           since `instr` is not a `FnBody.jmp` (it is not a terminal) nor it is a `FnBody.jdecl`. -/
+        if found || !instr.hasFreeVar x then
+          pure (instr.setBody b, found)
+        else
+          let b ← tryS x c b
+          pure (instr.setBody b, true)
+
+private def D (x : VarId) (c : CtorInfo) (b : FnBody) : M FnBody :=
+  Dmain x c b >>= Dfinalize x c
+
+partial def R : FnBody → M FnBody
+  | FnBody.case tid x xType alts   => do
+      let alts ← alts.mapM fun alt => do
+        let alt ← alt.mmodifyBody R
+        match alt with
+        | Alt.ctor c b =>
+          if c.isScalar then pure alt
+          else Alt.ctor c <$> D x c b
+        | _            => pure alt
+      pure $ FnBody.case tid x xType alts
+  | FnBody.jdecl j ys v b   => do
+    let v ← R v
+    let b ← withReader (fun ctx => ctx.addJP j ys v) (R b)
+    pure $ FnBody.jdecl j ys v b
+  | e => do
+    if e.isTerminal then pure e
+    else do
+      let (instr, b) := e.split
+      let b ← R b
+      pure (instr.setBody b)
+
+end ResetReuse
+
+open ResetReuse
+
+def Decl.insertResetReuse (d : Decl) : Decl :=
+  match d with
+  | .fdecl (body := b) ..=>
+    let nextIndex := d.maxIndex + 1
+    let bNew      := (R b {}).run' nextIndex
+    d.updateBody! bNew
+  | other => other
+
+end Lean.IR