Detail publikačního výsledku

Effect Summaries for Thread-Modular Analysis Sound Analysis Despite an Unsound Heuristic

HOLÍK, L.; MEYER, R.; VOJNAR, T.; WOLF, S.

Originální název

Effect Summaries for Thread-Modular Analysis Sound Analysis Despite an Unsound Heuristic

Anglický název

Effect Summaries for Thread-Modular Analysis Sound Analysis Despite an Unsound Heuristic

Druh

Stať ve sborníku v databázi WoS či Scopus

Originální abstrakt

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 for stateless effect summaries of programs by searching the code for instances of a copy-and-check programming idiom common in lock-free data structures. These candidate summaries are used to compute the interference among threads in linear time. Since a candidate summary need not be a sound effect summary, we show how to fully automatically check whether the precision of candidate summaries is sufficient. We can thus perform sound verification despite relying on an unsound heuristic. We have implemented our approach and found it up to two orders of magnitude faster than existing ones.

Anglický abstrakt

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 for stateless effect summaries of programs by searching the code for instances of a copy-and-check programming idiom common in lock-free data structures. These candidate summaries are used to compute the interference among threads in linear time. Since a candidate summary need not be a sound effect summary, we show how to fully automatically check whether the precision of candidate summaries is sufficient. We can thus perform sound verification despite relying on an unsound heuristic. We have implemented our approach and found it up to two orders of magnitude faster than existing ones.

Klíčová slova

Concurrent programs, thread-modular reasoning, effect summary, unbounded concurrency, dynamic lockless data structures.

Klíčová slova v angličtině

Concurrent programs, thread-modular reasoning, effect summary, unbounded concurrency, dynamic lockless data structures.

Autoři

HOLÍK, L.; MEYER, R.; VOJNAR, T.; WOLF, S.

Rok RIV

2018

Vydáno

30.08.2017

Nakladatel

Springer International Publishing

Místo

Cham

ISBN

978-3-319-66706-5

Kniha

SAS 2017: Static Analysis

Edice

Lecture Notes in Computer Science

ISSN

0302-9743

Periodikum

Lecture Notes in Computer Science

Svazek

10422

Číslo

1

Stát

Spolková republika Německo

Strany od

169

Strany do

191

Strany počet

23

URL

https://link.springer.com/chapter/10.1007%2F978-3-319-66706-5_9

BibTex

@inproceedings{BUT146270,
  author="Lukáš {Holík} and Roland {Meyer} and Tomáš {Vojnar} and Sebastian {Wolf}",
  title="Effect Summaries for Thread-Modular Analysis Sound Analysis Despite an Unsound Heuristic",
  booktitle="SAS 2017: Static Analysis",
  year="2017",
  series="Lecture Notes in Computer Science",
  journal="Lecture Notes in Computer Science",
  volume="10422",
  number="1",
  pages="169--191",
  publisher="Springer International Publishing",
  address="Cham",
  doi="10.1007/978-3-319-66706-5\{_}9",
  isbn="978-3-319-66706-5",
  issn="0302-9743",
  url="https://link.springer.com/chapter/10.1007%2F978-3-319-66706-5_9"
}

Dokumenty

hmvw-sas-17