Abstract | ||
---|---|---|
One approach in verifying the correctness of a multiprocessor system is to show that its execution results comply with the memory consistency model it is meant to implement. It has been shown in prior work, however, that accurately verifying such compliance even of a single execution result is an NP-complete problem, for an unlimited number of processors. In this paper, we present a suite of post-mortem algorithms that perform the compliance check in an efficient, although not exhaustive, manner. Our algorithms employ the concept of vector clocks together with a heuristic made from a variation of the problem in P class. An implementation of these algorithms has been successful in efficiently detecting several bugs during the course of validating the design of commercial microprocessors and systems.Although our algorithms are presented with the Total Store Order (TSO) memory model, the ideas can also be applied to other models ranging from Sequential Consistency (SC) to a more relaxed one such as Relaxed Memory Order (RMO). |
Year | DOI | Venue |
---|---|---|
2005 | 10.1145/1073970.1074011 | SPAA |
Keywords | Field | DocType |
execution result,verifying memory consistency,memory model,sequential consistency,compliance check,relaxed memory order,np-complete problem,single execution result,efficient algorithm,p class,memory consistency model,total store order,theory,vector clocks,np complete problem | Causal consistency,Local consistency,Sequential consistency,Computer science,Parallel computing,Distributed memory,Algorithm,Memory coherence,PRAM consistency,Consistency model,Distributed computing,Cache coherence | Conference |
ISBN | Citations | PageRank |
1-58113-986-1 | 17 | 0.94 |
References | Authors | |
16 | 2 |
Name | Order | Citations | PageRank |
---|---|---|---|
Chaiyasit Manovit | 1 | 114 | 6.48 |
Sudheendra Hangal | 2 | 536 | 35.73 |