CakeML / CakeML/cakeml

Automatically producing fast smallnum functions

Open
#367 0 comments 0 reactions 0 assignees View on GitHub
enhancement medium effort medium reward student project
Dominant language
Standard ML
Stars
1.2k
Forks
104
Avg merge
2d 21h
Merged PRs (30d)
16

Description

The CakeML source language has arbitrary precision integers as the
main integer type. These are implemented dynamically as either
smallnums or bignums. A smallnum is used in case the value fits within
a tagged machine word (32-bit or 64-bit depending on target
architecture). The bignum representation is only used when the value
doesn't fit a smallnum. A bignum is represented as a pointer to a
vector of machine words on the heap containning the large number.

The consquence of this generality is that each arithmetic operation
has to check whether it has a smallnum (unboxed value) or a bignum
(pointer). The checking code is tuned to be very fast. However, it
still comes at a cost -- not least in that the each bignum operation
is a call to a library routine for doing the bignum operation. The
prescence of such subroutine calls, even if they are seldomly used,
disrupt the register allocation around each arithmetic operation.

This issue is about adding a new compiler optimisation that notices
when a recursive function will from this point onwards have a smallnum
only in one or more of its arguments and then jump to code that is
optimised under this assumption.

**Example:**

The following function is a typical function used in the bootstrapped
CakeML compiler implementation. Optimising such functions might
improve the speed of the compiler itself.

The original function is:

genlist f n aux =
if n = 0 then aux else
let n = n - 1 in genlist n (f n :: aux)

This would be transformed into two functions:

genlist f n aux =
if is_small_num n /\ 0 <= n then genlist' f n aux else
if n = 0 then aux else
let n = n - 1 in genlist n (f n :: aux)

genlist' f n aux =
if n = 0 then aux else
let n = smallnum_minus n 1 in genlist' n (f n :: aux)

**General case:**

In general the optimisation should look for numbers that can only get
smaller in a loop. If it finds such, then it makes a copy of the
function and replaces all arithmetic operations that operate on the
smallnum by smallnum versions.

Since this optimisation duplicates code, it must be possibly for the
user of the compiler to control when it is applied. The simplest thing
would be to have an on-off switch, but there could be more
fine-grained controls too.

**MSc project:**

This issue is suitable as a MSc project on compiler verification. This
optimisation would most naturally fit around the BVI intermediate
language.

Contributor guide

No contributing guide indexed for this repository

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.