Syntax

Benchmarks use a simple S-expression syntax with the following grammar.

In this grammar, an FPCore term describes a single benchmark, with a set of free variables, a collection of metadata properties, and the floating-point expression defining the benchmark. White-space is ignored, and lines starting with the semicolon (;) are treated as comments and ignored. The basic tokens are defined as expected:

rational

An optional plus (+) or minus (-) sign, followed by a sequence of decimal digits that form the numerator, followed by a slash (/), followed by a nonzero sequence of decimal digits that form the denominator. This definition is implemented for ASCII by the regular expression:

[+-]?[0-9]+/[0-9]*[1-9][0-9]*

Every other kind of numeric literal only expresses rational numbers, so every other type of numeric literal can be considered syntax sugar for rational numbers.

decnum

An optional plus (+) or minus (-) sign followed by either a sequence of decimal digits which may optionally be followed by a period (.) and another sequence of digits, or by a period and a sequence of digits. This may be followed by an e, an optional plus or minus sign, and a final sequence of digits. This definition is implemented for ASCII by the regular expression:

[-+]?([0-9]+(\.[0-9]+)?|\.[0-9]+)(e[-+]?[0-9]+)?

hexnum

An optional plus (+) or minus (-) sign, followed by the hexadecimal literal identifier 0x, all followed by either a sequence of hexadecimal digits ([0-9a-f]) which may optionally be followed by a period (.) and another sequence of hex digits, or by a period and a sequence of hex digits. This may be followed by a p, an optional plus or minus sign, and a sequence of decimal digits. This definition is implemented for ASCII by the following regular expression, which is case-insensitive:

[+-]?0x([0-9a-f]+(\.[0-9a-f]+)?|\.[0-9a-f]+)(p[-+]?[0-9]+)?

symbol

Any sequence of letters, digits, or characters from the set ~!@$%^&*_-+=<>.?/: not starting with a digit and not matching any other basic token. In ASCII, all symbols match by this regular expression:

[a-zA-Z~!@$%^&*_\-+=<>.?/:][a-zA-Z0-9~!@$%^&*_\-+=<>.?/:]*

string

Any sequence of printable characters, spaces, tabs, or carriage returns, delimited by double quotes ("). Within the double quotes, backslashes (\) have special meaning. A backslash followed by a double quote represents a double quote and does not terminate the string; a backslash followed by a backslash represents a backslash; other escapes may also be supported by implementations, but their meaning is not defined in this standard. We recommend that implementations only use escapes defined in the C or Matlab standard libraries. This definition is implemented for ASCII by the regular expression:

"([\x20-\x21\x23-\x5b\x5d-\x7e]|\\["\\])*"

Supported operations

The following operations are supported:

All operations have the same signature as the equivalent operations in C11. The arithmetic functions are all binary operators, except that unary - represents negation. The comparison operators and boolean and and or allow an arbitrary number of arguments.

A comparison operator with more than two operators is interpreted as the conjuction of all ordered pairs of arguments. In other words, == tests that all its arguments are equal; != tests that all its arguments are distinct; and <, >, <=, and >= test that their arguments are sorted (in the appropriate order), with equal elements allowed for <= and >=, and disallowed for < and >.

Tensor operations do not perform any mathematical calculation; they only manipulate the N-dimensional array data structure of a tensor. For a tensor A, (dim A) returns the number of dimensions of A as an integer, (size A 0) returns the length of the first dimension of A as an integer, and (ref A 1 3) returns the element of A at position (1, 3) - i.e. the second element in the first dimesion, and the fourth in the second dimension.

Supported constants

The following constants are supported:

The floating-point constants are defined just like their analogs in GNU libc. All constants must evaluate to a value as close as possible to their mathematically-accurate real value, according to the rounding context.

Semantics

FPCore expressions can describe concrete floating-point computations, abstract specifications of those computations, or intermediates between the two. The semantics of FPCore are correspondingly flexible, and are made explicit by the rounding context.

Values in FPCore expressions are either boolean values or extended real numbers, which can be actual real numbers (usually rounded to some finite precision) or special floating-point values such as infinities and NaN. Numerical operations take extended real values as input and return the corresponding extended real result, rounded according to a rounding context. The behavior of rounding and the rounding context is described in detail under Rounding.

Values can be stored in N-dimensional arrays, or tensors. Tensors are created by array and tensor expressions and accessed by the special dim, size, and ref operations; numerical operations are restricted to scalar values. More information about tensors is provided under Data Structures.

Operations that receive values of mixed or incorrect types, such as (+ 1 TRUE) or (ref PI 5), are illegal and the results of evaluating them undefined.

Function application

The semantics of function application are standard.

If an FPCore is given an identifier before its list of inputs, then it can be used as a function in other FPCores.

if expressions

An if expression evaluates the conditional to a boolean and then returns the result of the first branch if the conditional is true or the second branch if the conditional is false.

let expressions

Bindings in a let expression are evaluated simultaneously, as in a simultaneous substitution. Thus, (let ([a b] [b a]) (- a b)) is the same as (- b a) and (let ([a 1] [b a]) b) is illegal unless a is available in the context. For sequentially binding variables, nest lets, or use sequentially binding form let*.

while expressions

A while loop contains a conditional, a list of bound variables, and a return expression. Both the conditional and the return expression may refer to the bound variables. While loops are evaluated according the equality:

