Formal Verification of RACE Protocol Using VIS


The Transactions of the Korea Information Processing Society (1994 ~ 2000), Vol. 7, No. 7, pp. 2219-2228, Jul. 2000
10.3745/KIPSTE.2000.7.7.2219,   PDF Download:

Abstract

Caches in a multiprocessing environment introduce the cache coherence problem. When multiple processors maintain locally cached copies of a unique shared-memory location, any local modification of the location can result in a globally inconsistent view of memory. Cache coherence protocols are important to operate a shared-memory multiprocessor system with efficiency and correctness. Since random testing and simulations are not enough to validate correctness of protocols, it is necessary to develop efficient and reliable verification methods. In this paper we present our experience in using VIS (Verification Interacting with Synthesis), a tool of formal method, to analyze a number of property of a cache coherence protocol, RACE (Remote Access Cache coherent Enforcement).


Statistics
Show / Hide Statistics

Statistics (Cumulative Counts from September 1st, 2017)
Multiple requests among the same browser session are counted as one view.
If you mouse over a chart, the values of data points will be shown.


Cite this article
[IEEE Style]
H. S. Um, J. Y. Choi, W. J. Han, A. D. Ki, K. H. Shim, "Formal Verification of RACE Protocol Using VIS," The Transactions of the Korea Information Processing Society (1994 ~ 2000), vol. 7, no. 7, pp. 2219-2228, 2000. DOI: 10.3745/KIPSTE.2000.7.7.2219.

[ACM Style]
Hyun Sun Um, Jin Young Choi, Woo Jong Han, An Do Ki, and Kyu Hyun Shim. 2000. Formal Verification of RACE Protocol Using VIS. The Transactions of the Korea Information Processing Society (1994 ~ 2000), 7, 7, (2000), 2219-2228. DOI: 10.3745/KIPSTE.2000.7.7.2219.