초록 ▼

병렬 프로그래밍 언어는 주어진 문제의 병렬성을 직접 알고리즘이나 프로그램으로 표현할 수 있게 함으로써 문제 중심의 해결방법을 가능하게 할 것으로 기대되나 기존의 병렬 언어들은 순차 언어에 병렬 구문을 첨가하는 방식으로 구성되므로 프로그램의 시멘틱스를 정형적으로 표현하거나 자동 검증을 필요로 할 때 복잡하고 임기응변적인 기법을 사용할 수밖에 없다. 순차 언어의 간단하고 명확한 시멘틱스 표현에 λ-calculus가 사용되듯이 병렬 언어에서도 π-calculus가 사용되어 프로세스간의 통신과 동기 문제를 정형화할 수 있을 뿐 아니라 기존

병렬 프로그래밍 언어는 주어진 문제의 병렬성을 직접 알고리즘이나 프로그램으로 표현할 수 있게 함으로써 문제 중심의 해결방법을 가능하게 할 것으로 기대되나 기존의 병렬 언어들은 순차 언어에 병렬 구문을 첨가하는 방식으로 구성되므로 프로그램의 시멘틱스를 정형적으로 표현하거나 자동 검증을 필요로 할 때 복잡하고 임기응변적인 기법을 사용할 수밖에 없다. 순차 언어의 간단하고 명확한 시멘틱스 표현에 λ-calculus가 사용되듯이 병렬 언어에서도 π-calculus가 사용되어 프로세스간의 통신과 동기 문제를 정형화할 수 있을 뿐 아니라 기존의 계산 모델도 시뮬레이션할 수 있다. 본 연구의 최종 목표는 병렬 프로그래밍 언어의 기반이 될 π-calculus의 변형을 연구하고 순전히 π-calculus의 구문만을 기반으로 하는 병렬 언어의 추상 기계를 정의함으로써 병렬 언어의 핵심 주제로 자리잡은 π-calculus에 대한 기초 기술과 병렬 언어의 설계 기술을 추적함에 있다. 이를 위하여 본 연구는 크게 두 가지 단계로 구성된다. 1차년 도에는 다양한 프로세스 계산의 표현력에 대한 고찰로서 본 연구의 핵심 언어가 될 π-calculus를 비롯한 프로세스 계산의 기본 개념을 연구하고 이들의 동작 원리와 시멘틱스를 규명한 후에 필요한 변형을 결정하여 이를 위한 타임 시스템을 정의하고 리덕션 시멘틱스를 이용하는 추상 기계를 정의한다. 또한 정의된 추상기계의 동작이 π-calculus의 리덕션과 일치함을 증명한다. 2차년에는 π-calculus의 기본 변형에 분산 처리에 필요한 개념인 location과 failure를 부가한 π-calculus의 분산 변형으로부터 분산 π-calculus의 합동성, 리덕션 규칙, 동적 타이핑 등을 연구하며, 분산 구현을 위한 추상기계와 모델을 정의하고 이에 대한 전당 성을 증명한 다. ,