Skip to content

[interpreter] implement atomic.fence, add wait/notify edge case tests #192

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Oct 11, 2022
Merged

[interpreter] implement atomic.fence, add wait/notify edge case tests #192

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
3537229
implement atomic.fence, add wait/notify edge case tests
conrad-watt Sep 29, 2022
9404b81
Update interpreter/exec/eval.ml
conrad-watt Oct 4, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions interpreter/binary/decode.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -466,6 +466,7 @@ let rec instr s =
| 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
| 0x03 -> expect 0x00 s "zero flag expected"; atomic_fence

| 0x10 -> let a, o = memop s in i32_atomic_load a o
| 0x11 -> let a, o = memop s in i64_atomic_load a o
Expand Down
3 changes: 3 additions & 0 deletions interpreter/binary/encode.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -221,6 +221,9 @@ let encode m =
assert false
| MemoryAtomicWait {ty = F32Type | F64Type; _} -> assert false

| AtomicFence ->
op 0xfe; op 0x03; op 0x00

| AtomicLoad ({ty = I32Type; sz = None; _} as mo) ->
op 0xfe; op 0x10; memop mo
| AtomicLoad ({ty = I64Type; sz = None; _} as mo) ->
Expand Down
16 changes: 15 additions & 1 deletion interpreter/exec/eval.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -132,6 +132,10 @@ let check_align addr ty sz at =
if not (Memory.is_aligned addr ty sz) then
Trap.error at "unaligned atomic memory access"

let check_shared mem at =
if shared_memory_type (Memory.type_of mem) <> Shared then
Trap.error at "expected shared memory"


(* Evaluation *)

Expand Down Expand Up @@ -319,18 +323,28 @@ let rec step_thread (t : thread) : thread =
(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 x, I32 count :: I32 i :: vs' ->
| 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;
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Shouldn't this symmetrically require shared as well?

Copy link
Collaborator Author

@conrad-watt conrad-watt Oct 4, 2022 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Currently we allow notify on unshared memory. It's only wait that's disallowed (see also #191).

let _ = Memory.load_value mem addr offset ty in
if count = 0l then
I32 0l :: vs', [] (* Trivial case waking 0 waiters *)
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
Expand Down
1 change: 1 addition & 0 deletions interpreter/syntax/ast.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -106,6 +106,7 @@ and instr' =
| Convert of cvtop (* conversion *)
| MemoryAtomicWait of atomicop (* atomically wait for notification at address *)
| MemoryAtomicNotify of atomicop (* atomically notify all waiters at address *)
| AtomicFence (* perform an atomic fence *)
| 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 *)
Expand Down
3 changes: 3 additions & 0 deletions interpreter/syntax/operators.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -78,6 +78,9 @@ let memory_atomic_wait32 align offset =
let memory_atomic_wait64 align offset =
MemoryAtomicWait {ty = I64Type; align; offset; sz = None}

let atomic_fence =
AtomicFence

let i32_atomic_load align offset =
AtomicLoad {ty = I32Type; align; offset; sz = None}
let i64_atomic_load align offset =
Expand Down
1 change: 1 addition & 0 deletions interpreter/text/arrange.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -311,6 +311,7 @@ let rec instr e =
| Convert op -> cvtop op, []
| MemoryAtomicWait op -> memoryatomicwaitop op, []
| MemoryAtomicNotify op -> memoryatomicnotifyop op, []
| AtomicFence -> "atomic.fence", []
| AtomicLoad op -> atomicloadop op, []
| AtomicStore op -> atomicstoreop op, []
| AtomicRmw (rmwop, op) -> atomicrmwop op rmwop, []
Expand Down
1 change: 1 addition & 0 deletions interpreter/text/lexer.mll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -259,6 +259,7 @@ rule token = parse
intop ("i" ^ sz)
(memory_atomic_wait32 (opt a 2))
(memory_atomic_wait64 (opt a 3)) o) }
| "atomic.fence" { ATOMIC_FENCE }
| (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) }
Expand Down
3 changes: 2 additions & 1 deletion interpreter/text/parser.mly
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -169,7 +169,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 MEMORY_ATOMIC_WAIT MEMORY_ATOMIC_NOTIFY
%token MEMORY_ATOMIC_WAIT MEMORY_ATOMIC_NOTIFY ATOMIC_FENCE
%token ATOMIC_LOAD ATOMIC_STORE ATOMIC_RMW ATOMIC_RMW_CMPXCHG
%token CONST UNARY BINARY TEST COMPARE CONVERT
%token UNREACHABLE MEMORY_SIZE MEMORY_GROW
Expand Down Expand Up @@ -358,6 +358,7 @@ plain_instr :
| CONVERT { fun c -> $1 }
| 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_FENCE { fun c -> atomic_fence }
| 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 }
Expand Down
3 changes: 3 additions & 0 deletions interpreter/valid/valid.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -308,6 +308,9 @@ let rec check_instr (c : context) (e : instr) (s : infer_stack_type) : op_type =
check_memop c memop (fun sz -> sz) e.at;
[I32Type; memop.ty; I64Type] --> [I32Type]

| AtomicFence ->
[] --> []

| AtomicLoad memop ->
check_memop c memop (fun sz -> sz) e.at;
[I32Type] --> [memop.ty]
Expand Down
52 changes: 52 additions & 0 deletions test/core/atomic.wast
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -417,6 +417,7 @@
(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)

Expand All @@ -431,10 +432,54 @@
)

(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)
Expand Down Expand Up @@ -488,6 +533,13 @@
(func (drop (i64.atomic.rmw32.cmpxchg_u (i32.const 0) (i64.const 0) (i64.const 0))))
)

;; atomic.fence: no memory is ok
(module
(func (export "fence") (atomic.fence))
)

(assert_return (invoke "fence"))

;; Fails with no memory
(assert_invalid (module (func (drop (memory.atomic.notify (i32.const 0) (i32.const 0))))) "unknown memory")
(assert_invalid (module (func (drop (memory.atomic.wait32 (i32.const 0) (i32.const 0) (i64.const 0))))) "unknown memory")
Expand Down