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
    ISBN (Electronic)0780357396, 9780780357396
    DOIs
    Publication statusPublished - 1999
    Event1999 IEEE Region 10 Conference, TENCON 1999 - Cheju Island, Korea, Republic of
    Duration: 1999 Sept 151999 Sept 17

    Publication series

    NameIEEE Region 10 Annual International Conference, Proceedings/TENCON
    Volume2
    ISSN (Print)2159-3442
    ISSN (Electronic)2159-3450

    Other

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

    Bibliographical note

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

    ASJC Scopus subject areas

    • Computer Science Applications
    • Electrical and Electronic Engineering

    Fingerprint

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

    Cite this