마일스톤(2) - 좌장 : 오학주 교수(고려대학교)
| 발표 | 임현승 교수(강원대학교) | 시간 | 10:00-10:25 |
|---|---|---|---|
| 제목 | XML 프로그램을 위한 거꾸로 타입 추론 기법 | ||
| 요약 | XML 타입체킹은 XML이 표준으로 도입된 이후부터 꾸준히 제기되어 온 문제이다. W3C 표준 XML 언어들은 XML 문서를 탐색하고 정보를 추출하기 위해 XPath 축 표현식을 이용한다. XPath 축 표현식은 강력하지만 타입체킹이 어렵다. 본 발표에서는 XPath를 사용하는 W3C 표준 XML 질의 언어인 XQuery를 위한 거꾸로 타입 추론 기법을 소개한다. 거꾸로 타입 추론은 프로그램과 그 프로그램의 실행 결과로 생성될 XML 문서의 타입이 주어졌을 때, 프로그램이 입력으로 취할 수 있는 XML 문서의 타입을 추론한다. 본 연구에서 제안하는 시스템은 기존 연구와 달리 XPath 축 표현식의 타입을 정확하게 추론하는 것으로 사료된다. | ||
| 발표 | 허충길 교수(서울대학교) | 시간 | 10:25-10:50 |
| 제목 | Towards verified compilation for the LLVM compiler | ||
| 요약 |
In this talk, I will give a high-level overview of my group's long-term project, called LLVMberry. The goal of the project is to develop a practical tool for formally guaranteeing the absence of compiler bugs in the LLVM compiler. More specifically, we develop a verified translation validator for the LLVM compiler. The validator checks the absence of optimization bugs in any given compilation result.
In the talk, I will show how we make our validator to be (i) formally sound (ie, generating a machine-checked proof of correctness of any compilation result passing the validator); (ii) complete by design (ie, validation succeeds for any compilation result unless one makes a mistake in the design or implementation of the compiler or validator); and (iii) practical (ie, validation cost is cheap enough for validator users; and development cost is cheap enough for validator writers). | ||
| 발표 | 강지훈(서울대학교) | 시간 | 11:00-11:25 |
| 제목 | C/C++ 동시성 메모리 모델 | ||
| 요약 |
C/C++ 동시성 메모리 모델은 오랫동안 제련된 아이디어를 집약한 좋은 모델이지만, 아직 뚱딴지같은 행동(out-of-thin-air behavior)을 허용 하는 단점이 있다. 뚱딴지같은 행동이란 대입하지도 않은 값이 메모리에 저장되는 행동을 말한다. 이런 행동은 (1) 프로그래머가 이해하기 힘들며, (2) 좋은 검증 기법을 고안하기 힘들고, (3) 컴파일이 어려우며, (4) 시스템의 보안을 위협한다.
우리는 뚱딴지같은 행동이 없는 C/C++ 동시성 메모리 모델을 제시한다. |
||
| 발표 | 김윤승(서울대학교) | 시간 | 11:25-11:50 |
| 제목 | Lightweight verification of separate compilation | ||
| 요약 | CompCert와 같은 검증된 컴파일러는 검증에 필요한 노력을 줄이기 위해 모든 소스 코드를 모아서 컴파일하는 경우만 가정하고 증명하였다. 그러나 실제로는 소스 코드를 각각 컴파일 후 링크하는 분할 컴파일 기법이 주로 사용된다. 분할 컴파일의 옳음을 정형적으로 증명하기 위한 연구가 있어왔으나 모두 이론과 구현이 복잡하여 실제에 적용하기에는 어려움이 있다. 우리는 동일한 검증된 컴파일러를 사용한다는 가정 하에 매우 간단히 분할 컴파일의 옳음을 증명할 수 있는 기법을 고안하였고, 이를 CompCert 2.4 버전에 적용하였다. 분할 컴파일을 검증하는 연구를 통해 CompCert에 존재했던 관련 버그를 찾아내기도 하였다. | ||
| 발표 | 고유선(연세대학교) | 시간 | 11:50-12:15 |
| 제목 | Program transformation of the synchronous data flow programming model | ||
| 요약 | Because of a growing interest in Big Data stream processing in the Cloud, the synchronous data flow (SDF) programming model is being revisited for its abundance of parallelism expressed through independent actors that communicate via FIFO data channels. FIFO data channels isolate the producer from the consumer, which is desirable as an abstraction mechanism for actor communication. However, the FIFO queue abstraction obscures data flow information which disrupts standard compiler optimizations. In this talk, program transformations that shift FIFO queue management from run-time to compile time will be introduced. The transformation eliminates splitters and joiners, and facilitates the formation of static single assignment form. Our transformation is conducted in two steps, (1) a local direct access transformation which explicates the token-flow within an actor, and (2) a global direct access transformation which resolves queue accesses across the whole program. We employ static program analysis to determine the token-flow within an actor and enhance the effectiveness of the transformation. | ||