Implied Set Closure and Its Application to Memory Consistency Verification

Hangal et. al. [3] have developed a procedure to check if an instance of the execution of a shared memory multiprocessor program, is consistent with the Total Store Order (TSO) memory consistency model. They also devised an algorithm based on this procedure with time complexity O(n5 ), where n is the total number of instructions in the program. Roy et. al. [6] have improved the implementation of the procedure and achieved O(n4 ) time complexity. We have identified the bottleneck in these algorithms as a graph problem of independent interest, called implied-set closure (ISC) problem. In this paper we propose an algorithm for ISC problem and show that using this algorithm, Hangal's consistency checking procedure can be implemented with O(n3 ) time complexity. We also experimentally show that the new algorithm is significantly faster than Roy's algorithm. Keywords Memory consistency model verification, Incremental transitive closure, Total store order, Shared memory multi-proces...

• Type: Conference
• Year: 2008
• Where: CAV
• Authors: Surender Baswana, Shashank K. Mehta, Vishal Powar
• Keywords: CAV 2008, Hardware, Memory Consistency Model, Time Complexity, Total Store Order