diff --git a/Dockerfile b/Dockerfile index 67990041d..da21b5be4 100644 --- a/Dockerfile +++ b/Dockerfile @@ -6,7 +6,7 @@ # Builds output under /herbie/egg-herbie FROM rust:1.61.0 as egg-herbie-builder WORKDIR /herbie -COPY . . +COPY egg-herbie egg-herbie RUN cargo build --release --manifest-path=egg-herbie/Cargo.toml # Production image @@ -14,7 +14,7 @@ FROM racket/racket:8.5-full AS production MAINTAINER Pavel Panchekha COPY --from=egg-herbie-builder /herbie/egg-herbie /src/egg-herbie RUN raco pkg install /src/egg-herbie -ADD src /src/herbie +COPY src /src/herbie RUN raco pkg install --auto /src/herbie ENTRYPOINT ["racket", "/src/herbie/herbie.rkt"] EXPOSE 80 diff --git a/egg-herbie/info.rkt b/egg-herbie/info.rkt index dea737d66..b1b7cd472 100644 --- a/egg-herbie/info.rkt +++ b/egg-herbie/info.rkt @@ -1,9 +1,11 @@ #lang info (define collection "egg-herbie") -(define version "1.5") +(define version "1.6") (define pkg-desc "Racket bindings for simplifying math expressions using egg") - (define pkg-authors `("Oliver Flatt")) + +(define build-deps + '("rackunit-lib")) diff --git a/src/config.rkt b/src/config.rkt index 1799ffb01..90e3f7698 100644 --- a/src/config.rkt +++ b/src/config.rkt @@ -108,7 +108,7 @@ (if (equal? out "") default out)) default)) -(define *herbie-version* "1.5") +(define *herbie-version* "1.6") (define *hostname* (run-command "hostname")) diff --git a/src/info.rkt b/src/info.rkt index b9aa98143..681de5aee 100644 --- a/src/info.rkt +++ b/src/info.rkt @@ -1,7 +1,7 @@ #lang info (define collection "herbie") -(define version "1.5") +(define version "1.6") ;; Packaging information @@ -23,13 +23,14 @@ ;; Dependencies (define deps - '(("base" #:version "7.0") + '(("base" #:version "8.0") "math-lib" "plot-lib" "profile-lib" "rackunit-lib" "web-server-lib" - ("egg-herbie" #:version "1.5") + "draw-lib" + ("egg-herbie" #:version "1.6") ("rival" #:version "1.4") ("fpbench" #:version "2.0.3"))) diff --git a/src/syntax/read.rkt b/src/syntax/read.rkt index 2a7da1a6e..630fdff1e 100644 --- a/src/syntax/read.rkt +++ b/src/syntax/read.rkt @@ -113,6 +113,7 @@ (unless (set=? vars used) (define unused (set-subtract vars used)) (warn 'unused-variable + #:url "faq.html#unused-variable" "unused ~a ~a" (if (equal? (set-count unused) 1) "variable" "variables") (string-join (map ~a unused) ", ")))) @@ -120,6 +121,7 @@ (for* ([var vars] [const (all-constants)]) (when (string-ci=? (symbol->string var) (symbol->string const)) (warn 'strange-variable + #:url "faq.html#strange-variable" "unusual variable ~a; did you mean ~a?" var const)))) (define (our-read-syntax port name) diff --git a/www/doc/1.6/faq.html b/www/doc/1.6/faq.html index 135547fa1..ebfb63fbc 100644 --- a/www/doc/1.6/faq.html +++ b/www/doc/1.6/faq.html @@ -111,6 +111,19 @@

Unsound rule application detected

failed to simplify the output.

+

Unused variable var

+ +

+ The input FPCore contains a variable that is not + used in the body expression. +

+ +

Strange variable var

+ +

+ The input expression contains a variable that is similar in name + to named constants, e.g. e instead of E. +

Known bugs

diff --git a/www/doc/1.7/diagrams.html b/www/doc/1.7/diagrams.html new file mode 100644 index 000000000..e3731df4d --- /dev/null +++ b/www/doc/1.7/diagrams.html @@ -0,0 +1,34 @@ + + + + + Diagrams + + + + + +
+ +

Diagrams

+
+ +
+ System diagram of Herbie +
+ +

+ High-level system diagram of Herbie. It highlights Herbie's core architecture, + external libraries, and user interactions. + Basic flow: Herbie passes user input (expression, precondition, etc.) to the + mainloop (scheduler) which alternates between generate and test phases multiple times, + maintaining and improving a set of accurate expressions at each iteration. + Once the generate-and-test phase is complete, Herbie extracts either + one or many output expressions using an algorithm called regime inference. + Regime inference chooses the "best" (usually most accurate) + generated candidate expression or combines multple candidates, + each "best" on a smaller part of the input range, with a branch condition. +

+ + + diff --git a/www/doc/1.7/docker.html b/www/doc/1.7/docker.html new file mode 100644 index 000000000..d71f3eb65 --- /dev/null +++ b/www/doc/1.7/docker.html @@ -0,0 +1,135 @@ + + + + + Herbie on Docker + + + + + +
+ +

Installing with Docker

+
+ +

+ Herbie is available + through Docker, which is + sort of like a virtual machine. This page describes how to install + the official Docker + image for Herbie. +

+ +

+ Herbie can also be installed from + package or source. Herbie via Docker is only recommended if + you already have Docker experience. +

+ +

Installing Herbie via Docker

+ +

+ First, install + Docker. Docker supports Windows, macOS, and Linux. Depending + on how you install Docker, you may need to prefix + the docker commands with sudo or run them + as the administrative user. +

+ +

With Docker installed, you can run the Herbie shell with:

+ +
docker run -it uwplse/herbie shell
+ +

This will read input from the standard input.

+ +

Note that Herbie in Docker is more limited; for example, it will + not recognize plugins installed outside the Docker container.

+ +

Running the web interface

+ +

+ You can run the Herbie web server locally with + +

docker run -it --rm -p 8000:80 uwplse/herbie
+ + and access the server at http://localhost:8000. +

+

+ (Herbie's Docker image binds to port 80 by + default; this command uses the -p <hostport>:80 option to expose Herbie on port 8000.) +

+ +

+ If you are using the --log + or --save-session flags for the web shell, + you will also need to mount the relevant directories into the + Docker container using the -v Docker option, as in + the examples below. +

+ +

Generating files and reports

+ +

+ To use Herbie in batch mode, you will + need to mount the input in the Docker container. Do that with: +

+ +
docker run -it --rm \
+    -v in-dir:/in \
+    -v out-dir:/out \
+    -u $USER \
+    uwplse/herbie improve /in/in-file /out/out-file
+ +

+ In this command, you are asking Herbie to read input + from in-file in in-dir, and write output + to out-file in out-dir. The command looks + the same if you want Herbie to read input from a directory; + just leave in-file blank. +

+ +

+ To generate reports from Herbie, you can run: +

+ +
docker run -it --rm \
+    -v in-dir:/in \
+    -v out-dir:/out \
+    -u $USER \
+    uwplse/herbie report /in/in-file /out/
+ +

+ As before, the input and output directories must be mounted inside + the Docker container. Note that both here and above, the user is + set to the current user. This is to ensure that the files Herbie creates + have the correct permissions set. +

+ +

For developers: updating the Docker image + Dockerfile

+ +

+ For building and testing, first clone the repo and confirm that Herbie builds correctly with make install. +

+

+ Next, examine the Dockerfile and Makefile together. The Dockerfile should follow a process exactly like the Makefile, except a clean initial environment is assumed. The build may be split into 2 or more stages to limit the size of the resulting image. Each stage consists of a FROM command and a series of further commands to build up the desired environment, and later stages can refer to earlier stages by name--for example, COPY --from=earlier-stage ... can copy files compiled in earlier images. You may need to do things like bumping the version of Rust used for binary compilation or the version of Racket used in production, or adjusting paths to match the newest version of the repo. +

+

+ Once you are ready to build: +

docker build -t herbie-testbuild .
+ from the repo's main directory will build a new test image with the tag herbie-testbuild. You can run this image with +
docker run -p 8000:80 -it herbie-testbuild
+ and see the web demo in the host machine's browser at http://localhost:8000. +

+ +

+ To open a shell in a running container for testing, first get the container ID with +

docker ps
+ and then open a shell in the container as root with +
docker exec -it <CONTAINER ID> sh
+ + The code and egg-herbie binaries should be under /src. +

+ + + diff --git a/www/doc/1.7/egg-rr-seed-variance.png b/www/doc/1.7/egg-rr-seed-variance.png new file mode 100644 index 000000000..a5322710b Binary files /dev/null and b/www/doc/1.7/egg-rr-seed-variance.png differ diff --git a/www/doc/1.7/faq.html b/www/doc/1.7/faq.html new file mode 100644 index 000000000..ebfb63fbc --- /dev/null +++ b/www/doc/1.7/faq.html @@ -0,0 +1,143 @@ + + + + + Herbie FAQ + + + + + +
+ +

Common Errors and Warnings

+
+ +

Herbie automatically transforms floating + point expressions into more accurate forms. This page troubleshoots + common Herbie errors, warnings, and known issues.

+ + +

Common errors

+ +

+ Herbie error messages refer to this second for additional + information and debugging tips. +

+ +

Invalid syntax

+ +

+ This error means you mis-formatted Herbie's input. Common errors + include misspelled function names and parenthesized expressions + that should not be parenthesized. For example, in + (- (exp (x)) 1), the expression x is a + variable so shouldn't be parenthesized. (- (exp x) 1) + would be the correct way to write that expression. + The input format documentation has more + details on Herbie's syntax. +

+ +

Cannot sample enough valid points

+ +

This error occurs when Herbie is unable to find enough valid + points. For example, the expression (acos (+ 1000 x)) + is invalid unless (<= -1001 x -999), a rather narrow + range. The simplest fix is to increase + the --num-analysis flag. + Specifying the range of valid points as + a precondition can also help. +

+ +

No valid values

+ +

This error indicates that your input has no valid inputs, usually + due to an overly restriction precondition. For example, the + precondition (< 3 x 2) excludes all inputs. The + solution is to fix the precondition or input program.

+ + +

Common warnings

+ +

Herbie warnings refer to this section for explanations and common + actions to take.

+ +

Could not determine a ground truth

+ +

+ Herbie raises this warning when some inputs require more than + 10,000 bits to compute an exact ground truth. For example, to + compute (/ (exp x) (exp x)) for very + large x, absurdly large exponents would be required. + Herbie discards such inputs and raises this warning. If you see + this warning, you should add a restrictive precondition, such + as :pre (< -100 x 100), to prevent large inputs. +

+ +

Using unsound ground truth evaluation

+ +

+ Herbie's ground truth evaluation does not directly support the + Gamma and Bessel functions. Thus, any input containing these + operators triggers this warning and causes Herbie to fall back to + a slower and unsound ground truth evaluation strategy. There is + currently no workaround. +

+ +

Operator op is deprecated

+ +

+ Herbie raises this warning when an operation is no longer supported. + Input expressions containing these operators may not be portable + across different platforms. + Consider creating a plugin to support them. +

+ +

Could not uniquely print val

+ +

+ Herbie will raise this warning when it needs more than 10,000 bits + to produce a string representation for a given value. This is + likely the result of a bug in a third-party plugin. +

+ +

Unsound rule application detected

+ +

+ Herbie uses a set of algebraic rewrite rules in order to simplify + expressions, but these rules can sometimes lead to a + contradiction. Herbie will automatically compensate for this, and + in most cases nothing needs to be done. However, Herbie may have + failed to simplify the output. +

+ +

Unused variable var

+ +

+ The input FPCore contains a variable that is not + used in the body expression. +

+ +

Strange variable var

+ +

+ The input expression contains a variable that is similar in name + to named constants, e.g. e instead of E. +

+ +

Known bugs

+ +

Bugs that cannot be directly fixed are documented in this section.

+ +

Missing reports chart on Chrome

+ +

+ When using Chrome to view web pages on your local machine, Herbie + reports cannot draw the arrow chart due to security restrictions. + Run + Chrome with --allow-file-access-from-files to fix + this error. +

+ + + diff --git a/www/doc/1.7/input.html b/www/doc/1.7/input.html new file mode 100644 index 000000000..02e468b10 --- /dev/null +++ b/www/doc/1.7/input.html @@ -0,0 +1,244 @@ + + + + + Herbie Input Format + + + + + +
+ +

The Input Format

+
+ +

+ Herbie uses + the FPCore format to specify an + input program, and has extensive options for precisely describing + its context. +

+ +

General format

+ +

FPCore format looks like this:

+ +
(FPCore (inputs ...) properties ... expression)
+
(FPCore name (inputs ...) properties ... expression)
+ +

+ Each input is a variable name, like x, + used in the expression. Properties are used to specify + additional information about the expression's context. + As of version 1.5, Herbie supports named functions. + If name is specified, the function can be inlined + within any subsequent FPCore in the file. +

+ +

+ The expression is written in prefix form, with every function call + parenthesized, as in Lisp. For example, the formula for the + hypotenuse of a triangle with legs a and b is: +

+ +
(FPCore (a b) (sqrt (+ (* a a) (* b b))))
+ +

+ The semicolon (;) character introduces a line comment. + We recommend the .fpcore file extension for Herbie input files. +

+ +

Supported functions

+ +

+ Herbie supports all functions + from math.h + with floating-point-only inputs and outputs. The best supported + functions include: +

+ +
+
+, -, *, /, fabs
+
The usual arithmetic functions
+
sqrt, cbrt
+
Square and cube roots
+
pow, exp, log
+
Various exponentiations and logarithms
+
sin, cos, tan
+
The trigonometric functions
+
asin, acos, atan, atan2
+
The inverse trigonometric functions
+
sinh, cosh, tanh
+
The hyperbolic functions
+
asinh, acosh, atanh
+
The inverse hyperbolic functions
+
fma, expm1, log1p, hypot
+
Specialized numeric functions
+
+ +

Herbie also supports the constants PI + and E. The arithmetic operators associate to the left, + and - is used for both subtraction and negation.

+ +

Herbie links against your computer's libm to + evaluate these functions. So, each function has the same behavior in + Herbie as in your code.

+ +

On Windows, the Bessel functions are not available in the + system libm, so Herbie will use a fallback + implementation and print a warning. Turn off the + the precision:fallback option + to disable those functions instead.

+ +

Conditionals

+ +

FPCore uses if for conditional expressions:

+ +
(if cond if-true if-false)
+ +

+ The conditional cond may use: +

+ +
+
==, !=, <, >, <=, >=
+
The usual comparison operators
+
and, or, not
+
The usual logical operators
+
TRUE, FALSE
+
The two boolean values
+
+ +

The comparison functions implement chained comparisons with more than two arguments.

+ +

Intermediate variables

+ +

Intermediate variables can be defined + using let and let*:

+ +
(let ([variable value] ...) body)
+ +

In both let and let*, + each variable is bound to its value and can be + used in the body. The difference between let + and let* is what order the values are + evaluated in:

+ +
+
let expressions
+
In a let expression, all the values are evaluated + in parallel, before they are bound to their variables. This + means that later values can't refer to earlier variables in the + same let block.
+ +
let* expressions
+
A let* block looks the same as a let + block, except the values are evaluated one at a time, and later + values can refer to earlier variables.
+
+ +

Note that Herbie treats intermediate values only as a notational + convenience, and inlines their values before improving the formula's + accuracy. Using intermediate variables will not help Herbie improve + a formula's accuracy or speed up its run-time.

+ +

Preconditions

+ +

By default, the arguments to formulas are assumed to be + arbitrarily large or small floating-point numbers. However, in most + programs a smaller range of argument values is possible. + The :pre property (for “precondition”) describes this + smaller range.

+ +

Preconditions use comparison and boolean operators, just + like conditional statements:

+ +
(FPCore (x) :pre (< 1 x 10) (/ 1 (- x 1)))
+ +

Herbie is particularly efficient when when the precondition is + an and of ranges for each variable, but more complex + preconditions also work.

+ +

Precisions

+ +

Herbie supports both single- and double-precision values; you can + specify the precision with the :precision property:

+ +
+
binary32
+
Single-precision IEEE-754 floating point
+
binary64
+
Double-precision IEEE-754 floating point
+
racket
+
Like binary64, but using Racket math functions + rather than your computer's libm.
+
+ +

By default, binary64 is assumed. Herbie also has + a plugin system to load additional + precisions.

+ +

Conversions

+ +

Herbie supports conversions between different precisions. + All conversions are assumed to be bi-directional. You can + specify conversions with the :herbie-conversions + property.

+ +
+
:herbie-conversions
([prec1 prec2] ...)
+
If an expression is computed with precision prec1, + Herbie is allowed to rewrite all (or some) of the expression so it + is computed with precision prec2 and vice versa.
+
+ +

For example, to let Herbie introduce single-precision + code when :precision is set to binary64 or vice versa, + specify :herbie-conversions ((binary64 binary32))

+ +

Specifications

+ +

In some cases, your input program is an approximation of some + more complex mathematical expression. The :spec (for + “specification”) lets you specify the more complex ideal case. + Herbie will then try to modify the input program to make it more + accurately evaluate the specification.

+ +

For example, suppose you want to evaluate sin(1/x) + via a series expansion. Write:

+ +
(FPCore (x)
+  :spec (sin (/ 1 x))
+  (+ (/ 1 x) (/ 1 (* 6 (pow x 3)))))
+ +

Herbie will only use the :spec expression to + evaluate error, not to search for accurate expressions.

+ +

Miscellaneous Properties

+ +

Herbie uses the :name property to name FPCores in + its UI. Its value ought to be a string.

+ +

Herbie's output provide additional information in custom + properties:

+ +
+
:herbie-status status
+
status describes whether Herbie worked: it is one + of success, timeout, error, + or crash.
+
:herbie-time ms
+
The time, in milliseconds, used by Herbie to find a more accurate formula.
+
:herbie-error-input
([pts err] ...)
+
The average error of the input program at pts points. Multiple entries correspond to Herbie's training and test sets.
+
:herbie-error-output
([pts err] ...)
+
The computed average error of the output program, similar to :herbie-error-input.
+
+ +

Herbie's benchmark suite also uses properties such + as :herbie-target for continuous integration, but these + are not supported and their use is discouraged.

+ + + diff --git a/www/doc/1.7/installing.html b/www/doc/1.7/installing.html new file mode 100644 index 000000000..eae03e45b --- /dev/null +++ b/www/doc/1.7/installing.html @@ -0,0 +1,134 @@ + + + + + + Installing Herbie + + + + + + +
+ +

Installing Herbie

+
+ +

+ Herbie supports Linux, macOS, and Windows. It + can be installed from a package or from source. To start, install + Racket, which Herbie is + written in. Install Rust + when building from source. (Herbie is also available as + a Docker image.) +

+ +

Installing Racket

+ +

+ Install Racket either using + the official + installer or distro-provided packages. Versions as old as 8.0 + are supported, but more recent versions are faster. +

+ +

+ Test that Racket is installed correctly and has a correct version: +

+ +
racket
+Welcome to Racket v8.5 [cs].
+> (exit)
+ +

Installing Herbie from source

+ +

+ Install Rust, using rustup or via some other means. + Versions as old as 1.60.0 are supported. + This installation method supports Windows, macOS, and Linux for various architectures. +

+ +

+ Once Racket and Rust are installed, download the Herbie source + from GitHub with: +

+ +
git clone https://github.com/uwplse/herbie
+ +

+ Change to the herbie directory; + you should see a README.md file, a directory named src, + a directory named bench/, and a few other directories. + Install Herbie on your system with: +

+ +
make install
+ +

+ This command installs Herbie and its dependencies, compiles it for + faster startup, and places the herbie executable in + your Racket user path (example paths for Racket 8.5): +

+ + + +

+ You can run herbie from that directory, or add it to + your executable path. Once Herbie is installed and working + correctly, check out the tutorial. +

+ +

Installing Herbie from a package

+ +

+ This installation method supports Windows, macOS, and Linux for x86-64. + This method of installation will fail for Apple M1 systems and other ARM architectures. + Once Racket is installed, install Herbie from a package with: +

+ +
raco pkg install --auto herbie
+ + + +

+ This command installs Herbie and its dependencies, compiles it for + faster startup, and places the herbie executable in + your Racket user path (example paths for Racket 8.1): +

+ + + +

+ You can run herbie from that directory, or add it to + your executable path. Once Herbie is installed and working + correctly, check out the tutorial. +

+ + + +

Installing Herbie with Docker

+ +

+ Docker is a container manager, + which is sort of like an easily-scriptable virtual machine. Herbie + in Docker is more limited; we do not recommend using Herbie + through Docker without prior Docker experience. +

+ +

+ The Docker documentation describes how + to install and run the official uwplse/herbie image. +

+ + + + diff --git a/www/doc/1.7/interactive-preconditions.png b/www/doc/1.7/interactive-preconditions.png new file mode 100644 index 000000000..bc512e1c1 Binary files /dev/null and b/www/doc/1.7/interactive-preconditions.png differ diff --git a/www/doc/1.7/old-rr-seed-variance.png b/www/doc/1.7/old-rr-seed-variance.png new file mode 100644 index 000000000..a446095b9 Binary files /dev/null and b/www/doc/1.7/old-rr-seed-variance.png differ diff --git a/www/doc/1.7/options.html b/www/doc/1.7/options.html new file mode 100644 index 000000000..4a7fd5051 --- /dev/null +++ b/www/doc/1.7/options.html @@ -0,0 +1,276 @@ + + + + + Herbie Command-line Options + + + + + +
+ +

Command-line Options

+
+ +

The herbie command has + subcommands and options that influence both its user interface and + the quality of its output.

+ +

Herbie commands

+ +

Herbie can be run both interactively and in batch mode, and can + generate output intended either for + the command line + or the web. We call these different + ways of running Herbie different tools. Herbie provides four + tools:

+ +
+
herbie web
+
Use Herbie through your browser. + The herbie web command runs Herbie on your local + machine and opens your browser to its main page.
+ +
herbie shell
+
Use Herbie via a command-line shell. + Enter an FPCore expression and Herbie + will print its more-accurate version.
+ +
herbie improve input output
+
Run Herbie on the expressions in the file or + directory input. The results are written + to output, a single file in FPCore format.
+ +
herbie report input output
+
Run Herbie on the expressions in the file or + directory input. The results are written + to output, a directory of + HTML reports. These pages can be viewed + in any browser (though with a quirk for + Chrome).
+
+ +

We recommend using web and report, + which produce reports with lots of + information about floating-point accuracy, including graphs it of + error versus input values. This can help you understand whether + Herbie's improvements matter for your use case.

+ +

Use herbie tool --help to available + command-line options for a tool. This command also shows unsupported + options not listed on this page.

+ +

General options

+ +

+ These options can be set on any tool. Pass them after the tool + name but before other arguments, like this: +

+ +
herbie report --timeout 60 in.fpcore out/
+ +

Arguments cannot go before options.

+ +
+
--seed S
+
The random seed, which changes the randomly-selected points + that Herbie evaluates candidate expressions on. The seed is a + number between 0 and 231 (exclusive both ends). This + option can be used to make Herbie's results reproducible or to + compare two different runs. Seeds are not preserved across + runs.
+ +
--num-points N
+
The number of input points Herbie uses to evaluate candidate + expressions. The default, 256, is a good balance for most + programs. Increasing this option, say to 512 or 1024, will slow + Herbie down but may make its results more consistent.
+ +
--num-iters N
+
The number of times Herbie attempts to improve accuracy. The + default, 4, suffices for most programs and helps keep Herbie + fast; in practice iterations beyond the first few rarely lead to + lower error. Increase this option, say to 6, to check that there + aren't further improvements that Herbie could seek out.
+ +
--num-analysis N
+
The number of input subdivisions to use when searching for + valid input points. The default is 14. Increasing this option + will slow Herbie down, but may fix the + "Cannot sample enough + valid points" error. +
+ +
--timeout T
+
The timeout to use per-input, in seconds. A fractional number + of seconds can be given.
+ +
--threads N (for the improve and report tools)
+
Enables multi-threaded operation. By default, no threads are + used. A number can be passed to this option to use that many + threads, or yes can be passed to tell Herbie to use + all of the hardware threads.
+ +
--pareto
+
Enables multi-objective improvement. Herbie will attempt to simultaneously + optimize for both accuracy and expression cost. Rather than generating + a single "ideal" output expression, Herbie will generate many output expressions. + This mode is still considered experimental. With this option, Herbie will + take a long time to run. We recommend timeouts measured in hours.
+
+ +

Web shell options

+ +

The web tool runs Herbie and connects to it from + your browser. It has options to control the underlying web + server.

+ +
+
--port N
+
The port the Herbie server runs on. The default port is 8000.
+ +
--save-session dir
+
Save all the reports to this directory. The directory also + caches previously-computed expressions.
+ +
--log file
+
Write an access log to this file, formatted like an Apache + log. This log does not contain crash tracebacks.
+ +
--quiet
+
By default, but not when this option is set, a browser is + automatically started to show the Herbie page. This option also + shrinks the text printed on start up.
+ +
--public
+
When set, users on other computers can connect to the demo and + use it. (In other words, the server listens + on 0.0.0.0.). Essential when Herbie is run + from Docker.
+
+ +

Rulesets

+ +

+ Herbie uses rewrite rules to change programs and improve accuracy. + The --disable rules:group + and --enable rules:group options turn rule + sets on and off. In general, turning a ruleset on makes Herbie + produce more accurate but more confusing programs. +

+ +

The full list of rule groups is:

+ + + + + + + + + + + + + +
Rule GroupTopic of rewrite rules
arithmeticBasic arithmetic facts
polynomialsFactoring and powers
fractionsFraction arithmetic
exponentsExponentiation identities
trigonometryTrigonometric identities
hyperbolicHyperbolic trigonometric identities
boolsBoolean operator identities
branchesif statement simplification
specialThe gamma, Bessel, and error functions
numericsNumerical compounds expm1, log1p, fma, and hypot
+ +

Search options

+ +

+ These options change the types of transformations that Herbie uses + to find candidate programs. We recommend sticking to the defaults. +

+ +

+ Each option can be turned off with the -o + or --disable command-line flag and on with + +o or --enable. Turning an option off + typically results in less-accurate results, while turning a option + on typically results in more confusing output expressions. +

+ +
+
precision:fallback
+
This option, on by default, tells Herbie to use fallback + functions if a native implementation is not found for an operation + (and print a warning). If turned off, operations with no native + implementation will be disabled entirely. To our knowledge, this + option only affects the Bessel functions on Windows.
+ +
setup:simplify
+
This option, on by default, simplifies the expression before + passing it to Herbie. If turned off, Herbie will not simplify + input programs before improving them.
+ +
generate:rr
+
This option, on by default, uses Herbie's recursive rewriting + algorithm to generate candidate programs. If turned off, Herbie + will use a non-recursive rewriting algorithm, which will + substantially limit Herbie's creativity.
+ +
generate:taylor
+
This option, on by default, uses series expansion to produce + new candidates during the main improvement loop. If turned off, + Herbie will not use series expansion. Turn this option off if you + want to avoid series-expansion-based rewrites, such as if you need + to preserve the equivalence of the input and output expressions as + real-number formulas.
+ +
generate:simplify
+
This option, on by default, simplifies candidates during the + main improvement loop. If turned off, candidates will not be + simplified, which typically results in much less accurate + expressions.
+ +
reduce:regimes
+
This option, on by default, uses Herbie's regime inference + algorithm to branch between several program candidates. If turned + off, branches will not be inferred and the output program will be + straight-line code (if the input was). Turn this option off if + your programming environment makes branches very expensive, such + as on a GPU.
+ +
reduce:avg-error
+
This option, on by default, causes Herbie to output the + candidate with the best average error over the chosen inputs. If + turned off, Herbie will choose the candidate with the least + maximum error instead. This usually produces programs with worse + overall accuracy. Turn this option off if worst-case accuracy is + more important to you than overall accuracy.
+ +
reduce:binary-search
+
This option, on by default, uses binary search to refine the + values used in inferred branches. If turned off, different runs of + Herbie will be less consistent, and accuracy near branches will + suffer.
+ +
reduce:branch-expressions
+
This option, on by default, allows Herbie to branch on + expressions, not just variables. This slows Herbie down, + particularly for large programs. If turned off, Herbie will only + try to branch on variables.
+
+ +

Upgrading from Herbie 1.0

+ +

Herbie 1.0 used + a different command line + syntax, without multiple tools. Translate like so:

+ + + +

The new syntax somewhat changes Herbie's behavior, such as by + using the input expression as the output if Herbie times out. It + also makes it easier to write Herbie's output to a file without + using command-line redirection.

+ + + + diff --git a/www/doc/1.7/pareto-screenshot.png b/www/doc/1.7/pareto-screenshot.png new file mode 100644 index 000000000..79e0769a0 Binary files /dev/null and b/www/doc/1.7/pareto-screenshot.png differ diff --git a/www/doc/1.7/plugins.html b/www/doc/1.7/plugins.html new file mode 100644 index 000000000..b23494bdc --- /dev/null +++ b/www/doc/1.7/plugins.html @@ -0,0 +1,438 @@ + + + + + Herbie Plugins + + + + + +
+ +

Plugins

+
+ +

Herbie plugins define new functions, add + rewrite rules, and even implement number representations.

+ +

Herbie plugins are installed separately. Herbie then + automatically loads and uses them.

+ +

Posit arithmetic

+ +

The softposit-herbie plugin implements support + for posit arithmetic. Install it + with:

+ +
raco pkg install --auto softposit-herbie
+ +

This plugin uses the SoftPosit library, only supported on Linux. + Even then is reported to misbehave on some machines. The plugin + support arithmetic operations, sqrt, and quires.

+ +

Once softposit-herbie is installed, + specify :precision posit16 to inform Herbie that it + should assume the core's inputs and outputs are posit numbers. Other + posit sizes (with 8 or 32 bits) and also quires (for 8, 16, and 32 + bit posits) are available, but are poorly supported.

+ + +

Complex numbers

+ +

The complex-herbie plugin has been removed as of Herbie 1.6. + This plugin may be brought back in the future. + +

Generic floating-point numbers

+ +

The float-herbie plugin implements support for any IEEE-754 + binary floating-point number. To install, check out the + source code + and run +

+ +
raco pkg install
+ +

+ at the top-level directory of the repository. + Once float-herbie is installed, + specify :precision (float ex nb) + to inform Herbie that it should assume the core's inputs and outputs are + floating-point numbers with ex exponent bits and nb total bits + (sign bit + mantissa bits + exponent bits). +

+ +

Generic fixed-point numbers

+ +

The fixedpoint-herbie plugin implements support for any fixed-point number. + To install, check out the + source code + and run +

+ +
raco pkg install
+ +

+ at the top-level directory of the repository. + Once fixedpoint-herbie is installed, + specify :precision (fixed nb sc) + to inform Herbie that it should assume the core's inputs and outputs are + signed fixed-point numbers with nb total bits and a scaling factor of + 2sc (integer formats have a scaling factor of 20). + This plugin also supports unsigned fixed-point numbers specified by + :precision (ufixed nb sc) and provides + simpler aliases for integer formats with :precision (integer nb) + and :precision (uinteger nb). +

+ +

Developing plugins

+ +

The following is a guide to creating a Herbie plugin. + Plugins are considered experimental and may change considerably + between releases. + If you run into issues, please write to the + + mailing list. + Be sure to check out the + built-in plugins in the Herbie repository before getting started.

+ +

First Steps
+ + All plugins are implemented as Racket packages. The easiest way to + initialize a new Racket package is to run + +

raco pkg new pkg-name
+ + in a new folder. Make sure the folder name is the same as the package name! + This will initialize a Racket package with all the necessary files. + Read the official Racket documentation on the + + raco tool for more information.

+ +

A single entry needs to be added to the package manifest stored in info.rkt, + and add (define herbie-plugin 'name) to the bottom of the file + where name is a unique symbol that doesn't conflict with other Herbie plugins. + As a suggestion, this should just be the package name.

+ +

Next, edit the main.rkt file by erasing everything except the + language specifier on the first line, and add the line (require herbie/plugin). + This gives the package access to the Herbie plugin interface. + Optionally add the following for debugging purposes + (eprintf "Loading pkg-name support...\n") + directly after the require statement.

+ +

Finally, run the following in the folder containing info.rkt + and main.rkt: + +

raco pkg install
+ + This should install your package and check for errors. + Now everything is set up! + Of course, your plugin is empty and doesn't add any useful features. + If you added the debugging line in main.rkt, you should see the string + when you run Herbie. +

+ +

Adding Features
+ + Now that you have an empty plugin, you can begin adding new functions, rewrite + rules, and number representatons. + The procedures exported by the Herbie plugin interface can be roughly divided into + two categories: unique and parameterized. + Whether or not you use the unique or parameterized half of the interface + (or maybe both!) depends entirely on the number representation a feature is being + implemented for. + First, identify if your number representation is unique or parameterized. + For example, if you are adding features for double precision + (or rather binary64), the representation is unique. + If you are adding features for a generic floating point format, say + (float ebits nbits), then the representation is parameterized.

+ +

Plugin Interface (Unique)
+ + The following are the signatures and descriptions of the + plugin procedures for unique representations. + These procedures are required to be at the top-level of + main.rkt rather than inside a function.

+ +
+
+ (define-type name (exact? inexact?) + exact->inexact inexact->exact) +
+
Adds a new type with the unique identifier name. + The arguments exact? and inexact? + return true if a value is an exact or high-precision approximate representation. + For Herbie's real type, exact? is implemented + with real? and inexact? is implemented + with bigfloat?. The procedures exact->inexact and + inexact->exact convert between exact? + and inexact? values. +
+ +
+ + + + + + + + + +
(define-representation (name type repr?)bigfloat->repr
repr->bigfloat
ordinal->repr
repr->ordinal
width
special?)
+
+
+
Adds a new representation with the unique identifier name. + The representation will inherit all rewrite rules defined for type. + By default, Herbie defines two types: real and bool. + Your representation will most likely inherit from real. + The width argument should be the bitwidth of the representation, + e.g. 64 for binary64. + The argument repr? is a procedure that accepts any argument and returns + true if the argument is a value in the representation, e.g. an integer representation + should use Racket's integer?, while special? takes a + value in the representation and returns true if it is not finite, e.g. NaN or infinity.

+ + The other four arguments are single-argument procedures that implement different conversions. + The first two convert between a value in your representation and a Racket + bigfloat + (you need to import math/bigfloat). + The last two convert between a value in your representation and its corresponding ordinal value. + Ordinal values for any representation must be within the interval [0, 2width - 1]. + Check Racket's definition of + + ordinals for floats. + Note that those ordinal values can be negative. +
+ +
+ + + + +
(define-operator (name itype-names ...) otype-name
[bf bf-fn]
[ival ival-fn]) +
+
+
+
Adds a new operator. Operators describe pure mathematical functions, + i.e. + or sin. + The parameters itype-names and otype-name + are the input type(s) and output type names. + For example, + takes two real inputs and produces + one real output. + The bf-fn argument is the + bigfloat implementation of your operator. + The ival-fn argument is the Rival + implementation of your operator. This is optional but improves the quality of Herbie's output. + If you don't want to implement this, set ival-fn to false. + To define operators with an unknown number of arguments, e.g. comparators, + add the attribute [itype itype]. + This will override the input type names defined by itype-names. + See the bottom of this section for support for constants. +
+ +
+ + + + + +
(define-operator-impl (op name irepr-names ...)orepr-name
[fl fl-fn]
...)
+
+
+
Implements op with input representation(s) irepr-names + and output representation orepr-name. + The field name must be unique. + For example, Herbie implements +.f64 and +.f32 + for double- and single-precision floats. + The argument fl-fn is the actual procedure that does the computation. + Like define-operator, the input representations can be + overridden with [itype irepr]. + By default, the attributes bf and ival + are inherited from op but can be overridden as previously + described. + See the bottom of this section for support for constant implementations. +
+ +
+ + + + + + +
(define-ruleset name (groups ...)#:type ([var repr] ...)
[rule-name match replace]
...)
+
+
+
Defines a set of rewrite rules. + The name of the ruleset as well as each rule-name + must be a unique symbol. + Each ruleset must be marked with a set of groups + (read here on ruleset groups). + Each rewrite rule takes the form match ⇝ replace where Herbie's rewriter + will replace match with replace (not vice-versa). + Each match and replace is an expression whose operators are + the names of operator implementations rather than pure mathematical operators. + Any variable must be listed in the type information with its associated representation. + See the softposit-herbie plugin for a more concrete example. +
+ +
+ + + + + + +
(define-ruleset* name (groups ...)#:type ([var type] ...)
[rule-name match replace]
...)
+
+
+
Like define-ruleset, but it defines a ruleset for every representation that + inherits from type. + Currently, every type must be the same, e.g. + all real, for this procedure to function correctly. + Unlike define-ruleset, match and replace + contain the names of operators rather than operator implementations. +
+
+ +

Procedures for declaring constants are not a part of the plugin interface. + Instead, constants and constant implementations are defined as + zero-argument operators and operator implementations. + The fields fl-fn, bf-fn, + and ival-fn should be implemented with zero-argument + procedures (thunks). + Similar to operator and operator implementations, constants describe pure + mathematical values like π or e while constant + implementations define an approximation of those constants in a particular + representation. +

+ +

Plugin Interface (Parameterized)
+ + Defining operators, constants, and representations for parameterized functions requires + a generator procedure for just-in-time loading of features for a particular + representation. + When Herbie encounters a representation it does not recognize (not explicitly defined + using define-representation) it queries a list of generators in case the + representation requires just-in-time loading. +

+ +

The following procedure handles represention objects:

+ +
+
(get-representation name)
+
Takes a representation name and returns a representation object. + Do not call this function before the associated representation has been registered! +
+
+ +

The following procedures handle generators:

+ +
+
(register-generator! gen)
+
Adds a representation generator procedure to Herbie's set of generators. + Representation generator procedures take the name of a representation and + return the associated representation object if it successfully created the + operators, constants, and rules for that representation. + In the case that your plugin does not register the requested representation, + the generator procedure need not do anything and should just return + false. +
+
+ +
+
(register-conversion-generator! gen)
+
Adds a conversion generator procedure to Herbie's set of generators. + Conversion generator procedures take the names of two representations + and returns true if it successfully registered conversion(s) + between the two representations. + Conversions are one-argument operator implementations of the cast + operator that have one representation as an input representation and + a different representation as an output representation. + User-defined conversions are OPTIONAL for multi-precision optimization, + since Herbie can synthesize these by default. + However Herbie's implementations are often slow since they are + representation-agnostic and work for any two representations. + In the case that your plugin does not register the requested conversion(s), + the generator procedure need not do anything and should just return + false. +
+
+ +

+ To actually add representations, operators, etc. within a generator procedure, + you must use a set of alternate procedures. +

+ +
+
+ + + + + + + + + + + +
(register-representation! name
type
repr?
bigfloat->repr
repr->bigfloat
ordinal->repr
repr->ordinal
width
special?)
+
+
+
Like define-representation, but used within generators.
+ +
+ + + +
(register-representation-alias! name repr)
+
+
+
Adds an alias name for an existing representation repr. + If two representations are equivalent, e.g. (float 8 32) and binary32, + this procedure can be used to declare the two representations equivalent. +
+ +
+ (register-operator! op name itype-names + otype-name attribs) +
+
Like define-operator, but used within generators. + The argument itype-names is a list of the input types + while the argument attribs are the same attributes for + define-operator, e.g. bf. + In this case, attribs is an association: + (list (cons 'bf bf-fn) ...). +
+ +
+ (register-operator-impl! op name ireprs + orepr attribs) +
+
Like define-operator-impl, but used within generators. + Unlike define-operator-impl, this procedure takes representation + objects rather than representation names for ireprs + and orepr. + Use get-representation to produce these objects. + See register-operator! for a description of attribs. +
+ +
(register-ruleset! name groups + var-repr-names rules) +
+
Like define-ruleset, but used within generators. + In this case, groups is a list of rule groups; + var-repr-names is an association + pairing each variable in the ruleset with its representation, e.g. + (list (cons 'x '(float 5 16)) ...); + and rules is a list of rules of the following + form (list (list rule-name match replace) ...). +
+ +
+ + + diff --git a/www/doc/1.7/quadp-old-branch.png b/www/doc/1.7/quadp-old-branch.png new file mode 100644 index 000000000..1e0c9fe83 Binary files /dev/null and b/www/doc/1.7/quadp-old-branch.png differ diff --git a/www/doc/1.7/quadp-short-branch.png b/www/doc/1.7/quadp-short-branch.png new file mode 100644 index 000000000..cb60d12cc Binary files /dev/null and b/www/doc/1.7/quadp-short-branch.png differ diff --git a/www/doc/1.7/range-input-2.png b/www/doc/1.7/range-input-2.png new file mode 100644 index 000000000..4d0eb5c6a Binary files /dev/null and b/www/doc/1.7/range-input-2.png differ diff --git a/www/doc/1.7/range-input.png b/www/doc/1.7/range-input.png new file mode 100644 index 000000000..f8243e70c Binary files /dev/null and b/www/doc/1.7/range-input.png differ diff --git a/www/doc/1.7/release-notes.html b/www/doc/1.7/release-notes.html new file mode 100644 index 000000000..0a67dc497 --- /dev/null +++ b/www/doc/1.7/release-notes.html @@ -0,0 +1,218 @@ + + + + + Herbie 1.6 Release Notes + + + + + + +
+ +

Herbie 1.6 Release Notes

+
+ +

The Herbie developers are excited to announce + Herbie 1.6! This release focuses on further integration of egg, improved reliability, + and a better web interface. Our favorite features are below.

+ + The Herbie team, working over Zoom to bring you Herbie 1.6 + +

What is Herbie? Herbie automatically improves the accuracy + of floating point expressions. This avoids the bugs, errors, and + surprises that so often occur with floating point arithmetic.

+ +

Join us! Join the Herbie developers on the + FPBench Slack, at the monthly + FPBench community meetings, and at + FPTalks 2022. + +

+ + +
+ Comparison of Herbie's total output error (bits) across 100 seeds with + the old recursive rewriter (top) versus the egg-based implementation (bottom). + The egg-based implementation has lower variability. +
+
+ +

Recursive Rewriting with egg

+ + Two releases ago, Herbie 1.4 featured a new simplifier that used the + egg library + for a substantial increase in speed. + This release further incorporates the egg library into Herbie by replacing + the recursive rewriter with an egg-based implementation. + Herbie's output is now more stable across seeds compared + to the previous implementation, maintains a similar level + of performance, and increases accuracy gains overall. + This change also makes it easier to add new rewrite rules, + since the egg-based rewriter's behavior is more predictable + than the old recursive rewriter was. + +
+ +
+ Preconditions in the new web interface. For each input, + users are asked to provide a range of values for Herbie + to focus on optimizing over. Input ranges vary depending + on the user's application and should always be + supplied to maximize accuracy. +
+
+ +

Interactive Herbie

+ +

+ Despite the fact that most users interact with Herbie via + the demo page, + the web interface has historically had a minimal design, + with important features like preconditions hidden behind + advanced configuration dialogs. + As part of an ongoing push to make Herbie more user-friendly, + we have added support for preconditions to the main interface, + and have improved the display of warnings and errors. + We expect the demo page to change further in the coming year + to provide users with more support in analyzing Herbie's output + and testing their own ideas for rewritings. +

+ +
+ + + + + +
+
+ Comparison of the midpoint (left) vs. shortest number (right) methods for + selecting branch conditions. +
+
+ +

Shorter Branch Conditions

+ +

+ Herbie now synthesizes branch conditions with shorter split values. + Before, Herbie's binary search algorithm would narrow down the set of + possible split values to a small interval from which Herbie took the midpoint. + Often the midpoint had a long string representation which made it seem + like it was chosen with high precision. + Now Herbie will choose a value on that same interval with a short string representation. + This change makes output programs more readable and highlights the + low precision in the result of binary search. + +

+ +
+ +
+ System diagram for Herbie 1.6, with key changes in red dotted boxes. + From top to bottom: double-precision (binary64) and single-precision (binary32) types + are loaded through plugins instead of being embedded in Herbie's core; + a new patching subsystem bundles together the various + rewriting methods behind a simple interface; + recursive rewrite uses egg. + Compare Herbie 1.5 and 1.6 system diagrams here + and here. +
+
+ +

Patching and Plugins

+ +

Herbie has undergone a significant architectural change since the previous release. + Although this change may not be visible to users, we hope that it + makes future Herbie development more streamlined and provides a clearer + answer to the question: what is Herbie? + In particular, two major improvements include adding the "patch table" + and moving number system specifics out of Herbie's + core architecture. +

+ +

The patch table manages most rewriting capabilities, provides a + minimal interface to generate variants from a set of expressions, + and caches variants in case of duplicate input expressions. + Creating this subsystem to handle variant generation more cleanly + separates the "generate" and "test" parts within Herbie. +

+ +

Herbie's double-precision and single-precision representations + are now implemented as plugins that automatically ship + with Herbie. + Representation-specific operators and definitions are + no longer present in Herbie's core architecure. + This change makes Herbie representation-agnostic and loads + double- and single-precision representations through the plugin interface. + Not only is this design cleaner, but these plugins now + serve as examples for plugin developers. + In the future, we hope to move additional definitions + out of core Herbie and into plugins such as error metrics + and cost models (Pherbie). +

+
+

Other improvements

+ + +

Deprecations and removals

+ +
+

Try it out!

+ +

+ We want Herbie to be more useful to scientists, engineers, and + programmers around the world. We've got a lot of features we're + excited to work on in the coming months. Please + report bugs, + join + the + mailing list, + or contribute. +

+
+

If you find Herbie + useful, let us know!

+ + diff --git a/www/doc/1.7/report-derivation.png b/www/doc/1.7/report-derivation.png new file mode 100644 index 000000000..0fb9d793f Binary files /dev/null and b/www/doc/1.7/report-derivation.png differ diff --git a/www/doc/1.7/report-error.png b/www/doc/1.7/report-error.png new file mode 100644 index 000000000..bfb60cad1 Binary files /dev/null and b/www/doc/1.7/report-error.png differ diff --git a/www/doc/1.7/report-large.png b/www/doc/1.7/report-large.png new file mode 100644 index 000000000..bce9ba7e8 Binary files /dev/null and b/www/doc/1.7/report-large.png differ diff --git a/www/doc/1.7/report-plot2.png b/www/doc/1.7/report-plot2.png new file mode 100644 index 000000000..641688086 Binary files /dev/null and b/www/doc/1.7/report-plot2.png differ diff --git a/www/doc/1.7/report-prog.png b/www/doc/1.7/report-prog.png new file mode 100644 index 000000000..09f416e50 Binary files /dev/null and b/www/doc/1.7/report-prog.png differ diff --git a/www/doc/1.7/report-prog2.png b/www/doc/1.7/report-prog2.png new file mode 100644 index 000000000..98036a71c Binary files /dev/null and b/www/doc/1.7/report-prog2.png differ diff --git a/www/doc/1.7/report-reproduce.png b/www/doc/1.7/report-reproduce.png new file mode 100644 index 000000000..356edd733 Binary files /dev/null and b/www/doc/1.7/report-reproduce.png differ diff --git a/www/doc/1.7/report-try-it.png b/www/doc/1.7/report-try-it.png new file mode 100644 index 000000000..14e8406d2 Binary files /dev/null and b/www/doc/1.7/report-try-it.png differ diff --git a/www/doc/1.7/report.html b/www/doc/1.7/report.html new file mode 100644 index 000000000..7e2a6a1c0 --- /dev/null +++ b/www/doc/1.7/report.html @@ -0,0 +1,143 @@ + + + + + Herbie reports + + + + + +
+ +

Herbie reports

+
+ + +

The Herbie report

+ +

When used in the browser, Herbie + generates HTML reports full of information about the accuracy of + your input and its output expressions.

+ +

Summary numbers

+ +

First, a brief summary of the results. For most uses, the + “Average Error” number, which describes how accurate the input and + output expressions are, is the most important statistic in this + section. The other numbers list time Herbie took to improve the + program and the precision + assumed for floating-point operations. +

+ +
+ +
Summary numbers from a Herbie report. The "binary64" + precision refers to double-precision IEEE-754 + arithmetic.
+
+ +

Input and output programs

+ +

Second, the input and output programs themselves, in standard + mathematical syntax. In the top-right corner, the drop-down can be + used to switch to C syntax or some other format.

+ +
+ +
Input and output program from a Herbie report.
+
+ +

Error graph

+ +

+ Third, under Error, a graph of floating-point error + versus input value. This is helpful for understanding the sorts of + inputs Herbie is improving accuracy on. Sometimes, Herbie improved + accuracy on some inputs at the cost of accuracy on other inputs + that you care more about. You can add + a precondition to restrict + Herbie to certain inputs in those cases. +

+ +

+ These graphs show the error of the input program with a red line, + and the error of the output program with a blue line. Both can be + toggled. If the expression has multiple variables, the variable + picker on the bottom left selects which variable is placed on the + horizontal axis. If Herbie decided to insert an if + statement into the program, the locations of those if + statements will be marked with vertical bars. +

+ +
+ +
An error graph from a Herbie report. Note the variable + selector (x is selected) and the toggles for the + input and output program (both are toggled on).
+
+ +

Interactive inputs

+ +

+ Fourth, a interactive form where you can the output of both your + and Herbie's programs. on inputs of your choice Enter argument + values on the left, and the input and output programs will be + evaluated on those arguments and the results printed on the right. +

+ +
+ +
+ The interactive section of a Herbie report. "In" is your program, + "Out" is Herbie's. +
+
+ +

Derivation

+ +

Fifth, Herbie's derivation of its output program. These can be + helpful in understanding how Herbie works. Each substantive step + in the derivation also lists the error, in bits, of that step's + output. Sometimes you can use that to pick a less-complex and + not-substantially-less-accurate program.

+ +

Derivations sometime name arithmetic laws used by Herbie, or they + might claim derivation steps are done by simplification, series + expansion, or other Herbie strategies. The derivation will also + call out any time the input is split into cases. When one part of + the program is colored blue, that is the part modified in that + derivation step. +

+ +
+ +
A short derivation from a Herbie report. Note the + error, in gray, measured after each derivation step.
+
+ +

Reproduction

+ +

Sixth, a command to reproduce this Herbie result. If you find a + Herbie bug, include this code snippet when + filing an + issue.

+ +
+ +
Reproduction information for a Herbie run. You can use + this when submitting bug reports.
+
+ + + +

The top of the page has a right-hand menu bar with additional + links. “Report” returns you to Herbie's main page. “Log” and + “Metrics” give you detailed internal information about Herbie.

+ +

We expect the report to grow more informative with future + versions. Please get in + touch if there is more information you'd like to see.

+ + + diff --git a/www/doc/1.7/system-1.6-changes.png b/www/doc/1.7/system-1.6-changes.png new file mode 100644 index 000000000..aa6efb805 Binary files /dev/null and b/www/doc/1.7/system-1.6-changes.png differ diff --git a/www/doc/1.7/system-1.6.png b/www/doc/1.7/system-1.6.png new file mode 100644 index 000000000..e36ef55c0 Binary files /dev/null and b/www/doc/1.7/system-1.6.png differ diff --git a/www/doc/1.7/team.png b/www/doc/1.7/team.png new file mode 100644 index 000000000..be7c3befb Binary files /dev/null and b/www/doc/1.7/team.png differ diff --git a/www/doc/1.7/toc.js b/www/doc/1.7/toc.js new file mode 100644 index 000000000..d1f1a1671 --- /dev/null +++ b/www/doc/1.7/toc.js @@ -0,0 +1,22 @@ +function make_toc() { + var headings = document.querySelectorAll("h2"); + var toc = document.createElement("nav"); + toc.classList.add("toc") + var list = document.createElement("ul"); + for (var i = 0; i < headings.length; i++) { + var li = document.createElement("li"); + var a = document.createElement("a"); + var h = headings[i]; + if (! h.id) { + h.setAttribute("id", "heading-" + i); + } + a.setAttribute("href", "#" + h.id); + a.innerHTML = h.innerHTML; + li.appendChild(a); + list.appendChild(li); + } + toc.appendChild(list); + headings[0].parentNode.insertBefore(toc, headings[0]); +} + +window.addEventListener("load", make_toc); diff --git a/www/doc/1.7/tutorial.html b/www/doc/1.7/tutorial.html new file mode 100644 index 000000000..728ae7d77 --- /dev/null +++ b/www/doc/1.7/tutorial.html @@ -0,0 +1,302 @@ + + + + + Herbie Tutorial + + + + +
+ +

Herbie Tutorial

+
+ +

+ Herbie rewrites floating point expressions to + make them more accurate. Floating point arithmetic is + inaccurate; even 0.1 + 0.2 ≠ 0.3 for a computer. Herbie helps + find and fix these mysterious inaccuracies. +

+ +

+ To get started, download and install + Herbie. You're then ready to begin using Herbie. +

+ +

Giving Herbie expressions

+ +

Start Herbie with:

+ +
herbie web
+ +

+ After a brief wait, this will open your web browser and show you + Herbie's main window. The most important part of the page is this + bit: +

+ +
+ The program input field in the Herbie web UI. +
+ +

Type (1 + x) - x into this box. You should see two + boxes appear for entering the lower and upper bound on the range + of values for x. Select the lowest and highest options, like this: +

+ The input range field in the Herbie web UI. +
+ Finally, hit the "Improve with Herbie" button. You should see the + entry box gray out, then some text will appear on the + screen describing what Herbie is doing. After a few seconds, you'll + be redirected to a page with Herbie's results. The most important + part of that page is the large gray box in the middle: +

+ +
+ Input and output program from a Herbie report. +
+ +

+ It shows the input, (1 + x) - x, and Herbie's more + accurate way to evaluate that expression: 1. Herbie + did a good job, which you can see from the statistics at the top + of the page: +

+ +
+ Statistics and error measures for this Herbie run. +
+ +

+ The initial program had 29.0 bits of error (on average), while + Herbie's better version had 0 bits of error. That's because + (1 + x) - x should always be exactly equal + to 1, but in floating-point arithmetic, + when x is really big, 1 + x rounds down + to x and the expression returns 0. +

+ +

+ There is more information on this + results web page, which you can use explain more about the + expression's errors and how Herbie derived its result. +

+ +

Programming with Herbie

+ +

Now that you've run Herbie and know how to read its results, + let's apply Herbie to a realistic program.

+ +

+ Herbie's input expressions can come from source code, mathematical + models, or even a debugging tool + like Herbgrind. But most + often, they come from your mind, while you're writing new + mathematical code. +

+ +

When you're writing a new numerical program, it's best to keep + Herbie open in a browser tab so you can run it easily. That way, you + can run Herbie on any complex floating-point expression you're + coding up and so always use an accurate version of that expression. + Herbie has options to log all the + expressions you enter, so that you can refer to them later.

+ +

However, let's suppose you're instead tracking down a + floating-point bug in existing code. Then you'll need start by + identifying the problematic floating-point expression.

+ +

To demonstrate the workflow, let's walk through + bug 208 + in math.js, a math library for + JavaScript. The bug deals with inaccurate square roots for complex + numbers. (For a full write-up of the bug itself, check out + a blog + post by one of the Herbie authors.) +

+ +

Finding the problematic expression

+ +

+ In most programs, there's a small core that does the mathematical + computations, while the rest of the program sets up parameters, + handles control flow, visualizes or print results, and so on. The + mathematical core is what Herbie will be interested in. +

+ +

+ For our example, let's start + in lib/function/. + This directory contains many subdirectories; each file in each + subdirectory defines a collection of mathematical functions. The + bug we're interested in is about complex square root, which is + defined in + arithmetic/sqrt.js. +

+ +

+ This file handles argument checks, five different number types, + and error handling, for both real and complex square roots. None + of that is of interest to Herbie; we want to extract just the + mathematical core. So skip down to the isComplex(x) + case: +

+ +
var r = Math.sqrt(x.re * x.re + x.im * x.im);
+if (x.im >= 0) {
+  return new Complex(
+      0.5 * Math.sqrt(2.0 * (r + x.re)),
+      0.5 * Math.sqrt(2.0 * (r - x.re))
+  );
+}
+else {
+  return new Complex(
+      0.5 * Math.sqrt(2.0 * (r + x.re)),
+      -0.5 * Math.sqrt(2.0 * (r - x.re))
+  );
+}
+ +

This is the mathematical core that we want to send to Herbie.

+ +

Converting problematic code to Herbie input

+ +

+ In this code, x is of type Complex, a + data structure with multiple fields. Herbie only deals with + floating-point numbers, not data structures, so we will treat the + input x as two separate inputs to + Herbie: xre and xim. We'll also pass + each field of the output to Herbie separately. +

+ +

+ This code also branches between non-negative x.im and + negative x.im. It's usually better to send each + branch to Herbie separately. So in total this code turns into four + Herbie inputs: two output fields, for each of two branches. +

+ +

Let's focus on first field of the output for the case of + non-negative x.im.

+ +

The variable r is an intermediate variable in this + code block. Intermediate variables provide Herbie with crucial + information that Herbie can use to improve accuracy, so you want to + expand or inline them. The result looks like this:

+ +
0.5 * sqrt(2.0 * (sqrt(xre * xre + xim * xim) + xre))
+ +

Recall that this code is only run when x.im is + non-negative (but it runs for all values of x.re). So, + select the full range of values for x.re, but restrict + the range of x.im, like this: + +

+ Restricting the input range to xim >= 0. +
+ + This asks Herbie to consider only non-negative + values of xim when improving the accuracy of this + expression.

+ +

Using Herbie's results

+ +

Herbie will churn for a few seconds and produce an output, + perhaps something like this:

+ +
+ +
Herbie's version of the complex square root expression.
+
+ +

Herbie's algorithm is randomized, so you likely won't see the + exact same thing. For example, the branch expression xre ≤ + -4.780438341784697e-111 will probably have some other really + small number. And perhaps Herbie will choose slightly different + expressions. But the result should be recognizably similar. In this + case, Herbie reports that the initial expression had 38.7 bits of + error, and that the output has 29.4.

+ +

It's a little harder to describe what Herbie found wrong with the + original expression, and why its new version is better—it is due to + a floating-point phenomenon called “cancellation”. But you can get + some insight from the error plot just below the program block. + Select the xim variable just below the plot, and you + will see something like this:

+ +
+ +
Herbie's error plot for the complex square root expression.
+
+ +

There's a lot going on here. Along the horizontal axis, you have + the various values of xim. Note that the graph is + log-scale, and includes only non-negative values thanks to our + precondition. The value 1 is in the middle; to the left are values + with small exponents close to zero, and to the right you have values + with large exponents approaching infinity.

+ +

The vertical axis measures bits of error, from 0 to 64. Lower is + better. There are two lines drawn: a red one for the original + expression and a blue one for Herbie's version. You can see from the + plot that as xim gets smaller (toward the left, closer + to zero), Herbie's improvement becomes more and more significant. + You can also see that for very large values of xim, the + original program had maximal error (in fact, it overflows) but the + Herbie's version is better, though not great.

+ +

Of course, your exact output will differ a bit from the + screenshots and descriptions here, because Herbie is randomized.

+ +

Now that you have the more accurate version of this expression, + all you need to do is insert it back into the program:

+ +
var r = Math.sqrt(x.re * x.re + x.im * x.im);
+// Herbie version of 0.5 * Math.sqrt(2.0 * (r + x.re))
+var re;
+if (x.re <= -4.780438341784697e-111) {
+    re = Math.abs(x.im) * Math.sqrt(0.5) / Math.sqrt(r - x.re);
+} else if (x.re <= 1.857088496624289e-105) {
+    re = 0.5 * Math.sqrt(2.0 * (x.re + x.im));
+} else if (x.re <= 117.16871373388169) {
+    re = 0.5 * Math.sqrt(2.0 * (r + x.re));
+} else if (x.re <= 5.213930590364927e+88) {
+    re = 0.5 * Math.sqrt(2.0 * (x.re + x.im));
+} else {
+    re = 0.5 * Math.sqrt(2.0 * (x.re + x.re));
+}
+if (x.im >= 0) {
+  return new Complex(
+      re,
+      0.5 * Math.sqrt(2.0 * (r - x.re))
+  );
+}
+else {
+  return new Complex(
+      0.5 * Math.sqrt(2.0 * (r + x.re)),
+      -0.5 * Math.sqrt(2.0 * (r - x.re))
+  );
+}
+ +

Note that I've left the original code in place in a comment. As + Herbie gets better, you can re-run it on this original expression to + see if it comes up with improvements in accuracy.

+ +

By the way, for some languages, like C, you can use the drop-down + in the top-right corner of the gray program block to translate + Herbie's output to that language.

+ +

Next steps

+ +

With this change, we've made this part of the complex square root + function much more accurate, and we could repeat the same steps for + the other branches and other fields in this program. You now have a + pretty good understanding of Herbie and how to use it. + Please let us know if + Herbie has helped you, and check out + the documentation to learn more about + Herbie's various options and outputs.

+ + + diff --git a/www/doc/1.7/using-cli.html b/www/doc/1.7/using-cli.html new file mode 100644 index 000000000..ad7c67123 --- /dev/null +++ b/www/doc/1.7/using-cli.html @@ -0,0 +1,88 @@ + + + + + Using Herbie from the Command Line + + + + + +
+ +

Using Herbie from the Command Line

+
+ +

Herbie can be used from the command-line or + from the browser. This page covers + using Herbie from the command line.

+ +

The Herbie shell

+ +

+ The Herbie shell lets you interact with Herbie: you type in input + expressions and Herbie prints their more accurate versions. Run + the Herbie shell with this command: +

+ +
herbie shell
+Herbie 1.4 with seed 2098242187
+Find help on https://herbie.uwplse.org/, exit with Ctrl-D
+herbie> 
+ + +

+ Herbie prints a seed, which you can use to + reproduce a Herbie run, and links you to documentation. Then, + it waits for inputs, which you can type directly into your + terminal in FPCore format: +

+ +
herbie> (FPCore (x) (- (+ 1 x) x))
+(FPCore
+  (x)
+  ...
+  1.0)
+ +

Herbie suggests that 1 is more accurate than the + original expression (- (+ 1 x) x). The + the ... elides + additional information provided + by Herbie.

+ +

The Herbie shell makes it easy to play with different expressions + and try multiple variants, informed by Herbie's advice.

+ +

Batch processing FPCores

+ +

+ Alternatively, you can run Herbie on a file with multiple + expressions in it, writing Herbie's versions of each to a file. + This mode is intended for use by scripts. +

+ +
herbie improve bench/tutorial.fpcore out.fpcore
+Starting Herbie on 3 problems (seed: 1809676410)...
+  1/3   [   1.799s]   39→ 0     Expanding a square
+  2/3   [   3.256s]    0→ 0     Commute and associate
+  3/3   [   0.937s]   29→ 0     Cancel like terms
+ +

+ The output file out.fpcore contains more accurate + versions of each program: +

+ +
;; seed: 1809676410
+
+(FPCore (x) ... 1.0)
+(FPCore (x) ... (* x (+ x 2.0)))
+(FPCore (x y z) ... 0.0)
+ +

+ Note that output file is in the same order as the input file. For + more control over Herbie, see the documentation of + Herbie's command-line options. +

+ + + diff --git a/www/doc/1.7/using-web.html b/www/doc/1.7/using-web.html new file mode 100644 index 000000000..004bece61 --- /dev/null +++ b/www/doc/1.7/using-web.html @@ -0,0 +1,105 @@ + + + + + Using Herbie from the Browser + + + + + +
+ +

Using Herbie from the Browser

+
+ +

+ Herbie rewrites floating point expressions to + make them more accurate. Herbie can be used + from the command-line or from the + browser; this page is about using Herbie from the browser.

+ + +

The Herbie web shell

+ +

+ The Herbie web shell lets you interact with Herbie through your + browser, featuring a convenient input format. The web shell is the + friendliest and easiest way to use Herbie. Run the Herbie web + shell with this command: +

+ +
herbie web
+ +

After a few seconds, the web shell will rev up and direct your + browser to Herbie:

+ +
herbie web
+Herbie 1.6 with seed 841489305
+Find help on https://herbie.uwplse.org/, exit with Ctrl-C
+Your Web application is running at http://localhost:8000/.
+Stop this program at any time to terminate the Web Server.
+ +
+ A screenshot of the Herbie web shell main page. +
+ +

+ Type expressions in standard mathematical syntax (parsed + by Math.js). For each input variable, + specify the range of values that Herbie should consider when trying + to improve the expression. Hit the "Improve with Herbie" button to have + Herbie attempt to improve the expression. +

+ +
+ +
Herbie shows improvement logs as it works.
+
+ +

+ The web shell reports Herbie's progress and redirects to a + report once Herbie is done. +

+ +

+ The web shell can also automatically save the generated reports, + and has many other options you might + want to explore. +

+ + +

Batch report generation

+ +

A report can also be generated directly + from a file of input expressions:

+ +
herbie report bench/tutorial.fpcore output/
+Starting Herbie on 3 problems (seed: 1809676410)...
+  1/3   [   1.799s]   39→ 0     Expanding a square
+  2/3   [   3.256s]    0→ 0     Commute and associate
+  3/3   [   0.937s]   29→ 0     Cancel like terms
+ +

+ This command asks Herbie to generate a report from the input + expressions in bench/tutorial.fpcore and to save the report in + the directory output/. It's best if that directory + doesn't exist before running this command. +

+ +

+ Once generated, open output/results.html in your + favorite browser (but see the FAQ if you're + using Chrome). That page summarizes Herbie's results for all + expression in your input file, and you can click on individual + expressions to see their report. +

+ +

Batch report generation is the most informative way to run Herbie + on a large collection of inputs. Like the web shell, it can be + customized through command-line options, + including parallelizing Herbie with multiple threads.

+ + + + diff --git a/www/doc/1.7/web-input.png b/www/doc/1.7/web-input.png new file mode 100644 index 000000000..58bfd8774 Binary files /dev/null and b/www/doc/1.7/web-input.png differ diff --git a/www/doc/1.7/web-main.png b/www/doc/1.7/web-main.png new file mode 100644 index 000000000..6a53ec356 Binary files /dev/null and b/www/doc/1.7/web-main.png differ diff --git a/www/doc/1.7/web-progress.png b/www/doc/1.7/web-progress.png new file mode 100644 index 000000000..3ea032b59 Binary files /dev/null and b/www/doc/1.7/web-progress.png differ diff --git a/www/doc/latest b/www/doc/latest index 400122e60..dc39e58d9 120000 --- a/www/doc/latest +++ b/www/doc/latest @@ -1 +1 @@ -1.5 \ No newline at end of file +1.6 \ No newline at end of file