Bend to Go
This project translates programs from a new language, Bend, into Go, a language that many companies already use. The goal is simple. The translated program must give the same answers and run at least as fast.
The idea in one picture
Why do this?
Bend lets a programmer write down what a program must do, then have the computer prove that the program does it. That is very useful when an AI writes the code, because you do not have to trust the AI.
But few teams use Bend today. Many teams use Go. With this translator, a team can get checked code in a language that they can already read and run.
What makes it hard
Bend normally turns programs into C, one of the fastest languages. It can also run them on a graphics card. So Go has to compete with the best of both.
Think of a processor as a few expert chefs. A graphics card is thousands of helpers who are fast only when they all do the same step together. Some jobs suit the chefs. Other jobs suit the helpers. Our translator must choose well and split the work.
Go also has a cleaner. The cleaner stops to find and remove memory that a program no longer needs. This is convenient, but programs that make millions of small objects keep the cleaner very busy.
The score so far
9 of 16
We race Go against Bend's C version on 16 test programs. C gets its faster time from the processor or the graphics card. Go wins a test if it matches or beats that time. The goal is 16 of 16. This score comes from the last full run on our Linux computer.
Colored tiles are wins. Gray tiles are still behind.
The 7 races we still lose
Shorter bars are better. The times are in seconds.
We are closing the gap. Bitonic took 11.3 seconds in the last full run and now takes about 2.1. Matmul took 2.75 seconds and now takes about 0.8. Merkle and kmeans look the hardest, because starting the graphics card takes almost as long as merkle's whole target time.
Speed tricks that worked
Reuse the box
A program often throws away a box of data and then immediately asks for a new one. We keep the old box and refill it. The cleaner then has less work.
Buy boxes in bulk
Each worker gets a large tray of memory and takes boxes from it. This is faster than asking for one box at a time.
Practice run
With a new option, the translated program runs once while Go watches which parts are busy. Go then tunes those parts. One test became 22% faster.
Use the graphics card
The translator can now write graphics card code for suitable work. The processor and the graphics card can share a job, or race each other to finish it.
Does it give the right answers?
Speed is useless if the answers are wrong, so every change gets a large test. We compare the Go program's output with the expected output.
- 644 of 654 test programs pass.
- 1168 of 1170 test libraries pass.
Most failures are about exact timing, error message wording, or unusual characters. Two library failures are crashes that happen only on the MacBook. These numbers come from the MacBook, because the newest version has not had a full run on Linux.
The tests also caught a real bug. On the MacBook, two programs gave slightly wrong answers, because Go merged two math steps into one and rounded differently. We fixed this by writing the math so that Go cannot merge the steps.
What comes next
- Tidier trees. Store data in one neat block instead of scattering it. A hand-written test beat C on bitonic with 1.37 seconds against 1.55. The translator cannot do this yet.
- Faster graphics card start. This is the main problem for merkle and kmeans.
- A full run on Linux. This gives the new official score.
Longer term, we could add a tool that makes any ordinary Go program run in parallel, support Apple graphics chips, and test the C and Go versions against each other with random programs. Work on the parallel tool has started, but it cannot use the graphics card yet.
Honest limits
- The project is an experiment. The work is not published.
- We check the translation with tests. We do not have a mathematical proof that the Go matches the Bend.
- The times in the 7 races come from different runs, so a new full run can change them.
Words used here
- Language
- A way to write instructions for a computer. Bend, Go and C are languages.
- Processor (CPU)
- The main chip in a computer. It has a few powerful workers.
- Graphics card (GPU)
- A chip with thousands of simple workers.
- Parallel
- Many workers do parts of a job at the same time.
- Memory
- The space where a running program keeps its data.
- Cleaner (garbage collector)
- The part of Go that finds and frees memory that a program no longer needs.