(while cond ([x init update] ...) retexpr)
(let ([x init] ...)
  (if cond
    (while cond ([x update update] ...) retexpr)
    retexpr)

In other words, the list of bound variables gives the variable's name, its initial value, and the expression by which it is updated to after each iteration. The loop initializes all bound variables; evaluates the condition; if true, simultaneously updates the variables with the update expression and repeats; if false, the return expression is evaluated and its value is returned.

for expressions

A for loop is similar to a while loop, but instead of a conditional, the loop is run for a predetermined integer number of steps. for loops with a single index variable can be converted to while loops according to the equality:

(for ([i n]) ([x init update] ...) retexpr)
(while (< i n)
  ([i 0 (+ i 1)]
   [x init update] ...)
  retexpr)

If multiple index variables are provided, then they are iterated in a nested fashion, with the last variable being the innermost loop.

cast expressions

A cast performs explicit rounding according to the rounding context. If the context specifies real precision, it is guaranteed to be a no-op.

! annotations

A ! annotation updates the rounding context for a subexpression. Properties specified in the annotation are set to the provided values, and all other properties are inherited from the parent context. See Rounding.

digits

The digits constructor allows exact numbers to be specified in any floating-point radix as a triple of significand (or mantissa), exponent, and base. (digits m e b) represents exactly the value m ✕ b^e. m, e, and b are integers, with b ≥ 2. The sign of the value is determined by the sign of m.

let*, while*, and for*

let* expressions are sequentially binding variants of let familiar from most lisp dialects. Rather than being evaluated simultaneously, the bindings are evaluated in order, so that (let* ([a b] [b a]) (- a b)) is the same as (- b b) and (let* ([a 1] [b a])b) is the same as 1.

The initializations and updates in the body of a while* loop, and in the body (but not the index variables) of a for* loop, are performed sequentially in an analogous way.

let* expressions can be desugared into nested let expressions by the following rule:

(let* ([var value] rest ...) body)
(let ([var value])
  (let* (rest ...) body))

Similarly, while* loops can be desugared into regular, simultaneously-binding while and let* expressions (which can be further desugared into lets):

(while* cond ([x x-init x-update] [y y-init y-update] ...) retexpr)
(while cond
  ([x
    (let* ([x x-init] [y y-init] ...) x))
    (let* ([x x-update] [y y-update] ...) x))]
   [y
    (let* ([x x-init] [y y-init] ...) y))
    (let* ([x x-update] [y y-update] ...) y))]
   ...)
  retexpr)

Alternatively, a while* loop can be given semantics directly in terms of let*, according to the equality:

(while* cond ([x init update] ...) retexpr)
(let* ([x init] ...)
  (if cond
    (while* cond ([x update update] ...) retexpr)
    retexpr)

Like for loops, for* loops with a single index variable can be desugared into while* loops:

(for* ([i n]) ([x init update] ...) retexpr)
(while* (< i n)
  ([x init update]
   ...
   [i 0 (+ i 1)])
  retexpr)

Note that the index variable update is moved after the other updates in the loop body. As with for loops, multiple index variables are iterated in a nested fashion, with the last variable being the innermost loop.

Data Structures

FPBench provides support for structured data in N-dimensional arrays, or "tensors."

array literals

Literal arrays behave like lists in most lisp dialects, but they cannot be extended or modified once created. array constructs an array from its arguments; arrays can be nested to form higher-dimensional data structures.

tensor expressions

tensor constructs an array dynamically, by tabulating over a set of indices in the same way as a for loop. The body expression is evaluated independently for each element in the array, so there is no interdependence between the values of the elements.

tensor* expressions

Like tensor, tensor* constructs an array dynamically, but it enforces the same iteration order as a for* loop and allows dependence between the computed values of the elements.

In addition to the index variables, tensor* allows for loop updates and inits to be specified; these updates are performed as for a for* loop and the values are available to the element body expression in the same way as the values of the index variables.

Rounding

FPCore allows the precision of program inputs, constants, and operations to be controlled via a rounding context. The context consists of a set of metadata properties, which affect how function application, casts, and constants are rounded.

Number literals, mathematical constants, and program inputs are rounded according to the rounding context. Variables, however, are not rounded where they appear as values (since they hold rounded values, either from the expressions where they are bound or from rounded program inputs).

Function applications round their results using the rounding context. More precisely, a function application (f e1 ...) in a rounding context ρ must evaluate to the same value as if f were evaluated in exact real arithmetic, and then rounded according to the rounding context. Formally:

    vi = ⟦ei⟧ρ 
 ⟦ (f ei ...) ⟧ρ = round( ρ, ⟦f⟧(vi , ... ) )
  

Casts behave identically to applying the identity function (and then rounding the result).

FPCore does not restrict the behavior of the rounding function or the set of metadata properties that its behavior depends on. Some common precision and rounding direction properties are described for the metadata properties :precision and :round. Tools are not required to support all of these rounding behaviors, and are allowed to introduce new ones and new metadata properties to control them.

Rounding contexts are initialized with the properties of the overall FPCore benchmark and are updated with ! annotations. Program inputs can also be annotated to describe the precision of the input. ! annotations use lexical scoping. For example, in the expression

(! :precision binary64 :round nearestEven
  (let ([ y (! :precision binary32 (- x 1))])
    (+ y 1)))))

the subtraction will take place in a context with binary32 precision, but the addition will take place in a context that has inherited binary64 precision from the annotation enclosing the entire let. Both operations will take place in a context that has inherited nearestEven rounding behavior. The examples contain more details.

If tools do not support the rounding context specified for a computation, the result is undefined, and the tool should give some indication of the reason for the failure. FPCore does not restrict the representation used internally by a tool to store values. Numeric values can be floating-point values of various precisions, fixed-point values, intervals, or any sort of symbolic representations of mathematical real numbers. Though FPCore can represent exact real computations, tools are not required to be able to represent arbitrary real numbers exactly.