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.