[spec] Update spec for option B' #283

rossberg · 2023-10-14T10:38:08Z

This updates the spec document to option B'.

@ioannad, would you be interested in reviewing this change? I know it is rather large, but it's deleting more than it's adding. :)

conrad-watt · 2023-10-14T12:06:52Z

@rossberg I can probably take a look at this while I'm in the air on Sunday.

titzer

I'd be OK merging this PR into exnref-1b before review and then reviewing the merged branch as a PR on the main branch. (AFAICT there is no PR to merge exnref-1b into the main branch yet, and I already noticed a typo there).

rossberg · 2023-10-16T18:36:54Z

AFAICT there is no PR to merge exnref-1b into the main branch yet

There is: #285 ;)

Happy to do it in either order.

rossberg · 2023-10-16T18:50:09Z

Thinking again, it probably makes sense not to block #285, so people see an up-to-date explainer and tests etc. I rather hold off on merging this one until @conrad-watt or somebody else did a proper review.

conrad-watt · 2023-10-19T08:53:54Z

Apologies for the delay, on this now.

conrad-watt · 2023-10-19T09:08:21Z

EDIT: I originally complained about a build warning here, but I was building on the wrong branch

conrad-watt · 2023-10-19T09:09:47Z

document/core/appendix/index-instructions.py

    Instruction(r'\DROP', r'\hex{1A}', r'[t] \to []', r'valid-drop', r'exec-drop'),
    Instruction(r'\SELECT', r'\hex{1B}', r'[t~t~\I32] \to [t]', r'valid-select', r'exec-select'),
    Instruction(r'\SELECT~t', r'\hex{1C}', r'[t~t~\I32] \to [t]', r'valid-select', r'exec-select'),
    Instruction(None, r'\hex{1D}'),
    Instruction(None, r'\hex{1E}'),
-    Instruction(None, r'\hex{1F}'),
+    Instruction(r'\TRYTABLE~\X{bt}', r'\hex{1F}', r'[t_1^\ast] \to [t_2^\ast]', r'valid-try_table', r'exec-try_table'),


Are we no longer listing the catch opcodes separately?

They are no longer in the space of instruction opcodes, but just flag bytes in a vector.

conrad-watt · 2023-10-19T09:16:08Z

document/core/appendix/properties.rst

@@ -59,16 +59,12 @@ Results
   }


-:ref:`Results <syntax-result>` :math:`\val^\ast~(\THROWadm~\tagaddr)`
+:ref:`Results <syntax-result>` :math:`\XT[(\REFEXNADDR~a)~\THROWREF]`


It feels kind of nasty to classify an instruction inside a context as a "result". Can you walk me through why you don't want to use something like \THROWadm any more?

The introduction of the context is actually unrelated to replacing THROWadm, its absence was simply wrong before. We need it here since there is no reduction rule that can eliminate it on the outermost level (outside a function). We can't simply add a rule XT[exn] ⇝ exn, since that would introduce overlapping rules.

I see two ways to fix this in the future: (1) switching to a bubbling semantics for exceptions (avoiding overlap), or (2) introducing a separate global reduction relation like we have with threads. The former should go along with changes to other parts of the semantics to stay coherent, the latter I'd rather do after we have merged with threads. Hence I don't want to do either in this PR.

conrad-watt · 2023-10-19T09:25:33Z

document/core/util/macros.def

@@ -1280,6 +1290,7 @@
 .. |vdashglobalinst| mathdef:: \xref{appendix/properties}{valid-globalinst}{\vdash}


line 1283 (above): .. |vdashval| mathdef:: \xref{appendix/properties}{valid-val}{\vdash}

should be exec/modules rather than appendix/properties (I think)

Indeed, fixed.

conrad-watt · 2023-10-19T09:33:41Z

document/core/exec/instructions.rst

+      \iff & F.\AMODULE.\MITAGS[x] = a \\
+      \land & S.\STAGS[a].\TAGITYPE = [t^n] \toF [] \\
+      \land & \X{exn} = \{ \EITAG~a, \EIFIELDS~\val^n \} \\
+      \land & S' = S \with \SEXNS = S.\SEXNS~\X{exn} ) \\


Is it necessary to allocate exceptions in the store? Since they're immutable, can the abstract semantics not just treat them as ordinary values?

References need internal identity, because it can become observable in the host, e.g. in JS. This is analogous to functions, which are likewise immutable.

(The lack of exn identity was one of the problems we faced with the JS API spec in the old proposal.)

rossberg

Thanks for the review!

rossberg · 2023-10-19T09:44:43Z

document/core/appendix/index-instructions.py

    Instruction(r'\DROP', r'\hex{1A}', r'[t] \to []', r'valid-drop', r'exec-drop'),
    Instruction(r'\SELECT', r'\hex{1B}', r'[t~t~\I32] \to [t]', r'valid-select', r'exec-select'),
    Instruction(r'\SELECT~t', r'\hex{1C}', r'[t~t~\I32] \to [t]', r'valid-select', r'exec-select'),
    Instruction(None, r'\hex{1D}'),
    Instruction(None, r'\hex{1E}'),
-    Instruction(None, r'\hex{1F}'),
+    Instruction(r'\TRYTABLE~\X{bt}', r'\hex{1F}', r'[t_1^\ast] \to [t_2^\ast]', r'valid-try_table', r'exec-try_table'),


They are no longer in the space of instruction opcodes, but just flag bytes in a vector.

