##
**Effective abstractions for verification under relaxed memory models.**
*(English)*
Zbl 1432.68259

D’Souza, Deepak (ed.) et al., Verification, model checking, and abstract interpretation. 16th international conference, VMCAI 2015, Mumbai, India, January 12–14, 2015. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8931, 449-466 (2015).

Summary: We present a new abstract interpretation based approach for automatically verifying concurrent programs running on relaxed memory models.

Our approach is based on three key insights: (i) behaviors of relaxed models (e.g. TSO and PSO) are naturally captured using explicit encodings of store buffers. Directly using such encodings for program analysis is challenging due to shift operations on buffer contents that result in significant loss of analysis precision. We present a new abstraction of the memory model that eliminates expensive shifting of store buffer contents and significantly improves the precision and scalability of program analysis, (ii) an encoding of store buffer sizes that leverages knowledge of the abstract interpretation domain, further improving analysis precision, and (iii) a source-to-source transformation that realizes the above two techniques: given a program \(P\) and a relaxed memory model \(M\), it produces a new program \(P _{M }\) where the behaviors of \(P\) running on \(M\) are over-approximated by the behavior of \(P _{M }\) running on sequential consistency (SC). This step makes it possible to directly use state-of-the-art analyzers under SC.

We implemented our approach and evaluated it on a set of finite and infinite-state concurrent algorithms under two memory models: Intel’s x86 TSO and PSO. Experimental results indicate that our technique achieves better precision and efficiency than prior work: we can automatically verify algorithms with fewer fences, faster and with lower memory consumption.

For the entire collection see [Zbl 1303.68013].

Our approach is based on three key insights: (i) behaviors of relaxed models (e.g. TSO and PSO) are naturally captured using explicit encodings of store buffers. Directly using such encodings for program analysis is challenging due to shift operations on buffer contents that result in significant loss of analysis precision. We present a new abstraction of the memory model that eliminates expensive shifting of store buffer contents and significantly improves the precision and scalability of program analysis, (ii) an encoding of store buffer sizes that leverages knowledge of the abstract interpretation domain, further improving analysis precision, and (iii) a source-to-source transformation that realizes the above two techniques: given a program \(P\) and a relaxed memory model \(M\), it produces a new program \(P _{M }\) where the behaviors of \(P\) running on \(M\) are over-approximated by the behavior of \(P _{M }\) running on sequential consistency (SC). This step makes it possible to directly use state-of-the-art analyzers under SC.

We implemented our approach and evaluated it on a set of finite and infinite-state concurrent algorithms under two memory models: Intel’s x86 TSO and PSO. Experimental results indicate that our technique achieves better precision and efficiency than prior work: we can automatically verify algorithms with fewer fences, faster and with lower memory consumption.

For the entire collection see [Zbl 1303.68013].

### MSC:

68Q60 | Specification and verification (program logics, model checking, etc.) |

68M07 | Mathematical problems of computer architecture |

68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |

68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |