Closed santolucito closed 2 years ago
https://docs.aws.amazon.com/AmazonCloudFront/latest/DeveloperGuide/QueryStringParameters.html
Looks like we can cache results easily with CloudFront.
proposing the following architecture for caching (memoizing seems like a better word, it is more permanent than caching) cvc5 queries
might also be nice to allow queries that timeout to run on another lambda with a longer timeout (maybe 1 min? max is 15 mins but that can get expensive, and CVC5 usually doesnt find much past 1 min). Doing this will allow us to memoize this longer running query so it is avaible next time through the database.
closing this issue with eeebd6e51345ab56bc0d28f863fc4023eb35312c which implements basic memoization of synth requests. still todo is the above comment on allowing longer synth requests to run for future queries. will reopen that comment as a new issue
We should cache synthesis requests in order to reduce the calls to the AWS Lambda for CVC5 we make.
Since plenty of synthesis requests will have been seen before by other users, we should be able to speed up synthesis significantly by caching requests.
I think this should happen on the AWS side of things (an extra Lambda in front of CVC5 that checks if the request already exists in a database) so that the local install can still run without needing to access a database. Caching can be turned on and off with a flag similar to how serverless works now
The basic structure would then be:
within synthesizer.js: