Memory allocation and arrays on the word RAM

Algorithms on the word RAM keep their arrays in memory. This file provides, as ordinary structured programs with exact instruction counts:

• Cslib.WordRAM.zeroFill: zeroing a range of cells, in 4 k + 2 instructions for k cells;
• Cslib.WordRAM.alloc: allocating a zeroed block of k cells at a frontier that only grows, in 4 k + 7 instructions. Addresses are never reused, so blocks allocated at different times are disjoint (Cslib.WordRAM.Block.disjoint_of_le); the frontier is the high-water mark of the memory used;
• Cslib.WordRAM.readAt, Cslib.WordRAM.writeAt: reading and writing the cell at a pointer plus an index, in two instructions each.

None of them adds an instruction to the machine: allocation is a loop of stores, and an indexed access is an addition followed by a load or a store. The registers they use are parameters, and Cslib.WordRAM.Block.Realizes relates the contents of a block to a function on its indices.

Main definitions

• Cslib.WordRAM.Block: a block of consecutive cells; Cslib.WordRAM.clear: memory with a range of cells set to 0.
• Cslib.WordRAM.zeroFill, Cslib.WordRAM.alloc, Cslib.WordRAM.readAt, Cslib.WordRAM.writeAt: the programs.

Main results

• Cslib.WordRAM.zeroFill_exec, Cslib.WordRAM.alloc_exec, Cslib.WordRAM.readAt_exec, Cslib.WordRAM.writeAt_exec: their executions, with exact instruction counts.

References

• MIT–ULB CompGeom Group, Undecidability of tiling with a tromino; allocation by a frontier, the zeroing loop and indexed access are adapted from its accompanying Lean formalization.

Blocks of memory

structure Cslib.WordRAM.Block : Type

A block of length consecutive memory cells starting at address base.

• base : ℕ

  The address of the first cell.

• length : ℕ

  The number of cells.

theorem Cslib.WordRAM.Block.ext_iff {x y : Block} : x = y ↔ x.base = y.base ∧ x.length = y.length

theorem Cslib.WordRAM.Block.ext {x y : Block} (base : x.base = y.base) (length : x.length = y.length) : x = y

@[instance_reducible]

instance Cslib.WordRAM.instDecidableEqBlock : DecidableEq Block

def Cslib.WordRAM.instDecidableEqBlock.decEq (x✝ x✝¹ : Block) : Decidable (x✝ = x✝¹)

def Cslib.WordRAM.instReprBlock.repr : Block → ℕ → Std.Format

@[instance_reducible]

instance Cslib.WordRAM.instReprBlock : Repr Block

def Cslib.WordRAM.Block.Owns (b : Block) (a : ℕ) : Prop

The block contains the cell at address a.

def Cslib.WordRAM.Block.read (b : Block) (m : ℕ → ℕ) (i : Fin b.length) : ℕ

The contents of the block's cells in memory m, indexed from 0.

def Cslib.WordRAM.Block.Realizes (b : Block) (m : ℕ → ℕ) (vs : Fin b.length → ℕ) : Prop

The block holds the values vs in memory m.

theorem Cslib.WordRAM.Block.disjoint_of_le {b : Block} {frontier k : ℕ} (hb : b.base + b.length ≤ frontier) {a : ℕ} (ha : b.Owns a) : ¬{ base := frontier, length := k }.Owns a

A block below the frontier is disjoint from any block allocated at the frontier.

theorem Cslib.WordRAM.Block.Realizes.update {b : Block} {m : ℕ → ℕ} {vs : Fin b.length → ℕ} (h : b.Realizes m vs) (i : Fin b.length) (v : ℕ) : b.Realizes (Function.update m (b.base + ↑i) v) (Function.update vs i v)

Writing a cell of the block updates the value at its index.

theorem Cslib.WordRAM.Block.Realizes.update_of_not_owns {b : Block} {m : ℕ → ℕ} {vs : Fin b.length → ℕ} (h : b.Realizes m vs) {a : ℕ} (ha : ¬b.Owns a) (v : ℕ) : b.Realizes (Function.update m a v) vs

Writing a cell outside the block leaves its contents unchanged.

def Cslib.WordRAM.clear (m : ℕ → ℕ) (base k : ℕ) : ℕ → ℕ

Memory m with the k cells from address base set to 0.

theorem Cslib.WordRAM.clear_of_owns {m : ℕ → ℕ} {base k a : ℕ} (h : { base := base, length := k }.Owns a) : clear m base k a = 0

theorem Cslib.WordRAM.clear_of_not_owns {m : ℕ → ℕ} {base k a : ℕ} (h : ¬{ base := base, length := k }.Owns a) : clear m base k a = m a

@[simp]

theorem Cslib.WordRAM.clear_zero (m : ℕ → ℕ) (base : ℕ) : clear m base 0 = m

theorem Cslib.WordRAM.clear_succ (m : ℕ → ℕ) (base k : ℕ) : clear m base (k + 1) = Function.update (clear m base k) (base + k) 0

