초록 ▼

□ 연구개요
멀티코어 프로그래밍은 병렬화를 통해 시스템의 성능을 비약적으로 향상할 수 있지만, 그 안전성과 정확성을 검증하기 매우 어려운 양날의 검이다. 따라서 멀티코어 프로그래밍을 중요한 애플리케이션에 사용하려면 통상적으로 사용하는 코드 리뷰나 테스팅과 같은 방법에서 더 나아가 그 안정성과 정확성을 철저히 검증해야만 한다. 그러나 멀티코어 프로그램을 위한 검증 이론은 아직 실제 시스템에 적용할 수 있을 정도로 발전하지 않았다. 본 연구에서는 효율적인 멀티코어 소프트웨어를 수학적인 명세부터 실행 가능한 머신 코드까지 엄밀하게

□ 연구개요
멀티코어 프로그래밍은 병렬화를 통해 시스템의 성능을 비약적으로 향상할 수 있지만, 그 안전성과 정확성을 검증하기 매우 어려운 양날의 검이다. 따라서 멀티코어 프로그래밍을 중요한 애플리케이션에 사용하려면 통상적으로 사용하는 코드 리뷰나 테스팅과 같은 방법에서 더 나아가 그 안정성과 정확성을 철저히 검증해야만 한다. 그러나 멀티코어 프로그램을 위한 검증 이론은 아직 실제 시스템에 적용할 수 있을 정도로 발전하지 않았다. 본 연구에서는 효율적인 멀티코어 소프트웨어를 수학적인 명세부터 실행 가능한 머신 코드까지 엄밀하게 검증하기 위한 이론을 개발하고 실제 시스템에 적용한다.

□ 연구 목표대비 연구결과
연구 분야의 동향에 따라 일부 세부 목표를 수정했고, 수정한 목표를 초과 달성했다: 느슨한 메모리상의 동시성 프로그램의 모듈식 검증을 용이하게 하는 논리적 원자성 기반 강한 명세 작성 방법 개발. 느슨한 메모리상의 복잡한 동시성 프로그램의 편리한 검증을 위한 다구역 불변식과 atomic points-to 이론 개발. 다구역 불변식과 atomic points-to를 이용해 강한 명세를 다양한 자료구조에 대해 모듈식으로 검증. 포인터 보호 기법과 구역 보호 기법의 장점을 취하고 단점을 보완하는 포인터-구역 보호 기법 개발. 포인터 보호 기법의 적용성을 향상하는 HP++ 기법 개발. 포인터 보호 기법과 구역 보호 기법의 명세 작성 및 검증. 각 메모리 재활용 기법을 사용하는 다양한 자료구조 검증. 비동기 코루틴 실행기에 사용되는 Chase-Lev 데크(양방향큐)의 검증.

□ 연구발성과의 활용 계획 및 기대효과 (연구개발결과의 중요성)
멀티코어 프로그램 검증 기법: 본 연구의 동시성 프로그램 검증 이론을 적용하면, 비행기나 원자력 발전기와 같이 안전이 극도로 중요한 시스템에서도 자신 있게 멀티코어 프로그램을 사용할 수 있게 될 것이다. 또한 안전성이 검증되면 공격적인 최적화를 통해 대부분의 컴퓨터 시스템에서 큰 성능 이득을 볼 수 있을 것이다.
메모리 재활용 기법: 포인터-구역 보호 기법과 HP++을 동시성 자료구조를 사용하는 고성능 시스템 소프트웨어에 적용해 작업 처리량과 지연시간을 개선할 수 있다.

(출처 : 연구결과 요약문 2p)

목차 Contents

• 표지 ... 1
• 연구결과 요약문 ... 2
• 목차 ... 3
• 1. 연구개발과제의 개요 ... 4
• 1.1. 목적 ... 4
• 1.2. 필요성 ... 4
• 1.3. 목표 ... 5
• 2. 연구개발과제의 수행 과정 및 수행 내용 ... 7
• 2.1. 목표 2-1: 메모리 재활용기 (1년차) ... 7
• 2.2. 이론 연구 목표 조정 ... 7
• 2.3. 목표 1-3: 느슨한 메모리상의 동시성 프로그램을 위한 강한 명세 작성 방법론 개발 (1-2년차) ... 9
• 2.4. 목표 1-4: 느슨한 메모리를 위한 동시성 프로그램 검증 방법론 개발 (2년차) ... 9
• 2.5. 목표 2-1: 메모리 재활용기 검증 (2-3년차) ... 10
• 2.6. 목표 2-1: 메모리 재활용기 개발 (3년차) ... 12
• 2.7. 목표 2-2: 비동기 코루틴 실행기 (3년차) ... 12
• 3. 연구개발과제의 수행 결과 및 목표 달성 수준 ... 13
• 3.1. 정성적 연구개발성과(연구개발결과) ... 13
• 3.2. 세부 정량적 연구개발성과 ... 14
• 3.3. 목표 달성 수준 ... 14
• 3.4. 목표 미달 시 원인 분석 ... 14
• 4. 연구개발성과의 관련 분야에 대한 기여 정도(연구개발결과의 중요성) ... 15
• 4.1. 메모리 재활용 기법 ... 15
• 4.2. 멀티코어 프로그램 검증 기법 ... 15
• 5. 연구개발성과의 관리 및 활용 계획 ... 15
• 5.1. 메모리 재활용 기법 ... 15
• 5.2. 프로그램 검증 기법 ... 15
• 6. 자체점검표 ... 16
• 7. 참고문헌 ... 17
• 붙임1. 세부 정량적 연구개발성과 ... 19
• 붙임2. 연구책임자 대표적 연구실적 및 증빙(요약문 및 사본) ... 25
• 끝페이지 ... 37