微信服务号

微信订阅号

2025-5-11- 17
Home > Archive>Volume 21, Issue 4, 2010 >863-874
PDF HTML XML Export Cite reminder
Memory Consistency Verification of Chip Multi-Processor
Author:
Affiliation:

  • Article
    • | |
  • Metrics
    • |
  • Reference [21]
    • |
  • Related [20]
    • |
  • Cited by [2]
    • | |
  • Comments
    Abstract:

    Memory consistency verification is an important part of functional validation of CMP (chip multi- processor). Since checking an execution of a parallel program against a memory consistency model is known to be an NP-hard problem, in practice, incomplete verification methods with higher than O(n3) time complexity are used to deal with memory consistency verification. In this paper, a linear time complexity memory consistency verification tool LCHECK is introduced. In the multi-processor system which supports store atomicity, there must be a time order between two operations with disjoint execution periods: The former operation in time order must be observed by the latter operation. LCHECK localizes memory consistency verification based on time order. It infers edges of orders and checks correctness in bounded operations. LCHECK is used in the verification of an industrial CMP, Godson-3, and finds many bugs of memory subsystem of Godson-3.

    Reference
    [1] Chatterjee P, Sivaraj H, Gopalakrishnan G. Shared memory consistency protocol verification against weak memory models: Refinement via model-checking. In: Proc. of the 14th Int’l Conf. on Computer Aided Verification (CAV 2002). 2002. http://www.cs.utah.edu/formal_verification/papers/cav02paper.pdf
    [2] Yang Y, Gopalakrishnan G, Lindstrom G, Slind K. Nemos: A framework for axiomatic and executable specifications of memory consistency models. In: Proc. of the 18th Int’l Parallel and Distributed Processing Symp. (IPDPS 2004). 2004. http://ieeexplore. ieee.org/stamp/stamp.jsp?tp=&arnumber=1302944
    [3] Gibbons P, Korach E. On testing cache-coherent shared memories. In: Proc. of the 6th ACM Symp. on Parallel Algorithms and Architectures (SPAA’94). 1994. http://delivery.acm.org/10.1145/190000/181328/p177-gibbons.pdf?key1=181328&key2=318237 8621&coll=GUIDE&dl=GUIDE&CFID=82133830&CFTOKEN=76647768
    [4] Gibbons P, Korach E. Testing shared memories. SIAM Journal on Computing, 1997,26(4):1208-1244.
    [5] Meixner A, Sorin D. Dynamic verification of sequential consistency. In: Proc. of the 32nd Int’l Symp. on Computer Architecture (ISCA 2005). 2005. http://people.ee.duke.edu/～sorin/papers/isca05_dvsc.pdf
    [6] Meixner A, Sorin D. Dynamic verification of memory consistency in cache-coherent multithreaded computer architectures. In: Proc. of the Int’l Conf. on Dependable Systems and Networks (DSN 2006). 2006. http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=& arnumber=1633497&userType=inst
    [7] Hangal S, Vahia D, Manovit C, Lu J, Narayanan S. Tsotool: A program for verifying memory systems using the memory consistency model. In: Proc. of the 31st Int’l Symp. on Computer Architecture (ISCA 2004). 2004. http://ieeexplore.ieee.org/ iel5/9170/29103/01310768.pdf?arnumber=1310768
    [8] Manovit C, Hangal S. Efficient algorithms for verifying memory consistency. In: Proc. of the 17th ACM Symp. on Parallelism in Algorithms and Architecture (SPAA 2005). 2005. http://delivery.acm.org/10.1145/1080000/1074011/p245-manovit.pdf?key1= 1074011&key2=6873378621&coll=GUIDE&dl=GUIDE&CFID=82135957&CFTOKEN=66149051
    [9] Roy A, Zeisset S, Fleckenstein C, Huang J. Fast and generalized polynomial time memory consistency verification. In: Proc. of the 18th Int’l Conf. on Computer Aided Verification (CAV 2006). Berlin, Heidelberg: Springer-Verlag, 2006. 503-516.
    [10] Manovit C, Hangal S. Completely verifying memory consistency of test program executions. In: Proc. of the 12th Int’l Symp. on High-Performance Computer Architecture (HPCA 2006). 2006. http://ieeexplore.ieee.org/iel5/10647/33614/01598123.pdf? arnumber=1598123
    [11] Scheurich C, Dubois M. Correct memory operation of cached-based multiprocessors. In: Proc. of the 14th Int’l Symp. on Computer Architecture (ISCA’87). 1987.
    [12] Goodman J. Cache consistency and sequential consistency. Technical Report, No. 61, SCI Committee, 1989.
    [13] Dubois M, Scheurich C, Briggs F. Memory access buffering in multiprocessors. In: Proc. of the 13th Int’l Symp. on Computer Architecture (ISCA’86). New York: ACM Press, 1986. 320-328.
    [14] Chen YJ, Lv Y, Hu W, Chen TS, Shen HH, Wang PY, Pan H. Fast complete memory consistency verification. In: Proc. of the 15th Int’l Symp. on High-Performance Computer Architecture (HPCA’15). Raleigh, 2009. 381-392.
    [15] Arvind, Maessen J. Memory model=instruction reordering+store atomicity. In: Proc. of the 33rd Int’l Symp. on Computer Architecture (ISCA2006). 2006. http://csg.csail.mit.edu/pubs/memos/Memo-493/memo-493.pdf
    [16] Hu W, Gao X, Chen YJ. Micro-Architecture of Godson-3 multi-core processor. In: Proc. of the 20th Hot Chips. 2008.
    [17] Hu W, Wang J, Gao X, Chen YJ, Liu Q. Godson-3: A scalable multicore—RISC processor with x86 emulation. IEEE Micro, 2009,29(2). http://filesbay.net/search/godson-3-a-scalable-multicore-risc-processor-with-x86-emulation.html
    [18] Hu W. Shared Memory Architecture. Beijing: Higher Education Press, 2007 (in Chinese).
    [19] Hu W. A graph model for investigating memory consistency. In: Proc. of the 8th Int’l Parallel and Distributed Processing Symp. (IPDPS’94). 1994. 516-523.
    [20] Lamport L. Time, clocks, and the ordering of event in a distributed system. Communications of the ACM, 1978,21(7).
    附中文参考文献: [18] 胡伟武.共享存储系统结构.北京:高等教育出版社,2001.
    Comments
    Comments
    分享到微博
    Submit
Get Citation

王朋宇,陈云霁,沈海华,陈天石,张珩.片上多核处理器存储一致性验证.软件学报,2010,21(4):863-874

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:December 10,2008
  • Revised:July 23,2009
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2043805Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063