탐색시간의 개선을 위한 함수형 배열의 설계 및 구현

유원희(Yoo Weon Hee),주형석(Joo Hyung Seok) 한국정보처리학회 1996 정보처리학회논문지 Vol.3 No.5

Pure functional languages have the referential transparency feature so that all objects cannot be updated destructively. Once an aggregated data structure such as array is updated, both the original and newly updated array must be preserved to maintain referential transparency. Thus, it is required to develop an efficient mechanism with which can reduce the maintenance cost while maintaining referential transparency for whole data.This study is to suggest a functional array to solve the problem, and then test it. For that, the proposed mechanism was implemented on a combinator graph reduction machine. The result shows that proposed mechanism reduces traversal time for array operations. Also, updating all versions and accessing the recent version are achieved in constant time without reconstruction of updated data in execution time.

GML파일을 이용한 검증조건의 시각화

유원희(Weon-Hee Yoo),박준석(Joon-Seok Park),김제민(Je-Min Kim),허혜림(Hye-Lim Hu) 한국컴퓨터정보학회 2012 韓國컴퓨터情報學會論文誌 Vol.17 No.7

프로그램 검증을위해 사용되는방법으로 프로그램을 검증조건으로 변환하여정리증명기를 통해 프로그램의유효성을 확인하는 방법이 있다. 검증조건 생성을 통한 프로그램의 검증의 경우 검증조건은 프로그램을 검증하기 위한 충분하고 정확한 정보를 가지고 있어야한다. 하지만 프로그램의 변환을 통해 생성된 검증조건의 경우 논리식만으로 구성되어 있어 사용자가 쉽게 그 내용을파악할 수 없다. 본 논문에서는 가독성이 떨어지는 검증조건을 시각화하는 프로그램을 구현하였다. 프로그램을 통해 검증조건을 구성하고 있는 논리식간의 관계 등을 비롯한 정보를 보다 쉽게 확인할 수 있다. There is a method which identifies validity of program by transforming program to verification condition to verify program. If program is verified by generating verification condition, verification condition must have enough and accurate information for verifying program. However, verification condition is consisting of logical formulas, so the user cannot easily identify the verification condition. In this paper, we implemented program that visualize the poorly readable verification conditions. By the program, the users can easily identify information, such as the relationship between logical formulas that represent verification condition.

바이트코드를 위한 정적 단일 배정문 기반의 정적 타입 추론

유원희(Yoo Weon Hee),김제민(Kim Je Min),김기태(Kim Ki Tea),김지민(Kim Ji Min) 한국컴퓨터정보학회 2006 韓國컴퓨터情報學會論文誌 Vol.11 No.4

바이트코드는 많은 장점을 가지고 있으나 수행 속도가 느리고 프로그램의 분석과 최적화에 알맞은 표현은 아니다. 분석과 최적화를 위하여 바이트코드를 정적 단일 배정문(SSA Form)으로 변환이 수행되어야 한다. 그러나 바이트코드에서 SSA Form으로 변환 시 어떤 변수는 타입 정보를 상실한다. 이를 해결하기 위하여 본 논문에서는 바이트코드에 대한 확장된 제어 흐름 그래프를 생성한다. 또한 정적으로 분석하기 위해 제어 흐름 그래프를 SSA Form으로 변환한다. SSA Form으로 변환을 위하여 지배자, 직접 지배자, 지배자 경계, ?-함수, 재명명 등 많은 정보에 대한 계산을 수행한다. 생성된 SSA Form에 알맞은 타입을 선언하기 위해서 다음과 같은 동작들을 수행한다. 먼저 클래스의 호출그래프와 상속 그래프를 생성한다. 그리고 각 노드에 대한 정보를 수집한다. 수집된 정보를 기반으로 동등한 타입의 노드를 찾고 강 결합 요소로 설정한 후 각 노드에 타입을 효율적으로 설정하는 방법을 제안하였다. Although bytecode has many good features, it has slow execution speed and it is not an ideal representation for program analysis or optimization. For analysises and optimizations, bytecode must be translated to a Static Single Assignment Form(SSA Form). But when bytecode is translated a SSA Form it has lost type informations of some variables. For resolving these problemㄴ in this paper, we create extended control flow graph on bytecode. Also we convert the control flow graph to SSA Form for static analysis. Calculation about many informations such as dominator, immediate dominator, dominance frontier, ?-Function, renaming are required to convert to SSA Form. To obtain appropriate type for generated SSA Form, we proceed the followings. First, we construct call graph and derivation graph of classes. And the we collect informationㄴ associated with each node. After finding equivalence nodes and constructing Strongly Connected Component based on the collected informations, we assign type to each node.

SSA Form에서 부분 중복 제거를 이용한 최적화

김기태,유원희,Kim, Ki-Tae,Yoo, Weon-Hee 한국정보처리학회 2007 정보처리학회논문지D Vol.14 No.2

CTOC에서는 정적으로 값과 타입을 결정하기 위해 변수를 배정에 따라 분리하는 SSA Form을 사용한다. SSA Form은 최근 데이터 흐름분석과 코드 최적화를 위해 컴파일러의 중간 표현으로 많이 사용되고 있다. 하지만 기존의 SSA Form은 표현적보다는 주로 변수에 관련된 것이다. 따라서 SSA Form 형태의 표현식에 대해 최적화를 적용하기 위해 중복된 표현식을 제거한다. 본 논문에서는 좀더 최적화된 코드를 얻기 위해 부분 중복 표현식을 정의하고, 부분 중복 표현식을 제거하는 방법을 구현한다. In order to determine the value and type statically. CTOC uses the SSA Form which separates the variable according to assignment. The SSA Form is widely being used as the intermediate expression of the compiler for data flow analysis as well as code optimization. However, the conventional SSA Form is more associated with variables rather than expressions. Accordingly, the redundant expressions are eliminated to optimize expressions of the SSA From. This paper defines the partial redundant expression to obtain a more optimized code and also implements the technique for eliminating such expressions.

자바 언어를 위한 알고리즈믹 디버깅 기술의 설계

고훈준,유원희,Kouh, Hoon-Joon,Yoo, Weon-Hee 한국정보처리학회 2004 정보처리학회논문지 A Vol.11 No.1

This paper proposes to use an algorithmic debugging technique for locating logical errors in Java programs. The algorithmic debugging is a semi-automated debugging technique that builds an execution tree from a source program and locates logical errors, if any, included in the program from the execution tree with top-down method. So, it is very important to build a suitable execution tree from the various programming languages. In this paper we propose the method for building an execution tree iron Java programs and walk through an example. This approach could reduce the number of interactions between a user and a debugging system than the traditional step-wise debugging technique. 본 논문은 자바 프로그램에서 논리적인 오류를 발견하기 위해 알고리즈믹 디버깅 기술의 이용을 제안한다. 알고리즈믹 디버깅 기술은 원시프로그램으로부터 실행 트리를 생성하고, 실행 트리로부터 프로그램 내에 포함된 논리적인 오류를 하향식 방법으로 발견하는 반자동화 디버깅기술이다. 따라서 알고리즈믹 디버깅 기술은 다양한 프로그래밍 언어에 알맞은 실행 트리를 생성하는 것이 중요하다. 주 논문에서는 자바 프로그램으로부터 실행 트리를 생성하는 방법을 제안하고 예제론 통해서 자바 프로그램을 위한 알고리즈믹 디버깅 기술을 확인한다. 이 접근은 전통적인 순차적 디버깅 기술보다 사용자와 디버깅 시스템 사이에서 상호작용의 수를 줄일 수 있다.

CTOC에서 자바 바이트코드를 위한 정적 단일 배정 형태

김기태,유원희,Kim, Ki-Tae,Yoo, Weon-Hee 한국정보처리학회 2006 정보처리학회논문지D Vol.13 No.7

