ICFP 2021
Sun 22 - Sat 28 August 2021
Sat 28 Aug 2021 01:30 - 02:00 at OCaml - Session 5 Chair(s): Ashish Agarwal

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 Aug

Displayed time zone: Seoul change

01:30 - 03:00
Session 5OCaml at OCaml
Chair(s): Ashish Agarwal
01:30
30m
Talk
From 2n+1 to n
OCaml
Nandor Licker University of Cambridge, Timothy M. Jones University of Cambridge, UK
File Attached
02:00
20m
Talk
Property-Based Testing for OCaml through Coq
OCaml
Paaras Bhandari University of Maryland, College Park, Leonidas Lampropoulos University of Maryland, College Park
02:20
20m
Talk
Safe Protocol Updates via Propositional Logic
OCaml
Michael O'Connor Jane Street