+ FPBench is a standard benchmark suite for the
+ floating-point community. The benchmark suite contains a common format
+ for floating-point computation and metadata and a common set
+ of accuracy measures:
+
+ FPCore is the format used for FPBench benchmarks. It is a simple
+ functional programming language with conditionals and
+ loops. The syntax is an easy-to-parse S-expression syntax.
+
+
+
+
+
+
+
+
+
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:
+
+
+
+
symbol
+
Any sequence of letters, digits, or characters from the
+ set ~!@$%^&*_-+=<>.?/: not starting with a digit,
+ implemented for ASCII by the regular expression:
+
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:
+
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]*
+
+
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:
+
+
+
+
Supported Mathematical Operations
+
+
+
+
-
*
/
fabs
+
+
fma
exp
exp2
expm1
log
+
+
log10
log2
log1p
pow
sqrt
+
+
cbrt
hypot
sin
cos
tan
+
+
asin
acos
atan
atan2
sinh
+
+
cosh
tanh
asinh
acosh
atanh
+
+
erf
erfc
tgamma
lgamma
ceil
+
+
floor
fmod
remainder
fmax
fmin
+
+
fdim
copysign
trunc
round
nearbyint
+
+
+
Supported Testing Operations
+
+
+
<
>
<=
>=
==
+
+
!=
and
or
not
isfinite
+
+
isinf
isnan
isnormal
signbit
+
+
+
+
+
+
+
+ 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 >.
+
+
+
+
+
Supported constants
+
+
The following constants are supported:
+
+
+
+
+
+
Supported Mathematical Constants
+
+
+
E
LOG2E
LOG10E
LN2
LN10
+
+
PI
PI_2
PI_4
1_PI
2_PI
+
+
2_SQRTPI
SQRT2
SQRT1_2
INFINITY
NAN
+
+
Supported Boolean Constants
+
+
+
TRUE
FALSE
+
+
+
+
+
+ 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 (usualy rounded to some
+ finite precision) or special
+ floating-point values such as infinities and NaN. Numerical operations are
+ treated as rounded real operations: they take extended real values as input
+ and return the corresponding extended real result, rounded according to the
+ rounding context. The behavior of rounding and the rounding context is
+ described in detail under rounding.
+
+
+
+ Operations that receive values of mixed or incorrect types, such
+ as (+ 1 TRUE), are illegal and the results of
+ evaluating them undefined. If tools do not support the rounding context
+ specified for a computation, the result is similarly undefined, and the
+ tool should give some indication for the reason of failure.
+
+
+
+
Function application
+
+ The semantics of function application are standard.
+
+
+
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, use nested
+ lets.
+
+
+
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:
+
+ In other words,
+ the list of bound variables gives
+ the variable's name,
+ its initial value,
+ and the value it is updated to after each iteration.
+ The loop is executed by
+ initializing all bound variables
+ and then
+ evaluating the condition
+ and simultaneously updating the variables
+ until the condition returns false.
+ Once the condition returns false,
+ the return expression is evaluated
+ and its value is returned.
+
+
+
+
+
+
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. All metadata properties in the current rounding context
+ are removed and replaced with the properties provided in the annotation.
+ See rounding.
+
+
+
+
+
+
+
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
+ are initially inherited from the overall properties of the FPCore
+ and can be updated for a subexpression by wrapping it with a
+ ! annotation, or for a program input by supplying an annotation on the argument.
+
+
+
+ Rounding contexts use lexical scoping. For example, in the expression
+
+
+
+
+
+ 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.
+
+
+
+
+
+ Number literals, mathematical constants, and program inputs
+ are also rounded according to the rounding context. Variables are not rounded
+ where they appear as values, but will usually hold rounded values, either from
+ the expressions where they are bound or from rounded program inputs.
+
+
+
+ FPCore does not restrict the behvior 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.
+
+
+
+ Similarly, 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, or symbolic representations of mathematical real numbers. This specification
+ uses mathematical reals as a universal way to describe the value of any representation,
+ but tools are not required to be able to represent arbitrary real numbers exactly.
+
+ FPBench is a standard benchmark suite for the
+ floating point community. The benchmark suite contains a common format
+ for floating-point computation and metadata and a common set
+ of accuracy measures:
+
+ FPBench standardizes several measures of accuracy; tools that measure
+ accuracy should state which of the FPBench accuracy measures they use, so
+ that the community can more easily compare tools.
+
+
+
+
+ FPBench analyses floating-point accuracy along several axes:
+ scaling vs non-scaling error, forward vs. backward error, and maximum vs.
+ average error. Tools that measure error may use sound vs. statistical
+ techniques, and tools that transform programs have several options for how to
+ measure accuracy improvement.
+
+
+
Scaling vs. non-scaling error (\(\varepsilon\))
+
+
+ There are several ways to measure the error of producing the inaccurate value
+ \(\hat x\) instead of the true value \(x\). Two common mathematical notions are
+ the absolute and relative error:
+
+
+
+
+ Relative error scales with the quantity being measured, and thus makes sense
+ for measuring both large and small numbers, much like the floating-point
+ format itself. A notion of error more closely tied to the floating-point
+ format is the Units in the Last Place (ULPs) difference.
+
+
+
+ Some tools instead use the logarithm of the ULPs, which approximately
+ describes the number of incorrect low-order bits in \(\hat x\). These two
+ measures are defined as:
+
+
+
+
+ The floating-point numbers are distributed roughly exponentially, so this
+ measure of error scales in a similar manner to relative error; however, it
+ is better-behaved in the presence of denormal numbers and infinities.
+
+
+
Forward vs. backward error (\(\epsilon\))
+
+
+ Forward error and backward error are two common measures for the error of a
+ mathematical computation. For a true function \(f\) and its
+ approximation \(\hat f\), forward error measures the difference between
+ outputs for a fixed input, while backward error measures the difference
+ between inputs for a fixed output. Formally:
+
+
+
+
+
+ Backward error is important for evaluating the stability of an algorithm, and
+ in scientific applications where multiple sources of error (algorithmic error
+ vs. sensor error) must be compared. Existing tools typically measure
+ forward error because backward error can be tricky to compute for
+ floating-point computations, where there may not be an input that produces
+ the true output.
+
+
Average vs. maximum error (\(E\))
+
+
+ Describing the error of a floating-point computation means summarizing its
+ behaviour across multiple inputs. Existing tools use either maximum or
+ average error for this task. Formally:
+
+
+
+
+
+ Worst-case error tends to be easier to measure soundly, while average error
+ tends to be easier to measure statistically.
+
+
+
Sound vs. statistical techniques
+
+
+ Running a floating-point program on all valid inputs is intractable. Existing
+ tools either soundly overapproximate the error using static analysis, or
+ approximate the error using statistical sampling.
+
+
+
+ Most static techniques are based on interval or affine arithmetic to
+ over-approximate floating-point arithmetic, often using abstract
+ interpretation. Abstract interpretation may use either non-relational or
+ relational abstract domains, and may use acceleration techniques (widenings)
+ to over-approximate loops without unrolling them. While such techniques tend
+ to provide loose over-approximations of the floating-point error of programs,
+ they are fast and provide sound error bounds. In some embedded applications,
+ correctness is critical and unsound techniques will not do.
+
+
+
+ In domains where correctness is not absolutely critical, sampling can provide
+ tight approximations of error. Many sampling techniques are used, including
+ naive random samples and Markov-chain Monte Carlo. These techniques involve
+ running a program multiple times, so they tend to be slower than static
+ analysis.
+
+
+
Measuring improvement (\(\iota\))
+
+
+ Tools that transform floating-point programs need to compare the
+ accuracy of two floating-point implementations of a function, the original
+ and the transformed. Several comparison measures are possible. Comparisons
+ can use the improvement in worst-case or average error between the original
+ \(\hat f\) and improved \(\hat f'\) implementation of the same mathematical
+ function \(f\):
+
+ However, one cannot usually improve the accuracy of a computation
+ simultaneously on all inputs. It is thus often necessary to make a
+ computation less accurate on some points to make it more accurate overall. In
+ this case, it may be useful to report the largest unimprovement, which
+ measures the cost of improving accuracy:
+
+ FPBench is a standard benchmark suite for the
+ floating point community. The benchmark suite contains a common format
+ for floating-point computation and metadata and a common set
+ of accuracy measures:
+
+ The metadata properties allow describing additional information
+ about each benchmark, such as their name, description,
+ precision, citations, or preconditions.
+
+
+
+
+
+ FPBench 1.1 defines the meaning of the following properties:
+
+
+
+
:name
+
+ A string name for the benchmark. If a name is needed and not
+ provided, we recommend using the body expression.
+
+
+
:description
+
+ A string description for the benchmark and its inputs. We
+ recommend describing the physical meaning and units of inputs
+ when applicable.
+
+
+
:cite
+
+ A list of symbols that describe the sources of the benchmark.
+ We recommend making available a BibTeX file which uses the
+ same symbols as keys.
+
+
+
:precision
+
+ Describes the floating-point precision used for rounding. It is expected
+ to be a symbol for one of the IEEE 754 names (such as binary32
+ and binary64) or one of the special values real or
+ integer. real precision indicates that no rounding
+ should take place, while integer precision specifies the behavior of
+ (unbounded) mathematical integers. If no :precision property is specified,
+ implementations should assume a sane default, such as binary64 or
+ possibly real depending on the application domain.
+
+
+
:round
+
+ The floating-point rounding mode used for rounding. Expected to be one of the IEEE 754 modes
+ nearestEven, nearestAway, toPositive,
+ toNegative, or toZero.
+
+
+
+
+
:pre
+
+ A precondition on inputs to the benchmark. Tools should not use
+ points that fail the precondition to determine the accuracy of the
+ benchmark. It is expected to be
+ an expression that
+ returns a boolean value. A rounding context can be given explicitly
+ for the expression, but if it is not, the default rounding context is assumed
+ to have real precision rather than the overall properties specified
+ for the FPCore.
+
+
+
:spec
+
+ A real-valued function approximated by the benchmark. If not provided,
+ then it is assumed to be the body of the benchmark. As with preconditions
+ specified with :pre, a rounding context can be provided explicitly,
+ but it is assumed to have real precision rather than the overall properties specified
+ for the FPCore.
+
+
+
:math-library
+
+ The library used in the source to implement floating-point
+ operations. It is expected to be a symbol identifying a library
+ implementation and version, such as gnu-libm-2.34.
+
+
+
+
+ Additionally, properties prefixed by the name of a tool (such
+ as :xxx-foobar) are reserved for definition by that
+ tool. Only that tool may define the meaning of those properties;
+ other tools should not depend on the meaning of those
+ properties, nor must the defining tool keep the meaning constant.
+
:cite (hamming-1987)
:pre (>= x 0)
(- (sqrt (+ x 1)) (sqrt x)))
-
An example FPCore program, from the hamming-ch3 suite.
+
An example FPCore benchmark, from the hamming-ch3 suite.
+
+
In this grammar, an FPCore term describes
a single benchmark, with a set of free variables, a collection of
@@ -286,13 +292,6 @@
Supported constants
Semantics
-
-
FPCore expressions can describe concrete floating-point
computations, abstract specifications of those computations, or
@@ -302,24 +301,28 @@
Semantics
Values in FPCore expressions are either boolean values or extended
- real numbers, which can be actual real numbers (usualy rounded to some
- finite precision) or special
- floating-point values such as infinities and NaN. Numerical operations are
- treated as rounded real operations: they take extended real values as input
- and return the corresponding extended real result, rounded according to the
- rounding context. The behavior of rounding and the rounding context is
- described in detail under rounding.
+ 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.
+
+
Operations that receive values of mixed or incorrect types, such
as (+ 1 TRUE), are illegal and the results of
- evaluating them undefined. If tools do not support the rounding context
- specified for a computation, the result is similarly undefined, and the
- tool should give some indication for the reason of failure.
+ evaluating them undefined.
-
+
Function application
The semantics of function application are standard.
@@ -340,10 +343,13 @@
Semantics
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, use nested
+ context. For sequentially binding variables, nest
lets.
+
while expressions
@@ -353,35 +359,25 @@
Semantics
While loops are evaluated according the equality:
-
- In other words,
- the list of bound variables gives
- the variable's name,
- its initial value,
- and the value it is updated to after each iteration.
- The loop is executed by
- initializing all bound variables
- and then
- evaluating the condition
- and simultaneously updating the variables
- until the condition returns false.
- Once the condition returns false,
- the return expression is evaluated
- and its value is returned.
+ 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.
-
cast expressions
@@ -397,7 +393,7 @@
Semantics
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.
+ from the parent context. See Rounding.
@@ -408,194 +404,95 @@
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
- are initially inherited from the overall properties of the FPCore
- benchmark and can be updated for a subexpression by wrapping it with a
- ! annotation, or for a program input by supplying an annotation on the argument.
+ 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.
- Rounding contexts use lexical scoping. For example, in the expression
+ 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).
-
-
(! :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.
+ Function applications round their results using the rounding context.
+ More precisely, a function application
+ (fe1 ...) 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:
- Number literals, mathematical constants, and program inputs
- are also rounded according to the rounding context. Variables are not rounded
- where they appear as values, but will usually hold rounded values, either from
- the expressions where they are bound or from rounded program inputs.
+ 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.
+ :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.
+
+
- Similarly, 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, or symbolic representations of mathematical real numbers. This specification
- uses mathematical reals as a universal way to describe the value of any representation,
- but tools are not required to be able to represent arbitrary real numbers exactly.
+ 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.
+ ! use lexical scoping. For example, in the expression
-
-
-
-
Examples
-
-
-
Rounding with cast
-
-
- The cast operation is necessary for explicitly rounding values
- without performing other numerical operations. Precision annotations specified
- with ! never cause any numerical operations to occur; they only
- change the rounding context.
-
-
-
- For example, the expression
-
-
-
-
(! :precision binary64 (! :precision binary32 x))
-
-
-
- will not round the value of the variable x. This expression is the
- same as simply specifying
-
-
-
-
x
-
-
-
- regardless of the rounding context. To round x, it is necessary
- to cast it in a context with the desired precision. The expression
-
- will round x to binary32 precision (here the outer
- annotation for binary64 precision is redundant, as it will be overwritten by the
- inner one), while the expression
-
- will round x twice, first to binary32 precision, and then from binary32
- to binary64 precision.
-
-
-
- Because numerical operations already round their outputs, it should not be necessary
- to cast in most cases, unless double rounding is specifically intended.
- For example, in an expression such as
-
-
-
-
(! :precision binary64
- (let ([ x (+ y 1)])
- x))
-
-
-
- the value stored in x will already be rounded to binary64 precision,
- as the addition is done in a context with that precision. Inserting an explicit
- cast around either the addition or the use of x would
- cause double rounding, and while in the case of binary64 precision
- this is a no-op, for other rounding contexts it could lead to undesirable behavior.
-
-
-
-
Inheriting properties in rounding contexts
-
-
- All properties not explicitly specified in a ! precision annotation
- are inherited from the parent context. For the top level expression in an
- FPCore benchmark, the parent context includes all the overall properties of the benchmark.
-
- the sin operation will take place in a context with name
- "foo", math-librarygnu-libm-2.34, spec 0, and
- binary64 precision. Even properties that are seemingly unrelated to
- rounding, such as the name of the benchmark, are inherited. The FPCore standard does
- not prohibit tools from implementing rounding functions that depend on these properties,
- or other tool-specific properties, although having a rounding function that depends on
- name is not advised.
-
-
-
- Properties in the rounding context might come from multiple different annotations. For example,
- in the expression
-
(! :precision binary64 :round nearestEven
+ (let ([ y (! :precision binary32 (- x 1))])
+ (+ y 1)))))
+
-
- the addition will take place as expected in a context with binary32 precision,
- toZero rounding direction, and the gnu-libm-2.34 math library. This
- can be useful if some, but not all, of the properties are shared by multiple subexpressions.
- For example, in the expression
-
+
+ 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.
+
-
-
(! :precision binary64 (- (! :round toPositive (+ x y)) (! :round toNegative (+ x y))))
-
+
+ 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.
+
-
- all of the operations will take place in a context with binary64 precision, but the additions
- will use different rounding directions.
-
overall FPCore benchmark and are updated with
! annotations. Program inputs can also be annotated
to describe the precision of the input.
- ! use lexical scoping. For example, in the expression
+ ! annotations use lexical scoping. For example, in the expression