Completely verifying memory consistency of test program executions

12 years 5 months ago
Completely verifying memory consistency of test program executions
An important means of validating the design of commercial-grade shared memory multiprocessors is to run a large number of pseudo-random test programs on them. However, when intentional data races are placed in a test program, there may be many correct results according to the memory consistency model supported by the system. For popular memory models like SC and TSO, the problem of verifying correctness of an execution is known to be NP-complete. As a result, analysis techniques implemented in the past have been incomplete: violations of the memory model are flagged if provable, otherwise the result is inconclusive and it is assumed optimistically that the machine's results are correct. In this paper, we describe for the first time a practical, new algorithm which can solve this problem with certainty, thus ensuring that incorrect behavior of a large, complex multiprocessor cannot escape. We present results of our analysis algorithm on test programs run on a newly designed multip...
Chaiyasit Manovit, Sudheendra Hangal
Added 01 Dec 2009
Updated 01 Dec 2009
Type Conference
Year 2006
Where HPCA
Authors Chaiyasit Manovit, Sudheendra Hangal
Comments (0)