CSE271: Principles of Programming Languages

Garbage Collection

Jooyong Yi (UNIST)

Question

  (value-of 𝑟𝑎𝑡𝑜𝑟 ρ₁ σ₁) = ((proc-val (procedure 𝑣𝑎𝑟 𝑏𝑜𝑑𝑦 ρ₂)), σ₂)                                                   
  (value-of 𝑟𝑎𝑛𝑑 ρ₁ σ₂) = (𝑣𝑎𝑙, σ₃)
---------------------------------------------------------------------------- 𝑙 ∉ dom(σ₃)
  (value-of (call-exp 𝑟𝑎𝑡𝑜𝑟 𝑟𝑎𝑛𝑑) ρ₁ σ₁) = (value-of 𝑏𝑜𝑑𝑦 [𝑣𝑎𝑟=𝑙]ρ₂ [𝑙=𝑣𝑎𝑙]σ₃)

• What happens to 𝑙 ∈ σ₃ once the procedure returns?

Manual Memory Management

[Concrete Syntax]
Expression ::= ...
            | newRef (Expression)
            | deref (Expression)
            | setRef (Expression, Expression)
            | freeRef (Expression)

[Abstract Syntax]
Expression ::= ...
            |  newref-exp (exp)
            |  deref-exp (exp)
            |  setref-exp (exp1 exp2)
            |  freeref-exp (exp)

Spec of freeRef

      (value-of 𝑒𝑥𝑝 ρ σ₀) = (𝑙, σ₁)
--------------------------------------------------
(value-of (freeRef-exp 𝑒𝑥𝑝) ρ σ₀) = (__, [𝑙=⊥]σ₁)

• ([𝑙=⊥]σ₁)(𝑙) = ⊥ (not defined)

Difficulties of Manual Memory Management

• Memory Leak: A memory location is not freed after it is no longer needed.
• Double Free: A memory location is freed more than once.
• Use After Free (Dangling Pointer): A memory location is accessed after it is freed.

Automatic Memory Management: Garbage Collection

1. Pause the program.
2. Identify garbage (memory locations that are no longer accessible).
3. Free the garbage.

Example

begin 
(let f = proc (x) (+ x 1)
 in let a = f 1
    in (+ a 2));
...
end    

• ρ = [f=𝑙₁][a=𝑙₃]
• σ = [𝑙₁=(proc-val (procedure x <<(+ x 1)>> ∅))][𝑙₂=1][𝑙₃=2]

Example

begin 
(let f = proc (x) (+ x 1)
 in let a = f 1
    in (+ a 2));
...
end    

• ρ = [f=𝑙₁][a=𝑙₃]
• σ = [𝑙₁=(proc-val (procedure x <<(+ x 1)>> ∅))][𝑙₂=1][𝑙₃=2]

Mark-and-Sweep Garbage Collection

1. Mark: Identify all accessible memory locations.

begin 
(let f = proc (x) (+ x 1)
 in let a = f 1
    in (+ a 2));
...
end    

• ρ = [f=𝑙₁][a=𝑙₃]
• σ = [𝑙₁=(proc-val (procedure x <<(+ x 1)>> ∅))][𝑙₂=1][𝑙₃=2]

Mark-and-Sweep Garbage Collection

1. Mark: Identify all accessible memory locations.
2. Sweep: Free all unmarked memory locations.

begin 
(let f = proc (x) (+ x 1)
 in let a = f 1
    in (+ a 2));
...
end    

• ρ = [f=𝑙₁][a=𝑙₃]
• σ = [𝑙₁=(proc-val (procedure x <<(+ x 1)>> ∅))][𝑙₂=1][𝑙₃=2]

Mutable Pair

(define-datatype mutpair mutpair?
  (a-pair (left-loc reference?) (right-loc reference?)))

(define make-pair
  (lambda (val1 val2)
    (a-pair (newref val1) (newref val2))))

(define left
  (lambda (p)
    (cases mutpair p
      (a-pair (left-loc right-loc)
        (deref left-loc)))))

(define set-left 
  (lambda (p val)
    (cases mutpair p
      (a-pair (left-loc right-loc)
        (setref! left-loc val)))))

GC Example

ρ = [x = 𝑙₁, y = 𝑙₂]

