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.
| Original language | English |
|---|---|
| Title of host publication | IEEE Region 10 Annual International Conference, Proceedings/TENCON |
| Publisher | Institute of Electrical and Electronics Engineers Inc. |
| Pages | 1083-1086 |
| Number of pages | 4 |
| Volume | 2 |
| ISBN (Electronic) | 0780357396, 9780780357396 |
| DOIs | |
| Publication status | Published - 1999 Jan 1 |
| Event | 1999 IEEE Region 10 Conference, TENCON 1999 - Cheju Island, Korea, Republic of Duration: 1999 Sep 15 → 1999 Sep 17 |
Other
| Other | 1999 IEEE Region 10 Conference, TENCON 1999 |
|---|---|
| Country | Korea, Republic of |
| City | Cheju Island |
| Period | 99/9/15 → 99/9/17 |
Fingerprint
ASJC Scopus subject areas
- Computer Science Applications
- Electrical and Electronic Engineering
Cite this
Formal verification of RACE protocol using SSM. / Kim, Hahnseng; Choi, Jin Young; Ki, Ando; Han, Woo Jong.
IEEE Region 10 Annual International Conference, Proceedings/TENCON. Vol. 2 Institute of Electrical and Electronics Engineers Inc., 1999. p. 1083-1086.Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
}
TY - GEN
T1 - Formal verification of RACE protocol using SSM
AU - Kim, Hahnseng
AU - Choi, Jin Young
AU - Ki, Ando
AU - Han, Woo Jong
PY - 1999/1/1
Y1 - 1999/1/1
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=1642303559&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=1642303559&partnerID=8YFLogxK
U2 - 10.1109/TENCON.1999.818611
DO - 10.1109/TENCON.1999.818611
M3 - Conference contribution
VL - 2
SP - 1083
EP - 1086
BT - IEEE Region 10 Annual International Conference, Proceedings/TENCON
PB - Institute of Electrical and Electronics Engineers Inc.
ER -