스마트 코드 생성을 위한 프로그램 분석 시스템 연구
The LET Project: program analysis for smalL/safE/smarT code


프로그램 분석 시스템 연구단
과학기술부 창의적 연구 진흥사업
서울대

[English]

연구책임자: 이 광근
(.ps, slides.ps)

문제제기

지구상의 모든 컴퓨터가 초고속 넷트웍으로 연결되면 지금까지와는 판이한 컴퓨팅 환경이 만들어진다. 지금까지 실험실에서 소규모로 구성된 분산 병렬 컴퓨터가, 지구위에서 거대한 스케일과 부정형적인 토폴로지로 조성되는 것이다. 이러한 컴퓨팅 환경에서는 프로그램 실행중에 필요한 코드부품이나 데이타들이 한 컴퓨터에 모여있지 않고 전 세계의 컴퓨터에 흩어져 있게 된다. 프로그램 부품들은 그 부품에 특화된 기술을 갖춘 팀에의해 최상의 품질로 넷트웍을 통해 지체없이 제공될 수 있기 때문이다. 모든 프로그램은 지구위를 광속으로 돌아다니면서 필요한 곳에서 필요한 자원(코드 부품, 데이타, CPU, 메모리등)을 적시에 동원하여 작업을 끝마치는 것이 일상적이 되는 것이다.

이러한 컴퓨팅 환경에 최적으로 적응하는 코드를 만들기 위해서는 지금까지 생각지 못한 많은 문제들이 해결되야한다. 물론, 현재의 컴퓨팅환경(desk-top computing) 에서도 실행코드의 부품과 데이타를 적시에 동원해서(디스크로부터 불러들여서) 프로그램을 실행하는 것은 가능해왔던 일이다. 그러나 미래의 전 지구적 컴퓨팅 환경에서 문제가 되는 것은, 그러한 일들이 전세계의 모든 컴퓨터를 묶은 초고속 넷트웍을 타고 엄청난 양과 빈도로 발생하게 된다는 것이다. 전세계 모든 코드가 광속으로 지구위를 움직이면서 사용자에게 최적의 성능을 제공하려고 경쟁하는 환경에서 그러한 일들이 일어나는 것이다. 이러한 환경에서 최적으로 수행되는 코드는 다음의 문제를 해결하고 있어야 한다.

본 연구의 차별성

우리는 프로그래밍 언어 이론에 기초한 엄밀한 프로그램 분석(static analysis) 이론을 이용해서 제안한 문제들의 해결책을 연구할 것이다. 물론, 지금까지의 연구들이 수학적으로 잘 정리된 이론에 기초하지 않고도 성공적인 연구결과를 가져올 수 있었고, 소프트웨어 이론들도 컴퓨팅 현실을 충분히 분석할 수 있는 모델을 제공해 주지 못한 면이 있다. 그러나 전 지구적 넷트웍 컴퓨팅 환경은 그 규모와 복잡성이 지금까지와는 비교될 수 없기 때문에 수학적으로 요약된 모델이 꼭 필요하고, 최근의 프로그래밍 언어 이론에 대한 연구성과들은 이러한 환경에서 실행되는 프로그램을 분석하는데 유용한 이론이 될 수 있을 만큼 비약적으로 성장하고 있다. 이러한 이론에 기초하지 않고서는 고안된 해결방안의 한계를 파악할 수 도 없고, 흔히 있을 수 있는 연구결과의 오류를 엄격히 검증할 수도 없다. 소홀한 기반위에서 고안된 연구결과는 어느순간 무너져 버리는 다리와 같이 위태로울 수 밖에 없고, 영향력있는 연구결과로 발전하기에는 역부족이 될 것이다.

전세계적으로, 프로그래밍 시스템을 연구하는 그룹은 대상으로 하는 프로그래밍 인구의 관성(programming sociology)을 따라가기 때문에(Java 주변의 경우와 같이) 프로그래밍 언어의 신 이론을 받아들이는 것이 느리고, 프로그래밍 언어 이론에 몰두하는 그룹은 프로그래밍 시스템 기술에의 응용에 무관심하다. 이 틈새를 본 연구가 공략할 것이다. 본인이 이 두 분야의 대표적인 연구그룹 (Center for Supercomputing Research and Development, University of Illinois at Urbana-ChampaignSoftware Principles Research Department, Bell Laboratories) 에서 연구한 잇점을 모두 동원할 것이며, 그 중심에는 본인이 지금까지 성공적으로 수행해온, 의미구조에 입각한 프로그램 분석 (semantics-based static analysis) 연구가 자리할 것이다.

더군다나, 지금까지의 글로벌 프로그래밍 시스템의 여러가지 문제를 해결하는 데에는 프로그램 분석 분야에서 연구된 많은 결과들이 매우 유용하게 사용될 수 있는 데도 불구하고 이 두 분야가 아직 활발히 소통하고 있지 못하다\cite{ToTh97}. 어쩌면, 글로벌 프로그래밍 시스템의 문제들이 어떤것이 있을지도 아직 정확하게 정의되지 않은 상태라서, 프로그램 분석이론이 어떻게 사용될 수 있을 지가 드러나지 않은 것일 수도 있다.

연구가설

본 과제에서 제안한 문제들의 해결에는, 프로그래밍 언어의 엄밀한 의미구조에 기초한 프로그램 분석(semantics-based static analysis) 기술이 핵심이 된다는 것이 우리의 입장이다. 프로그램 분석(static analysis)을 통해서 프로그램이 실행중에 가질 수 있는 성질을 미리 예측할 수 있는데, 이 예측을 통해서 가능하게 될 수 있기 때문이다. 본인은, 프로그래밍 언어의 정형적인 의미구조(mathematical semantics)로 부터 프로그램의 성질을 예측하는 연구를 수행에 왔는데, 이 연구 성과들을 계기로 해서 위의 세 가지 문제들이 해결될 수 있을 것으로 믿게 되었다:

