메모리 타입 분석을 통한 안전하고 효율적인 메모리 재사용 메모리 타입 분석을 통한 안전하고 효율적인 메모리 재사용 이욱세 이광근 전자전산학과 / 프로그램 분석 시스템 연구단 한국과학기술원 2002년 4월 27일
동기 자동 메모리 관리가 항상 좋은가? 안전하게 제거(deallocation)할 수 있는가? fun append x y = case x of [] => y | h::t => h :: append x t 안전하게 제거(deallocation)할 수 있는가? 재귀적인 데이터 구조에 대해 적절한 방법론이 없다
목적 재귀적 데이터 구조와 제거 명령어가 있는 언어의 안전성 검증
메모리 분석 각 변수에서 볼 수 있는 메모리의 모양새를 분석 각 칸(heap cell)은 이름 붙여 구별 x y x y a b ::(1, ) ::(2, ) ::(3, ) [] x y a b c d ::(;, ) [] x y a b c d
무너뜨린 타입 메모리의 모양새가 일정치 않을 수 있음 무너뜨려 분석 x y xory a b c d c d ::(;, ) ::(;, ) ::(;, ) [] c d y ::(;, ) [] xory = if … then x else y a,c ::! {b,c} []! {d} xory ::(;, )
재건축 무너뜨린 것은 재건축 가능 xory xory a,c ::! {b,c} []! {d} case (tl xory) of … ::(;, ) case (tl xory) of … a,c b,c ::! {b,c} []! {d} xory ::(;, ) ::(;, )
e1에서 제거한 것 Å e2 에서 사용/제거한 것 = ; 사용/제거의 안전성 검증 메모리 분석을 통해 각 프로그램 부분에서 사용/제거한 것을 모음 제거한 것을 이후에 사용/제거 불가 let x = e1 in e2 e1에서 제거한 것 Å e2 에서 사용/제거한 것 = ;
함수 분석과 이름 혼동 (aliases) 인자에 대해 가정하고 함수 코드를 분석한 것을 결과로 함 ! (, U, R) 함수 호출시 가정에 맞추어 얻어진 결과를 사용 이름이 혼동되는 경우 한 쪽이 함수 코드에서 제거되었으면 다른 쪽은 사용/제거 금지
분석 정확도 높이기 정교한 재건축 실행 시간 제거 여부 전달과 선택적 제거 경로별 분석
정교한 재건축 경우에 따라 정교한 재건축 가능 xory xory e + f = { b, c } a,c ::! {b,c} []! {d} xory ::(;, ) case (tl xory) of … a,c e ::! { f } []! {d } xory ::(;, ) ::(;, ) e + f = { b, c }
선택적 제거 함수 호출의 상황에 따라 제거 여부가 결정 실행 시간에 제거 여부를 전달받아 선택적 제거 fun append x y = … free x … append l1 l2 실행 시간에 제거 여부를 전달받아 선택적 제거 fun append x y = … free x when … append false l1 l2 append true l1 l2 제거한 것에 제거 조건을 붙여 모음으로써 해결
경로별 분석 경로별로 분석하지 않아 제거 못하는 경우 경로별로 분석 가능 let fun incr x = case x of [] => [] | h::t => h+1 :: incr t val z = if … then l else incr l in print_list z end 경로별로 분석 가능
메모리 재사용에 응용한 실험 결과 제거 + 할당 = 재사용 리스트 기반 작은 프로그램 실험 플랫폼: 수정된 Objective Caml
결론 재귀적 데이터 구조의 제거의 안전함을 보장하는 타입 시스템 제시 2.8-99% 메모리 재사용 DAG 형태 데이터 구조에 취약 예상