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

Volume

2

fYear

1999

fDate

36495

Firstpage

1083

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;

fLanguage

English

Publisher

ieee

Conference_Titel

TENCON 99. Proceedings of the IEEE Region 10 Conference

Conference_Location

Cheju Island

Print_ISBN

0-7803-5739-6

Type

conf

DOI

10.1109/TENCON.1999.818611

Filename

818611