3 ms·

I grilled an LLM for a bit to see if it could justify the old forward progress rule. The only thing I got that passed the smell test was that it’s useful for th

by amluto 13d ago

I grilled an LLM for a bit to see if it could justify the old forward progress rule. The only thing I got that passed the smell test was that it’s useful for the optimizer to be able to optimize: messy_pure_computation(); some_atomic.store(1, relaxed); by moving the store before the computation. (Stronger stores would require additional analysis.) I admit I’m unconvinced that this is particularly useful. (I got many other ideas that did not pass my personal smell test.)

raphlinus 13d ago
You will find the answer you seek not from an LLM, but from the talk Forward Progress Guarantees in C++ by Olivier Giroux at CppNow 2023. It's a long talk, with lots of details about forward progress, but I've set the timestamp[1] to the infinite loop bit. [1]: https://youtu.be/g9Rgu6YEuqY?si=_l9JwKhjvIdFEDEX&t=3819 https://youtu.be/g9Rgu6YEuqY?si=_l9JwKhjvIdFEDEX&t=3819
- amluto 12d ago
  I don’t really buy that justification, for three reasons: 1. Most implementations do not do this automatic cooperative multitasking trick and most users [0] don’t want it done to their code. 2. The fact that a “step” is guaranteed to happen in finite time is far too weak for most use cases. I’ve done plenty of kernel programming, and a lot of kernels are partially or fully cooperative scheduled. Even somewhat long loops need manually inserted preemption points. 3. “Finite” can be a very long time indeed. There are literally competitions to see who can make the largest busy beaver machine. Put another way, undefined behavior is a sharp line - if code has UB, it has UB and it if doesn’t, it doesn’t. But code being slow is not a sharp line - something can take 1 ns or 1 ms or 1 second or 1 hour or 1 year or 100 years or 1M years, etc. A scheduler that fails to schedule a runnable thread in finite time is wrong, but so is a scheduler that fails to schedule it for 100 years or for a week. If it merely takes a minute, then whether it’s right or wrong depends on the situation. So if you’re talking about schedulers (which that part of talk mostly is), then I don’t think the ability to say “infinite loop without side effects are UB, so my scheduler is correct if I assume that all side-effect-free loops are finite” is actually useful. There are real world examples. At one point, Go only preempted its cooperative threads at certain points, but this was a problem and newer versions of Go can even preempt tight loops. Python, which threads the worst-of-both-worlds middle ground between asynchronous and cooperative preemption, does not allow an infinite loop (in ordinary Python code) to starve other threads. [0] Most users of C- or Rust-like languages anyway. Quite a few more managed languages (e.g. Go) are the other way around.