theorem Cslib.WordRAM.Block.realizes_clear (m : ℕ → ℕ) (base k : ℕ) : { base := base, length := k }.Realizes (clear m base k) fun (x : Fin { base := base, length := k }.length) => 0

A cleared block holds zeros.

Zeroing a range of cells

def Cslib.WordRAM.zeroFill {r : ℕ} (cur stop zero one : Fin r) : Code Basis.standard r

Zero the cells from the address in register cur up to the address in register stop, counting cur up to stop; registers zero and one hold 0 and 1.

theorem Cslib.WordRAM.zeroFill_exec {r w : ℕ} {cur stop zero one : Fin r} {x : Data r} (hcs : cur ≠ stop) (hcz : cur ≠ zero) (hco : cur ≠ one) (h0 : x.regs zero = 0) (h1 : x.regs one = 1) (hle : x.regs cur ≤ x.regs stop) (hw : Fits w (x.regs stop)) : Exec w (zeroFill cur stop zero one) x { regs := Function.update x.regs cur (x.regs stop), mem := clear x.mem (x.regs cur) (x.regs stop - x.regs cur) } (4 * (x.regs stop - x.regs cur) + 2)

Zeroing k cells takes 4 k + 2 instructions: a store, an addition, a branch and a jump per cell, and a branch and a jump to leave the loop.

Allocation

def Cslib.WordRAM.alloc {r : ℕ} (frontier count result cur zero one : Fin r) : Code Basis.standard r

Allocate a zeroed block of as many cells as register count holds, at the address in register frontier: the address of the block is left in register result, and frontier advances past the block. Registers cur, zero and one are scratch.

theorem Cslib.WordRAM.alloc_exec {r w : ℕ} {frontier count result cur zero one : Fin r} {x : Data r} (hd : [frontier, count, result, cur, zero, one].Nodup) (h1 : Fits w 1) (hw : Fits w (x.regs frontier + x.regs count)) : Exec w (alloc frontier count result cur zero one) x { regs := Function.update (Function.update (Function.update (Function.update (Function.update x.regs zero 0) one 1) result (x.regs frontier)) frontier (x.regs frontier + x.regs count)) cur (x.regs frontier + x.regs count), mem := clear x.mem (x.regs frontier) (x.regs count) } (4 * x.regs count + 7)

Allocation. Allocating a zeroed block of k cells at frontier f takes 4 k + 7 instructions. It sets result to f and frontier and cur to f + k, zero and one to 0 and 1, zeroes the cells f, …, f + k - 1, and leaves all other registers and cells unchanged.

Arrays

def Cslib.WordRAM.readAt {r : ℕ} (tmp dst ptr idx : Fin r) : Code Basis.standard r

dst ← (ptr)[idx]: load the cell at the address in ptr plus the index in idx, through the scratch register tmp.

def Cslib.WordRAM.writeAt {r : ℕ} (tmp ptr idx src : Fin r) : Code Basis.standard r

(ptr)[idx] ← src: store register src to the cell at the address in ptr plus the index in idx, through the scratch register tmp.

theorem Cslib.WordRAM.readAt_exec {r w : ℕ} {tmp dst ptr idx : Fin r} {x : Data r} (h : Fits w (x.regs ptr + x.regs idx)) : Exec w (readAt tmp dst ptr idx) x ((x.set tmp (x.regs ptr + x.regs idx)).set dst (x.mem (x.regs ptr + x.regs idx))) 2

An indexed read takes two instructions.

theorem Cslib.WordRAM.writeAt_exec {r w : ℕ} {tmp ptr idx src : Fin r} {x : Data r} (hs : src ≠ tmp) (h : Fits w (x.regs ptr + x.regs idx)) : Exec w (writeAt tmp ptr idx src) x ((x.set tmp (x.regs ptr + x.regs idx)).write (x.regs ptr + x.regs idx) (x.regs src)) 2

An indexed write takes two instructions; the stored register must differ from the scratch register.

Additive-basis primitives

def Cslib.WordRAM.Op.addAdditive {r : ℕ} (d i j : Fin r) : Op Basis.additive r

addAdditive d i j sets register d to register i plus register j over Basis.additive.

def Cslib.WordRAM.zeroFillAdditive {r : ℕ} (cur stop zero one : Fin r) : Code Basis.additive r

Zero the cells from the address in register cur up to the address in register stop over Basis.additive.

def Cslib.WordRAM.allocAdditive {r : ℕ} (frontier count result cur zero one : Fin r) : Code Basis.additive r

Allocate a zeroed block of count cells at frontier over Basis.additive.

def Cslib.WordRAM.readAtAdditive {r : ℕ} (tmp dst ptr idx : Fin r) : Code Basis.additive r

dst ← (ptr)[idx] over Basis.additive.

def Cslib.WordRAM.writeAtAdditive {r : ℕ} (tmp ptr idx src : Fin r) : Code Basis.additive r

(ptr)[idx] ← src over Basis.additive.