4 Search Results for "Dreyer, Alexander"


Document
Continuous Non-Intrusive Hybrid WCET Estimation Using Waypoint Graphs

Authors: Boris Dreyer, Christian Hochberger, Alexander Lange, Simon Wegener, and Alexander Weiss

Published in: OASIcs, Volume 55, 16th International Workshop on Worst-Case Execution Time Analysis (WCET 2016)


Abstract
Traditionally, the Worst-Case Execution Time (WCET) of Embedded Software has been estimated using analytical approaches. This is effective, if good models of the processor/System-on-Chip (SoC) architecture exist. Unfortunately, modern high performance SoCs often contain unpredictable and/or undocumented components that influence the timing behaviour. Thus, analytical results for such processors are unrealistically pessimistic. One possible alternative approach seems to be hybrid WCET analysis, where measurement data together with an analytical approach is used to estimate worst-case behaviour. Previously, we demonstrated how continuous evaluation of basic block trace data can be used to produce detailed statistics of basic blocks in embedded software. In the meantime it has become clear that the trace data provided by modern SoCs delivers a different type of information. In this contribution, we show that even under realistic conditions, a meaningful analysis can be conducted with the trace data.

Cite as

Boris Dreyer, Christian Hochberger, Alexander Lange, Simon Wegener, and Alexander Weiss. Continuous Non-Intrusive Hybrid WCET Estimation Using Waypoint Graphs. In 16th International Workshop on Worst-Case Execution Time Analysis (WCET 2016). Open Access Series in Informatics (OASIcs), Volume 55, pp. 4:1-4:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{dreyer_et_al:OASIcs.WCET.2016.4,
  author =	{Dreyer, Boris and Hochberger, Christian and Lange, Alexander and Wegener, Simon and Weiss, Alexander},
  title =	{{Continuous Non-Intrusive Hybrid WCET Estimation Using Waypoint Graphs}},
  booktitle =	{16th International Workshop on Worst-Case Execution Time Analysis (WCET 2016)},
  pages =	{4:1--4:11},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-025-5},
  ISSN =	{2190-6807},
  year =	{2016},
  volume =	{55},
  editor =	{Schoeberl, Martin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2016.4},
  URN =		{urn:nbn:de:0030-drops-68977},
  doi =		{10.4230/OASIcs.WCET.2016.4},
  annote =	{Keywords: Hybrid Worst-Case Execution Time (WCET) Estimation for Multicore Processors, Real-time Systems}
}
Document
Precise Continuous Non-Intrusive Measurement-Based Execution Time Estimation

Authors: Boris Dreyer, Christian Hochberger, Simon Wegener, and Alexander Weiss

Published in: OASIcs, Volume 47, 15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015)


Abstract
Precise estimation of the Worst-Case Execution Time (WCET) of embedded software is a necessary precondition in safety critical systems. Static methods for WCET analysis rely on precise models of the target processor’s micro-architecture. Measurement-based methods, in contrast, rely on exhaustive measurements performed on the real hardware. The rise of the multicore processors often renders staticWCET analysis infeasible, either due to the computational complexity or due the lack of necessary documentation. Current approaches for (hybrid) measurement-based WCET estimation process the trace data offline and thus need to store large amounts of data. In this contribution, we present a novel approach that performs continuous online aggregation of timing measurements. This enables long observation periods and increases the possibility to catch rare circumstances. Moreover, we incorporate the execution contexts of basic blocks. We can therefore account for typical cache behaviour, without being overly pessimistic.

Cite as

Boris Dreyer, Christian Hochberger, Simon Wegener, and Alexander Weiss. Precise Continuous Non-Intrusive Measurement-Based Execution Time Estimation. In 15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015). Open Access Series in Informatics (OASIcs), Volume 47, pp. 45-54, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{dreyer_et_al:OASIcs.WCET.2015.45,
  author =	{Dreyer, Boris and Hochberger, Christian and Wegener, Simon and Weiss, Alexander},
  title =	{{Precise Continuous Non-Intrusive Measurement-Based Execution Time Estimation}},
  booktitle =	{15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015)},
  pages =	{45--54},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-95-8},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{47},
  editor =	{Cazorla, Francisco J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2015.45},
  URN =		{urn:nbn:de:0030-drops-52555},
  doi =		{10.4230/OASIcs.WCET.2015.45},
  annote =	{Keywords: Hybrid Worst-Case Execution Time (WCET) Estimation for Multicore Processors, Real-time Systems}
}
Document
Network-driven Boolean Normal Forms

Authors: Michael Brickenstein and Alexander Dreyer

Published in: Dagstuhl Seminar Proceedings, Volume 10271, Verification over discrete-continuous boundaries (2010)


