Persist solver, part 2

[robdockins]

Push solver instances higher, into the REPL monad or the SolverState.

Some remaining questions regarding the remote API server:

1. Will this cause problems with concurrent clients?
2. There doesn't seem to be any way to do cleanup actions when
   the server is shut down, so the solver will not be shut down
   gracefully. Is this a problem?

[pnwamk]

Some remaining questions regarding the remote API server:

1. Will this cause problems with concurrent clients?

I guess it depends on what kinds of problems we're worried about:

1. If we're worried about multiple clients accessing the solver simultaneously, that shouldn't be an issue: the underlying server implementation (Argo) currently uses a global MVar to lock access to the internal store of app states while a responding to a particular RPC, so only one client would ever have a handle to the solver at a time with how things currently work.

2. If we're worried about the solver needing to persist state between requests from the same client without interruption in order to function properly... then we might have a small but easily addressable problem. If each client needs their own solver instance and cannot "take turns" using it, then we would want to change this line here from PureState to MutableState, which signals to the server backend that a new initial state needs be created for each unique client because there is some underlying (observable) mutability in the app state.

2. There doesn't seem to be any way to do cleanup actions when
   the server is shut down, so the solver will not be shut down
   gracefully. Is this a problem?

I'm not sure. I guess part of that depends on what's the worst that could happen if we just let the solver connection get GC'd by the Haskell runtime? (Or perhaps I don't have a good mental model for this aspect of the implementation...?) Does the solver get shutdown when the connection is GC'd? Does it matter if that's graceful or not...? Note, that if our answer to (1) above is that we do not need to create a Z3 connection for each user and they can share a connection, then this would only happen when the entire server is shutdown... in which case I'd have a hard time seeing if we cared... so long as we're not leaving zombie processes around or similar in the host machine.

[robdockins]

The solver "shouldn't" be carrying state from query to query that we need to worry about (although I am a bit worried about the robustness of maintaining a solver connection indefinitely). So, I think we should be OK as long as client requests have mutual exclusion.

Currently, the solvers are not set up to be shutdown as part of a GC finalizer. I don't like this method of managing external resources, as it isn't reliable. So, indeed, the worry is that zombie processes will be left on the machine after server shutdown.

[pnwamk]

Okay, well then it seems like overall what you've already got here should work fine, and we can make a TODO w.r.t. improving the graceful shutdown story and how we handle long running server connections.

W.r.t. the lengthy server connection bit, is the worry just that they're generally not meant to be run for long periods and so we may hit issues since we're using them in an atypical way? Or is it more about the need to possibly restart the solver if it crashes?

[robdockins]

I don't know that it's "atypical", but you run greater risk of encountering space leaks and other abstraction-breaking problems by not restarting from a blank slate on a regular basis. EDIT: there's also more "fate sharing", as a problem caused during the execution of another user's request could crash the solver and leave other clients out of luck.

[robdockins]

@LisannaAtGalois, should I be concerned about the CI failures on this PR? I'm not sure what those checks are doing or why they've failed.

[lisanna-dettwyler]

@LisannaAtGalois, should I be concerned about the CI failures on this PR? I'm not sure what those checks are doing or why they've failed.

@robdockins Nope, they're a spurious issue with docker relating to some recent CI rework. Looking into a fix - feel free to ignore it in this PR.