Title :
Formal verification of RACE protocol using SSM
Author :
Kim, Hahnsang ; Choi, Jin-Young ; Ki, Ando ; Han, Woo-Jong
Author_Institution :
Dept. of Comput. Sci. & Eng., Korea Univ., Seoul, South Korea
Abstract :
Cache coherence protocols are important for operating a shared-memory multiprocessor system with efficiency and correctness. Cache coherence protocols have become increasingly complex because physical memory is logically distributed, so that it is difficult for programmers to understand the view of logical shared-memory systems. Since random testing and simulations are not enough to validate the correctness of these protocols, it is necessary to develop efficient and reliable verification methods. Through the use of the Symbolic State Model (SSM) of Fong Pong (1995), we verified a directory-based protocol called the RACE (Remote-Access Cache coherence Enforcement) protocol. The protocol is verified for any system size, without state-space explosion
Keywords :
cache storage; coherence; formal verification; memory protocols; shared memory systems; state-space methods; RACE protocol; cache coherence protocol; directory-based protocol; formal verification; logical shared-memory systems; logically distributed memory; protocol correctness validation; random testing; remote-access cache coherence enforcement; shared-memory multiprocessor system; symbolic state model; system size; Access protocols; Computer science; Electronic mail; Error correction; Explosions; Formal verification; Multiprocessing systems; Network interfaces; State-space methods; Testing;
Conference_Titel :
TENCON 99. Proceedings of the IEEE Region 10 Conference
Conference_Location :
Cheju Island
Print_ISBN :
0-7803-5739-6
DOI :
10.1109/TENCON.1999.818611
