What memory model should Rust use?

Relegating parts of the memory model with unclear&#x2F;hard-to-specify semantics (i.e. relaxed or consume) to the &quot;unsafe&quot; part of the language is an interesting idea, but it kind of goes against the spirit of &quot;unsafe&quot; (this point is debatable, of course).<p>The purpose of the unsafe keyword is to mark code that could cause safety issues (undefined behavior) if its expectations about the surrounding code are not met. (e.g., an unchecked array access expects its index to be in bounds).<p>With unlimited time and resources, it should be possible to give a mathematical proof about those unsafe blocks, showing that their expectations are met and that undefined behavior will not actually occur (by for example proving that the array index supplied will always be in bounds).<p>But since relaxed and consume have unclear semantics, it hard to formally reason about the correctness of any code that uses them (and it is also hard to build tools to do that checking, as mentioned).<p>So in an ideal world, we would have a 100% clear semantics for all parts of the language, _including_ the unsafe fragment. Unsafe should not be a place to put poorly specified languages features.<p>Of course, we don&#x27;t live in this ideal world, but I would rather hope for fixing the memory model so that it be made completely formal and precise (if necessary, giving up some currently allowed compiler&#x2F;hardware optimizations if they&#x27;re more trouble than they are worth). As an extreme example, sequential consistency is easy to understand as long as you don&#x27;t mix it with other types of atomic accesses and avoid non-atomic data races.

So many thoughts.<p>* Rust threads run on CPU cores, but also GPU cores, FPGA cores, and a wider range of nastier hardware than Linux kernel threads run on.<p>* The author implies throughout the text that safe Rust operations might not be allowed in unsafe Rust. This hints at a deep misunderstanding of how Rust works.<p>* C, C++, and similar languages, do not have as a goal to be &quot;sound&quot;. Soundness is, however, core to Rust&#x27;s value proposition.<p>* C, C++, and similar languages, do not have the goal that undefined behavior must always trap in their abstract machines. But Rust does.<p>* C++ and similar languages do not have the goal of forever-backwards-compatibility (e.g. C++ breaks backwardward compatibility on almost every new standard release). Rust, however, guarantees that all programs written for Rust 1.0 in 2015 that have no undefined behavior will build and run correctly _forever_.<p>* Rust has many compiler backends, e.g., LLVM-IR, GCC, Cranelift, SPIR-V, etc. Rust code is translated to the IR of those toolchains. That is, those IRs would need to be extended with the new semantics as well to be useful.<p>&gt; But again, this decision rests not with me, but with the Rust communty.<p>The Rust community needs people working on formalizing the memory model further. So if they are interested, they should jump right in.<p>They should probably start by understanding Rust as is today, learning about unsafe code, and well the blog post cites <a href="https:&#x2F;&#x2F;plv.mpi-sws.org&#x2F;rustbelt&#x2F;rbrlx&#x2F;" rel="nofollow">https:&#x2F;&#x2F;plv.mpi-sws.org&#x2F;rustbelt&#x2F;rbrlx&#x2F;</a> , but it is clear from the exposition that the author has not deeply understood that paper, so maybe they should also take a deeper look at that. All the proofs are open-source. So if they think they can extend the soundness proofs with new features that are also sound, that could be a place to start.

I am woefully under-informed about the LKMM, but one useful comment I can contribute to this discussion is that the recommended strategy here would be extremely difficult to implement, because you can use both the relaxed and consume orderings in safe Rust today, and so making them unsafe would be a breaking change.<p>Furthermore, because they&#x27;re standard library constructs, they are not straightforward to change in an edition either.

I&#x27;m confused:<p>&quot;Inspired by the apparent success of Java&#x27;s new memory model, many of the same people set out to define a similar memory model for C++, eventually adopted in C++11.&quot; - <a href="https:&#x2F;&#x2F;research.swtch.com&#x2F;plmm" rel="nofollow">https:&#x2F;&#x2F;research.swtch.com&#x2F;plmm</a><p>&quot;Rust&#x27;s growing connection to the deep embedded world rules out the memory models of dynamic languages such as Java and Javascript.&quot;<p>So what is Rust using now, C++11 or C++20? &quot;memory model for atomics from C++20&quot;?!

I&#x27;d kill for a &quot;volatile&quot; with guaranteed semantics in Rust. Possibly more than one person.

&gt;Rust&#x27;s growing connection to the deep embedded world rules out the memory models of dynamic languages such as Java and Javascript.<p>Since when is Java a dynamic language?

What is a memory model?

The shallowness of rusts correctness has pretty much killed my interest in it.<p>Much of its purported virtue seems to be mostly lore and myth, and doesn&#x27;t keep its promises under close inspection and scrutiny.<p>For example the &quot;Rustonomicon&quot; is only half finished and doesn&#x27;t have that much real insight that couldn&#x27;t be gained from a lot of basic-ish rust tutorials.<p>The memory model is not propery defined and only kinda sorta borrowed from C++ as the article mentions.<p>The borrow checker has only been formally specified and veryfied in a much simplified form and only very recently [2] ,with the actual model &quot;just being what the borrow checker implementation does&quot;.<p>Having a fancy datalog based borrow checker is cool, but I&#x27;d much rather have a formal specifiation of the semantics.<p>Rust took the big bang approach of building everything at once, implementing stuff first without any formal semantics and just floating on an iceberg of implementation definedness, with endless discussions on how things COULD be formalized.<p>That&#x27;s pretty much the antithesis to rusts safety philosophy; it&#x27;s teaching water but drinking barrels of wine. It wants your code to be well defined and follow its rules, but its rules are completely arbitrary, not properly defined nor written down.<p>I wish instead they had just started with a small borrow checked core language, and grown it from there, like described in Guy Steeles talk on &quot;growing a language&quot; [1].<p>I feel that Zig is doing a much better job in this regard, they have a tiny well thoughought language with a rigorous semantic description, and a good reference document.<p>I&#x27;m sure it would be much easier to add a borrow checker to the well-defined-ness and correctness of Zig, than to make Rust well defined and correct.<p>Super friendly community though. Who knows, maybe someday the language that people think rust is, will crystalize from that community through their collective effort, like a self fulfilling prophecy.<p>1. <a href="https:&#x2F;&#x2F;m.youtube.com&#x2F;watch?v=lw6TaiXzHAE" rel="nofollow">https:&#x2F;&#x2F;m.youtube.com&#x2F;watch?v=lw6TaiXzHAE</a><p>2. <a href="https:&#x2F;&#x2F;arxiv.org&#x2F;pdf&#x2F;1903.00982.pdf" rel="nofollow">https:&#x2F;&#x2F;arxiv.org&#x2F;pdf&#x2F;1903.00982.pdf</a>

OTOH - TIL : LiveJournal.com still exists, even when giants such as Friendster, MySpace, Google Plus #cough have perished. Awesome.

I’m but a mere mortal but as an outside observer of rust and from my playing around with it, doesn’t the borrow checker currently handle this for you? Ie part of fearless concurrency?

What history model is that site using?