Specification
In addition to alias hazards, lowering materializes the sequenced-before rules
from the actor contracts:
- atomic actors and fences in one logical source strand preserve their
selected order;
- volatile actors in one logical source strand preserve their relative order;
- release actors and fences wait for prior memory-effect tails whose
visibility they publish;
- acquire actors and fences precede later constrained memory effects;
acq_rel and seq_cst apply both directions; and
- atomic-volatile actors participate in both strand relations.
|
In addition to alias hazards, lowering materializes the sequenced-before rules |
|
from the actor contracts: |
|
|
|
* atomic actors and fences in one logical source strand preserve their |
|
selected order; |
|
* volatile actors in one logical source strand preserve their relative order; |
|
* release actors and fences wait for prior memory-effect tails whose |
|
visibility they publish; |
|
* acquire actors and fences precede later constrained memory effects; |
|
* `acq_rel` and `seq_cst` apply both directions; and |
|
* atomic-volatile actors participate in both strand relations. |
A test that follows it, and fails at 289b7fa4
Three graphs, one per rule: two volatile loads of one address, an acquire
load followed by a volatile load of another memref, and two seq_cst loads.
In each, the second actor is sequenced after the first by the list above, so
it may not take the graph entry token as its control. It has to wait for the
first actor's done, directly or through dataflow.sync.
// RUN: loom-raise-opt --loom-lower-graph-memory %s | FileCheck %s
// docs/spec-compiler-part-3-mem.md: graph memory lowering materializes the
// sequenced-before rules from the actor contracts, not only the alias hazards.
// After the first constrained actor in each graph, no later memory actor may
// take the graph entry token as its control: it has to wait, directly or
// through dataflow.sync, for the done of the actor it is sequenced after.
// Volatile actors in one logical source strand preserve their relative order.
// CHECK-LABEL: dataflow.graph private @volatile_pair(
// CHECK-SAME: %[[START:[^:]+]]: none
// CHECK: dataflow.load {{.*}} %[[START]] {contract = #dataflow.plain_access<is_volatile = true>}
// CHECK-NOT: %[[START]] {contract
// CHECK: dataflow.graph.return
dataflow.graph private @volatile_pair(
%start: none, %idx: index, %a: memref<16xf32>) -> ()
attributes {input_segments = array<i32: 1, 0, 1>,
result_segments = array<i32: 0, 0, 0>} {
%v0, %d0 = dataflow.load %a[%idx] %start {contract = #dataflow.plain_access<is_volatile = true>} : memref<16xf32>
%v1, %d1 = dataflow.load %a[%idx] %start {contract = #dataflow.plain_access<is_volatile = true>} : memref<16xf32>
dataflow.graph.return %start : none
}
// Acquire actors precede later constrained memory effects.
// CHECK-LABEL: dataflow.graph private @acquire_then_load(
// CHECK-SAME: %[[START:[^:]+]]: none
// CHECK: dataflow.load {{.*}} %[[START]] {contract = #dataflow.atomic_access<ordering = acquire
// CHECK-NOT: %[[START]] {contract
// CHECK: dataflow.graph.return
dataflow.graph private @acquire_then_load(
%start: none, %idx: index, %flag: memref<16xi32>, %data: memref<16xi32>) -> ()
attributes {input_segments = array<i32: 1, 0, 2>,
result_segments = array<i32: 0, 0, 0>} {
%f, %fd = dataflow.load %flag[%idx] %start {contract = #dataflow.atomic_access<ordering = acquire, sync_scope = <system>, source_alignment_bytes = 4>} : memref<16xi32>
%v, %vd = dataflow.load %data[%idx] %start {contract = #dataflow.plain_access<is_volatile = true>} : memref<16xi32>
dataflow.graph.return %start : none
}
// Atomic actors in one logical source strand preserve their selected order.
// CHECK-LABEL: dataflow.graph private @atomic_load_pair(
// CHECK-SAME: %[[START:[^:]+]]: none
// CHECK: dataflow.load {{.*}} %[[START]] {contract = #dataflow.atomic_access<ordering = seq_cst
// CHECK-NOT: %[[START]] {contract
// CHECK: dataflow.graph.return
dataflow.graph private @atomic_load_pair(
%start: none, %idx: index, %a: memref<16xi32>) -> ()
attributes {input_segments = array<i32: 1, 0, 1>,
result_segments = array<i32: 0, 0, 0>} {
%r0, %d0 = dataflow.load %a[%idx] %start {contract = #dataflow.atomic_access<ordering = seq_cst, sync_scope = <system>, source_alignment_bytes = 4>} : memref<16xi32>
%r1, %d1 = dataflow.load %a[%idx] %start {contract = #dataflow.atomic_access<ordering = seq_cst, sync_scope = <system>, source_alignment_bytes = 4>} : memref<16xi32>
dataflow.graph.return %start : none
}
At 289b7fa4 every second load takes the entry token, and the two done
tokens meet only in the retirement dataflow.sync:
%data, %done = dataflow.load %arg2[%arg1] %arg0 {contract = #dataflow.plain_access<is_volatile = true>} : memref<16xf32>
%data_0, %done_1 = dataflow.load %arg2[%arg1] %arg0 {contract = #dataflow.plain_access<is_volatile = true>} : memref<16xf32>
%0:2 = dataflow.sync %done, %done_1 : (none, none) -> (none, none)
issue-graph-memory-sequenced-before.mlir:13:15: error: CHECK-NOT: excluded string found in input
// CHECK-NOT: %[[START]] {contract
The same error is reported for the acquire graph and the atomic graph. The
LLVM-level forms (llvm.load volatile, llvm.load atomic acquire) through
--loom-lower-scf-to-dfg give the same control edges.
Specification
loom/docs/spec-compiler-part-3-mem.md
Lines 228 to 238 in 289b7fa
A test that follows it, and fails at
289b7fa4Three graphs, one per rule: two volatile loads of one address, an acquire
load followed by a volatile load of another memref, and two
seq_cstloads.In each, the second actor is sequenced after the first by the list above, so
it may not take the graph entry token as its control. It has to wait for the
first actor's
done, directly or throughdataflow.sync.At
289b7fa4every second load takes the entry token, and the twodonetokens meet only in the retirement
dataflow.sync:The same error is reported for the acquire graph and the atomic graph. The
LLVM-level forms (
llvm.load volatile,llvm.load atomic acquire) through--loom-lower-scf-to-dfggive the same control edges.