Sound and Complete Monitoring of Sequential Consistency for Relaxed Memory Models
Source: University of California
The authors present a technique for verifying that a program has no executions violating Sequential Consistency (SC) when run under the relaxed memory models Total Store Order (TSO) and Partial Store Order (PSO). The technique works by monitoring sequentially consistent executions of a program to detect if similar program executions could fail to be sequentially consistent under TSO or PSO. They propose novel monitoring algorithms that are sound and complete for TSO and PSO - if a program can exhibit an SC violation under TSO or PSO, then the corresponding monitor can detect this on some SC execution.