Robustheit gegenüber schwachen Speichermodellen
Rechnerarchitektur, eingebettete und massiv parallele Systeme
Zusammenfassung der Projektergebnisse
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.
Projektbezogene Publikationen (Auswahl)
- 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
(Siehe online unter 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
(Siehe online unter 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
(Siehe online unter 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
(Siehe online unter 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
(Siehe online unter 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
(Siehe online unter https://doi.org/10.1007/978-3-319-66706-5_9)
