OCaml relies on a type-agnostic object representation centred around values which unify odd integers and aligned pointers. The last bit of a value distinguishes the two variants: zero indicates a pointer on the OCaml heap, while one encodes a tagged integer $n$ as $2n+1$. While this approach provides significant benefits, enabling a powerful foreign-function interface (FFI) and allowing the garbage collector to easily traverse the heap, a significant runtime overhead is also incurred. An operation as simple as the addition of $n$ and $m$ requires two hardware instructions: one to add the two odd numbers forming $2(n+m)+2$, followed by another to decrement the result and adjust the tag bit, yielding $2(n+m)+1$. In many instances, particularly in the standard library, sequences of such instructions present redundancies that are not properly eliminated by the compiler, despite obvious benefits to both execution time and binary size. In this talk, we discuss a type analysis implemented in the \textit{Duplo} post-link optimiser that narrows the classification of registers from storing values to regular integers, enabling a variety of simple and effective transformations. Although we show improvements on benchmarks quantifying the performance of the standard library, we also highlight the shortcomings of such an analysis on a low-level representation, arguing for it to be implemented on a higher-level representation in the compiler.
Slides (2n+1 to n.pdf) | 194KiB |
Sat 28 AugDisplayed time zone: Seoul change
01:30 - 03:00 | |||
01:30 30mTalk | From 2n+1 to n OCaml File Attached | ||
02:00 20mTalk | Property-Based Testing for OCaml through Coq OCaml Paaras Bhandari University of Maryland, College Park, Leonidas Lampropoulos University of Maryland, College Park | ||
02:20 20mTalk | Safe Protocol Updates via Propositional Logic OCaml Michael O'Connor Jane Street |