Hacker News Reader

Do any CPUs ship with correctness guarantees?

You can definitely get CPUs which run in pairs and verify amongst themselves that they both come to the same answer when running the same code on the same inputs: https://en.wikipedia.org/wiki/Lockstep_(computing).

Being physical devices, even if the design adheres to the spec any individual CPU might still be defective of course. You can only test "is it still good" by periodically running one through a test suite and re-certifying that it still returns the correct answers, but there is never any guarantee that it won't break a second later due to freak circumstances. You can get down to acceptable margins though.

Using redundant systems helps detect (dual redunant) and even correct (triple modular redundant) physical faults in the system, where one system will provide a different answer than the other(s). System redundancy does not detect/correct for design flaws, which are a common mode failure. Catching design flaws is currently done by testing (compared to known correct answers) and peer review (by domain experts). Someday, mathematical proofs might be used (known as "formal methods"), but currently these are only possible to use on very small software projects, such as the seL4 project that formally proved correctness for around 10K lines of code.

You can check TI's Hercules Safety MCUs which has 2 MCUs which operate in lockstep. It guarantees the hardware faults I think.

In Railways I have seen two systems running on the same processing and doing a check of the results and then sending it out. If something is opposed then it fails gracefully and safely.

Reply on news.ycombinator.com