Many software systems today are concurrent programs as multi-core processors become popular. However, the correctness of an industrial-size concurrent program (e.g. operating system) is difficult to achieve by the traditional testing or model checking technique. In this research, we propose a light-weight concurrency bug detection technique based on bug pattern matching targeting for Linux kernel source code. In order to understand concurrency bugs (e.g. deadlock, data race), we first survey the previously reported bugs detected from Linux file systems, and then classify the bugs with respect to the five attributes: symptom, fault, resolution, synchronization primitives, and synchronization granularity. Second, we identify ten concurrency bug patterns. And then we develop the bug pattern detectors and applied to the Linux file systems. Finally, and foremost, we improve the accuracy of the concurrency bug detection technique by enhancing semantic information in pattern matching. We demonstrate the effectiveness of our technique through detection of concurrency bugs in the Linux file systems.
멀티코어 프로세서가 널리 보급됨에 따라 오늘날 많은 소프트웨어 시스템은 동시성 프로그램(concurrent program)으로 작성된다. 하지만, 기존의 테스팅 기법과 모델 체킹 기법으로는 운영체제와 같은 상용 프로그램 수준 크기의 동시성 프로그램의 동작정확성 검증이 어려운 실정이다. 이 연구에서는 리눅스 운영체제 커널 소스 코드를 주대상으로 개발한 결함 패턴 매칭(bug pattern matching) 기법을 통한 동시성결함 검출 기법을 소개한다. 데이터 레이스(data race), 교착상태(deadlock)와 같은 동시성결함을 이해하기 위하여, 리눅스 파일 시스템에서 실제 발견되었던 결함들을 조사하였으며, 각 결함을 증상, 원인, 해결방법, 관련 동기화 기법, 동기화 범위에 따라 분류하는 분류체계를 개발하였다. 이를 바탕으로 10개의 동시성결함 패턴을 만들었으며, 패턴 매칭을 통해 결함을 검출하는 프로그램을 작성하여 리눅스 파일 시스템 코드에 적용하였다. 마지막으로, 패턴매칭에 시맨틱 정보를 추가로 고려함으로써 동시성결함 검출의 정확도를 향상 시켰으며, 개발된 기술을 리눅스 파일 시스템 코드에 적용하여 유용성을 확인하였다.
