3 ms·

When you start thinking about how to write correct C code, there are a few steps along the way. Glorified linters are a great first step; in the best case, they

by addaon 3y ago

When you start thinking about how to write correct C code, there are a few steps along the way. Glorified linters are a great first step; in the best case, they prove useful safety properties of code (no access to uninitialized variables, etc). From there, static analyzers start proving more complex properties -- no stack overflow, for example. The final step along this journey is to proof assistants, proving arbitrary properties not just with regards to safety, but correctness. One often overlooked part is CompCert [1], a pretty-much-verified C compiler. All of the tools mentioned above prove properties on the semantics of the C code that is written. These properties are only conserved in practice if the translation of the C code to equivalent-semantic machine code is correct, and the execution of the machine code is correct with regards to its modeled semantics. The first part of this chain of trust is where CompCert slots in; for the second part, in practice, we are at the mercy of our silicon vendors. https://compcert.org/compcert-C.html https://compcert.org/compcert-C.html

AlotOfReading 3y ago
Compcert is a true tour de force in what can be done with formal methods, but my experience is that almost no one is actually in a position where semantic equivalence is major source of issues for them. I more commonly see it brought up internally as a way for people to avoid facing the larger issues traditionally plaguing high assurance C development that aren't as simple as "just" changing the compiler.
- 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.
nullifidian 3y ago
Comcert is verified functional code in coq that is translated to ocaml for execution, the compiler for which isn't verified. It doesn't solve the problem of verification of imperative code. The state of the art approaches to imperative code verification using coq ( such as https://gitlab.mpi-sws.org/iris/refinedc https://gitlab.mpi-sws.org/iris/refinedc ) struggle to verify the basic college textbook algorithms and are extremely clunky in practice.

by addaon 3y ago

AlotOfReading 3y ago

Compcert is a true tour de force in what can be done with formal methods, but my experience is that almost no one is actually in a position where semantic equivalence is major source of issues for them. I more commonly see it brought up internally as a way for people to avoid facing the larger issues traditionally plaguing high assurance C development that aren't as simple as "just" changing the compiler.

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.

nullifidian 3y ago

Comcert is verified functional code in coq that is translated to ocaml for execution, the compiler for which isn't verified. It doesn't solve the problem of verification of imperative code. The state of the art approaches to imperative code verification using coq ( such as https://gitlab.mpi-sws.org/iris/refinedc https://gitlab.mpi-sws.org/iris/refinedc ) struggle to verify the basic college textbook algorithms and are extremely clunky in practice.