make chalk inner loop "fuel friendly"

[nikomatsakis]

The goal of this issue is to ensure that the chalk engine's "inner loop" doesn't do an "unbounded" amount of work between invocations. The idea then is that the outer engine, the one that is driving chalk and asking for answers, is able to control how much work is done and to "give up" if it seems like things are taking too long. This is an alternative to #227, in that the "fuel" is pushed out from chalk to the surrounding context.

Actually, the design of the engine today is relatively close to this. For example, the result of asking for more answers (e.g., via ensure_root_answer) always includes a QuantumExceeded result, which basically means "didn't reach an answer yet, try again".

However, there are still a few bits of the engine that can do an "unbounded" amount of work. I'll elaborate on the changes needed to fix each of them in comments below:

• flounding (relatively easy)
• cycle handling (harder)

[Matthias247]

Wouldn't adding general cancellation support being an alternative to adding any kind "fuel" values? Then callers can cancel operations depending on their requirements. E.g. they can cancel after a given timeout, user moved away to another operation, etc.

Adding cancellation support to a pure CPU bound problem is not too hard. You can add cancel_token: &CancellationToken parameters to methods, and do cancel_token.check_for_cancellation()?` at required places (e.g. in some main loops). The tricky part might be on the caller site, because for timeouts they would need to trigger cancelation from a different thread. But even that can be encapsulated.

[nikomatsakis]

Note for the future:

Now that we've landed the non-recursive form, one scenario that is worrying me is something like this:

• Start processing X but encounter a cycle
• Continue processing other strands but encounter QuantumExceeded, perhaps because of running out of fuel
• Never actually detect that no more answers will come because we never get to the point of running out of cycles

I think that without fuel maybe this scenario can't take place, because instead of getting QuantumExceeded, if all we are getting is cycles, we'll just keep processing further strands. Still, there is an efficiency concern here (we'd want to measure) where we'll repeatedly re-process cycles.

We might be able to circumvent this by preserving the stack in the case of running out of fuel and jumping back where we left off if the same root goal is given again.

[nikomatsakis]

@Matthias247 yes, we could add general cancellation, it's not so different from fuel I suppose.

[jackh726]

With the addition of solve_limited, this can be closed.