Deriving Control Flow Analyses for Java by Multi-level Rule Transformation

Byeong-Mo Chang(창병모) 한국정보과학회 2013 정보과학회논문지 : 소프트웨어 및 응용 Vol.40 No.10

집합-기반 분석을 보다 굵은 수준으로 설계할 수 있는 변환-기반 방법이 제안되었다. 이 방법을 이용하면 식-수준의 분석으로부터 규칙 변환을 통해 덜 정확하지만 보다 효율적인 분석을 설계할 수 있다. 이 방법은 원래 분석이 각 식에 대해서 하나의 집합 변수를 구성하는 식-수준에서 설계되었다고 가정하였으므로, 식-수준의 분석에만 적용 가능하다는 한계를 가지고 있다. 그러나 이 아이디어는 꼭 식 수준에 한정될 필요가 없으며 확장될 필요가 있다. 본 연구에서는 규칙-변환 방법을 확장하여 어느 수준의 분석에도 적용될 수 있도록 확장하고 이를 통해 실용적인 집합-기반 분석을 설계할 수 있는 다단계 규칙-변환 메커니즘을 제시한다. 또한 이 변환 메커니즘을 이용하여 프로시저 사이의 제어흐름을 보여주는 Java 언어를 위한 다양한 수준의 제어흐름 분석들 사이의 관계를 조명하고 이를 정리한다. A transformation-based approach was proposed to design constraint-based analyses at coarser granularity. This approach lets us be able to design a less precise but more efficient version of an original expression-level analysis by transforming the original construction rules. Since this approach assumes that the original analysis is designed at expression-level. it has a limit that it is applicable only to expression-level analyses. However, this idea need not be confined to expressionlevel, and need to be extended. In this paper, we extend this rule-transformation approach so that it can be applied to any analyses which are designed at any level, and so provide a {\em multi-level} mechanism to design practical constraint-based analyses by rule transformation. Using this approach, we also investigate the relationship between a number of CFAs for Java systematically, which determine the interprocedural control flow information.

순환 논리 질의 최적화를 위한 정적 필터의 고정점 계산

창병모(Byeong-Mo Chang),최광무(Kwang-Moo Choe),한태숙(Taisook Han) 한국정보과학회 1993 정보과학회논문지 Vol.20 No.9

정적 필터링은 시스템 그래프 수행을 기초로한 순환 논리 질의 최적화 방법이다. 이 방법은 수행하는 동안에 정적 필터를 이용하여 데이터의 흐름을 제한한다. 본 논문은 정적 필터의 계산 과정을 partially ordered set(poset) 위에서 하나의 변환으로 정형화하고 그 변환의 최소고정점을 구함으로써 정적 필터를 구한다. 계산된 정적 필터의 완전성(completeness)은 제시된 정형화를 이용하여 증명한다. 또한 관련 연구에 대해서 간단히 살펴보고 정적 필터링 방법과 비교한다. 본 논문에서는 정적 필터와 그 계산에 대한 정형화된 새로운 관점을 제공한다. Static filtering is a graph-bsed optimization method for recursive logic queries based on the system graph evaluation. It restricts data-flow during evaluation by means of static filers. We formalize the computation of static filters by defining a transformation on a partially ordered set (poset) so that the least fixed point of the transformation can be the static filters. The static filters are computed by computing the least fixed point of the transformation. The completeness of the static filtering with the computed static filters is proved based on the formalism. Moreover, we review some related works in brevity and compare the static filtering with them. The formalism presented in this paper gives a new formal view to static filter and its computation.

Function - free 논리 프로그램의 Bottom - up 수행의 최적화를 위한 정적 필터의 최소 고정점 정형화

창병모(Byeong-Mo Chang),최광무(Kwang-Moo Choe),한태숙(Tai-sook Han) 한국정보과학회 1992 한국정보과학회 학술발표논문집 Vol.19 No.1

필터링을 이용한 논리 프로그램의 bottom-up 수행은 논리 프로그램 수행의 최적화를 위한 강력한 방법이다. 본 논문에서는 정적 필터의 계산을 연립 방정식 형태로 정형화하고 그 최소 고정점(least fixed point)이 구하고자하는 정적 필터가 되도록 한다. 정적 필터의 계산 과정은 연립 방정식의 최소 고정점을 구하는 과정으로써 설명된다. 여기서 구한 정적 필터를 일반화하여 각 rule의 sideways passing graph(SPG)를 고려하여 부분 정적 필터(partial static filter)를 계산할 수 있으며 동적 필터는 부분 정적 필터로부터 시작하여 단계적으로 계산할 수 있다. 이를 위한 방법이 [CCH92]에 설명되어 있으며 정적 필터만을 이용할 때보다 효율적임이 증명되었고 그 방법의 completeness가 증명되었다.

논리 프로그램의 두 단계 추상 해석 틀

창병모(Byeong-Mo Chang) 한국정보과학회 1996 정보과학회논문지(B) Vol.23 No.6

