Add support for cache eviction

[atomb]

No description provided.

[pnwamk]

See also #89 for some discussion on the topic.

[pnwamk]

Here is some initial tinkering aimed at limiting memory usage which aims to "give users the option to save a result state, but ensure incremental states don't sit around eating up resources" (as suggested by @weaversa in #89): https://github.com/GaloisInc/argo/tree/feature/bounded-memory-usage

Approach Details

In that branch, Argo essentially aims to guarantee a bound on memory use by:

• keeping only the initial server state cached indefinitely,
• keeping alive a (customizable) number of recently used states while evicting others from the cache when it fills (along with any no longer in-use file contents loaded from disk), and
• allows states to be explicitly pinned in the cache, which would keep them in memory until they are explicitly unpinned.

The main cost of such an approach is that arbitrary states no longer in cache cannot be "replayed" or "resurrected" automatically when a request mentioning them is received once they are evicted (such a state would either have to be manually pinned or rebuilt by the client through standard interactions).

Other memory leaks...?

I thought there were some memory leaks (glancing at MacOS's Activity Monitor and seeing the Memory usage skyrocket), but after doing some GHC heap profiling I'm... less convinced there is an issue: https://gist.github.com/pnwamk/1accd1f95fcaabb5ac30d963aab0ee0f

The memory usage does seem to climb when query numbers climb in the socket case, but the jump from n=10,000 to n=100,000 is so much smaller than the jump from n=1,000 to n=10,000 I'm not sure what to make of it.

Remaining Questions

1. How important is the "guaranteed replayability" of past states for Argo? The aforementioned approach to limiting memory usage sets that feature aside to make things relatively simple... presumably there's a hybrid approach which supports some replayability while still bounding memory use. At the moment, however, (a) I don't think we have any use cases currently which require replayability (please correct me if I'm wrong there), and (b) some of our intended apps have backends that may already fundamentally struggle w.r.t. true replayability (e.g., Cryptol with newtypes and more advanced modules begins to risk being non-replayable (although currently things may be structured in a deterministic/replayable enough way), and SAW may already be not entirely replaybable w.r.t. keeping in sync with an external user).

2. How important is truly bounded memory usage? Given that we're beginning to investigate loading these servers into some fairly constrained runtimes... I'm assuming having memory leaks will be a potentially frequent frustration going forward for users. But perhaps one could argue reducing leaks to a trickle and resetting the servers at regular intervals is good enough...? At the moment my personal bias is towards having explicit bounds/guarantees on memory usage... maybe that's just me though ¯\_(ツ)_/¯

[pnwamk]

I updated the comments above regarding a possible memory leak with some actual GHC Heap profiling data. When being profiled the file-echo-api server seem more or less bounded in both cases.

[pnwamk]

There is now rudimentary support for bounded cache size, flushing caches, etc. If more complex support is desired we can open an issue then with those specific requirements.