%0 Journal Article
%T Memory Consistency Verification of Chip Multi-Processor<br>片上多核处理器存储一致性验证
%A WANG Peng-Yu
%A CHEN Yun-Ji
%A SHEN Hai-Hu
%A CHEN Tian-Shi
%A ZHANG Heng
%A <br>王朋宇
%A 陈云霁
%A 沈海华
%A 陈天石
%A 张珩
%J 软件学报
%D 2010
%I 
%X 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.
%K memory consistency model
%K verification
%K time order
%K chip multi-processor
%K cache coherence<br>存储一致性模型
%K 验证
%K 时间序
%K 片上多核处理器
%K 缓存一致性
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=7735F413D429542E610B3D6AC0D5EC59&aid=FFE093521FA3440D8E831F492C6F8486&yid=140ECF96957D60B2&vid=659D3B06EBF534A7&iid=E158A972A605785F&sid=AD0A5DE51C29AB9F&eid=3893EBCAC6700388&journal_id=1000-9825&journal_name=软件学报&referenced_num=0&reference_num=21