Fast complete memory consistency verification

The verification of an execution against memory consistency is known to be NP-hard. This paper proposes a novel fast memory consistency verification method by identifying a new natural partial order: time order. In multiprocessor systems with store atomicity, a time order restriction exists between two operations whose pending periods are disjoint: the former operation in time order must be observed by the latter operation. Based on the time order restriction, memory consistency verification is localized: for any operation, both inferring related orders and checking related cycles need to take into account only a bounded number of operations. Our method has been implemented in a memory consistency verification tool for CMP (Chip Multi Processor), named LCHECK. The time complexity of the algorithm in LCHECK is O(Cp p2 n2 ) (where C is a constant, p is the number of processors and n is the number of operations) for soundly and completely checking, and O(p3 n) for soundly but incompletel...

• Type: Conference
• Year: 2009
• Where: HPCA
• Authors: Yunji Chen, Yi Lv, Weiwu Hu, Tianshi Chen, Haihua Shen, Pengyu Wang, Hong Pan
• Keywords: Computer Architecture, Consistency Verification Method, Consistency Verification Tool, HPCA 2009, Memory Consistency Verification