Search Results

Documents authored by Vollmer, Michael

Artifact
Software
DOI: 10.4230/artifacts.23657
packed-data

Authors: Arthur Jamet and Michael Vollmer

Abstract
Cite as

Copy BibTex To Clipboard

@misc{dagpub-supp--paper-22509-urlhackage.haskell.org-package-packed-data,
   title = {{packed-data}}, 
   author = {Jamet, Arthur and Vollmer, Michael},
   note = {Software, version 0.1.0.3., swhId: \href{https://archive.softwareheritage.org/swh:1:dir:027d47580c14b18a2969e17a715e86c2094246ad;origin=https://github.com/Arthi-chaud/packed-data;visit=swh:1:snp:e38671f0f86fd4c070f3d08db14c41ec7e7ef143;anchor=swh:1:rev:33072fdaccd3f25cd416276780f2a2b2778e29d3}{\texttt{swh:1:dir:027d47580c14b18a2969e17a715e86c2094246ad}} (visited on 2025-06-25)},
   url = {https://github.com/Arthi-chaud/packed-data.git},
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.15
Spegion: Implicit and Non-Lexical Regions with Sized Allocations

Authors: Jack Hughes, Michael Vollmer, and Mark Batty

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
Region based memory management is a powerful tool designed with the goal of ensuring memory safety statically. The region calculus of Tofte and Talpin is a well known example of a region based system, which uses regions to manage memory in a stack-like fashion. However, the region calculus is lexically scoped and requires explicit annotation of memory regions, which can be cumbersome for the programmer. Other systems have addressed non-lexical regions, but these approaches typically require the use of a substructural type system to track the lifetimes of regions. We present Spegion, a language with implicit non-lexical regions, which provides these same memory safety guarantees for programs that go beyond using memory allocation in a stack-like manner. We are able to achieve this with a concise syntax, and without the use of substructural types, relying instead on an effect system to enforce constraints on region allocation and deallocation. These regions may be divided into sub-regions, i.e., Splittable rEgions, allowing fine grained control over memory allocation. Furthermore, Spegion permits sized allocations, where each value has an associated size which is used to ensure that regions are not over-allocated into. We present a type system for Spegion and prove it is type safe with respect to a small-step operational semantics.
Cite as

Jack Hughes, Michael Vollmer, and Mark Batty. Spegion: Implicit and Non-Lexical Regions with Sized Allocations. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 15:1-15:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{hughes_et_al:LIPIcs.ECOOP.2025.15,
  author =	{Hughes, Jack and Vollmer, Michael and Batty, Mark},
  title =	{{Spegion: Implicit and Non-Lexical Regions with Sized Allocations}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{15:1--15:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.15},
  URN =		{urn:nbn:de:0030-drops-233082},
  doi =		{10.4230/LIPIcs.ECOOP.2025.15},
  annote =	{Keywords: Regions, Type Systems, Effect Systems, Programming Languages, Memory}
}
Document
Experience Paper
DOI: 10.4230/LIPIcs.ECOOP.2025.38
Type-Safe and Portable Support for Packed Data (Experience Paper)

Authors: Arthur Jamet and Michael Vollmer

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
When components of a system exchange data, they need to serialise the data so that it can be sent over the network. Then, the recipient has to deserialise the data in order to be able to process it. These steps take time and have an impact on the overall system’s performance. A solution to this is to use packed data, which has a unified representation between the memory and the network, removing the need for any marshalling steps. Additionally, using this data representation can improve the program’s performance thanks to the data locality enabled by the compact representation of the data in memory. Unfortunately, no mainstream programming languages support packed data, whether it’s out-of-the-box or through a compiler extension. We present packed-data, a Haskell library that allows for type safe building and reading of packed data in a functional style. The library does not rely on compiler modifications, making it portable, and leverages meta-programming to allow programmers to pack their own data types effortlessly. We evaluate the usability and performance of the library, and conclude that it allows traversing packed data up to 60% faster than unpacked data. We also reflect on how to enhance the performance of library-based support for packed data. Our implementation approach is general and can easily be used with any programming languages that support higher-kinded types.
Cite as

Arthur Jamet and Michael Vollmer. Type-Safe and Portable Support for Packed Data (Experience Paper). In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 38:1-38:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{jamet_et_al:LIPIcs.ECOOP.2025.38,
  author =	{Jamet, Arthur and Vollmer, Michael},
  title =	{{Type-Safe and Portable Support for Packed Data}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{38:1--38:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.38},
  URN =		{urn:nbn:de:0030-drops-233301},
  doi =		{10.4230/LIPIcs.ECOOP.2025.38},
  annote =	{Keywords: program optimisation, data structures, data layout, packed data}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2024.38
Optimizing Layout of Recursive Datatypes with Marmoset: Or, Algorithms + Data Layouts = Efficient Programs

Authors: Vidush Singhal, Chaitanya Koparkar, Joseph Zullo, Artem Pelenitsyn, Michael Vollmer, Mike Rainey, Ryan Newton, and Milind Kulkarni

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
While programmers know that memory representation of data structures can have significant effects on performance, compiler support to optimize the layout of those structures is an under-explored field. Prior work has optimized the layout of individual, non-recursive structures without considering how collections of those objects in linked or recursive data structures are laid out. This work introduces Marmoset, a compiler that optimizes the layouts of algebraic datatypes, with a special focus on producing highly optimized, packed data layouts where recursive structures can be traversed with minimal pointer chasing. Marmoset performs an analysis of how a recursive ADT is used across functions to choose a global layout that promotes simple, strided access for that ADT in memory. It does so by building and solving a constraint system to minimize an abstract cost model, yielding a predicted efficient layout for the ADT. Marmoset then builds on top of Gibbon, a prior compiler for packed, mostly-serial representations, to synthesize optimized ADTs. We show experimentally that Marmoset is able to choose optimal layouts across a series of microbenchmarks and case studies, outperforming both Gibbon’s baseline approach, as well as MLton, a Standard ML compiler that uses traditional pointer-heavy representations.
Cite as

Vidush Singhal, Chaitanya Koparkar, Joseph Zullo, Artem Pelenitsyn, Michael Vollmer, Mike Rainey, Ryan Newton, and Milind Kulkarni. Optimizing Layout of Recursive Datatypes with Marmoset: Or, Algorithms + Data Layouts = Efficient Programs. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 38:1-38:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{singhal_et_al:LIPIcs.ECOOP.2024.38,
  author =	{Singhal, Vidush and Koparkar, Chaitanya and Zullo, Joseph and Pelenitsyn, Artem and Vollmer, Michael and Rainey, Mike and Newton, Ryan and Kulkarni, Milind},
  title =	{{Optimizing Layout of Recursive Datatypes with Marmoset: Or, Algorithms + Data Layouts = Efficient Programs}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{38:1--38:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.38},
  URN =		{urn:nbn:de:0030-drops-208875},
  doi =		{10.4230/LIPIcs.ECOOP.2024.38},
  annote =	{Keywords: Tree traversals, Compilers, Data layout optimization, Dense data layout}
}
Document
Artifact
DOI: 10.4230/DARTS.10.2.21
Optimizing Layout of Recursive Datatypes with Marmoset (Artifact)

Authors: Vidush Singhal, Chaitanya Koparkar, Joseph Zullo, Artem Pelenitsyn, Michael Vollmer, Mike Rainey, Ryan Newton, and Milind Kulkarni

Published in: DARTS, Volume 10, Issue 2, Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
While programmers know that memory representation of data structures can have significant effects on performance, compiler support to optimize the layout of those structures is an under-explored field. Prior work has optimized the layout of individual, non-recursive structures without considering how collections of those objects in linked or recursive data structures are laid out. This work introduces Marmoset, a compiler that optimizes the layouts of algebraic datatypes, with a special focus on producing highly optimized, packed data layouts where recursive structures can be traversed with minimal pointer chasing. Marmoset performs an analysis of how a recursive ADT is used across functions to choose a global layout that promotes simple, strided access for that ADT in memory. It does so by building and solving a constraint system to minimize an abstract cost model, yielding a predicted efficient layout for the ADT. Marmoset then builds on top of Gibbon, a prior compiler for packed, mostly-serial representations, to synthesize optimized ADTs. We show experimentally that Marmoset is able to choose optimal layouts across a series of microbenchmarks and case studies, outperforming both Gibbon’s baseline approach, as well as MLton, a Standard ML compiler that uses traditional pointer-heavy representations.
Cite as

Vidush Singhal, Chaitanya Koparkar, Joseph Zullo, Artem Pelenitsyn, Michael Vollmer, Mike Rainey, Ryan Newton, and Milind Kulkarni. Optimizing Layout of Recursive Datatypes with Marmoset (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 21:1-21:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{singhal_et_al:DARTS.10.2.21,
  author =	{Singhal, Vidush and Koparkar, Chaitanya and Zullo, Joseph and Pelenitsyn, Artem and Vollmer, Michael and Rainey, Mike and Newton, Ryan and Kulkarni, Milind},
  title =	{{Optimizing Layout of Recursive Datatypes with Marmoset (Artifact)}},
  pages =	{21:1--21:10},
  journal =	{Dagstuhl Artifacts Series},
  ISBN =	{978-3-95977-342-3},
  ISSN =	{2509-8195},
  year =	{2024},
  volume =	{10},
  number =	{2},
  editor =	{Singhal, Vidush and Koparkar, Chaitanya and Zullo, Joseph and Pelenitsyn, Artem and Vollmer, Michael and Rainey, Mike and Newton, Ryan and Kulkarni, Milind},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.21},
  URN =		{urn:nbn:de:0030-drops-209199},
  doi =		{10.4230/DARTS.10.2.21},
  annote =	{Keywords: Tree traversals, Compilers, Data layout optimization, Dense data layout}
}
Document
Experience Paper
DOI: 10.4230/LIPIcs.ECOOP.2023.39
Rust for Morello: Always-On Memory Safety, Even in Unsafe Code (Experience Paper)

Authors: Sarah Harris, Simon Cooksey, Michael Vollmer, and Mark Batty

Published in: LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract
Memory safety issues are a serious concern in systems programming. Rust is a systems language that provides memory safety through a combination of a static checks embodied in the type system and ad hoc dynamic checks inserted where this analysis becomes impractical. The Morello prototype architecture from ARM uses capabilities, fat pointers augmented with object bounds information, to catch failures of memory safety. This paper presents a compiler from Rust to the Morello architecture, together with a comparison of the performance of Rust’s runtime safety checks and the hardware-supported checks of Morello. The cost of Morello’s always-on memory safety guarantees is 39% in our 19 benchmark suites from the Rust crates repository (comprising 870 total benchmarks). For this cost, Morello’s capabilities ensure that even unsafe Rust code benefits from memory safety guarantees.
Cite as

Sarah Harris, Simon Cooksey, Michael Vollmer, and Mark Batty. Rust for Morello: Always-On Memory Safety, Even in Unsafe Code (Experience Paper). In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 39:1-39:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{harris_et_al:LIPIcs.ECOOP.2023.39,
  author =	{Harris, Sarah and Cooksey, Simon and Vollmer, Michael and Batty, Mark},
  title =	{{Rust for Morello: Always-On Memory Safety, Even in Unsafe Code}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{39:1--39:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.39},
  URN =		{urn:nbn:de:0030-drops-182322},
  doi =		{10.4230/LIPIcs.ECOOP.2023.39},
  annote =	{Keywords: Compilers, Rust, Memory Safety, CHERI}
}
Document
Artifact
DOI: 10.4230/DARTS.9.2.25
Rust for Morello: Always-On Memory Safety, Even in Unsafe Code (Artifact)

Authors: Sarah Harris, Simon Cooksey, Michael Vollmer, and Mark Batty

Published in: DARTS, Volume 9, Issue 2, Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract
Cite as

Sarah Harris, Simon Cooksey, Michael Vollmer, and Mark Batty. Rust for Morello: Always-On Memory Safety, Even in Unsafe Code (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 25:1-25:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{harris_et_al:DARTS.9.2.25,
  author =	{Harris, Sarah and Cooksey, Simon and Vollmer, Michael and Batty, Mark},
  title =	{{Rust for Morello: Always-On Memory Safety, Even in Unsafe Code (Artifact)}},
  pages =	{25:1--25:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2023},
  volume =	{9},
  number =	{2},
  editor =	{Harris, Sarah and Cooksey, Simon and Vollmer, Michael and Batty, Mark},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.25},
  URN =		{urn:nbn:de:0030-drops-182650},
  doi =		{10.4230/DARTS.9.2.25},
  annote =	{Keywords: Compilers, Rust, Memory Safety, CHERI}
}
Document
DOI: 10.4230/LIPIcs.ESA.2019.80
Simultaneous Representation of Proper and Unit Interval Graphs

Authors: Ignaz Rutter, Darren Strash, Peter Stumpf, and Michael Vollmer

Published in: LIPIcs, Volume 144, 27th Annual European Symposium on Algorithms (ESA 2019)

Abstract
In a confluence of combinatorics and geometry, simultaneous representations provide a way to realize combinatorial objects that share common structure. A standard case in the study of simultaneous representations is the sunflower case where all objects share the same common structure. While the recognition problem for general simultaneous interval graphs - the simultaneous version of arguably one of the most well-studied graph classes - is NP-complete, the complexity of the sunflower case for three or more simultaneous interval graphs is currently open. In this work we settle this question for proper interval graphs. We give an algorithm to recognize simultaneous proper interval graphs in linear time in the sunflower case where we allow any number of simultaneous graphs. Simultaneous unit interval graphs are much more "rigid" and therefore have less freedom in their representation. We show they can be recognized in time O(|V|*|E|) for any number of simultaneous graphs in the sunflower case where G=(V,E) is the union of the simultaneous graphs. We further show that both recognition problems are in general NP-complete if the number of simultaneous graphs is not fixed. The restriction to the sunflower case is in this sense necessary.
Cite as

Ignaz Rutter, Darren Strash, Peter Stumpf, and Michael Vollmer. Simultaneous Representation of Proper and Unit Interval Graphs. In 27th Annual European Symposium on Algorithms (ESA 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 144, pp. 80:1-80:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{rutter_et_al:LIPIcs.ESA.2019.80,
  author =	{Rutter, Ignaz and Strash, Darren and Stumpf, Peter and Vollmer, Michael},
  title =	{{Simultaneous Representation of Proper and Unit Interval Graphs}},
  booktitle =	{27th Annual European Symposium on Algorithms (ESA 2019)},
  pages =	{80:1--80:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-124-5},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{144},
  editor =	{Bender, Michael A. and Svensson, Ola and Herman, Grzegorz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2019.80},
  URN =		{urn:nbn:de:0030-drops-112013},
  doi =		{10.4230/LIPIcs.ESA.2019.80},
  annote =	{Keywords: Intersection Graphs, Recognition Algorithm, Proper/Unit Interval Graphs, Simultaneous Representations}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2017.26
Compiling Tree Transforms to Operate on Packed Representations

Authors: Michael Vollmer, Sarah Spall, Buddhika Chamith, Laith Sakka, Chaitanya Koparkar, Milind Kulkarni, Sam Tobin-Hochstadt, and Ryan R. Newton

Published in: LIPIcs, Volume 74, 31st European Conference on Object-Oriented Programming (ECOOP 2017)

Abstract
When written idiomatically in most programming languages, programs that traverse and construct trees operate over pointer-based data structures, using one heap object per-leaf and per-node. This representation is efficient for random access and shape-changing modifications, but for traversals, such as compiler passes, that process most or all of a tree in bulk, it can be inefficient. In this work we instead compile tree traversals to operate on pointer-free pre-order serializations of trees. On modern architectures such programs often run significantly faster than their pointer-based counterparts, and additionally are directly suited to storage and transmission without requiring marshaling. We present a prototype compiler, Gibbon, that compiles a small first-order, purely functional language sufficient for tree traversals. The compiler transforms this language into intermediate representation with explicit pointers into input and output buffers for packed data. The key compiler technologies include an effect system for capturing traversal behavior, combined with an algorithm to insert destination cursors. We evaluate our compiler on tree transformations over a real-world dataset of source-code syntax trees. For traversals touching the whole tree, such as maps and folds, packed data allows speedups of over 2x compared to a highly-optimized pointer-based baseline.
Cite as

Michael Vollmer, Sarah Spall, Buddhika Chamith, Laith Sakka, Chaitanya Koparkar, Milind Kulkarni, Sam Tobin-Hochstadt, and Ryan R. Newton. Compiling Tree Transforms to Operate on Packed Representations. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 26:1-26:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{vollmer_et_al:LIPIcs.ECOOP.2017.26,
  author =	{Vollmer, Michael and Spall, Sarah and Chamith, Buddhika and Sakka, Laith and Koparkar, Chaitanya and Kulkarni, Milind and Tobin-Hochstadt, Sam and Newton, Ryan R.},
  title =	{{Compiling Tree Transforms to Operate on Packed Representations}},
  booktitle =	{31st European Conference on Object-Oriented Programming (ECOOP 2017)},
  pages =	{26:1--26:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-035-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{74},
  editor =	{M\"{u}ller, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.26},
  URN =		{urn:nbn:de:0030-drops-72737},
  doi =		{10.4230/LIPIcs.ECOOP.2017.26},
  annote =	{Keywords: compiler optimization, program transformation, tree traversal}
}
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact