See also: mim::plug::mem

Dependencies

import compile;

Types

M

This type tracks all kinds of side effects in the given address space.

axm M: Nat → *;

Ptr

Pointer type with pointee type T and address space a. At the moment, the address space is not really used and serves as a placeholder for future work.

axm Ptr: [*, Nat] → *;
 
anx lam Ptr0(T: *): * = Ptr (T, 0);

Operations w/ Side Effects

The following operations have side effects. For this reason, they consume a mem.M a and yield a new mem.M a.

load

Loads the pointee of type T from a pointer of type mem.Ptr (T, a).

axm load: {T: *, a: Nat} as Ta → [M a, Ptr Ta] → [M a, T], normalize_load;

store

Stores a value of type T to the location pointed to by a pointer of type mem.Ptr (T, a).

axm store: {T: *, a: Nat} as Ta → [M a, Ptr Ta, T] → M a, normalize_store;

remem

Creates a new dummy mem.M a-typed value in order to acknowledge the fact that some unspecified side-effect happened.

axm remem: {a: Nat} → M a → M a, normalize_remem;

fresh

Passes a fresh mem.M a for address space a to its return continuation: ret mem = mem.fresh $ 0. Conversion-only phases (e.g. tensor.lower_to_mem) emit memory operations before memory has been threaded. Each call site's return continuation is a distinct mutable, so the received memories are distinct by construction - hash-consing cannot collapse two otherwise identical memory operations into one. mem.add_mem resolves each call by jumping to the continuation with the memory that is current at that point.

axm fresh: Fn [a: Nat] → M a;

alloc

Allocates memory of type T in address space a.

axm alloc: [*, a: Nat] as Ta → [M a] → [M a, Ptr Ta];

slot

Reserves a stack slot for type T in address space a. The slot is passed to the continuation and its lifetime is scoped to that continuation.

axm slot: [*, a: Nat] as Ta → Fn M a → [M a, Ptr Ta];

malloc

Allocates memory of type T in address space a. The difference to mem.alloc is that the size is passed explicitly (in bytes) instead of being derived from T.

axm malloc: [*, a: Nat] as Ta → [M a, Nat] → [M a, Ptr Ta];

free

Frees memory of type T in address space a.

axm free: {*, a: Nat} as Ta → [M a, Ptr Ta] → M a;

mslot

Reserves a stack slot for type T in address space a. The reserved slot will be size bytes large. The slot is passed to the continuation and its lifetime is scoped to that continuation.

axm mslot: [*, a: Nat] as Ta → Fn [M a, size: Nat] → [M a, Ptr Ta];

Operations w/o Side Effects

lea

Load effective address. Performs address computation by offsetting the passed pointer with index i.

axm lea: {n: Nat, Ts: «n; *», a: Nat} → [Ptr («j: n; Ts#j», a), i: Idx n] → Ptr (Ts#i, a), normalize_lea;

Phases

add_mem

Threads mem.M through functions that lack it.

axm add_mem: compile.Phase;

seo

Symbolic Expression Optimization — SSA construction, expression propagation, and GVN in one fixed point (see mim::plug::mem::phase::SEO).

axm seo: compile.Phase;

remem_repl

Removes mem.remems.

axm remem_repl: compile.Phase;

alloc2malloc_repl

Rewrites mem.alloc / mem.slot into mem.malloc / mem.mslot.

axm alloc2malloc_repl: compile.Phase;