| 연구목표 |
**효율적인 멀티코어 소프트웨어를 수학적인 명세부터 실행가능한 머신 코드까지 엄밀하게 검증하기 위한 이론을 개발하고 실제 시스템에 적용***목표 1: 이론 개발.* 효율적인 논블로킹 (nonblocking) 멀티코어 소프트웨어를 엄밀하게 검증하기 위한 최첨단 이론인 동시성 분리 논리는 (concurrent separation logic) 아직 실제 멀티코어... |
| 연구내용 |
*이론 개발 1: 동시성 분리 논리에서 SC fence 지원*. 기존 동시성 분리 논리를 확장하여 SC fence를 사용해 동기화한 프로그램을 검증할 수 있도록 지원한다. 이를 통해 실제 멀티코어 시스템에서 사용되는 느슨한 동시성을 위한 동기화 기법을 검증할 수 있게 된다.*이론 개발 2: 논블로킹 멀티코어 프로그램을 위한 컴파일러 검증.* 소스 코드만이 ... |
| 기대효과 |
**멀티코어 프로그램의 안전성, 정확성과 효율성 확보***안전성과 정확성.* 멀티코어 프로그램은 본질적인 비결정성으로 인해 안전성과 정확성을 확신하기 매우 어렵다. 코드 리뷰나 테스팅도 싱글코어 프로그램과는 달리 멀티코어 프로그램에서는 효과적이지 않다. 따라서 멀티코어 프로그램의 안전성과 정확성을 확신하기 위해서는 반드시 엄밀하게 검증해야 한다. 이 연구과... |
| 키워드 |
멀티코어,동시성,프로그램 검증,분리 논리,컴파일러 검증,시뮬레이션 |