Formal overview address latest review #205

ioannad · 2022-02-25T12:45:14Z

This PR attempts to address @rossberg 's last review on merged PR#143, and makes some extra changes for readability, and documentation.

@rossberg @aheejin

Continuing here the last discussion from the merged PR #143, because that PR is closed and difficult to follow.

The change to remove the +1 from the typing rule of the administrative delegate (will call it adm.delegate) was related to the decision to allow a plain (try bt instr* delegate 0) in the function body. It seems I forgot to update the typing rule for try-delegate itself to be in accord with that decision.

So I think the correct rule for try-delegate should be the following (previously the 3rd premise was C.labels[l] = [t'*], which was equivalent to |C.labels| > l).

C ⊢ bt : [t1*]→[t2*]
C, labels [t2*] ⊢ instr* : [t1*]→[t2*]
|C.labels| ≥ l
-------------------------------------------
C ⊢ try bt instr* delegate l : [t1*]→[t2*]

This way, a context with an empty labels vector can validate this even for l=0.

If we now rewrite the typing rule of adm.delegate in the same style it becomes:

S;C, labels [t*] ⊢ instr* : []→[t*]
|C.labels| ≥ l
-----------------------------------------------------
S;C, labels [t*] ⊢ delegate{l} instr* end : []→[t*]

So perhaps there was no +1 missing from this rule, but a label too many in the typing rule of try.delegate?

Question

Do you think this new rule for try-delegate addresses your concerns with regard to type preservation?
Would it be better (and perhaps equivalent?) to write the typing rule for adm.delegate as follows?

S;C ⊢ instr* : []→[t*]
|C.labels| > l
-----------------------------------------------------
S;C ⊢ delegate{l} instr* end : []→[t*]

ioannad · 2022-02-25T12:56:45Z

@aheejin about your question in the last comment of that discussion:

If we change the current rule
F; val^n (try bt instr* delegate l)
  ↪ F; label_m{} (delegate{l} val^n instr* end) end
to
F; val^n (try bt instr* delegate l)
  ↪ F; delegate(l) (label_m{} val^n instr* end) end
meaning, if we put the label created by the try-delegate itself within the scope of adm.delegate, can this confusion be helped?

I think the reason for putting the label outside of adm.delegate was so that it's similar to what happens in try-catch. I don't know if a different behaviour there would be a different source of confusion, but I don't mind either way.

rossberg · 2022-03-01T08:55:24Z

Well, I don't know, I would very much prefer to avoid non-standard premises talking about the size or depending on the ordering of the context, which is a bit of an abstraction leak. Note that the condition |C.labels| >= l is technically equivalent to saying C.labels[l] = t* for some t*, so it should be fine to keep the latter – we could easily prove a lemma saying that if C.labels[l+1] = t* then C.labels[l] = t'*`, which would make your previous formulation work. Yet, either way, it is a bit too hacky for my taste, and I fear such an abstraction leak would get in the way of clean formal reasoning about the context for other purposes.

@aheejin is right that it would be natural and solve the problem to nest label and admin delegate the other way around. You are also right that the current reduction keeps it symmetric with catch. But that was itself a hack, so it may be better to keep that confined to catch. WDYT?

aheejin

Sorry for the late reply.

It would be probably better to split out the other non-delegate-related parts into another PR and commit it, so this PR only concerns delegate..?

@ioannad

So I think the correct rule for try-delegate should be the following (previously the 3rd premise was C.labels[l] = [t'*], which was equivalent to |C.labels| > l).

Does this account for the added label in delegate's execution semantics, which @rossberg was concerned about?

@rossberg

Note that the condition |C.labels| >= l is technically equivalent to saying C.labels[l] = t* for some t*, so it should be fine to keep the latter – we could easily prove a lemma saying that if C.labels[l+1] = t* then C.labels[l] = t'*`, which would make your previous formulation work.

Can this handle the the case @ioannad described, in which delegate N delegates to the caller? For example,

(func $test
  (try
    (do
      ...
    )
    (delegate 0)
  )
)

given that there's no label this delegate targets within this function? Or, do we implicitly push a label when a function is entered in the formal spec?

How do we handle br without a block? Is that a validation failure?

(func $test
  (br 0)
)

Is this a validation failure or it just exits the function?

proposals/exception-handling/Exceptions-formal-overview.md

aheejin · 2022-03-18T06:22:38Z

proposals/exception-handling/Exceptions-formal-overview.md

@@ -152,34 +154,34 @@ An absent tag address in a `catch` administrative instruction (i.e., `a? = ε`)
 ```
 F; throw x  ↪  F; throw a  (if F.module.tagaddrs[x]=a)

-caught{a val^n} B^l[rethrow l] end
-  ↪ caught{a val^n} B^l[val^n (throw a)] end
+caught{a val*} B^l[rethrow l] end


In the formal spec, when do we use ^n and when do we use *? Can they be used interchangeably? I see both notations in the current (standardized) formal spec and I'm not very familiar with the formal notation, so..

IIUC we use ^n when the n has a constraint in the rule it is mentioned, but I think in the formal spec document this is not always the case.

This change is to implement exactly this idea, so to only use the n if it has a particular constraint, as it does for example in lines 163-164.

I think that this change makes the formal overview a bit more concise, as I see the formal overview as a "cheatsheet" for Wasm exceptions.

aheejin · 2022-03-18T06:26:35Z

Also I wasn't able to follow every argument from https://github.com/WebAssembly/exception-handling/pull/143/files#r759907998, partly due to I wasn't able to understand this rule.

S; C |- instr0*: [t1^n] -> [t2*]
S; C, labels [t1^n] |- instr* : [] -> [t2*]
-------------------------------------------------------
S; C |- label_n{instr0*} instr* end : [] -> [t2*]

Why is instr*'s result t2* and not t1^n? (And what'd the difference between the notation ^n and *?)
It looks instr* should produce t1^n, because the label's result type is t1^n, and that's what instr0* consumes after the instr* is executed. Which part am I getting wrong?

rossberg · 2022-03-23T13:28:58Z

@aheejin:

Or, do we implicitly push a label when a function is entered in the formal spec?

Yes, a function creates an implicit outermost label.

proposals/exception-handling/Exceptions-formal-overview.md

aheejin · 2022-03-23T23:31:48Z

For delegate, do we allow a label immediate greater than the function-level block? For example,

(func $test
  try
  delegate 0 ;; throw to the caller
  try
  delegate N ;; For any N >= 1. Do we allow this?
)

In this case delegate 0 is throwing up to the caller. Do we allow N equal to or greater than 1? @ioannad's equation seems to be assuming that we allow this and @rossberg's doesn't seem to. I've been somehow assuming we allow this, but I can't find any past discussions on this. I'm OK either way. For br we don't seem to allow br greater than 0 in that case:

(func $test
  br 0 ;; allowed
  br N ;; N >= 1 is not allowed
)

rossberg · 2022-04-04T08:29:58Z

@aheejin, I agree that delegate shouldn't allow unbound labels, but I don't think @ioannad's formulation does that, since it requires l <= |C.labels|.

aheejin · 2022-04-07T13:47:12Z

@aheejin, I agree that delegate shouldn't allow unbound labels, but I don't think @ioannad's formulation does that, since it requires l <= |C.labels|.

Ah right, I was confused. Thanks, then I think we should assume we don't allow unbound labels. (Maybe I was the only one who was assuming we were allowing this anyway)

aheejin · 2022-05-02T23:45:22Z

@ioannad Gentle ping :) Are you planning to update this soon?

ioannad · 2022-05-06T16:03:25Z

Apologies for the long silence @aheejin !
I am working on updating the formal overview and spec asap.

ioannad · 2022-05-07T16:52:23Z

@rossberg

Note that the condition |C.labels| >= l is technically equivalent to saying C.labels[l] = t* for some t*, so it should be fine to keep the latter – we could easily prove a lemma saying that if C.labels[l+1] = t* then C.labels[l] = t'*`, which would make your previous formulation work.

I don't understand why is "|C.labels| >= l" technically equivalent to "there exists t* such that C.labels[l] = t*". If |C.labels| = l then there is no C.labels[l]. Or does the equivalence somehow involve/assume @aheejin's formulation with the "delegate"-label after the delegate administrative instruction?

@aheejin is right that it would be natural and solve the problem to nest label and admin delegate the other way around. You are also right that the current reduction keeps it symmetric with catch. But that was itself a hack, so it may be better to keep that confined to catch. WDYT?

I haven't checked all the details yet, but now I think this should work fine.

rossberg · 2022-05-10T08:21:23Z

@ioannad, oops, you are right, I missed the =. Rather, |C.labels| >= l would be equivalent to C.labels[l-1] = t*, which is a bit more nasty. Either way, I'd like to avoid going there. :)

ioannad · 2022-05-11T18:49:56Z

Just rebased but I see something went wrong there, fixing...

Still todo: haven't finished switching to @aheejin's suggestion yet - checking the examples work as expected.

This is not the suggestion given in that last review of WebAssembly#143: https://github.com/WebAssembly/exception-handling/pull/143/files#r759907998 but a potential fix of the issue raised there.

…to formal-overview-address-latest-review

The original review comment: https://github.com/WebAssembly/exception-handling/pull/143/files#r759907998 The explanation line clarifies what happens if the label targets the frame, and what labels are allowed.

ioannad · 2022-08-17T17:29:38Z

@aheejin, @rossberg,
About the new reduction rule for try-delegate (see comment above), which puts the label after the administrative delegate{l}:

I tried to implement this in the interpreter and ran into some issues that I'm not sure how to resolve, although they are probably solvable.

In order to keep things confined and more easily searchable (so to not have a too long discussion in the PR or inline), I will make a new PR dedicated to that change, in which I will also include the changes I tried in the interpreter, and more details.

To wrap up this PR, I reverted the changes involving the length of C.labels and instead I did what the PR title says, that is addressed "the latest review", by adding the +1 to the C.labels premise of the typing rule for delegate{l}, as requested.

ioannad · 2022-08-17T20:51:53Z

@rossberg, reading again this comment of the original discussion in #143, I am thinking that your objection may be in using C.labels[l] instead of (C labels [t*]).labels[l+1] in that rule's premise.

Am I reading that comment correctly, so is it the case that you think that the typing rule for delegate{l} should be as follows?

S;C' ⊢ instr* : []→[t*]
C'.labels[ l+1 ] = [t0*]
------------------------------------------------------
S;C' ⊢ delegate{l} instr* end : []→[t*]

Or am I misunderstanding that comment?

aheejin · 2022-08-17T23:42:11Z

@rossberg, reading again this comment of the original discussion in #143, I am thinking that your objection may be in using C.labels[l] instead of (C labels [t*]).labels[l+1] in that rule's premise.

Am I reading that comment correctly, so is it the case that you think that the typing rule for delegate{l} should be as follows?
S;C' ⊢ instr* : []→[t*]
C'.labels[ l+1 ] = [t0*]
------------------------------------------------------
S;C' ⊢ delegate{l} instr* end : []→[t*]
Or am I misunderstanding that comment?

I'm also wondering about this. Only changing l to l+1 doesn't make sense to me, because as @ioannad described in https://github.com/WebAssembly/exception-handling/blob/main/proposals/exception-handling/Exceptions-formal-overview.md,

Because delegate{l} is always wrapped in its own label_n{} ... end [2], with the same lookup as for br l we end up breaking inside the l+1th surrounding block, and throwing there.

And what @rossberg said in https://github.com/WebAssembly/exception-handling/pull/143/files#r811680384 was:

The problem I see is that (4) is not the premise you'll need when arriving at the adm.delegate rule. Instead you'll need
(4') C'[l'] = [t'*]
with C' = C, labels [t^n] and some l', because that's the context you now enter the rule with. The only suitable l' that allows you to prove this from (4) is l+1, I believe.

So we should change the LHS to C? @rossberg

rossberg · 2022-08-23T13:36:16Z

@ioannad, you are right, the first premise needs changing as well – the added label is wrong there, since that's added by the surrounding label construct, not by delegate.

aheejin · 2022-08-25T23:22:41Z

@ioannad Can we make the change and merge it?

…ests) [Currently](https://github.com/WebAssembly/exception-handling/blob/main/proposals/exception-handling/Exceptions-formal-overview.md) `(try ... delegate l)` reduces to `(label_n{} ( delegate{l} ... end ) end)`, so by putting a label outside (i.e., before) the administrative `delegate{l}`. An idea proposed in past [unresolved](WebAssembly#205 (comment)) [discussions](https://github.com/WebAssembly/exception-handling/pull/143/files#r812476148) of WebAssembly#205 and WebAssembly#143, is to simplify and improve the formalism by instead putting the delegate label inside (i.e., after) the `delegate{l}`. So instead to reduce to `(delegate{l} ( label_n{} ... end ) end)`. TL;DR ----- I can't seem to make it work. This PR explored an approach to implement this idea, in the [formal overview file ](https://github.com/WebAssembly/exception-handling/blob/main/proposals/exception-handling/Exceptions-formal-overview.md), as well as in the interpreter, but had failing tests which I wasn't able to fix. Perhaps I'm overseeing some other solution or approach, or there is some mistake in the interpreter implementation and/or argumentation below. Details ------- I think the problem is as follows. With the current [definition of block contexts](https://webassembly.github.io/exception-handling/core/exec/runtime.html#block-contexts), the instruction sequence `B^l[ delegate{l} T[val^n (throw a)] end ]` not only is ambiguous, but doesn't work with a try-catch label located outside of the try-catch. Take for example the following possible reduction. ``` (try (try (throw x) delegate 0) catch x end) ↪ (label_0{} (catch{a_x ε} (delegate{0} (label_0{} (throw a_x) end) end) end) end) ``` The intention for this delegate is to throw inside the handler `catch{a_x ε}` and be caught there. However, a possible `B^0` for the reduction of `delegate{0}` is `B^0 = [_] catch{a_x ε}`, in which case the reduction rule gives the following. ``` ↪ (label_0{} (throw a_x) end) ↪ (throw a_x) ``` The issue here seems to be that there is no label between the `delegate{l}` and the `catch{...}`. Perhaps there is a different change we can easily make it work, for example changing control contexts or block contexts? Failing tests ............. We can observe the above wrong behaviour also in the interpreter tests, although this could be fixable somehow. In particular, the first commit of this PR has the formal overview changes also implemented in the execution steps of the interpreter (in `interpreter/exec/eval.ml`): - The reduction of `try ... delegate l` puts the `label{}` after the `delegate{l}`. - The reduction of `delegate{l}` does not pattern match for an initial label. I tried to minimise a failing test from `test/core/try_delegate.wast` in the file `test/core/try_delegate_minimal_fail.wast`. To reproduce the failure build the interpreter and run the above test file as follows, for example from a Linux terminal in the base directory of the repository: ``` cd interpreter make ./wasm ../test/core/try_delegate_minimal_fail.wast ``` See also comments in the test file.

This was referenced Feb 25, 2022

formal spec overview for the 3rd exception handling proposal #143

Merged

Update formal spec to (partially) implement the 3rd EH proposal #180

Merged

aheejin reviewed Mar 18, 2022

View reviewed changes

proposals/exception-handling/Exceptions-formal-overview.md Outdated Show resolved Hide resolved

proposals/exception-handling/Exceptions-formal-overview.md Outdated Show resolved Hide resolved

aheejin reviewed Mar 18, 2022

View reviewed changes

aheejin reviewed Mar 23, 2022

View reviewed changes

proposals/exception-handling/Exceptions-formal-overview.md Outdated Show resolved Hide resolved

ioannad mentioned this pull request May 6, 2022

Formal overview minor fixes #208

Merged

ioannad force-pushed the formal-overview-address-latest-review branch from a236e95 to ba7edb6 Compare May 11, 2022 18:45

Fix typing rule of administrative delegate.

46d3f94

This is not the suggestion given in that last review of WebAssembly#143: https://github.com/WebAssembly/exception-handling/pull/143/files#r759907998 but a potential fix of the issue raised there.

ioannad force-pushed the formal-overview-address-latest-review branch from ba7edb6 to 46d3f94 Compare May 11, 2022 18:55

ioannad added 2 commits August 17, 2022 17:50

Merge remote-tracking branch 'WebAssembly/exception-handling/main' in…

9c28e65

…to formal-overview-address-latest-review

Addressed the original review comment, added an explanation line.

e11012d

The original review comment: https://github.com/WebAssembly/exception-handling/pull/143/files#r759907998 The explanation line clarifies what happens if the label targets the frame, and what labels are allowed.

ioannad requested a review from rossberg August 17, 2022 17:29

Fix typing of administrative delegate.

cb5cc85

Ms2ger approved these changes Aug 26, 2022

View reviewed changes

Ms2ger merged commit f3c5987 into WebAssembly:main Aug 26, 2022

ioannad mentioned this pull request Sep 2, 2022

Attempt to put the try-delegate label after delegate{l} (failing tests) #220

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Formal overview address latest review #205

Formal overview address latest review #205

ioannad commented Feb 25, 2022 •

edited

Loading

ioannad commented Feb 25, 2022

rossberg commented Mar 1, 2022

aheejin left a comment

aheejin Mar 18, 2022

ioannad May 6, 2022 •

edited

Loading

aheejin commented Mar 18, 2022 •

edited

Loading

rossberg commented Mar 23, 2022

aheejin commented Mar 23, 2022 •

edited

Loading

rossberg commented Apr 4, 2022

aheejin commented Apr 7, 2022

aheejin commented May 2, 2022

ioannad commented May 6, 2022

ioannad commented May 7, 2022 •

edited

Loading

rossberg commented May 10, 2022

ioannad commented May 11, 2022 •

edited

Loading

ioannad commented Aug 17, 2022 •

edited

Loading

ioannad commented Aug 17, 2022 •

edited

Loading

aheejin commented Aug 17, 2022

rossberg commented Aug 23, 2022

aheejin commented Aug 25, 2022

Formal overview address latest review #205

Formal overview address latest review #205

Conversation

ioannad commented Feb 25, 2022 • edited Loading

ioannad commented Feb 25, 2022

rossberg commented Mar 1, 2022

aheejin left a comment

Choose a reason for hiding this comment

aheejin Mar 18, 2022

Choose a reason for hiding this comment

ioannad May 6, 2022 • edited Loading

Choose a reason for hiding this comment

aheejin commented Mar 18, 2022 • edited Loading

rossberg commented Mar 23, 2022

aheejin commented Mar 23, 2022 • edited Loading

rossberg commented Apr 4, 2022

aheejin commented Apr 7, 2022

aheejin commented May 2, 2022

ioannad commented May 6, 2022

ioannad commented May 7, 2022 • edited Loading

rossberg commented May 10, 2022

ioannad commented May 11, 2022 • edited Loading

ioannad commented Aug 17, 2022 • edited Loading

ioannad commented Aug 17, 2022 • edited Loading

aheejin commented Aug 17, 2022

rossberg commented Aug 23, 2022

aheejin commented Aug 25, 2022

ioannad commented Feb 25, 2022 •

edited

Loading

ioannad May 6, 2022 •

edited

Loading

aheejin commented Mar 18, 2022 •

edited

Loading

aheejin commented Mar 23, 2022 •

edited

Loading

ioannad commented May 7, 2022 •

edited

Loading

ioannad commented May 11, 2022 •

edited

Loading

ioannad commented Aug 17, 2022 •

edited

Loading

ioannad commented Aug 17, 2022 •

edited

Loading