Update formal spec to (partially) implement the 3rd EH proposal #180
Conversation
As described in `proposals/exceptions/Exceptions.md` and in
`proposals/exceptions/Exceptions-formal-overview.md`.
* Detailed changes from the previous (2nd proposal) formal spec:
- Removed:
+ the reference type "exnref" is removed,
+ the administrative instruction "REFEXNADDR" is removed,
+ Release dependencies "bulk instructions" and "reference types" are removed.
- Renamed:
+ "exn" and (most occurrences of) "exception" renamed to "tag",
+ "EITYPE" renamed to "TAGITYPE",
+ "ETYPE" renamed to "TAGTYPE",
+ variable names for tags changed from "et" to "tt" or "tagt" and "iet" to "itagt",
+ "CATCHN" is renamed to "CATCHadm".
+ "THROWADDR" is renamed to "THROWadm".
- Adjusted:
+ syntax and rules for "TRY-CATCH", "RETHROW", and "CATCHadm",
+ folded text format for "TRY-CATCH",
+ validation example of control frame with opcode catch.
- Added:
+ validation example of control frame with opcode catch_all,
+ administrative instructions "CAUGHTadm" and "DELEGATEadm" with rules,
+ syntax and rules for "TRY-DELEGATE".
- Most prose that is changing in the 3rd spec is removed and a temporary "**TODO: add prose**" is added.
+ This will be updated in a followup PR to include the new prose instead.
iIn several places added or adjusted prose or added TODO items to add prose in a followup PR.
- Several similar **TODO**s are added for uncaught exceptions.
ioannad
force-pushed
the
core-formal-spec-fulltext
branch
from
b72b682
to
4bd749a
Compare
|
Friendly ping! :) Sorry for bugging you again, but I would appreciate a rough plan on the timeline. I think this draft is already in pretty good shape and like 95% done, so if you are unable to finish this for a long time I can potentially take over and finish. Please let me you what your plan is. Thanks! |
Co-authored-by: Heejin Ahn <aheejin@gmail.com> Co-authored-by: Andreas Rossberg <rossberg@mpi-sws.org>
|
@ioannad Sorry for the repeated pings 😅 2022 Q2 is mostly over already, and I would like to tie remaining loose ends including this and advance the spec to the phase 4 by the end of Q3 in the latest. Can I ask your plan and timeline on finishing the spec? Or, if you are not available for a few months, please let me know in that case as well, so that we can have an alternative plan. |
Pending to address the rest.
@aheejin I apologise for the long silence. I am now focusing on this and will be updating addressing any comments at a minimum of 1-2 week, until the spec reaches Stage 4 and 5. |
document/core/exec/runtime.rst
Outdated
| :ref:`Handling <exec-throwaddr>` the thrown exception address :math:`a` in the throw context | ||
| :math:`T=\LABEL_1 \{\}[\_]~\END`, with the exception handler :math:`\CATCHN_1\{\RETURN\}` gives: | ||
| :ref:`Handling <exec-throwadm>` the thrown exception with tag address :math:`a` in the throw context | ||
| :math:`T=[\_]`, with the exception handler :math:`H=\CATCHadm\{a~\RETURN\}` gives: |
There was a problem hiding this comment.
@rossberg should these metavariables be listed somewhere, like an index of metavariables?
document/core/exec/runtime.rst
Outdated
| Contrary to block contexts, throw contexts don't skip over handlers. | ||
|
|
||
| Since handlers are not included above, there is always a unique maximal throw context to match the reduction rules. | ||
| This basically means that :math:`\CAUGHTadm {\dots} instr^\ast \END` is not a potential catching block for exceptions thrown by :math:`\instr^\ast`, since these are instructions in the scope of a |CATCH| or a |CATCHALL|. |
There was a problem hiding this comment.
Not sure what this sentence means.. What does "caught in the scope of catch" mean?
There was a problem hiding this comment.
I meant to say that an exception thrown by instr* would be caught by a catch or catch_all. This was not a good sentence indeed, and is now replaced after addressing this forgotten comment that you found.
document/core/exec/runtime.rst
Outdated
| \end{array} | ||
|
|
||
| When a throw occurs, execution halts until that throw is the continuation of a throw context in a catching try block. | ||
| When a throw occurs, we pop the values :math:`val^m:[t^m]` and append them to the tag address :math:`a` into | ||
| a |CAUGHTadm| instruction. We then search for the maximal surrounding throw context `T`, which means we pop |
There was a problem hiding this comment.
Which caught instruction do we append the values..? When a throw occurs, do we even know which catch will catch the exception? If we don't know even whether there's any catch is around to catch the exception, which caught are we talking about here?
There was a problem hiding this comment.
@aheejin this is indeed unclear, I am updating it to
When a throw of the form :math:
val^m (throw a)occurs, we search for the maximal surrounding throw contextT, which means we pop any other values, labels, frames, and |CAUGHTadm| instructions surrounding the throw :math:val^m (throw a), until we find an exception handler (corresponding to a try block) that :ref:handles the exception <syntax-handler>.
We then append the values :math:val^m:[t^m]to the tag address :math:ainto a new |CAUGHTadm| instruction which we push on the stack.
Does this make more sense now?
|
@ioannad Thanks for your latest commits! I really don't want to hold off on landing this, and if new discussions get any longer, let's address them in follow-up PRs. Because this PR has so many comments already, I marked many comments as resolved, and the below are unresolved comments: Questions or requests for confirmation to @rossberg from @ioannad: Simple questions or fixes, which I think we can address before landing: My new questions about the new context example. If this gets longer, let's land this anyway; this doesn't need to be addressed or answered here. |
|
@ioannad Gentle ping :) I hope we can land this soon and start addressing remaining TODOs 😀 |
Co-authored-by: Heejin Ahn <aheejin@gmail.com>
Co-authored-by: Heejin Ahn <aheejin@gmail.com>
… in the previous commit. This comment: WebAssembly#180 (comment)
|
@aheejin I think I addressed everything in your comment listing the missing things to do in this PR. Thank you so much for combing through the open discussions! Please let me know if I failed to see any more things that need change. I think that the only open question to @rossberg is this one, asking whether I should list somewhere the metavariable @aheejin since I know you would like to land this asap, I am also happy to make this possible change in a followup PR. |
|
About latest commit: the button to "commit change" from @aheejin 's review comment had added some accidental + signs, also a I think it's really ok now. :) |
document/core/util/macros.def
Outdated
| .. |LCATCH| mathdef:: \xref{valid/conventions}{context}{\mathrel{\K{catch}}} | ||
|
|
||
| .. Contexts, non-terminals | ||
|
|
||
| .. |labeltype| mathdef:: \xref{valid/conventions}{valid-labeltype}{\mathrel{\X{labeltype}}} | ||
| .. |labeltype| mathdef:: \xref{valid/conventions}{context}{\mathrel{\X{labeltype}}} |
There was a problem hiding this comment.
Why do these have an additional \mathrel that other entries above don't have?
There was a problem hiding this comment.
Good catch! I had added it when these two were under "Notation" a few lines above, where the other two entries also had \mathrel. Removing it in a followup commit of this PR.
| \stepto & S;~F;~\LABEL_m\{\}~(\CAUGHTadm\{a~\val^m\}~\val^m~\RETURN~\END)~\END & \hspace{9ex}\ \\ | ||
| \stepto & \val^m & \\ |
There was a problem hiding this comment.
I still don't really understand this example. I tried to understand this as a simple case, let's say, when n == 3 and m == 2. Then after we throw two values (because the tag's signature is t^m) we still have one value (n-m, which means 3-2 here) value remaning. Where does that value go in this equation? This equation only has m and not n.
Can you guide me through this with a simple example, say, n == 3, n == 2, and t^n == i32 f32 i64 and t^m == f32 i64 or something?
There was a problem hiding this comment.
Thank you for this suggestion, the example will be nicer with such concrete values. I will update it in a followup PR.
Co-authored-by: Heejin Ahn <aheejin@gmail.com>
| \stepto & S;~F;~\LABEL_m\{\}~(\CAUGHTadm\{a~\val^m\}~\val^m~\RETURN~\END)~\END & \hspace{9ex}\ \\ | ||
| \stepto & \val^m & \\ |
There was a problem hiding this comment.
Thank you for this suggestion, the example will be nicer with such concrete values. I will update it in a followup PR.
document/core/util/macros.def
Outdated
| .. |LCATCH| mathdef:: \xref{valid/conventions}{context}{\mathrel{\K{catch}}} | ||
|
|
||
| .. Contexts, non-terminals | ||
|
|
||
| .. |labeltype| mathdef:: \xref{valid/conventions}{valid-labeltype}{\mathrel{\X{labeltype}}} | ||
| .. |labeltype| mathdef:: \xref{valid/conventions}{context}{\mathrel{\X{labeltype}}} |
There was a problem hiding this comment.
Good catch! I had added it when these two were under "Notation" a few lines above, where the other two entries also had \mathrel. Removing it in a followup commit of this PR.
| when the handler catches a thrown exception. | ||
| Intuitively, for each target :math:`\{\tagaddr^?~\instr^\ast\}` of a |CATCHadm|, :math:`\instr^\ast` is the *continuation* to execute | ||
| when the handler catches a thrown exception with tag |tagaddr|, or for any exception, when a target specifies no tag address. | ||
| In that case, we say that the exception is handled by the exception handler |CATCHadm|. |
There was a problem hiding this comment.
As a stylistic remark, the spec avoids formulations in first person like using "we". (Although I noticed that some recently sneaked in through the SIMD extension.)
There was a problem hiding this comment.
Thank you for the tip! Will try to avoid them from now on.
…e values. Addresses @aheejin's request in a previous review comment: WebAssembly#180 (comment) Originally I wrote this using - `val_{i32} = (i32.const 1)`, - `val_{f32} = (f32.const 2.0)`, and - `val_{i64} = (i64.const 3)`, but the example seemed then really long. To keep the example relatively short I switched to the current version.
- Change 'We denote X = Y' to 'Let A be Y' (suggested in WebAssembly#180 (comment)) - Remove uses of 'we' pronouns (suggested in WebAssembly#180 (comment))
- Change 'We denote X = Y' to 'Let A be Y' (suggested in WebAssembly#180 (comment)) - Remove uses of 'we' pronouns (suggested in WebAssembly#180 (comment))
- Change 'We denote X = Y' to 'Let A be Y' (suggested in #180 (comment)) - Remove uses of 'we' pronouns (suggested in #180 (comment))
…te values. (#219) * Simplified throw context example, with concrete types but not concrete values. Addresses @aheejin's request in a previous review comment: #180 (comment) Originally I wrote this using - `val_{i32} = (i32.const 1)`, - `val_{f32} = (f32.const 2.0)`, and - `val_{i64} = (i64.const 3)`, but the example seemed then really long. To keep the example relatively short I switched to the current version. * Typesetting fixes. * Addressed review comments. Co-authored-by: Andreas Rossberg <rossberg@mpi-sws.org>
Updates formal spec to (partially) implement the 3rd EH proposal.
In particular:
In particular there are still the following items marked as
TODO:
[] to add prose for typing rule of DELEGATEadm
[] to add prose for execution rules of TRY-CATCH, TRY-DELEGATE, and RETHROW
[] to finish prose for "Throwing an exception" (exec/instructions.rst)
[] to add EXCEPTION result value, signifying throwing an exception to the embedder
[] to adjust block contexts by adding CATCHadm, DELEGATEadm, and CAUGHTadm
[] to change labels to include the label type "catch" (in section "Contexts")
[] to add prose for validation rules of TRY-DELEGATE and RETHROW