Normative: Fix hangs with top-level await

[syg]

Closes #3356.

Modules that depend on modules with top-level await but do not themselves have a top-level await may currently hang. When a module with TLA finishes evaluating, it triggers evaluation of ancestors modules that depend on it.

Currently, ancestors that do not have TLA themselves are evaluated and have their [[Status]] set to ~evaluated~ but incorrectly leaves their [[AsyncEvaluation]] field unchanged as true. This means subsequent importers of those ancestors consider them as in the middle of async evaluation and will wait on them in InnerModuleEvaluation. But since they are already evaluated, those waits cause a hang.

This PR sets [[AsyncEvaluation]] to false for those ancestors when their [[Status]] transition to ~evaluated~.

Note that the ancestors that error out during evaluation do not need this fix because there is a bail-out path for errored out modules in InnerModuleEvaluation.

[guybedford]

Thanks for finding this bug. Agreed it's a spec bug. In terms of the fix, my concern is that we would need to consistently ensure in the state model for all possible success and failure cases that AsyncEvaluation is set to false, which is not currently part of the model assumptions?

An alternative fix that doesn't require this level of vetting might be to just add an extra check to the conditional in InnerModuleEvaluation to verify the condition.

Perhaps something like this in InnerModuleEvaluation:

                1. Let _requiredModule_ be GetImportedModule(_module_, _required_).
                1. Set _index_ to ? InnerModuleEvaluation(_requiredModule_, _stack_, _index_).
                1. If _requiredModule_ is a Cyclic Module Record, then
                  1. Assert: _requiredModule_.[[Status]] is one of ~evaluating~, ~evaluating-async~, or ~evaluated~.
                  1. Assert: _requiredModule_.[[Status]] is ~evaluating~ if and only if _stack_ contains _requiredModule_.
                  1. If _requiredModule_.[[Status]] is ~evaluating~, then
                    1. Set _module_.[[DFSAncestorIndex]] to min(_module_.[[DFSAncestorIndex]], _requiredModule_.[[DFSAncestorIndex]]).
                  1. Else,
                    1. Set _requiredModule_ to _requiredModule_.[[CycleRoot]].
                    1. Assert: _requiredModule_.[[Status]] is either ~evaluating-async~ or ~evaluated~.
-                   1. If _requiredModule_.[[EvaluationError]] is not ~empty~, return ? _requiredModule_.[[EvaluationError]].
+                 1. If _requiredModule_.[[Status]] is ~evaluated~, then
+                    1. If _requiredModule_.[[EvaluationError]] is not ~empty~, return ? _requiredModule_.[[EvaluationError]].
-                 1. If _requiredModule_.[[AsyncEvaluation]] is *true*, then
+                 1. Else if _requiredModule_.[[AsyncEvaluation]] is *true*, then
                    1. Set _module_.[[PendingAsyncDependencies]] to _module_.[[PendingAsyncDependencies]] + 1.
                    1. Append _module_ to _requiredModule_.[[AsyncParentModules]].

[syg]

An alternative fix that doesn't require this level of vetting might be to just add an extra check to the conditional in InnerModuleEvaluation to verify the condition.

My preference would be to use [[AsyncEvaluation]] only for ordering, and use [[Status]] for state machine transitions. In an offline convo with @lucacasonato he said maybe that doesn't quite work but I didn't dig into it further.

@guybedford WDYT?

[syg]

At the same time, I'll argue against myself in https://github.com/tc39/ecma262/pull/3357#issuecomment-2187093937. I want to resist a large refactoring which is likely to introduce more latent undiscovered bugs, and do the most incremental thing here.

[guybedford]

@syg if I'm understanding you right, you're referring to a bigger refactoring? To dig into the discussion then (and please backtrack if I'm misunderstanding) the other feature of [[AsyncEvaluation]] is that it is able to determine execution state within a cycle. During the Tarjan algorithm we transition states together for all cycles, which makes [[State]] unreliable to check if we've already executed something if it is part of the same cycle we are currently iterating in.

To fully refactor [[AsyncEvaluation]] to be purely an ordering field, would require solving this cycle state in another way. I was tempted to break the cycle transition invariant of [[State]] and allow [[State]] to transition piecemeal through cycles as it seemed cute but perhaps unnecessary, but that seemed tougher to consider at the time TLA was specified. Perhaps we reopen that discussion? It may involve something like ensuring the blanket cycle state transitions during error handling and success conditions instead.

[syg]

I... think I see. If [[Status]] is unreliable as part of the same cycle we're currently iterating in, is that an issue for your preferred alternative fix in https://github.com/tc39/ecma262/pull/3357#issuecomment-2185397857?

[guybedford]

I... think I see.

Great. I would love to refactor to make AsyncEvaluation purely an ordering thing too. Perhaps we can do a follow-on?

If [[Status]] is unreliable as part of the same cycle we're currently iterating in, is that an issue for your preferred alternative fix in https://github.com/tc39/ecma262/pull/3357#issuecomment-2185397857?

I believe it does not, since the change I've suggested there would still check both conditions (that is, if the dependency has already been processed in the current Tarjan cycle processing, it's not something we need to "listen" to, the important case, and case not captured by the evaluating state, is where it hasn't been).

I'd need to dig into this further, but I wonder if we could do a check of either the module being in evaluating or the module being in stack but before the level of stack where dfsindex equals dfsancestor as a replacement of the AsyncEvaluation check...

[syg]

Perhaps we can do a follow-on?

Yep, I think doing the most incremental fix we can in this PR and leave the refactoring for a follow-up is the most prudent course of action.

[guybedford]

Okay, I can aim to look into a follow-up after this lands.

For this PR for now, the fix looks good, although for a consistent model let's also set it to false inside of AsyncModuleExecutionRejected while we're at it as well then?

[syg]

For this PR for now, the fix looks good, although for a consistent model let's also set it to false inside of AsyncModuleExecutionRejected while we're at it as well then?

Recapping editor call discussion: will set it to false in the rejection closure for consistency with a note that the value is not consulted in the error path.

[nicolo-ribaudo]

This change looks correct to me, and I agree with the proposed extra update from the editors group.

Fyi, I started trying to formalize the modules evaluation algorithms to be able to formally prove their behavior (using https://lean-lang.org/, recommended by @jessealama).

[bakkot]

@nicolo-ribaudo You might want to get in touch with @conrad-watt, who has done formalizations of other parts of the spec (specifically the memory model - https://arxiv.org/abs/2005.10554) in Coq.

[guybedford]

I was looking at this algorithm again last night, and one viable way we can replace AsyncEvaluation would be to have a new shared ordered list argument to the inner evaluation function, something like asyncEvaluations. Just maintaining this "completed" list or state while the algorithm is being performed (since afterwards async-evaluation checks are sufficient), is really all this is field is for (along with maintaining ordering for the async completions of course).

[syg]

In the last plenary we presented this spec bug fix as FYI, saying we'd merge if there're no concerns raised on the issue. It's been quite a while now, so putting the merge label on.