rossberg · 2023-10-19T09:52:42Z

document/core/appendix/properties.rst

@@ -59,16 +59,12 @@ Results
   }


-:ref:`Results <syntax-result>` :math:`\val^\ast~(\THROWadm~\tagaddr)`
+:ref:`Results <syntax-result>` :math:`\XT[(\REFEXNADDR~a)~\THROWREF]`


The introduction of the context is actually unrelated to replacing THROWadm, its absence was simply wrong before. We need it here since there is no reduction rule that can eliminate it on the outermost level (outside a function). We can't simply add a rule XT[exn] ⇝ exn, since that would introduce overlapping rules.

I see two ways to fix this in the future: (1) switching to a bubbling semantics for exceptions (avoiding overlap), or (2) introducing a separate global reduction relation like we have with threads. The former should go along with changes to other parts of the semantics to stay coherent, the latter I'd rather do after we have merged with threads. Hence I don't want to do either in this PR.

rossberg · 2023-10-19T09:55:20Z

document/core/exec/instructions.rst

+      \iff & F.\AMODULE.\MITAGS[x] = a \\
+      \land & S.\STAGS[a].\TAGITYPE = [t^n] \toF [] \\
+      \land & \X{exn} = \{ \EITAG~a, \EIFIELDS~\val^n \} \\
+      \land & S' = S \with \SEXNS = S.\SEXNS~\X{exn} ) \\


References need internal identity, because it can become observable in the host, e.g. in JS. This is analogous to functions, which are likewise immutable.

(The lack of exn identity was one of the problems we faced with the JS API spec in the old proposal.)

rossberg · 2023-10-19T09:58:44Z

document/core/util/macros.def

@@ -1280,6 +1290,7 @@
 .. |vdashglobalinst| mathdef:: \xref{appendix/properties}{valid-globalinst}{\vdash}


Indeed, fixed.

conrad-watt

In the longer term, I'd like to revisit the way the exception "value" is formalised, but beyond that things seem fine.

* Reintroduce exnref * Fix type_of * Simplify parser * Implement 1b * Change opcodes for catch/catch_all to avoid conflict * Put catch clauses first * Remove obsolete Delegating cases * Change exn type opcode to -0x17 * Switch to B' variant * [interpreter] Add boilerplate for ref.exn result patterns * [ci] Deactivate node run, since it can't handle try_table yet * Try -> TryTable in AST * [spec] Update spec for option B' (#283) * Deactivate Bikeshed * [spec/tests] Specification of legacy exceptions + tests (#284) * [legacy] Create specification doc for legacy exception handling * [test] Create infra for legacy tests

[spec] Update spec for option B'

a252a00

rossberg mentioned this pull request Oct 14, 2023

Proposed instruction format for reintroducing exnref #281

Open

rossberg added 3 commits October 14, 2023 14:25

Fix layout bugs

55db8d2

Typos

5b23269

[jsapi] Ban exnref in JS for now

a83562c

rossberg mentioned this pull request Oct 15, 2023

[interpreter/tests] Switch to Option B' #285

Merged

titzer approved these changes Oct 16, 2023

View reviewed changes

conrad-watt reviewed Oct 19, 2023

View reviewed changes

Fix cross-ref

fd20cf4

rossberg commented Oct 19, 2023

View reviewed changes

conrad-watt approved these changes Oct 20, 2023

View reviewed changes

rossberg merged commit a905e9b into exnref-1b Oct 20, 2023

rossberg deleted the exnref-1b-spec branch October 20, 2023 18:49

tanishiking mentioned this pull request Mar 27, 2024

Fix #32: Implement exception handling. tanishiking/scala-wasm#38

Merged

q82419 mentioned this pull request Aug 6, 2024

Add example for doing exception handling WasmEdge/WasmEdge#2406

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[spec] Update spec for option B' #283

[spec] Update spec for option B' #283

rossberg commented Oct 14, 2023

conrad-watt commented Oct 14, 2023

titzer left a comment

rossberg commented Oct 16, 2023

rossberg commented Oct 16, 2023

conrad-watt commented Oct 19, 2023

conrad-watt commented Oct 19, 2023 •

edited

Loading

conrad-watt Oct 19, 2023

rossberg Oct 19, 2023

conrad-watt Oct 19, 2023

rossberg Oct 19, 2023

conrad-watt Oct 19, 2023

rossberg Oct 19, 2023

conrad-watt Oct 19, 2023

rossberg Oct 19, 2023

rossberg left a comment •

edited

Loading

rossberg Oct 19, 2023

rossberg Oct 19, 2023

rossberg Oct 19, 2023

rossberg Oct 19, 2023

conrad-watt left a comment

		@@ -1280,6 +1290,7 @@
		.. \|vdashglobalinst\| mathdef:: \xref{appendix/properties}{valid-globalinst}{\vdash}

[spec] Update spec for option B' #283

[spec] Update spec for option B' #283

Conversation

rossberg commented Oct 14, 2023

conrad-watt commented Oct 14, 2023

titzer left a comment

Choose a reason for hiding this comment

rossberg commented Oct 16, 2023

rossberg commented Oct 16, 2023

conrad-watt commented Oct 19, 2023

conrad-watt commented Oct 19, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

rossberg left a comment • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

conrad-watt left a comment

Choose a reason for hiding this comment

conrad-watt commented Oct 19, 2023 •

edited

Loading

rossberg left a comment •

edited

Loading