diff --git a/document/core/appendix/index-instructions.rst b/document/core/appendix/index-instructions.rst index cc34fd05..e8137e3a 100644 --- a/document/core/appendix/index-instructions.rst +++ b/document/core/appendix/index-instructions.rst @@ -200,8 +200,8 @@ Instruction Binary Opcode :math:`\F32.\REINTERPRET\K{\_}\I32` :math:`\hex{BE}` :math:`[\I32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` :math:`\F64.\REINTERPRET\K{\_}\I64` :math:`\hex{BF}` :math:`[\I64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` :math:`\ATOMICNOTIFY~\memarg` :math:`\hex{FE}~\hex{00}` :math:`[\I32~\I64] \to [\I64]` :ref:`validation ` -:math:`\I32.\ATOMICWAIT~\memarg` :math:`\hex{FE}~\hex{01}` :math:`[\I32~\I32~\I64] \to [\I32]` :ref:`validation ` -:math:`\I64.\ATOMICWAIT~\memarg` :math:`\hex{FE}~\hex{02}` :math:`[\I32~\I64~\I64] \to [\I32]` :ref:`validation ` +:math:`\MEMORYATOMICWAIT32~\memarg` :math:`\hex{FE}~\hex{01}` :math:`[\I32~\I32~\I64] \to [\I32]` :ref:`validation ` +:math:`\MEMORYATOMICWAIT64~\memarg` :math:`\hex{FE}~\hex{02}` :math:`[\I32~\I64~\I64] \to [\I32]` :ref:`validation ` :math:`\I32.\ATOMICLOAD~\memarg` :math:`\hex{FE}~\hex{10}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` :math:`\I64.\ATOMICLOAD~\memarg` :math:`\hex{FE}~\hex{11}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` :math:`\I32.\ATOMICLOAD\K{8\_u}~\memarg` :math:`\hex{FE}~\hex{12}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` diff --git a/document/core/binary/instructions.rst b/document/core/binary/instructions.rst index 3699bc28..46dc8f73 100644 --- a/document/core/binary/instructions.rst +++ b/document/core/binary/instructions.rst @@ -184,9 +184,9 @@ Each variant of :ref:`atomic memory instruction ` is .. math:: \begin{array}{llclll} \production{instruction} & \Binstr &::=& \dots && \phantom{thisshouldbeenough} \\ &&|& - \hex{FE}~\hex{00}~~m{:}\Bmemarg &\Rightarrow& \ATOMICNOTIFY~m \\ &&|& - \hex{FE}~\hex{01}~~m{:}\Bmemarg &\Rightarrow& \I32.\ATOMICWAIT~m \\ &&|& - \hex{FE}~\hex{02}~~m{:}\Bmemarg &\Rightarrow& \I64.\ATOMICWAIT~m \\ + \hex{FE}~\hex{00}~~m{:}\Bmemarg &\Rightarrow& \MEMORYATOMICNOTIFY~m \\ &&|& + \hex{FE}~\hex{01}~~m{:}\Bmemarg &\Rightarrow& \MEMORYATOMICWAIT\K{32}~m \\ &&|& + \hex{FE}~\hex{02}~~m{:}\Bmemarg &\Rightarrow& \MEMORYATOMICWAIT\K{64}~m \\ \end{array} diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index d21e71f6..5fab4956 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -966,8 +966,8 @@ See :ref:`above `. .. _exec-wait: -:math:`t\K{.}\ATOMICWAIT` -......................... +:math:`\MEMORYATOMICWAIT{N}` +............................ .. todo:: update to new rules .. todo:: add text @@ -975,37 +975,37 @@ See :ref:`above `. .. math:: \begin{array}{l} \begin{array}{lcl@{\qquad}l} - F; (\I64.\CONST~k)~(t.\CONST~c)~(\I32.\CONST~i)~t.\ATOMICWAIT - &\stepto^{(\ARD~a.\LLEN~n)~(\ARD~a.\LDATA[i]~b^{|t|})}& + F; (\I64.\CONST~k)~(\iN.\CONST~c)~(\I32.\CONST~i)~\MEMORYATOMICWAIT{N} + &\stepto^{(\ARD~a.\LLEN~n)~(\ARD~a.\LDATA[i]~b^{N})}& F; (\WAITX~a.\LDATA[i]) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} - (\iff & \X{ea} + |t|/8 \leq n \\ - \wedge & \X{ea} \mod |t|/8 = 0 \\ - \wedge & b^{|t|} = \bytes_t(c) \\ + (\iff & \X{ea} + N/8 \leq n \\ + \wedge & \X{ea} \mod N/8 = 0 \\ + \wedge & b^{N} = \bytes_t(c) \\ \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - F; (\I64.\CONST~k)~(t.\CONST~c)~(\I32.\CONST~i)~t.\ATOMICWAIT - &\stepto^{(\ARD~a.\LLEN~n)~(\ARD~a.\LDATA[i]~b^{|t|})}& + F; (\I64.\CONST~k)~(\iN.\CONST~c)~(\I32.\CONST~i)~\MEMORYATOMICWAIT{N} + &\stepto^{(\ARD~a.\LLEN~n)~(\ARD~a.\LDATA[i]~b^{N})}& F; (\I32.\CONST~1) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} - (\iff & \X{ea} + |t|/8 \leq n \\ - \wedge & \X{ea} \mod |t|/8 = 0 \\ - \wedge & b^{|t|} \neq \bytes_t(c) \\ + (\iff & \X{ea} + N/8 \leq n \\ + \wedge & \X{ea} \mod N/8 = 0 \\ + \wedge & b^{N} \neq \bytes_t(c) \\ \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - F; (\I64.\CONST~k)~(t.\CONST~c)~(\I32.\CONST~i)~t.\ATOMICWAIT + F; (\I64.\CONST~k)~(\iN.\CONST~c)~(\I32.\CONST~i)~\MEMORYATOMICWAIT{N} &\stepto^{(\ARD~a.\LLEN~n)}& F; \TRAP \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} - (\iff i + |t|/8 > n \vee i \mod |t|/8 \neq 0) \\ + (\iff i + N/8 > n \vee i \mod N/8 \neq 0) \\ \end{array} \\[2ex] \begin{array}[t]{@{}r@{~}l@{}} @@ -1017,8 +1017,8 @@ See :ref:`above `. .. _exec-notify: -:math:`\ATOMICNOTIFY` -..................... +:math:`\MEMORYATOMICNOTIFY` +........................... .. todo:: update to new rules .. todo:: add text; operand order? is the trap case correct (issue #105)? diff --git a/document/core/syntax/instructions.rst b/document/core/syntax/instructions.rst index bacbba72..bd96e678 100644 --- a/document/core/syntax/instructions.rst +++ b/document/core/syntax/instructions.rst @@ -287,8 +287,8 @@ Instructions in this group are concerned with accessing :ref:`linear memory ` have behavior of the :ref:`ibinop ` of the same name. -The |ATOMICWAIT| and |ATOMICNOTIFY| instructions provide primitive -synchronization between :ref:`threads `. The |ATOMICWAIT| +The |MEMORYATOMICWAIT| and |MEMORYATOMICNOTIFY| instructions provide primitive +synchronization between :ref:`threads `. The |MEMORYATOMICWAIT| instructions atomically load a value from the calculated effective address and compare it to an expected value. If they are equal, the thread is then suspended until a given timeout expires or another thread wakes it. The -|ATOMICNOTIFY| instruction wakes threads that are waiting on a given address, up -to a given maximum. +|MEMORYATOMICNOTIFY| instruction wakes threads that are waiting on a given +address, up to a given maximum. .. index:: ! control instruction, ! structured control, ! label, ! block, ! branch, ! unwinding, result type, label index, function index, type index, vector, trap, function, table, function type diff --git a/document/core/text/instructions.rst b/document/core/text/instructions.rst index 95c34497..4fb91bf5 100644 --- a/document/core/text/instructions.rst +++ b/document/core/text/instructions.rst @@ -241,9 +241,9 @@ The offset immediate to atomic memory instructions is optional, and defaults to .. math:: \begin{array}{llclll} \production{instruction} & \Tplaininstr_I &::=& \dots \phantom{thisshouldbeenoughnowitissee} && \phantom{thisshouldbeenough} \\ &&|& - \text{atomic.notify}~~m{:}\Tmemarg_4 &\Rightarrow& \ATOMICNOTIFY~m \\ &&|& - \text{i32.atomic.wait}~~m{:}\Tmemarg_4 &\Rightarrow& \I32.\ATOMICWAIT~m \\ &&|& - \text{i64.atomic.wait}~~m{:}\Tmemarg_8 &\Rightarrow& \I64.\ATOMICWAIT~m \\ + \text{memory.atomic.notify}~~m{:}\Tmemarg_4 &\Rightarrow& \MEMORYATOMICNOTIFY~m \\ &&|& + \text{memory.atomic.wait32}~~m{:}\Tmemarg_4 &\Rightarrow& \MEMORYATOMICWAIT{32}~m \\ &&|& + \text{memory.atomic.wait64}~~m{:}\Tmemarg_8 &\Rightarrow& \MEMORYATOMICWAIT{64}~m \\ \end{array} .. math:: diff --git a/document/core/util/macros.def b/document/core/util/macros.def index a89c211a..63b974d0 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -379,8 +379,8 @@ .. |REINTERPRET| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{reinterpret}} .. |ATOMIC| mathdef:: \xref{syntax/instructions}{syntax-instr-atomic-memory}{\K{atomic}} -.. |ATOMICWAIT| mathdef:: \xref{syntax/instructions}{syntax-instr-atomic-memory}{\K{atomic.wait}} -.. |ATOMICNOTIFY| mathdef:: \xref{syntax/instructions}{syntax-instr-atomic-memory}{\K{atomic.notify}} +.. |MEMORYATOMICWAIT| mathdef:: \xref{syntax/instructions}{syntax-instr-atomic-memory}{\K{memory.atomic.wait}} +.. |MEMORYATOMICNOTIFY| mathdef:: \xref{syntax/instructions}{syntax-instr-atomic-memory}{\K{memory.atomic.notify}} .. |ATOMICADD| mathdef:: \xref{syntax/instructions}{syntax-instr-atomic-memory}{\K{add}} .. |ATOMICSUB| mathdef:: \xref{syntax/instructions}{syntax-instr-atomic-memory}{\K{sub}} .. |ATOMICAND| mathdef:: \xref{syntax/instructions}{syntax-instr-atomic-memory}{\K{and}} diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 4396042b..d7a66664 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -433,8 +433,8 @@ Atomic Memory Instructions .. _valid-atomic-notify: -:math:`\ATOMICNOTIFY~\memarg` -............................. +:math:`\MEMORYATOMICNOTIFY~\memarg` +................................... * The memory :math:`C.\CMEMS[0]` must be defined in the context. @@ -450,29 +450,29 @@ Atomic Memory Instructions \qquad 2^{\memarg.\ALIGN} = 4 }{ - C \vdash \ATOMICNOTIFY~\memarg : [\I32~\I64] \to [\I64] + C \vdash \MEMORYATOMICNOTIFY~\memarg : [\I32~\I64] \to [\I64] } .. _valid-atomic-wait: -:math:`t\K{.}\ATOMICWAIT~\memarg` -................................. +:math:`\MEMORYATOMICWAIT{N}~\memarg` +.................................... * The memory :math:`C.\CMEMS[0]` must be defined in the context. * Let :math:`\limits~\share` be the :ref:`memory type ` :math:`C.\CMEMS[0]`. -* The alignment :math:`2^{\memarg.\ALIGN}` must be equal to the :ref:`width ` of :math:`t` divided by :math:`8`. +* The alignment :math:`2^{\memarg.\ALIGN}` must be equal to :math:`N` divided by :math:`8`. -* Then the instruction is valid with type :math:`[\I32~t~\I64] \to [\I32]`. +* Then the instruction is valid with type :math:`[\I32~\K{i}{N}~\I64] \to [\I32]`. .. math:: \frac{ C.\CMEMS[0] = \memtype \qquad - 2^{\memarg.\ALIGN} = |t|/8 + 2^{\memarg.\ALIGN} = N/8 }{ - C \vdash t\K{.}\ATOMICWAIT~\memarg : [\I32~t~\I64] \to [\I32] + C \vdash \MEMORYATOMICWAIT{N}~\memarg : [\I32~\K{i}{N}~\I64] \to [\I32] } .. _valid-atomic-load: diff --git a/interpreter/binary/decode.ml b/interpreter/binary/decode.ml index 3186374b..3f2bc0ff 100644 --- a/interpreter/binary/decode.ml +++ b/interpreter/binary/decode.ml @@ -209,9 +209,9 @@ let memop s = let atomic_instr s = let pos = pos s in match op s with - | 0x00 -> let a, o = memop s in atomic_notify a o - | 0x01 -> let a, o = memop s in i32_atomic_wait a o - | 0x02 -> let a, o = memop s in i64_atomic_wait a o + | 0x00 -> let a, o = memop s in memory_atomic_notify a o + | 0x01 -> let a, o = memop s in memory_atomic_wait32 a o + | 0x02 -> let a, o = memop s in memory_atomic_wait64 a o | 0x10 -> let a, o = memop s in i32_atomic_load a o | 0x11 -> let a, o = memop s in i64_atomic_load a o diff --git a/interpreter/binary/encode.ml b/interpreter/binary/encode.ml index 8471cafa..ed2f347c 100644 --- a/interpreter/binary/encode.ml +++ b/interpreter/binary/encode.ml @@ -207,17 +207,18 @@ let encode m = | Store ({ty = I64Type; sz = Some Pack32; _} as mo) -> op 0x3e; memop mo | Store {ty = F32Type | F64Type; sz = Some _; _} -> assert false - | AtomicNotify ({ty = I32Type; sz = None; _} as mo) -> + | MemoryAtomicNotify ({ty = I32Type; sz = None; _} as mo) -> op 0xfe; op 0x00; memop mo - | AtomicNotify {ty = I32Type; sz = Some _; _} -> assert false - | AtomicNotify {ty = I64Type | F32Type | F64Type; _} -> assert false + | MemoryAtomicNotify {ty = I32Type; sz = Some _; _} -> assert false + | MemoryAtomicNotify {ty = I64Type | F32Type | F64Type; _} -> assert false - | AtomicWait ({ty = I32Type; sz = None; _} as mo) -> + | MemoryAtomicWait ({ty = I32Type; sz = None; _} as mo) -> op 0xfe; op 0x01; memop mo - | AtomicWait ({ty = I64Type; sz = None; _} as mo) -> + | MemoryAtomicWait ({ty = I64Type; sz = None; _} as mo) -> op 0xfe; op 0x02; memop mo - | AtomicWait {ty = I32Type | I64Type; sz = Some _; _} -> assert false - | AtomicWait {ty = F32Type | F64Type; _} -> assert false + | MemoryAtomicWait {ty = I32Type | I64Type; sz = Some _; _} -> + assert false + | MemoryAtomicWait {ty = F32Type | F64Type; _} -> assert false | AtomicLoad ({ty = I32Type; sz = None; _} as mo) -> op 0xfe; op 0x10; memop mo diff --git a/interpreter/exec/eval.ml b/interpreter/exec/eval.ml index d4b220a4..f6961926 100644 --- a/interpreter/exec/eval.ml +++ b/interpreter/exec/eval.ml @@ -276,8 +276,7 @@ let rec step (c : config) : config = v1 :: vs', [] with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at]); - | AtomicWait {offset; ty; sz; _}, I64 timeout :: ve :: I32 i :: vs' -> - (* TODO: Trap if memory is not shared *) + | 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 @@ -290,7 +289,7 @@ let rec step (c : config) : config = I32 1l :: vs', [] (* Not equal *) with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at]) - | AtomicNotify x, I32 count :: I32 i :: vs' -> + | MemoryAtomicNotify x, I32 count :: I32 i :: vs' -> if count = 0l then I32 0l :: vs', [] (* Trivial case waking 0 waiters *) else diff --git a/interpreter/syntax/ast.ml b/interpreter/syntax/ast.ml index 3b3e6715..7a5e2335 100644 --- a/interpreter/syntax/ast.ml +++ b/interpreter/syntax/ast.ml @@ -102,8 +102,8 @@ and instr' = | Unary of unop (* unary numeric operator *) | Binary of binop (* binary numeric operator *) | Convert of cvtop (* conversion *) - | AtomicWait of atomicop (* atomically wait for notification at address *) - | AtomicNotify of atomicop (* atomically notify all waiters at address *) + | MemoryAtomicWait of atomicop (* atomically wait for notification at address *) + | MemoryAtomicNotify of atomicop (* atomically notify all waiters at address *) | AtomicLoad of atomicop (* atomically read memory at address *) | AtomicStore of atomicop (* atomically write memory at address *) | AtomicRmw of rmwop * atomicop (* atomically read, modify, write memory at address *) diff --git a/interpreter/syntax/operators.ml b/interpreter/syntax/operators.ml index 3b4bb10d..75a19cf1 100644 --- a/interpreter/syntax/operators.ml +++ b/interpreter/syntax/operators.ml @@ -71,13 +71,13 @@ let i64_store16 align offset = let i64_store32 align offset = Store {ty = I64Type; align; offset; sz = Some Pack32} -let atomic_notify align offset = - AtomicNotify {ty = I32Type; align; offset; sz = None} +let memory_atomic_notify align offset = + MemoryAtomicNotify {ty = I32Type; align; offset; sz = None} -let i32_atomic_wait align offset = - AtomicWait {ty = I32Type; align; offset; sz = None} -let i64_atomic_wait align offset = - AtomicWait {ty = I64Type; align; offset; sz = None} +let memory_atomic_wait32 align offset = + MemoryAtomicWait {ty = I32Type; align; offset; sz = None} +let memory_atomic_wait64 align offset = + MemoryAtomicWait {ty = I64Type; align; offset; sz = None} let i32_atomic_load align offset = AtomicLoad {ty = I32Type; align; offset; sz = None} diff --git a/interpreter/text/arrange.ml b/interpreter/text/arrange.ml index 9ee4ebd6..4fd24981 100644 --- a/interpreter/text/arrange.ml +++ b/interpreter/text/arrange.ml @@ -196,6 +196,11 @@ let extension = function | Memory.SX -> "_s" | Memory.ZX -> "_u" +let wait_size = function + | I32Type -> "32" + | I64Type -> "64" + | _ -> assert false + let rmw = function | I32 I32Op.RmwAdd | I64 I64Op.RmwAdd -> "add" | I32 I32Op.RmwSub | I64 I64Op.RmwSub -> "sub" @@ -225,14 +230,16 @@ let storeop op = | None -> memop "store" op (size op.ty) | Some sz -> memop ("store" ^ pack_size sz) op (Memory.packed_size sz) -let atomicwaitop op = +let memoryatomicwaitop op = match op.sz with - | None -> memop "atomic.wait" op (size op.ty) + | None -> + memop_without_type ("memory.atomic.wait" ^ (wait_size op.ty)) op + (size op.ty) | Some sz -> assert false -let atomicnotifyop op = +let memoryatomicnotifyop op = match op.sz with - | None -> memop_without_type "atomic.notify" op (size op.ty) + | None -> memop_without_type "memory.atomic.notify" op (size op.ty) | Some sz -> assert false let atomicloadop op = @@ -302,8 +309,8 @@ let rec instr e = | Unary op -> unop op, [] | Binary op -> binop op, [] | Convert op -> cvtop op, [] - | AtomicWait op -> atomicwaitop op, [] - | AtomicNotify op -> atomicnotifyop op, [] + | MemoryAtomicWait op -> memoryatomicwaitop op, [] + | MemoryAtomicNotify op -> memoryatomicnotifyop op, [] | AtomicLoad op -> atomicloadop op, [] | AtomicStore op -> atomicstoreop op, [] | AtomicRmw (rmwop, op) -> atomicrmwop op rmwop, [] diff --git a/interpreter/text/lexer.mll b/interpreter/text/lexer.mll index 85b6cd00..ab03290b 100644 --- a/interpreter/text/lexer.mll +++ b/interpreter/text/lexer.mll @@ -154,11 +154,12 @@ let string = '"' character* '"' let name = '$' (letter | digit | '_' | symbol)+ let reserved = ([^'\"''('')'';'] # space)+ (* hack for table size *) -let ixx = "i" ("32" | "64") -let fxx = "f" ("32" | "64") +let xx = "32" | "64" +let ixx = "i" xx +let fxx = "f" xx let nxx = ixx | fxx let mixx = "i" ("8" | "16" | "32" | "64") -let mfxx = "f" ("32" | "64") +let mfxx = "f" xx let sign = "s" | "u" let mem_size = "8" | "16" | "32" let rmw = "add" | "sub" | "and" | "or" | "xor" | "xchg" @@ -251,11 +252,13 @@ rule token = parse (i64_store16 (opt a 1)) (i64_store32 (opt a 2)) o)) } - | "atomic.notify" - { ATOMIC_NOTIFY (fun a o -> (atomic_notify (opt a 2)) o) } - | (ixx as t)".atomic.wait" - { ATOMIC_WAIT (fun a o -> - intop t (i32_atomic_wait (opt a 2)) (i64_atomic_wait (opt a 3)) o) } + | "memory.atomic.notify" + { MEMORY_ATOMIC_NOTIFY (fun a o -> (memory_atomic_notify (opt a 2)) o) } + | "memory.atomic.wait"(xx as sz) + { MEMORY_ATOMIC_WAIT (fun a o -> + intop ("i" ^ sz) + (memory_atomic_wait32 (opt a 2)) + (memory_atomic_wait64 (opt a 3)) o) } | (ixx as t)".atomic.load" { ATOMIC_LOAD (fun a o -> intop t (i32_atomic_load (opt a 2)) (i64_atomic_load (opt a 3)) o) } diff --git a/interpreter/text/parser.mly b/interpreter/text/parser.mly index 071ee1f7..37feb12e 100644 --- a/interpreter/text/parser.mly +++ b/interpreter/text/parser.mly @@ -158,7 +158,7 @@ let inline_type_explicit (c : context) x ft at = %token CALL CALL_INDIRECT RETURN %token LOCAL_GET LOCAL_SET LOCAL_TEE GLOBAL_GET GLOBAL_SET %token LOAD STORE OFFSET_EQ_NAT ALIGN_EQ_NAT -%token ATOMIC_WAIT ATOMIC_NOTIFY +%token MEMORY_ATOMIC_WAIT MEMORY_ATOMIC_NOTIFY %token ATOMIC_LOAD ATOMIC_STORE ATOMIC_RMW ATOMIC_RMW_CMPXCHG %token CONST UNARY BINARY TEST COMPARE CONVERT %token UNREACHABLE MEMORY_SIZE MEMORY_GROW @@ -186,8 +186,8 @@ let inline_type_explicit (c : context) x ft at = %token CONVERT %token Memory.offset -> Ast.instr'> LOAD %token Memory.offset -> Ast.instr'> STORE -%token Memory.offset -> Ast.instr'> ATOMIC_WAIT -%token Memory.offset -> Ast.instr'> ATOMIC_NOTIFY +%token Memory.offset -> Ast.instr'> MEMORY_ATOMIC_WAIT +%token Memory.offset -> Ast.instr'> MEMORY_ATOMIC_NOTIFY %token Memory.offset -> Ast.instr'> ATOMIC_LOAD %token Memory.offset -> Ast.instr'> ATOMIC_STORE %token Memory.offset -> Ast.instr'> ATOMIC_RMW @@ -345,8 +345,8 @@ plain_instr : | UNARY { fun c -> $1 } | BINARY { fun c -> $1 } | CONVERT { fun c -> $1 } - | ATOMIC_WAIT offset_opt align_opt { fun c -> $1 $3 $2 } - | ATOMIC_NOTIFY offset_opt align_opt { fun c -> $1 $3 $2 } + | MEMORY_ATOMIC_WAIT offset_opt align_opt { fun c -> $1 $3 $2 } + | MEMORY_ATOMIC_NOTIFY offset_opt align_opt { fun c -> $1 $3 $2 } | ATOMIC_LOAD offset_opt align_opt { fun c -> $1 $3 $2 } | ATOMIC_STORE offset_opt align_opt { fun c -> $1 $3 $2 } | ATOMIC_RMW offset_opt align_opt { fun c -> $1 $3 $2 } diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml index a62149c8..d4a59d50 100644 --- a/interpreter/valid/valid.ml +++ b/interpreter/valid/valid.ml @@ -292,11 +292,11 @@ let rec check_instr (c : context) (e : instr) (s : infer_stack_type) : op_type = let t1, t2 = type_cvtop e.at cvtop in [t1] --> [t2] - | AtomicNotify memop -> + | MemoryAtomicNotify memop -> check_memop c memop (Some Shared) (fun sz -> sz) e.at; [I32Type; I32Type] --> [I32Type] - | AtomicWait memop -> + | MemoryAtomicWait memop -> check_memop c memop (Some Shared) (fun sz -> sz) e.at; [I32Type; memop.ty; I64Type] --> [I32Type] diff --git a/proposals/threads/Overview.md b/proposals/threads/Overview.md index 57451c88..2d2ef87f 100644 --- a/proposals/threads/Overview.md +++ b/proposals/threads/Overview.md @@ -50,12 +50,12 @@ mutex is unlocked. If its value is 1, the mutex is locked. (br_if $done) ;; Wait for the other agent to finish with mutex. - (i32.atomic.wait + (memory.atomic.wait32 (local.get $mutexAddr) ;; mutex address (i32.const 1) ;; expected value (1 => locked) (i64.const -1)) ;; infinite timeout - ;; i32.atomic.wait returns: + ;; memory.atomic.wait32 returns: ;; 0 => "ok", woken by another agent. ;; 1 => "not-equal", loaded value != expected value ;; 2 => "timed-out", the timeout expired @@ -81,7 +81,7 @@ mutex is unlocked. If its value is 1, the mutex is locked. ;; Notify one agent that is waiting on this lock. (drop - (atomic.notify + (memory.atomic.notify (local.get $mutexAddr) ;; mutex address (i32.const 1))) ;; notify 1 waiter ) @@ -352,8 +352,9 @@ will not be suspended for other reasons, unless all agents in that cluster are also suspended. An agent suspended via `Atomics.wait` can be woken by the WebAssembly -`atomic.notify` operator. Similarly, an agent suspended by `i32.atomic.wait` or -`i64.atomic.wait` can be woken by [`Atomics.notify`][]. +`memory.atomic.notify` operator. Similarly, an agent suspended by +`memory.atomic.wait32` or `memory.atomic.wait64` can be woken by +[`Atomics.notify`][]. ### Wait @@ -380,15 +381,15 @@ woken, the wait operator returns 0 ("ok"). If the timeout expires before another agent notifies this one, this operator returns 2 ("timed-out"). Note that when the agent is suspended, it will not be [spuriously woken](https://en.wikipedia.org/wiki/Spurious_wakeup). The agent is only woken -by `atomic.notify` (or [`Atomics.notify`][] in the web embedding). +by `memory.atomic.notify` (or [`Atomics.notify`][] in the web embedding). When an agent is suspended, if the number of waiters (including this one) is equal to 232, then trap. - * `i32.atomic.wait`: load i32 value, compare to expected (as `i32`), and wait for notify at same address - * `i64.atomic.wait`: load i64 value, compare to expected (as `i64`), and wait for notify at same address + * `memory.atomic.wait32`: load i32 value, compare to expected (as `i32`), and wait for notify at same address + * `memory.atomic.wait64`: load i64 value, compare to expected (as `i64`), and wait for notify at same address -For the web embedding, `i32.atomic.wait` is equivalent in behavior to executing the following: +For the web embedding, `memory.atomic.wait32` is equivalent in behavior to executing the following: 1. Let `memory` be a `WebAssembly.Memory` object for this module. 1. Let `buffer` be `memory`([`Get`][](`memory`, `"buffer"`)). @@ -399,7 +400,7 @@ For the web embedding, `i32.atomic.wait` is equivalent in behavior to executing 1. Return an `i32` value as described in the above table: ("ok" -> `0`, "not-equal" -> `1`, "timed-out" -> `2`). -`i64.atomic.wait` has no equivalent in ECMAScript as it is currently specified, as there is +`memory.atomic.wait64` has no equivalent in ECMAScript as it is currently specified, as there is no `Int64Array` type, and an ECMAScript `Number` cannot represent all values of a 64-bit integer. That said, the behavior can be approximated as follows: @@ -428,9 +429,9 @@ returns the number of waiters that were woken as an unsigned `i32`. Note that if the notify operator is used with an unshared linear memory, the number of waiters will always be zero. - * `atomic.notify`: notify `count` threads waiting on the given address via `i32.atomic.wait` or `i64.atomic.wait` + * `memory.atomic.notify`: notify `count` threads waiting on the given address via `memory.atomic.wait32` or `memory.atomic.wait64` -For the web embedding, `atomic.notify` is equivalent in behavior to executing the following: +For the web embedding, `memory.atomic.notify` is equivalent in behavior to executing the following: 1. Let `memory` be a `WebAssembly.Memory` object for this module. 1. Let `buffer` be `memory`([`Get`][](`memory`, `"buffer"`)). @@ -572,8 +573,8 @@ The [instruction syntax][] is modified as follows: atomicop ::= add | sub | and | or | xor | xchg | cmpxchg instr ::= ... | - inn.atomic.wait memarg | - atomic.notify memarg | + memory.atomic.wait{nn} memarg | + memory.atomic.notify memarg | atomic.fence | @@ -596,9 +597,9 @@ memarg32 ::= 0x02 o: offset => {align 2, offset: o} memarg64 ::= 0x03 o: offset => {align 3, offset: o} instr ::= ... - | 0xFE 0x00 m:memarg32 => atomic.notify m - | 0xFE 0x01 m:memarg32 => i32.atomic.wait m - | 0xFE 0x02 m:memarg64 => i64.atomic.wait m + | 0xFE 0x00 m:memarg32 => memory.atomic.notify m + | 0xFE 0x01 m:memarg32 => memory.atomic.wait32 m + | 0xFE 0x02 m:memarg64 => memory.atomic.wait64 m | 0xFE 0x03 0x00 => atomic.fence diff --git a/test/core/atomic.wast b/test/core/atomic.wast index 79484041..3ac79a93 100644 --- a/test/core/atomic.wast +++ b/test/core/atomic.wast @@ -470,15 +470,15 @@ (func (export "init") (param $value i64) (i64.store (i32.const 0) (local.get $value))) - (func (export "atomic.notify") (param $addr i32) (param $count i32) (result i32) - (atomic.notify (local.get 0) (local.get 1))) - (func (export "i32.atomic.wait") (param $addr i32) (param $expected i32) (param $timeout i64) (result i32) - (i32.atomic.wait (local.get 0) (local.get 1) (local.get 2))) - (func (export "i64.atomic.wait") (param $addr i32) (param $expected i64) (param $timeout i64) (result i32) - (i64.atomic.wait (local.get 0) (local.get 1) (local.get 2))) + (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_return (invoke "i32.atomic.wait" (i32.const 0) (i32.const 0) (i64.const 0)) (i32.const 1)) -(assert_return (invoke "i64.atomic.wait" (i32.const 0) (i64.const 0) (i64.const 0)) (i32.const 1)) -(assert_return (invoke "atomic.notify" (i32.const 0) (i32.const 0)) (i32.const 0)) +(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)) +(assert_return (invoke "memory.atomic.notify" (i32.const 0) (i32.const 0)) (i32.const 0))