Abstract



Title  : 공리적 의미론의 소개: 다익스트라의 술어변환자를 중심으로
Author : 김 도형, 성신여대
Abstract :
 프로그래밍 언어의 설계, 프로그램 정확성의 정형적 검증이나 한 걸음 더 나아가 자동 프로그래밍 연구의 초석이 되는 정형적 의미론 중 공리적 의미론을 소개한다.
 특히 다익스트라가 제안한 술어변환자(predicate transformer)를 중심으로 설명한다. 기본적 원리를 소개하고 간단한 예제들을 통해 그 이해를 돕는다.

Title  : 교환기 소프트웨어 개발에서 프로그래밍 언어와 컴파일러 기술 요구
   (Needs of Programming Language and Compiler Technology in the Development of A Switching
   System Software)
Author : 권 경인, LG 정보통신 (LG Information & Communications, Ltd.)
Abstract :
 교환기 시스템은 통신망의 핵심 기능을 수행하는 시스템으로 일반적으로 고 신뢰성과 실시간 처리가 요구되며 매우 복잡하고 많은 기능을 수행한다. 이러한 교환기 소프트웨어의 효율적인 개발과 유지보수를 위해서는 다양한 도구의 활용이 필요하다. 이 논문에서는 대형 교환기 소프트웨어의 개발과 유지보수 등에 필요한 도구 가운데 프로그래밍 언어와 컴파일러 기술이 필요한 분야와 사례에 대해 LG정보통신의 교환기 개발을 중심으로 살펴본다.

Title  : 의미구조의 모듈화 향상을 위한 기법
Author : 도 경구, 한양대
Abstract :
 전통적인 표시적의미론(denotational semantics)과 동작적의미론 (operational semantics)의 기법으로 정의되는 의미구조는 실제로 정의된 부분을 수정 또는 확장할 때 많은 부분을 재구성해야 하는 약점이 있다. 최근 이 약점을 보완하기 위한 여러 가지 기법들이 제안되고 있다. 따라서 본 튜토리얼에서는 의미구조의 모듈화 향상을 위하여 최근 제안된 여러 가지 기법들을 정리하여 살펴보고, 그 장단점을 분석한다.

Title   : 값을 자르는 분석 (Static Value Slicing)
Author : 이 광근, KAIST 전산학과
Abstract :
 주어진 식 e가 최종적으로 집합 V에 속한 값을 계산해 내려면 그 내부식들의 값은 무엇이되어야 할까?
이러한 문제의 답을 구해주는 프로그램 분석기를 (static analysis를) 고안하는 것이 우리의 목표이다.
예를들어, 주어진 함수의 최종값의 범위가 주어지면 그 값들을 만들어 내는 인자값의 범위를 역추적하는 분석인 것이다.
 주어진 최종값의 범위에 있는 값들을 만들어 내는 내부 식들의 값들은 가능한 값중에서 불필요한 부위를 배재해가면서 구해진다.
이러한 분석은 기존의 기술이 (static backward slicing 이) 프로그램의 텍스트를 (syntactic objects, 예를들어, 프로그램의 식이나 문장등을) 잘라나가는 반면에, 프로그램 \bf 들을 도려내가는 방식이된다.
 이 분석기가 표현하는 값들의 집합은 \em 정규 문법식을 (regularterm grammar를) 이용한다. 사용자는 주어진 식의 값의 범위를 정규문법식으로 표현하며, 분석결과로서 내부 식들이 가져야 하는 값들의 범위도 정규 문법식으로 표현한다.

Title   : 프로그래밍 언어 학습을 위한 가상 실습 환경
Author : 이 수현, 창원대학교 컴퓨터공학과
Abstract :
 현재 다양한 패러다임의 수 많은 프로그래밍 언어가 존재하고 있으며, 각각의 프로그래밍 언어를 연습하려면 해석기(interpreter)나 컴파일러 같은 언어처리기를 갖추는 것이 필요하다. 언어처리기를 개별적으로 갖추는 것은 설치에 대한 부담, 설치에 의한 자원 낭비, 업그레이드의 필요성 등으로 인해서 언어 학습과 직접적인 관련이 없는 부분에 대한 부담이 커진다.
 본 논문에서는 WWW 환경에서 프로그래밍 언어를 실습할 수 있는 환경을 구축하였다. 구축된 환경하에서 실습자는 웹 브라우저를 실행함으로서 실습에 대한 준비가 끝나며, 프로그램의 해석이나 컴파일 등 언어처리기의 실행과 컴파일된 프로그램의 실행은 서버에서 모두 이루어진다.
 또한 각 프로그래밍 언어에 대한 정보, 예제 프로그램 등을 하이퍼링크로 연결하여 프로그래밍 언어의 학습을 위한 통합된 환경을 제공한다.

