WasmFX documents&examples (#46)

WebAssembly · Apr 12, 2024 · 1d67c4d · 1d67c4d
1 parent 3ec1e39
commit 1d67c4d
Show file tree

Hide file tree

Showing 14 changed files with 589 additions and 401 deletions.
diff --git a/proposals/continuations/Explainer.md b/proposals/continuations/Explainer.md
diff --git a/proposals/continuations/Overview.md b/proposals/continuations/Overview.md
@@ -19,33 +19,40 @@ Based on [typed reference proposal](https://github.com/WebAssembly/function-refe
   - `cont.new $ct : [(ref null? $ft)] -> [(ref $ct)]`
     - iff `$ct = cont $ft`
 
-* `cont.bind <typidx>` binds a continuation to (partial) arguments
-  - `cont.bind $ct : [t3* (ref null? $ct')] -> [(ref $ct)]`
+* `cont.bind <typeidx> <typeidx>` binds a continuation to (partial) arguments
+  - `cont.bind $ct $ct' : [t3* (ref null? $ct)] -> [(ref $ct')]`
     - iff `$ct = cont $ft`
-    - and `$ft = [t1*] -> [t2*]`
+    - and `$ft = [t3* t1*] -> [t2*]`
     - and `$ct' = cont $ft'`
-    - and `$ft' = [t3* t1'*] -> [t2'*]`
-    - and `[t1'*] -> [t2'*] <: [t1*] -> [t2*]`
+    - and `$ft' = [t1'*] -> [t2'*]`
+    - and `[t1*] -> [t2*] <: [t1'*] -> [t2'*]`
 
 * `suspend <tagidx>` suspends the current continuation
   - `suspend $t : [t1*] -> [t2*]`
     - iff `tag $t : [t1*] -> [t2*]`
 
-* `resume (tag <tagidx> <labelidx>)*` resumes a continuation
-  - `resume (tag $e $l)* : [t1* (ref null? $ct)] -> [t2*]`
+* `resume <typeidx> (tag <tagidx> <labelidx>)*` resumes a continuation
+  - `resume $ct (tag $t $l)* : [t1* (ref null? $ct)] -> [t2*]`
     - iff `$ct = cont $ft`
     - and `$ft = [t1*] -> [t2*]`
     - and `(tag $t : [te1*] -> [te2*])*`
     - and `(label $l : [te1'* (ref null? $ct')])*`
     - and `([te1*] <: [te1'*])*`
     - and `($ct' = cont $ft')*`
-    - and `([te2*] -> [t2*] <: $ft')*`
+    - and `$ft' = [t1'*] -> [t2'*]`
+    - and `([te2*] -> [t2*] <: [t1'*] -> [t2'*])*`
 
-* `resume_throw <tagidx>` aborts a continuation
-  - `resume_throw $e : [te* (ref null? $ct)] -> [t2*]`
-    - iff `exception $e : [te*]`
+* `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*] -> [])`
     - and `$ct = cont $ft`
     - and `$ft = [t1*] -> [t2*]`
+    - and `(tag $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'*])*`
 
 * `barrier <blocktype> <instr>* end` blocks suspension
   - `barrier $l bt instr* end : [t1*] -> [t2*]`
@@ -111,36 +118,37 @@ H^ea ::=
   - and `$ct = cont $ft`
   - and `$ft = [t1^n] -> [t2*]`
 
-* `S; F; (ref.null t) (cont.bind $ct)  -->  S; F; trap`
+* `S; F; (ref.null t) (cont.bind $ct $ct')  -->  S; F; trap`
 
-* `S; F; (ref.cont ca) (cont.bind $ct)  -->  S'; F; trap`
+* `S; F; (ref.cont ca) (cont.bind $ct $ct')  -->  S'; F; trap`
   - iff `S.conts[ca] = epsilon`
 
-* `S; F; v^n (ref.cont ca) (cont.bind $ct)  -->  S'; F; (ref.const |S.conts|)`
+* `S; F; v^n (ref.cont ca) (cont.bind $ct $ct')  -->  S'; F; (ref.const |S.conts|)`
   - iff `S.conts[ca] = (E' : n')`
-  - and `$ct = cont $ft`
-  - and `$ft = [t1'*] -> [t2'*]`
+  - and `$ct' = cont $ft'`
+  - and `$ft' = [t1'*] -> [t2'*]`
   - and `n = n' - |t1'*|`
   - and `S' = S with conts[ca] = epsilon with conts += (E : |t1'*|)`
   - and `E = E'[v^n _]`
 
-* `S; F; (ref.null t) (resume (tag $e $l)*)  -->  S; F; trap`
+* `S; F; (ref.null t) (resume $ct (tag $e $l)*)  -->  S; F; trap`
 
-* `S; F; (ref.cont ca) (resume (tag $e $l)*)  -->  S; F; trap`
+* `S; F; (ref.cont ca) (resume $ct (tag $e $l)*)  -->  S; F; trap`
   - iff `S.conts[ca] = epsilon`
 
-* `S; F; v^n (ref.cont ca) (resume (tag $e $l)*)  -->  S'; F; handle{(ea $l)*} E[v^n] end`
+* `S; F; v^n (ref.cont ca) (resume $ct (tag $t $l)*)  -->  S'; F; handle{(ea $l)*} E[v^n] end`
   - iff `S.conts[ca] = (E : n)`
-  - and `(ea = F.tags[$e])*`
+  - and `(ea = F.tags[$t])*`
   - and `S' = S with conts[ca] = epsilon`
 
-* `S; F; (ref.null t) (resume_throw $e)  -->  S; F; trap`
+* `S; F; (ref.null t) (resume_throw $ct $e (tag $t $l)*)  -->  S; F; trap`
 
-* `S; F; (ref.cont ca) (resume_throw $e)  -->  S; F; trap`
+* `S; F; (ref.cont ca) (resume_throw $ct $e (tag $t $l)*)  -->  S; F; trap`
   - iff `S.conts[ca] = epsilon`
 
-* `S; F; v^m (ref.cont ca) (resume_throw $e)  -->  S'; F; E[v^m (throw $e)]`
+* `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`
   - iff `S.conts[ca] = (E : n)`
+  - and `(ea = F.tags[$t])*`
   - and `S.tags[F.tags[$e]].type = [t1^m] -> [t2*]`
   - and `S' = S with conts[ca] = epsilon`
 

diff --git a/proposals/continuations/examples/actor-lwt.wast b/proposals/continuations/examples/actor-lwt.wast
@@ -52,7 +52,7 @@
     (loop $l
       (if (i32.eqz (local.get $n))
         (then (suspend $send (i32.const 42) (local.get $p)))
-        (else (local.set $p (suspend $spawn (cont.bind (type $cont) (local.get $p) (cont.new (type $i-cont) (ref.func $next)))))
+        (else (local.set $p (suspend $spawn (cont.bind $i-cont $cont (local.get $p) (cont.new $i-cont (ref.func $next)))))
               (local.set $n (i32.sub (local.get $n) (i32.const 1)))
               (br $l))
       )
@@ -73,7 +73,7 @@
   (table $queue 0 (ref null $cont))
   (memory 1)
 
-  (exception $too-many-mailboxes)
+  (tag $too-many-mailboxes)
 
   (global $qdelta i32 (i32.const 10))
 
@@ -190,8 +190,8 @@
 
   (func $log (import "spectest" "print_i32") (param i32))
 
-  (exception $too-many-mailboxes)
-  (exception $too-many-messages)
+  (tag $too-many-mailboxes)
+  (tag $too-many-messages)
 
   (memory 1)
 
@@ -274,7 +274,7 @@
     (loop $l
       (if (i32.eqz (local.get $n))
         (then (suspend $send (i32.const 42) (local.get $p)))
-        (else (local.set $p (suspend $spawn (cont.bind (type $cont) (local.get $p) (cont.new (type $i-cont) (ref.func $next)))))
+        (else (local.set $p (suspend $spawn (cont.bind $i-cont $cont (local.get $p) (cont.new $i-cont (ref.func $next)))))
               (local.set $n (i32.sub (local.get $n) (i32.const 1)))
               (br $l))
       )
@@ -371,7 +371,7 @@
       (if (call $queue-empty) (then (return)))
       (block $on_yield (result (ref $cont))
         (block $on_fork (result (ref $cont) (ref $cont))
-          (resume (tag $yield $on_yield) (tag $fork $on_fork)
+          (resume $cont (tag $yield $on_yield) (tag $fork $on_fork)
             (call $dequeue)
           )
           (br $l)  ;; thread terminated
@@ -397,8 +397,8 @@
 
   ;; -1 means empty
 
-  (exception $too-many-mailboxes)
-  (exception $too-many-messages)
+  (tag $too-many-mailboxes)
+  (tag $too-many-messages)
 
   (memory 1)
 
@@ -489,52 +489,52 @@
   (elem declare func $actk)
 
   (func $actk (param $mine i32) (param $nextk (ref $cont))
+    (local $ik (ref $i-cont))
+    (local $k (ref $cont))
+    (local $you (ref $cont))
+    (local $yours i32)
     (loop $l
       (block $on_self (result (ref $i-cont))
         (block $on_spawn (result (ref $cont) (ref $i-cont))
           (block $on_send (result i32 i32 (ref $cont))
             (block $on_recv (result (ref $i-cont))
-               (resume (tag $self $on_self)
-                       (tag $spawn $on_spawn)
-                       (tag $send $on_send)
-                       (tag $recv $on_recv)
-                       (local.get $nextk)
+               (resume $cont (tag $self $on_self)
+                             (tag $spawn $on_spawn)
+                             (tag $send $on_send)
+                             (tag $recv $on_recv)
+                             (local.get $nextk)
                )
                (return)
             ) ;;   $on_recv (result (ref $i-cont))
-            (let (local $ik (ref $i-cont))
-              ;; block this thread until the mailbox is non-empty
-              (loop $blocked
-                (if (call $empty-mb (local.get $mine))
-                    (then (suspend $yield)
-                          (br $blocked))
-                )
+            (local.set $ik)
+            ;; block this thread until the mailbox is non-empty
+            (loop $blocked
+              (if (call $empty-mb (local.get $mine))
+                  (then (suspend $yield)
+                        (br $blocked))
               )
-              (local.set $nextk (cont.bind (type $cont) (call $recv-from-mb (local.get $mine)) (local.get $ik)))
             )
+            (local.set $nextk (cont.bind $i-cont $cont (call $recv-from-mb (local.get $mine)) (local.get $ik)))
             (br $l)
           ) ;;   $on_send (result i32 i32 (ref $cont))
-          (let (param i32 i32) (local $k (ref $cont))
-            (call $send-to-mb)
-            (local.set $nextk (local.get $k))
-          )
+          (local.set $k)
+          (call $send-to-mb)
+          (local.set $nextk (local.get $k))
           (br $l)
         ) ;;   $on_spawn (result (ref $cont) (ref $i-cont))
-        (let (local $you (ref $cont)) (local $ik (ref $i-cont))
-          (call $new-mb)
-          (let (local $yours i32)
-            (suspend $fork (cont.bind (type $cont)
-                                      (local.get $yours)
-                                      (local.get $you)
-                                      (cont.new (type $ic-cont) (ref.func $actk))))
-            (local.set $nextk (cont.bind (type $cont) (local.get $yours) (local.get $ik)))
-          )
-        )
+        (local.set $ik)
+        (local.set $you)
+        (call $new-mb)
+        (local.set $yours)
+        (suspend $fork (cont.bind $ic-cont $cont
+                                  (local.get $yours)
+                                  (local.get $you)
+                                  (cont.new $ic-cont (ref.func $actk))))
+        (local.set $nextk (cont.bind $i-cont $cont (local.get $yours) (local.get $ik)))
         (br $l)
       ) ;;   $on_self (result (ref $i-cont))
-      (let (local $ik (ref $i-cont))
-        (local.set $nextk (cont.bind (type $cont) (local.get $mine) (local.get $ik)))
-      )
+      (local.set $ik)
+      (local.set $nextk (cont.bind $i-cont $cont (local.get $mine) (local.get $ik)))
       (br $l)
     )
   )
@@ -560,7 +560,7 @@
   (func $scheduler (import "scheduler" "run") (param $k (ref $cont)))
 
   (func $run-actor (export "run-actor") (param $k (ref $cont))
-    (call $scheduler (cont.bind (type $cont) (local.get $k) (cont.new (type $cont-cont) (ref.func $act))))
+    (call $scheduler (cont.bind $cont-cont $cont (local.get $k) (cont.new $cont-cont (ref.func $act))))
   )
 )
 (register "actor-scheduler")
@@ -578,7 +578,7 @@
   (func $chain (import "chain" "chain") (param $n i32))
 
   (func $run-chain (export "run-chain") (param $n i32)
-    (call $run-actor (cont.bind (type $cont) (local.get $n) (cont.new (type $i-cont) (ref.func $chain))))
+    (call $run-actor (cont.bind $i-cont $cont (local.get $n) (cont.new $i-cont (ref.func $chain))))
   )
 )
 

diff --git a/proposals/continuations/examples/actor.wast b/proposals/continuations/examples/actor.wast
@@ -52,7 +52,7 @@
     (loop $l
       (if (i32.eqz (local.get $n))
         (then (suspend $send (i32.const 42) (local.get $p)))
-        (else (local.set $p (suspend $spawn (cont.bind (type $cont) (local.get $p) (cont.new (type $i-cont) (ref.func $next)))))
+        (else (local.set $p (suspend $spawn (cont.bind $i-cont $cont (local.get $p) (cont.new $i-cont (ref.func $next)))))
               (local.set $n (i32.sub (local.get $n) (i32.const 1)))
               (br $l))
       )
@@ -73,7 +73,7 @@
   (table $queue 0 (ref null $cont))
   (memory 1)
 
-  (exception $too-many-mailboxes)
+  (tag $too-many-mailboxes)
 
   (global $qdelta i32 (i32.const 10))
 
@@ -190,8 +190,8 @@
 
   (func $log (import "spectest" "print_i32") (param i32))
 
-  (exception $too-many-mailboxes)
-  (exception $too-many-messages)
+  (tag $too-many-mailboxes)
+  (tag $too-many-messages)
 
   (memory 1)
 
@@ -296,10 +296,10 @@
     (local $res i32)
     (suspend $recv)
     (local.set $res)
-    (resume (local.get $res) (local.get $ik))
+    (resume $i-cont (local.get $res) (local.get $ik))
   )
   (func $recv-again (param $ik (ref $i-cont)) (result (ref $cont))
-    (cont.bind (type $cont) (local.get $ik) (cont.new (type $i-cont-cont) (ref.func $recv-againf)))
+    (cont.bind $i-cont-cont $cont (local.get $ik) (cont.new $i-cont-cont (ref.func $recv-againf)))
   )
 
   ;; There are multiple ways of avoiding the need for
@@ -317,6 +317,10 @@
 
   (func $run (export "run") (param $nextk (ref null $cont))
     (local $mine i32)                ;; current mailbox
+    (local $ik (ref $i-cont))
+    (local $k (ref $cont))
+    (local $you (ref $cont))
+    (local $yours i32)
     (call $init)
     (local.set $mine (call $new-mb))
     (loop $l
@@ -325,48 +329,44 @@
         (block $on_spawn (result (ref $cont) (ref $i-cont))
           (block $on_send (result i32 i32 (ref $cont))
             (block $on_recv (result (ref $i-cont))
-               (resume (tag $self $on_self)
-                       (tag $spawn $on_spawn)
-                       (tag $send $on_send)
-                       (tag $recv $on_recv)
-                       (local.get $nextk)
+               (resume $cont (tag $self $on_self)
+                             (tag $spawn $on_spawn)
+                             (tag $send $on_send)
+                             (tag $recv $on_recv)
+                             (local.get $nextk)
                )
                (local.set $mine (call $dequeue-mb))
                (local.set $nextk (call $dequeue-k))
                (br $l)
             ) ;;   $on_recv (result (ref $i-cont))
-            (let (local $ik (ref $i-cont))
-              ;; block this thread until the mailbox is non-empty
-              (if (call $empty-mb (local.get $mine))
-                  (then (call $enqueue-mb (local.get $mine))
-                        (call $enqueue-k (call $recv-again (local.get $ik)))
-                        (local.set $mine (call $dequeue-mb))
-                        (local.set $nextk (call $dequeue-k))
-                        (br $l))
-              )
-              (local.set $nextk (cont.bind (type $cont) (call $recv-from-mb (local.get $mine)) (local.get $ik)))
+            (local.set $ik)
+            ;; block this thread until the mailbox is non-empty
+            (if (call $empty-mb (local.get $mine))
+                (then (call $enqueue-mb (local.get $mine))
+                      (call $enqueue-k (call $recv-again (local.get $ik)))
+                      (local.set $mine (call $dequeue-mb))
+                      (local.set $nextk (call $dequeue-k))
+                      (br $l))
             )
+            (local.set $nextk (cont.bind $i-cont $cont (call $recv-from-mb (local.get $mine)) (local.get $ik)))
             (br $l)
           ) ;;   $on_send (result i32 i32 (ref $cont))
-          (let (param i32 i32) (local $k (ref $cont))
-            (call $send-to-mb)
-            (local.set $nextk (local.get $k))
-          )
+          (local.set $k)
+          (call $send-to-mb)
+          (local.set $nextk (local.get $k))
           (br $l)
         ) ;;   $on_spawn (result (ref $cont) (ref $i-cont))
-        (let (local $you (ref $cont)) (local $ik (ref $i-cont))
-          (call $new-mb)
-          (let (local $yours i32)
-            (call $enqueue-mb (local.get $yours))
-            (call $enqueue-k (local.get $you))
-            (local.set $nextk (cont.bind (type $cont) (local.get $yours) (local.get $ik)))
-          )
-        )
+        (local.set $ik)
+        (local.set $you)
+        (call $new-mb)
+        (local.set $yours)
+        (call $enqueue-mb (local.get $yours))
+        (call $enqueue-k (local.get $you))
+        (local.set $nextk (cont.bind $i-cont $cont (local.get $yours) (local.get $ik)))
         (br $l)
       ) ;;   $on_self (result (ref $i-cont))
-      (let (local $ik (ref $i-cont))
-        (local.set $nextk (cont.bind (type $cont) (local.get $mine) (local.get $ik)))
-      )
+      (local.set $ik)
+      (local.set $nextk (cont.bind $i-cont $cont (local.get $mine) (local.get $ik)))
       (br $l)
     )
   )
@@ -388,7 +388,7 @@
   (func $chain (import "chain" "chain") (param $n i32))
 
   (func $run-chain (export "run-chain") (param $n i32)
-    (call $act (cont.bind (type $cont) (local.get $n) (cont.new (type $i-cont) (ref.func $chain))))
+    (call $act (cont.bind $i-cont $cont (local.get $n) (cont.new $i-cont (ref.func $chain))))
   )
 )