7 citations · 12 across the 4 of their papers we have counts for
4 papers · 1 filter
Pointer Life Cycle Types for Lock-Free Data Structures with Memory Reclamation
Roland Meyer, Sebastian Wolff
We consider the verification of lock-free data structures that manually manage their memory with the help of a safe memory reclamation (SMR) algorithm. Our first contribution is a…
Decoupling Lock-Free Data Structures from Memory Reclamation for Static Analysis
Roland Meyer, Sebastian Wolff
Verification of concurrent data structures is one of the most challenging tasks in software verification. The topic has received considerable attention over the course of the last…
Effect Summaries for Thread-Modular Analysis
Lukáš Holík, Roland Meyer, Tomáš Vojnar +1
We propose a novel guess-and-check principle to increase the efficiency of thread-modular verification of lock-free data structures. We build on a heuristic that guesses candidates…
Checking Robustness against TSO
Ahmed Bouajjani, Egor Derevenetc, Roland Meyer
We present algorithms for checking and enforcing robustness of concurrent programs against the Total Store Ordering (TSO) memory model. A program is robust if all its TSO computati…