improve process pool scope

[0xkarmacoma]

Problem

Currently each FunctionContext (https://github.com/a16z/halmos/blob/main/src/halmos/solve.py#L178) has one SolvingContext, and each SolvingContext has one PopenExecutor.

PopenExecutor serves as a process pool:

• it lets us fire async solving queries as external processes
• it lets us control how many external processes can run concurrently (ideally < than the number of CPU cores available)
• it also lets us interrupt work, for instance when we reach a global timeout or when a solver has found a successful solution

This last point is why PopenExecutor is scoped at the function level (1 function = 1 test), meaning that when a solution is found for a test, we can interrupt the other solvers running for that test, but other tests would be unaffected.

However:

• having 1 solver pool per test defeats the purpose of controlling how many external processes can run concurrently
• the model breaks down when testing probes during invariant testing (these are "freestanding" assertions that are not part of a specific test function). We currently create a dummy function context, so all probes share the same PopenExecutor, which does not make sense (one probe getting a successful query would interrupt queries from other probes).

Solution

I think a better alternative would be to have a single global PopenExecutor process pool. This would definitely help us control how many processes can run at a given time. This means queries from any tests now need to be multiplexed onto the same process pool -- but we still need to be able to shut down work for a given test.

Therefore instead of shutting down the pool for a given test (which is now a global pool), we could submit each query with a relevant tag (e.g. the test name). This would let us:

• shut down the pool when a global time out is reached (all tests are interrupted)
• shut down queries that belong to a specific test by adding a new API like PopenExecutor.interrupt(tag: str) -- all processes with that tag are interrupted, but processes with another tag are unaffected.

This also needs to work with probes, each probe should get its own tag, guaranteeing isolation.