Skip to content

Commit

Permalink
Resume table syntax (#39)
Browse files Browse the repository at this point in the history
* Resume table syntax

This patch changes the syntax of resume tables:

```wast
(resume $ct (tag $t $h)) => (resume $ct (on $t $h))
(resume_throw $ct $e (tag $t $h)) => (resume_throw $ct $e (on $t $h))
```

* Update examples

* Update overview document

* Update explainer document
  • Loading branch information
dhil authored Jul 31, 2024
1 parent 2f6a9e8 commit 3a32c7f
Show file tree
Hide file tree
Showing 18 changed files with 103 additions and 324 deletions.
4 changes: 2 additions & 2 deletions interpreter/text/arrange.ml
Original file line number Diff line number Diff line change
Expand Up @@ -525,10 +525,10 @@ let rec instr e =
| Suspend x -> "suspend " ^ var x, []
| Resume (x, xys) ->
"resume " ^ var x,
List.map (fun (x, y) -> Node ("tag " ^ var x ^ " " ^ var y, [])) xys
List.map (fun (x, y) -> Node ("on " ^ var x ^ " " ^ var y, [])) xys
| ResumeThrow (x, y, xys) ->
"resume_throw " ^ var x ^ " " ^ var y,
List.map (fun (x, y) -> Node ("tag " ^ var x ^ " " ^ var y, [])) xys
List.map (fun (x, y) -> Node ("on " ^ var x ^ " " ^ var y, [])) xys
| Barrier (bt, es) -> "barrier", block_type bt @ list instr es
| Throw x -> "throw " ^ var x, []
| ThrowRef -> "throw_ref", []
Expand Down
1 change: 1 addition & 0 deletions interpreter/text/lexer.mll
Original file line number Diff line number Diff line change
Expand Up @@ -769,6 +769,7 @@ rule token = parse
| "data" -> DATA
| "declare" -> DECLARE
| "offset" -> OFFSET
| "on" -> ON
| "item" -> ITEM
| "import" -> IMPORT
| "export" -> EXPORT
Expand Down
6 changes: 3 additions & 3 deletions interpreter/text/parser.mly
Original file line number Diff line number Diff line change
Expand Up @@ -338,7 +338,7 @@ let parse_annots (m : module_) : Custom.section list =
%token VEC_SHUFFLE
%token<int -> Ast.instr'> VEC_EXTRACT VEC_REPLACE
%token FUNC START TYPE PARAM RESULT LOCAL GLOBAL CONT
%token TABLE ELEM MEMORY TAG DATA DECLARE OFFSET ITEM IMPORT EXPORT
%token TABLE ELEM MEMORY ON TAG DATA DECLARE OFFSET ITEM IMPORT EXPORT
%token MODULE BIN QUOTE
%token SCRIPT REGISTER INVOKE GET
%token ASSERT_MALFORMED ASSERT_INVALID ASSERT_UNLINKABLE
Expand Down Expand Up @@ -782,7 +782,7 @@ resume_instr_instr :
let hs, es = $4 c in resume_throw x tag hs @@ loc1, es }

resume_instr_handler_instr :
| LPAR TAG var var RPAR resume_instr_handler_instr
| LPAR ON var var RPAR resume_instr_handler_instr
{ fun c -> let hs, es = $6 c in ($3 c tag, $4 c label) :: hs, es }
| instr1
{ fun c -> [], $1 c }
Expand Down Expand Up @@ -940,7 +940,7 @@ call_expr_results :
{ fun c -> [], $1 c }

resume_expr_handler :
| LPAR TAG var var RPAR resume_expr_handler
| LPAR ON var var RPAR resume_expr_handler
{ fun c -> let hs, es = $6 c in ($3 c tag, $4 c label) :: hs, es }
| expr_list
{ fun c -> [], $1 c }
Expand Down
34 changes: 17 additions & 17 deletions proposals/continuations/Explainer.md
Original file line number Diff line number Diff line change
Expand Up @@ -216,7 +216,7 @@ a *handler*, which handles subsequent control suspensions within the
continuation.

```wast
resume $ct (tag $e $l)* : [tp* (ref $ct)] -> [tr*]
resume $ct (on $e $l)* : [tp* (ref $ct)] -> [tr*]
where:
- $ct = cont [tp*] -> [tr*]
```
Expand All @@ -234,7 +234,7 @@ abortive action" which causes the stack to be unwound.


