4 ms·

Compilers preserve semantics. That is part of their contract. Whether the output has instructions in one order or another does not matter as long as the output

Compilers preserve semantics. That is part of their contract. Whether the output has instructions in one order or another does not matter as long as the output is observationally/functionally equivalent. Article does not do a good job of actually explaining this & instead meanders around sources of irrelevant "stochasticity" like timestamps & build-time UUIDs & concludes by claiming that LLMs have solved the halting problem.

markatto 8mo ago
It matters for things like verifiable builds.
- measurablefunc 8mo ago
  You have to specify what exactly you're verifying.
- adonovan 8mo ago
  Full determinism is also highly prized by compiler writers because it massively simplifies the task of reproducing and debugging problematic executions.
fragmede 8mo ago
Thank you for reading! I wrote "We have not remotely solved the halting problem in the formal sense", which does not read like a claim that LLMs have solved the halting problem to me, but I'm open to rewording it. How would you put it? I added in a bit about compiler contract, wdyt?
- measurablefunc 8mo ago
  We haven't solve it in the formal sense b/c it is formally unsolvable so hedging adds no semantic content. It's not a formal article so you can phrase things however you want but an uncritical reading will leave the reader confused about what exactly you were trying to explain.
Findecanor 8mo ago
C and C++ compilers are limited to preserving semantics for data-race free code only, though. They are allowed to turn a single load into multiple loads, or even a store into multiple stores: things that won't affect anything if you have only one thread accessing memory but for multithreaded programs, changing compiler or just making seemingly unrelated changes and recompiling can make existing data-race bugs have effects or not. Attempting to get consistent results from floating-point code is another rabbit hole. GCC and clang have various flags for "fast math" which can enable different optimisations that reduce precision. Before SSE, fp on x86 was done by the "x87" FPU which always had 80-bit precision, even if the type in the source code was 32 or 64 bits — and it used to be accepted to sometimes get more precision than asked for. Java got its "strictfp" mode mainly because of x87.
- measurablefunc 8mo ago
  Data races are undefined behavior¹ so in that case the compiler is still technically preserving semantics but if you use the proper primitives to remove undefined behavior (atomic operations, locks) for any shared state then the compiler will not generate code w/ undefined behavior & all modifications/mutations will be serialized in some order. You can then further refine the code if you want the operations to happen in a certain order. At the end of the day you must assume that the compiler will preserve your intended semantics otherwise we'd still be writing assembly b/c no high level specification would ever mean what it was intended to mean for the low-level executable machine model/target of the compiler. ¹https://cppreference.com/w/cpp/language/multithread.html https://cppreference.com/w/cpp/language/multithread.html
  - Findecanor 8mo ago
    Yes, but the spooky thing is still that the code with the bug and the code affected by a change in the compiler that triggers the effect of the bug could be in two different code modules.
- wakawaka28 8mo ago
  Runtime semantics are different from output semantics. You can build a nondeterministic program with a deterministic compiler, and the bytes of that program should be identical every time (notwithstanding the stupid metadata that most compilers inject, which is not semantically relevant).

markatto 8mo ago

It matters for things like verifiable builds.

measurablefunc 8mo ago
You have to specify what exactly you're verifying.
adonovan 8mo ago
Full determinism is also highly prized by compiler writers because it massively simplifies the task of reproducing and debugging problematic executions.

fragmede 8mo ago

Thank you for reading! I wrote "We have not remotely solved the halting problem in the formal sense", which does not read like a claim that LLMs have solved the halting problem to me, but I'm open to rewording it. How would you put it? I added in a bit about compiler contract, wdyt?

measurablefunc 8mo ago
We haven't solve it in the formal sense b/c it is formally unsolvable so hedging adds no semantic content. It's not a formal article so you can phrase things however you want but an uncritical reading will leave the reader confused about what exactly you were trying to explain.

Findecanor 8mo ago

C and C++ compilers are limited to preserving semantics for data-race free code only, though. They are allowed to turn a single load into multiple loads, or even a store into multiple stores: things that won't affect anything if you have only one thread accessing memory but for multithreaded programs, changing compiler or just making seemingly unrelated changes and recompiling can make existing data-race bugs have effects or not. Attempting to get consistent results from floating-point code is another rabbit hole. GCC and clang have various flags for "fast math" which can enable different optimisations that reduce precision. Before SSE, fp on x86 was done by the "x87" FPU which always had 80-bit precision, even if the type in the source code was 32 or 64 bits — and it used to be accepted to sometimes get more precision than asked for. Java got its "strictfp" mode mainly because of x87.

measurablefunc 8mo ago
Data races are undefined behavior¹ so in that case the compiler is still technically preserving semantics but if you use the proper primitives to remove undefined behavior (atomic operations, locks) for any shared state then the compiler will not generate code w/ undefined behavior & all modifications/mutations will be serialized in some order. You can then further refine the code if you want the operations to happen in a certain order. At the end of the day you must assume that the compiler will preserve your intended semantics otherwise we'd still be writing assembly b/c no high level specification would ever mean what it was intended to mean for the low-level executable machine model/target of the compiler. ¹https://cppreference.com/w/cpp/language/multithread.html https://cppreference.com/w/cpp/language/multithread.html
- Findecanor 8mo ago
  Yes, but the spooky thing is still that the code with the bug and the code affected by a change in the compiler that triggers the effect of the bug could be in two different code modules.
wakawaka28 8mo ago
Runtime semantics are different from output semantics. You can build a nondeterministic program with a deterministic compiler, and the bytes of that program should be identical every time (notwithstanding the stupid metadata that most compilers inject, which is not semantically relevant).