Formal verification of RACE protocol using SSM

Hahnseng Kim; Jin Young Choi; Ando Ki; Woo Jong Han

doi:10.1109/TENCON.1999.818611

Formal verification of RACE protocol using SSM

Hahnseng Kim, Jin Young Choi, Ando Ki, Woo Jong Han

Graduate School of Information Study

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

2 Citations (Scopus)

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
ISBN (Electronic)	0780357396, 9780780357396
DOIs	https://doi.org/10.1109/TENCON.1999.818611
Publication status	Published - 1999
Event	1999 IEEE Region 10 Conference, TENCON 1999 - Cheju Island, Korea, Republic of Duration: 1999 Sep 15 → 1999 Sep 17

Publication series

Name	IEEE Region 10 Annual International Conference, Proceedings/TENCON
Volume	2
ISSN (Print)	2159-3442
ISSN (Electronic)	2159-3450

Other

Other	1999 IEEE Region 10 Conference, TENCON 1999
Country	Korea, Republic of
City	Cheju Island
Period	99/9/15 → 99/9/17

ASJC Scopus subject areas

Computer Science Applications
Electrical and Electronic Engineering

Access to Document

10.1109/TENCON.1999.818611

Fingerprint Dive into the research topics of 'Formal verification of RACE protocol using SSM'. Together they form a unique fingerprint.

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. Institute of Electrical and Electronics Engineers Inc., 1999. p. 1083-1086 (IEEE Region 10 Annual International Conference, Proceedings/TENCON; Vol. 2).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Kim, H, Choi, JY, Ki, A & Han, WJ 1999, Formal verification of RACE protocol using SSM. in IEEE Region 10 Annual International Conference, Proceedings/TENCON. IEEE Region 10 Annual International Conference, Proceedings/TENCON, vol. 2, Institute of Electrical and Electronics Engineers Inc., pp. 1083-1086, 1999 IEEE Region 10 Conference, TENCON 1999, Cheju Island, Korea, Republic of, 99/9/15. https://doi.org/10.1109/TENCON.1999.818611

@inproceedings{73a3b8777d0c4e1d8ffc385a743b796b,

title = "Formal verification of RACE protocol using SSM",

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.",

author = "Hahnseng Kim and Choi, {Jin Young} and Ando Ki and Han, {Woo Jong}",

note = "Funding Information: 'This work was supported by Electronics and Telecommunication Research Institute under Contract No. 98241.; 1999 IEEE Region 10 Conference, TENCON 1999 ; Conference date: 15-09-1999 Through 17-09-1999",

year = "1999",

doi = "10.1109/TENCON.1999.818611",

language = "English",

series = "IEEE Region 10 Annual International Conference, Proceedings/TENCON",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

pages = "1083--1086",

booktitle = "IEEE Region 10 Annual International Conference, Proceedings/TENCON",

}

TY - GEN

T1 - Formal verification of RACE protocol using SSM

AU - Kim, Hahnseng

AU - Choi, Jin Young

AU - Ki, Ando

AU - Han, Woo Jong

N1 - Funding Information: 'This work was supported by Electronics and Telecommunication Research Institute under Contract No. 98241.

PY - 1999

Y1 - 1999

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

AN - SCOPUS:1642303559

T3 - IEEE Region 10 Annual International Conference, Proceedings/TENCON

SP - 1083

EP - 1086

BT - IEEE Region 10 Annual International Conference, Proceedings/TENCON

PB - Institute of Electrical and Electronics Engineers Inc.

T2 - 1999 IEEE Region 10 Conference, TENCON 1999

Y2 - 15 September 1999 through 17 September 1999

ER -