Title   : Ada Real-time State Machine
Author : 이 문근, 정 명선, 전북대학교, 컴퓨터과학과
Abstract :
 This paper reports Ada Real-time State Machine (ARSM) to represent the dynamic behavior of very large and extremely complex Ada real-time software for understanding. Generally the software consists of millions lines of codes with a large number of processes interacting heavily with each other. Due to size and complexity, it is commonly very difficult to understand the dynamic behavior of the software. ARSM is a new notion of state machine to describe the software by reverse specification for this purpose. Here reverse specification implies a reverse engineering activity to transform the software in source code level to a formal method in specification level. ARSM has real-time and non-real-time features similar to Communicating Real-time State Machine (CRSM).
The new features of ARSM are the capabilities of representing the execution behavior of the software in a physical environment with the formal method. The capabilities include changing execution control among related machines, handling duplicated images of an ARSM to represent multiple calls to a procedure or function, handling types of events, such as task activation/termination, procedure or function substitution, communication, IO with an external environment, processing a/synchronous events with non-instantaneous execution time, etc. A noticeable feature in representing the software is the way of representing the execution behavior of the software in hierarchical order with abstraction.
This is accomplished by an architecture of the software and ARSM tree. The architecture is the skeleton of the software, where the modules and software units are organized hierarchically by abstraction, and the tree is the representation of ARSMs with these abstraction relations among them. The abstraction means the representation of 1) static structure of sub-modules or sub-program-units with a single entity and 2) dynamic behavior of sub-ARSM with a single execution event. These provide an background for understanding of dynamic behavior of the software in scalably understandable level and size, and the understanding is guided by navigating them with abstraction and explosion on the architecture and the tree. The paper describes the definition of ARSM, a Producer-Buffer-Consumer example with Ada code, simulation, output, analysis, and discussion for problems and future researches.

Title   : Persistent Java에서의 동시성 제어
Author : 이 정태, 류 기열, 백 경원, 아주대학교 정보통신 대학
Abstract :
 본 논문에서는 Java에 Persistent 프로그래밍 언어로서의 기능을 추가한 Orthogonally Persistent Java(PJama)의 동시성 제어 문제를 다룬다. Orthogonally Persistent Java를 비롯한 Persistent 프로그래밍 언어에서는 프로그래밍 언어와 데이터베이스 각각의 영역에서 다르게 정의된 동시성 제어에 대한 통합된 개념과 메커니즘을 필요로 한다.
 PJama에서는 지속성 자료에 대한 동시성 제어를 위하여 트랜잭션 모형을 제공하고 있지만 현재까지 제공되는 트랜잭션 모형을 적용하는 경우 Orthogonally Persistent Principle 중, 자료의 지속성 유무에 관계없이 프로그램의 형태는 같아야 한다는 Persistent Independence Principle을 유지할 수 없다.
 본 논문에서는 PJama의 프로그램 소스 코드에 대한 제어 흐름과 자료 흐름을 분석하여 트랜잭션으로 처리되어야 될 부분을 감지하고, 컴파일러가 자동으로 트랜잭션을 설정하게 함으로써 Persistent Independence Principle이 유지 될 수 있는 방안을 제안하고자 한다.

Title   : Preparing s Static Analysis for Run-time Specialization
Author : 어 현준, 이 광근
Abstract :
 프로그램의 실행 도중 사용자의 입력 패턴에 따라 프로그램의 분석을 전문화(specialize) 시킬 수 있다. 기존의 정적 분석 방법으로부터 실행시간 입력에 따라 분석을 전문화 시킬수 있는 방법을 고안하는 것이 이 연구의 목표이다.

 정적 분석에서 우리는 실행시간 입력에 대해서는 모든 값을 가질 수 있다고 전제하고 분석을 시작한다. 따라서, 입력에 의존하는 모든 식들은 그 결과가 헐렁하게 나올 수 밖에 없다. 만약, 입력에 의존하는 식들에 대해서는 분석을 진행하지 않고, 입력과 상관없이 컴파일 시간에 가능한 분석들을 모두 진행한 후, 입력을 보고 나머지 분석을 진행한다면 정적 분석보다 더 정확한 결과를 얻을 수 있을 것이다. 그러나, 이 방법은 실행시간 부담이 큰 단점이 있다.

 본 연구에서는 값을 자르는 분석(Static Value Slicing)을 이용해 실행시간 부담을 줄이면서 입력에 따른 전문화가 가능하도록 하는 분석 방법을 제안한다. 값을 자르는 분석은 주어진 식 e가 최종적으로 집합 V에 속한 값을 내려면 그 내부식들의 값은 무엇이 되어야 하는 지를 찾아내는 방법이다. 값을 자르는 분석을 이용하여 주어진 식 e가 어떤 집합 V에 속한 값을 내려면 프로그램의 입력 w가 어떤 값에 속해야 하는 지를 찾아낼 수 있고, 이를 이용하여 우리는 입력 w가 주어지자마자 프로그램의 정확한 (정적 분석에 비해) 분석 결과를 얻을 수 있다.

