Vitte

Parallel Borrow Analysis (174)

Objective: make borrowck compatible with parallelism.

Contracts

  • Send equivalent:
  • a value moved to a thread context must be transferable without a concurrent mutable alias.
  • Sync equivalent:
  • any cross-threaded mutable shared access must be explicitly synchronized.
  • Shared mutation:
  • concurrent shared resource mutation without lock/atomic is rejected.
  • Thread ownership:
  • a mutable reference must not escape from its logical owner to a concurrent thread.

Foundation diagnostics

  • BORROWCK_E_PARALLEL_SEND_VIOLATION
  • BORROWCK_E_PARALLEL_SYNC_VIOLATION
  • BORROWCK_E_SHARED_MUTATION_ACROSS_THREADS
  • BORROWCK_E_THREAD_OWNERSHIP_VIOLATION
  • BORROWCK_E_CONCURRENCY_RACE_RISK

Current implementation

  • Heuristic analysis of thread/send/sync/race patterns from HIR statements.
  • Merger of diagnostics with the existing borrowck (ownership/moves/loans/lifetimes).