Platforms define Herbie compilation targets. A platform might be specific to a programming language, to a math library, or to a hardware ISA. Writing a custom platforms can help Herbie produce faster and more accurate programs.
Herbie operates on mathematical specifications and floating-point expressions.
Specifications are built from rational numbers,
variables, and functions like +
,
sin
, <
, and if
. A
specification has a type, which is
either real
or bool
.
Types, functions, and specifications have floating-point analogs.
Representations are the floating-point analogs of
types, and Herbie comes with three built in:
<binary32>
and <binary64>
are
reprentations of real
and correspond to single- and
double-precision IEEE-754 arithmetic. There's also
a <bool>
representation for booleans. It's
possible to define new representations, described
on another page.
Operations are the floating-point analog of functions
and represent the actual floating-point operation the compilation
target can perform. There are typically several operations for each
supported function; for example, in the C standard library
provides
cosf
and cos
, both of which correspond to
the cos
function but for different representations
(<binary32>
and <binary64>
).
Expressions are the floating-point analog of specifications and represent target-specific floating-point computations. Platforms, to put it simply, just define the set of representations and operations that expressions are allowed to use. Herbie then searches for a fast and accurate expression that corresponds to the user's input specification.
Each representation, operation, and thus expression has a
cost, which is a non-negative real number. Generally, the
cost of a representation is the time it takes to read a value of
that representation from memory and the cost of an operation is the
time it takes to execute that operation. However, in principle,
platforms can use cost to represent another metric like area or
latency. Only relative costs matter. If you're not sure, just
putting "1
" for all the costs is not a bad place to
start.
A platform definition is a text file that starts with:
#lang herbie/platform
Herbie can then be informed to use this platform by passing
the --platform path/to/file
command-line
argument.
The file contains Racket
code. That code can define the platform's representations and
operations using define-representation
and define-operation
. It can also define variables and
helper functions, import external packages, or anything else Racket
can do. If necessary, it can define new representations.
Herbie's built-in
platforms are good example platforms to study or modify. If you
use them as an example, you'll need to change the #lang
line at the top of the file to be herbie/platforms
; the
built-in platforms are different because they are built in to Herbie
and can't assume Herbie is installed.
The typical platform starts by defining the representations it
uses and their costs with define-representation
:
(define-representation <bool> #:cost 1) (define-representation <binary64> #:cost 1.5)
This cost is the cost for reading a variable or literal of that
representation. Note that platforms must explicitly define a cost
for the <bool>
representation if it uses
booleans. If the platform forgets to define a representation that it
uses, Herbie will produce an error when loading the platform.
If the same cost is used repeatedly, it can be convenient to define a variable:
(define cost 1) (define-representation <bool> #:cost cost)
After defining the representations it uses, a platform then defines all the operations it supports.
An operation is defined by four fields:
The define-operation
construct requires exactly
these four fields:
(define-operation (recip [x <binary32>]) <binary32> #:spec (/ 1 x) #:impl (lambda (x) ...) #:cost 3)
The first line gives the operation's signature: it is
named recip
, it has one single-precision
input x
, and it outputs a single-precision float.
The #:spec
field gives this operation's
specification as (/ 1 x)
, one divided
by x
. In other words, this operation computes a
number's reciprocal.
The #:impl
field gives this operation's
implementation, as a Racket function (defined
with lambda
). An operation's implementation is a Racket
function with as many arguments as the operation. It is called with
concrete inputs in the corresponding input representations, and must
return an output in the output representation. It can be defined
using a lambda
, a define
block, or any
other function-defining Racket construct.
When an implementation function is called,
<binary64>
and <binary32>
arguments are passed as Racket
flonums,
while <bool>
arguments are passed as Racket
booleans.
Single-precision numbers aren't a separate type in Racket. instead,
you create them from double-precision floats by
calling flsingle
.
For this example, to compute a 32-bit reciprocal for a 32-bit
input, one could use (flsingle (/ 1.0 x))
for the body
of the lambda
.
The #:cost
field gives this operation's cost, 3.
Realistic platform usually have a lot of similar operations:
addition, subtraction, multiplication, and division, or sine,
cosine, tangent, and so on. The define-operations
construct defines multiple operations at a time, as long as they
have the same input and output representations:
(define-operations ([x <binary64>] [y <binary64>]) <binary64> [+ #:spec (+ x y) #:impl + #:cost 0.200] [- #:spec (- x y) #:impl - #:cost 0.200] [* #:spec (* x y) #:impl * #:cost 0.250] [/ #:spec (/ x y) #:impl / #:cost 0.350])
This block defines four functions, each with their own name,
specification, implementation, and cost. Note that in this case
the #:impl
column refers to the Racket
functions +
, -
, *
,
and /
.
This section lists common kinds of operations and notes things you should keep in mind when defining them.
Most operating systems have a standard libm
library
that provides elementary functions like cos
. You can
use Herbie's from-libm
helper to load implementations
from libm
:
(define-operation (fabs.f32 [x <binary32>]) <binary32> #:spec (fabs x) #:impl (from-libm 'fabsf) #:cost 0.125)
The from-libm
uses dynamic linking to
load libm
, extracts the symbol passed
to from-libm
, and then uses the operation's signature
to call into the dynamically-linked library from Racket. Must make
sure to pass the correct symbol name; for single-precision
functions, make sure to add the "f
" suffix.
Some platforms provide numeric variations like log1p
or cosd
for common functions. You can define operations
for them using complex specifications:
(define-operation (cosd [x <binary64>]) <binary64> #:spec (cos (* x (/ (PI) 180))) #:impl (lambda (x) ...) #:cost 4)
The #:spec
in this example explains to Herbie
that cosd
is the cosine of x
in degrees.
Herbie will then use cosd
when that improves
accuracy.
Other common numeric variations
include fma
, log1p
, expm1
,
and hypot
. If they're available on your target,
we strongly recommend defining operations for them; they
often improve accuracy by quite a bit!
A conversion or cast operation uses mixed representations:
(define-operation (64->32 [x <binary64>]) <binary32> #:spec x #:impl flsingle #:cost 1)
This operation has a 64-bit input and a 32-bit output. Its
specification is just x
, which means it doesn't
actually do anything mathematically. The implementation is the
standard Racket flsingle
function (which converts from
double- to single-precision) and it has a cost of 1.
Herbie will use this conversion operation for casting between the two types.
Comparison operations return <bool>
:
(define-operations ([x <binary64>] [y <binary64>])[==.f64 #:spec (== x y) #:impl = #:cost 1] [!=.f64 #:spec (!= x y) #:impl (negate =) #:cost 1] [<.f64 #:spec (< x y) #:impl < #:cost 1] [>.f64 #:spec (> x y) #:impl > #:cost 1] [<=.f64 #:spec (<= x y) #:impl <= #:cost 1] [>=.f64 #:spec (>= x y) #:impl >= #:cost 1])
Here, negate
is
a Racket
function that negates a comparison function.
A platform only needs to provide the comparison functions
available on the target. However, Herbie's "regimes" pass uses
the <=
operation, so it's best to provide one if one
is available.
A platform that uses both representation needs to define
separate <binary32>
and <binary64>
comparison operations. They can
have different costs.
Conditionals can be defined as operations with a boolean argument:
(define-operation (if-f64 [c] [t <binary64>] [f <binary64>]) <binary64> #:spec (if c t f) #:impl if-impl #:cost (if-cost 14) )
Here if-impl
is a Herbie-provided Racket function
that wraps a standard if
statement, while
the if
inside the #:spec
is how
specifications refer to mathematical conditional expressions.
Conditional operations usually pass a procedure to
#:cost
. The helper if-cost
returns a procedure
that receives the costs of the arguments and combines them into a
total cost. It computes the cost of evaluating the condition plus the
larger of the two branch costs. In this example we add a constant cost
of 14 to that value.
A platform needs to define both <binary32>
and <binary64>
conditional operations if it uses
both representations. They can have different costs. There's
typically no need to define conditional operations
for <bool>
as Herbie does not rewrite boolean
expressions.
Mathematical constants like E
and PI
are considered operations in Herbie; they just have no inputs. For
example, to define a 64-bit inverse-π constant, write:
(define-operation (INVPI) <binary64> #:spec (/ 1 (PI)) #:impl (lambda () ...) #:fpcore PI #:cost 0.5)
Note the parentheses in various fields. The
name INVPI
has parentheses around it like all operation
signatures; it just doesn't have any arguments after the name. In
the #:spec
, the PI
constant is also
wrapped in parentheses because it is also treated as a zero-argument
function. And in the #:impl
, the implementation is
given by a Racket function of no arguments. You can also use
the Racket const
function to construct these no-argument functions.
But in the #:fpcore
field the PI
value
doesn't use parentheses, because FPCore treats constants as
constants, not zero-argument functions.
Constants can be defined in any precision. If you want the same constant to be available in multiple precisions, you have to define multiple constant operations.
Herbie's specification language has a negation function, and it's usually a good idea to define a negation operation if your target has one. Define it like this:
(define-operation (neg.f32 [x <binary64>]) <binary64> #:spec (neg x) #:impl - #:fpcore (- x) #:cost 0.125)
Here, in the #:spec
, (neg x)
refers to
the negation function in Herbie's specification language, while
the -
symbol after #:impl
refers to
Racket's subtraction function, which also acts as a negation
function.
There is also an #:fpcore
field. This field tells
Herbie how to represent this operation in FPCore (for user input and
output). The default #:fpcore
is the operation's
#:spec
but there are a few functions (like negation)
where Herbie's specification language uses a different syntax from
FPCore and #:fpcore
needs to be specified manually.
If a platform supports both <binary32>
and <binary64>
, they often support similar
operations:
(define-operations ([x <binary32>]) <binary32> #:fpcore (! :precision binary32 _) [fabs.f32 #:spec (fabs x) #:impl (from-libm 'fabsf) #:cost 0.125] [sin.f32 #:spec (sin x) #:impl (from-libm 'sinf) #:cost 4.250] ...) (define-operations ([x <binary64>]) <binary64> #:fpcore (! :precision binary64 _) [fabs.f64 #:spec (fabs x) #:impl (from-libm 'fabs) #:cost 0.125] [sin.f64 #:spec (sin x) #:impl (from-libm 'sin) #:cost 4.200] ...)
Here, two define-operations
blocks define two sets
of functions with different signatures but identical specifications.
To disambiguate these functions in FPCore output,
the #:fpcore
argument to define-operations
defines different FPCore properties for
each set of operations. In that argument, the underscore is replaced
by each operation's #:spec
.
Sometimes a platform will offer an operation that's difficult to
implement accurately. In this case, Herbie's from-rival
helper can provide a slow but correctly-rounded implementation:
(define-opertion (dotprod [a <binary64>] [b <binary64>] [c <binary64>] [d <binary64>]) <binary64> #:spec (+ (* a b) (* c d)) #:impl (from-rival) #:cost 1.25)
The from-rival
helper uses
the MPFR library to evaluate the
operation's specification. Compilation is usually much
slower than with a native floating-point implementation, but for
unusual operations that are difficult to implement otherwise, it can
still allow compilation to proceed.
Note that from-rival
implementations are always
"correctly-rounded", meaning as accurate as possible. Most targets
don't actually offer correctly-rounded operations, which can mean
that Herbie's outputs won't be as accurate as Herbie assumes. It's
always better to execute the actual operation on the actual target
if possible, so as to precisely emulate its actual behavior.