2019/05/10 by Sanjana Singh, Singh, Sanjana, Divyanjali Sharma +3
Computer Science · Engineering · #Distributed #FOS: Computer and information sciences #Parallel #Parallel Computing and Optimization Techniques #Programming Languages (cs.PL) #Radiation Effects in Electronics #Security and Verification in Computing #and Cluster Computing (cs.DC)
paper · pdf · doi:10.48550/arxiv.1905.03957
openalex publication_date 2019/05/10 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Program executions under relaxed memory model (rmm) semantics are significantly more difficult to analyze; the rmm semantics result in out of order execution of program events leading to an explosion of state-space. Dynamic partial order reduction (DPOR) is a powerful technique to address such a state-space explosion and has been used to verify programs under rmm such as TSO, PSO, and POWER. Central to such DPOR techniques is the notion of trace-equivalence, which is computed based on the independence relation among program events. We propose a coarser notion of rmm-aware trace equivalence called observational equivalence (OE). Two program behaviors are observationally equivalent if every read event reads the same value in both the behaviors. We propose a notion of observational independence (OI) and provide an algorithmic construction to compute trace equivalence (modulo OI) efficiently. We also demonstrate the effectiveness of DPOR with OE on threaded C/C++ programs by first providing an elaborate happensbefore (hb) relation for capturing the C/C++ concurrency semantics. We implement the presented technique in a runtime model checker called Drista. Our experiments reflect that (i) when compared to existing nonOE techniques, we achieve significant savings in the number of traces explored under OE, and (ii) our treatment of C/C++ concurrency is more extensive than the existing state-of-the-art techniques.