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(n(5)), 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(n(4)) 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(n(3)) time complexity. We also experimentally show that the new algorithm is significantly faster than Roy's algorithm.