3 ms·
That's what I was getting at with the second sentence in my post: we can verify the code matches the spec, but not that the spec is flawed. So this verificatio
by sbf501 4y ago
That's what I was getting at with the second sentence in my post: we can verify the code matches the spec, but not that the spec is flawed.
So this verification is what CPU designers do: they create a RTL (HDL, VHDL, Verilog) and then a circuit (gates) and then Magma or Cadence or Synopsys tools formally verify that the logic in the behavioral model matches the implementation model.
However, if the microarchitect had a brain fart, the RTL is bugged to begin with.
I was hoping this could go backwards one step further and give the microarchitect/RFC-editor a swift kick in the pants. :)
- drpixie 4y agoI think that's the real advantage of RISC architectures - a small spec leaves less space for problems. Not no space, but less space.
- rurban 4y agoYes, but the various HW bugs and exploits, e.g cache leaks and poisoning - Spectre, Meltdown, ..., are not handled. Also not in the mentioned and formally proven crypto libs.
- sbf501 4y agoAdvantage over what? The idea that RISC is somehow simpler went the way of the dinosaur 30 years ago. The ISA does not define performance, that is the microarchitecture, which is where all of the engineering effort is spent. You can have the classic ISA of the Turing Machine that we all learned about in comp-sci 101 classes: "Load/Store/Add/Compare/Jump" and it would be simple but dog-ass slow. Not to mention open to all sorts of attacks and exploits (buffer overflows, stack smashing), and meta attacks (side-channel), or Goedels incompleteness. The uarch is where the action happens.
- drpixie 4y agoWe were talking about correctness. RISCs by definition have simpler architectures that CISCs - that's what makes them RISCs. And simpler architectures leave less room for confusion/bugs/faults in the architecture, irrespective how they are implemented.
- deterministic 4y agoNon-proven correct code doesn’t even have specs you can test the code against. So comparing non-proven code without a formal spec with code that has a formal spec and an end-to-end proof chain from spec to machine code, and then saying they are equally likely to be buggy is frankly ridiculous.