mitxela 13d ago
I thought it was generally so the compiler can merge two computation loops without proving if one of them runs forever .
- murderfs 13d ago
  Correct. See N1528: "Why undefined behavior for infinite loops?" https://www.open-std.org/jtc1/sc22/wg14/www/docs/n1528.htm https://www.open-std.org/jtc1/sc22/wg14/www/docs/n1528.htm
  - cryptonector 12d ago
    That is not worth this nonsense.
  - amluto 12d ago
    That’s actually a fairly good answer. I think I’d summarize the meat of it as: even a non-atomic, non volatile store can be observable in the sense that it can transform data-race-free code into racy code, and the compiler may not do this in a manner that changes observable behavior. I’m starting to wonder whether newly designed programming languages should explicitly distinguish probably terminating loops from potentially infinite loops. Lean does, for good reason.
    - cryptonector 12d ago
      Is it a good answer though? How often does this opportunity come up? And if you have two trivial infinite loops one after the other, do you really need to insert `yield()` in order to be able to merge them?
      - amluto 12d ago
        That's not the issue. Suppose you have some state like this: const node *head1; int sum1, sum2; And you have: void func() { for ( int *p = head; p; p = p->next ) sum1 += p->val1; for ( int *p = head; p; p = p->next ) sum2 += p->val2; } The compiler really wants to merge the loops (this will be a nearly 2x speedup in this contrived case). In other words, the compiler would like to generate this instead: void func() { for ( int *p = head; p; p = p->next ) { sum1 += p->val1; sum2 += p->val2; } } Naively, this optimization looks obviously correct: since there is no synchronization in func(), nothing could validly observe the changes in the order of the stores. Here's the problem. While C and C++ consider data races to be UB (which is why the compiler is allowed to mess with the order in which potentially shared state is written here), the presence of a data race is still observable in a problematic sense. Suppose thread 2 is doing something like this: while (true) { printf("%d\n", sum2); } If thread 1 calls func() while this loop is running, then the program has undefined behavior [0]. Except there's a really nasty corner case. If the linked list has a cycle, then func() contains an infinite loop. (All it takes to cause this is head->next == head.) And, if func() has an infinite loop then, as originally written, sum2 is never modified and there is not a data race. So a sneaky programmer could set up the infinite loop, call func() in one thread, do the printf loop in another thread, and the compiler would need to run that code correctly because it's not UB. If the compiler transforms func() as above, then it introduces a data race where none existed, and it's a bug. But this optimization seems important, and C and C++ sidestep this issue by declaring that func() itself is UB if the linked list contains a cycle. So the transformation does not introduce UB in my example because, in the problematic case, the UB is already there in the original code. Problem solved. Yuck. (Realistically the compiler will also probably accumulate the sum in registers and add to sum1 and sum2 at the end. One could quibble that this subsequent transformation invalidates my point, but it's easy enough to make a slightly more complex example that doesn't have this problem.) None of this is to say that I like C and C++'s solution. It's gross. The new C++ change to sort-of-solve it is extremely gross. FWIW (and I sort of alluded to this above), there is an IMO much more interesting reason that compilers should care about infinite loops that doesn't apply to C/C++. In languages like Lean (but borrowing C-like syntax), you can write something like: ProofType proof() { // some body here } The entire basis of the proof model in Lean is that the existence of a "term" like proof() that returns the type ProofType implies that an object of ProofType can be constructed (I think this is usually described as saying that ProofType is "inhabited"). This is pretty concrete -- you could literally run proof() to obtain this object. But infinite loops completely break it: you could just write: ProofType proof() { while (true) ; } (Sure, a clever compiler could reject this particular function. But a clever programmer can out-clever the compiler.) So, in Lean, you either need to prove to the compiler that all your loops terminate or you need to mark the function as "partial", which tells the compiler that it cannot assume that the existence of the function means that the return type is inhabited. This would be a pretty radical change to C and C++, but it would fully solve forward-progress problem :) [0] This one is no joke. I can come up with examples that would jump to inappropriate addresses using a construct like this if there's a data race -- just replace sum2 with a function pointer.

by amluto 13d ago

raphlinus 13d ago

You will find the answer you seek not from an LLM, but from the talk Forward Progress Guarantees in C++ by Olivier Giroux at CppNow 2023. It's a long talk, with lots of details about forward progress, but I've set the timestamp[1] to the infinite loop bit. [1]: https://youtu.be/g9Rgu6YEuqY?si=_l9JwKhjvIdFEDEX&t=3819 https://youtu.be/g9Rgu6YEuqY?si=_l9JwKhjvIdFEDEX&t=3819

amluto 12d ago
I don’t really buy that justification, for three reasons: 1. Most implementations do not do this automatic cooperative multitasking trick and most users [0] don’t want it done to their code. 2. The fact that a “step” is guaranteed to happen in finite time is far too weak for most use cases. I’ve done plenty of kernel programming, and a lot of kernels are partially or fully cooperative scheduled. Even somewhat long loops need manually inserted preemption points. 3. “Finite” can be a very long time indeed. There are literally competitions to see who can make the largest busy beaver machine. Put another way, undefined behavior is a sharp line - if code has UB, it has UB and it if doesn’t, it doesn’t. But code being slow is not a sharp line - something can take 1 ns or 1 ms or 1 second or 1 hour or 1 year or 100 years or 1M years, etc. A scheduler that fails to schedule a runnable thread in finite time is wrong, but so is a scheduler that fails to schedule it for 100 years or for a week. If it merely takes a minute, then whether it’s right or wrong depends on the situation. So if you’re talking about schedulers (which that part of talk mostly is), then I don’t think the ability to say “infinite loop without side effects are UB, so my scheduler is correct if I assume that all side-effect-free loops are finite” is actually useful. There are real world examples. At one point, Go only preempted its cooperative threads at certain points, but this was a problem and newer versions of Go can even preempt tight loops. Python, which threads the worst-of-both-worlds middle ground between asynchronous and cooperative preemption, does not allow an infinite loop (in ordinary Python code) to starve other threads. [0] Most users of C- or Rust-like languages anyway. Quite a few more managed languages (e.g. Go) are the other way around.

mitxela 13d ago

I thought it was generally so the compiler can merge two computation loops without proving if one of them runs forever .

murderfs 13d ago
Correct. See N1528: "Why undefined behavior for infinite loops?" https://www.open-std.org/jtc1/sc22/wg14/www/docs/n1528.htm https://www.open-std.org/jtc1/sc22/wg14/www/docs/n1528.htm
- cryptonector 12d ago
  That is not worth this nonsense.
- amluto 12d ago
  That’s actually a fairly good answer. I think I’d summarize the meat of it as: even a non-atomic, non volatile store can be observable in the sense that it can transform data-race-free code into racy code, and the compiler may not do this in a manner that changes observable behavior. I’m starting to wonder whether newly designed programming languages should explicitly distinguish probably terminating loops from potentially infinite loops. Lean does, for good reason.
  - cryptonector 12d ago
    Is it a good answer though? How often does this opportunity come up? And if you have two trivial infinite loops one after the other, do you really need to insert `yield()` in order to be able to merge them?
    - amluto 12d ago
      That's not the issue. Suppose you have some state like this: const node *head1; int sum1, sum2; And you have: void func() { for ( int *p = head; p; p = p->next ) sum1 += p->val1; for ( int *p = head; p; p = p->next ) sum2 += p->val2; } The compiler really wants to merge the loops (this will be a nearly 2x speedup in this contrived case). In other words, the compiler would like to generate this instead: void func() { for ( int *p = head; p; p = p->next ) { sum1 += p->val1; sum2 += p->val2; } } Naively, this optimization looks obviously correct: since there is no synchronization in func(), nothing could validly observe the changes in the order of the stores. Here's the problem. While C and C++ consider data races to be UB (which is why the compiler is allowed to mess with the order in which potentially shared state is written here), the presence of a data race is still observable in a problematic sense. Suppose thread 2 is doing something like this: while (true) { printf("%d\n", sum2); } If thread 1 calls func() while this loop is running, then the program has undefined behavior [0]. Except there's a really nasty corner case. If the linked list has a cycle, then func() contains an infinite loop. (All it takes to cause this is head->next == head.) And, if func() has an infinite loop then, as originally written, sum2 is never modified and there is not a data race. So a sneaky programmer could set up the infinite loop, call func() in one thread, do the printf loop in another thread, and the compiler would need to run that code correctly because it's not UB. If the compiler transforms func() as above, then it introduces a data race where none existed, and it's a bug. But this optimization seems important, and C and C++ sidestep this issue by declaring that func() itself is UB if the linked list contains a cycle. So the transformation does not introduce UB in my example because, in the problematic case, the UB is already there in the original code. Problem solved. Yuck. (Realistically the compiler will also probably accumulate the sum in registers and add to sum1 and sum2 at the end. One could quibble that this subsequent transformation invalidates my point, but it's easy enough to make a slightly more complex example that doesn't have this problem.) None of this is to say that I like C and C++'s solution. It's gross. The new C++ change to sort-of-solve it is extremely gross. FWIW (and I sort of alluded to this above), there is an IMO much more interesting reason that compilers should care about infinite loops that doesn't apply to C/C++. In languages like Lean (but borrowing C-like syntax), you can write something like: ProofType proof() { // some body here } The entire basis of the proof model in Lean is that the existence of a "term" like proof() that returns the type ProofType implies that an object of ProofType can be constructed (I think this is usually described as saying that ProofType is "inhabited"). This is pretty concrete -- you could literally run proof() to obtain this object. But infinite loops completely break it: you could just write: ProofType proof() { while (true) ; } (Sure, a clever compiler could reject this particular function. But a clever programmer can out-clever the compiler.) So, in Lean, you either need to prove to the compiler that all your loops terminate or you need to mark the function as "partial", which tells the compiler that it cannot assume that the existence of the function means that the return type is inhabited. This would be a pretty radical change to C and C++, but it would fully solve forward-progress problem :) [0] This one is no joke. I can come up with examples that would jump to inappropriate addresses using a construct like this if there's a data race -- just replace sum2 with a function pointer.