Fix: Spurious message of checkerpool already disposed.

MikaelMayer commented 3 months ago

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.

MikaelMayer commented 3 months ago

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 commented 3 months ago

Made a PR that might resolve the issue: https://github.com/boogie-org/boogie/pull/941

MikaelMayer commented 3 months ago

Made a PR that might resolve the issue: https://github.com/boogie-org/boogie/pull/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.

boogie-org / boogie

Fix: Spurious message of checkerpool already disposed. #937

Rationale.