Publication result detail

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

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

Original Title

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

English Title

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

Type

Paper in proceedings (conference paper)

Original Abstract

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.

English abstract

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.

Keywords

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

Key words in English

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

Authors

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

RIV year

2018

Released

30.08.2017

Publisher

Springer International Publishing

Location

Cham

ISBN

978-3-319-66706-5

Book

SAS 2017: Static Analysis

Edition

Lecture Notes in Computer Science

ISBN

0302-9743

Periodical

Lecture Notes in Computer Science

Volume

10422

Number

1

State

Federal Republic of Germany

Pages from

169

Pages to

191

Pages count

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"
}

Documents

hmvw-sas-17