Message-ID: <7edf8624-c9a0-4d8d-a09e-2eac55dc6fc5@ralfj.de>
Date: Wed, 26 Feb 2025 23:28:20 +0100
From: Ralf Jung <post@...fj.de>
To: Ventura Jack <venturajack85@...il.com>
Cc: Kent Overstreet <kent.overstreet@...ux.dev>,
 Miguel Ojeda <miguel.ojeda.sandonis@...il.com>, Gary Guo <gary@...yguo.net>,
 torvalds@...ux-foundation.org, airlied@...il.com, boqun.feng@...il.com,
 david.laight.linux@...il.com, ej@...i.de, gregkh@...uxfoundation.org,
 hch@...radead.org, hpa@...or.com, ksummit@...ts.linux.dev,
 linux-kernel@...r.kernel.org, rust-for-linux@...r.kernel.org
Subject: Re: C aggregate passing (Rust kernel policy)

Hi all,

On 26.02.25 19:09, Ventura Jack wrote:
> On Wed, Feb 26, 2025 at 9:32 AM Ralf Jung <post@...fj.de> wrote:
>>
>> Hi VJ,
>>
>>>>
>>>>> - Rust has not defined its aliasing model.
>>>>
>>>> Correct. But then, neither has C. The C aliasing rules are described in English
>>>> prose that is prone to ambiguities and misintepretation. The strict aliasing
>>>> analysis implemented in GCC is not compatible with how most people read the
>>>> standard (https://bugs.llvm.org/show_bug.cgi?id=21725). There is no tool to
>>>> check whether code follows the C aliasing rules, and due to the aforementioned
>>>> ambiguities it would be hard to write such a tool and be sure it interprets the
>>>> standard the same way compilers do.
>>>>
>>>> For Rust, we at least have two candidate models that are defined in full
>>>> mathematical rigor, and a tool that is widely used in the community, ensuring
>>>> the models match realistic use of Rust.
>>>
>>> But it is much more significant for Rust than for C, at least in
>>> regards to C's "restrict", since "restrict" is rarely used in C, while
>>> aliasing optimizations are pervasive in Rust. For C's "strict aliasing",
>>> I think you have a good point, but "strict aliasing" is still easier to
>>> reason about in my opinion than C's "restrict". Especially if you
>>> never have any type casts of any kind nor union type punning.
>>
>> Is it easier to reason about? At least GCC got it wrong, making no-aliasing
>> assumptions that are not justified by most people's interpretation of the model:
>> https://bugs.llvm.org/show_bug.cgi?id=21725
>> (But yes that does involve unions.)
> 
> For that specific bug issue, there is a GitHub issue for it.
> 
>      https://github.com/llvm/llvm-project/issues/22099

Yeah sorry this was an LLVM issue, not a GCC issue. I mixed things up.

> And the original test case appears to have been a compiler bug
> and have been fixed, at least when I run on Godbolt against
> a recent version of Clang. Another comment says.
> 
>      "The original testcase seems to be fixed now but replacing
>      the union by allocated memory makes the problem come back."
> 
> And the new test case the user mentions involves a void pointer.
> 
> I wonder if they could close the issue and open a new issue
> in its stead that only contains the currently relevant compiler
> bugs if there are any. And have this new issue refer to the old
> issue. They brought the old issue over from the old bug tracker.
> But I do not have a good handle on that issue.
> 
> Unions in C, C++ and Rust (not Rust "enum"/tagged union) are
> generally sharp. In Rust, it requires unsafe Rust to read from
> a union.

Definitely sharp. At least in Rust we have a very clear specification though, 
since we do allow arbitrary type punning -- you "just" reinterpret whatever 
bytes are stored in the union, at whatever type you are reading things. There is 
also no "active variant" or anything like that, you can use any variant at any 
time, as long as the bytes are "valid" for the variant you are using. (So for 
instance if you are trying to read a value 0x03 at type `bool`, that is UB.)
I think this means we have strictly less UB here than C or C++, removing as many 
of the sharp edges as we can without impacting the rest of the language.

>> In contrast, Miri checks for all the UB that is used anywhere in the Rust
>> compiler -- everything else would be a critical bug in either Miri or the compiler.
>> But yes, it only does so on the code paths you are actually testing. And yes, it
>> is very slow.
> 
> I may have been ambiguous again, or unclear or misleading,
> I need to work on that.
> 
> The description you have here indicates that Miri is in many ways
> significantly better than sanitizers in general.
> 
> I think it is more accurate of me to say that Miri in some aspects
> shares some of the advantages and disadvantages of sanitizers,
> and in other aspects is much better than sanitizers.

I can agree with that. :)

> Is Miri the only one of its kind in the programming world?
> There are not many system languages in mass use, and
> those are the languages that first and foremost deal
> with undefined behavior. That would make Miri extra impressive.

