Fix: Spurious message of checkerpool already disposed.

[MikaelMayer]

Looking at the CI result of https://github.com/dafny-lang/dafny/actions/runs/10330235840/job/28615735562?pr=5675, I see like often:

System.Exception: CheckerPool was already disposed
         at VC.CheckerPool.FindCheckerFor(Program program, Split split, CancellationToken cancellationToken)
         at Microsoft.Boogie.VerificationTask.StartRun(CancellationToken cancellationToken)+MoveNext()
         at Microsoft.Boogie.VerificationTask.StartRun(CancellationToken

This PR hopefully fixes this message.

Rationale.

This message does not seem to cause any trouble whatsoever, it's just that the exception is never caught.
Since at the call site, there is a catch of OperationCanceledException, I piggy back on this exception to return it instead of a generic exception, so that the control flow will not display this exception anymore.

I don't know of a way to test this PR, but we will see if the already disposed messages in PR CI disappear.

[keyboardDrummer]

Shouldn't we prevent the exception from being thrown in the first place?

Since at the call site, there is a catch of OperationCanceledException, I piggy back on this exception to return it instead of a generic exception, so that the control flow will not display this exception anymore.

That sounds like it would need a comment both where you throw and where you catch the exception, but better would be not to piggyback on OperationCanceledException.

[MikaelMayer]

from

We really have a nasty concurrency issue here, and even I am not sure of my fix. Before any brittleness issue on the LSP, I almost always saw one of these message. But I don't know if they always appear or just during errors.

If you wanted to get rid of the exception, you'd have to ensure that FindCheckerFor is never called when disposed is true, or remove the exception while ensuring everything goes as planned. The first case is not possible, because the only thing that can turn dispose to true is the method Dispose(), and that method is called only if Engine.Dispose() is called, which according to the Dafny source code, can be called at any moment.

Now if you remove the exception and disposed is true,, you'll enter checkersSemaphore.WaitAsync(cancellationToken), and since all threads should have been cancelled, you'll end with nothing in availableCheckers, so one new checker will be created and returned, although that's useless. Could it lead to memory leaks? I don't know.

What's your take on all of this information?

[keyboardDrummer]

Made a PR that might resolve the issue: #941

[MikaelMayer]

Made a PR that might resolve the issue: #941

You're the best. Closing this one then and I'll post my review on yours because it seem like it does the right thing.