추상 해석은 Cousot와 Cousot에 의해서 제안된 시맨틱스에 기초한 데이터 흐름 분석 틀이다. 본 논문에서는 논리 프로그램을 위해서 상향 분석과 하향 분석으로 이루어진 두 페이즈 추상 해석 틀을 제안한다. 이 틀에 기초한 분석은 질의에 관련된 절의 모든 성공 패턴에 대한 근사값을 제공한다. 제안된 틀에 기초한 분석 예로서 타입 분석 방법을 제시한다. 또한 제안된 틀에 기초한 분석 결과를 이용하여 논리 프로그램의 수행을 최적화 하는 예들을 제시한다. Abstract interpretation is a semantics-based data-flow analysis framework proposed by Cousot and Cousot. This paper provides a two-phase abstract interpretation framework, which consists of a bottom-up phase followed by a top-down phase. Analyses based on this framework give an approximation of all success patterns of clauses relevant to a query A type analysis is given as an example analysis based on the framework. Optimization techniques for improving execution of logic programs are given, which use the results of analyses based on the framework.

상향식 추상 해석을 이용한 논리 프로그램의 AND/0R 병렬 수행 모델 개선

창병모(Byeong-Mo Chang),최광무(Kwang-Moo Choe),한태숙(Taisook Han) 한국정보과학회 1994 정보과학회논문지 Vol.21 No.5

본 논문에서는 상향식 추상 해석(bottom-up abstract interpretation)을 이용하여 논리 프로그램의 병렬 수행 모델인 AND/OR 프로세스 모델을 개선한다. 이를 위하여 기존의 상향식 추상 해석을 깊이 k 추상화를 기초로하여 프로그램의 각 절의 성공 패턴(success pattern)에 대한 근사값을 구할 수 있도록 확장하였다. 확장된 추상 해석은 각 절의 성공 패턴에 대한 근사값을 구할 수 있으며 이를 이용하면 어떠한 subgoal은 실행중에 실패할 것이라는 사실을 컴파일 시간에 결정할 수 있다. 본 연구에서는 이러한 성질을 이용하여 AND/OR 프로세스 모델을 개선하며 이 모델에서 AND 프로세스는 자식 OR 프로세스가 실패할 것이 확실한 경우에 자식 OR 프로세스를 생성하지 않는다. 이 방법론은 다른 하향식 (병렬) 수행에도 쉽게 적용 가능하다. This paper improves the AND/OR Process Model, a parallel execution model of logic programs, using a bottom-up abstract interpretation. We first extend a bottom-up abstract interpretation framework so that it can approximate the program's success patterns of program clauses by depth k abstraction. By the ability of the extended framework to approximate possibly non-ground success patterns for clauses, it can be statically determined whether some subgoals will fail during execution. We improve the AND/OR Process Model using this property, in which AND processes do not create child OR processes if it is statically determined that they will fall during execution. This approach can also be easily applied to other top-down (parallel) execution models.

논리 프로그램의 AND 병렬 수행을 위한 정형적인 제안

창병모(Chang Byeong-Mo),최광무(Choe Kwang-Moo) 한국정보과학회 1990 한국정보과학회 학술발표논문집 Vol.17 No.1

본 논문에서는 논리 프로그램의 AND 병렬 수행을위한 하부구조 (framework)를 논리적인 정의를 통해서 제안하고 제안된 하부구조를 기초로하여 지능적인 resetting 방법을 제안한다. 여기서 제안된 지능적인 resetting 방법은 실패한 리터럴의 바인딩 정보를 기초로하며, 이 정보는 resetting 할 때 지능의 주된 요인이다. 우리들은 제안된 지능적인 resetting 방법의 정확성을 framework에 기초하여 간단하고 논리적인 방법으로 증명한다.

논리 프로그램의 타입 및 모드 분석의 계층 구조

창병모(Byeong-Mo Chang) 한국정보과학회 1999 정보과학회논문지(B) Vol.26 No.3

논리 프로그램의 타입 및 모드 분석은 실행 시간에 변수가 갖게 되는 텀의 집합에 대한 근사 값을 구하는데 보통 요약 해석을 기반으로 하여 설계되고 개발되어 왔다. 이 논문에서는 타입 및 모드 분석을 위해서 설계된 다양한 요약 도메인을 고려하여 그들간의 계층 관계를 Galois insertion을 기준으로 밝힌다. 이 논문에서는 요약 도메인으로써 타입 그래프, 깊이-k 타입, 깊이-k 모드, 순환 모드, 그리고 모드를 고려할 것이다. 특히 깊이-k 모드는 타입 및 모드 분석을 통합하기 위한 도메인으로써 깊이-k 타입을 확장하여 제안하였다. Type and mode analyses of (constraint) logic programs approximates a set of terms, with which arguments can be instantiated during execution. They have been designed and developed usually based on abstract interpretation. This paper considers various abstract domains designed for type and mode analysis, and to show a hierarchy of them in terms of Galois insertion. We are going to take the following abstract domains into consideration : type graph, depth-k type, depth-k mode, recursive mode, and mode. Depth-k mode is proposed as a new abstract domain for an integration of type and mode analysis, by extending depth-k type of Sato and Tamaki's.

