Memory Model-aware Testing - a Unified Complexity Analysis
We develop memory model-aware testing algorithms for concurrent programs. For the purpose of testing, a concurrent program is given as a set of sequences of operations, one for each process. The task is to check whether these operations can be interleaved to an execution of the full program that is valid under the memory model of interest. Our contribution is a unified complexity analysis of testing. Rather than solving the testing problem for single memory models, we propose three concepts that allow us to settle the complexity for all memory models in an extended Steinke-Nutt hierarchy, which includes prominent models like SC, TSO, PRAM, SLOW, and LOCAL consistency. (i) We show that testing is in NP by reduction to Boolean satisfiability. Interestingly, a single SAT encoding works for all models in the Steinke-Nutt hierarchy. It phrases validity of a test uniformly as the ability to serialize partial orders, and only the choice of the partial orders depends on the memory model. (ii) For the stronger memory models, we establish matching lower bounds. To again achieve a uniform treatment, we extend the concept of reductions from complexity theory in order to propagate hardness results between memory models. (iii) For the remaining and weaker models, we show polynomial-time testing algorithms. We stress that our results are not only of theoretical interest, but immediately lead to practical testing methods for assembly code that are provably optimal.
by Florian Furbach, Roland Meyer, Klaus Schneider, and Maximilian Senftleben