Formal verification of RACE protocol using SSM

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

Research output: Chapter in Book/Report/Conference proceedingConference 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 languageEnglish
Title of host publicationIEEE Region 10 Annual International Conference, Proceedings/TENCON
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages1083-1086
Number of pages4
Volume2
ISBN (Electronic)0780357396, 9780780357396
DOIs
Publication statusPublished - 1999 Jan 1
Event1999 IEEE Region 10 Conference, TENCON 1999 - Cheju Island, Korea, Republic of
Duration: 1999 Sep 151999 Sep 17

Other

Other1999 IEEE Region 10 Conference, TENCON 1999
CountryKorea, Republic of
CityCheju Island
Period99/9/1599/9/17

Fingerprint

Network protocols
Data storage equipment
Computer systems
Explosions
Formal verification
Testing

ASJC Scopus subject areas

  • Computer Science Applications
  • Electrical and Electronic Engineering

Cite this

Kim, H., Choi, J. Y., Ki, A., & Han, W. J. (1999). Formal verification of RACE protocol using SSM. In IEEE Region 10 Annual International Conference, Proceedings/TENCON (Vol. 2, pp. 1083-1086). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/TENCON.1999.818611

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 proceedingConference 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. 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
Kim H, Choi JY, Ki A, Han WJ. Formal verification of RACE protocol using SSM. In IEEE Region 10 Annual International Conference, Proceedings/TENCON. Vol. 2. Institute of Electrical and Electronics Engineers Inc. 1999. p. 1083-1086 https://doi.org/10.1109/TENCON.1999.818611
Kim, Hahnseng ; Choi, Jin Young ; Ki, Ando ; Han, Woo Jong. / Formal verification of RACE protocol using SSM. IEEE Region 10 Annual International Conference, Proceedings/TENCON. Vol. 2 Institute of Electrical and Electronics Engineers Inc., 1999. pp. 1083-1086
@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}",
year = "1999",
month = "1",
day = "1",
doi = "10.1109/TENCON.1999.818611",
language = "English",
volume = "2",
pages = "1083--1086",
booktitle = "IEEE Region 10 Annual International Conference, Proceedings/TENCON",
publisher = "Institute of Electrical and Electronics Engineers Inc.",

}

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

AN - SCOPUS:1642303559

VL - 2

SP - 1083

EP - 1086

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

PB - Institute of Electrical and Electronics Engineers Inc.

ER -