```wast
resume_throw $ct $exn (tag $e $l)* : [tp* (ref $ct)])] -> [tr*]
resume_throw $ct $exn (on $e $l)* : [tp* (ref $ct)])] -> [tr*]
where:
- $ct = cont [ta*] -> [tr*]
- $exn : [tp*] -> []
Expand Down Expand Up @@ -423,7 +423,7 @@ We now define a scheduler.
(loop $l
(if (call $queue-empty) (then (return)))
(block $on_yield (result (ref $cont))
(resume $cont (tag $yield $on_yield)
(resume $cont (on $yield $on_yield)
(call $dequeue)
)
(br $l) ;; thread terminated
Expand All @@ -440,7 +440,7 @@ We assume a suitable interface to a queue of active threads
represented as continuations. The scheduler is a loop which repeatedly
runs the continuation (thread) at the head of the queue. It does so by
resuming the continuation with a handler for the `$yield` tag. The
handler `(tag $yield $on_yield)` specifies that the `$yield` tag
handler `(on $yield $on_yield)` specifies that the `$yield` tag
is handled by running the code immediately following the block
labelled with `$on_yield`, the `$on_yield` clause. The result of the
block `(result (ref $cont))` declares that there will be a
Expand Down Expand Up @@ -598,8 +598,8 @@ thread to completion without actually yielding.
(if (ref.is_null (local.get $nextk)) (then (return)))
(block $on_yield (result (ref $cont))
(block $on_fork (result (ref $cont) (ref $cont))
(resume $cont (tag $yield $on_yield)
(tag $fork $on_fork)
(resume $cont (on $yield $on_yield)
(on $fork $on_fork)
(local.get $nextk)
)
(local.set $nextk (call $dequeue))
Expand Down Expand Up @@ -673,8 +673,8 @@ schedulers.
(if (ref.is_null (local.get $nextk)) (then (return)))
(block $on_yield (result (ref $cont))
(block $on_fork (result (ref $cont) (ref $cont))
(resume $cont (tag $yield $on_yield)
(tag $fork $on_fork)
(resume $cont (on $yield $on_yield)
(on $fork $on_fork)
(local.get $nextk)
)
(local.set $nextk (call $dequeue))
Expand All @@ -697,8 +697,8 @@ schedulers.
(if (ref.is_null (local.get $nextk)) (then (return)))
(block $on_yield (result (ref $cont))
(block $on_fork (result (ref $cont) (ref $cont))
(resume $cont (tag $yield $on_yield)
(tag $fork $on_fork)
(resume $cont (on $yield $on_yield)
(on $fork $on_fork)
(local.get $nextk)
)
(local.set $nextk (call $dequeue))
Expand All @@ -721,8 +721,8 @@ schedulers.
(if (ref.is_null (local.get $nextk)) (then (return)))
(block $on_yield (result (ref $cont))
(block $on_fork (result (ref $cont) (ref $cont))
(resume $cont (tag $yield $on_yield)
(tag $fork $on_fork)
(resume $cont (on $yield $on_yield)
(on $fork $on_fork)
(local.get $nextk)
)
(local.set $nextk (call $dequeue))
Expand All @@ -746,8 +746,8 @@ schedulers.
(if (ref.is_null (local.get $nextk)) (then (return)))
(block $on_yield (result (ref $cont))
(block $on_fork (result (ref $cont) (ref $cont))
(resume $cont (tag $yield $on_yield)
(tag $fork $on_fork)
(resume $cont (on $yield $on_yield)
(on $fork $on_fork)
(local.get $nextk)
)
(local.set $nextk (call $dequeue))
Expand Down Expand Up @@ -933,7 +933,7 @@ First we implement control/prompt.
(tag $control (export "control") (param (ref $cont-func))) ;; control : [([contref ([] -> [])] -> [])] -> []
(func $prompt (export "prompt") (param $nextk (ref null $cont)) ;; prompt : [(contref ([] -> []))] -> []
(block $on_control (result (ref $cont-func) (ref $cont))
(resume $cont (tag $control $on_control)
(resume $cont (on $control $on_control)
(local.get $nextk))
(return)
) ;; $on_control (param (ref $cont-func) (ref $cont))
Expand Down Expand Up @@ -1439,7 +1439,7 @@ executing a variant of the `resume` instruction and is passed to the
continuation:

```wast
resume_with $ht $ct (tag $e $l)* : [ t1* (ref $ht) (ref $ct) ] -> [ t2* ]
resume_with $ht $ct (on $e $l)* : [ t1* (ref $ht) (ref $ct) ] -> [ t2* ]
where:
- $ht = handler t2*
- $ct = cont ([ (ref $ht) t1* ] -> [ t2* ])
Expand Down Expand Up @@ -1491,7 +1491,7 @@ instruction for switching directly to another continuation:
This behaves as if there was a built-in tag