I am not aware of a comparable tool that would be in wide-spread use, or that is 
carefully aligned with the semantics of an actual compiler.
For C, there is Cerberus (https://www.cl.cam.ac.uk/~pes20/cerberus/) as an 
executable version of the C specification, but it can only run tiny examples.
The verified CompCert compiler comes with a semantics one could interpret, but 
that only checks code for compatibility with CompCert C, which has a lot less 
(and a bit more) UB than real C.
There are also two efforts that turned into commercial tools that I have not 
tried, and for which there is hardly any documentation of how they interpret the 
C standard so it's not clear what a green light from them means when compiling 
with gcc or clang. I also don't know how much real-world code they can actually run.
- TrustInSoft/tis-interpreter, mostly gone from the web but still available in 
the wayback machine 
(https://web.archive.org/web/20200804061411/https://github.com/TrustInSoft/tis-interpreter/); 
I assume this got integrated into their "TrustInSoft Analyzer" product.
- kcc, a K-framework based formalization of C that is executable. The public 
repo is dead (https://github.com/kframework/c-semantics) and when I tried to 
build their tool that didn't work. The people behind this have a company that 
offers "RV-Match" as a commercial product claiming to find bugs in C based on "a 
complete formal ISO C11 semantics" so I guess that is where their efforts go now.

For C++ and Zig, I am not aware of anything comparable.

Part of the problem is that in C, 2 people will have 3 ideas for what the 
standard means. Compiler writers and programmers regularly have wildly 
conflicting ideas of what is and is not allowed. There are many different places 
in the standard that have to be scanned to answer "is this well-defined" even 
for very simple programs. (https://godbolt.org/z/rjaWc6EzG is one of my favorite 
examples.) A tool can check a single well-defined semantics, but who gets to 
decide what exactly those semantics are?
Formalizing the C standard requires extensive interpretation, so I am skeptical 
of everyone who claims that they "formalized the C standard" and built a tool on 
that without extensive evaluation of how their formalization compares to what 
compilers do and what programmers rely on. The Cerberus people have done that 
evaluation (see e.g. https://dl.acm.org/doi/10.1145/2980983.2908081), but none 
of the other efforts have (to my knowledge). Ideally such a formalization effort 
would be done in close collaboration with compiler authors and the committee so 
that the ambiguities in the standard can be resolved and the formalization 
becomes the one canonical interpretation. The Cerberus people are the ones that 
pushed the C provenance formalization through, so they made great progress here. 
However, many issues remain, some quite long-standing (e.g. 
https://www.open-std.org/jtc1/sc22/wg14/www/docs/dr_260.htm and 
https://www.open-std.org/jtc1/sc22/wg14/www/docs/dr_451.htm, which in my eyes 
never got properly resolved by clarifying the standard). Martin and a few others 
are slowly pushing things in the right direction, but it takes a long time. 
Rust, by having a single project in charge of the one canonical implementation 
and the specification, and having an open process that is well-suited for 
incorporating user concerns, can move a lot quicker here. C has a huge 
head-start, Rust has nothing like the C standard, but we are catching up -- and 
our goal is more ambitious than that; we are doing our best to learn from C and 
C++ and concluded that that style of specification is too prone to ambiguity, so 
we are trying to achieve a formally precise unambiguous specification. Wasm 
shows that this can be done, at industry scale, albeit for a small language -- 
time we do it for a large one. :)

So, yes I think Miri is fairly unique. But please let me know if I missed something!

(As an aside, the above hopefully also explains why some people in Rust are 
concerned about alternative implementations. We do *not* want the current 
de-factor behavior to ossify and become the specification. We do *not* want the 
specification to just be a description of what the existing implementations at 
the time happen to do, and declare all behavior differences to be UB or 
unspecified or so just because no implementation is willing to adjust their 
behavior to match the rest. We want the specification to be prescriptive, not 
descriptive, and we will adjust the implementation as we see fit to achieve that 
-- within the scope of Rust's stability guarantees. That's also why we are so 
cagey about spelling out the aliasing rules until we are sure we have a good 
enough model.)

> There are some issues in Rust that I am curious as to
> your views on. rustc or the Rust language has some type
> system holes, which still causes problems for rustc and
> their developers.
> 
>      https://github.com/lcnr/solver-woes/issues/1
>      https://github.com/rust-lang/rust/issues/75992
> 
> Those kinds of issues seem difficult to solve.
> 
> In your opinion, is it accurate to say that the Rust language
> developers are working on a new type system for
> Rust-the-language and a new solver for rustc, and that
> they are trying to make the new type system and new solver
> as backwards compatible as possible?

It's not really a new type system. It's a new implementation for the same type 
system. But yes there is work on a new "solver" (that I am not involved in) that 
should finally fix some of the long-standing type system bugs. Specifically, 
this is a "trait solver", i.e. it is the component responsible for dealing with 
trait constraints. Due to some unfortunate corner-case behaviors of the old, 
organically grown solver, it's very hard to do this in a backwards-compatible 
way, but we have infrastructure for extensive ecosystem-wide testing to judge 
the consequences of any given potential breaking change and ensure that almost 
all existing code keeps working. In fact, Rust 1.84 already started using the 
new solver for some things 
(https://blog.rust-lang.org/2025/01/09/Rust-1.84.0.html) -- did you notice? 
Hopefully not. :)

Kind regards,
Ralf

Powered by blists - more mailing lists