Search Results

Documents authored by Wachter, Björn

Document
DOI: 10.4230/OASIcs.WCET.2007.1190
Towards Symbolic State Traversal for Efficient WCET Analysis of Abstract Pipeline and Cache Models

Authors: Stephan Wilhelm and Björn Wachter

Published in: OASIcs, Volume 6, 7th International Workshop on Worst-Case Execution Time Analysis (WCET'07) (2007)

Abstract
Static program analysis is a proven approach for obtaining safe and tight upper bounds on the worst-case execution time (WCET) of program tasks. It requires an analysis on the microarchitectural level, most notably pipeline and cache analysis. In our approach, the integrated pipeline and cache analysis operates on sets of possible abstract hardware states. Due to the growth of CPU complexity and the existence of timing anomalies, the analysis must handle an increasing number of possible abstract states for each program point. Symbolic methods have been proposed as a way to reduce memory consumption and improve runtime in order to keep pace with the growing hardware complexity. This paper presents the advances made since the original proposal and discusses a compact representation of abstract caches for integration with symbolic pipeline analysis.
Cite as

Stephan Wilhelm and Björn Wachter. Towards Symbolic State Traversal for Efficient WCET Analysis of Abstract Pipeline and Cache Models. In 7th International Workshop on Worst-Case Execution Time Analysis (WCET'07). Open Access Series in Informatics (OASIcs), Volume 6, pp. 1-6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{wilhelm_et_al:OASIcs.WCET.2007.1190,
  author =	{Wilhelm, Stephan and Wachter, Bj\"{o}rn},
  title =	{{Towards Symbolic State Traversal for Efficient WCET Analysis of Abstract Pipeline and Cache Models}},
  booktitle =	{7th International Workshop on Worst-Case Execution Time Analysis (WCET'07)},
  pages =	{1--6},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-05-7},
  ISSN =	{2190-6807},
  year =	{2007},
  volume =	{6},
  editor =	{Rochange, Christine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2007.1190},
  URN =		{urn:nbn:de:0030-drops-11904},
  doi =		{10.4230/OASIcs.WCET.2007.1190},
  annote =	{Keywords: WCET, worst-case execution time, hard real-time, embedded systems, abstract interpretation, pipeline analysis, cache analysis, symbolic state traversal BDD}
}
Document
DOI: 10.4230/OASIcs.TrustworthySW.2006.701
Explaining Data Type Reduction in the Shape Analysis Framework

Authors: Björn Wachter

Published in: OASIcs, Volume 3, Workshop on Trustworthy Software (2006)

Abstract
Automatic formal verification of systems composed of a large or even unbounded number of components is difficult as the state space of these systems is prohibitively large. Abstraction techniques automatically construct finite approximations of infinite-state systems from which safe information about the original system can be inferred. We study two abstraction techniques shape analysis, a technique from program analysis, and data type reduction, originating from model checking. Until recently we did not properly understand how shape analysis and data type reduction relate. In this talk, we shed light on this relation in a comprehensive way. This is a step towards a more unified view of abstraction employed in the static analysis and model checking community.
Cite as

Björn Wachter. Explaining Data Type Reduction in the Shape Analysis Framework. In Workshop on Trustworthy Software. Open Access Series in Informatics (OASIcs), Volume 3, pp. 1-6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{wachter:OASIcs.TrustworthySW.2006.701,
  author =	{Wachter, Bj\"{o}rn},
  title =	{{Explaining Data Type Reduction in the Shape Analysis Framework}},
  booktitle =	{Workshop on Trustworthy Software},
  pages =	{1--6},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-02-6},
  ISSN =	{2190-6807},
  year =	{2006},
  volume =	{3},
  editor =	{Autexier, Serge and Merz, Stephan and van der Torre, Leon and Wilhelm, Reinhard and Wolper, Pierre},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TrustworthySW.2006.701},
  URN =		{urn:nbn:de:0030-drops-7016},
  doi =		{10.4230/OASIcs.TrustworthySW.2006.701},
  annote =	{Keywords: Canonical abstraction, data type reduction, model checking, parameterized system, infinite-state}
}
Document
DOI: 10.4230/OASIcs.WCET.2006.671
A Definition and Classification of Timing Anomalies

Authors: Jan Reineke, Björn Wachter, Stefan Thesing, Reinhard Wilhelm, Ilia Polian, Jochen Eisinger, and Bernd Becker

Published in: OASIcs, Volume 4, 6th International Workshop on Worst-Case Execution Time Analysis (WCET'06) (2006)

Abstract
Timing Anomalies are characterized by counterintuitive timing behaviour. A locally faster execution leads to an increase of the execution time of the whole program. The presence of such behaviour makes WCET analysis more difficult: It is not safe to assume local worst-case behaviour wherever the analysis encounters uncertainty. Existing definitions of Timing Anomalies are rather imprecise and intuitive in nature. Some do not cover all kinds of known Timing Anomalies. After giving an overview of related work, we give a concise formal definition of Timing Anomalies. We then begin to identify different classes of anomalies. One of these classes, coined Scheduling Timing Anomalies, coincides with previous restricted definitions.
Cite as

Jan Reineke, Björn Wachter, Stefan Thesing, Reinhard Wilhelm, Ilia Polian, Jochen Eisinger, and Bernd Becker. A Definition and Classification of Timing Anomalies. In 6th International Workshop on Worst-Case Execution Time Analysis (WCET'06). Open Access Series in Informatics (OASIcs), Volume 4, pp. 1-6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{reineke_et_al:OASIcs.WCET.2006.671,
  author =	{Reineke, Jan and Wachter, Bj\"{o}rn and Thesing, Stefan and Wilhelm, Reinhard and Polian, Ilia and Eisinger, Jochen and Becker, Bernd},
  title =	{{A Definition and Classification of Timing Anomalies}},
  booktitle =	{6th International Workshop on Worst-Case Execution Time Analysis (WCET'06)},
  pages =	{1--6},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-03-3},
  ISSN =	{2190-6807},
  year =	{2006},
  volume =	{4},
  editor =	{Mueller, Frank},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2006.671},
  URN =		{urn:nbn:de:0030-drops-6713},
  doi =		{10.4230/OASIcs.WCET.2006.671},
  annote =	{Keywords: Timing analysis, Worst-case execution time, Timing anomalies, Scheduling Anomalies, Abstraction}
}
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