Solver result caching

[m-yac]

This PR adds a solver-backend-aware system for caching SMT solver results.

• Check out the Caching Solver Results section of the SAW manual for a description and an example of this feature.
• Check out the top of SolverCache.hs for more information on how the system works internally.

Example (Out of date, see the manual for an update)

First we enable caching to disk and run a few queries:

sawscript> enable_experimental 
sawscript> set_solver_cache_path "test.cache"
sawscript> prove_print w4 {{ \(x:[64]) -> 2 * x == x + x }}
[18:32:12.839] Caching result: 4b6a78359fb7b9cc (What4 v1.3-29-g6c462cd, Z3 version 4.8.7 - 64 bit)
[18:32:12.840] Theorem (let { x@1 = Vec 64 Bool
      x@2 = TCNum 64
      x@3 = PRingSeqBool x@2
    }
 in (x : x@1)
-> EqTrue
     (ecEq x@1 (PEqSeqBool x@2)
        (ecMul x@1 x@3 (ecNumber (TCNum 2) x@1 (PLiteralSeqBool x@2)) x)
        (ecPlus x@1 x@3 x x)))

sawscript> prove_print z3 {{ \(x:[64])(y:[64]) -> y == x }}
[18:32:18.640] Caching result: 91ad8684b52cf5d1 (SBV 9.2, Z3 version 4.8.7 - 64 bit)

Stack trace:
"prove_print" (<stdin>:1:1-1:12)
prove: 1 unsolved subgoal(s)
Invalid: [x = 18446744073709551615, y = 0]

Next, we can use print_solver_cache to see what was cached (print_solver_cache "" will show all entries) and print_solver_cache_stats to get statistics about how the solver cache has been used so far this run:

sawscript> print_solver_cache "4b6a78359fb7b9cc"
[18:32:30.093] SHA: 4b6a78359fb7b9cc2c6ca3868b07a6e156a0ab17a9d40ef4ec2d5a48174f00cf
[18:32:30.093] - Result: unsat
[18:32:30.093] - Solver: "W4 ->z3"
[18:32:30.093] - Versions: What4 v1.3-29-g6c462cd, Z3 version 4.8.7 - 64 bit

sawscript> print_solver_cache "91ad8684b52cf5d1"
[18:33:19.790] SHA: 91ad8684b52cf5d1cc586cbe37a8896eee2eb3783cdb8d75d1f602ab66e9bcb5
[18:33:19.790] - Result: sat [(0,18446744073709551615),(1,0)]
[18:33:19.790] - Solver: "SBV->Z3"
[18:33:19.790] - Versions: SBV 9.2, Z3 version 4.8.7 - 64 bit

sawscript> print_solver_cache_stats
[18:33:47.962] == Solver result cache statistics ==
[18:33:47.962] - 2 results cached in /.../test.cache
[18:33:47.962] - 2 insertions into the cache so far this run (0 failed attempts)
[18:33:47.962] - 0 usages of cached results so far this run (0 failed attempts)

Finally, we can start up saw again and verify that these results will be used – in particular, order doesn't matter, local variable names don't matter, but the solver backend does:

sawscript> enable_experimental 
sawscript> set_solver_cache_path "test.cache"
sawscript> prove_print z3 {{ \(new1:[64])(new2:[64]) -> new2 == new1 }}
[18:34:56.895] Using cached result: 91ad8684b52cf5d1 (SBV 9.2, Z3 version 4.8.7 - 64 bit)

Stack trace:
"prove_print" (<stdin>:1:1-1:12)
prove: 1 unsolved subgoal(s)
Invalid: [new1 = 18446744073709551615, new2 = 0]

sawscript> prove_print w4 {{ \(new1:[64])(new2:[64]) -> new2 == new1 }}
[18:35:02.952] Caching result: 6ab538591daf0e8f (What4 v1.3-29-g6c462cd, Z3 version 4.8.7 - 64 bit)

Stack trace:
"prove_print" (<stdin>:1:1-1:12)
prove: 1 unsolved subgoal(s)
Invalid: [new1 = 18446744073709551615, new2 = 0]

sawscript> prove_print w4 {{ \(new:[64]) -> 2 * new == new + new }}
[18:35:08.710] Using cached result: 4b6a78359fb7b9cc (What4 v1.3-29-g6c462cd, Z3 version 4.8.7 - 64 bit)
[18:35:08.710] Theorem (let { x@1 = Vec 64 Bool
      x@2 = TCNum 64
      x@3 = PRingSeqBool x@2
    }
 in (new : x@1)
-> EqTrue
     (ecEq x@1 (PEqSeqBool x@2)
        (ecMul x@1 x@3 (ecNumber (TCNum 2) x@1 (PLiteralSeqBool x@2))
           new)
        (ecPlus x@1 x@3 new new)))

There are also two other ways to interact with solver caching:

• The enable_solver_cache command, which turns on solver result caching in memory but does not save anything to disk. If set_solver_cache_path is later run, everything from memory is written to disk. If set_solver_cache_path is never run, the cached results are forgotten after saw execution ends.
• The SAW_SOLVER_CACHE_PATH environment variable, which has the same behavior as calling set_solver_cache_path with the value of the variable at the start of execution.

A quick and dirty test on a larger example shows that there is a performance improvement – in the case of intTests/test_w4/prims.saw on my machine (see below) it takes 3.467s to run the test with caching turned off, 3.541s to run the test with caching turned on but nothing in the cache (so 0.1s of extra time spent caching the entries), and 2.540s to run the test with a loaded cache (so 1s less time calling solvers, a ~30% speed increase). I imagine for files with more complicated SMT queries than prims.saw (which mostly contains zeroth-order queries such as (16:[8]) >> 3 == 2), this speed increase can get much larger.

$ time ./bin/saw intTests/test_w4/prims.saw > /dev/null
./bin/saw intTests/test_w4/prims.saw > /dev/null  2.75s user 0.58s system 96% cpu 3.467 total
$ time SAW_SOLVER_CACHE_PATH="prims.cache" ./bin/saw intTests/test_w4/prims.saw > /dev/null
SAW_SOLVER_CACHE_PATH="prims.cache" ./bin/saw intTests/test_w4/prims.saw >   2.74s user 0.57s system 93% cpu 3.541 total
$ time SAW_SOLVER_CACHE_PATH="prims.cache" ./bin/saw intTests/test_w4/prims.saw > /dev/null
SAW_SOLVER_CACHE_PATH="prims.cache" ./bin/saw intTests/test_w4/prims.saw >   1.99s user 0.43s system 95% cpu 2.540 total

Additional Changes

Note that this PR also makes the following changes:

• The Setup.hs script now also includes AIG, What4, and SBV version information in GitRev.hs, used by Builtins.hs and Interpreter.hs to generate solver backend version information for caching. Accordingly the saw-script library and executable now also depend on GitRev in saw-script.cabal.
• Instead of every solver backend individually calling sequentToSATQuery on its given Sequent, we now call sequentToSATQuery in one place (applyProverToGoal) and pass the resulting SATQuery to each backend directly.

[bboston7]

@bboston7 has some thoughts on this.

To clarify for the curious: I used sqlite extensively at my previous job and from experience it gets a bit tricky when concurrency is involved. You'll notice that the page on when to use sqlite calls out high levels of concurrent writes as something sqlite does not handle well. In practice there are tricks to make this better (such as enabling WAL mode), but still any application that makes use of concurrent writes (or reads while writing) will need to handle sqlite errors that can arise at any point a query is made. Usually a simple "wait and try again" approach works, but ultimately it can take a few months of tweaks to get everything working well.

Additionally, sqlite's performance can vary significantly depending on how you structure your tables and queries. We would probably want to take the time to design that out before implementing it.

