Vše

Co hledáte?

Vše
Projekty
Výsledky výzkumu
Subjekty

Rychlé hledání

  • Projekty podpořené TA ČR
  • Významné projekty
  • Projekty s nejvyšší státní podporou
  • Aktuálně běžící projekty

Chytré vyhledávání

  • Takto najdu konkrétní +slovo
  • Takto z výsledků -slovo zcela vynechám
  • “Takto můžu najít celou frázi”

Checking Just Pairs of Threads for Efficient and Scalable Incremental Verification of Multithreaded Programs

Identifikátory výsledku

  • Kód výsledku v IS VaVaI

    <a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F23%3A10447448" target="_blank" >RIV/00216208:11320/23:10447448 - isvavai.cz</a>

  • Výsledek na webu

    <a href="https://doi.org/10.1145/3573074.3573082" target="_blank" >https://doi.org/10.1145/3573074.3573082</a>

  • DOI - Digital Object Identifier

    <a href="http://dx.doi.org/10.1145/3573074.3573082" target="_blank" >10.1145/3573074.3573082</a>

Alternativní jazyky

  • Jazyk výsledku

    angličtina

  • Název v původním jazyce

    Checking Just Pairs of Threads for Efficient and Scalable Incremental Verification of Multithreaded Programs

  • Popis výsledku v původním jazyce

    Many techniques of automated verification target multithreaded programs, because subtle interactions between threads may trigger concurrency errors such as deadlocks and data races. However, techniques and tools involving systematic exploration of the whole space of possible thread interleavings do not scale to large software systems, despite various clever algorithmic optimizations. A viable approach is to use incremental verification techniques that, in each run, focus just on the recently modified code and the relatively small number of affected execution traces, and therefore can provide results (bug reports) very quickly.In this paper we present a new algorithm for incremental verification of multithreaded programs based on the pairwise approach, whose key idea is systematic exploration of all possible thread interleavings just for specific relevant pairs of threads.We implemented the algorithm with Java Pathfinder as the backend verification tool, and evaluated it on several multithreaded Java programs. Results show that our incremental algorithm (1) can find errors very fast, (2) greatly reduces time needed for complete safety verification, and (3) it can find the same errors as full verification of the whole state space.

  • Název v anglickém jazyce

    Checking Just Pairs of Threads for Efficient and Scalable Incremental Verification of Multithreaded Programs

  • Popis výsledku anglicky

    Many techniques of automated verification target multithreaded programs, because subtle interactions between threads may trigger concurrency errors such as deadlocks and data races. However, techniques and tools involving systematic exploration of the whole space of possible thread interleavings do not scale to large software systems, despite various clever algorithmic optimizations. A viable approach is to use incremental verification techniques that, in each run, focus just on the recently modified code and the relatively small number of affected execution traces, and therefore can provide results (bug reports) very quickly.In this paper we present a new algorithm for incremental verification of multithreaded programs based on the pairwise approach, whose key idea is systematic exploration of all possible thread interleavings just for specific relevant pairs of threads.We implemented the algorithm with Java Pathfinder as the backend verification tool, and evaluated it on several multithreaded Java programs. Results show that our incremental algorithm (1) can find errors very fast, (2) greatly reduces time needed for complete safety verification, and (3) it can find the same errors as full verification of the whole state space.

Klasifikace

  • 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)

Návaznosti výsledku

  • Projekt

    <a href="/cs/project/GA20-07487S" target="_blank" >GA20-07487S: Škálovatelné techniky pro analýzu komplexních vlastností počítačových systémů</a><br>

  • Návaznosti

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

Ostatní

  • Rok uplatnění

    2023

  • 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ů

Údaje specifické pro druh výsledku

  • Název statě ve sborníku

    ACM SIGSOFT Software Engineering Notes

  • ISBN

  • ISSN

    0163-5948

  • e-ISSN

  • Počet stran výsledku

    5

  • Strana od-do

    27-31

  • Název nakladatele

    ACM

  • Místo vydání

    New York, USA

  • Místo konání akce

    Michigan, United States

  • Datum konání akce

    10. 10. 2022

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

    WRD - Celosvětová akce

  • Kód UT WoS článku