de
en
Schliessen
Detailsuche
Bibliotheken
Projekt
Impressum
Datenschutz
Schliessen
Publizieren
Besondere Sammlungen
Digitalisierungsservice
Hilfe
Impressum
Datenschutz
zum Inhalt
Detailsuche
Schnellsuche:
OK
Ergebnisliste
Titel
Titel
Inhalt
Inhalt
Seite
Seite
Im Werk suchen
Verifying concurrent programs under weak memory models / vorgelegt von Oleg Travkin, M.Sc. Paderborn, 2017
Inhalt
Introduction
Concurrency on Modern Multicore Processors
Weak Memory Models
Towards Program Correctness
Contributions
Overview
Memory Models
Programs
Parameterized Semantics
Sequential Consistency
Total Store Order
Partial Store Order
Relaxed Memory Order
Related Work
Reduction from Weak Semantics to Sequential Consistency
Symbolic Execution with Weak Memory Semantics
Store Buffer Graph
Store Buffer Graphs Properties
Transformation to a new SC Program
Reduction is Sound and Compositional
Local Bisimulation Equivalence
Compositionality of the Approach
Related Work and Discussion
Weak2SC – The Implementation
Architecture of Weak2SC
Case Study – Work Stealing Queue
From LLVM IR to a Store Buffer Graph
Template-based Generation of new Programs
Generating Promela Programs
Generating KIV Program Encoding
Promela Programs for Operational Memory Models
Discussion and Possible Future Extensions
Correctness of Concurrent Data Structures
Linearizability
Linearizability - Original Definition
Adaptations to Weak Memory Models
Discussion
Verification Methods for Linearizability
Other Correctness Conditions
Verifying Linearizability under Weak Memory Models
Model Checking under Weak Memory Models
The Idea - Abstract Atomic Specifications
Experiments
An alternative Idea - History Checking
Proving Linearizability under Weak Memory Models
Overview
Abstract Data Type
Concrete Data Type
Abstraction Function
Invariant
Proof Procedure and Comparison
Related Work and Discussion
Conclusion
Summary
Future Work
Design Decisions
Concluding Thoughts
Proofs
Behavioral Equivalence
Compositionality
Code Examples
Bibliography
Die detaillierte Suchanfrage erfordert aktiviertes Javascript.