2011년 5월 23일 월요일

자바 메모리 모델을 이용한 멀티 스레드 자바 코드 검증

최신의 컴파일러는 실행 속도를 높이기 위해서 최적화 작업을 수행한다. 그러나 최적화 작업 중에 프로그램 구문의 실행 순서가 바뀔 수 있다. 단일 스레드 소프트웨어 에서는 최적화가 실행 결과에 영향을 주지 않지만 멀티 스레드 소프트웨어에서는 최적화로 인해서 기존의 실행 과
정을 계산하는 방법으로는 설명할 수 없는 실행 결과가 발생할 수 있다. 이 문제점을 해결하기 위해서 자바 메모리 모델이 제안되었다. 자바 메모리 모델은 구문의 재배치를 고려하여 멀티 스레드 소프트웨어의 가능한 실행 과정을 명세하고 있다. 현재 자바 메모리 모델은 자바의 표준 메모리 모델로 정의되어 있다. 하지만 대부분의 멀티스레드 소프트웨어 검증 도구는 자바 표준 메모리 모델인 자바 메모리 모델 대신에 순차 일관성메모리 모델만을 고려하고 있다. 순차 일관성 메모리모델에서는 구문의 재배치를 고려하지 않는다. 본 논문에서는 자바 메모리 모델을 이용한 소프트웨어 모델 체킹 기법을 설명한다. 이를 이용하여 기존 소프트웨어 검증 도구인 JavaPathFinder 에서 오류가 없다고 한 소프트웨어의 오류를 찾아내었다.

키워드 : 자바 메모리 모델, 검증, 멀티스레드 소프트웨어, 만족성 문제

논문받기

댓글 없음:

댓글 쓰기

블록체인 개요 및 오픈소스 동향

블록체인(block chain) 블록체인은 공공 거래장부이며 가상 화폐로 거래할때 발생할때 발생할 수 있는 해킹을 막는 기술. 분산 데이터베이스의 한 형태로, 지속적으로 성장하는 데이터 기록 리스트로서 분산 노드의 운영자에 의한 임의 조작이 불가...