It's not that I think we shouldn't use a database for this at some point, I just wanted to push back on the idea that it's a quick change to use sqlite in a concurrent application like this.

[kquick]

Can you say more about that What4 cache file that is next to the Z3 cache file?

What4 tests currently do determine solver versions; it seems reasonable that this could be moved into the what4 library itself and surfaced somewhere in the API: https://github.com/GaloisInc/what4/blob/master/what4/test/ProbeSolvers.hs#L39

My opinion is that we definitely want a solver-specific cache (different solvers can give different answers) and a version-specific solver cache (does a new version of a solver still give the same answers?).

[m-yac]

Can you say more about that What4 cache file that is next to the Z3 cache file?

Not sure exactly what you're asking, but currently the cache files all have the same format: the filename is the hash of the saw-core term which is passed to the solver backend, and the solver version is just saved as a string in that file.

What4 tests currently do determine solver versions; it seems reasonable that this could be moved into the what4 library itself and surfaced somewhere in the API: https://github.com/GaloisInc/what4/blob/master/what4/test/ProbeSolvers.hs#L39

Amazing - thanks for the link! I'm going to use this to quickly get a version where we also cache by solver version up and running and I'll update the example.

[kquick]

Can you say more about that What4 cache file that is next to the Z3 cache file?

Not sure exactly what you're asking, but currently the cache files all have the same format: the filename is the hash of the saw-core term which is passed to the solver backend, and the solver version is just saved as a string in that file.

Oh, I misread the original and thought you only had one query, but you generated two different queries from the sawscript> prompt. It's clear to me now.

[eddywestbrook]

Let's be clear about goals: the primary goal of this SMT caching feature is to speed up CI. It could maybe be useful in other contexts, but CI is the main use case of interest.

Now, the easiest way to use this sort of cache in github CI is to use the github cache action, which gives each workflow its own local version of the cache. There doesn't seem to be a straightforward way to get different workflows to share a cache, and in fact different workflows will probably make different queries anyway on the whole, so separating the caches to different CI workflows is probably a good thing in the end. Thus, we only really have to worry about concurrency inside a single workflow. Some of our existing workflows are completely sequential, since they are just a single SAW file. But things like the intTests run a bunch of different tests, which at least should be run concurrently, though I'm not sure if they currently are.

Given all of this, I would say we only need to support a low degree of concurrency. SQLite seems feasible, but OTOH the one file per query approach seems intriguing as well, for the reasons you outlined. And in fact, the one file per query approach could actually have better performance, because most of the concurrent processes in a CI run will be making different SMT queries: the one file per query approach would allow these to happen concurrently, while SQLite would serialize the writes. It should even be straightforward to correctly handle the concurrency here: the O_CREAT plus O_EXCL flags to the open syscall should make file creation an atomic action, and the SMT cache could be implemented so that only the process that creates the cache file gets to write to it. A reader could still see an SMT cache file that has been only partially written, but the failure case should be either to try again or, as @m-yac says above, to just do the query anyway. So maybe the existing one file per SMT query approach is the way to go. And, as @m-yac says, it's the easiest, so maybe we should just try it for now and see how it fares in the CI system.

My suggestion for SMT solver versions is this: each SMT cache should be globally marked when it is created with the versions of all the solvers it was created with. Whenever a CI workflow is started and the SMT cache is loaded / installed, some process should check those SMT solver versions against the current versions that are installed, and just wipe the cache if any of those solver versions have changed. The expectation is that we are only occasionally going to change SMT solver versions, and when we do, we don't expect to go back to an old version, so there is no reason to keep the old cached values around. I could imagine trying to only wipe the cached queries corresponding to the particular solver whose version was updated, but then you have to associate each query with the solver it was made against, and this creates additionally complexity. Again, we are only occasionally going to change SMT solver versions for any of our solvers, so we might as well save ourselves the trouble and just wipe the whole SMT cache.

