다중 프로세서 시스템에서 각각의 프로세서에 할당되어 있는 지역 캐쉬에 데이터의 복사본이 분산 공유되어 있는 경우 데이터의 일관성 유지가 필요하다. 따라서 캐쉬 일관성 유지 프로토콜은 공유 메모리 다중 프로세서 시스템의 정확하고 효율적인 작동에 중요하다. 그러므로 시스템이 복잡해짐과 비례하여 현재 사용되고 있는 무작위적 테스트나 시뮬레이션은 프로토콜의 정확성을 확인하기에 충분하지 못하므로 보다 효율적이고 믿을 만한 검증 방법이 필요하다. 본 논문은 ETRI에서 개발된 캐쉬 일관성 프로토콜인 RACE(Remote Access Cache coherent Enforcement)프로토콜의 몇 가지 특성(property)들을 정형기법에 쓰이는 도구 중의 하나인 VIS(Verification Interacting with Synthesis)를 이용하여 검증한다.

Caches in a multiprocessing environment introduce the cache coherence problem. When multiple processors maintain locally cached copies of a unique shared-memory location, any local modification of the location can result in a globally inconsistent view of memory. Cache coherence protocols are important to operate a shared-memory multiprocessor system with efficiency and correctness. Since random testing and simulations are not enough to validate correctness of protocols, it is necessary to develop efficient and reliable verification methods. In this paper we present our experience in using VIS (Verification Interacting with Synthesis), a tool of formal method, to analyze a number of property of a cache coherence protocol, RACE (Remote Access Cache coherent Enforcement).