TY  - THES
AB  - 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.
AU  - Travkin, Oleg
CY  - Paderborn
DA  - 2017
DO  - 10.17619/UNIPB/1-247
DP  - Universität Paderborn
LA  - eng
N1  - Tag der Verteidigung: 27.11.2017
N1  - Universität Paderborn, Dissertation, 2017
PB  - Veröffentlichungen der Universität
PY  - 2017
SP  - 1 Online-Ressource (xv, 217 Seiten)
T2  - Institut für Informatik
TI  - Verifying concurrent programs under weak memory models
UR  - https://nbn-resolving.org/urn:nbn:de:hbz:466:2-29964
Y2  - 2026-01-18T16:41:27
ER  -