Skip to content

Commit

Permalink
Implement single-shot semantics (#7)
Browse files Browse the repository at this point in the history
  • Loading branch information
rossberg authored Feb 25, 2021
1 parent 6b0b593 commit 707dec0
Show file tree
Hide file tree
Showing 11 changed files with 76 additions and 23 deletions.
2 changes: 1 addition & 1 deletion interpreter/binary/decode.ml
Original file line number Diff line number Diff line change
Expand Up @@ -560,7 +560,7 @@ let rec instr s =
let bt = block_type s in
let es' = instr_block s in
end_ s;
guard bt es'
barrier bt es'

| 0xfc as b ->
(match vu32 s with
Expand Down
2 changes: 1 addition & 1 deletion interpreter/binary/encode.ml
Original file line number Diff line number Diff line change
Expand Up @@ -218,7 +218,7 @@ let encode m =
| Suspend x -> op 0xe1; var x
| Resume xls -> op 0xe2; vec var_pair xls
| ResumeThrow x -> op 0xe3; var x
| Guard (bt, es) -> op 0xe4; block_type bt; list instr es; end_ ()
| Barrier (bt, es) -> op 0xe4; block_type bt; list instr es; end_ ()

| Drop -> op 0x1a
| Select None -> op 0x1b
Expand Down
22 changes: 15 additions & 7 deletions interpreter/exec/eval.ml
Original file line number Diff line number Diff line change
Expand Up @@ -78,7 +78,7 @@ and admin_instr' =
and ctxt = code -> code

type cont = int * ctxt (* TODO: represent type properly *)
type ref_ += ContRef of cont
type ref_ += ContRef of cont option ref

let () =
let type_of_ref' = !Value.type_of_ref' in
Expand Down Expand Up @@ -314,7 +314,7 @@ let rec step (c : config) : config =
| ContNew x, Ref (FuncRef f) :: vs ->
let FuncType (ts, _) = Func.type_of f in
let ctxt code = compose code ([], [Invoke f @@ e.at]) in
Ref (ContRef (List.length ts, ctxt)) :: vs, []
Ref (ContRef (ref (Some (List.length ts, ctxt)))) :: vs, []

| Suspend x, vs ->
let evt = event c.frame.inst x in
Expand All @@ -325,22 +325,30 @@ let rec step (c : config) : config =
| Resume xls, Ref (NullRef _) :: vs ->
vs, [Trapping "null continuation reference" @@ e.at]

| Resume xls, Ref (ContRef (n, ctxt)) :: vs ->
| Resume xls, Ref (ContRef {contents = None}) :: vs ->
vs, [Trapping "continuation resumed twice" @@ e.at]

| Resume xls, Ref (ContRef ({contents = Some (n, ctxt)} as cont)) :: vs ->
let hs = List.map (fun (x, l) -> event c.frame.inst x, l) xls in
let args, vs' = split n vs e.at in
cont := None;
vs', [Handle (Some hs, ctxt (args, [])) @@ e.at]

| ResumeThrow x, Ref (NullRef _) :: vs ->
vs, [Trapping "null continuation reference" @@ e.at]

| ResumeThrow x, Ref (ContRef (n, ctxt)) :: vs ->
| ResumeThrow x, Ref (ContRef {contents = None}) :: vs ->
vs, [Trapping "continuation resumed twice" @@ e.at]

| ResumeThrow x, Ref (ContRef ({contents = Some (n, ctxt)} as cont)) :: vs ->
let evt = event c.frame.inst x in
let EventType (FuncType (ts, _), _) = Event.type_of evt in
let args, vs' = split (List.length ts) vs e.at in
let vs1', es1' = ctxt (args, [Plain (Throw x) @@ e.at]) in
cont := None;
vs1' @ vs', es1'

| Guard (bt, es'), vs ->
| Barrier (bt, es'), vs ->
let FuncType (ts1, _) = block_type c.frame.inst bt e.at in
let args, vs' = split (List.length ts1) vs e.at in
vs', [
Expand Down Expand Up @@ -735,13 +743,13 @@ let rec step (c : config) : config =
vs' @ vs, []

| Handle (None, (vs', {it = Suspending _; at} :: es')), vs ->
vs, [Trapping "guard suspended" @@ at]
vs, [Trapping "barrier hit by suspension" @@ at]

| Handle (Some hs, (vs', {it = Suspending (evt, vs1, ctxt); at} :: es')), vs
when List.mem_assq evt hs ->
let EventType (FuncType (_, ts), _) = Event.type_of evt in
let ctxt' code = compose (ctxt code) (vs', es') in
[Ref (ContRef (List.length ts, ctxt'))] @ vs1 @ vs,
[Ref (ContRef (ref (Some (List.length ts, ctxt'))))] @ vs1 @ vs,
[Plain (Br (List.assq evt hs)) @@ e.at]

| Handle (hso, (vs', {it = Suspending (evt, vs1, ctxt); at} :: es')), vs ->
Expand Down
2 changes: 1 addition & 1 deletion interpreter/syntax/ast.ml
Original file line number Diff line number Diff line change
Expand Up @@ -100,7 +100,7 @@ and instr' =
| Suspend of idx (* suspend continuation *)
| Resume of (idx * idx) list (* resume continuation *)
| ResumeThrow of idx (* abort continuation *)
| Guard of block_type * instr list (* guard against suspension *)
| Barrier of block_type * instr list (* guard against suspension *)
| LocalGet of idx (* read local idxiable *)
| LocalSet of idx (* write local idxiable *)
| LocalTee of idx (* write local idxiable and keep value *)
Expand Down
2 changes: 1 addition & 1 deletion interpreter/syntax/free.ml
Original file line number Diff line number Diff line change
Expand Up @@ -109,7 +109,7 @@ let rec instr (e : instr) =
| RefNull t -> heap_type t
| RefFunc x -> funcs (idx x)
| Const _ | Test _ | Compare _ | Unary _ | Binary _ | Convert _ -> empty
| Block (bt, es) | Loop (bt, es) | Guard (bt, es) -> block_type bt ++ block es
| Block (bt, es) | Loop (bt, es) | Barrier (bt, es) -> block_type bt ++ block es
| If (bt, es1, es2) -> block_type bt ++ block es1 ++ block es2
| Let (bt, ts, es) ->
let free = block_type bt ++ block es in
Expand Down
2 changes: 1 addition & 1 deletion interpreter/syntax/operators.ml
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ let cont_new x = ContNew x
let suspend x = Suspend x
let resume xys = Resume xys
let resume_throw x = ResumeThrow x
let guard bt es = Guard (bt, es)
let barrier bt es = Barrier (bt, es)

let local_get x = LocalGet x
let local_set x = LocalSet x
Expand Down
2 changes: 1 addition & 1 deletion interpreter/text/arrange.ml
Original file line number Diff line number Diff line change
Expand Up @@ -281,7 +281,7 @@ let rec instr e =
"resume",
List.map (fun (x, y) -> Node ("event " ^ var x ^ " " ^ var y, [])) xys
| ResumeThrow x -> "resume_throw " ^ var x, []
| Guard (bt, es) -> "guard", block_type bt @ list instr es
| Barrier (bt, es) -> "barrier", block_type bt @ list instr es
| LocalGet x -> "local.get " ^ var x, []
| LocalSet x -> "local.set " ^ var x, []
| LocalTee x -> "local.tee " ^ var x, []
Expand Down
2 changes: 1 addition & 1 deletion interpreter/text/lexer.mll
Original file line number Diff line number Diff line change
Expand Up @@ -219,7 +219,7 @@ rule token = parse
| "suspend" { SUSPEND }
| "resume" { RESUME }
| "resume_throw" { RESUME_THROW }
| "guard" { GUARD }
| "barrier" { BARRIER }

| "local.get" { LOCAL_GET }
| "local.set" { LOCAL_SET }
Expand Down
10 changes: 5 additions & 5 deletions interpreter/text/parser.mly
Original file line number Diff line number Diff line change
Expand Up @@ -217,7 +217,7 @@ let inline_func_type_explicit (c : context) x ft at =
%token UNREACHABLE NOP DROP SELECT
%token BLOCK END IF THEN ELSE LOOP LET
%token THROW TRY DO CATCH CATCH_ALL
%token CONT_NEW SUSPEND RESUME RESUME_THROW GUARD
%token CONT_NEW SUSPEND RESUME RESUME_THROW BARRIER
%token BR BR_IF BR_TABLE BR_ON_NULL
%token CALL CALL_REF CALL_INDIRECT RETURN RETURN_CALL_REF FUNC_BIND
%token LOCAL_GET LOCAL_SET LOCAL_TEE GLOBAL_GET GLOBAL_SET
Expand Down Expand Up @@ -626,8 +626,8 @@ block_instr :
| TRY labeling_opt block CATCH labeling_end_opt LPAR EXCEPTION var RPAR instr_list END labeling_end_opt
{ fun c -> let c' = $2 c ($5 @ $12) in
let ts, es1 = $3 c' in try_ ts es1 (Some ($8 c' event)) ($10 c') }
| GUARD labeling_opt block END labeling_end_opt
{ fun c -> let c' = $2 c $5 in let bt, es = $3 c' in guard bt es }
| BARRIER labeling_opt block END labeling_end_opt
{ fun c -> let c' = $2 c $5 in let bt, es = $3 c' in barrier bt es }

block :
| type_use block_param_body
Expand Down Expand Up @@ -744,8 +744,8 @@ expr1 : /* Sugar */
{ fun c ->
let bt, (es1, xo, es2) = $2 c in
[], try_ bt es1 xo es2 }
| GUARD labeling_opt block
{ fun c -> let c' = $2 c [] in let bt, es = $3 c' in [], guard bt es }
| BARRIER labeling_opt block
{ fun c -> let c' = $2 c [] in let bt, es = $3 c' in [], barrier bt es }

select_expr_results :
| LPAR RESULT value_type_list RPAR select_expr_results
Expand Down
2 changes: 1 addition & 1 deletion interpreter/valid/valid.ml
Original file line number Diff line number Diff line change
Expand Up @@ -486,7 +486,7 @@ let rec check_instr (c : context) (e : instr) (s : infer_stack_type) : op_type =
| _ -> assert false
)

| Guard (bt, es) ->
| Barrier (bt, es) ->
let FuncType (ts1, ts2) as ft = check_block_type c bt e.at in
check_block {c with labels = ts2 :: c.labels} es ft e.at;
ts1 --> ts2
Expand Down
51 changes: 48 additions & 3 deletions test/core/cont.wast
Original file line number Diff line number Diff line change
Expand Up @@ -55,19 +55,60 @@

(elem declare func $f3)
(func $f3
(guard (call $f4))
(barrier (call $f4))
)
(func $f4
(suspend $e1)
)

(func (export "guarded")
(func (export "barrier")
(block $h (result (ref $k1))
(resume (event $e1 $h) (cont.new (type $k1) (ref.func $f3)))
(unreachable)
)
(resume_throw $exn)
)

(elem declare func $r0 $r1)
(func $r0)
(func $r1 (suspend $e1))

(func $nl0 (param $k (ref $k1))
(resume (local.get $k))
(resume (local.get $k))
)
(func $nl1 (param $k (ref $k1))
(block $h (result (ref $k1))
(resume (event $e1 $h) (local.get $k))
(unreachable)
)
(resume (local.get $k))
(unreachable)
)
(func $nl2 (param $k (ref $k1))
(block $h1 (result (ref $k1))
(resume (event $e1 $h1) (local.get $k))
(unreachable)
)
(let (local $k' (ref $k1))
(block $h2 (result (ref $k1))
(resume (event $e1 $h2) (local.get $k'))
(unreachable)
)
(resume (local.get $k'))
(unreachable)
)
)

(func (export "non-linear-1")
(call $nl0 (cont.new (type $k1) (ref.func $r0)))
)
(func (export "non-linear-2")
(call $nl1 (cont.new (type $k1) (ref.func $r1)))
)
(func (export "non-linear-3")
(call $nl1 (cont.new (type $k1) (ref.func $r1)))
)
)

(assert_suspension (invoke "unhandled-1") "unhandled")
Expand All @@ -78,7 +119,11 @@
(assert_exception (invoke "uncaught-1") "unhandled")
(assert_exception (invoke "uncaught-2") "unhandled")

(assert_trap (invoke "guarded") "guard suspended")
(assert_trap (invoke "barrier") "barrier")

(assert_trap (invoke "non-linear-1") "continuation resumed twice")
(assert_trap (invoke "non-linear-2") "continuation resumed twice")
(assert_trap (invoke "non-linear-3") "continuation resumed twice")


;; Simple state example
Expand Down

0 comments on commit 707dec0

Please sign in to comment.