정적분석을 이용한 자바 언어의 권한검사 시각화 시스템

김윤경,창병모,Kim, Yun-Kyung,Chang, Byeong-Mo 한국정보처리학회 2006 정보처리학회논문지 A Vol.13 No.5

Java 2에서 자원에 대한 접근 권한관리를 위하여 프로그래머는 프로그램 실행에 필요한 권한들을 정책파일(polic file)에 기술하고, 보안관 리자(Security Manager)를 설치하여 프로그램을 수행시킨다. 프로그램 실행 중에 자원에 대한 접근을 시도할 때마다. 보안관리자는 스택 인스펙션을 통해 접근 권한이 있는지 검사한다. 본 논문에서는 프로그래머가 안전한 보안정책을 세우는데 편의를 제공하고자 권한검사 관련 정보를 정적으로 분석하여 시각적으로 보여주는 시스템을 구현하였다. 권한김사 시각화 시스템은 정적 권한검사 분석에 기반하여, 각 메소드 별로 항상 성공하거나 항상 실패하는 권한검사를 계산한다. 프로그래머는 프로그램을 실행시켜보기 전에 권한검사와 스택 인스펙션이 어떻게 수행되는지 시각적으로 확인해 볼 수 있다. 이러한 정보를 토대로 안전한 보안정책을 세우기 위해 프로그램이나 정책파일을 수정할 수 있다. In Jana 2, to enforce a suity policy of a program, programmer writes permission sets required by the code at the policy file, sets Security Manager on system and executes the program. Then Security Manager checks by stack inspection whether an access request to resource should be granted or denied whenever code tries to access critical resource. In this paper, we develop a visualization tool which helps programmers enforce security policy effectively into programs. This system is based on the static permission check analysis which analyzes permission checks which must succeed or fail at each method. Based on this analysis information, programmer can examine visually how permission checks and their stack inspection are performed. By modifying program or policy file if necessary and examining analysis information repeatedly, programmer can enforce security policy correctly.

Java 프로그램의 효율적인 분석을 위한 집합-기반 분석의 변환

조장우,창병모,Jo, Jang-Wu,Chang, Byeong-Mo 한국정보과학회 2002 정보과학회논문지 : 소프트웨어 및 응용 Vol.29 No.7

본 논문에서는 Java 프로그램에 대한 집합기반 분석 설계 시, 효율적인 분석을 위해 분석의 단위를 조절하는 생성규칙 변환 방법을 제안한다. 기존의 생성규칙을 변환함으로서 기존의 분석보다는 정확성이 감소하지만 보다 효율적인 분석을 설계할 수 있다. 본 방법을 응용한 예로서 기존의식 수준의 클래스 분석과 예외 상황 분석에 대해 생성규칙 변환을 사용하여 효율적인 클래스 분석과 예외상황 분석을 설계하였다. 클래스 분석에서는 메소드와 필드 변수 단위의 분석을 설계하였으며, 예외상황 분석에서는 메소드와 try 구문 단위의 분석을 설계하였다. 그리고 예외상황 분석에서는 식 수준의 분석과 변환된 메소드 수준의 분석이 각 메소드에 대해서 동등한 정보를 제공함을 보였다. This paper proposes a transformation-based approach to design constraint-based analyses for Java at a coarser granularity. In this approach, we design a less or equally precise but more efficient version of an original analysis by transforming the original construction rules into new ones. As applications of this rule transformation, we provide two instances of analysis design by rule-transformation. The first one designs a sparse version of class analysis for Java and the second one deals with a sparse exception analysis for Java. Both are designed based on method-level, and the sparse exception analysis is shown to give the same information for every method as the original analysis.

Java 언어를 위한 쓰레드 모니터링 시스템

문세원,창병모,Moon Se-Won,Chang Byeong-Mo 한국정보처리학회 2006 정보처리학회논문지 A Vol.13 No.3

본 연구에서는 견고한 멀티 쓰레드 소프트웨어 개발을 돕기 위한 쓰레드 모니터링 시스템을 개발하였다. 이 시스템은 쓰레드 실행 과정과 동기화 과정를 시각적으로 추적, 모니터링 할 수 있다. 또한 사용자는 실행 전에 옵션 선택을 통해 관심 있는 쓰레드와 동기화만을 선택하여 이들을 중점적으로 모니터링 할 수 있으며 실행 후에는 실행된 쓰레드와 동기화의 특징을 요약한 프로파일 정보를 제공한다. 본 연구에서는 코드 인라인 기법을 기반으로 이 시스템을 구현하였으며 실험을 통한 실험 결과를 통해 그 효융성을 보인다. To assist developing robust multithreaded software, we develop a thread monitoring system for multithreaded Java programs, which can trace or monitor running threads and synchronization. We design a monitoring system which has options to select interesting threads and synchronizations. Using this tool, programmers can monitor only interesting threads and synchronization in more details by selecting options. It also provides profile information after execution, which summarizes behavior of running threads and synchronizations during execution. We implement the system based on code inlining, and presents some experimental results.