Then, for each copy of SAW that gets run in the workflow, the SMT caching component(s) will check if the solver versions it sees are the same as those given in the SMT cache. If not, then something is wrong with the CI setup. It should probably raise an error, though I could imagine cases where we want to turn that into a warning instead, though it should be a stern warning. :) If it's a warning and not an error, it should at least be something that the user can easily see when checking the CI logs.

That is my 2 cents. Which buys a lot of text these days, apparently.

[m-yac]

Caching is now dependent on the solver used as well as the version of the solver used. Thanks @kquick for the pointer!

I updated the example in the PR description, but here's the short of it:

sawscript> prove_print z3 {{ \(x:[64])(y:[64]) -> y == x }}
[01:11:51.457] Caching result: 91ad8684b52cf5d1 (SBV 9.2, Z3 version 4.8.7 - 64 bit)
...
sawscript> prove_print z3 {{ \(new1:[64])(new2:[64]) -> new2 == new1 }}
[01:16:09.078] Using cached result from disk: 91ad8684b52cf5d1 (SBV 9.2, Z3 version 4.8.7 - 64 bit)
...
sawscript> prove_print w4 {{ \(new1:[64])(new2:[64]) -> new2 == new1 }}
[01:16:46.052] Caching result: a7289621deecd800 (what4 v1.3-29-g6c462cd, Z3 version 4.8.7 - 64 bit)

I also updated the last question in the PR description, since now I have questions about the implementation I went with.

[kquick]

My suggestion for SMT solver versions is this: each SMT cache should be globally marked when it is created with the versions of all the solvers it was created with.

I'm actually more in favor of including the SMT version in the file (and as part of the input to the hash for the file's name). I don't see it as a lot of additional work, and while the primary utilization of the cache is intended to be the CI, the caching is being implemented by saw-script itself and not the CI, so I think it should be robust against other uses. It's also worth noting that the what4 repo tests multiple different solver versions during its CI and that might be desirable for saw at some future point as well.

[weaversa]

Along with saving/hashing against solver version, I suggest also saving/hashing against any command line options to the solver, in case they also change. Our CI scripts mostly use the Python interfaces though both saw-remote-api and cryptol-remote-api, so it would be _great_ to give both python interfaces access to these new caching options.

…

On Fri, May 19, 2023 at 9:51 PM Kevin Quick ***@***.***> wrote: My suggestion for SMT solver versions is this: each SMT cache should be globally marked when it is created with the versions of all the solvers it was created with. I'm actually more in favor of including the SMT version in the file (and as part of the input to the hash for the file's name). I don't see it as a lot of additional work, and while the primary utilization of the cache is intended to be the CI, the caching is being implemented by saw-script itself and not the CI, so I think it should be robust against other uses. It's also worth noting that the what4 repo tests multiple different solver versions during its CI and that might be desirable for saw at some future point as well. — Reply to this email directly, view it on GitHub <#1873 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABYQSOTGC5ST3IJQWPZHLPDXHAPSDANCNFSM6AAAAAAYICQ3C4> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[andreistefanescu]

I would suggest to use a persistent key/value store rather than a SQL database. I think LMDB is simple to use and fits well. There are haskell binding, such as lmdb-simple. Alternatively, RocksDB (https://rocksdb.org/) supports more features, but I don't think we require any here. There are haskell binding as well, such as rocksdb-haskell.

[m-yac]

I'm actually more in favor of including the SMT version in the file (and as part of the input to the hash for the file's name).

For the record, both of these things are done currently. Once I make sure the CI passes on my latest commit, I'm also going to add a clean_solver_cache command to SAW, which will delete any entries with outdated versions. This should also satisfy @eddywestbrook's concern of making sure no old entries build up on the CI.

Along with saving/hashing against solver version, I suggest also saving/hashing against any command line options to the solver

There's no easy way to save the exact command line options passed to each solver, since each backend (i.e. What4, SBV, etc.) has its own system for actually calling out to solvers. However, as part of version information we save which backend was used as well as all additional options the user provides. For example, results obtained with z3_using [tac] will have [tac] as part of the version information, so it cannot be confused with results obtained with z3 or z3_using [other_tac] or w4 (i.e. Z3 with What4 instead of SBV). Assuming What, SBV, etc. are deterministic, this should be enough information to ensure the command line options passed to the solver will always be the same if there's a cache hit.

I would suggest to use a persistent key/value store rather than a SQL database. I think LMDB is simple to use and fits well.

Wow, this is perfect – thanks for the suggestion! The one thing I wasn't sure about was how to properly handle the fact that we now have a new C dependency for saw, namely the lmdb C library. There are no official releases of LMDB from OpenLDAP so it seems the canonical way to install LMDB is to build it from source (e.g. the homebrew formula). @andreistefanescu @kquick @(anyone else) is this C library a reasonable dependency to add? Is there anything beyond updating the README and CI that we need to do when adding this dependency? As for the CI, let me know if anyone has any suggestions – I took a total guess that I'm not sure will work.

[andreistefanescu]

I'm late with this feedback, but I think LLDB should be linked statically, not dynamically. Requesting our users to install the library locally, or in CI, is a problem, and we can solve it for them. @m-yac I see from the commit history that you run into some issues with linking statically. Maybe someone with more experience with linking C libraries in haskell can help, @RyanGlScott?

[m-yac]

I'm late with this feedback, but I think LLDB should be linked statically, not dynamically.

For some reason I got the impression from reading the docs around lmdb-simple that this couldn't be done, but doing some basic research now it seems like maybe we could in fact statically link the LMDB .a files and have lmdb-simple just work?

That being said, I don't have very much time left to work on this task, and something like this doesn't seem super easy to configure and get working (especially on CI). If Ryan comes back and says it's super easy then I can try to get it working, otherwise someone else might have to jump in. But, if someone just gets lmdb-simple working with a statically-linked LMDB on the CI, I can definitely do the rest (i.e. updating the solver caching code to use lmdb-simple again).

[RyanGlScott]

Sorry, I'm missing context on the linking issues you're alluding to. Can you describe what the problem is in more detail?

[m-yac]

Sorry, I'm missing context on the linking issues you're alluding to. Can you describe what the problem is in more detail?

@RyanGlScott Originally, this PR used the lmdb-simple Haskell library for interacting with LMDB databases instead of calling out to Python. However, by default, this requires the dynamically-linked LMDB C library to be installed at runtime, the installation of which is too much to ask of every SAW user. The question: Is it possible, and if so, how easy would it be to statically link the LMDB C library when building SAW and have that work with lmdb-simple?

[RyanGlScott]

I still feel like I'm missing something. After all, the approach you are using still requires users to install LMDB themselves, but via Python instead of Haskell. I'm not sure why one approach is considered too much while the other isn't...

[m-yac]

@RyanGlScott Sorry, maybe this will be more helpful. The difference is:

1. Dynamically linking the LMDB C library requires all users to have the dynamically-linked library installed in order for the saw executable to work at all – regardless of whether or not they intend to enable solver caching. (At least, this is the observed behavior of the Haskell lmdb bindings.) Installation of this dynamically-linked library can be confusing (e.g. there is no official release) and difficult (e.g. on Windows, as we found trying to set up the CI). This requirement, that all users of SAW must now go through a potentially difficult installation to support a feature they may not even use, seems too much.
2. Calling out to a Python process at runtime only requires those users who want to enable solver caching to have Python and the Python LMDB bindings installed. Installation of these bindings is easy (pip install lmdb) and does not require installing the LMDB dynamically-linked C library. This requirement is acceptable, as it does not effect the way anyone currently uses or installs saw.
3. Statically linking the LMDB C library would not have any requirements on the user. This is the most ideal solution, but I wasn't sure whether it was possible to do it with an existing library like the Haskell lmdb bindings, which by default seem to need the LMDB dynamically-linked library.

[RyanGlScott]

OK. If I understand correctly, the issue isn't really in static vs. dynamic linking, but rather requiring users to install a third-party C library that powers an optional feature in SAW. From this perspective, I don't see that great of a difference between options (1) and (3), as statically linking against lmdb would still require users to install the C library separately on their system.

Unfortunately, this sort of thing is awkward to accomplish. I can foresee two ways to make this not terrible for SAW users, but both of them would require downstream changes to the Haskell lmdb bindings (or creating our own):

1. Have the Haskell lmdb library bundle a copy of the lmdb C library as part its sources, which are compiled when building lmdb with cabal. (This is basically the same approach that the Python lmdb bindings use, if I understand correctly.)
2. Use the same trick that Haskell's GLUT bindings use: don't link directly against lmdb, but instead call out to lmdb at runtime using dlopen/LoadLibrary. This would mean that if a user doesn't have lmdb installed when building SAW, everything would still work unless they explicitly enable caching.

Of these options, (1) would probably be easiest, considering that the Python bindings already do this.

[m-yac]

Ah, okay – thanks, Ryan! For some reason I thought static linking would work similar to (1), i.e. that the C parts would be compiled into the saw executable, and the user wouldn't have to install anything. (Shows you how much I've actually used C/C++ in my life!). Sorry if that misunderstanding was part of your confusion.

Given the amount of time I have left to work on this, I think I'd prefer to just keep the current Python solution instead of trying to write a new Haskell LMDB library. @andreistefanescu what do you think?

On another note: I think I've addressed all of your comments now, @RyanGlScott! The only things left that I think need review are the new docs I added in 0e2efb2 and bbdfdf0, as well as the question I asked about running pip install lmdb on the CI.

[RyanGlScott]

For some reason I thought static linking would work similar to (1), i.e. that the C parts would be compiled into the saw executable

To be clear, that is how static linking works. The contentious bit is where the static library comes from, i.e., whether the user has to install it themselves, or if they can use a copy of the library that is bundled with lmdb itself.

In any case, I'm fine with using the Python approach. If you want, you could file an issue to track the idea of switching to an in-Haskell solution.

[m-yac]

Okay, this is ready for review again! Here's what's been done:

• Update to use Galois' newly forked Haskell LMDB bindings (thanks, @RyanGlScott!) which now statically link with the LMDB C library. This replaces the previous messy workaround of calling out to a Python process at runtime.
• Remove the ability to cache results purely in memory. It seemed like this feature was not very useful in the first place, and it would've required extra work to keep around now that we're using the Haskell LMDB bindings as our backend. This change means enable_solver_cache was removed and now the only ways to use solver caching are through the SAW_SOVLER_CACHE_PATH environment variable and the set_solver_cache_path command
• When using the SAW_SOVLER_CACHE_PATH environment variable, don't create an LMDB database at the given path until the cache is actually used (as requested by @weaversa)
• Save the timestamp of the last time each entry was used (as requested by @weaversa)
• Move the Python interface for interacting with the solver cache to the SAW Python API (solver_cache.py) since that interface is quite useful and should be made accessible somewhere. Unlike the set of solver caching commands available in saw-script, this interface can be used to perform arbitrary database operations on the solver cache – for example, deleting all entries with timestamps older than a specific date. Note: This solver_cache.py file has not yet been integrated with the rest of the SAW Remote API. We do intend to integrate it, and add the solver caching commands present in saw-script to the Remote API, but we're currently thinking that this will be done in a separate PR.

[RyanGlScott]

There are some new test failures in the integration tests CI job. I've taken another pass through SAWScript.SolverCache now that it is based on lmdb-simple.

[RyanGlScott]

Excellent, I'm quite happy with how this has turned out. Great work, @m-yac!