Abstract
We apply the PolyBoRi framework for Groebner bases computations with Boolean polynomials to bit-valued problems from algebraic cryptanalysis and formal verification. First, we proposed zero-suppressed binary decision diagrams (ZDDs) as a suitable data structure for Boolean polynomials. Utilizing the advantages of ZDDs we develop new reduced normal form algorithms for linear lexicographical lead rewriting systems. The latter play an important role in modeling bit-valued components of digital systems. Next, we reorder the variables in Boolean polynomial rings with respect to the topology of digital components. This brings computational algebra to digital circuits and small scale crypto systems in the first place. We additionally propose an optimized topological ordering, which tends to keep the intermediate results small. Thus, we successfully applied the linear lexicographical lead techniques to non-trivial examples from formal verification of digital systems. Finally, we evaluate the performance using benchmark examples from formal verification and cryptanalysis including equivalence checking of a bit-level formulation of multiplier components. Before we introduced topological orderings in PolyBoRi, state of the art for the algebraic approach was a bit-width of 4 for each factor. By combining our techniques we raised this bound to 16, which is an important step towards real-world applications.

Cite as

Michael Brickenstein and Alexander Dreyer. Network-driven Boolean Normal Forms. In Verification over discrete-continuous boundaries. Dagstuhl Seminar Proceedings, Volume 10271, pp. 1-8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


Copy BibTex To Clipboard

@InProceedings{brickenstein_et_al:DagSemProc.10271.3,
  author =	{Brickenstein, Michael and Dreyer, Alexander},
  title =	{{Network-driven Boolean Normal Forms}},
  booktitle =	{Verification over discrete-continuous boundaries},
  pages =	{1--8},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10271},
  editor =	{Bernd Becker and Luca Cardelli and Holger Hermanns and Sofiene Tahar},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10271.3},
  URN =		{urn:nbn:de:0030-drops-27894},
  doi =		{10.4230/DagSemProc.10271.3},
  annote =	{Keywords: Groebner, normal forms, Boolean polynomials, cryptanalysis, verification}
}
Document
Solving hard instances in QF-BV combining Boolean reasoning with computer algebra

Authors: Markus Wedler, Evgeny Pavlenko, Alexander Dreyer, Frank Seelisch, Dominik Stoffel, Gert-Martin Greuel, and Wolfgang Kunz

Published in: Dagstuhl Seminar Proceedings, Volume 9461, Algorithms and Applications for Next Generation SAT Solvers (2010)


Abstract
This paper describes our new satisfyability (SAT) modulo theory (SMT) solver STABLE for the quantifier-free logic over fixed size bit vectors. Our main application domain is formal verification of system-on-chip (SoC) modules designed for complex computational tasks, for example, in signal processing applications. Ensuring proper functional behavior for such modules, including arithmetic correctness of the data paths, is considered a very difficult problem. We show how methods from computer algebra can be integrated into an SMT solver such that instances can be handled where the arithmetic problem parts are specified mixing various levels of abstraction from the plain gate level for small highly optimized components up to the pure word level used in high-level specifications. If the arithmetic problem parts include multiplications such mixed problem descriptions quickly drive current SMT solvers towards their capacity limits. High performance data paths are often designed at a level of abstraction that we call the arithmetic bit level (ABL). We show how ABL information, if available in an SMT instance, can be used to transform the decision problem into an equivalent set of variety subset problems. These problems can be solved efficiently with techniques from computer algebra based on Gröbner basis theory over finite rings Z/2^n . Sometimes, instances contain problem parts at a level below the ABL using gate-level operations. These problem parts, e.g., originate from custom-designed arithmetic components that are highly optimized using the gate-level constructs of a hardware description language (HDL). For such cases we integrate a local ABL extraction technique based on local Reed-Muller forms.

Cite as

Markus Wedler, Evgeny Pavlenko, Alexander Dreyer, Frank Seelisch, Dominik Stoffel, Gert-Martin Greuel, and Wolfgang Kunz. Solving hard instances in QF-BV combining Boolean reasoning with computer algebra. In Algorithms and Applications for Next Generation SAT Solvers. Dagstuhl Seminar Proceedings, Volume 9461, pp. 1-20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


Copy BibTex To Clipboard

@InProceedings{wedler_et_al:DagSemProc.09461.4,
  author =	{Wedler, Markus and Pavlenko, Evgeny and Dreyer, Alexander and Seelisch, Frank and Stoffel, Dominik and Greuel, Gert-Martin and Kunz, Wolfgang},
  title =	{{Solving hard instances in QF-BV combining Boolean reasoning with computer algebra}},
  booktitle =	{Algorithms and Applications for Next Generation SAT Solvers},
  pages =	{1--20},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9461},
  editor =	{Bernd Becker and Valeria Bertacoo and Rolf Drechsler and Masahiro Fujita},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.09461.4},
  URN =		{urn:nbn:de:0030-drops-25096},
  doi =		{10.4230/DagSemProc.09461.4},
  annote =	{Keywords: SAT modulo Theory, Quantifier Free logic over fixed sized bitvectors; Computer Algebra}
}
  • Refine by Author
  • 2 Dreyer, Alexander
  • 2 Dreyer, Boris
  • 2 Hochberger, Christian
  • 2 Wegener, Simon
  • 2 Weiss, Alexander
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 2 Hybrid Worst-Case Execution Time (WCET) Estimation for Multicore Processors
  • 2 Real-time Systems
  • 1 Boolean polynomials
  • 1 Groebner
  • 1 Quantifier Free logic over fixed sized bitvectors; Computer Algebra
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 2 2010
  • 1 2015
  • 1 2016

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