σ = [𝑙₁ = 1, 
     𝑙₂ = (a-pair (𝑙₄ 𝑙₅)),
     𝑙₃ = 𝑙₄,
     𝑙₄ = (proc-val (procedure x 𝐸 [z = 𝑙₆])),
     𝑙₅ = 4,
     𝑙₆ = 5,
     𝑙₇ = 𝑙₈]

GC Example

ρ = [x = 𝑙₁, y = 𝑙₂]

σ = [𝑙₁ = 1, 
     𝑙₂ = (a-pair (𝑙₄ 𝑙₅)),
     𝑙₃ = 𝑙₄,
     𝑙₄ = (proc-val (procedure x 𝐸 [z = 𝑙₆])),
     𝑙₅ = 4,
     𝑙₆ = 5,
     𝑙₇ = 𝑙₈]

GC(ρ, σ) = [𝑙₁ = 1, 
            𝑙₂ = (a-pair (𝑙₄ 𝑙₅)),
            𝑙₄ = (proc-val (procedure x 𝐸 [z = 𝑙₆])),
            𝑙₅ = 4,
            𝑙₆ = 5]

GC Formalization

• : the set of locations in that are reachable from the variables in

GC Formalization

• : the smallest set of locations that satisfies the following rules:

-------------------- x ∈ dom(ρ)
 ρ(x) ∈ reach(ρ, σ)

GC Formalization

• : the smallest set of locations that satisfies the following rules:

                                      𝑙 ∈ reach(ρ, σ)   σ(𝑙) = 𝑙'
-------------------- x ∈ dom(ρ)     -----------------------------
 ρ(x) ∈ reach(ρ, σ)                       𝑙' ∈ reach(ρ, σ)

GC Formalization

• : the smallest set of locations that satisfies the following rules:

                                      𝑙 ∈ reach(ρ, σ)   σ(𝑙) = 𝑙'
-------------------- x ∈ dom(ρ)     -----------------------------
 ρ(x) ∈ reach(ρ, σ)                       𝑙' ∈ reach(ρ, σ)


   𝑙 ∈ reach(ρ, σ)     σ(𝑙) = (a-pair (𝑙₁, 𝑙₂))
----------------------------------------------
        {𝑙₁, 𝑙₂} ⊆ reach(ρ, σ)

GC Formalization

• : the smallest set of locations that satisfies the following rules:

                                      𝑙 ∈ reach(ρ, σ)   σ(𝑙) = 𝑙'
-------------------- x ∈ dom(ρ)     -----------------------------
 ρ(x) ∈ reach(ρ, σ)                       𝑙' ∈ reach(ρ, σ)


   𝑙 ∈ reach(ρ, σ)     σ(𝑙) = (a-pair (𝑙₁, 𝑙₂))
----------------------------------------------
        {𝑙₁, 𝑙₂} ⊆ reach(ρ, σ)


    𝑙 ∈ reach(ρ, σ)     σ(𝑙) = (proc-val (procedure x 𝐸 ρ'))
--------------------------------------------------------------
        reach(ρ', σ) ⊆ reach(ρ, σ)

Undecidability of GC

begin
𝐸₁;
𝐸₂
end

• Assume that GC is performed after evaluating 𝐸₁ and (ρ, σ₁) = σ₂
• Identifying garbage precisely is impossible. Given a location 𝑙, it is undecidable whether 𝑙 is garbage or not.

Undecidability of GC

begin
𝐸₁;
𝐸₂
end

• Assume that GC is performed after evaluating 𝐸₁ and (ρ, σ₁) = σ₂
• Identifying garbage precisely is impossible. Given a location 𝑙, it is undecidable whether 𝑙 is garbage or not.
  • Peforimg GC precisely is an undecidable problem.

Proving the Undecidability of GC

• Halting Problem: Given a program 𝑃, decides whether 𝑃 halts.

Proving the Undecidability of GC

• Suppose that we have an algorithm that performs garbage collection precisely.
• Then, we can construct an algorithm as follows:
  1. takes a program as input and executes the following program:

  let x = newRef(1) in P; deref(x)
  

  2. Invoke right before evaluating and obtain a set that contains all locations that will be used in the future.
  3. If contains the location of , then we know that terminates. Otherwise, does not terminate.