Verifying optimizations of concurrent programs in the promising semantics
Junpeng Zha, Hongjin Liang, Xinyu Feng · 2022
Weak memory models for concurrent programming languages are expected to admit standard compiler optimizations. However, prior works on verifying optimizations in weak memory models are mostly focused on simple optimizations on small code snippets which satisfy certain syntactic requirements. It receives less attention whether weak memory models can admit real-world optimization algorithms based on program analyses.