8. 레코드, 포인터, 메모리 관리(수동, 가비지컬렉션)

레코드

Records란 이름이 있는 메모리의 모음이다. 즉, C언어의 struct와 유사하다. 물론 배열 또한 메모리 위치들의 모음이지만 이 위치들의 이름은 자연수, index이다.

 

Syntax

E → ...

       | {}

       | { x:= E, y := E }

       | E.x

       | E.x := E

 

Values

Val = Z + Bool + {.} + Procedure + Record + Loc

 

Procedure = Var × E × Env

r ∈Record = Field → Loc

p ∈ Env = Var → Loc

σ ∈ Mem = Loc → Val

 

Semantics

빈 레코드의 결과는 . 이고, 메모리는 바뀌지 않는다.

 

x := E1, y := E2로 초기화 되는 레코드를 생성한다.

환경에는 {x ↦ l1, y ↦ l2} 가 추가되고, 메모리에는 l1 ↦ v1, l2 ↦ v2가 추가된다.

 

레코드에 있는 x는 메모리 l을 가진다.

메모리 σ에서 l이 가지는 값이 결과이다.

 

E1의 x에 E2를 대입한다.

결과는 E2의 결과인 v, 메모리에서 r(x)는 v를 가진다.

 

 

포인터

Syntax

E → ...

       | &x

       | &E.x

       | *E

       | *E := E

 

Semantics

주소값은 환경에서의 x의 값이다.

 

레코드에서의 주소값은 레코드에서의 x의 값이다.

 

여기서 E는 주소값, E의 결과가 l이라고 할 때 역참조한 값은 메모리에서의 l이 가진 값이다.

 

E1의 결과는 l, E2의 결과는 v라고 할 때

위 식의 결과는 v가 되고 메모리에서 l은 v를 가지게 된다.

 

 

Memory Management

현재 프로그램은 실행 중에 할당된 메모리가 해제되지 않아 결국 메모리 고갈로 이어진다. 하지만 미래에 사용될 메모리 위치를 정확히 식별하는 것은 불가능하다. 따라서 메모리 관리의 두 가지 접근 방법이 있다.

 

1. Manual memory manangement (수동 메모리 관리, C, C++ ...)

사용되지 않는 모든 메모리 위치를 수동으로 해제한다. 메모리 사용에 대한 세밀한 제어가 가능하나, 올바른 코드를 작성해야하는 부담이 있다.

 

2. Runtime garbage collection (런타임 가비지 컬렉션, Java, Ocaml...)

미래에 사용되지 않을 메모리 위치를 대략적으로 찾아서 재활용한다. 메모리 안정성이 있지만 세밀한 제어가 불가능하고 런타임 오버헤드가 발생한다.

 

Rust와 같은 최근 언어에서는 정적 타입 시스템을 사용해서 안전성과 제어를 모두 달성한다.

 

 

Manual Memory Management

Syntax

E → ...

      | free(E)

 

Semantics

E의 결과인 l을 해제한다.

반환은 없고, l을 제거한 새로운 메모리 상태를 얻는다. (Dom(σ)\{l)은 l이 없는 도메인 σ을 뜻한다)

 

 

다만 수동 메모리 관리의 경우 여러 오류를 가질 수 있다.

1. memory-leak: 메모리를 늦게 해제하는 경우, 시스템 자원이 낭비된다.

2. double-free: 같은 메모리를 두 번 해제하는 경우, 오류나 문제가 발생한다.

3. use-after-free: 메모리를 해제하고 사용하려고 하면 오류나 문제가 발생한다.

 

 

Garbage Collection

1. 프로그램 일시 중지

2. 현재 환경에서 도달 가능한 메모리 위치 수집

3. 도달할 수 없는 메모리 위치 재활용

 

가비지 컬렉션은 위 세 가지 단계로 이뤄진다.

 

아래에서, reach(p, σ)는 p의 엔트리들로부터 σ에서 도달 가능한 위치들의 집합이다.

p의 요소 x에 대하여, p(x)는 reach(p, σ)에 속한다.

 

reach(p, σ)에 속한 l이 있고, σ(l)이 l'일 때,

l'은 reach(p, σ)에 속한다.

 

reach(p, σ)에 속한 l이 있고, σ(l)이 Record일 때,

Record의 모든 변수가 가진 위치들은 reach(p, σ)에 포함된다.

 

reach(p, σ)에 속한 l이 있고, σ(l)이 (x, E, p') 즉 프로시저일 때,

프로시저가 생성될 때 도달 가능한 위치들 reach(p', σ)는 reach(p, σ)에 포함된다.

 

GC(p, σ)는 메모리에 현재 도달 가능한 위치만 남기고, 나머지는 해제한다.

 

표현식을 평가하기 전에 GC(p, σ)를 사용하여 메모리 상태를 정리한 후 평가를 수행한다.

 

 

가비지 컬렉션은 메모리 관리를 안전하게 수행하지만, 완전하지 않을 수 있다. 즉 모든 사용되지 않는 메모리 위치를 정확히 식별하고 해제하지 못할 수 있다. 어떤 메모리 위치가 프로그램 실행 중 도달 가능하지만 실제로 사용되지 않는 경우도 있고, 보수적으로 동작하여 사용될 가능성이 있는 모든 위치를 포함시키는 경우 일부 위치가 사용되지 않아도 해제되지 않는다.

 

GC가 안전하다는 것을 증명하기 위해 E에 대한 귀납법을 사용한다.

 

1. Base Case

⇒ E = x일 때, p(x)가 가리키는 메모리 위치는 reach(p, σ)에 포함된다.

 

2. Inductive Step

 

2-1. 연산

⇒ E = E1 + E2인 경우, E1과 E2를 각각 평가하여 그 결과를 더한다.

⇒ E1과 E2의 평가 과정에서 사용된 메모리 위치는 reach(p, σ)에 포함된다.

⇒ E1의 평가 과정에서 사용된 메모리 위치도 reach(p, σ)에 포함된다.

 

2-2. 함수 호출

⇒ E = f(E1)인 경우, E1을 평가하여 인자 값을 얻고, f를 호출한다.

⇒ 함수 f가 사용하는 메모리 위치는 함수 환경 p'에 의해 결정되며, 이는 reach(p', σ)에 포함된다.

⇒ E1의 평가 과정에서 사용된 메모리 위치도 reach(p, σ)에 포함된다.

⇒ 따라서 함수 호출 f(E1)의 평가 과정에서 사용된 모든 메모리 위치도 reach(p, σ)에 포함된다.