The mem Plugin

Table of Contents

• Dependencies
• Types
  • %mem.M
  • %mem.Ptr
• Operations w/ Side Effects
  • %mem.load
  • %mem.store
  • %mem.remem
  • %mem.alloc
  • %mem.slot
  • %mem.malloc
  • %mem.free
  • %mem.mslot
• Operations w/o Side Effects
  • %mem.lea
• Stages
  • Phases
  • Repls
  • Passes
    • • mem.reshape
  • Pipelines

See also

mim::plug::mem

Dependencies

import compile;

Types

%mem.M

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

axm %mem.M: Nat → *;

%mem.Ptr

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

axm %mem.Ptr: [*, Nat] → *;
 
lam %mem.Ptr0(T: *): * = %mem.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.

%mem.load

Loads from a pointer of type %mem.Ptr (T, a) the pointed value of type T.

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

%mem.store

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

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

%mem.remem

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

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

%mem.alloc

Allocates memory of type T in address space a.

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

%mem.slot

Reserves a memory slot for type T in address space a. id has to be provided a unique id.

axm %mem.slot: [*, a: Nat] as Ta → [%mem.M a, id: Nat] → [%mem.M a, %mem.Ptr Ta];

%mem.malloc

Allocates memory of type T in address space a. The difference to %mem.alloc is that the size is automatically inferred.

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

%mem.free

Frees memory of type T in address space a.

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

%mem.mslot

Reserves a memory slot for type T in address space a. The reserved slot will be size bytes large. id has to be provided an unique id.

axm %mem.mslot: [*, a: Nat] as Ta → [%mem.M a, size: Nat, id: Nat] → [%mem.M a, %mem.Ptr Ta];

Operations w/o Side Effects

%mem.lea

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

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

Stages

Phases

axm %mem.add_mem_phase: %compile.Phase;

Repls

axm %mem.remem_repl:        %compile.Repl;
axm %mem.alloc2malloc_repl: %compile.Repl;

Passes

axm %mem.ssa_pass:              %compile.Pass;
axm %mem.copy_prop_pass: Bool → %compile.Pass;

mem.reshape

axm %mem.reshape_mode: *;
axm %mem.reshape_flat: %mem.reshape_mode;
axm %mem.reshape_arg:  %mem.reshape_mode;

axm %mem.reshape_pass: %mem.reshape_mode → %compile.Pass;

Pipelines

let mem_opt_passes = %compile.passes (
    //%compile.beta_red_pass,
    //%compile.eta_red_pass ff,
    //%compile.eta_exp_pass,
    %mem.ssa_pass,
    %mem.copy_prop_pass ff,
);