Skip to content

Performance regression in SBV library between make mode and expression-evaluation mode

I'm working an understanding a SBV performance issue where the same program finishes in 1.5 minutes using ghc -e ... compared to 15 minutes in make mode. Those times are on a mac, on my linux boxes make mode finishes in 42 minutes while eval mode finishes 1 min 50 seconds.

My purpose with this ticket

I'm not familiar with the code paths for the -e mode. So I'm trying to understand the differences in GHC when run in make and when run in expr-eval mode. I suspect that this isn't only a GHC issue but also a SBV issue, in which case I'd like to understand the GHC side and patch the SBV side. So any help appreciated!

What I know so far

  • This same failure mode occurs with 9.4.x, 9.2.x, 8.10.7 and 8.8.
  • the sha256 program (as opposed to the sha512) does not exhibit such a difference between -e and -make.
  • compiling the program in make mode with -O0 does not make a difference, i.e., I still observe 42 minutes vs 1.9 minutes difference.
  • the output of both methods is identical
  • compiling with -fno-state-hack makes no difference (this was a guess)
  • sbv 8.4 is the first release of sbv to include the test program. This was using base-4.11.0 (ghc-8.4.1)
  • This still occurs with sbv-8.4 and ghc-8.4.1
  • Also occurs with ghc 7.04

What the test program is doing

The test program is doing a lot of IO. Its generating a C program to calculate a sha512 function through sbv. This does not use z3, and occurs completely on the haskell side. I'll update this as I know more.

Edited by jeffrey young
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information