cookcu talk

An Example of Program Analysis: Inserting Safe Memory Re-use Commands into ML-like Programs: 

An Example of Program Analysis: Inserting Safe Memory Re-use Commands into ML-like Programs Oukseh Lee, Hongseok Yang, and Kwangkeun Yi {cookcu; hyang; kwang}@ropas.kaist.ac.kr Research On Program Analysis System, KAIST http://ropas.kaist.ac.kr December 5, 2002 CS520

Motivation (1/2): 

Motivation (1/2) Thanks to many compilation techniques, ML can produce fast code, but still has the overhead for managing the memory. Garbage collection is usually faster than the manual memory management. Then what is the reason of the memory inefficiency?

Motivation (2/2): 

Motivation (2/2) Unnecessary allocation in ML programs: 1 2 3 5 6 fun insert i l = case l of [] =andgt; i::[] | h::t =andgt; if iandlt;h then i::l else let z = insert i t in h::z

Our Goal: 

Our Goal To insert safe memory-reuse commands: 1 2 6 fun insert i l = case l of [] =andgt; i::[] | h::t =andgt; if iandlt;h then i::l else let z = insert i t in (free l; h::z) 4 3 5

How to Find it? : 

How to Find it? By an accurate but effective program analysis: Individual heap-cell as the unit of analysis. Context pruning at the conditional branches. Keeping sharing information using multi-set formula. Parameterized analysis, so poly-variance at function calls. Deallocation inside a function can be conditioned by extra boolean parameters (called dynamic flags).

Experimental Result: 

Experimental Result

Example: copyright: 

Example: copyright free a? fun copyright a = case a of Leaf =andgt; Leaf | Node(a1,a2) =andgt; let r = copyright a2 in Node(a1, r) Tree a will not be used later

Key: Precise Separation: 

# all left subtrees Key: Precise Separation Tree a will not be used later fun copyright a = case a of Leaf =andgt; Leaf | Node(a1,a2) =andgt; let r = copyright a2 in Node(a1, r) free a?

Safe Only Under the Assumption: 

Safe Only Under the Assumption fun copyright a = case a of Leaf =andgt; Leaf | Node(a1,a2) =andgt; let r = copyright a2 in (free a; Node(a1, r)) Tree a will not be used later Tree a has no shared sub-parts X

Passing the Assumption in Run-time: 

Passing the Assumption in Run-time fun copyright [b,bs] a = case a of Leaf =andgt; Leaf | Node(a1,a2) =andgt; let r = copyright [bÆ:bs,bs] a2 in (free a when b; Node(a1, r))

Input Language: 

Input Language

Output Language: 

Output Language

First Step: 

First Step Memory-usage analysis: Computes the memory-type (abstraction of heap objects) and usage for each expression. free-commands insertion: Inserts free-commands and adds dynamic flags using the result from the memory-usage analysis.

How to Represent a Set of Heap Objects?: 

How to Represent a Set of Heap Objects? let x = ... in ...

A Set of Locations (NO!): 

A Set of Locations (NO!) Not enough for sharing information. x = Node(Leaf,Leaf) y = Node(x,x) x = Node(Leaf,Leaf) y = Node(x,Leaf) x y

Multi-set Formula: 

Multi-set Formula Describes a set of locations with sharing information: note:

Memory-Type for a Tree: 

Memory-Type for a Tree Describes a set of trees: note: left right root

Memory-Type for a Function: 

Memory-Type for a Function Describes the behavior of the function. The memory-type of function copyright is: result usage input new

Analysis: 

fun copyright a = case a of Leaf =andgt; Leaf | Node(a1,a2) =andgt; let r = copyright a2 in Node(a1, r) Analysis

Second Step: 

Second Step Memory-usage analysis: Computes the memory-type and usage for each expression. free-commands insertion: Inserts free-commands and adds dynamic flags using the result from the memory-usage analysis.

Insertion (1/3): 

fun copyright [b,bs] a = case a of Leaf =andgt; Leaf | Node(a1,a2) =andgt; let r = copyright a2 in Node (a1, r) Insertion (1/3) b: it is safe to free the input (excluding the result) bs: the input may have shared sub-parts.

Insertion (2/3): 

Insertion (2/3) :bs fun copyright [b,bs] a = case a of Leaf =andgt; Leaf | Node(a1,a2) =andgt; let r = copyright a2 in Node (a1, r) b

Insertion (3/3): 

fun copyright [b,bs] a = case a of Leaf =andgt; Leaf | Node(a1,a2) =andgt; let r = copyright [bÆ:bs,bs] a2 in Node (a1, r) Insertion (3/3) b true true

Result: 

Result fun copyright [b,bs] a = case a of Leaf =andgt; Leaf | Node(a1,a2) =andgt; let r = copyright [bÆ:bs,bs] a2 in (free a when b; Node (a1, r))

Conclusion: 

Conclusion We present a static analysis and source-level transformation for inserting safe memory-reuse commands. Reuse ratio: 5.2-98.7% Analysis cost: 415-4500 lines/sec Weak for prevalent sharing but enough for usual cases. Plan to apply this analysis to our nML compiler.