자바 바이트코드는 많은 장점을 갖지만 수행 속도가 느리고 분석이 어렵다는 단점을 갖는다. 이를 극복하기 위해 바이트코드에 대한 분석과 최적화가 수행되어야 한다. 최적화된 코드를 위해 CTOC를 구현하였다. 바이트코드에 대해 분석과 최적화를 수행하기 위해서는 우선 CFG를 생성해야 한다. 바이트코드의 특성 때문에 기존의 제어 흐름 분석 기술을 바이트코드에 적합하게 확장해야 한다. 또한 정적으로 분석하기 위해 CFG를 SSA Form으로 변환한다. SSA Form으로 변환하기 위해서는 지배 관계, 지배자 트리, 직접 지배자, $\phi$-함수, 재명명, 지배자 경계 등 많은 정보에 대한 계산을 수행한다. 본 논문은 기존의 CFG로부터 SSA Form으로 변환을 위해 알고리즘과 변환 과정을 기술한다. SSA Form이 적용된 그래프는 추후에 타입 추론과 최적화를 위해 사용된다. Although the Java bytecode has numerous advantages, there are also shortcomings such as slow execution speed and difficulty in analysis. In order to overcome such disadvantages, bytecode analysis and optimization must be performed. We implements CTOC for optimized codes. An extended CFG must be first created in order to analyze and optimize a bytecode. Due to unique bytecode properties, the existing CFG must be expanded according to the bytecode. Furthermore, the CFG must be converted into SSA Form for a static analysis, for which calculation is required for various information such as the dominate relation, dominator tree, immediate dominator, $\phi$-function, rename, and dominance frontier. This paper describes the algorithm and the process for converting the existing CFG into the SSA From. The graph that incorporates the SSA Form is later used for type inference and optimization.

동기화 동작을 포함하는 분산 실시간 프로그램의 스케줄가능성 분석

박흥복(Hung Bog Park),유원희(Weon Hee Yoo) 한국정보과학회 1995 정보과학회논문지 Vol.22 No.3

본 논문에서는 분산 실시간 프로그램의 스케줄가능성 분석을 제안한다. 스케줄가능성 분석을 위한 여러가지 방법이 개발되었지만, 이 방법들은 가능한 고정 우선순위 스케줄링 방법을 사용하거나 생성되는 모든 상태공간을 탐색한다. 이러한 방법들은 지수승의 시간과 공간적 복잡성때문에 상태공간을 줄여서 더 이른 시간단위에서 스케줄가능성을 조사하는 방법이 필요하다. 본 논문에서 제시한 스케줄가능성 분석은 동기화 동작을 종료하는데 걸리는 최소단위시간, 동기화 후에 동작을 종료하는데 걸리는 최소단위시간, 마감시간을 사용하여 더 이른 시간단위에서 스케줄가능성 분석을 조사하고, 탐색할 상태공간을 줄이기 위한 동적 스케줄링 방법을 이용한다. 만약 처리기가 프로세스를 수행할 수 있고 프로세스가 스케줄가능하다면 프로세스는 단일 처리기에 할당된다. 또한 계산과 동기화 동작의 수행시간이 처리기의 능력을 초과하고 프로세스가 스케줄가능하다면 하나 이상의 처리기에 프로세스들을 할당하여 스케줄이 가능하도록 한다. 프로세스들의 스케줄가능성 분석을 하는 동안 결정된 스케줄이 가능한 프로세스의 수행순서를 스케줄링에 이용하는 정적 스케줄링 정책을 주기 프로세스의 스케줄링에 사용하고, sporadic 프로세스에 대해서는 sporadic 프로세스가 도착할 때 그 프로세스를 마감시간내에 처리할 수 있는 처리기를 찾아 스케줄링하는 동적 스케줄링 정책을 사용한다. In this paper, we propose a schedulability analysis for distributed real-time programs. Several approaches to anlayzing schedulability have been developed, but these approaches used a fixed priority scheduling scheme and/or traverse all possible state spaces. Because of exponential time and space complexity of these methods, it is necessary to reduce a state space and detect schedulability at earlier time unit. Our schedulability analysis scheme uses a minimum unit time taken to terminate synchronization action, a minimum unit time taken to terminate actions after synchronization, and a deadline of processes to detect unschedulability at earlier time unit and dynamic scheduling scheme to reduce state space. If a processor is capable of executing processes and processes are schedulable, processes are assigned to a single processor. If computation and synchronization time exceed the capability of a processor and process is schedulable, one or more processes are distributed to another processor to achieve schedulability. Using execution order of processes gained during schedulability analysis phase, static scheduling scheme is done. Sporadic processes are sent to a processor to have surplus capability enough to satisfiy the deadline constraints of sporadic processes.

