4 ms·

I'm a digital hardware (chips) guy. We use compilers (synthesis tools) and normally won't get a second chance to recompile if the logic gates in our silicon chi

I'm a digital hardware (chips) guy. We use compilers (synthesis tools) and normally won't get a second chance to recompile if the logic gates in our silicon chip are wrong as a result of compiler bugs or misinterpretation of source. We automatically distrust the compiler (synthesis tool) to do the right thing. You formally prove the 'compiled' output (logic gates) that will be manufactured matches with the source code of the design (verilog/vhdl) using tools written independently to the compiler. This isn't easy, and I know the problem space is larger, but does anyone ever do this for software?

nkurz 10y ago
SQLite is usually (and correctly) held as an example of thorough software testing: https://www.sqlite.org/testing.html https://www.sqlite.org/testing.html Perhaps you could offer a sense of how this compares to the hardware testing practices you use?
- whaaswijk 10y ago
  Typically in hardware design you'd use combinational equivalence checking (CEC) to formally prove that a synthesized design is correct. See https://en.wikipedia.org/wiki/Formal_equivalence_checking https://en.wikipedia.org/wiki/Formal_equivalence_checking. In CEC you use a SAT solver to prove that a new (synthesized and optimized) circuit is equivalent to some reference model (aka golden model) which you know is correct. So instead of relying on just testing (which is incomplete) you have a formal proof that your design is correct. Of course you still have to trust that the SAT solver works correctly... :-)
- StringyBob 10y ago
  In hardware design you typically test functionality through logic simulation or emulation (effectively running the code in a computer simulation or fpga), use test harnesses, look for code coverage, run unit tests, random code fuzzing, code assertions etc. You might also do formal checks for some assertions to e.g. avoid deadlocks. A secondary check is that the source that you functionally tested is logically equivalent to what you manufacture. This is where you are not checking your code, but the issue is trust of compiler/ compiler optimisations in synthesis. It needs to be redone if you recompile - that's the step I don't really ever see in software development - if I use a different compiler option or underlying instruction set architecture to the SQLite Dev team, do I still trust my binary? Of course the level of paranoia is far higher in hardware where it costs multiple millions of dollars to crank out a new spin of a chip!
  - dalke 10y ago
    > if I use a different compiler option or underlying instruction set architecture to the SQLite Dev team, do I still trust my binary? If that is critical, you can join the SQLite Consortium Membership for $75K/year and access to the test suite. There's also an option to pay SQLite developers to "run TH3 on specialized hardware and/or using specialized compile-time options, according to customer specification, either remotely or on customer premises." The TH3 test harness is an aviation-grade test suite. The level of paranoia for aviation software is also rather high.