Title   : 정리증명에서 순환함수 사용 (Using Recursive Functions in Theorem Proving)
Author : 배 민오
Abstract :
 논리프로그래밍과 같이 순수 논리만 이용한 정리 증명기에서 원자식까지는 삭제 규칙(Elimination Rule)에 의해 분해하여 추론하는 것이 가능하지만 원자식부터는 더 분석하여 추론하는 것이 불가능하다. 즉 원자식의 진리를 판단하기 위해서는 이 원자식이 주어진 도메인 상에서 참인지 거짓인지를 계산을 하여야 한다. 본 연구에서는 위와 같은 순수 논리 시스템을 보완하기 위해 Luo의 CC의 수축 이론적 의미론(Reductional Semantics)을 이용하여 정리증명을 하므로서 정리 증명과 계산이 자연스럽게 융화될 수 있다는 것을 보였다.

Title   : CC-NUMA구조를 위한 자동 쓰레드 생성 컴파일러에 관한 연구
Author : 김 홍숙, 나 상옥, 한 동수, 지 동해*
   한국정보통신대학원대학교 시스템 소프트웨어연구실
   한국전자통신연구원 컴퓨터·소프트웨어기술 연구소*
Abstract :
 본 논문은 입력으로 주어진 순차적 포트란 77 프로그램 코드로부터 CC-NUMA구조에서의 실행을 위하여 쓰레드 관련 코드가 삽입된 병렬 코드를 자동으로 생성하는 컴파일러의 설계 및 구현에 관한 연구이다. 쓰레드 코드 생성을 위하여 데이터 종속성 분석 등의 해석 기법을 사용하여 병렬화 가능 루프를 구분하였다. 병렬화 가능 루프에 대해서는 CC-NUMA구조의 중요한 성능 향상 요소인 캐쉬의 지역성 향상을 위하여 루프 교환 등의 프로그램 변형 기법을 사용하였으며, 병렬 수행을 위하여 삽입되는 쓰레드 관련 코드는 SPMD방식에 근거하여 생성하였다. 또한 성능에 영향을 줄 것으로 예상되는 요인들을 변화시키면서 컴파일러가 생성한 코드의 수행시간을 측정하고 코드 변환 시에 사용한 루프 교환 기법이 코드의 수행시간에 미치는 영향을 분석하였다.

Title   : An Uncaught Exception Analysis of Java
Author : Byeong-Mo Chang and Kwangkeun Yi, Sookmyung Women's University, KAIST
Abstract :
 In Java, uncaught exceptions of a method must be speci ed, and the current implementation of Java compiler analyzes uncaught exceptions based on types and user speci cations. However, speci cations may be missing or too broad like just specifying as Exception. Therefore, we need more elaborate uncaught exception analysis not depending on user speci cations.
In Java, variables declared to be a class may also refer to objects of its subclasses, and method calls are bound dynamically. So the rst 246 543 261 555 problem is an interprocedural class analysis to approximates at each method invocation point the set of classes, to which the objects of variables or expressions may belong. Then, for every method, uncaught exception analaysis approximates all the uncaught exceptions generated in the method, using the class analysis information. We present the analyses using set constraints.

Title   : LaTTe: a Java VM Just-in-Time Compiler
Author : 이 승일, 이 준표, 문 수묵, 서울대학교 전기공학부
Abstract :
 자바 언어는 네트웍 환경을 위한 언어로 개발되어 embedded system에서 뿐만 아니라 enterprise 서버에 이르기까지 점차 그 영역을 확대하고 있다. 이렇듯 자바 언어의 쓰임이 확대됨에 따라 자바로 만들어진 프로그램을 빠르게 수행시킬 수 있는 자바 가상머신의 필요성이 증대되고 있다.
 본 논문에서는 JIT 컴파일러 방식에 기반한 LaTTe 자바 가상머신을 소개한다. LaTTe에 탑재된 JIT 컴파일러는 효율적으로 복사 명령을 제거할 수 있는 빠른 레지스터 할당기와 중복 연산 제거, 죽은 코드 제거, 메소드 인라이닝과 같은 최적화 기법을 포함하고 있다. LaTTe 자바 가상 머신은 그밖에 효율적인 쓰레기 처리, 빠른 모니터 락 처리, 그리고 필요 에 따른 예외 처리를 수행한다. 이와 같이 구성되어 있는 LaTTe 자바 가상 머신은 자바 프로그램을 매우 빠르게 수행할 수 있다.
 SPEC jvm98에 대하여 실험한 결과에 따르면, LaTTe는 실행 시간에 있어서 SUN에서 제공하는 JDK1.1.6과 비교하여 평균 2.3배 정도 향상된 결과를 얻을 수 있었다.