프로그램유도 컴비네이터를 이용하는 함수프로그램의 프로세스망 구성

신승철(Shin Seung Cheol),유원희(Yoo Weon Hee) 한국정보처리학회 1996 정보처리학회논문지 Vol.3 No.3

For parallel implementations of functional programs without concurrent primitives, the -calculus encodings have been introduced. A functional program may be transformed into a process network using process calculi by the -calculus encoding and the result of a program can be obtained by a deal of communication actions in it''s process network. But the -calculus encodings cause too many communication actions even in constant expressions. This paper shows the encoding for a combinator program without concurrency primitives which can combine the graph reduction and the process-net reduction using computable processes, ''chores''. A ''chores'' may have graph reduction functions for primitive operations of constants for which local graph reduction may be possible, and be encoded from a ''G-reducible'' subexpression which is obtained by an annotation and transformation for a combinator program, assuring that it does not include any combinator application. Also, we show that a process network with chores raises less communication actions than one without chores.

할당공간의 크기 변화를 통한 세대별 메모리 재활용 알고리즘

주형석(Hyung Seok Joo),유원희(Weon Hee Yoo) 한국정보과학회 1996 정보과학회논문지(B) Vol.23 No.11

세대별 메모리 재활용(generational garbage collection) 방법[2]은 일반적인 복사 방법에 비해 프로그램의 실행시간을 단축시킬 수 있는 장점을 갖고 있으나 할당공간(allocation space)과 복사공간(copy space)을 고정된 크기로 운영하기 때문에 메모리의 이용효율이 저하된다. 따라서, 효율적인 기억장소 운영을 위하여 복사공간의 사용되지 않는 공간을 줄이기 위한 방안이 필요하다. 본 논문에서는 세대별 메모리 재활용 방법을 개선하기 위하여 전-세대로 부터 발생되는 활성노드량, 활성노드의 증감율, 안정적 증감율 등의 경험적 정보를 이용하여 효율적인 메모리 운영을 위한 알고리즘을 제안한다. 개선된 알고리즘에 의해 메모리 이용효율이 향상되며, 메모리 재활용을 위한 호출을 줄일 수 있다. 제안된 방법은 결합자 그래프 감축기(combinator graph reduction machine) 상에서 구현하며, 이에 대한 성능 평가를 보인다. Generational garbage collection has an advantage of faster program execution time than general copying garbage collection. But, it suffers poor performance in memory management, because it allocates free space to allocation space and copy space in same size. For efficient memory usage, we need to reduce unused space in copy space. To improve generational garbage collector, we extract heuristic information from pre-generation, such as amount of active node, variation of active node, and safety variation, So, we propose algorithm for efficient memory management using this information. This algorithm enhances performance in memory management, and reduces invocation of garbage collector. Proposed mechanism is implemented on a combinator graph reduction machine, and performance evaluation of the result is given.

CTOC에서 3-주소 코드를 위한 정적 타입 추론

김기태 ( Ki-tae Kim ),유원희 ( Weon-hee Yoo ) 한국정보처리학회 2004 한국정보처리학회 학술대회논문집 Vol.11 No.2

자바 바이트 코드 명령어는 타입에 관한 정보를 포함하고 있다. 그러나 기본적으로 스택 기반으로 동작이 수행되기 때문에 지역 변수를 위한 명시적인 타입을 가지지 않는다. 하지만 프로그램의 최적화나 역컴파일을 위해서는 지역 변수의 타입을 아는 것이 중요하다. 본 논문은 스택을 사용하지 않는 3-주소 코드에서 지역 변수를 위한 정적 타입 추론을 구현한다. 이를 위해 본 논문에서는 SSA와 방향성 그래프를 적용한다.