Esterel is an imperative synchronous language with the perfect synchrony hypothesis which divides time into a sequence of logical time units. Esterel is well-adapted to develop control-dominant reactive systems. It is because imperative features of Esterel on the synchrony hypothesis help to control synchronization and preemption among threads that are executed simultaneously. However, it is hard to compute exact synchronization process and interferences among threads from Esterel programs, and this makes it difficult to analyze or diagnose the programs. In this thesis, we propose a new control flow graph (CFG) and a new logical semantics of Esterel that focus on exposing the synchronization process and implicit interferences among threads.
First, we present an over-approximated CFG of an Esterel program. Simple and convenient CFGs can help to analyze Esterel programs or to detect errors from the programs. Regardless of imperative features of Esterel, combination of parallel execution and preemption causes implicit interferences between threads, and they make it difficult to build CFGs of Esterel programs. Previous researches are not suitable for CFG-based static analyses of Esterel, because they focus on compilation or simulation of Esterel programs. We develop a new method to construct over-approximate CFGs of Esterel programs that expose invisible interferences among threads and show program structures explicitly. The over-approximated CFGs represent all possible execution paths at run-time though they may contain some unreachable paths. Therefore, our CFGs are useful for a program analysis or diagnosis based on graph theory or control-/data- flows.
Second, we present a new logical semantics of Esterel. Explicit synchronization control with imperative features is an important characteristic of Esterel. Esterel has some versions of logical semantics that provide simple and good formalisms for formal verification. However, the entire synchronization process is not explicitly exposed in existing semantics. The implicit synchronization process of former semantics make it hard to check global reachability of some locally erroneous execution paths, and the semantics reject several correct programs that have unreachable erroneous execution paths. Our logical semantics that retains the simplicity of former logical semantics divides derivation rules into two groups: computations within an instant (micro-steps) and computations across instants (macro-steps). This separation helps to expose the synchronization process explicitly and to describe erroneous behaviors formally. Moreover, our semantics can check global feasibility of detected errors through the exposed synchronization process. As a result, the semantics accepts more programs than existing semantics.
We believe that our over-approximated CFGs and logical semantics can be a proper framework to analyze Esterel programs and to detect errors from the programs, and this leads analyzers to achieve meaningful analysis results.
Esterel은 제어 중심의 실시간 반응형 시스템(reactive system) 개발을 목적으로 고안된 절차형(imperative) 동기식(synchronous) 프로그래밍 언어이다. Esterel의 가장 중요한 특징은 시간을 논리적 단위시간(instant)으로 나누고, 절차형 명령어들을 통한 병렬 수행과 동기화, 선점(preemption) 등을 지원하는 점인데, 이들은 반응형 시스템을 효과적으로 설계하는 데에 많은 도움을 준다. 그런데, 병렬로 수행중인 쓰레드 간에 이루어지는 동기화 과정이 프로그램상에 명료하게 나타나지 않기 때문에, 정적 분석 통한 프로그램 분석이나 오류 검출이 쉽지 않다. 본 논문에서는 Esterel의 특징을 정확하게 반영하고 동기화 과정을 명확하게 나타내는 제어흐름그래프(CFG: Control Flow Graph)와 논리적 의미구조(logical semantics)를 제안한다.
먼저, 본 논문에서는 주어진 Esterel 프로그램에 대한 근사-제어흐름그래프 (Over-approximated CFG) 를 생성하는 방법을 제안한다. Esterel에서 병렬 수행과 선점의 복잡한 조합은 프로그램 상에 나타나지 않는 다양한 형태의 제어흐름과 간섭(interference)을 야기하고, 이는 프로그램 분석에서 사용하기에 적합한 제어흐름그래프 생성을 어렵게 한다. 이전의 여러 연구에서 컴파일이나 시뮬레이션 등을 위해 다양한 형태의 제어흐름그래프를 사용하고 있다. 이들은 프로그램에 나타날 수 있는 정확한 제어흐름을 표현하기 위해 프로그램 의존성을 나타내는 부가적인 자료구조나 간섭을 처리해주는 별도의 처리기를 이용하고 있어서 프로그램 분석에서 사용하기에는 적합하지 않다. 본 논문에서 제안한 방법으로 생성된 근사-제어흐름그래프는 동시에 수행중인 쓰레드 간에 발생할 수 있는 모든 간섭을 명시적으로 표현하고, 일반적인 절차형 언어에서 사용하는 것과 유사하게 프로그램의 구조를 직관적으로 표현한다. 실제로 도달 불가능한 경로를 일부 포함할 수 있지만, 실행시간에 나타날 수 있는 모든 경로를 빠짐없이 포함하기 때문에 그래프에 기반한 프로그램 분석이나 오류검출에 매우 적합하게 사용될 수 있다.
그리고, 본 논문에서는 Esterel에 대한 새로운 논리적 의미구조를 제안한다. Esterel에 대한 여러 형태의 논리적 의미구조(logical semantics)가 존재하는데, 이들은 단순 명료한 수식을 이용하기 때문에 프로그램 분석이나 검증에 이용하기가 좋다. 하지만, 기존 의미구조에서는 Esterel 프로그램의 동기화 과정이 명확하게 기술되어 있지가 않아서, 분석 결과의 유효성 여부를 확인 할 수가 없다. 따라서, 각종 오류나 비정상적인 연산에 대한 엄밀한 정의가 어렵고, 검출된 오류 중에서 실행 시간에 절대로 일어날 수 없는 오류를 구분 할 방법이 없다. 본 논문에서 제안한 의미구조는 기존 연구와는 다르게 단위시간 내부에서 일어나는 유도 과정(micro-step)과 단위시간 사이에 일어나는 유도 과정(macro-step)으로 구분하고 있다. 이러한 구분은 이전의 의미구조에서 묵시적으로 이루어지던 동기화 과정을 명시적으로 드러내 표현내고, 다양한 오류를 엄밀하게 정의하는 데에 큰 도움을 준다. 또한, 동기화가 이루어 지는 동안 동기화 이전에 발견된 오류의 유효성 여부를 확인할 수 있어서, 기존 의미구조에서 잘못된 것으로 인식되던 실현 불가능한 오류를 포함한 프로그램들을 올바른 프로그램으로 인식한다.
본 논문에서 제안한 Esterel의 새로운 근사-제어흐름그래프와 논리적 의미구조는 동기화 과정을 보다 명확하게 표현하고 있고, 이는 프로그램의 오류나 비정상적인 연산을 기술하고 검출하거나 프로그램이 가져야하는 제약조건을 검증하는 것과 같이 프로그램을 정적으로 분석하는 데에 유용한 기반 구조가 될 것이다.
