Effect Summaries for Thread-Modular Analysis

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F17%3APU127284" target="_blank" >RIV/00216305:26230/17:PU127284 - isvavai.cz</a>

Výsledek na webu

<a href="https://link.springer.com/chapter/10.1007%2F978-3-319-66706-5_9" target="_blank" >https://link.springer.com/chapter/10.1007%2F978-3-319-66706-5_9</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-319-66706-5_9" target="_blank" >10.1007/978-3-319-66706-5_9</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Effect Summaries for Thread-Modular Analysis

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Effect Summaries for Thread-Modular Analysis

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2017

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

SAS 2017: Static Analysis

ISBN

978-3-319-66706-5

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

23

Strana od-do

169-191

Název nakladatele

Springer International Publishing

Místo vydání

Cham

Místo konání akce

New York City

Datum konání akce

30. 8. 2017

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000455332000009