```wast
(tag $Switch (param t1* (ref $ct1)) (result t3*))
(on $Switch (param t1* (ref $ct1)) (result t3*))
```

with which the computation suspends to the handler, and the handler
Expand Down
26 changes: 13 additions & 13 deletions proposals/continuations/Overview.md
Original file line number Diff line number Diff line change
Expand Up @@ -31,23 +31,23 @@ Based on [typed reference proposal](https://github.com/WebAssembly/function-refe
- `suspend $t : [t1*] -> [t2*]`
- iff `tag $t : [t1*] -> [t2*]`

* `resume <typeidx> (tag <tagidx> <labelidx>)*` resumes a continuation
- `resume $ct (tag $t $l)* : [t1* (ref null? $ct)] -> [t2*]`
* `resume <typeidx> (on <tagidx> <labelidx>)*` resumes a continuation
- `resume $ct (on $t $l)* : [t1* (ref null? $ct)] -> [t2*]`
- iff `$ct = cont $ft`
- and `$ft = [t1*] -> [t2*]`
- and `(tag $t : [te1*] -> [te2*])*`
- and `(on $t : [te1*] -> [te2*])*`
- and `(label $l : [te1'* (ref null? $ct')])*`
- and `([te1*] <: [te1'*])*`
- and `($ct' = cont $ft')*`
- and `$ft' = [t1'*] -> [t2'*]`
- and `([te2*] -> [t2*] <: [t1'*] -> [t2'*])*`

* `resume_throw <typeidx> <tagidx> (tag <tagidx> <labelidx>)` aborts a continuation
- `resume_throw $ct $e (tag $t $l): [te* (ref null? $ct)] -> [t2*]`
- iff `(tag $e : [te*] -> [])`
* `resume_throw <typeidx> <tagidx> (on <tagidx> <labelidx>)` aborts a continuation
- `resume_throw $ct $e (on $t $l): [te* (ref null? $ct)] -> [t2*]`
- iff `(on $e : [te*] -> [])`
- and `$ct = cont $ft`
- and `$ft = [t1*] -> [t2*]`
- and `(tag $t : [te1*] -> [te2*])*`
- and `(on $t : [te1*] -> [te2*])*`
- and `(label $l : [te1'* (ref null? $ct')])*`
- and `([te1*] <: [te1'*])*`
- and `($ct' = cont $ft')*`
Expand Down Expand Up @@ -131,22 +131,22 @@ H^ea ::=
- and `S' = S with conts[ca] = epsilon with conts += (E : |t1'*|)`
- and `E = E'[v^n _]`

* `S; F; (ref.null t) (resume $ct (tag $e $l)*) --> S; F; trap`
* `S; F; (ref.null t) (resume $ct (on $e $l)*) --> S; F; trap`

* `S; F; (ref.cont ca) (resume $ct (tag $e $l)*) --> S; F; trap`
* `S; F; (ref.cont ca) (resume $ct (on $e $l)*) --> S; F; trap`
- iff `S.conts[ca] = epsilon`

* `S; F; v^n (ref.cont ca) (resume $ct (tag $t $l)*) --> S'; F; handle{(ea $l)*} E[v^n] end`
* `S; F; v^n (ref.cont ca) (resume $ct (on $t $l)*) --> S'; F; handle{(ea $l)*} E[v^n] end`
- iff `S.conts[ca] = (E : n)`
- and `(ea = F.tags[$t])*`
- and `S' = S with conts[ca] = epsilon`

* `S; F; (ref.null t) (resume_throw $ct $e (tag $t $l)*) --> S; F; trap`
* `S; F; (ref.null t) (resume_throw $ct $e (on $t $l)*) --> S; F; trap`

* `S; F; (ref.cont ca) (resume_throw $ct $e (tag $t $l)*) --> S; F; trap`
* `S; F; (ref.cont ca) (resume_throw $ct $e (on $t $l)*) --> S; F; trap`
- iff `S.conts[ca] = epsilon`

* `S; F; v^m (ref.cont ca) (resume_throw $ct $e (tag $t $l)*) --> S'; F; handle{(ea $l)*} E[v^m (throw $e)] end`
* `S; F; v^m (ref.cont ca) (resume_throw $ct $e (on $t $l)*) --> S'; F; handle{(ea $l)*} E[v^m (throw $e)] end`
- iff `S.conts[ca] = (E : n)`
- and `(ea = F.tags[$t])*`
- and `S.tags[F.tags[$e]].type = [t1^m] -> [t2*]`
Expand Down
Loading

0 comments on commit 3a32c7f

Please sign in to comment.