Schloss Dagstuhl - Leibniz-Zentrum fΓΌr Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum fΓΌr Informatik GmbH scholarly article en Kulkarni, Rucha; Mathur, Umang; Pavlogiannis, Andreas https://www.dagstuhl.de/lipics License: Creative Commons Attribution 4.0 license (CC BY 4.0)
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-143931
URL:

; ;

Dynamic Data-Race Detection Through the Fine-Grained Lens

pdf-format:


Abstract

Data races are among the most common bugs in concurrency. The standard approach to data-race detection is via dynamic analyses, which work over executions of concurrent programs, instead of the program source code. The rich literature on the topic has created various notions of dynamic data races, which are known to be detected efficiently when certain parameters (e.g., number of threads) are small. However, the fine-grained complexity of all these notions of races has remained elusive, making it impossible to characterize their trade-offs between precision and efficiency.
In this work we establish several fine-grained separations between many popular notions of dynamic data races. The input is an execution trace Οƒ with 𝒩 events, 𝒯 threads and β„’ locks. Our main results are as follows. First, we show that happens-before HB races can be detected in O(𝒩⋅ min(𝒯, β„’)) time, improving over the standard O(𝒩⋅ 𝒯) bound when β„’ = o(𝒯). Moreover, we show that even reporting an HB race that involves a read access is hard for 2-orthogonal vectors (2-OV). This is the first rigorous proof of the conjectured quadratic lower-bound in detecting HB races. Second, we show that the recently introduced synchronization-preserving races are hard to detect for 3-OV and thus have a cubic lower bound, when 𝒯 = Ξ©(𝒩). This establishes a complexity separation from HB races which are known to be strictly less expressive. Third, we show that lock-cover races are hard for 2-OV, and thus have a quadratic lower-bound, even when 𝒯 = 2 and β„’ = Ο‰(log 𝒩). The similar notion of lock-set races is known to be detectable in O(𝒩⋅ β„’) time, and thus we achieve a complexity separation between the two. Moreover, we show that lock-set races become hitting-set (HS)-hard when β„’ = Θ(𝒩), and thus also have a quadratic lower bound, when the input is sufficiently complex. To our knowledge, this is the first work that characterizes the complexity of well-established dynamic race-detection techniques, allowing for a rigorous comparison between them.

BibTeX - Entry

@InProceedings{kulkarni_et_al:LIPIcs.CONCUR.2021.16,
  author =	{Kulkarni, Rucha and Mathur, Umang and Pavlogiannis, Andreas},
  title =	{{Dynamic Data-Race Detection Through the Fine-Grained Lens}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{16:1--16:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/14393},
  URN =		{urn:nbn:de:0030-drops-143931},
  doi =		{10.4230/LIPIcs.CONCUR.2021.16},
  annote =	{Keywords: dynamic analyses, data races, fine-grained complexity}
}

Keywords: dynamic analyses, data races, fine-grained complexity
Seminar: 32nd International Conference on Concurrency Theory (CONCUR 2021)
Issue date: 2021
Date of publication: 13.08.2021


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI