5 ms·

> almost no one is actually in a position where semantic equivalence is major source of issues for them Well, they don't necessarily know if it is or not... W

by addaon 3y ago

> almost no one is actually in a position where semantic equivalence is major source of issues for them Well, they don't necessarily know if it is or not... When you're dealing with safety-critical software (DO-178, etc) where the cost of verification and validation can be easily 100x - 1000x the cost of writing the code, having traceability from C code to machine code be correct by proof instead of a manual process can be a lifesaver. Are a significant number of bugs actually excluded this way? That basically comes down to how much the defect rate has been reduced at the C code level by other activities, to determine significance. It's hard for me to imagine working on DAL B or DAL A code and not at least seriously considering use CompCert just to reduce the scope of necessary verification activities a bit.

AlotOfReading 3y ago
Absolutely agree. Compcert solves a very difficult problem better than pretty much any other solution. However, that problem is mostly a theoretical one, even if it's important to mitigate it. It's not a replacement for source level verification and migrating the compiler can be put off until relatively late in a project.
Quekid5 3y ago
As you alluded to... How many compiler bugs materially affect the C->ASM bit of the pipeline rather than the C source code just being incorrect? I'd wager it's a tiny ratio, but I honestly don't know. Could you point to any research on this, if you happen to have links handy? I could imagine even 0.01% being significant for e.g. space missions or (if we're being optimistic) lives are at stake.
- addaon 3y ago
  You're asking about the ratio of "compiler bugs in code generation impacting behavior" to "bugs in C source code"? Obviously the number depends critically on the denominator... Defect density for DAL A software is well studied and very, very low. See, e.g., [1]. "Most estimates put the number of residual defects for a good software process at 1 to 10 per KNCSL," of which 1% are of catastrophic severity. These processes give a low enough defect rate that real-world failures are dominated by errors in the requirements process rather than in the process of converting requirements to source code; it's not hard to see that at this point compiler bugs can be non-negligible. [1] https://apps.dtic.mil/sti/pdfs/AD1088687.pdf https://apps.dtic.mil/sti/pdfs/AD1088687.pdf
- astrange 3y ago
  CompCert has had bugs in its C compilation before, for instance because the assembly to binary translation wasn't verified.
- rsaxvc 3y ago
  I found one in a supposedly IEC 61508 compiler. It was nasty. Every so often our OS needed to read a memory mapped asynchronous timer, comparing values it emitted until they stopped changing to confirm that the various system clock demands were safely aligned and that the addition of a periodic tick was not rippling its way through the counter, before using the value. This time I ran at 32.768 kHz, but to see the glitch required reading the timer exactly as the adder rippled. Most of the time the CPU would read in between the ripples and it would work fine. This driver had worked on several released products with an earlier version of the compiler, we upgraded the compiler slightly to take advantage of a new instruction set in the next chip. The updated compiler would rarely assume sequential volatile reads from the same address had the same value. Something like while(v!=v){} would become the equivalent of if(v!=v)while(1){}; This compiler fault meant that our previously working driver would lock up the machine between maybe an hour and a few days, whenever a particular IRQ occurred during the clock domains race. Normally watchdogs would trap most infinite loops in the system, but it didn't I knew that it had to be this particular IRQ. Disassembled the whole thing, which only had one loop in it (this one). Took me forever to find because the loop structure was essentially correct except that it was branching just past one of the loads that needed redone. So instead of load x, load y, compare y,x, branch if difference to load x, it branches to load y, a difference of two bytes in the branch offset. The compiler vendor confirmed this and corrected it in the next compiler version. The ticket number used to be on their website but they no longer publish the change log that far back.

by addaon 3y ago

AlotOfReading 3y ago

Absolutely agree. Compcert solves a very difficult problem better than pretty much any other solution. However, that problem is mostly a theoretical one, even if it's important to mitigate it. It's not a replacement for source level verification and migrating the compiler can be put off until relatively late in a project.

Quekid5 3y ago

As you alluded to... How many compiler bugs materially affect the C->ASM bit of the pipeline rather than the C source code just being incorrect? I'd wager it's a tiny ratio, but I honestly don't know. Could you point to any research on this, if you happen to have links handy? I could imagine even 0.01% being significant for e.g. space missions or (if we're being optimistic) lives are at stake.

addaon 3y ago
You're asking about the ratio of "compiler bugs in code generation impacting behavior" to "bugs in C source code"? Obviously the number depends critically on the denominator... Defect density for DAL A software is well studied and very, very low. See, e.g., [1]. "Most estimates put the number of residual defects for a good software process at 1 to 10 per KNCSL," of which 1% are of catastrophic severity. These processes give a low enough defect rate that real-world failures are dominated by errors in the requirements process rather than in the process of converting requirements to source code; it's not hard to see that at this point compiler bugs can be non-negligible. [1] https://apps.dtic.mil/sti/pdfs/AD1088687.pdf https://apps.dtic.mil/sti/pdfs/AD1088687.pdf
astrange 3y ago
CompCert has had bugs in its C compilation before, for instance because the assembly to binary translation wasn't verified.
rsaxvc 3y ago
I found one in a supposedly IEC 61508 compiler. It was nasty. Every so often our OS needed to read a memory mapped asynchronous timer, comparing values it emitted until they stopped changing to confirm that the various system clock demands were safely aligned and that the addition of a periodic tick was not rippling its way through the counter, before using the value. This time I ran at 32.768 kHz, but to see the glitch required reading the timer exactly as the adder rippled. Most of the time the CPU would read in between the ripples and it would work fine. This driver had worked on several released products with an earlier version of the compiler, we upgraded the compiler slightly to take advantage of a new instruction set in the next chip. The updated compiler would rarely assume sequential volatile reads from the same address had the same value. Something like while(v!=v){} would become the equivalent of if(v!=v)while(1){}; This compiler fault meant that our previously working driver would lock up the machine between maybe an hour and a few days, whenever a particular IRQ occurred during the clock domains race. Normally watchdogs would trap most infinite loops in the system, but it didn't I knew that it had to be this particular IRQ. Disassembled the whole thing, which only had one loop in it (this one). Took me forever to find because the loop structure was essentially correct except that it was branching just past one of the loads that needed redone. So instead of load x, load y, compare y,x, branch if difference to load x, it branches to load y, a difference of two bytes in the branch offset. The compiler vendor confirmed this and corrected it in the next compiler version. The ticket number used to be on their website but they no longer publish the change log that far back.