E4014

Error · Borrow/Ownership

E4014 — A task that can still run when a variable that it uses ends or changes. A task in a loop that the same pass does not join runs at the same time as the next pass, so it must not write a variable from outside the loop, or read one that the loop writes. A task must not use a variable that ends before its tasks block, such as one of the loop body. Join the task in the same block: let h = spawn { .. }; and then h.join();.

What the compiler reports

Error[E4014] at [[@LINE+4]]:5: a task that this loop starts writes 'x'
Error[E4014] at [[@LINE+4]]:5: a task that this loop starts reads 'v'
Error[E4001] at [[@LINE+9]]:16: Use of moved or consumed linear variable: v
Error[E4014] at [[@LINE+6]]:7: the task uses 'r', which points at 'n', but 'n' ends before its `tasks` block does
Error[E4001] at [[@LINE+9]]:15: Use of moved or consumed linear variable: v
Error[E3055] at [[@LINE+4]]:5: the task reads 'c', which the code around the task can read at the same time, so its type 'SharedCell<i32>' must be `Sync`: 'SharedCell<i32>' is never `Sync`
Error[E3055] at [[@LINE+5]]:5: the task copies 'p' into itself, so its type '*mut i32' must be `Send`: '*mut i32' is a raw pointer, which is not `Send`
{{^}}Semantic check failed on {{.*}}: 10 error(s) emitted

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
//
//
// A task runs at the same time as the code after its `spawn`, until its `join()` or the end of
// its `tasks` block. It holds each variable that it writes, and each one that it reads and does
// not copy, for that time. A task in a loop also runs at the same time as the next pass.
//
// A task that writes a value, or moves it into itself, needs the value to be `Send`. A task that
// reads a variable in place needs it to be `Sync`.

import core::cell;
import std::vec;

fn read_while_a_task_writes() -> i32 {
  let mut x = 0;
  tasks {
    spawn {
      x += 1;
    };
    let y = x;
  }
  return x;
}

fn two_tasks_write() -> i32 {
  let mut x = 0;
  tasks {
    spawn {
      x += 1;
    };
    spawn {
      x += 2;
    };
  }
  return x;
}

fn change_what_a_task_reads() -> i32 {
  let mut v = Vec<i32>::new();
  tasks {
    let h = spawn {
      v.len()
    };
    v = Vec<i32>::new();
    h.join();
  }
  return 0;
}

fn task_in_a_loop_writes() -> i32 {
  let mut x = 0;
  tasks {
    for i in 0..4 {
      spawn {
        x += i;
      };
    }
  }
  return x;
}

fn loop_changes_what_a_task_reads() -> void {
  let mut v = Vec<i32>::new();
  tasks {
    for i in 0..3 {
      v.push(i);
      spawn {
        v.len();
      };
    }
  }
}

// A task moves `v`, because `v` ends before the task's join. So the pass cannot use `v` again.
fn use_a_local_that_a_task_moved() -> void {
  tasks {
    for i in 0..3 {
      let mut v = Vec<i32>::new();
      v.push(i);
      spawn {
        v.len();
      };
      let _w = v;
    }
  }
}

fn task_outlives_what_a_reference_points_at() -> void {
  tasks {
    for i in 0..3 {
      let n = i;
      let r = &n;
      spawn {
        *r;
      };
    }
  }
}

fn use_after_moving_into_a_task() -> i32 {
  let v = Vec<i32>::new();
  tasks {
    spawn {
      let w = v;
      w.len();
    };
  }
  let again = v;
  return 0;
}

fn share_a_shared_cell() -> void {
  let c = SharedCell<i32>::new(1);
  tasks {
    spawn {
      c.get();
    };
  }
}

fn copy_a_raw_pointer() -> i32 {
  let mut x = 0;
  let p = (&mut x) as *mut i32;
  tasks {
    spawn {
      unsafe { *p = 1; }
    };
  }
  return x;
}

fn main() -> i32 {
  return 0;
}

// The errors above are all the errors.

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

Related