arXiv subjects

Ryan Newton

Publications and source records attributed to Ryan Newton.

3 recordsLinked to original sources

arXiv2024

Optimizing Layout of Recursive Datatypes with Marmoset

While programmers know that the low-level 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 Gibbons baseline approach, as well as MLton, a Standard ML compiler that uses traditional pointer-heavy representations.

cs.PL↗

arXiv2021

Profile-Guided, Multi-Version Binary Rewriting

The static instrumentation of machine code, also known as binary rewriting, is a power technique, but suffers from high runtime overhead compared to compiler-level instrumentation. Recent research has shown that tools can achieve near-to-zero overhead when rewriting binaries (excluding the overhead from the application specific instrumentation). However, the users of binary rewriting tools often have difficulties in understanding why their instrumentation is slow and how to optimize their instrumentation. We are inspired by a traditional program optimization workflow, where one can profile the program execution to identify performance hot spots, modify the source code or apply suitable compiler optimizations, and even apply profile-guided optimization. We present profile-guided, Multi-Version Binary Rewriting to enable this optimization workflow for static binary instrumentation. Our new techniques include three components. First, we augment existing binary rewriting to support call path profiling; one can interactively view instrumentation costs and understand the calling contexts where the costs incur. Second, we present Versioned Structure Binary Editing, which is a general binary transformation technique. Third, we use call path profiles to guide the application of binary transformation. We apply our new techniques to shadow stack and basic block code coverage. Our instrumentation optimization workflow helps us identify several opportunities with regard to code transformation and instrumentation data layout. Our evaluation on SPEC CPU 2017 shows that the geometric overhead of shadow stack and block coverage is reduced from 7.6% and 161.3% to 1.4% and 4.0%, respectively. We also achieve promising results on Apache HTTP Server, where the shadow stack overhead is reduced from about 20% to 3.5%.

cs.CR↗

arXiv2017

Deriving Law-Abiding Instances

Liquid Haskell's refinement-reflection feature augments the Haskell language with theorem proving capabilities, allowing programmers to retrofit their existing code with proofs. But many of these proofs require routine, boilerplate code that is tedious to write. Moreover, many such proofs do not scale well, as the size of proof terms can grow superlinearly with the size of the datatypes involved in the proofs. We present a technique for programming with refinement reflection which solves this problem by leveraging datatype-generic programming. Our observation is that we can take any algebraic datatype, generate an equivalent representation type, and have Liquid Haskell automatically construct (and prove) an isomorphism between the original type and the representation type. This reduces many proofs down to easy theorems over simple algebraic "building block" types, allowing programmers to write generic proofs cheaply and cheerfully.

cs.PL↗