Search Results

Documents authored by Toman, John

Document
DOI: 10.4230/LIPIcs.ECOOP.2018.24
Legato: An At-Most-Once Analysis with Applications to Dynamic Configuration Updates

Authors: John Toman and Dan Grossman

Published in: LIPIcs, Volume 109, 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

Abstract
Modern software increasingly relies on external resources whose location or content can change during program execution. Examples of such resources include remote network hosts, database entries, dynamically updated configuration options, etc. Long running, adaptable programs must handle these changes gracefully and correctly. Dealing with all possible resource update scenarios is difficult to get right, especially if, as is common, external resources can be modified without prior warning by code and/or users outside of the application's direct control. If a resource unexpectedly changes during a computation, an application may observe multiple, inconsistent states of the resource, leading to incorrect program behavior. This paper presents a sound and precise static analysis, Legato, that verifies programs correctly handle changes in external resources. Our analysis ensures that every value computed by an application reflects a single, consistent version of every external resource's state. Although consistent computation in the presence of concurrent resource updates is fundamentally a concurrency issue, our analysis relies on the novel at-most-once condition to avoid explicitly reasoning about concurrency. The at-most-once condition requires that all values depend on at most one access of each resource. Our analysis is flow-, field-, and context-sensitive. It scales to real-world Java programs while producing a moderate number of false positives. We applied Legato to 10 applications with dynamically updated configurations, and found several non-trivial consistency bugs.
Cite as

John Toman and Dan Grossman. Legato: An At-Most-Once Analysis with Applications to Dynamic Configuration Updates. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 24:1-24:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{toman_et_al:LIPIcs.ECOOP.2018.24,
  author =	{Toman, John and Grossman, Dan},
  title =	{{Legato: An At-Most-Once Analysis with Applications to Dynamic Configuration Updates}},
  booktitle =	{32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
  pages =	{24:1--24:32},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-079-8},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{109},
  editor =	{Millstein, Todd},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.24},
  URN =		{urn:nbn:de:0030-drops-92290},
  doi =		{10.4230/LIPIcs.ECOOP.2018.24},
  annote =	{Keywords: Static Analysis, Dynamic Configuration Updates}
}
Document
DOI: 10.4230/DARTS.4.3.2
Legato: An At-Most-Once Analysis with Applications to Dynamic Configuration Updates (Artifact)

Authors: John Toman and Dan Grossman

Published in: DARTS, Volume 4, Issue 3, Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

Abstract
This artifact supports Legato, an at-most-once analysis. An at-most-once analysis ensures that an application never observes inconsistent versions of its environment by checking that every value depends on at most one access of every external resource used by the application. We have applied this general analysis to the problem of finding errors in applications that support dynamic configuration updates (DCU), i.e., configuration updates that are applied immediately without program restart. When configurations may change at any point during execution, the enforcing the at-most-once condition for each configuration option guarantees that the program never observes inconsistent versions of configuration options. This artifact recreates our experiments, which applied Legato to 10 applications that support DCU and found several bugs across 9 of the 10 programs.
Cite as

John Toman and Dan Grossman. Legato: An At-Most-Once Analysis with Applications to Dynamic Configuration Updates (Artifact). In Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Dagstuhl Artifacts Series (DARTS), Volume 4, Issue 3, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{toman_et_al:DARTS.4.3.2,
  author =	{Toman, John and Grossman, Dan},
  title =	{{Legato: An At-Most-Once Analysis with Applications to Dynamic Configuration Updates (Artifact)}},
  pages =	{2:1--2:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2018},
  volume =	{4},
  number =	{3},
  editor =	{Toman, John and Grossman, Dan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.4.3.2},
  URN =		{urn:nbn:de:0030-drops-92342},
  doi =		{10.4230/DARTS.4.3.2},
  annote =	{Keywords: Static Analysis, Dynamic Configuration Updates}
}
Document
DOI: 10.4230/LIPIcs.SNAPL.2017.18
Taming the Static Analysis Beast

Authors: John Toman and Dan Grossman

Published in: LIPIcs, Volume 71, 2nd Summit on Advances in Programming Languages (SNAPL 2017)

Abstract
While industrial-strength static analysis over large, real-world codebases has become commonplace, so too have difficult-to-analyze language constructs, large libraries, and popular frameworks. These features make constructing and evaluating a novel, sound analysis painful, error-prone, and tedious. We motivate the need for research to address these issues by highlighting some of the many challenges faced by static analysis developers in today's software ecosystem. We then propose our short- and long-term research agenda to make static analysis over modern software less burdensome.
Cite as

John Toman and Dan Grossman. Taming the Static Analysis Beast. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 18:1-18:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{toman_et_al:LIPIcs.SNAPL.2017.18,
  author =	{Toman, John and Grossman, Dan},
  title =	{{Taming the Static Analysis Beast}},
  booktitle =	{2nd Summit on Advances in Programming Languages (SNAPL 2017)},
  pages =	{18:1--18:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-032-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{71},
  editor =	{Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2017.18},
  URN =		{urn:nbn:de:0030-drops-71213},
  doi =		{10.4230/LIPIcs.SNAPL.2017.18},
  annote =	{Keywords: static analysis, frameworks, api knowledge, library specifications}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2016.24
Staccato: A Bug Finder for Dynamic Configuration Updates

Authors: John Toman and Dan Grossman

Published in: LIPIcs, Volume 56, 30th European Conference on Object-Oriented Programming (ECOOP 2016)

Abstract
Modern software applications are highly configurable, allowing configuration options to be changed even during program execution. When dynamic configuration updating is implemented incorrectly, program errors can result. These program errors occur primarily when stale data—computed from old configurations—or inconsistent data—computed from different configurations—are used. We introduce Staccato, the first tool designed to detect these errors. Staccato uses a dynamic analysis in the style of taint analysis to find the use of stale configuration data in Java programs. It supports concurrent programs running on commodity JVMs. In some cases, Staccato can provide automatic bug avoidance and semi-automatic repair when errors occur. We evaluated Staccato on 3 open-source applications that support complex reconfigurability. Staccato found multiple errors in all of them. Staccato requires only modest annotation overhead and has moderate performance overhead.
Cite as

John Toman and Dan Grossman. Staccato: A Bug Finder for Dynamic Configuration Updates. In 30th European Conference on Object-Oriented Programming (ECOOP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 56, pp. 24:1-24:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{toman_et_al:LIPIcs.ECOOP.2016.24,
  author =	{Toman, John and Grossman, Dan},
  title =	{{Staccato: A Bug Finder for Dynamic Configuration Updates}},
  booktitle =	{30th European Conference on Object-Oriented Programming (ECOOP 2016)},
  pages =	{24:1--24:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-014-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{56},
  editor =	{Krishnamurthi, Shriram and Lerner, Benjamin S.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2016.24},
  URN =		{urn:nbn:de:0030-drops-61185},
  doi =		{10.4230/LIPIcs.ECOOP.2016.24},
  annote =	{Keywords: Dynamic Configuration Updates, Dynamic Analysis, Software configuration}
}
Document
DOI: 10.4230/DARTS.2.1.14
Staccato: A Bug Finder for Dynamic Configuration Updates (Artifact)

Authors: John Toman and Dan Grossman

Published in: DARTS, Volume 2, Issue 1, Special Issue of the 30th European Conference on Object-Oriented Programming (ECOOP 2016)

Abstract
This artifact is based on Staccato, a tool for finding errors in dynamic configuration update (DCU) implementations. Dynamic configuration update refers to configuration changes that occur at runtime without program restart. Errors in DCU implementations occur when stale data - computed from old configurations - or inconsistent data - computed from different configurations - are used. Staccato uses a dynamic analysis in the style of taint analysis to detect these errors. Staccato supports concurrent programs running on commodity JVMs. We evaluated Staccato on three open-source applications and found errors in all of them.
Cite as

John Toman and Dan Grossman. Staccato: A Bug Finder for Dynamic Configuration Updates (Artifact). In Special Issue of the 30th European Conference on Object-Oriented Programming (ECOOP 2016). Dagstuhl Artifacts Series (DARTS), Volume 2, Issue 1, pp. 14:1-14:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@Article{toman_et_al:DARTS.2.1.14,
  author =	{Toman, John and Grossman, Dan},
  title =	{{Staccato: A Bug Finder for Dynamic Configuration Updates (Artifact)}},
  pages =	{14:1--14:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2016},
  volume =	{2},
  number =	{1},
  editor =	{Toman, John and Grossman, Dan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.2.1.14},
  URN =		{urn:nbn:de:0030-drops-61350},
  doi =		{10.4230/DARTS.2.1.14},
  annote =	{Keywords: Dynamic Configuration Updates, Dynamic Analysis, Software configuration}
}
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