Robustness against Relaxed Memory Models (R2M2)
Computer Architecture, Embedded and Massively Parallel Systems
Final Report Abstract
We studied the problem of checking whether a program is robust against execution on a relaxed memory model. A program is robust if for every computation on the relaxed memory model there is an equivalent sequentially consistent computation. Our first contribution is a proof method for deriving decidability and complexity results about robustness. It is a combination of combinatorial reasoning and automata-theoretic techniques. Our second result is an application of the proof method to architectures as complex as PGAS and Power. For both architectures, we proved the robustness problem to only be PSpace-complete. This came as a surprise as the reachability problem is not even decidable under Power. Given the versatility of the proof method, we suggest the following rule of thumb. Robustness tends to be PSpace-complete. It is Sequential Consistency that dominates the complexity, not the relaxed memory model. The above results satisfy the criteria for success of the project that were stated in the proposal. In an additional line of work, we observed that the robustness problem can be used as an oracle in a TSO-reachability analysis. Interestingly, despite being restricted to robustness-violating computations, the analysis is complete for bug hunting. We decided to adapt the work package on concurrency libraries. The original plan was to consider robustness for parameterized programs. Instead, we addressed the static analysis of lock-free data structures under explicit memory management. The main finding and the biggest surprise of the project was that the combinatorial reasoning mechanisms developed for relaxed memory models carry over to this setting. In particular, we developed a notion of pointer race freedom and proved the following theorem. If the program of interest is pointer race free under garbage collection, then it is sound to conduct the overall analysis under garbage collection. This line of research ultimately led to an approach that decouples the verification of a lock-free data structure from the verification of its memory reclamation. We added a work package on memory model-aware verification, verification algorithms that do not hardcode the semantics of a program but expect a memory model as part of the input. Given the generality of the problem, we limited the analysis to bounded model checking. The main findings are compact SMT encodings for fixed-point computations. Fixed points occur frequently in more complex memory models (like Power). We developed five tools some of which mature enough to be usable outside academia: Trencher-rob checks robustness against TSO, Trencher-reach is a TSO-reachability checker, TMRexp is a static analysis for lock-free data structures under explicit memory management that scales to industry-grade implementations, Porthos is a memory model-aware bounded model checker for portability among architectures, Dartagnan is a memory model-aware bounded model checker for reachability.
Publications
- A theory of partitioned global address spaces, in FSTTCS, ser. LIPIcs, vol. 24, Schloss Dagstuhl, 2013, pp. 127–139
G. Călin, E. Derevenetc, R. Majumdar, and R. Meyer
(See online at https://doi.org/10.4230/LIPIcs.FSTTCS.2013.127) - Robustness against Power is PSpace-complete, in ICALP, ser. LNCS, vol. 8573, Springer, 2014, pp. 158–170
E. Derevenetc and R. Meyer
(See online at https://doi.org/10.1007/978-3-662-43951-7_14) - Lazy TSO reachability, in FASE, ser. LNCS, vol. 9033, Springer, 2015, pp. 267–282
A. Bouajjani, G. Călin, E. Derevenetc, and R. Meyer
(See online at https://doi.org/10.1007/978-3-662-46675-9_18) - Memory model-aware testing: a unified complexity analysis, ACM TECS, vol. 14, no. 4, 63:1–63:25, 2015
F. Furbach, R. Meyer, K. Schneider, and M. Senftleben
(See online at https://doi.org/10.1109/ACSD.2014.27) - Pointer race freedom, in VMCAI, ser. LNCS, vol. 9583, Springer, 2016, pp. 393–412
F. Haziza, L. Holík, R. Meyer, and S. Wolff
(See online at https://doi.org/10.1007/978-3-662-49122-5_19) - Effect summaries for thread-modular analysis — sound analysis despite an unsound heuristic, in SAS, ser. LNCS, vol. 10422, Springer, 2017, pp. 169–191
L. Holík, R. Meyer, T. Vojnar, and S. Wolff
(See online at https://doi.org/10.1007/978-3-319-66706-5_9)