연구내용및 추진체계

연구 추진은 두 가지 축으로 구성된다: 한 방향은 위의 세가지 연구 문제를 하나씩 해결해 가는 것이고, 다른 한 방향은 고안된 해결책들을 실제 프로그래밍 시스템을 구축하면서 실현해보는 것이다. 이때 구축하는 프로그래밍 시스템은 ML\cite{MTHM97}이라는 언어의 새로운 -- 위의 문제들에 대한 답을 갖춘 코드를 생성해내는 -- 컴파일러가 될 것이다. ML은 위에 제안한 문제들을 푸는데 필요한 언어 이론을 가장 충실히 갖춘 언어중의 하나이면서, 차세대 시스템 프로그래밍 언어로 부상하고 있기 때문이다. 본인은 지난 3년동안 ML의 엄밀한 의미구조에 기초해서 ML 프로그램의 안전성을 검증하는 기술(exception analysis)과 타입 유추 알고리즘에서 세계적으로 주목받는 연구성과를 이루어오고 있으며, 우리는 이 연장선상에서, 위에서 논의한 해결방안들을 ML의 컴파일러로 구현해서 그 실용성을 확인해 갈 것이다. 이렇게 해서 성공적으로 판별된 해결방안과, ML이 드러냈던 제한점들을 가지고 ML의 대안으로 글로벌 컴퓨팅 환경에 적합한 프로그래밍 언어 시스템을 구축하는 것도 가능할 것으로 예상된다. 이 단계까지 전세계 연구팀과의 교류:협력:경쟁의 비율이 4:3:3 정도가 될 것이다.

연구테마의 가치

세계적 연구동향

글로벌 프로그래밍 시스템에 대한 연구는 현재의 인터넷 프로그래밍 시스템에 대한 연구들\cite{DeFeWa96,Ro96}이나 차세대 넷트웍 아키텍춰\cite{TeWe96,SFGNFS96}에 대한 연구로 나누어질 수 있다. 인터넷 프로그래밍 환경연구는 Java를 중심으로 현재의 인터넷에서 효과적으로 사용될 소프트웨어 시스템에 관한 연구이고, 차세대 넷트웍 아키텍춰 연구는 현재의 인터넷의 한계를 넘어서서, 본 제안서에서 상정하는, 전 지구적 넷트웍 컴퓨팅 환경을 구축하고자 하는 방향의 연구이다.

대표적인 연구 그룹은 아래와 같다.

본 연구계획과 가장 가까운 연구를 진행하고 있고 있는 그룹은 CMU 그룹인데, 증명(theorem proving) 시스템과 타입 이론을 이용해서 코드의 안전성 검증 문제를 다루고 있다. 이 그룹은 아직 프로그램 분석(static analysis) 분야에서 축적한 이론들을 이용하고 있지 못하고 있다.

Java나 Agent관련 연구그룹들은 글로벌 컴퓨팅 모델의 엄밀한 분석에 기초하고 있지 않을 뿐더러, 미래의 넷트웍은 지금의 인터넷과는 많은 차이(각 스위칭 노드가 프로그램 가능한 일반 프로세서의 수준으로 향상되는 등)가 있을 것이기 때문에, 이러한 연구들이 차세대 넷트웍 프로그래밍 환경에 쉽게 적용되는 기반기술을 만들어 낼지는 의문이다.

국내의 프로그래밍 시스템 연구들은 Java 관련 연구들이 활발하게 진행되고 있는데, 이 연구들도 프로그래밍 언어 이론이나 엄밀한 컴퓨팅 모델에 기초하고 있지 않기 때문에, 미래의 효과적인 글로벌 컴퓨팅을 가능하게 하는 핵심 기반기술로 부각되기는 힘들것으로 보인다.

그리고, 본 연구가 진행중에 항상 그 발전과정을 염두에 두어야 하는 분야로, 프로그래밍 언어 모델에 대한 연구가 있다. 미래의 글로벌 컴퓨팅 환경의 계산 모델을 제안하고 그 모델에 기초한 다양한 프로그래밍 언어 모델들을 고안하는 연구로써, Milner의 Pi-calculus\cite{MiPaWa89a,MiPaWa89b}, Fournet의 Join-calculus\cite{FoGo96,FGLMR96,FLMR96}, Cardelli의 Ambient-calculus\cite{CaGo98}, Abadi의 Spi-calculus\cite{AbGo97,AbGo97b}등이 있다. 미래에는, 이러한 기초적인 모델들에 기반한 새로운 글로벌 프로그래밍 언어가 만들어지거나(Obliq\cite{Ca94,BrNa96}, PLAN\cite{HKMGN98} 등), 기존의 언어에 적절한 확장이\cite{Fac93} 이루어 질 것으로 예상된다. 우리는 이러한 글로벌 프로그래밍 모델의 핵심 구조들에 대한 이론 연구를 항상 고려하게 될 것이다. 첫째 이유는, 본 연구가 이러한 모델에 기초한 미래의 언어들의 컴파일러 시스템에 쉽게 적용되는 핵심기술을 만들어내야 하기 때문이고, 둘째 이유는, 그러한 엄밀한 모델에 기초한 연구는 우리가 대상으로 하는 프로그래밍 언어의 엄밀한 의미구조를 제공하는 기초가 되어 우리 연구를 엄격히 검증하고 그 한계를 규명하는 데에 필수이기 때문이다.