Many safety issues in complex compute environments are predicated on the notion that many different threads/contexts can manipulate the data structures in somewhat arbitrary and unpredictable orders. This is approximately correct for classic multithreaded software.

In some software architectures, there are schedulers with a global view of the entire (potential) conflict graph and they have complete control of what gets executed when. These architectures don’t even require locks because the scheduler has enough visibility and control to guarantee that execution won’t be scheduled such that there would ever be a contended lock or some other concurrency conflict. No amount of mutable references to the same memory will break these models, and the correctness of some implementations have been formally verified. The scheduler can always dynamically reorder execution to guarantee the invariants of the system. These models have the added benefit of having insanely good locality properties such that throughput is excellent.

These software architectures originated in HPC over a decade ago and eventually bled over into high-end database kernels. I learned it from when I worked in HPC many years ago and have used it every since, due to its unambiguous advantages.

Thanks! Sounds interesting, but it's not obvious to me that such a framework can't be captured in the Rust type/ownership system in a reasonably ergonomic way. Has anyone even tried doing that?

For example you might be able to wrap shared-mutable state in a kind of degenerate mutex and pass a "scheduler guarantee" token around that unlocks those "mutexes" without doing any runtime work.

Do you have any references to HPC systems that exemplify this approach?