An Efficient Verification Method of Cache CoherenceProtocol Based on Pseudo-cutoff
DOI:
Author:
Affiliation:

Clc Number:

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    Abstract:

    Regarding the state space explosion problem in model checking Cache coherence protocol, the concept of pseudo-cutoff, a limit of the nodes which share the same memory block, is put forward in this paper. Based on the analysis of the inherent characteristics of parallel programs, the pseudo-cutoff value in relaxed consistency Cache coherent non-uniform memory access system under certain conditions is deduced. The state space of the directory-based Cache protocol is optimized effectively using pseudo-cutoff, and a new scheme to small probability matter of wide sharing is presented. Experimental results show that, the method of protocol model optimization based on pseudo-cutoff can effectively reduce the state space of Cache protocol, accelerate verification speed and improve the capability of verifying large scale Cache protocol.

    Reference
    Related
    Cited by
Get Citation
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:August 26,2008
  • Revised:
  • Adopted:
  • Online: December 07,2012
  • Published:
Article QR Code