Publication Details

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

HOLÍK Lukáš, MEYER Roland, VOJNAR Tomáš and WOLF Sebastian. Effect Summaries for Thread-Modular Analysis. In: SAS 2017: Static Analysis. Lecture Notes in Computer Science, vol. 10422. Cham: Springer International Publishing, 2017, pp. 169-191. ISBN 978-3-319-66706-5. ISSN 0302-9743. Available from: https://link.springer.com/chapter/10.1007%2F978-3-319-66706-5_9
Czech title
Souhrny efektů pro vláknově modulární analýzu
Type
conference paper
Language
english
Authors
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Meyer Roland (UNIKL)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
Wolf Sebastian (UNIKL)
URL
Keywords

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

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.

Published
2017
Pages
169-191
Journal
Lecture Notes in Computer Science, vol. 10422, no. 1, ISSN 0302-9743
Proceedings
SAS 2017: Static Analysis
Series
Lecture Notes in Computer Science
Conference
24th International Static Analysis Symposium, New York City, US
ISBN
978-3-319-66706-5
Publisher
Springer International Publishing
Place
Cham, DE
DOI
UT WoS
000455332000009
EID Scopus
BibTeX
@INPROCEEDINGS{FITPUB11563,
   author = "Luk\'{a}\v{s} Hol\'{i}k and Roland Meyer and Tom\'{a}\v{s} Vojnar and Sebastian Wolf",
   title = "Effect Summaries for Thread-Modular Analysis Sound Analysis Despite an Unsound Heuristic",
   pages = "169--191",
   booktitle = "SAS 2017: Static Analysis",
   series = "Lecture Notes in Computer Science",
   journal = "Lecture Notes in Computer Science",
   volume = 10422,
   number = 1,
   year = 2017,
   location = "Cham, DE",
   publisher = "Springer International Publishing",
   ISBN = "978-3-319-66706-5",
   ISSN = "0302-9743",
   doi = "10.1007/978-3-319-66706-5\_9",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/11563"
}
Back to top