21–30 of 43 posts
Is there any introductory course for these kind of stuff?
It has a pretty large cost for small amounts of work, but Z3 seems like a good dependency for an optimizing compiler - asking it to do nothing from C++ seems to cost about 4ms, which isn't cheap but you can batch these things. I'm not sure exactly what data structures LLVM uses to track knowledge about the program it's optimising, but with SMT you can ask the solver very non-trivial questions about the code and eithe…
Google's one step ahead of you there :) https://github.com/google/souper
First time I see Z3 in the wild. Bonus points for the CLI friendly model checker, but lisp syntax... is less legible than TLA+ imho. Gotta give it a try someday to see for myself if the experience of creating the spec is better.
I've developed theorem provers with more natural syntax, and in retrospect simpler grammars are better. The stone cold truth is that most people aren't interested in using theorem provers directly; instead, they're programmatically generating queries. Simpler grammar = easier to generate, and that out-weighs direct usability.
In my next system I'll be supporting both types of grammars in the parser.
It has a pretty large cost for small amounts of work, but Z3 seems like a good dependency for an optimizing compiler - asking it to do nothing from C++ seems to cost about 4ms, which isn't cheap but you can batch these things. I'm not sure exactly what data structures LLVM uses to track knowledge about the program it's optimising, but with SMT you can ask the solver very non-trivial questions about the code and eithe…
First time I see Z3 in the wild. Bonus points for the CLI friendly model checker, but lisp syntax... is less legible than TLA+ imho. Gotta give it a try someday to see for myself if the experience of creating the spec is better.
Z3 is intended as more of a backend for higher-level languages, like TLA+, to use in model checking. I would be surprised if anyone were writing specs in the input language directly.
It has a pretty large cost for small amounts of work, but Z3 seems like a good dependency for an optimizing compiler - asking it to do nothing from C++ seems to cost about 4ms, which isn't cheap but you can batch these things. I'm not sure exactly what data structures LLVM uses to track knowledge about the program it's optimising, but with SMT you can ask the solver very non-trivial questions about the code and eithe…
Well, optimizing similar to how Rust guides the developer to write more optimized code. Comparing them is comparing apples to oranges however. There are many ways to get there. With Z3 you can do symbolic testing and it’s very much about defining if the expected output of the constructed IR is the same as the real output. When it comes to the IR I like to think of Z3 as almost an abstract assembler. Usually a separat…
You can already get some serious performance increases by giving the compiler information - if I assert two arrays have equal length in D, I can then add an inline statement equivalent to GCC's builtin_unreachable and the compiler does s surprisingly good job of eliding length checks that it normally can't assume.
It has a pretty large cost for small amounts of work, but Z3 seems like a good dependency for an optimizing compiler - asking it to do nothing from C++ seems to cost about 4ms, which isn't cheap but you can batch these things. I'm not sure exactly what data structures LLVM uses to track knowledge about the program it's optimising, but with SMT you can ask the solver very non-trivial questions about the code and eithe…
Google's one step ahead of you there :) https://github.com/google/souper
My scheme would really be a cheap way of getting some symbolic optimisations for free during the early days of a compiler, I don't think it's a realistic strategy for all compilation.
Is there any introductory course for these kind of stuff?
Is there any introductory course for these kind of stuff?
I'm giving a tutorial in a couple of days. Vids will be up later. https://github.com/philzook58/z3_tutorial
- rise4fun https://rise4fun.com/z3/tutorialcontent/guide
- https://ericpony.github.io/z3py-tutorial/guide-examples.htm
- Programming Z3 -https://theory.stanford.edu/~nikolaj/programmingz3.html
- Nikolaj Bjorner's tutorial https://youtu.be/nGwyNmsxX6I
- Hakank's examples http://www.hakank.org/z3/
- Yurichev's book "SMT by Example" https://yurichev.com/writings/SAT_SMT_by_example.pdf
- http://hackage.haskell.org/package/sbv
- https://www.youtube.com/watch?v=ruNFcH-KibY Tikhon Jelvis - Analyzing Programs with Z3
- https://www.youtube.com/watch?v=rvPWDgJc0O4&ab_channel=ACMSI... - Nadia Polykarpova on Z3
- SAT SMT school https://sat-smt.in/
- Emina Torlak's course https://courses.cs.washington.edu/courses/cse507/19au/calend...
- Lindsey Kuper - SMT Solving and Solver-Aided Systems http://composition.al/CSE290Q-2019-09/
It has a pretty large cost for small amounts of work, but Z3 seems like a good dependency for an optimizing compiler - asking it to do nothing from C++ seems to cost about 4ms, which isn't cheap but you can batch these things. I'm not sure exactly what data structures LLVM uses to track knowledge about the program it's optimising, but with SMT you can ask the solver very non-trivial questions about the code and eithe…
TBF this isn't always true. Unison[1] characterizes register allocation as geometric packing, a solution which is very robust on irregular architectures like Hexagon. GPUs have problems like extremely large register files that the literature doesn't treat very well which some solvers might help with, etc. And fully automated solvers are useful as complementary tools for any compiler, like Souper or Alive2. They're certainly good for specialized tools, especially validators.
Personally, I think to prototype and construct a general program analysis quickly, you're better off with a tool like a Datalog variant. Souffle is pretty good. If you want to make generalized optimizers cheaper and more quickly, especially ones that can explore emergent optimizations that heuristics may not discover, solutions like equality saturation might be a better starting point[2] (it's kind of like a generalized version of a global cost-based SQL optimizer -- so the engine implicitly combines small rules together into more powerful rules.) Specialized solvers for particular logics or domains are still going to be valuable beyond that, of course. If you're writing a production compiler, your job is still cut out for you no matter what.
If someone smart out there could "just" write an SMT solver and a robust Datalog that are efficient and easy to integrate as Lua ("drop in C files and go"), I'd fund that work.
[1] https://unison-code.github.io/ [2] https://egraphs-good.github.io/