E8007

Error · Contract/Verification

E8007 — An atomic(t) clause that does not name a tensor, or a body that uses that tensor without an atomic operation

What the compiler reports

Error[E8007] at 51:{{.*}}`atomic(u)` names no parameter of `names_no_parameter`
Error[E8007] at 57:{{.*}}`atomic(t)` must name a `&` tensor of `i32`, `u32`, `i64`, `u64` or `f32`, but `t` is `&mut Tensor<i32, [?], Memory::HBM>`
Error[E8007] at 63:{{.*}}`atomic(t)` must name a `&` tensor{{.*}} but `t` is `i32`
Error[E8007] at 69:{{.*}}`atomic` takes one parameter of `names_two_things`
Error[E8007] at 77:{{.*}}`reads_an_element` says `atomic(t)`, so it may use `t` only in an atomic operation
Error[E8007] at 83:{{.*}}`passes_it_to_a_block_without_a_clause` says `atomic(t)`
Error[E8007] at 94:{{.*}}`passes_it_to_a_function_without_a_contract` says `atomic(t)`
Error[E8007] at 98:{{.*}}an `atomic` clause of an `mlir!` block names one of its inputs
Error[E8007] at 104:{{.*}}the block says `atomic(t)`, but `%v = memref.load %t[%k] : memref<?xi32>` reads or writes `%t` without an atomic operation
Error[E8007] at 112:{{.*}}`memref.store %i, %u[%k] : memref<?xi32>` writes `%u`, which the clauses of the block do not name
Error[E6032] at 124:{{.*}}the passes of this block loop change `count` with atomic operations, so every access to it in the loop must be one
Error[E6032] at 135:{{.*}}the call to `add_one_plain` may write through an argument

The fragments the test suite holds the compiler to. An ellipsis marks text the test does not constrain; the emitted message also carries a source location.

A program that triggers it

//
// Part of the Vx Project, under the Apache License v2.0 with LLVM Exceptions.
// See LICENSE for license information.
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
//
// `ensures atomic(t)` says that a function uses the elements of the tensor `t` only in atomic
// operations. The first functions break the contract or name the wrong thing (E8007). The
// kernels at the end use an atomic tensor in an `across` loop without an atomic operation, or
// call a function that has no contract (E6032).
//

// A correct contract, for the kernels below.
fn add_one(t : &Tensor<i32, [?], Memory::HBM>, i : i32) on Topology::Device -> i32
ensures atomic(t)
{
  return mlir!( inputs : (%t = t : memref<?xi32>, %i = i : i32), returns : i32, dialects : ["memref", "arith"], ensures : [atomic(t)]) {
    %k = arith.index_cast %i : i32 to index
    %one = arith.constant 1 : i32
    %old = memref.atomic_rmw addi %one, %t[%k] : (i32, memref<?xi32>) -> i32
    macro.yield %old : i32
  };
}

// The same function with no contract.
fn add_one_plain(t : &Tensor<i32, [?], Memory::HBM>, i : i32) on Topology::Device -> i32 {
  return mlir!( inputs : (%t = t : memref<?xi32>, %i = i : i32), returns : i32, dialects : ["memref", "arith"]) {
    %k = arith.index_cast %i : i32 to index
    %one = arith.constant 1 : i32
    %old = memref.atomic_rmw addi %one, %t[%k] : (i32, memref<?xi32>) -> i32
    macro.yield %old : i32
  };
}

fn names_no_parameter(t : &Tensor<i32, [?], Memory::HBM>) on Topology::Device -> i32
ensures atomic(u)
{
  return 0;
}

fn names_a_mut_tensor(t : &mut Tensor<i32, [?], Memory::HBM>) on Topology::Device -> i32
ensures atomic(t)
{
  return 0;
}

fn names_a_scalar(t : i32) on Topology::Device -> i32
ensures atomic(t)
{
  return t;
}

fn names_two_things(t : &Tensor<i32, [?], Memory::HBM>, u : &Tensor<i32, [?], Memory::HBM>) on Topology::Device -> i32
ensures atomic(t, u)
{
  return 0;
}

fn reads_an_element(t : &Tensor<i32, [?], Memory::HBM>, i : i32) on Topology::Device -> i32
ensures atomic(t)
{
  return t[i];
}

fn passes_it_to_a_block_without_a_clause(t : &Tensor<i32, [?], Memory::HBM>, i : i32) on Topology::Device -> i32
ensures atomic(t)
{
  return mlir!( inputs : (%t = t : memref<?xi32>, %i = i : i32), returns : i32, dialects : ["memref", "arith"]) {
    %k = arith.index_cast %i : i32 to index
    %one = arith.constant 1 : i32
    %old = memref.atomic_rmw addi %one, %t[%k] : (i32, memref<?xi32>) -> i32
    macro.yield %old : i32
  };
}

fn passes_it_to_a_function_without_a_contract(t : &Tensor<i32, [?], Memory::HBM>, i : i32) on Topology::Device -> i32
ensures atomic(t)
{
  return add_one_plain(t, i);
}

fn block_names_no_input(t : &Tensor<i32, [?], Memory::HBM>, i : i32) on Topology::Device -> i32 {
  return mlir!( inputs : (%i = i : i32), returns : i32, dialects : ["arith"], ensures : [atomic(t)]) {
    macro.yield %i : i32
  };
}

fn block_loads_the_atomic_tensor(t : &Tensor<i32, [?], Memory::HBM>, i : i32) on Topology::Device -> i32 {
  return mlir!( inputs : (%t = t : memref<?xi32>, %i = i : i32), returns : i32, dialects : ["memref", "arith"], ensures : [atomic(t)]) {
    %k = arith.index_cast %i : i32 to index
    %v = memref.load %t[%k] : memref<?xi32>
    macro.yield %v : i32
  };
}

fn block_writes_a_tensor_it_does_not_name(t : &Tensor<i32, [?], Memory::HBM>, u : &Tensor<i32, [?], Memory::HBM>, i : i32) on Topology::Device -> i32 {
  return mlir!( inputs : (%t = t : memref<?xi32>, %u = u : memref<?xi32>, %i = i : i32), returns : i32, dialects : ["memref", "arith"], ensures : [atomic(t)]) {
    %k = arith.index_cast %i : i32 to index
    memref.store %i, %u[%k] : memref<?xi32>
    macro.yield %i : i32
  };
}

pub fn reads_the_counter_in_the_loop(count : &Tensor<i32, [?], Memory::HBM>, out : &mut Tensor<i32, [?], Memory::HBM>) -> void {
  spawn on(Topology::Device) {
    for b in 0..4 across blocks {
      for l in 0..32 across lanes {
        let _old = add_one(count, 0);
        out[b * 32 + l] = count[0];
      }
    }
  }
  return;
}

pub fn calls_a_function_without_a_contract(count : &Tensor<i32, [?], Memory::HBM>) -> void {
  spawn on(Topology::Device) {
    for b in 0..4 across blocks {
      for l in 0..32 across lanes {
        let _old = add_one_plain(count, 0);
      }
    }
  }
  return;
}

From tests/frontend/fail/atomic_contracts_that_do_not_hold.vx, which asserts this diagnostic on every commit.

Related