Sie befinden Sich nicht im Netzwerk der Universität Paderborn. Der Zugriff auf elektronische Ressourcen ist gegebenenfalls nur via VPN oder Shibboleth (DFN-AAI) möglich.
mehr Informationen...
Verifying concurrent programs under weak memory models : = Verifikation nebenläufiger Programme unter schwachen Speichermodellen
Ort / Verlag
Paderborn
Erscheinungsjahr
2017
Verknüpfte Titel
Beschreibungen/Notizen
Tag der Verteidigung: 27.11.2017
ger: Moderne Multicore Prozessoren haben schwache Speichermodelle. Diese Speichermodelle sortieren scheinbar Programm-Operationen um. Damit weichen sie von der üblicherweise angenommenen Sequenziellen Konsistenz (SC) ab. Bei der Verifikation nebenläufiger Programme müssen schwache Semantiken berücksichtigt werden. Linearisierbarkeit, ein de-facto Standard Korrektheitskriterium für nebenläufige Datenstrukturen, wurde unter der Annahme von SC definiert und seine Bedeutung unter schwachen Speichermodellen blieb lange unklar. Erst kürzlich wurden neue Varianten vorgeschlagen. Wir präsentieren einen Verifikationsansatz für nebenläufige Programme unter den schwachen Speichermodellen TSO und PSO. Der Ansatz basiert auf einer Reduktion von nebenläufigen Programmen unter TSO (resp. PSO) auf SC Programme und ermöglicht den Einsatz von Standart-SC-Verifikations-Tools. Die Reduktion erfolgt in zwei Schritten: Eine symbolische Exploration, die zu einer Repräsentation des Programmverhaltens unter TSO (resp. PSO) als Store Buffer Graph führt. Letzterer wird anschließend in ein neues SC Programm transformiert. Wir beweisen, dass beide Programme verhaltensäquivalent sind (Bisimulation). Unser Tool Weak2SC implementiert den Ansatz. Außerdem evaluieren wir den Reduktionsansatz, indem wir ihn gegen üblichere (explizite) Modelle schwacher Speichersemantiken vergleichen. Wir nehmen existierende Verifikationsansätze für Linearisierbarkeit unter SC und adaptieren diese für schwache Speichermodelle. Wir wenden diese Ansätze auf eine Menge typischer nebenläufiger Datenstrukturen an und erhalten vielversprechende Resultate. Außerdem diskutieren wir, wie die verwendeten Verifikationsverfahren mit den neuen Formalisierungen von Linearisierbarkeit unter schwachen Speichermodellen zusammenhängen.
eng: Modern multicore processors provide weak memory models. These memory models seemingly reorder program operations. Thus, they deviate from the commonly assumed sequential consistency (SC) semantics. Verification techniques for concurrent programs consequently need to take these weak semantics into account. Linearizability, a de-facto standard correctness condition for concurrent data structures, has been defined under assumption of SC and its meaning under weak memory models was uncertain for years. Just recently, new adaptations were proposed. We present a verification approach for concurrent programs under the weak memory models TSO and PSO. The approach is based on a reduction of concurrent programs under TSO (resp. PSO) to an SC program enabling many standard SC verification tools. The reduction involves two steps: a symbolic exploration, which results in a representation of the program behavior under TSO (resp. PSO) as a store buffer graph. The latter is then transformed into a new SC program. We prove both programs to be behaviorally equivalent (bisimulation). Our tool Weak2SC implements the presented approach. Furthermore, we evaluate our reduction approach by comparing it against more common explicit models of weak memory semantics. We take existing approaches for verification of linearizability under SC and adapt them for weak memory models. We apply these approaches to a set of typical concurrent data structures and achieve promising results in terms of performance (resp. proof effort). In addition, we also discuss how the adapted verification approaches relate to the new formalizations of linearizability under weak memory models.