Search Results

Documents authored by Nagele, Julian

Document
DOI: 10.4230/OASIcs.FMBC.2020.3
Populating the Peephole Optimizer of a Smart Contract Compiler

Authors: Maria A. Schett and Julian Nagele

Published in: OASIcs, Volume 84, 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)

Abstract
Developing compiler optimizations, especially for new, rapidly evolving smart contract languages, can be onerous and error-prone, but is especially important for smart contracts, where deployment and execution directly translate to monetary cost and which cannot change once deployed. One common optimization technique is the use of peephole optimizations, replacement rules that are applied using pattern-matching. These rules are normally constructed using human expertise, which is both time-consuming and far from systematic in exploring opportunities for optimization. In this work we propose a pipeline to automatically populate the peephole optimizer of a smart contract compiler. We apply superoptimization to an existing code base to obtain sequences of instructions, which can be replaced by cheaper, observationally equivalent instructions. We then generate peephole optimization rules by extracting the underlying patterns of these optimizations. We provide a case study of our approach and a prototype implementation for bytecode of the Ethereum Virtual Machine, the tool ppltr, which combines the superoptimizer ebso and the rule generator sorg. Then we evaluate our approach by generating and applying nearly 1k peephole optimization rules extracted from 2k optimizations obtained from deployed bytecode.
Cite as

Maria A. Schett and Julian Nagele. Populating the Peephole Optimizer of a Smart Contract Compiler. In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 3:1-3:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{schett_et_al:OASIcs.FMBC.2020.3,
  author =	{Schett, Maria A. and Nagele, Julian},
  title =	{{Populating the Peephole Optimizer of a Smart Contract Compiler}},
  booktitle =	{2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
  pages =	{3:1--3:15},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-169-6},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{84},
  editor =	{Bernardo, Bruno and Marmsoler, Diego},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.3},
  URN =		{urn:nbn:de:0030-drops-134169},
  doi =		{10.4230/OASIcs.FMBC.2020.3},
  annote =	{Keywords: Compiler Optimizations, Constraint Solving, Ethereum Bytecode}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2018.32
Confluence Competition 2018

Authors: Takahito Aoto, Makoto Hamana, Nao Hirokawa, Aart Middeldorp, Julian Nagele, Naoki Nishida, Kiraku Shintani, and Harald Zankl

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
We report on the 2018 edition of the Confluence Competition, a competition of software tools that aim to (dis)prove confluence and related properties of rewrite systems automatically.
Cite as

Takahito Aoto, Makoto Hamana, Nao Hirokawa, Aart Middeldorp, Julian Nagele, Naoki Nishida, Kiraku Shintani, and Harald Zankl. Confluence Competition 2018. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 32:1-32:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{aoto_et_al:LIPIcs.FSCD.2018.32,
  author =	{Aoto, Takahito and Hamana, Makoto and Hirokawa, Nao and Middeldorp, Aart and Nagele, Julian and Nishida, Naoki and Shintani, Kiraku and Zankl, Harald},
  title =	{{Confluence Competition 2018}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{32:1--32:5},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.32},
  URN =		{urn:nbn:de:0030-drops-92023},
  doi =		{10.4230/LIPIcs.FSCD.2018.32},
  annote =	{Keywords: Confluence, competition, rewrite systems}
}
Document
DOI: 10.4230/LIPIcs.RTA.2015.257
Improving Automatic Confluence Analysis of Rewrite Systems by Redundant Rules

Authors: Julian Nagele, Bertram Felgenhauer, and Aart Middeldorp

Published in: LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015)

Abstract
We describe how to utilize redundant rewrite rules, i.e., rules that can be simulated by other rules, when (dis)proving confluence of term rewrite systems. We demonstrate how automatic confluence provers benefit from the addition as well as the removal of redundant rules. Due to their simplicity, our transformations were easy to formalize in a proof assistant and are thus amenable to certification. Experimental results show the surprising gain in power.
Cite as

Julian Nagele, Bertram Felgenhauer, and Aart Middeldorp. Improving Automatic Confluence Analysis of Rewrite Systems by Redundant Rules. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 257-268, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{nagele_et_al:LIPIcs.RTA.2015.257,
  author =	{Nagele, Julian and Felgenhauer, Bertram and Middeldorp, Aart},
  title =	{{Improving Automatic Confluence Analysis of Rewrite Systems by Redundant Rules}},
  booktitle =	{26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
  pages =	{257--268},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-85-9},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{36},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.257},
  URN =		{urn:nbn:de:0030-drops-52010},
  doi =		{10.4230/LIPIcs.RTA.2015.257},
  annote =	{Keywords: term rewriting, confluence, automation, transformation}
}
Document
DOI: 10.4230/LIPIcs.RTA.2015.269
Certified Rule Labeling

Authors: Julian Nagele and Harald Zankl

Published in: LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015)

Abstract
The rule labeling heuristic aims to establish confluence of (left-)linear term rewrite systems via decreasing diagrams. We present a formalization of a confluence criterion based on the interplay of relative termination and the rule labeling in the theorem prover Isabelle. Moreover, we report on the integration of this result into the certifier CeTA, facilitating the checking of confluence certificates based on decreasing diagrams for the first time. The power of the method is illustrated by an experimental evaluation on a (standard) collection of confluence problems.
Cite as

Julian Nagele and Harald Zankl. Certified Rule Labeling. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 269-284, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{nagele_et_al:LIPIcs.RTA.2015.269,
  author =	{Nagele, Julian and Zankl, Harald},
  title =	{{Certified Rule Labeling}},
  booktitle =	{26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
  pages =	{269--284},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-85-9},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{36},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.269},
  URN =		{urn:nbn:de:0030-drops-52024},
  doi =		{10.4230/LIPIcs.RTA.2015.269},
  annote =	{Keywords: term rewriting, confluence, decreasing diagrams, certification}
}
Document
DOI: 10.4230/LIPIcs.RTA.2012.339
On the Formalization of Termination Techniques based on Multiset Orderings

Authors: René Thiemann, Guillaume Allais, and Julian Nagele

Published in: LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012)

Abstract
Multiset orderings are a key ingredient in certain termination techniques like the recursive path ordering and a variant of size-change termination. In order to integrate these techniques in a certifier for termination proofs, we have added them to the Isabelle Formalization of Rewriting. To this end, it was required to extend the existing formalization on multiset orderings towards a generalized multiset ordering. Afterwards, the soundness proofs of both techniques have been established, although only after fixing some definitions. Concerning efficiency, it is known that the search for suitable parameters for both techniques is NP-hard. We show that checking the correct application of the techniques--where all parameters are provided--is also NP-hard, since the problem of deciding the generalized multiset ordering is NP-hard.
Cite as

René Thiemann, Guillaume Allais, and Julian Nagele. On the Formalization of Termination Techniques based on Multiset Orderings. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 339-354, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{thiemann_et_al:LIPIcs.RTA.2012.339,
  author =	{Thiemann, Ren\'{e} and Allais, Guillaume and Nagele, Julian},
  title =	{{On the Formalization of Termination Techniques based on Multiset Orderings}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{339--354},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.339},
  URN =		{urn:nbn:de:0030-drops-35029},
  doi =		{10.4230/LIPIcs.RTA.2012.339},
  annote =	{Keywords: formalization, term rewriting, termination, orderings}
}
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