Search Results

Documents authored by Mathur, Umang

Document
DOI: 10.4230/LIPIcs.CONCUR.2021.16
Dynamic Data-Race Detection Through the Fine-Grained Lens

Authors: Rucha Kulkarni, Umang Mathur, and Andreas Pavlogiannis

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

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.
Cite as

Rucha Kulkarni, Umang Mathur, and Andreas Pavlogiannis. Dynamic Data-Race Detection Through the Fine-Grained Lens. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 16:1-16:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@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/entities/document/10.4230/LIPIcs.CONCUR.2021.16},
  URN =		{urn:nbn:de:0030-drops-143931},
  doi =		{10.4230/LIPIcs.CONCUR.2021.16},
  annote =	{Keywords: dynamic analyses, data races, fine-grained complexity}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.31
A Decidable Fragment of Second Order Logic With Applications to Synthesis

Authors: P. Madhusudan, Umang Mathur, Shambwaditya Saha, and Mahesh Viswanathan

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
We propose a fragment of many-sorted second order logic called EQSMT and show that checking satisfiability of sentences in this fragment is decidable. EQSMT formulae have an exists^*forall^* quantifier prefix (over variables, functions and relations) making EQSMT conducive for modeling synthesis problems. Moreover, EQSMT allows reasoning using a combination of background theories provided that they have a decidable satisfiability problem for the exists^*forall^* FO-fragment (e.g., linear arithmetic). Our decision procedure reduces the satisfiability of EQSMT formulae to satisfiability queries of exists^*forall^* formulae of each individual background theory, allowing us to use existing efficient SMT solvers supporting exists^*forall^* reasoning for these theories; hence our procedure can be seen as effectively quantified SMT (EQSMT) reasoning.
Cite as

P. Madhusudan, Umang Mathur, Shambwaditya Saha, and Mahesh Viswanathan. A Decidable Fragment of Second Order Logic With Applications to Synthesis. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 31:1-31:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{madhusudan_et_al:LIPIcs.CSL.2018.31,
  author =	{Madhusudan, P. and Mathur, Umang and Saha, Shambwaditya and Viswanathan, Mahesh},
  title =	{{A Decidable Fragment of Second Order Logic With Applications to Synthesis}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{31:1--31:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.31},
  URN =		{urn:nbn:de:0030-drops-96987},
  doi =		{10.4230/LIPIcs.CSL.2018.31},
  annote =	{Keywords: second order logic, synthesis, decidable fragment}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2014.505
Computing Information Flow Using Symbolic Model-Checking

Authors: Rohit Chadha, Umang Mathur, and Stefan Schwoon

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
Several measures have been proposed in literature for quantifying the information leaked by the public outputs of a program with secret inputs. We consider the problem of computing information leaked by a deterministic or probabilistic program when the measure of information is based on (a) min-entropy and (b) Shannon entropy. The key challenge in computing these measures is that we need the total number of possible outputs and, for each possible output, the number of inputs that lead to it. A direct computation of these quantities is infeasible because of the state-explosion problem. We therefore propose symbolic algorithms based on binary decision diagrams (BDDs). The advantage of our approach is that these symbolic algorithms can be easily implemented in any BDD-based model-checking tool that checks for reachability in deterministic non-recursive programs by computing program summaries. We demonstrate the validity of our approach by implementing these algorithms in a tool Moped-QLeak, which is built upon Moped, a model checker for Boolean programs. Finally, we show how this symbolic approach extends to probabilistic programs.
Cite as

Rohit Chadha, Umang Mathur, and Stefan Schwoon. Computing Information Flow Using Symbolic Model-Checking. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 505-516, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{chadha_et_al:LIPIcs.FSTTCS.2014.505,
  author =	{Chadha, Rohit and Mathur, Umang and Schwoon, Stefan},
  title =	{{Computing Information Flow Using Symbolic Model-Checking}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{505--516},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.505},
  URN =		{urn:nbn:de:0030-drops-48676},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.505},
  annote =	{Keywords: Information leakage, Min Entropy, Shannon Entropy, Abstract decision diagrams, Program summaries}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact