@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.

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?).

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.

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.

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.

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.

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.

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.

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.

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?

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).

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

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?

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...

@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.

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.

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.

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.