Proposal: BLOKE - Optimize BRIL with STOKE

[keikun555]

What will you do? We seek to apply STOKE to Bril. If time permits, we will extend the two-stage process in STOKE with simulated annealing and measure its impact in synthesis time and resulting optimized program.

How will you do it?

1. Read the STOKE paper to understand necessary details.
2. Gauge if we can use stochopy for this project.
   1. If not applicable, implement our own stochastic search algorithm. If we need to do this, there might not be enough time to implement simulated annealing with respect to the performance component.
3. Generate test cases for incremental cost function development.
4. Implement the two cost functions as done in STOKE. The first function where the performance component is completely ignored to find correct programs, and the second function to use the correct programs as starting points that includes the performance component.
   1. Incrementally implement a transpiler from Bril to Z3. This can become its own library.
   2. Use the transpiler to translate Bril to Z3 to show equivalance of original program and optimized program.
5. Implement the cost functions into stochopy or our in-house stochastic optimization implementation.
6. Measure Bril STOKE with the original two stages as baseline. In particular, we are interested in
   • optimizer runtime; and
   • the resulting optimized program performance, including runtime and total dynamic instructions executed using the brili -p command in the main BRIL repository .
7. Implement simulated annealing with regards to performance component into the cost function.
8. Measure simulated annealing impacts on Bril on STOKE.

How will you empirically measure success? We will measure the Bril STOKE optimizer runtime as well as the total dynamic instructions executed on the resulting Bril STOKE optimized program.

Team members: @keikun555

[sampsyo]

Awesome! I really like the idea of reusing an existing optimizer as much as possible for this—especially because it would be possible to sink a lot of time into making your own and to see very little progress result.

I vaguely recall we may have chatted about this before, but for the symbolic verification step, you might consider salvaging any reusable parts of this previous verifier project, although it doubtless will not apply directly to your use case.

Here's one high-level question: are you planning on doing this to individual basic blocks, or will it work on entire programs (with control flow, and possibly multiple functions)?

[keikun555]

For now I assume the input programs are:

• Loop-free (STOKE assumes this as well)
• memory-operation-free
• speculation-free
• character-operation-free
• call-free (so no multiple functions)
• print-free

I might add support for memory operations and print statements using Z3's theory of Arrays, if time permits.

I was able to lift the branching br operation into Z3 using z3.If here. So we can lift multiple blocks.

It is certainly possible to call functions, it's just tricky because we will need to bookkeep how many times the function has been called.

Right now I have finished the equivalence checkers for Bril programs given the above assumptions. I am moving on to the MCMC part of BLOKE using an in-house implementation of MCMC with a simulated annealing component. It turns out that stochopy is not what we want, because the package is for continuous function optimization.

[sampsyo]

Excellent; sounds great!