New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Better spreading SMT solver load? #863

Open

chadbrewbaker opened this issue Dec 12, 2022 · 0 comments

chadbrewbaker commented Dec 12, 2022

I was playing with zstd yesterday. The Makefile is easy to play with, just do:

# sudo service redis-server start  # Remember to turn Redis on.
 CC=$SOUPER_BIN/sclang make -j

(Aside) The zstd runtime was worse worse with Souper. Is Souper is breaking cache boundaries or branch predictions?

I noticed Souper had a really hard time spreading load across cores when compiling a wllvm fat IR file.

# What I remember running, might have a typo
LLVM_COMPILER=clang CC=wllvm make -j
extract-bc pkg-config
$SOUPER_BIN/sclang pkg-config.bc

Is there a flag I am missing to break Z3 solves into smaller chunks, or should I noodle on a PR?

Also, similer to gcc -fverbose-asm, how would you get the optimizations Souper produces printed as assembler comments?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment