From 59843653ab9c79185088ce418d3c5f301413a89e Mon Sep 17 00:00:00 2001 From: conrad Date: Wed, 19 Oct 2022 03:48:16 +0100 Subject: [PATCH 1/6] implement wait and notify --- interpreter/exec/eval.ml | 658 ++++++++++++++++-------------- interpreter/runtime/memory.ml | 3 + interpreter/runtime/memory.mli | 2 + test/core/atomic.wast | 63 --- test/core/atomic_wait_notify.wast | 108 +++++ 5 files changed, 471 insertions(+), 363 deletions(-) create mode 100644 test/core/atomic_wait_notify.wast diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml index 55277d48..7bf8dde7 100644 --- a/interpreter/exec/eval.ml +++ b/interpreter/exec/eval.ml @@ -34,6 +34,8 @@ let numeric_error at = function string_of_int i ^ ", got " ^ Types.string_of_value_type (type_of v)) | exn -> raise exn +(* Must be positive and non-zero *) +let timeout_epsilon = 1000000L (* Administrative Expressions & Configurations *) @@ -57,11 +59,19 @@ and admin_instr' = | Label of int32 * instr list * code | Frame of int32 * frame * code +type suspend_signal = + No_signal + (* memory, cell index, target timestamp *) + | Wait_signal of memory_inst * Memory.address * float + (* memory, cell index, number of threads to wake *) + | Notify_signal of memory_inst * Memory.address * int32 + type thread = { frame : frame; code : code; budget : int; (* to model stack overflow *) + suspend_signal : suspend_signal } type config = thread list @@ -69,7 +79,7 @@ type thread_id = int type status = Running | Result of value list | Trap of exn let frame inst locals = {inst; locals} -let thread inst vs es = {frame = frame inst []; code = vs, es; budget = 300} +let thread inst vs es = {frame = frame inst []; code = vs, es; budget = 300; suspend_signal = No_signal} let empty_thread = thread empty_module_inst [] [] let empty_config = [] let spawn (c : config) = List.length c, c @ [empty_thread] @@ -150,305 +160,348 @@ let check_shared mem at = *) let rec step_thread (t : thread) : thread = - let {frame; code = vs, es; _} = t in - let e = List.hd es in - let vs', es' = - match e.it, vs with - | Plain e', vs -> - (match e', vs with - | Unreachable, vs -> - vs, [Trapping "unreachable executed" @@ e.at] - - | Nop, vs -> - vs, [] - - | Block (bt, es'), vs -> - let FuncType (ts1, ts2) = block_type frame.inst bt in - let n1 = Lib.List32.length ts1 in - let n2 = Lib.List32.length ts2 in - let args, vs' = take n1 vs e.at, drop n1 vs e.at in - vs', [Label (n2, [], (args, List.map plain es')) @@ e.at] - - | Loop (bt, es'), vs -> - let FuncType (ts1, ts2) = block_type frame.inst bt in - let n1 = Lib.List32.length ts1 in - let args, vs' = take n1 vs e.at, drop n1 vs e.at in - vs', [Label (n1, [e' @@ e.at], (args, List.map plain es')) @@ e.at] - - | If (bt, es1, es2), I32 0l :: vs' -> - vs', [Plain (Block (bt, es2)) @@ e.at] - - | If (bt, es1, es2), I32 i :: vs' -> - vs', [Plain (Block (bt, es1)) @@ e.at] - - | Br x, vs -> - [], [Breaking (x.it, vs) @@ e.at] - - | BrIf x, I32 0l :: vs' -> - vs', [] - - | BrIf x, I32 i :: vs' -> - vs', [Plain (Br x) @@ e.at] - - | BrTable (xs, x), I32 i :: vs' when I32.ge_u i (Lib.List32.length xs) -> - vs', [Plain (Br x) @@ e.at] - - | BrTable (xs, x), I32 i :: vs' -> - vs', [Plain (Br (Lib.List32.nth xs i)) @@ e.at] - - | Return, vs -> - [], [Returning vs @@ e.at] - - | Call x, vs -> - vs, [Invoke (func frame.inst x) @@ e.at] - - | CallIndirect x, I32 i :: vs -> - let func = func_elem frame.inst (0l @@ e.at) i e.at in - if type_ frame.inst x <> Func.type_of func then - vs, [Trapping "indirect call type mismatch" @@ e.at] - else - vs, [Invoke func @@ e.at] - - | Drop, v :: vs' -> - vs', [] - - | Select, I32 0l :: v2 :: v1 :: vs' -> - v2 :: vs', [] - - | Select, I32 i :: v2 :: v1 :: vs' -> - v1 :: vs', [] - - | LocalGet x, vs -> - !(local frame x) :: vs, [] - - | LocalSet x, v :: vs' -> - local frame x := v; - vs', [] - - | LocalTee x, v :: vs' -> - local frame x := v; - v :: vs', [] - - | GlobalGet x, vs -> - Global.load (global frame.inst x) :: vs, [] - - | GlobalSet x, v :: vs' -> - (try Global.store (global frame.inst x) v; vs', [] - with Global.NotMutable -> Crash.error e.at "write to immutable global" - | Global.Type -> Crash.error e.at "type mismatch at global write") - - | Load {offset; ty; sz; _}, I32 i :: vs' -> - let mem = memory frame.inst (0l @@ e.at) in - let addr = I64_convert.extend_i32_u i in - (try - let v = - match sz with - | None -> Memory.load_value mem addr offset ty - | Some (sz, ext) -> Memory.load_packed sz ext mem addr offset ty - in v :: vs', [] - with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at]) - - | Store {offset; sz; _}, v :: I32 i :: vs' -> - let mem = memory frame.inst (0l @@ e.at) in - let addr = I64_convert.extend_i32_u i in - (try - (match sz with - | None -> Memory.store_value mem addr offset v - | Some sz -> Memory.store_packed sz mem addr offset v - ); - vs', [] - with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at]); - - | AtomicLoad {offset; ty; sz; _}, I32 i :: vs' -> - let mem = memory frame.inst (0l @@ e.at) in - let addr = I64_convert.extend_i32_u i in - (try - check_align addr ty sz e.at; - let v = - match sz with - | None -> Memory.load_value mem addr offset ty - | Some sz -> Memory.load_packed sz ZX mem addr offset ty - in v :: vs', [] - with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at]) - - | AtomicStore {offset; ty; sz; _}, v :: I32 i :: vs' -> - let mem = memory frame.inst (0l @@ e.at) in - let addr = I64_convert.extend_i32_u i in - (try - check_align addr ty sz e.at; - (match sz with - | None -> Memory.store_value mem addr offset v - | Some sz -> Memory.store_packed sz mem addr offset v - ); - vs', [] - with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at]); - - | AtomicRmw (rmwop, {offset; ty; sz; _}), v :: I32 i :: vs' -> - let mem = memory frame.inst (0l @@ e.at) in - let addr = I64_convert.extend_i32_u i in - (try - check_align addr ty sz e.at; - let v1 = - match sz with - | None -> Memory.load_value mem addr offset ty - | Some sz -> Memory.load_packed sz ZX mem addr offset ty - in let v2 = Eval_numeric.eval_rmwop rmwop v1 v - in (match sz with - | None -> Memory.store_value mem addr offset v2 - | Some sz -> Memory.store_packed sz mem addr offset v2 - ); - v1 :: vs', [] - with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at]) - - | AtomicRmwCmpXchg {offset; ty; sz; _}, vn :: ve :: I32 i :: vs' -> - let mem = memory frame.inst (0l @@ e.at) in - let addr = I64_convert.extend_i32_u i in - (try - check_align addr ty sz e.at; - let v1 = - match sz with - | None -> Memory.load_value mem addr offset ty - | Some sz -> Memory.load_packed sz ZX mem addr offset ty - in (if v1 = ve then - match sz with - | None -> Memory.store_value mem addr offset vn - | Some sz -> Memory.store_packed sz mem addr offset vn - ); - v1 :: vs', [] - with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at]); - - | MemoryAtomicWait {offset; ty; sz; _}, I64 timeout :: ve :: I32 i :: vs' -> - let mem = memory frame.inst (0l @@ e.at) in - let addr = I64_convert.extend_i32_u i in - (try - assert (sz = None); - check_align addr ty sz e.at; - check_shared mem e.at; - let v = Memory.load_value mem addr offset ty in - if v = ve then - assert false (* TODO *) - else - I32 1l :: vs', [] (* Not equal *) - with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at]) - - | MemoryAtomicNotify {offset; ty; sz; _}, I32 count :: I32 i :: vs' -> - let mem = memory frame.inst (0l @@ e.at) in - let addr = I64_convert.extend_i32_u i in - (try - check_align addr ty sz e.at; - let _ = Memory.load_value mem addr offset ty in - if count = 0l then - I32 0l :: vs', [] (* Trivial case waking 0 waiters *) + let {frame; code = vs, es; budget; suspend_signal} = t in + match suspend_signal with + (* TODO: meaningful timestamp handling *) + | Wait_signal _ -> t + (* notify signal should have been handled and cleared already *) + | Notify_signal _ -> assert false + | No_signal -> + let e = List.hd es in + let vs', es', susp_signal = + match e.it, vs with + | Plain e', vs -> + (match e', vs with + | Unreachable, vs -> + vs, [Trapping "unreachable executed" @@ e.at], No_signal + + | Nop, vs -> + vs, [], No_signal + + | Block (bt, es'), vs -> + let FuncType (ts1, ts2) = block_type frame.inst bt in + let n1 = Lib.List32.length ts1 in + let n2 = Lib.List32.length ts2 in + let args, vs' = take n1 vs e.at, drop n1 vs e.at in + vs', [Label (n2, [], (args, List.map plain es')) @@ e.at], No_signal + + | Loop (bt, es'), vs -> + let FuncType (ts1, ts2) = block_type frame.inst bt in + let n1 = Lib.List32.length ts1 in + let args, vs' = take n1 vs e.at, drop n1 vs e.at in + vs', [Label (n1, [e' @@ e.at], (args, List.map plain es')) @@ e.at], No_signal + + | If (bt, es1, es2), I32 0l :: vs' -> + vs', [Plain (Block (bt, es2)) @@ e.at], No_signal + + | If (bt, es1, es2), I32 i :: vs' -> + vs', [Plain (Block (bt, es1)) @@ e.at], No_signal + + | Br x, vs -> + [], [Breaking (x.it, vs) @@ e.at], No_signal + + | BrIf x, I32 0l :: vs' -> + vs', [], No_signal + + | BrIf x, I32 i :: vs' -> + vs', [Plain (Br x) @@ e.at], No_signal + + | BrTable (xs, x), I32 i :: vs' when I32.ge_u i (Lib.List32.length xs) -> + vs', [Plain (Br x) @@ e.at], No_signal + + | BrTable (xs, x), I32 i :: vs' -> + vs', [Plain (Br (Lib.List32.nth xs i)) @@ e.at], No_signal + + | Return, vs -> + [], [Returning vs @@ e.at], No_signal + + | Call x, vs -> + vs, [Invoke (func frame.inst x) @@ e.at], No_signal + + | CallIndirect x, I32 i :: vs -> + let func = func_elem frame.inst (0l @@ e.at) i e.at in + if type_ frame.inst x <> Func.type_of func then + vs, [Trapping "indirect call type mismatch" @@ e.at], No_signal else - assert false (* TODO *) - with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at]) - - | AtomicFence, vs -> - vs, [] - - | MemorySize, vs -> - let mem = memory frame.inst (0l @@ e.at) in - I32 (Memory.size mem) :: vs, [] - - | MemoryGrow, I32 delta :: vs' -> - let mem = memory frame.inst (0l @@ e.at) in - let old_size = Memory.size mem in - let result = - try Memory.grow mem delta; old_size - with Memory.SizeOverflow | Memory.SizeLimit | Memory.OutOfMemory -> -1l - in I32 result :: vs', [] - - | Const v, vs -> - v.it :: vs, [] - - | Test testop, v :: vs' -> - (try value_of_bool (Eval_numeric.eval_testop testop v) :: vs', [] - with exn -> vs', [Trapping (numeric_error e.at exn) @@ e.at]) - - | Compare relop, v2 :: v1 :: vs' -> - (try value_of_bool (Eval_numeric.eval_relop relop v1 v2) :: vs', [] - with exn -> vs', [Trapping (numeric_error e.at exn) @@ e.at]) - - | Unary unop, v :: vs' -> - (try Eval_numeric.eval_unop unop v :: vs', [] - with exn -> vs', [Trapping (numeric_error e.at exn) @@ e.at]) - - | Binary binop, v2 :: v1 :: vs' -> - (try Eval_numeric.eval_binop binop v1 v2 :: vs', [] - with exn -> vs', [Trapping (numeric_error e.at exn) @@ e.at]) - - | Convert cvtop, v :: vs' -> - (try Eval_numeric.eval_cvtop cvtop v :: vs', [] - with exn -> vs', [Trapping (numeric_error e.at exn) @@ e.at]) - - | _ -> - let s1 = string_of_values (List.rev vs) in - let s2 = string_of_value_types (List.map type_of (List.rev vs)) in - Crash.error e.at - ("missing or ill-typed operand on stack (" ^ s1 ^ " : " ^ s2 ^ ")") - ) - - | Trapping msg, vs -> - [], [Trapping msg @@ e.at] - - | Returning vs', vs -> - Crash.error e.at "undefined frame" - - | Breaking (k, vs'), vs -> - Crash.error e.at "undefined label" - - | Label (n, es0, (vs', [])), vs -> - vs' @ vs, [] - - | Label (n, es0, (vs', {it = Trapping msg; at} :: es')), vs -> - vs, [Trapping msg @@ at] - - | Label (n, es0, (vs', {it = Returning vs0; at} :: es')), vs -> - vs, [Returning vs0 @@ at] - - | Label (n, es0, (vs', {it = Breaking (0l, vs0); at} :: es')), vs -> - take n vs0 e.at @ vs, List.map plain es0 - - | Label (n, es0, (vs', {it = Breaking (k, vs0); at} :: es')), vs -> - vs, [Breaking (Int32.sub k 1l, vs0) @@ at] - - | Label (n, es0, code'), vs -> - let t' = step_thread {t with code = code'} in - vs, [Label (n, es0, t'.code) @@ e.at] - - | Frame (n, frame', (vs', [])), vs -> - vs' @ vs, [] - - | Frame (n, frame', (vs', {it = Trapping msg; at} :: es')), vs -> - vs, [Trapping msg @@ at] - - | Frame (n, frame', (vs', {it = Returning vs0; at} :: es')), vs -> - take n vs0 e.at @ vs, [] - - | Frame (n, frame', code'), vs -> - let t' = step_thread {frame = frame'; code = code'; budget = t.budget - 1} in - vs, [Frame (n, t'.frame, t'.code) @@ e.at] - - | Invoke func, vs when t.budget = 0 -> - Exhaustion.error e.at "call stack exhausted" - - | Invoke func, vs -> - let FuncType (ins, out) = func_type_of func in - let n1, n2 = Lib.List32.length ins, Lib.List32.length out in - let args, vs' = take n1 vs e.at, drop n1 vs e.at in - (match func with - | Func.AstFunc (t, inst', f) -> - let locals' = List.rev args @ List.map default_value f.it.locals in - let frame' = {inst = !inst'; locals = List.map ref locals'} in - let instr' = [Label (n2, [], ([], List.map plain f.it.body)) @@ f.at] in - vs', [Frame (n2, frame', ([], instr')) @@ e.at] - - | Func.HostFunc (t, f) -> - try List.rev (f (List.rev args)) @ vs', [] - with Crash (_, msg) -> Crash.error e.at msg - ) - in {t with code = vs', es' @ List.tl es} - + vs, [Invoke func @@ e.at], No_signal + + | Drop, v :: vs' -> + vs', [], No_signal + + | Select, I32 0l :: v2 :: v1 :: vs' -> + v2 :: vs', [], No_signal + + | Select, I32 i :: v2 :: v1 :: vs' -> + v1 :: vs', [], No_signal + + | LocalGet x, vs -> + !(local frame x) :: vs, [], No_signal + + | LocalSet x, v :: vs' -> + local frame x := v; + vs', [], No_signal + + | LocalTee x, v :: vs' -> + local frame x := v; + v :: vs', [], No_signal + + | GlobalGet x, vs -> + Global.load (global frame.inst x) :: vs, [], No_signal + + | GlobalSet x, v :: vs' -> + (try Global.store (global frame.inst x) v; vs', [], No_signal + with Global.NotMutable -> Crash.error e.at "write to immutable global" + | Global.Type -> Crash.error e.at "type mismatch at global write") + + | Load {offset; ty; sz; _}, I32 i :: vs' -> + let mem = memory frame.inst (0l @@ e.at) in + let addr = I64_convert.extend_i32_u i in + (try + let v = + match sz with + | None -> Memory.load_value mem addr offset ty + | Some (sz, ext) -> Memory.load_packed sz ext mem addr offset ty + in v :: vs', [], No_signal + with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], No_signal) + + | Store {offset; sz; _}, v :: I32 i :: vs' -> + let mem = memory frame.inst (0l @@ e.at) in + let addr = I64_convert.extend_i32_u i in + (try + (match sz with + | None -> Memory.store_value mem addr offset v + | Some sz -> Memory.store_packed sz mem addr offset v + ); + vs', [], No_signal + with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], No_signal); + + | AtomicLoad {offset; ty; sz; _}, I32 i :: vs' -> + let mem = memory frame.inst (0l @@ e.at) in + let addr = I64_convert.extend_i32_u i in + (try + check_align addr ty sz e.at; + let v = + match sz with + | None -> Memory.load_value mem addr offset ty + | Some sz -> Memory.load_packed sz ZX mem addr offset ty + in v :: vs', [], No_signal + with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], No_signal) + + | AtomicStore {offset; ty; sz; _}, v :: I32 i :: vs' -> + let mem = memory frame.inst (0l @@ e.at) in + let addr = I64_convert.extend_i32_u i in + (try + check_align addr ty sz e.at; + (match sz with + | None -> Memory.store_value mem addr offset v + | Some sz -> Memory.store_packed sz mem addr offset v + ); + vs', [], No_signal + with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], No_signal); + + | AtomicRmw (rmwop, {offset; ty; sz; _}), v :: I32 i :: vs' -> + let mem = memory frame.inst (0l @@ e.at) in + let addr = I64_convert.extend_i32_u i in + (try + check_align addr ty sz e.at; + let v1 = + match sz with + | None -> Memory.load_value mem addr offset ty + | Some sz -> Memory.load_packed sz ZX mem addr offset ty + in let v2 = Eval_numeric.eval_rmwop rmwop v1 v + in (match sz with + | None -> Memory.store_value mem addr offset v2 + | Some sz -> Memory.store_packed sz mem addr offset v2 + ); + v1 :: vs', [], No_signal + with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], No_signal) + + | AtomicRmwCmpXchg {offset; ty; sz; _}, vn :: ve :: I32 i :: vs' -> + let mem = memory frame.inst (0l @@ e.at) in + let addr = I64_convert.extend_i32_u i in + (try + check_align addr ty sz e.at; + let v1 = + match sz with + | None -> Memory.load_value mem addr offset ty + | Some sz -> Memory.load_packed sz ZX mem addr offset ty + in (if v1 = ve then + match sz with + | None -> Memory.store_value mem addr offset vn + | Some sz -> Memory.store_packed sz mem addr offset vn + ); + v1 :: vs', [], No_signal + with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], No_signal); + + | MemoryAtomicWait {offset; ty; sz; _}, I64 timeout :: ve :: I32 i :: vs' -> + let mem = memory frame.inst (0l @@ e.at) in + let addr = I64_convert.extend_i32_u i in + (try + assert (sz = None); + check_align addr ty sz e.at; + check_shared mem e.at; + let v = Memory.load_value mem addr offset ty in + if v = ve then + if timeout >= 0L && timeout < timeout_epsilon then + I32 2l :: vs', [], No_signal (* Treat as though wait timed out immediately *) + else + (* TODO: meaningful timestamp handling *) + vs', [], (Wait_signal (mem, addr, 0.)) + else + I32 1l :: vs', [], No_signal (* Not equal *) + with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], No_signal) + + | MemoryAtomicNotify {offset; ty; sz; _}, I32 count :: I32 i :: vs' -> + let mem = memory frame.inst (0l @@ e.at) in + let addr = I64_convert.extend_i32_u i in + (try + check_align addr ty sz e.at; + let _ = Memory.load_value mem addr offset ty in + if count = 0l then + I32 0l :: vs', [], No_signal (* Trivial case waking 0 waiters *) + else + vs', [], (Notify_signal (mem, addr, count)) + with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], No_signal) + + | AtomicFence, vs -> + vs, [], No_signal + + | MemorySize, vs -> + let mem = memory frame.inst (0l @@ e.at) in + I32 (Memory.size mem) :: vs, [], No_signal + + | MemoryGrow, I32 delta :: vs' -> + let mem = memory frame.inst (0l @@ e.at) in + let old_size = Memory.size mem in + let result = + try Memory.grow mem delta; old_size + with Memory.SizeOverflow | Memory.SizeLimit | Memory.OutOfMemory -> -1l + in I32 result :: vs', [], No_signal + + | Const v, vs -> + v.it :: vs, [], No_signal + + | Test testop, v :: vs' -> + (try value_of_bool (Eval_numeric.eval_testop testop v) :: vs', [], No_signal + with exn -> vs', [Trapping (numeric_error e.at exn) @@ e.at], No_signal) + + | Compare relop, v2 :: v1 :: vs' -> + (try value_of_bool (Eval_numeric.eval_relop relop v1 v2) :: vs', [], No_signal + with exn -> vs', [Trapping (numeric_error e.at exn) @@ e.at], No_signal) + + | Unary unop, v :: vs' -> + (try Eval_numeric.eval_unop unop v :: vs', [], No_signal + with exn -> vs', [Trapping (numeric_error e.at exn) @@ e.at], No_signal) + + | Binary binop, v2 :: v1 :: vs' -> + (try Eval_numeric.eval_binop binop v1 v2 :: vs', [], No_signal + with exn -> vs', [Trapping (numeric_error e.at exn) @@ e.at], No_signal) + + | Convert cvtop, v :: vs' -> + (try Eval_numeric.eval_cvtop cvtop v :: vs', [], No_signal + with exn -> vs', [Trapping (numeric_error e.at exn) @@ e.at], No_signal) + + | _ -> + let s1 = string_of_values (List.rev vs) in + let s2 = string_of_value_types (List.map type_of (List.rev vs)) in + Crash.error e.at + ("missing or ill-typed operand on stack (" ^ s1 ^ " : " ^ s2 ^ ")") + ) + + | Trapping msg, vs -> + [], [Trapping msg @@ e.at], No_signal + + | Returning vs', vs -> + Crash.error e.at "undefined frame" + + | Breaking (k, vs'), vs -> + Crash.error e.at "undefined label" + + | Label (n, es0, (vs', [])), vs -> + vs' @ vs, [], No_signal + + | Label (n, es0, (vs', {it = Trapping msg; at} :: es')), vs -> + vs, [Trapping msg @@ at], No_signal + + | Label (n, es0, (vs', {it = Returning vs0; at} :: es')), vs -> + vs, [Returning vs0 @@ at], No_signal + + | Label (n, es0, (vs', {it = Breaking (0l, vs0); at} :: es')), vs -> + take n vs0 e.at @ vs, List.map plain es0, No_signal + + | Label (n, es0, (vs', {it = Breaking (k, vs0); at} :: es')), vs -> + vs, [Breaking (Int32.sub k 1l, vs0) @@ at], No_signal + + | Label (n, es0, code'), vs -> + let t' = step_thread {t with code = code'} in + vs, [Label (n, es0, t'.code) @@ e.at], t'.suspend_signal + + | Frame (n, frame', (vs', [])), vs -> + vs' @ vs, [], No_signal + + | Frame (n, frame', (vs', {it = Trapping msg; at} :: es')), vs -> + vs, [Trapping msg @@ at], No_signal + + | Frame (n, frame', (vs', {it = Returning vs0; at} :: es')), vs -> + take n vs0 e.at @ vs, [], No_signal + + | Frame (n, frame', code'), vs -> + let t' = step_thread {frame = frame'; code = code'; budget = t.budget - 1; suspend_signal = t.suspend_signal} in + vs, [Frame (n, t'.frame, t'.code) @@ e.at], t'.suspend_signal + + | Invoke func, vs when t.budget = 0 -> + Exhaustion.error e.at "call stack exhausted" + + | Invoke func, vs -> + let FuncType (ins, out) = func_type_of func in + let n1, n2 = Lib.List32.length ins, Lib.List32.length out in + let args, vs' = take n1 vs e.at, drop n1 vs e.at in + (match func with + | Func.AstFunc (t, inst', f) -> + let locals' = List.rev args @ List.map default_value f.it.locals in + let frame' = {inst = !inst'; locals = List.map ref locals'} in + let instr' = [Label (n2, [], ([], List.map plain f.it.body)) @@ f.at] in + vs', [Frame (n2, frame', ([], instr')) @@ e.at], No_signal + + | Func.HostFunc (t, f) -> + try List.rev (f (List.rev args)) @ vs', [], No_signal + with Crash (_, msg) -> Crash.error e.at msg + ) + in {t with code = vs', es' @ List.tl es; suspend_signal = susp_signal} + +let rec push_to_inner_stack (c : code) (v : value) : code = + let vs, es = c in + match es with + | {it = Label (n, es0, c'); at} :: es' -> + vs, {it = Label (n, es0, push_to_inner_stack c' v); at} :: es' + | {it = Frame (n, f, c'); at} :: es' -> + vs, {it = Frame (n, f, push_to_inner_stack c' v); at} :: es' + | _ -> + v :: vs, es + +let wake_one (t : thread) (m : memory_inst) (addr : Memory.address) : (thread * int32) = + match t.suspend_signal with + | No_signal -> + t, 0l + | Notify_signal _ -> + assert false (* no other threads should be signalling notify *) + | Wait_signal (m', addr', timeout) -> + if Memory.is_same_memory m m' && addr = addr' then + {t with code = push_to_inner_stack t.code (I32 0l); suspend_signal = No_signal}, 1l + else + t, 0l + +let rec wake (c : config) (m : memory_inst) (addr : Memory.address) (count : int32) : (config * int32) = + if count = 0l then + c, 0l + else + match c with + | [] -> + c, 0l + | t :: ts -> + let t', count' = wake_one t m addr in + let ts', count'' = wake ts m addr (Int32.sub count count') in + (t' :: ts', Int32.add count' count'') let rec step (c : config) (n : thread_id) : config = let ts1, t, ts2 = Lib.List.extract n c in @@ -457,7 +510,12 @@ let rec step (c : config) (n : thread_id) : config = else let t' = try step_thread t with Stack_overflow -> Exhaustion.error (List.hd (snd t.code)).at "call stack exhausted" - in ts1 @ [t'] @ ts2 + in match t'.suspend_signal with + | Notify_signal (m, addr, count) -> + let ts1', count1 = wake ts1 m addr count in + let ts2', count2 = wake ts2 m addr (Int32.sub count count1) in + ts1' @ [{t' with code = push_to_inner_stack t'.code (I32 (Int32.add count1 count2)); suspend_signal = No_signal}] @ ts2' + | _ -> ts1 @ [t'] @ ts2 let rec eval (c : config ref) (n : thread_id) : value list = match status !c n with diff --git a/interpreter/runtime/memory.ml b/interpreter/runtime/memory.ml index 764f295f..4c7088e0 100644 --- a/interpreter/runtime/memory.ml +++ b/interpreter/runtime/memory.ml @@ -20,6 +20,9 @@ exception OutOfMemory let page_size = 0x10000L (* 64 KiB *) +let is_same_memory m1 m2 = + m1.content == m2.content + let is_aligned a t sz = let align = match sz with diff --git a/interpreter/runtime/memory.mli b/interpreter/runtime/memory.mli index e765e91c..63cf0454 100644 --- a/interpreter/runtime/memory.mli +++ b/interpreter/runtime/memory.mli @@ -16,6 +16,8 @@ exception OutOfMemory val page_size : int64 +val is_same_memory : memory -> memory -> bool + val is_aligned : address -> value_type -> pack_size option -> bool val alloc : memory_type -> memory (* raises SizeOverflow, OutOfMemory *) diff --git a/test/core/atomic.wast b/test/core/atomic.wast index 66ad0ebb..54c02f6c 100644 --- a/test/core/atomic.wast +++ b/test/core/atomic.wast @@ -437,69 +437,6 @@ (assert_trap (invoke "i64.atomic.rmw16.cmpxchg_u" (i32.const 1) (i64.const 0) (i64.const 0)) "unaligned atomic") (assert_trap (invoke "i64.atomic.rmw32.cmpxchg_u" (i32.const 1) (i64.const 0) (i64.const 0)) "unaligned atomic") -;; wait/notify -(module - (memory 1 1 shared) - - (func (export "init") (param $value i64) (i64.store (i32.const 0) (local.get $value))) - - (func (export "memory.atomic.notify") (param $addr i32) (param $count i32) (result i32) - (memory.atomic.notify (local.get 0) (local.get 1))) - (func (export "memory.atomic.wait32") (param $addr i32) (param $expected i32) (param $timeout i64) (result i32) - (memory.atomic.wait32 (local.get 0) (local.get 1) (local.get 2))) - (func (export "memory.atomic.wait64") (param $addr i32) (param $expected i64) (param $timeout i64) (result i32) - (memory.atomic.wait64 (local.get 0) (local.get 1) (local.get 2))) -) - -(invoke "init" (i64.const 0xffffffffffff)) - -;; wait returns immediately if values do not match -(assert_return (invoke "memory.atomic.wait32" (i32.const 0) (i32.const 0) (i64.const 0)) (i32.const 1)) -(assert_return (invoke "memory.atomic.wait64" (i32.const 0) (i64.const 0) (i64.const 0)) (i32.const 1)) - -;; notify always returns -(assert_return (invoke "memory.atomic.notify" (i32.const 0) (i32.const 0)) (i32.const 0)) - -;; OOB wait and notify always trap -(assert_trap (invoke "memory.atomic.wait32" (i32.const 65536) (i32.const 0) (i64.const 0)) "out of bounds memory access") -(assert_trap (invoke "memory.atomic.wait64" (i32.const 65536) (i64.const 0) (i64.const 0)) "out of bounds memory access") - -;; in particular, notify always traps even if waking 0 threads -(assert_trap (invoke "memory.atomic.notify" (i32.const 65536) (i32.const 0)) "out of bounds memory access") - -;; similarly, unaligned wait and notify always trap -(assert_trap (invoke "memory.atomic.wait32" (i32.const 65531) (i32.const 0) (i64.const 0)) "unaligned atomic") -(assert_trap (invoke "memory.atomic.wait64" (i32.const 65524) (i64.const 0) (i64.const 0)) "unaligned atomic") - -(assert_trap (invoke "memory.atomic.notify" (i32.const 65531) (i32.const 0)) "unaligned atomic") - -;; atomic.wait traps on unshared memory even if it wouldn't block -(module - (memory 1 1) - - (func (export "init") (param $value i64) (i64.store (i32.const 0) (local.get $value))) - - (func (export "memory.atomic.notify") (param $addr i32) (param $count i32) (result i32) - (memory.atomic.notify (local.get 0) (local.get 1))) - (func (export "memory.atomic.wait32") (param $addr i32) (param $expected i32) (param $timeout i64) (result i32) - (memory.atomic.wait32 (local.get 0) (local.get 1) (local.get 2))) - (func (export "memory.atomic.wait64") (param $addr i32) (param $expected i64) (param $timeout i64) (result i32) - (memory.atomic.wait64 (local.get 0) (local.get 1) (local.get 2))) -) - -(invoke "init" (i64.const 0xffffffffffff)) - -(assert_trap (invoke "memory.atomic.wait32" (i32.const 0) (i32.const 0) (i64.const 0)) "expected shared memory") -(assert_trap (invoke "memory.atomic.wait64" (i32.const 0) (i64.const 0) (i64.const 0)) "expected shared memory") - -;; notify still works -(assert_return (invoke "memory.atomic.notify" (i32.const 0) (i32.const 0)) (i32.const 0)) - -;; OOB and unaligned notify still trap -(assert_trap (invoke "memory.atomic.notify" (i32.const 65536) (i32.const 0)) "out of bounds memory access") -(assert_trap (invoke "memory.atomic.notify" (i32.const 65531) (i32.const 0)) "unaligned atomic") - - ;; unshared memory is OK (module (memory 1 1) diff --git a/test/core/atomic_wait_notify.wast b/test/core/atomic_wait_notify.wast new file mode 100644 index 00000000..2e312c37 --- /dev/null +++ b/test/core/atomic_wait_notify.wast @@ -0,0 +1,108 @@ +;; wait/notify +(module + (memory 1 1 shared) + + (func (export "init") (param $value i64) (i64.store (i32.const 0) (local.get $value))) + + (func (export "memory.atomic.notify") (param $addr i32) (param $count i32) (result i32) + (memory.atomic.notify (local.get 0) (local.get 1))) + (func (export "memory.atomic.wait32") (param $addr i32) (param $expected i32) (param $timeout i64) (result i32) + (memory.atomic.wait32 (local.get 0) (local.get 1) (local.get 2))) + (func (export "memory.atomic.wait64") (param $addr i32) (param $expected i64) (param $timeout i64) (result i32) + (memory.atomic.wait64 (local.get 0) (local.get 1) (local.get 2))) +) + +(invoke "init" (i64.const 0xffffffffffff)) + +;; wait returns immediately if values do not match +(assert_return (invoke "memory.atomic.wait32" (i32.const 0) (i32.const 0) (i64.const 0)) (i32.const 1)) +(assert_return (invoke "memory.atomic.wait64" (i32.const 0) (i64.const 0) (i64.const 0)) (i32.const 1)) + +;; wait times out if values do match and timeout is small +(assert_return (invoke "memory.atomic.wait32" (i32.const 0) (i32.const 0xffffffff) (i64.const 10)) (i32.const 2)) +(assert_return (invoke "memory.atomic.wait64" (i32.const 0) (i64.const 0xffffffffffff) (i64.const 10)) (i32.const 2)) + +;; notify always returns +(assert_return (invoke "memory.atomic.notify" (i32.const 0) (i32.const 0)) (i32.const 0)) +(assert_return (invoke "memory.atomic.notify" (i32.const 0) (i32.const 10)) (i32.const 0)) + +;; OOB wait and notify always trap +(assert_trap (invoke "memory.atomic.wait32" (i32.const 65536) (i32.const 0) (i64.const 0)) "out of bounds memory access") +(assert_trap (invoke "memory.atomic.wait64" (i32.const 65536) (i64.const 0) (i64.const 0)) "out of bounds memory access") + +;; in particular, notify always traps even if waking 0 threads +(assert_trap (invoke "memory.atomic.notify" (i32.const 65536) (i32.const 0)) "out of bounds memory access") + +;; similarly, unaligned wait and notify always trap +(assert_trap (invoke "memory.atomic.wait32" (i32.const 65531) (i32.const 0) (i64.const 0)) "unaligned atomic") +(assert_trap (invoke "memory.atomic.wait64" (i32.const 65524) (i64.const 0) (i64.const 0)) "unaligned atomic") + +(assert_trap (invoke "memory.atomic.notify" (i32.const 65531) (i32.const 0)) "unaligned atomic") + +;; atomic.wait traps on unshared memory even if it wouldn't block +(module + (memory 1 1) + + (func (export "init") (param $value i64) (i64.store (i32.const 0) (local.get $value))) + + (func (export "memory.atomic.notify") (param $addr i32) (param $count i32) (result i32) + (memory.atomic.notify (local.get 0) (local.get 1))) + (func (export "memory.atomic.wait32") (param $addr i32) (param $expected i32) (param $timeout i64) (result i32) + (memory.atomic.wait32 (local.get 0) (local.get 1) (local.get 2))) + (func (export "memory.atomic.wait64") (param $addr i32) (param $expected i64) (param $timeout i64) (result i32) + (memory.atomic.wait64 (local.get 0) (local.get 1) (local.get 2))) +) + +(invoke "init" (i64.const 0xffffffffffff)) + +(assert_trap (invoke "memory.atomic.wait32" (i32.const 0) (i32.const 0) (i64.const 0)) "expected shared memory") +(assert_trap (invoke "memory.atomic.wait64" (i32.const 0) (i64.const 0) (i64.const 0)) "expected shared memory") + +;; notify still works +(assert_return (invoke "memory.atomic.notify" (i32.const 0) (i32.const 0)) (i32.const 0)) + +;; OOB and unaligned notify still trap +(assert_trap (invoke "memory.atomic.notify" (i32.const 65536) (i32.const 0)) "out of bounds memory access") +(assert_trap (invoke "memory.atomic.notify" (i32.const 65531) (i32.const 0)) "unaligned atomic") + +;; test that looping notify eventually unblocks a parallel waiting thread +(module $Mem + (memory (export "shared") 1 1 shared) +) + +(thread $T1 (shared (module $Mem)) + (register "mem" $Mem) + (module + (memory (import "mem" "shared") 1 10 shared) + (func (export "run") (result i32) + (memory.atomic.wait32 (i32.const 0) (i32.const 0) (i64.const -1)) + ) + ) + ;; test that this thread eventually gets unblocked + (assert_return (invoke "run") (i32.const 0)) +) + +(thread $T2 (shared (module $Mem)) + (register "mem" $Mem) + (module + (memory (import "mem" "shared") 1 1 shared) + (func (export "notify-0") (result i32) + (memory.atomic.notify (i32.const 0) (i32.const 0)) + ) + (func (export "notify-1-while") + (loop + (i32.const 1) + (memory.atomic.notify (i32.const 0) (i32.const 1)) + (i32.ne) + (br_if 0) + ) + ) + ) + ;; notifying with a count of 0 will not unblock + (assert_return (invoke "notify-0") (i32.const 0)) + ;; loop until something is notified + (assert_return (invoke "notify-1-while")) +) + +(wait $T1) +(wait $T2) From 8eebb97479189104a97294b04edb97eda5ecc332 Mon Sep 17 00:00:00 2001 From: conrad Date: Tue, 25 Oct 2022 01:53:55 +0100 Subject: [PATCH 2/6] comments --- interpreter/exec/eval.ml | 661 ++++++++++++++++++++------------------- 1 file changed, 333 insertions(+), 328 deletions(-) diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml index 7bf8dde7..b1f7c131 100644 --- a/interpreter/exec/eval.ml +++ b/interpreter/exec/eval.ml @@ -58,20 +58,20 @@ and admin_instr' = | Breaking of int32 * value stack | Label of int32 * instr list * code | Frame of int32 * frame * code + | Suspend of memory_inst * Memory.address * float -type suspend_signal = - No_signal +type action = + No_action (* memory, cell index, target timestamp *) - | Wait_signal of memory_inst * Memory.address * float + | Wait_action of memory_inst * Memory.address * float (* memory, cell index, number of threads to wake *) - | Notify_signal of memory_inst * Memory.address * int32 + | Notify_action of memory_inst * Memory.address * int32 type thread = { frame : frame; code : code; budget : int; (* to model stack overflow *) - suspend_signal : suspend_signal } type config = thread list @@ -79,7 +79,7 @@ type thread_id = int type status = Running | Result of value list | Trap of exn let frame inst locals = {inst; locals} -let thread inst vs es = {frame = frame inst []; code = vs, es; budget = 300; suspend_signal = No_signal} +let thread inst vs es = {frame = frame inst []; code = vs, es; budget = 300} let empty_thread = thread empty_module_inst [] [] let empty_config = [] let spawn (c : config) = List.length c, c @ [empty_thread] @@ -159,315 +159,314 @@ let check_shared mem at = * c : config *) -let rec step_thread (t : thread) : thread = - let {frame; code = vs, es; budget; suspend_signal} = t in - match suspend_signal with - (* TODO: meaningful timestamp handling *) - | Wait_signal _ -> t - (* notify signal should have been handled and cleared already *) - | Notify_signal _ -> assert false - | No_signal -> - let e = List.hd es in - let vs', es', susp_signal = - match e.it, vs with - | Plain e', vs -> - (match e', vs with - | Unreachable, vs -> - vs, [Trapping "unreachable executed" @@ e.at], No_signal - - | Nop, vs -> - vs, [], No_signal - - | Block (bt, es'), vs -> - let FuncType (ts1, ts2) = block_type frame.inst bt in - let n1 = Lib.List32.length ts1 in - let n2 = Lib.List32.length ts2 in - let args, vs' = take n1 vs e.at, drop n1 vs e.at in - vs', [Label (n2, [], (args, List.map plain es')) @@ e.at], No_signal - - | Loop (bt, es'), vs -> - let FuncType (ts1, ts2) = block_type frame.inst bt in - let n1 = Lib.List32.length ts1 in - let args, vs' = take n1 vs e.at, drop n1 vs e.at in - vs', [Label (n1, [e' @@ e.at], (args, List.map plain es')) @@ e.at], No_signal - - | If (bt, es1, es2), I32 0l :: vs' -> - vs', [Plain (Block (bt, es2)) @@ e.at], No_signal - - | If (bt, es1, es2), I32 i :: vs' -> - vs', [Plain (Block (bt, es1)) @@ e.at], No_signal - - | Br x, vs -> - [], [Breaking (x.it, vs) @@ e.at], No_signal - - | BrIf x, I32 0l :: vs' -> - vs', [], No_signal - - | BrIf x, I32 i :: vs' -> - vs', [Plain (Br x) @@ e.at], No_signal - - | BrTable (xs, x), I32 i :: vs' when I32.ge_u i (Lib.List32.length xs) -> - vs', [Plain (Br x) @@ e.at], No_signal - - | BrTable (xs, x), I32 i :: vs' -> - vs', [Plain (Br (Lib.List32.nth xs i)) @@ e.at], No_signal - - | Return, vs -> - [], [Returning vs @@ e.at], No_signal - - | Call x, vs -> - vs, [Invoke (func frame.inst x) @@ e.at], No_signal - - | CallIndirect x, I32 i :: vs -> - let func = func_elem frame.inst (0l @@ e.at) i e.at in - if type_ frame.inst x <> Func.type_of func then - vs, [Trapping "indirect call type mismatch" @@ e.at], No_signal - else - vs, [Invoke func @@ e.at], No_signal - - | Drop, v :: vs' -> - vs', [], No_signal - - | Select, I32 0l :: v2 :: v1 :: vs' -> - v2 :: vs', [], No_signal - - | Select, I32 i :: v2 :: v1 :: vs' -> - v1 :: vs', [], No_signal - - | LocalGet x, vs -> - !(local frame x) :: vs, [], No_signal - - | LocalSet x, v :: vs' -> - local frame x := v; - vs', [], No_signal - - | LocalTee x, v :: vs' -> - local frame x := v; - v :: vs', [], No_signal - - | GlobalGet x, vs -> - Global.load (global frame.inst x) :: vs, [], No_signal - - | GlobalSet x, v :: vs' -> - (try Global.store (global frame.inst x) v; vs', [], No_signal - with Global.NotMutable -> Crash.error e.at "write to immutable global" - | Global.Type -> Crash.error e.at "type mismatch at global write") - - | Load {offset; ty; sz; _}, I32 i :: vs' -> - let mem = memory frame.inst (0l @@ e.at) in - let addr = I64_convert.extend_i32_u i in - (try - let v = - match sz with - | None -> Memory.load_value mem addr offset ty - | Some (sz, ext) -> Memory.load_packed sz ext mem addr offset ty - in v :: vs', [], No_signal - with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], No_signal) - - | Store {offset; sz; _}, v :: I32 i :: vs' -> - let mem = memory frame.inst (0l @@ e.at) in - let addr = I64_convert.extend_i32_u i in - (try - (match sz with - | None -> Memory.store_value mem addr offset v - | Some sz -> Memory.store_packed sz mem addr offset v - ); - vs', [], No_signal - with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], No_signal); - - | AtomicLoad {offset; ty; sz; _}, I32 i :: vs' -> - let mem = memory frame.inst (0l @@ e.at) in - let addr = I64_convert.extend_i32_u i in - (try - check_align addr ty sz e.at; - let v = - match sz with - | None -> Memory.load_value mem addr offset ty - | Some sz -> Memory.load_packed sz ZX mem addr offset ty - in v :: vs', [], No_signal - with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], No_signal) - - | AtomicStore {offset; ty; sz; _}, v :: I32 i :: vs' -> - let mem = memory frame.inst (0l @@ e.at) in - let addr = I64_convert.extend_i32_u i in - (try - check_align addr ty sz e.at; - (match sz with - | None -> Memory.store_value mem addr offset v - | Some sz -> Memory.store_packed sz mem addr offset v - ); - vs', [], No_signal - with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], No_signal); - - | AtomicRmw (rmwop, {offset; ty; sz; _}), v :: I32 i :: vs' -> - let mem = memory frame.inst (0l @@ e.at) in - let addr = I64_convert.extend_i32_u i in - (try - check_align addr ty sz e.at; - let v1 = - match sz with - | None -> Memory.load_value mem addr offset ty - | Some sz -> Memory.load_packed sz ZX mem addr offset ty - in let v2 = Eval_numeric.eval_rmwop rmwop v1 v - in (match sz with - | None -> Memory.store_value mem addr offset v2 - | Some sz -> Memory.store_packed sz mem addr offset v2 - ); - v1 :: vs', [], No_signal - with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], No_signal) - - | AtomicRmwCmpXchg {offset; ty; sz; _}, vn :: ve :: I32 i :: vs' -> - let mem = memory frame.inst (0l @@ e.at) in - let addr = I64_convert.extend_i32_u i in - (try - check_align addr ty sz e.at; - let v1 = - match sz with - | None -> Memory.load_value mem addr offset ty - | Some sz -> Memory.load_packed sz ZX mem addr offset ty - in (if v1 = ve then - match sz with - | None -> Memory.store_value mem addr offset vn - | Some sz -> Memory.store_packed sz mem addr offset vn - ); - v1 :: vs', [], No_signal - with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], No_signal); - - | MemoryAtomicWait {offset; ty; sz; _}, I64 timeout :: ve :: I32 i :: vs' -> - let mem = memory frame.inst (0l @@ e.at) in - let addr = I64_convert.extend_i32_u i in - (try - assert (sz = None); - check_align addr ty sz e.at; - check_shared mem e.at; - let v = Memory.load_value mem addr offset ty in - if v = ve then - if timeout >= 0L && timeout < timeout_epsilon then - I32 2l :: vs', [], No_signal (* Treat as though wait timed out immediately *) - else - (* TODO: meaningful timestamp handling *) - vs', [], (Wait_signal (mem, addr, 0.)) - else - I32 1l :: vs', [], No_signal (* Not equal *) - with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], No_signal) - - | MemoryAtomicNotify {offset; ty; sz; _}, I32 count :: I32 i :: vs' -> - let mem = memory frame.inst (0l @@ e.at) in - let addr = I64_convert.extend_i32_u i in - (try - check_align addr ty sz e.at; - let _ = Memory.load_value mem addr offset ty in - if count = 0l then - I32 0l :: vs', [], No_signal (* Trivial case waking 0 waiters *) - else - vs', [], (Notify_signal (mem, addr, count)) - with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], No_signal) - - | AtomicFence, vs -> - vs, [], No_signal - - | MemorySize, vs -> - let mem = memory frame.inst (0l @@ e.at) in - I32 (Memory.size mem) :: vs, [], No_signal - - | MemoryGrow, I32 delta :: vs' -> - let mem = memory frame.inst (0l @@ e.at) in - let old_size = Memory.size mem in - let result = - try Memory.grow mem delta; old_size - with Memory.SizeOverflow | Memory.SizeLimit | Memory.OutOfMemory -> -1l - in I32 result :: vs', [], No_signal - - | Const v, vs -> - v.it :: vs, [], No_signal - - | Test testop, v :: vs' -> - (try value_of_bool (Eval_numeric.eval_testop testop v) :: vs', [], No_signal - with exn -> vs', [Trapping (numeric_error e.at exn) @@ e.at], No_signal) - - | Compare relop, v2 :: v1 :: vs' -> - (try value_of_bool (Eval_numeric.eval_relop relop v1 v2) :: vs', [], No_signal - with exn -> vs', [Trapping (numeric_error e.at exn) @@ e.at], No_signal) - - | Unary unop, v :: vs' -> - (try Eval_numeric.eval_unop unop v :: vs', [], No_signal - with exn -> vs', [Trapping (numeric_error e.at exn) @@ e.at], No_signal) - - | Binary binop, v2 :: v1 :: vs' -> - (try Eval_numeric.eval_binop binop v1 v2 :: vs', [], No_signal - with exn -> vs', [Trapping (numeric_error e.at exn) @@ e.at], No_signal) - - | Convert cvtop, v :: vs' -> - (try Eval_numeric.eval_cvtop cvtop v :: vs', [], No_signal - with exn -> vs', [Trapping (numeric_error e.at exn) @@ e.at], No_signal) - - | _ -> - let s1 = string_of_values (List.rev vs) in - let s2 = string_of_value_types (List.map type_of (List.rev vs)) in - Crash.error e.at - ("missing or ill-typed operand on stack (" ^ s1 ^ " : " ^ s2 ^ ")") - ) - - | Trapping msg, vs -> - [], [Trapping msg @@ e.at], No_signal - - | Returning vs', vs -> - Crash.error e.at "undefined frame" - - | Breaking (k, vs'), vs -> - Crash.error e.at "undefined label" - - | Label (n, es0, (vs', [])), vs -> - vs' @ vs, [], No_signal - - | Label (n, es0, (vs', {it = Trapping msg; at} :: es')), vs -> - vs, [Trapping msg @@ at], No_signal - - | Label (n, es0, (vs', {it = Returning vs0; at} :: es')), vs -> - vs, [Returning vs0 @@ at], No_signal - - | Label (n, es0, (vs', {it = Breaking (0l, vs0); at} :: es')), vs -> - take n vs0 e.at @ vs, List.map plain es0, No_signal - - | Label (n, es0, (vs', {it = Breaking (k, vs0); at} :: es')), vs -> - vs, [Breaking (Int32.sub k 1l, vs0) @@ at], No_signal - - | Label (n, es0, code'), vs -> - let t' = step_thread {t with code = code'} in - vs, [Label (n, es0, t'.code) @@ e.at], t'.suspend_signal - - | Frame (n, frame', (vs', [])), vs -> - vs' @ vs, [], No_signal - - | Frame (n, frame', (vs', {it = Trapping msg; at} :: es')), vs -> - vs, [Trapping msg @@ at], No_signal - - | Frame (n, frame', (vs', {it = Returning vs0; at} :: es')), vs -> - take n vs0 e.at @ vs, [], No_signal - - | Frame (n, frame', code'), vs -> - let t' = step_thread {frame = frame'; code = code'; budget = t.budget - 1; suspend_signal = t.suspend_signal} in - vs, [Frame (n, t'.frame, t'.code) @@ e.at], t'.suspend_signal - - | Invoke func, vs when t.budget = 0 -> - Exhaustion.error e.at "call stack exhausted" - - | Invoke func, vs -> - let FuncType (ins, out) = func_type_of func in - let n1, n2 = Lib.List32.length ins, Lib.List32.length out in +let rec step_thread (t : thread) : (thread * action) = + let {frame; code = vs, es; budget} = t in + let e = List.hd es in + let vs', es', action = + match e.it, vs with + | Plain e', vs -> + (match e', vs with + | Unreachable, vs -> + vs, [Trapping "unreachable executed" @@ e.at], No_action + + | Nop, vs -> + vs, [], No_action + + | Block (bt, es'), vs -> + let FuncType (ts1, ts2) = block_type frame.inst bt in + let n1 = Lib.List32.length ts1 in + let n2 = Lib.List32.length ts2 in let args, vs' = take n1 vs e.at, drop n1 vs e.at in - (match func with - | Func.AstFunc (t, inst', f) -> - let locals' = List.rev args @ List.map default_value f.it.locals in - let frame' = {inst = !inst'; locals = List.map ref locals'} in - let instr' = [Label (n2, [], ([], List.map plain f.it.body)) @@ f.at] in - vs', [Frame (n2, frame', ([], instr')) @@ e.at], No_signal - - | Func.HostFunc (t, f) -> - try List.rev (f (List.rev args)) @ vs', [], No_signal - with Crash (_, msg) -> Crash.error e.at msg - ) - in {t with code = vs', es' @ List.tl es; suspend_signal = susp_signal} + vs', [Label (n2, [], (args, List.map plain es')) @@ e.at], No_action + + | Loop (bt, es'), vs -> + let FuncType (ts1, ts2) = block_type frame.inst bt in + let n1 = Lib.List32.length ts1 in + let args, vs' = take n1 vs e.at, drop n1 vs e.at in + vs', [Label (n1, [e' @@ e.at], (args, List.map plain es')) @@ e.at], No_action + + | If (bt, es1, es2), I32 0l :: vs' -> + vs', [Plain (Block (bt, es2)) @@ e.at], No_action + + | If (bt, es1, es2), I32 i :: vs' -> + vs', [Plain (Block (bt, es1)) @@ e.at], No_action + + | Br x, vs -> + [], [Breaking (x.it, vs) @@ e.at], No_action + + | BrIf x, I32 0l :: vs' -> + vs', [], No_action + + | BrIf x, I32 i :: vs' -> + vs', [Plain (Br x) @@ e.at], No_action + + | BrTable (xs, x), I32 i :: vs' when I32.ge_u i (Lib.List32.length xs) -> + vs', [Plain (Br x) @@ e.at], No_action + + | BrTable (xs, x), I32 i :: vs' -> + vs', [Plain (Br (Lib.List32.nth xs i)) @@ e.at], No_action + + | Return, vs -> + [], [Returning vs @@ e.at], No_action + + | Call x, vs -> + vs, [Invoke (func frame.inst x) @@ e.at], No_action + + | CallIndirect x, I32 i :: vs -> + let func = func_elem frame.inst (0l @@ e.at) i e.at in + if type_ frame.inst x <> Func.type_of func then + vs, [Trapping "indirect call type mismatch" @@ e.at], No_action + else + vs, [Invoke func @@ e.at], No_action + + | Drop, v :: vs' -> + vs', [], No_action + + | Select, I32 0l :: v2 :: v1 :: vs' -> + v2 :: vs', [], No_action + + | Select, I32 i :: v2 :: v1 :: vs' -> + v1 :: vs', [], No_action + + | LocalGet x, vs -> + !(local frame x) :: vs, [], No_action + + | LocalSet x, v :: vs' -> + local frame x := v; + vs', [], No_action + + | LocalTee x, v :: vs' -> + local frame x := v; + v :: vs', [], No_action + + | GlobalGet x, vs -> + Global.load (global frame.inst x) :: vs, [], No_action + + | GlobalSet x, v :: vs' -> + (try Global.store (global frame.inst x) v; vs', [], No_action + with Global.NotMutable -> Crash.error e.at "write to immutable global" + | Global.Type -> Crash.error e.at "type mismatch at global write") + + | Load {offset; ty; sz; _}, I32 i :: vs' -> + let mem = memory frame.inst (0l @@ e.at) in + let addr = I64_convert.extend_i32_u i in + (try + let v = + match sz with + | None -> Memory.load_value mem addr offset ty + | Some (sz, ext) -> Memory.load_packed sz ext mem addr offset ty + in v :: vs', [], No_action + with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], No_action) + + | Store {offset; sz; _}, v :: I32 i :: vs' -> + let mem = memory frame.inst (0l @@ e.at) in + let addr = I64_convert.extend_i32_u i in + (try + (match sz with + | None -> Memory.store_value mem addr offset v + | Some sz -> Memory.store_packed sz mem addr offset v + ); + vs', [], No_action + with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], No_action); + + | AtomicLoad {offset; ty; sz; _}, I32 i :: vs' -> + let mem = memory frame.inst (0l @@ e.at) in + let addr = I64_convert.extend_i32_u i in + (try + check_align addr ty sz e.at; + let v = + match sz with + | None -> Memory.load_value mem addr offset ty + | Some sz -> Memory.load_packed sz ZX mem addr offset ty + in v :: vs', [], No_action + with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], No_action) + + | AtomicStore {offset; ty; sz; _}, v :: I32 i :: vs' -> + let mem = memory frame.inst (0l @@ e.at) in + let addr = I64_convert.extend_i32_u i in + (try + check_align addr ty sz e.at; + (match sz with + | None -> Memory.store_value mem addr offset v + | Some sz -> Memory.store_packed sz mem addr offset v + ); + vs', [], No_action + with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], No_action); + + | AtomicRmw (rmwop, {offset; ty; sz; _}), v :: I32 i :: vs' -> + let mem = memory frame.inst (0l @@ e.at) in + let addr = I64_convert.extend_i32_u i in + (try + check_align addr ty sz e.at; + let v1 = + match sz with + | None -> Memory.load_value mem addr offset ty + | Some sz -> Memory.load_packed sz ZX mem addr offset ty + in let v2 = Eval_numeric.eval_rmwop rmwop v1 v + in (match sz with + | None -> Memory.store_value mem addr offset v2 + | Some sz -> Memory.store_packed sz mem addr offset v2 + ); + v1 :: vs', [], No_action + with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], No_action) + + | AtomicRmwCmpXchg {offset; ty; sz; _}, vn :: ve :: I32 i :: vs' -> + let mem = memory frame.inst (0l @@ e.at) in + let addr = I64_convert.extend_i32_u i in + (try + check_align addr ty sz e.at; + let v1 = + match sz with + | None -> Memory.load_value mem addr offset ty + | Some sz -> Memory.load_packed sz ZX mem addr offset ty + in (if v1 = ve then + match sz with + | None -> Memory.store_value mem addr offset vn + | Some sz -> Memory.store_packed sz mem addr offset vn + ); + v1 :: vs', [], No_action + with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], No_action); + + | MemoryAtomicWait {offset; ty; sz; _}, I64 timeout :: ve :: I32 i :: vs' -> + let mem = memory frame.inst (0l @@ e.at) in + let addr = I64_convert.extend_i32_u i in + (try + assert (sz = None); + check_align addr ty sz e.at; + check_shared mem e.at; + let v = Memory.load_value mem addr offset ty in + if v = ve then + if timeout >= 0L && timeout < timeout_epsilon then + I32 2l :: vs', [], No_action (* Treat as though wait timed out immediately *) + else + (* TODO: meaningful timestamp handling *) + vs', [Suspend (mem, addr, 0.) @@ e.at], (Wait_action (mem, addr, 0.)) + else + I32 1l :: vs', [], No_action (* Not equal *) + with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], No_action) + + | MemoryAtomicNotify {offset; ty; sz; _}, I32 count :: I32 i :: vs' -> + let mem = memory frame.inst (0l @@ e.at) in + let addr = I64_convert.extend_i32_u i in + (try + check_align addr ty sz e.at; + let _ = Memory.load_value mem addr offset ty in + if count = 0l then + I32 0l :: vs', [], No_action (* Trivial case waking 0 waiters *) + else + vs', [], (Notify_action (mem, addr, count)) + with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], No_action) + + | AtomicFence, vs -> + vs, [], No_action + + | MemorySize, vs -> + let mem = memory frame.inst (0l @@ e.at) in + I32 (Memory.size mem) :: vs, [], No_action + + | MemoryGrow, I32 delta :: vs' -> + let mem = memory frame.inst (0l @@ e.at) in + let old_size = Memory.size mem in + let result = + try Memory.grow mem delta; old_size + with Memory.SizeOverflow | Memory.SizeLimit | Memory.OutOfMemory -> -1l + in I32 result :: vs', [], No_action + + | Const v, vs -> + v.it :: vs, [], No_action + + | Test testop, v :: vs' -> + (try value_of_bool (Eval_numeric.eval_testop testop v) :: vs', [], No_action + with exn -> vs', [Trapping (numeric_error e.at exn) @@ e.at], No_action) + + | Compare relop, v2 :: v1 :: vs' -> + (try value_of_bool (Eval_numeric.eval_relop relop v1 v2) :: vs', [], No_action + with exn -> vs', [Trapping (numeric_error e.at exn) @@ e.at], No_action) + + | Unary unop, v :: vs' -> + (try Eval_numeric.eval_unop unop v :: vs', [], No_action + with exn -> vs', [Trapping (numeric_error e.at exn) @@ e.at], No_action) + + | Binary binop, v2 :: v1 :: vs' -> + (try Eval_numeric.eval_binop binop v1 v2 :: vs', [], No_action + with exn -> vs', [Trapping (numeric_error e.at exn) @@ e.at], No_action) + + | Convert cvtop, v :: vs' -> + (try Eval_numeric.eval_cvtop cvtop v :: vs', [], No_action + with exn -> vs', [Trapping (numeric_error e.at exn) @@ e.at], No_action) + + | _ -> + let s1 = string_of_values (List.rev vs) in + let s2 = string_of_value_types (List.map type_of (List.rev vs)) in + Crash.error e.at + ("missing or ill-typed operand on stack (" ^ s1 ^ " : " ^ s2 ^ ")") + ) + + | Trapping msg, vs -> + [], [Trapping msg @@ e.at], No_action + + | Returning vs', vs -> + Crash.error e.at "undefined frame" + + | Breaking (k, vs'), vs -> + Crash.error e.at "undefined label" + + | Label (n, es0, (vs', [])), vs -> + vs' @ vs, [], No_action + + | Label (n, es0, (vs', {it = Trapping msg; at} :: es')), vs -> + vs, [Trapping msg @@ at], No_action + + | Label (n, es0, (vs', {it = Returning vs0; at} :: es')), vs -> + vs, [Returning vs0 @@ at], No_action + + | Label (n, es0, (vs', {it = Breaking (0l, vs0); at} :: es')), vs -> + take n vs0 e.at @ vs, List.map plain es0, No_action + + | Label (n, es0, (vs', {it = Breaking (k, vs0); at} :: es')), vs -> + vs, [Breaking (Int32.sub k 1l, vs0) @@ at], No_action + + | Label (n, es0, code'), vs -> + let t', act = step_thread {t with code = code'} in + vs, [Label (n, es0, t'.code) @@ e.at], act + + | Frame (n, frame', (vs', [])), vs -> + vs' @ vs, [], No_action + + | Frame (n, frame', (vs', {it = Trapping msg; at} :: es')), vs -> + vs, [Trapping msg @@ at], No_action + + | Frame (n, frame', (vs', {it = Returning vs0; at} :: es')), vs -> + take n vs0 e.at @ vs, [], No_action + + | Frame (n, frame', code'), vs -> + let t', act = step_thread {frame = frame'; code = code'; budget = t.budget - 1} in + vs, [Frame (n, t'.frame, t'.code) @@ e.at], act + + | Invoke func, vs when t.budget = 0 -> + Exhaustion.error e.at "call stack exhausted" + + | Invoke func, vs -> + let FuncType (ins, out) = func_type_of func in + let n1, n2 = Lib.List32.length ins, Lib.List32.length out in + let args, vs' = take n1 vs e.at, drop n1 vs e.at in + (match func with + | Func.AstFunc (t, inst', f) -> + let locals' = List.rev args @ List.map default_value f.it.locals in + let frame' = {inst = !inst'; locals = List.map ref locals'} in + let instr' = [Label (n2, [], ([], List.map plain f.it.body)) @@ f.at] in + vs', [Frame (n2, frame', ([], instr')) @@ e.at], No_action + + | Func.HostFunc (t, f) -> + try List.rev (f (List.rev args)) @ vs', [], No_action + with Crash (_, msg) -> Crash.error e.at msg + ) + + | Suspend _, vs -> + (* TODO: meaningful timestamp handling *) + vs, [e], No_action + + in {t with code = vs', es' @ List.tl es}, action let rec push_to_inner_stack (c : code) (v : value) : code = let vs, es = c in @@ -479,17 +478,23 @@ let rec push_to_inner_stack (c : code) (v : value) : code = | _ -> v :: vs, es -let wake_one (t : thread) (m : memory_inst) (addr : Memory.address) : (thread * int32) = - match t.suspend_signal with - | No_signal -> - t, 0l - | Notify_signal _ -> - assert false (* no other threads should be signalling notify *) - | Wait_signal (m', addr', timeout) -> +let rec try_unsuspend (c : code) (m : memory_inst) (addr : Memory.address) : code option = + let vs, es = c in + match es with + | {it = Label (n, es0, c'); at} :: es' -> + Lib.Option.map (fun c'' -> vs, {it = Label (n, es0, c''); at} :: es') (try_unsuspend c' m addr) + | {it = Frame (n, f, c'); at} :: es' -> + Lib.Option.map (fun c'' -> vs, {it = Frame (n, f, c''); at} :: es') (try_unsuspend c' m addr) + | {it = Suspend (m', addr', timeout); at} :: es' -> if Memory.is_same_memory m m' && addr = addr' then - {t with code = push_to_inner_stack t.code (I32 0l); suspend_signal = No_signal}, 1l + Some (((I32 0l) :: vs), es') else - t, 0l + None + | _ -> + None + +let try_wake_one (t : thread) (m : memory_inst) (addr : Memory.address) : thread option = + Lib.Option.map (fun c' -> {t with code = c'}) (try_unsuspend t.code m addr) let rec wake (c : config) (m : memory_inst) (addr : Memory.address) (count : int32) : (config * int32) = if count = 0l then @@ -499,7 +504,7 @@ let rec wake (c : config) (m : memory_inst) (addr : Memory.address) (count : int | [] -> c, 0l | t :: ts -> - let t', count' = wake_one t m addr in + let t', count' = (match (try_wake_one t m addr) with | None -> t, 0l | Some t'' -> t'', 1l) in let ts', count'' = wake ts m addr (Int32.sub count count') in (t' :: ts', Int32.add count' count'') @@ -508,13 +513,13 @@ let rec step (c : config) (n : thread_id) : config = if snd t.code = [] then step c n else - let t' = try step_thread t with Stack_overflow -> + let t', act = try step_thread t with Stack_overflow -> Exhaustion.error (List.hd (snd t.code)).at "call stack exhausted" - in match t'.suspend_signal with - | Notify_signal (m, addr, count) -> + in match act with + | Notify_action (m, addr, count) -> let ts1', count1 = wake ts1 m addr count in let ts2', count2 = wake ts2 m addr (Int32.sub count count1) in - ts1' @ [{t' with code = push_to_inner_stack t'.code (I32 (Int32.add count1 count2)); suspend_signal = No_signal}] @ ts2' + ts1' @ [{t' with code = push_to_inner_stack t'.code (I32 (Int32.add count1 count2))}] @ ts2' | _ -> ts1 @ [t'] @ ts2 let rec eval (c : config ref) (n : thread_id) : value list = From 1d3e39bd77349c276b5c87170b79eb48ef122468 Mon Sep 17 00:00:00 2001 From: Conrad Watt Date: Tue, 25 Apr 2023 07:04:25 +0100 Subject: [PATCH 3/6] Apply suggestions from code review Co-authored-by: Andreas Rossberg --- interpreter/exec/eval.ml | 38 ++++++++++++++++++---------------- interpreter/runtime/memory.ml | 2 +- interpreter/runtime/memory.mli | 2 +- 3 files changed, 22 insertions(+), 20 deletions(-) diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml index b1f7c131..234b9d89 100644 --- a/interpreter/exec/eval.ml +++ b/interpreter/exec/eval.ml @@ -37,6 +37,7 @@ let numeric_error at = function (* Must be positive and non-zero *) let timeout_epsilon = 1000000L + (* Administrative Expressions & Configurations *) type 'a stack = 'a list @@ -61,11 +62,11 @@ and admin_instr' = | Suspend of memory_inst * Memory.address * float type action = - No_action + | NoAction (* memory, cell index, target timestamp *) - | Wait_action of memory_inst * Memory.address * float + | WaitAction of memory_inst * Memory.address * float (* memory, cell index, number of threads to wake *) - | Notify_action of memory_inst * Memory.address * int32 + | NotifyAction of memory_inst * Memory.address * int32 type thread = { @@ -159,10 +160,10 @@ let check_shared mem at = * c : config *) -let rec step_thread (t : thread) : (thread * action) = - let {frame; code = vs, es; budget} = t in +let rec step_thread (t : thread) : thread * action = + let {frame; code = vs, es; _} = t in let e = List.hd es in - let vs', es', action = + let vs', es', act = match e.it, vs with | Plain e', vs -> (match e', vs with @@ -354,7 +355,7 @@ let rec step_thread (t : thread) : (thread * action) = if count = 0l then I32 0l :: vs', [], No_action (* Trivial case waking 0 waiters *) else - vs', [], (Notify_action (mem, addr, count)) + vs', [], Notify_action (mem, addr, count) with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], No_action) | AtomicFence, vs -> @@ -466,7 +467,7 @@ let rec step_thread (t : thread) : (thread * action) = (* TODO: meaningful timestamp handling *) vs, [e], No_action - in {t with code = vs', es' @ List.tl es}, action + in {t with code = vs', es' @ List.tl es}, act let rec push_to_inner_stack (c : code) (v : value) : code = let vs, es = c in @@ -487,7 +488,7 @@ let rec try_unsuspend (c : code) (m : memory_inst) (addr : Memory.address) : cod Lib.Option.map (fun c'' -> vs, {it = Frame (n, f, c''); at} :: es') (try_unsuspend c' m addr) | {it = Suspend (m', addr', timeout); at} :: es' -> if Memory.is_same_memory m m' && addr = addr' then - Some (((I32 0l) :: vs), es') + Some (I32 0l :: vs, es') else None | _ -> @@ -496,7 +497,7 @@ let rec try_unsuspend (c : code) (m : memory_inst) (addr : Memory.address) : cod let try_wake_one (t : thread) (m : memory_inst) (addr : Memory.address) : thread option = Lib.Option.map (fun c' -> {t with code = c'}) (try_unsuspend t.code m addr) -let rec wake (c : config) (m : memory_inst) (addr : Memory.address) (count : int32) : (config * int32) = +let rec wake (c : config) (m : memory_inst) (addr : Memory.address) (count : int32) : config * int32 = if count = 0l then c, 0l else @@ -504,9 +505,9 @@ let rec wake (c : config) (m : memory_inst) (addr : Memory.address) (count : int | [] -> c, 0l | t :: ts -> - let t', count' = (match (try_wake_one t m addr) with | None -> t, 0l | Some t'' -> t'', 1l) in + let t', count' = match try_wake_one t m addr with | None -> t, 0l | Some t' -> t', 1l in let ts', count'' = wake ts m addr (Int32.sub count count') in - (t' :: ts', Int32.add count' count'') + t' :: ts', Int32.add count' count'' let rec step (c : config) (n : thread_id) : config = let ts1, t, ts2 = Lib.List.extract n c in @@ -515,12 +516,13 @@ let rec step (c : config) (n : thread_id) : config = else let t', act = try step_thread t with Stack_overflow -> Exhaustion.error (List.hd (snd t.code)).at "call stack exhausted" - in match act with - | Notify_action (m, addr, count) -> - let ts1', count1 = wake ts1 m addr count in - let ts2', count2 = wake ts2 m addr (Int32.sub count count1) in - ts1' @ [{t' with code = push_to_inner_stack t'.code (I32 (Int32.add count1 count2))}] @ ts2' - | _ -> ts1 @ [t'] @ ts2 + in + match act with + | Notify_action (m, addr, count) -> + let ts1', count1 = wake ts1 m addr count in + let ts2', count2 = wake ts2 m addr (Int32.sub count count1) in + ts1' @ [{t' with code = push_to_inner_stack t'.code (I32 (Int32.add count1 count2))}] @ ts2' + | _ -> ts1 @ [t'] @ ts2 let rec eval (c : config ref) (n : thread_id) : value list = match status !c n with diff --git a/interpreter/runtime/memory.ml b/interpreter/runtime/memory.ml index 4c7088e0..ea3b3648 100644 --- a/interpreter/runtime/memory.ml +++ b/interpreter/runtime/memory.ml @@ -20,7 +20,7 @@ exception OutOfMemory let page_size = 0x10000L (* 64 KiB *) -let is_same_memory m1 m2 = +let same m1 m2 = m1.content == m2.content let is_aligned a t sz = diff --git a/interpreter/runtime/memory.mli b/interpreter/runtime/memory.mli index 63cf0454..e95e0a08 100644 --- a/interpreter/runtime/memory.mli +++ b/interpreter/runtime/memory.mli @@ -16,7 +16,7 @@ exception OutOfMemory val page_size : int64 -val is_same_memory : memory -> memory -> bool +val same : memory -> memory -> bool val is_aligned : address -> value_type -> pack_size option -> bool From fb73407a3045dc5a1578b8fa653a88b92c8b6d34 Mon Sep 17 00:00:00 2001 From: conrad Date: Tue, 25 Apr 2023 07:13:10 +0100 Subject: [PATCH 4/6] comments --- interpreter/exec/eval.ml | 153 +++++++++++++++++++-------------------- 1 file changed, 75 insertions(+), 78 deletions(-) diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml index 234b9d89..9d55ede9 100644 --- a/interpreter/exec/eval.ml +++ b/interpreter/exec/eval.ml @@ -168,83 +168,83 @@ let rec step_thread (t : thread) : thread * action = | Plain e', vs -> (match e', vs with | Unreachable, vs -> - vs, [Trapping "unreachable executed" @@ e.at], No_action + vs, [Trapping "unreachable executed" @@ e.at], NoAction | Nop, vs -> - vs, [], No_action + vs, [], NoAction | Block (bt, es'), vs -> let FuncType (ts1, ts2) = block_type frame.inst bt in let n1 = Lib.List32.length ts1 in let n2 = Lib.List32.length ts2 in let args, vs' = take n1 vs e.at, drop n1 vs e.at in - vs', [Label (n2, [], (args, List.map plain es')) @@ e.at], No_action + vs', [Label (n2, [], (args, List.map plain es')) @@ e.at], NoAction | Loop (bt, es'), vs -> let FuncType (ts1, ts2) = block_type frame.inst bt in let n1 = Lib.List32.length ts1 in let args, vs' = take n1 vs e.at, drop n1 vs e.at in - vs', [Label (n1, [e' @@ e.at], (args, List.map plain es')) @@ e.at], No_action + vs', [Label (n1, [e' @@ e.at], (args, List.map plain es')) @@ e.at], NoAction | If (bt, es1, es2), I32 0l :: vs' -> - vs', [Plain (Block (bt, es2)) @@ e.at], No_action + vs', [Plain (Block (bt, es2)) @@ e.at], NoAction | If (bt, es1, es2), I32 i :: vs' -> - vs', [Plain (Block (bt, es1)) @@ e.at], No_action + vs', [Plain (Block (bt, es1)) @@ e.at], NoAction | Br x, vs -> - [], [Breaking (x.it, vs) @@ e.at], No_action + [], [Breaking (x.it, vs) @@ e.at], NoAction | BrIf x, I32 0l :: vs' -> - vs', [], No_action + vs', [], NoAction | BrIf x, I32 i :: vs' -> - vs', [Plain (Br x) @@ e.at], No_action + vs', [Plain (Br x) @@ e.at], NoAction | BrTable (xs, x), I32 i :: vs' when I32.ge_u i (Lib.List32.length xs) -> - vs', [Plain (Br x) @@ e.at], No_action + vs', [Plain (Br x) @@ e.at], NoAction | BrTable (xs, x), I32 i :: vs' -> - vs', [Plain (Br (Lib.List32.nth xs i)) @@ e.at], No_action + vs', [Plain (Br (Lib.List32.nth xs i)) @@ e.at], NoAction | Return, vs -> - [], [Returning vs @@ e.at], No_action + [], [Returning vs @@ e.at], NoAction | Call x, vs -> - vs, [Invoke (func frame.inst x) @@ e.at], No_action + vs, [Invoke (func frame.inst x) @@ e.at], NoAction | CallIndirect x, I32 i :: vs -> let func = func_elem frame.inst (0l @@ e.at) i e.at in if type_ frame.inst x <> Func.type_of func then - vs, [Trapping "indirect call type mismatch" @@ e.at], No_action + vs, [Trapping "indirect call type mismatch" @@ e.at], NoAction else - vs, [Invoke func @@ e.at], No_action + vs, [Invoke func @@ e.at], NoAction | Drop, v :: vs' -> - vs', [], No_action + vs', [], NoAction | Select, I32 0l :: v2 :: v1 :: vs' -> - v2 :: vs', [], No_action + v2 :: vs', [], NoAction | Select, I32 i :: v2 :: v1 :: vs' -> - v1 :: vs', [], No_action + v1 :: vs', [], NoAction | LocalGet x, vs -> - !(local frame x) :: vs, [], No_action + !(local frame x) :: vs, [], NoAction | LocalSet x, v :: vs' -> local frame x := v; - vs', [], No_action + vs', [], NoAction | LocalTee x, v :: vs' -> local frame x := v; - v :: vs', [], No_action + v :: vs', [], NoAction | GlobalGet x, vs -> - Global.load (global frame.inst x) :: vs, [], No_action + Global.load (global frame.inst x) :: vs, [], NoAction | GlobalSet x, v :: vs' -> - (try Global.store (global frame.inst x) v; vs', [], No_action + (try Global.store (global frame.inst x) v; vs', [], NoAction with Global.NotMutable -> Crash.error e.at "write to immutable global" | Global.Type -> Crash.error e.at "type mismatch at global write") @@ -256,8 +256,8 @@ let rec step_thread (t : thread) : thread * action = match sz with | None -> Memory.load_value mem addr offset ty | Some (sz, ext) -> Memory.load_packed sz ext mem addr offset ty - in v :: vs', [], No_action - with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], No_action) + in v :: vs', [], NoAction + with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], NoAction) | Store {offset; sz; _}, v :: I32 i :: vs' -> let mem = memory frame.inst (0l @@ e.at) in @@ -267,8 +267,8 @@ let rec step_thread (t : thread) : thread * action = | None -> Memory.store_value mem addr offset v | Some sz -> Memory.store_packed sz mem addr offset v ); - vs', [], No_action - with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], No_action); + vs', [], NoAction + with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], NoAction); | AtomicLoad {offset; ty; sz; _}, I32 i :: vs' -> let mem = memory frame.inst (0l @@ e.at) in @@ -279,8 +279,8 @@ let rec step_thread (t : thread) : thread * action = match sz with | None -> Memory.load_value mem addr offset ty | Some sz -> Memory.load_packed sz ZX mem addr offset ty - in v :: vs', [], No_action - with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], No_action) + in v :: vs', [], NoAction + with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], NoAction) | AtomicStore {offset; ty; sz; _}, v :: I32 i :: vs' -> let mem = memory frame.inst (0l @@ e.at) in @@ -291,8 +291,8 @@ let rec step_thread (t : thread) : thread * action = | None -> Memory.store_value mem addr offset v | Some sz -> Memory.store_packed sz mem addr offset v ); - vs', [], No_action - with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], No_action); + vs', [], NoAction + with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], NoAction); | AtomicRmw (rmwop, {offset; ty; sz; _}), v :: I32 i :: vs' -> let mem = memory frame.inst (0l @@ e.at) in @@ -308,8 +308,8 @@ let rec step_thread (t : thread) : thread * action = | None -> Memory.store_value mem addr offset v2 | Some sz -> Memory.store_packed sz mem addr offset v2 ); - v1 :: vs', [], No_action - with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], No_action) + v1 :: vs', [], NoAction + with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], NoAction) | AtomicRmwCmpXchg {offset; ty; sz; _}, vn :: ve :: I32 i :: vs' -> let mem = memory frame.inst (0l @@ e.at) in @@ -325,8 +325,8 @@ let rec step_thread (t : thread) : thread * action = | None -> Memory.store_value mem addr offset vn | Some sz -> Memory.store_packed sz mem addr offset vn ); - v1 :: vs', [], No_action - with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], No_action); + v1 :: vs', [], NoAction + with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], NoAction); | MemoryAtomicWait {offset; ty; sz; _}, I64 timeout :: ve :: I32 i :: vs' -> let mem = memory frame.inst (0l @@ e.at) in @@ -338,13 +338,13 @@ let rec step_thread (t : thread) : thread * action = let v = Memory.load_value mem addr offset ty in if v = ve then if timeout >= 0L && timeout < timeout_epsilon then - I32 2l :: vs', [], No_action (* Treat as though wait timed out immediately *) + I32 2l :: vs', [], NoAction (* Treat as though wait timed out immediately *) else (* TODO: meaningful timestamp handling *) - vs', [Suspend (mem, addr, 0.) @@ e.at], (Wait_action (mem, addr, 0.)) + vs', [Suspend (mem, addr, 0.) @@ e.at], (WaitAction (mem, addr, 0.)) else - I32 1l :: vs', [], No_action (* Not equal *) - with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], No_action) + I32 1l :: vs', [], NoAction (* Not equal *) + with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], NoAction) | MemoryAtomicNotify {offset; ty; sz; _}, I32 count :: I32 i :: vs' -> let mem = memory frame.inst (0l @@ e.at) in @@ -353,17 +353,17 @@ let rec step_thread (t : thread) : thread * action = check_align addr ty sz e.at; let _ = Memory.load_value mem addr offset ty in if count = 0l then - I32 0l :: vs', [], No_action (* Trivial case waking 0 waiters *) + I32 0l :: vs', [], NoAction (* Trivial case waking 0 waiters *) else - vs', [], Notify_action (mem, addr, count) - with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], No_action) + vs', [], NotifyAction (mem, addr, count) + with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], NoAction) | AtomicFence, vs -> - vs, [], No_action + vs, [], NoAction | MemorySize, vs -> let mem = memory frame.inst (0l @@ e.at) in - I32 (Memory.size mem) :: vs, [], No_action + I32 (Memory.size mem) :: vs, [], NoAction | MemoryGrow, I32 delta :: vs' -> let mem = memory frame.inst (0l @@ e.at) in @@ -371,30 +371,30 @@ let rec step_thread (t : thread) : thread * action = let result = try Memory.grow mem delta; old_size with Memory.SizeOverflow | Memory.SizeLimit | Memory.OutOfMemory -> -1l - in I32 result :: vs', [], No_action + in I32 result :: vs', [], NoAction | Const v, vs -> - v.it :: vs, [], No_action + v.it :: vs, [], NoAction | Test testop, v :: vs' -> - (try value_of_bool (Eval_numeric.eval_testop testop v) :: vs', [], No_action - with exn -> vs', [Trapping (numeric_error e.at exn) @@ e.at], No_action) + (try value_of_bool (Eval_numeric.eval_testop testop v) :: vs', [], NoAction + with exn -> vs', [Trapping (numeric_error e.at exn) @@ e.at], NoAction) | Compare relop, v2 :: v1 :: vs' -> - (try value_of_bool (Eval_numeric.eval_relop relop v1 v2) :: vs', [], No_action - with exn -> vs', [Trapping (numeric_error e.at exn) @@ e.at], No_action) + (try value_of_bool (Eval_numeric.eval_relop relop v1 v2) :: vs', [], NoAction + with exn -> vs', [Trapping (numeric_error e.at exn) @@ e.at], NoAction) | Unary unop, v :: vs' -> - (try Eval_numeric.eval_unop unop v :: vs', [], No_action - with exn -> vs', [Trapping (numeric_error e.at exn) @@ e.at], No_action) + (try Eval_numeric.eval_unop unop v :: vs', [], NoAction + with exn -> vs', [Trapping (numeric_error e.at exn) @@ e.at], NoAction) | Binary binop, v2 :: v1 :: vs' -> - (try Eval_numeric.eval_binop binop v1 v2 :: vs', [], No_action - with exn -> vs', [Trapping (numeric_error e.at exn) @@ e.at], No_action) + (try Eval_numeric.eval_binop binop v1 v2 :: vs', [], NoAction + with exn -> vs', [Trapping (numeric_error e.at exn) @@ e.at], NoAction) | Convert cvtop, v :: vs' -> - (try Eval_numeric.eval_cvtop cvtop v :: vs', [], No_action - with exn -> vs', [Trapping (numeric_error e.at exn) @@ e.at], No_action) + (try Eval_numeric.eval_cvtop cvtop v :: vs', [], NoAction + with exn -> vs', [Trapping (numeric_error e.at exn) @@ e.at], NoAction) | _ -> let s1 = string_of_values (List.rev vs) in @@ -404,7 +404,7 @@ let rec step_thread (t : thread) : thread * action = ) | Trapping msg, vs -> - [], [Trapping msg @@ e.at], No_action + [], [Trapping msg @@ e.at], NoAction | Returning vs', vs -> Crash.error e.at "undefined frame" @@ -413,32 +413,32 @@ let rec step_thread (t : thread) : thread * action = Crash.error e.at "undefined label" | Label (n, es0, (vs', [])), vs -> - vs' @ vs, [], No_action + vs' @ vs, [], NoAction | Label (n, es0, (vs', {it = Trapping msg; at} :: es')), vs -> - vs, [Trapping msg @@ at], No_action + vs, [Trapping msg @@ at], NoAction | Label (n, es0, (vs', {it = Returning vs0; at} :: es')), vs -> - vs, [Returning vs0 @@ at], No_action + vs, [Returning vs0 @@ at], NoAction | Label (n, es0, (vs', {it = Breaking (0l, vs0); at} :: es')), vs -> - take n vs0 e.at @ vs, List.map plain es0, No_action + take n vs0 e.at @ vs, List.map plain es0, NoAction | Label (n, es0, (vs', {it = Breaking (k, vs0); at} :: es')), vs -> - vs, [Breaking (Int32.sub k 1l, vs0) @@ at], No_action + vs, [Breaking (Int32.sub k 1l, vs0) @@ at], NoAction | Label (n, es0, code'), vs -> let t', act = step_thread {t with code = code'} in vs, [Label (n, es0, t'.code) @@ e.at], act | Frame (n, frame', (vs', [])), vs -> - vs' @ vs, [], No_action + vs' @ vs, [], NoAction | Frame (n, frame', (vs', {it = Trapping msg; at} :: es')), vs -> - vs, [Trapping msg @@ at], No_action + vs, [Trapping msg @@ at], NoAction | Frame (n, frame', (vs', {it = Returning vs0; at} :: es')), vs -> - take n vs0 e.at @ vs, [], No_action + take n vs0 e.at @ vs, [], NoAction | Frame (n, frame', code'), vs -> let t', act = step_thread {frame = frame'; code = code'; budget = t.budget - 1} in @@ -456,26 +456,26 @@ let rec step_thread (t : thread) : thread * action = let locals' = List.rev args @ List.map default_value f.it.locals in let frame' = {inst = !inst'; locals = List.map ref locals'} in let instr' = [Label (n2, [], ([], List.map plain f.it.body)) @@ f.at] in - vs', [Frame (n2, frame', ([], instr')) @@ e.at], No_action + vs', [Frame (n2, frame', ([], instr')) @@ e.at], NoAction | Func.HostFunc (t, f) -> - try List.rev (f (List.rev args)) @ vs', [], No_action + try List.rev (f (List.rev args)) @ vs', [], NoAction with Crash (_, msg) -> Crash.error e.at msg ) | Suspend _, vs -> (* TODO: meaningful timestamp handling *) - vs, [e], No_action + vs, [e], NoAction in {t with code = vs', es' @ List.tl es}, act -let rec push_to_inner_stack (c : code) (v : value) : code = +let rec plug_value (c : code) (v : value) : code = let vs, es = c in match es with | {it = Label (n, es0, c'); at} :: es' -> - vs, {it = Label (n, es0, push_to_inner_stack c' v); at} :: es' + vs, {it = Label (n, es0, plug_value c' v); at} :: es' | {it = Frame (n, f, c'); at} :: es' -> - vs, {it = Frame (n, f, push_to_inner_stack c' v); at} :: es' + vs, {it = Frame (n, f, plug_value c' v); at} :: es' | _ -> v :: vs, es @@ -487,16 +487,13 @@ let rec try_unsuspend (c : code) (m : memory_inst) (addr : Memory.address) : cod | {it = Frame (n, f, c'); at} :: es' -> Lib.Option.map (fun c'' -> vs, {it = Frame (n, f, c''); at} :: es') (try_unsuspend c' m addr) | {it = Suspend (m', addr', timeout); at} :: es' -> - if Memory.is_same_memory m m' && addr = addr' then + if Memory.same m m' && addr = addr' then Some (I32 0l :: vs, es') else None | _ -> None -let try_wake_one (t : thread) (m : memory_inst) (addr : Memory.address) : thread option = - Lib.Option.map (fun c' -> {t with code = c'}) (try_unsuspend t.code m addr) - let rec wake (c : config) (m : memory_inst) (addr : Memory.address) (count : int32) : config * int32 = if count = 0l then c, 0l @@ -505,7 +502,7 @@ let rec wake (c : config) (m : memory_inst) (addr : Memory.address) (count : int | [] -> c, 0l | t :: ts -> - let t', count' = match try_wake_one t m addr with | None -> t, 0l | Some t' -> t', 1l in + let t', count' = match (try_unsuspend t.code m addr) with | None -> t, 0l | Some c' -> {t with code = c'}, 1l in let ts', count'' = wake ts m addr (Int32.sub count count') in t' :: ts', Int32.add count' count'' @@ -518,10 +515,10 @@ let rec step (c : config) (n : thread_id) : config = Exhaustion.error (List.hd (snd t.code)).at "call stack exhausted" in match act with - | Notify_action (m, addr, count) -> + | NotifyAction (m, addr, count) -> let ts1', count1 = wake ts1 m addr count in let ts2', count2 = wake ts2 m addr (Int32.sub count count1) in - ts1' @ [{t' with code = push_to_inner_stack t'.code (I32 (Int32.add count1 count2))}] @ ts2' + ts1' @ [{t' with code = plug_value t'.code (I32 (Int32.add count1 count2))}] @ ts2' | _ -> ts1 @ [t'] @ ts2 let rec eval (c : config ref) (n : thread_id) : value list = From f9fdd9e34f253698056ac4e3d24f0180c1a4d723 Mon Sep 17 00:00:00 2001 From: conrad Date: Tue, 25 Apr 2023 07:20:02 +0100 Subject: [PATCH 5/6] comment --- interpreter/exec/eval.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml index 9d55ede9..48db4cbb 100644 --- a/interpreter/exec/eval.ml +++ b/interpreter/exec/eval.ml @@ -66,7 +66,7 @@ type action = (* memory, cell index, target timestamp *) | WaitAction of memory_inst * Memory.address * float (* memory, cell index, number of threads to wake *) - | NotifyAction of memory_inst * Memory.address * int32 + | NotifyAction of memory_inst * Memory.address * I32.t type thread = { From 91dac9e5429af9655f9b5aa6b908f10e05ba4111 Mon Sep 17 00:00:00 2001 From: conrad Date: Fri, 19 May 2023 09:59:58 +0100 Subject: [PATCH 6/6] comments --- interpreter/exec/eval.ml | 6 ++---- interpreter/runtime/memory.ml | 3 --- interpreter/runtime/memory.mli | 2 -- 3 files changed, 2 insertions(+), 9 deletions(-) diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml index 48db4cbb..633fb4d0 100644 --- a/interpreter/exec/eval.ml +++ b/interpreter/exec/eval.ml @@ -63,8 +63,6 @@ and admin_instr' = type action = | NoAction - (* memory, cell index, target timestamp *) - | WaitAction of memory_inst * Memory.address * float (* memory, cell index, number of threads to wake *) | NotifyAction of memory_inst * Memory.address * I32.t @@ -341,7 +339,7 @@ let rec step_thread (t : thread) : thread * action = I32 2l :: vs', [], NoAction (* Treat as though wait timed out immediately *) else (* TODO: meaningful timestamp handling *) - vs', [Suspend (mem, addr, 0.) @@ e.at], (WaitAction (mem, addr, 0.)) + vs', [Suspend (mem, addr, 0.) @@ e.at], NoAction else I32 1l :: vs', [], NoAction (* Not equal *) with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at], NoAction) @@ -487,7 +485,7 @@ let rec try_unsuspend (c : code) (m : memory_inst) (addr : Memory.address) : cod | {it = Frame (n, f, c'); at} :: es' -> Lib.Option.map (fun c'' -> vs, {it = Frame (n, f, c''); at} :: es') (try_unsuspend c' m addr) | {it = Suspend (m', addr', timeout); at} :: es' -> - if Memory.same m m' && addr = addr' then + if m == m' && addr = addr' then Some (I32 0l :: vs, es') else None diff --git a/interpreter/runtime/memory.ml b/interpreter/runtime/memory.ml index ea3b3648..764f295f 100644 --- a/interpreter/runtime/memory.ml +++ b/interpreter/runtime/memory.ml @@ -20,9 +20,6 @@ exception OutOfMemory let page_size = 0x10000L (* 64 KiB *) -let same m1 m2 = - m1.content == m2.content - let is_aligned a t sz = let align = match sz with diff --git a/interpreter/runtime/memory.mli b/interpreter/runtime/memory.mli index e95e0a08..e765e91c 100644 --- a/interpreter/runtime/memory.mli +++ b/interpreter/runtime/memory.mli @@ -16,8 +16,6 @@ exception OutOfMemory val page_size : int64 -val same : memory -> memory -> bool - val is_aligned : address -> value_type -> pack_size option -> bool val alloc : memory_type -> memory (* raises SizeOverflow, OutOfMemory *)