ArkyBeagle 10y ago
I've seen that "no second chance" thing personally and it's hilarious to me. WTF? I would hum "Mars The Bringer of War" to FPGA guys at times because of this ( it's the theme used in "The Right Stuff" at Those Times in the movie ). In the general case, no. The economics of software don't favor it. There are tools that inspect code and make helpful suggestions. This is why you can't trust your synthesis tools, BTW. But much worse in software is the cultural ... "zero" ( as in a zero in a filter) about the axis of provability in general. It's a point of despair. I can tell you that in multiple cases, I was able to represent the "core" logic of systems much that I could build a test rig around it and do exhaustive testing ( with the caveat that it's only as good as the test framework ). Permutaitons are reasonably cheap these days. But to do this, you must nearly eschew the us of third party code and in cases, even large parts of standard libraries. But the standard answer is to despair and moan "it's impossible." The "prove it correct" people and the "git 'er done" people are two different tribes.
gsnedders 10y ago
> This isn't easy, and I know the problem space is larger, but does anyone ever do this for software? Typically the state space is simply too large to be practical. It is, admittedly, how a lot of verified software is done (because there are so few verified compilers), though often then the source-code to assembly correspondence is verified manually, which limits possible optimisations.
legulere 10y ago
The problem you describe is one of unreliable compilers, here the problem is that the C standard allows a few undefined things to cause an avalanche of undefined behaviour. What the compilers do is totally correct according to the standard, but not at all what programmers expect.
WallWextra 10y ago
The correctness proof of the seL4 microkernel supposedly makes no assumptions of the compiler and verifies the binary output. I don't know the details.
pgeorgi 10y ago
There's SPARK (http://spark-2014.org/ http://spark-2014.org/) that's an Ada dialect with verification features, and there's frama-c, doing something similar for C (http://frama-c.com/ http://frama-c.com/). In both cases the compiler is pretty much part of the trust base (which is a problem because they're annoyingly complex), but the issues discussed here are declared invalid by the subset (ie. you mustn't use statements that may lead to undefined behavior). For seL4, mentioned in another comment, there was proof that interesting properties of the high-level code and the low-level binary were equivalent. That only works with a relatively static compiler version and for some optimization levels (anything that optimizes too globally will seriously mess up such attempts of showing equivalence), but it takes the compiler out of the trust base.

nkurz 10y ago

SQLite is usually (and correctly) held as an example of thorough software testing: https://www.sqlite.org/testing.html https://www.sqlite.org/testing.html Perhaps you could offer a sense of how this compares to the hardware testing practices you use?

whaaswijk 10y ago
Typically in hardware design you'd use combinational equivalence checking (CEC) to formally prove that a synthesized design is correct. See https://en.wikipedia.org/wiki/Formal_equivalence_checking https://en.wikipedia.org/wiki/Formal_equivalence_checking. In CEC you use a SAT solver to prove that a new (synthesized and optimized) circuit is equivalent to some reference model (aka golden model) which you know is correct. So instead of relying on just testing (which is incomplete) you have a formal proof that your design is correct. Of course you still have to trust that the SAT solver works correctly... :-)
StringyBob 10y ago
In hardware design you typically test functionality through logic simulation or emulation (effectively running the code in a computer simulation or fpga), use test harnesses, look for code coverage, run unit tests, random code fuzzing, code assertions etc. You might also do formal checks for some assertions to e.g. avoid deadlocks. A secondary check is that the source that you functionally tested is logically equivalent to what you manufacture. This is where you are not checking your code, but the issue is trust of compiler/ compiler optimisations in synthesis. It needs to be redone if you recompile - that's the step I don't really ever see in software development - if I use a different compiler option or underlying instruction set architecture to the SQLite Dev team, do I still trust my binary? Of course the level of paranoia is far higher in hardware where it costs multiple millions of dollars to crank out a new spin of a chip!
- dalke 10y ago
  > if I use a different compiler option or underlying instruction set architecture to the SQLite Dev team, do I still trust my binary? If that is critical, you can join the SQLite Consortium Membership for $75K/year and access to the test suite. There's also an option to pay SQLite developers to "run TH3 on specialized hardware and/or using specialized compile-time options, according to customer specification, either remotely or on customer premises." The TH3 test harness is an aviation-grade test suite. The level of paranoia for aviation software is also rather high.

ArkyBeagle 10y ago

I've seen that "no second chance" thing personally and it's hilarious to me. WTF? I would hum "Mars The Bringer of War" to FPGA guys at times because of this ( it's the theme used in "The Right Stuff" at Those Times in the movie ). In the general case, no. The economics of software don't favor it. There are tools that inspect code and make helpful suggestions. This is why you can't trust your synthesis tools, BTW. But much worse in software is the cultural ... "zero" ( as in a zero in a filter) about the axis of provability in general. It's a point of despair. I can tell you that in multiple cases, I was able to represent the "core" logic of systems much that I could build a test rig around it and do exhaustive testing ( with the caveat that it's only as good as the test framework ). Permutaitons are reasonably cheap these days. But to do this, you must nearly eschew the us of third party code and in cases, even large parts of standard libraries. But the standard answer is to despair and moan "it's impossible." The "prove it correct" people and the "git 'er done" people are two different tribes.

gsnedders 10y ago

> This isn't easy, and I know the problem space is larger, but does anyone ever do this for software? Typically the state space is simply too large to be practical. It is, admittedly, how a lot of verified software is done (because there are so few verified compilers), though often then the source-code to assembly correspondence is verified manually, which limits possible optimisations.

legulere 10y ago

The problem you describe is one of unreliable compilers, here the problem is that the C standard allows a few undefined things to cause an avalanche of undefined behaviour. What the compilers do is totally correct according to the standard, but not at all what programmers expect.

WallWextra 10y ago

The correctness proof of the seL4 microkernel supposedly makes no assumptions of the compiler and verifies the binary output. I don't know the details.

pgeorgi 10y ago

There's SPARK (http://spark-2014.org/ http://spark-2014.org/) that's an Ada dialect with verification features, and there's frama-c, doing something similar for C (http://frama-c.com/ http://frama-c.com/). In both cases the compiler is pretty much part of the trust base (which is a problem because they're annoyingly complex), but the issues discussed here are declared invalid by the subset (ie. you mustn't use statements that may lead to undefined behavior). For seL4, mentioned in another comment, there was proof that interesting properties of the high-level code and the low-level binary were equivalent. That only works with a relatively static compiler version and for some optimization levels (anything that optimizes too globally will seriously mess up such attempts of showing equivalence), but it takes the compiler out of the trust base.