Title   : 유연한 컴포넌트 결합을 지원하는 컴포넌트 모델
Author : 류 기열, 이 정태, 김 윤명 (아주대)
Abstract :
 최근 들어, 소프트웨어의 재사용을 통한 효과적인 소프트웨어의 개발을 위한 컴포넌트 개념에 대한 연구가 활발하게 진행되고 있으며 상용 시스템에서까지 이러한 개념을 부분적으로 구현하고 있으나, 아직 컴포넌트 모델에 대한 개념이 이론적으로 명확하게 정립되지 않은 실정이다.
 본 논문에서는 기존의 여러 연구에서 정의되고 있는 컴포넌트 개념을 분석하고 컴포넌트 모델이 갖추어야 할 요구조건에 따라 하나의 새로운 컴포넌트 모델을 정의한다. 제안된 모델에서는 컴포넌트들이 부합성의 규칙에 따라 유연하게 결합될 수 있다. 본 논문에서는 컴포넌트의 기본 요소, 컴포넌트들간의 결합에 관한 규칙, 그리고 이미 조립된 복합 컴포넌트의 부품 컴포넌트의 교체 규칙 등 컴포넌트 모델에 대한 몇 가지 성질들을 정의한다.

Title   : ML 프로그램에서 예외상황을 발생시키는 테스트, 데이터 생성 방법
Author : 류 석영, 이 광근, KAIST 전산학과
Abstract :
 주어진 ML 프로그램에서 예외 상황을 발생시키는 테스트 데이터를 자동으로 생성해주는 분석기를 제안한다. 타입 검사를 거친 ML 프로그램이 비정상적으로 멈추는 경우는, 프로그램이 예외상황을 발생시킬 때 그 예외상황을 적절하게 처리해주지 못한 경우 밖에 없다. 따라서 프로그램 내의 모든 예외상황을 발생시키는 테스트 데이터를 만들어서, 각각의 경우에 프로그램이 제대로 처리해주도록 보완하면 안정성(safety)이 보장되는 프로그램을 개발할 수 있게 된다.
 주어진 프로그램에서 각각의 예외상황 Ei가 발생한다는 조건을 가지고, 프로그램의 입력 값인 테스트 데이터 집합 Di를 구한다. 전체 프로그램의 값인 예외상황 Ei를 시작점으로 하여 프로그램 내의 각 내부 식들이 가져야하는 값들을 "강요"해가면서, 그 과정 중에 테스트 데이터의 값을 구하게 된다. 분석결과로 얻게 되는 테스트 데이터들(Di)은, 그 중에 어느 값을 입력으로 사용하여 프로그램을 수행시켜도 예외상황 Ei가 발생한다는 것을 보장해야 한다. 이렇게 구한 테스트 데이터 집합 Di에서 각각 하나씩의 데이터를 선택하면, 프로그램 내의 모든 예외상황을 발생시키는 테스트 데이터 집합을 구하게 된다.
 테스트 데이터를 생성하는 분석 방법을 제안하고, 몇 가지 예를 통하여 이 분석 방법이 만족해야할 성질에 대해서 논의한다.

Title   : UltraSPARC을 위한 명령어 스케쥴링
Author : 윤 한샘, 문 수묵, 서울대학교 전기공학부
Abstract :
 근래에 개발된 마이크로프로세서는 대부분 여러 개의 명령어들을 동시에 수행시킬 수 있는 슈퍼스칼라 구조를 채택하고 있는데 Sun의 UltraSPARC, Intel의 Pentium-Pro/P6, IBM의 PowerPC 계열 등이 그 예이다. UltraSPARC와 같이 하드웨어가 명령어 스케쥴링을 하지 않는 경우 프로세서의 자원을 최대한으로 활용하기 위해서는 컴파일러에 의한 명령어 스케줄링이 필요한 것으로 알려져 있다. 소프트웨어 파이프라이닝(software pipelining)은 여러 iteration의 명령어들 사이에 존재하는 명령어 수준 병렬성(instruction-level parallelism)을 이용하는 루프 스케쥴링 기법이다. EPS(Enhanced Pipeline Scheduling)은 소프트웨어 파이프라이팅 기법의 하나로 정수 프로그램(integer program)에서 흔히 볼 수 있는 불규칙적인 루프(irregular loop)에 특히 적합한 것으로 알려져 있다. 이 논문에서는 EPS를 이용한 UltraSPARC 명령어 스케쥴링 기법을 소개하고 SPECint95 벤치마크를 대상으로 한 실험결과를 보여준다.