Module comments for reset-reuse

Figuring out what this module was doing, and why, took me a bit less
than half an hour. We should document what's happening for others in the
future so they don't need to follow up on Zulip necessarily.
This commit is contained in:
ayazhafiz 2022-01-10 20:16:56 -05:00
parent 76d4d5d664
commit e655ab7d3b
62 changed files with 563 additions and 551 deletions

View file

@ -1,3 +1,18 @@
//! This module inserts reset/reuse statements into the mono IR. These statements provide an
//! opportunity to reduce memory pressure by reusing memory slots of non-shared values. From the
//! introduction of the relevant paper:
//!
//! > [We] have added two additional instructions to our IR: `let y = reset x` and
//! > `let z = (reuse y in ctor_i w)`. The two instructions are used together; if `x`
//! > is a shared value, then `y` is set to a special reference, and the reuse instruction
//! > just allocates a new constructor value `ctor_i w`. If `x` is not shared, then reset
//! > decrements the reference counters of the components of `x`, and `y` is set to `x`.
//! > Then, reuse reuses the memory cell used by `x` to store the constructor value `ctor_i w`.
//!
//! See also
//! - [Counting Immutable Beans](https://arxiv.org/pdf/1908.05647.pdf) (Ullrich and Moura, 2020)
//! - [The lean implementation](https://github.com/leanprover/lean4/blob/master/src/Lean/Compiler/IR/ResetReuse.lean)
use crate::inc_dec::{collect_stmt, occurring_variables_expr, JPLiveVarMap, LiveVarSet};
use crate::ir::{
BranchInfo, Call, Expr, ListLiteralElement, Proc, Stmt, UpdateModeId, UpdateModeIds,