Writing a Herbie Platform

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.

Platform Concepts

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.

Defining a Platform

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.

Defining Representations

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.

Defining Operations

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.

Defining Multiple Operations

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 /.

Common Kinds of Operations

This section lists common kinds of operations and notes things you should keep in mind when defining them.

Math Library Functions

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.

Numeric Variations

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!

Conversions

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.

Comparisons

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

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.

Constants

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.

Negation

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.

Precision-specific Variations

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.

Hard-to-emulate Operations

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.