9 ms·

CPU manufacturers do do huge amounts of testing, and Intel does formal verification of some functional units. The reliability is far better than most software,

by wbl 9y ago

CPU manufacturers do do huge amounts of testing, and Intel does formal verification of some functional units. The reliability is far better than most software, in part because making a new release costs billions.

wyager 9y ago
This seems like precisely the sort of thing that a competent manufacturer should rule out formally. Formal verification of individual FUs isn't exactly ambitious... I think we're getting to levels of complexity where the process Intel uses, with lots of different QA and testing teams doing their best to look for bugs, just isn't going to cut it. We need formally verified models transformed step-by-verified-step all the way down to the silicon. It's already feasible, with free tools, to formally verify your high-level model (using e.g. LiquidHaskell) and then transform this to RTL (using e.g. Clash). With Intel's QA/testing budget, it's well within reach to A) verify the transformation steps and B) figure out how to close the performance gap between machine-generated (but maybe slower) and hand-rolled (faster, but evidently wrong) silicon.
- lorenzhs 9y ago
  So it's okay for software to have bugs that get fixed (I think everybody here acknowledges that software will always have bugs), but Intel isn't allowed to have issues in their processors, even if they can fix them with a software (microcode) update?
  - userbinator 9y ago
    In general, people expect hardware to be far more bug-free than all the software which depends on it. I'm disgusted enough at the current trend of continuously releasing half-baked software and "updating" it to fix some of the bugs (while introducing new bugs in the process); and yet it seems to be spreading to hardware too. From the perspective of formal verification, buggy hardware is like an incorrect axiom. but Intel isn't allowed to have issues in their processors, even if they can fix them with a software (microcode) update? They could've caught and fixed this one with some more testing, before actually releasing. Formal verification isn't necessarily going to help, if it's a statistical type of defect --- thus the concept of wafer yield, and why dies manufactured from the exact same masks can behave completely differently with respect to the clock speeds attainable and voltages required.
    - lorenzhs 9y ago
      Expectations of hardware are indeed higher than for software, but isn't it a valid trade-off for Intel to make as long as most of the issues can be fixed with a microcode update? On Windows, it's updated via Windows Update, and on most Linux distributions, a package exists for CPU microcode. Most users have an easy—if not automatic—way to obtain the updates. I believe the main issue with formally verifying everything is that reasoning about parallel code is extremely hard and might well make the entire endeavour unattainable. It would be great to have formally verified CPUs, though. > They could've caught and fixed this one with some more testing, before actually releasing. Isn't this true of any bug?
      - sqldba 9y ago
        Windows update applies CPU patches?! I know they did AMT but that was a special case and different.
        lorenzhs 9y ago
        Seems like they do when it fixes serious bugs, a quick search yields e.g. https://support.microsoft.com/en-us/help/3064209/june-2015-intel-cpu-microcode-update-for-windows https://support.microsoft.com/en-us/help/3064209/june-2015-i... ("This update fixes several issues with Intel CPUs that could cause computer crashes or functions incorrectly.")
    - Cyph0n 9y ago
      Formal verification cannot be used to fully verify an entire Intel CPU, simply because the computational resources required to do so are astronomical. Heck, the cache coherence unit alone is basically impossible to verify. Therefore, CPU designers verify the important units (e.g., the ALU) independently of each other, and then try to verify their interaction. But a system level design verification check is simply not possible. Obviously, faults that result from fabrication can still take place, so they are tested for using BIST and JTAG. Test coverage can be pretty high, but obviously not 100%. As you can see, there are still a ton of places where hardware errors can seep through.
  - AsyncAwait 9y ago
    It's funny, since many of today's software bugs are due to the legacy of C, faults of which can often times be attributed to mimicking the behaviour CPU hardware too closely. EDIT: My wording was poor, but what I meant was that it's not like hardware vendors do not make bugs happen due to deficiencies in their design, which are not only tolerated, but often reflected in software, which runs counter to OP saying that apparently hardware vendors are not allowed to have bugs, but the software ones are: > So it's okay for software to have bugs that get fixed (I think everybody here acknowledges that software will always have bugs), but Intel isn't allowed to have issues in their processors
    - blahman2 9y ago
      Go back to rust-land now :D
      - AsyncAwait 9y ago
        It was meant as a response to OP basically saying that hardware vendors make way fewer bugs that the software ones, which is true, but many bugs of software can arguably be attributed to hardware design, so it's not like they're without fault. Rust has nothing to do with it, not sure why even bring it up.
        blahman2 9y ago
        I get it - sorry, meant to playfully Sunday afternoon troll you. Ever since I moved from C to Java (I like low level stuff but the company I joined is such) I have been having one of three major problems - logic bugs, too many frameworks, causing bugs due to lack of in depth understanding of each one of them, and GC bottlenecks. Of all of them, I hate the GC ones the most.
  - throwaway2048 9y ago
    There are hardware bugs that are impossible to fix in microcode. What then?
    - baq 9y ago
      you make workarounds in software, obviously.
      - userbinator 9y ago
        ...or recall all the hardware and replace it: https://en.wikipedia.org/wiki/Pentium_FDIV_bug https://en.wikipedia.org/wiki/Pentium_FDIV_bug
    - coldtea 9y ago
      There will always be. What then? We stop producing cpus and wait for some magical new technology that prevents all bugs?
      - throwaway2048 9y ago
        Its why you can't treat hardware bugs and dismiss them flippantly like software ones.
  - kutkloon7 9y ago
    Well, if a software bug leads to data corruption it is not really "allowed" as well. It is quite amazing that there are not more bugs like this. Intel spends an insane amount of money on very large teams of very smart people to work on these insanely complicated systems. I don't think this is sustainable, and I think that massive arrays of relatively simple processors. First, we will need a culture shift that learns programmers to program concurrent programs from the start, and this will take a lot of time (because technology moves a lot faster than culture).
  - ComputerGuru 9y ago
    If this "fix" ends up disabling HT, how can I get a refund not just for the CPU but for the $3k laptop I spec'd around it? Without needing to sue?
    - lorenzhs 9y ago
      That's just the workaround until a fix is available for your CPU, if I understood correctly.
      - ComputerGuru 9y ago
        No, that's not what I meant. In the past, Intel's microcode updates have simply disabled the broken functionality as an official solution. http://techreport.com/news/26911/errata-prompts-intel-to-disable-tsx-in-haswell-early-broadwell-cpus http://techreport.com/news/26911/errata-prompts-intel-to-dis...
        lorenzhs 9y ago
        You specifically said the fix might be to permanently disable HT. The TSX situation was indeed unfortunate, I have one of the affected CPUs. But it was a new feature that was broken, not something that used to work, so the bug's impact was less serious, and disabling the feature didn't have too much of an impact.
    - brianwawok 9y ago
      Contact your laptop OEM.
      - voltagex_ 9y ago
        Have you ever had to do this? The Dell XPS 9350 (Skylake) has numerous issues with GPU noise, USB-C compatibility, wifi reliability - Dell don't care unless your consumer laws are strong enough to make them care.
        9y ago
  - sqldba 9y ago
    It would be nice if they allowed users to update rather than vendors. I have a mobile Xeon. I don't know if it's affected or not.
- laydn 9y ago
  I've done formal verification on several units of a microprocessor, and I can assure you, formal verification on individual FUs is very, very ambitious (think impossible) for a modern microprocessor. For example, you can not possibly formally verify the fetcher unit on its own, because the state space that you need to cover for several cycles for all the module inputs and outputs is beyond the capability of any formal verification tool. Typically, you run formal verification on sub-blocks of sub-blocks of FUs. For this particular bug, it looks like multiple functional units are involved, so it might have been missed by formal verification.
  - wyager 9y ago
    > because the state space that you need to cover for several cycles for all the module inputs and outputs is beyond the capability of any formal verification tool. Then use a proof methodology that doesn't require exhaustive enumeration. This objection is actually fairly alarming to me; perhaps there is a larger disconnect between industrial formal techniques for hardware and software than I thought. Strings also occupy a "large state space", but this obviously doesn't prevent us from doing formal verification on functions over strings.
    - Confusion 9y ago
      Then use a proof methodology that doesn't require exhaustive enumeration. You may as well have said "then you use a magical tool that doesn't exist". Strings also occupy a "large state space", but this obviously doesn't prevent us from doing formal verification on functions over strings. What is your reason to think this is 'obviously' the case?
      - wyager 9y ago
        > You may as well have said "then you use a magical tool that doesn't exist". Ok, so what this tells me is that you're not aware of what modern verification techniques look like. There's not really any one resource I can point you to, but take a look at these links. I've used these or similar technologies personally, but there are others I haven't used. https://en.m.wikipedia.org/wiki/Intuitionistic_type_theory https://en.m.wikipedia.org/wiki/Intuitionistic_type_theory https://en.m.wikipedia.org/wiki/Homotopy_type_theory https://en.m.wikipedia.org/wiki/Homotopy_type_theory https://leanprover.github.io/about/ https://leanprover.github.io/about/ http://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf http://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf > What is your reason to think this is 'obviously' the case? Because I've done this, and anyone who claims to be familiar with formal methods should be at least passingly familiar with all the things I mentioned. Even if you aren't, if you've ever heard of SAT (a fairly universal CS concept) you should at least be familiar with the idea that non-exhaustive proofs are a thing.
- bsder 9y ago
  Formal verification of a decode unit simply will never happen. The complexity is far too high. Formally verifying something like a multiplier block is difficult but doable if you care. Formally verifying an FPU is probably at about the limit. If you want formal verification, you would have to simplify a modern microprocessor a lot.
  - wyager 9y ago
    That's the whole point of doing a provably correct transformation from a simpler model domain. Even complicated OOOE engines are fairly tractable if you don't try to implement them at an RTL level... Perhaps we are imagining different formal verification methodologies. Can you tell me what kind of formal verification you're referring to?
heisenbit 9y ago
It may be far better than average software quality but far more also relies on it. The question is whether the quality is adequate in light of what is at stake.
- lorenzhs 9y ago
  Really? How is it different from a kernel bug that causes random behaviour? Both apparently can be fixed with a software update. They're both bad, but why should Intel be held to a higher standard if mitigation is similarly complex?
  - wav-part 9y ago
    Because futher down the stack, more reliable a tech has to be. Otherwise good luck debugging. Also agree with heisenbit.
    - justinclift 9y ago
      Hmmm... on that note, if the universe is a simulation, then a bug in that could have some interesting ramifications. "Don't use the bookshelf over there, physics is broken on that shiny spot." :D
      - roywiggins 9y ago
        The problem with finding a physics bug is that it's liable to be amplifiable. Break conservation laws just a little bit and suddenly you have potential for exponential runaway leading to an unplanned reality excursion, and say goodbye to your light-cone.
        justinclift 9y ago
        Well, by definition the behaviour would be undefined so could go any which way. ;) Modern day VM software has various levels of exception checking, and code to catch/mitigate/etc when bugs crop up. So, a universe-capable simulator might have any kind of behaviour if/when a bug occurs. It doesn't need to be an unbounded, runaway scenario. :)
autokad 9y ago
i am more willing to accept software having bugs / failing. i have 0 tolerance for hardware to have bugs
- baq 9y ago
  nobody has, but it ain't easy.
- pshc 9y ago
  I wonder if there's a CPU out there that doesn't have bugs.
  - userbinator 9y ago
    It depends on how exactly you define a bug, but something like a 6502 or Z80, which has essentially all the errata well-documented since it has existed for so long, might qualify.
    - DamonHD 9y ago
      Z80 implementations for one had a whole slew of undocumented instructions, allegedly because they were buggy in some way.
  - autokad 9y ago
    stop playing lawyer ball. i'm talking about the bugs that require turning off core functionality (such as hyperthreading) and/or that lead to system halts / corrupted data. yes it happens, but software bugs happen every day where as if your system blue screened every day you know dang well you'd be on the phone with the hardware vendor for a refund / new system.
    - coldtea 9y ago
      >yes it happens, but software bugs happen every day where as if your system blue screened every day you know dang well you'd be on the phone with the hardware vendor for a refund / new system. Well, since hundreds of millions of people use Skylake/Kaby Lake CPUs for 2 years now, and only now we learn about this, obviously this is not of the "system blue screens every day" variety but a very rare bug.
davidmr 9y ago
In my limited experience, their root cause analyses are really impressive as well with lots of internal attention and resources. I'm not allowed to talk about any Intel issues, but we reported a very strange issue to Nvidia, sent a couple of dozen cards back and six months later got a truly fascinating report back we with hundreds of pages of compute test result tables and electron microscope images and chemistry lab reports. Anything that hints of a manufacturing problem is taken incredibly seriously.
- baruch 9y ago
  I worked for a large company that used thousands of Intel CPUs every year and when we suspected a CPU bug we were mostly brushed off. We had a very persistent person on the team who kept tracking the issue to find correlations and some very good kernel developers that went on to nearly pin-point the issue and only then did Intel pay attention and it then took them still several months to acknowledge the issue give a brief report on the issue and acknowledge that our proposed workaround will indeed work. I've never seen Intel do a very good job at failure analysis or following on with failures unless prodded very hard.
  - Sharlin 9y ago
    To be fair, I don't even want to think about the amount of spurious bug reports they are probably receiving.
  - deleted 9y ago
    [deleted]
  - magila 9y ago
    Intel likely has very thorough data on the issue, but you'll never see it unless you are one of their tier 1 customers* and have an NDA with them. In my experience working for a large hardware manufacturer they are very skittish about releasing detailed failure analysis data to outside companies. * For Intel that would be companies like Dell, Apple, HP, and maybe a couple of others.
- dboreham 9y ago
ploxiln 9y ago
That's absolutely true. When it comes to CPU/memory, skilled software engineers always think, "it must be my bug, it always is". So in that super rare case of actually running into a CPU defect, it's a mindfuck, it'll drive you crazy. You'll be looking for the flaw in your algorithm which makes it fail once a week under production load. But you just can't find it, it makes no sense ... (When it comes to drivers for network/storage/graphics etc devices, it's a whole different story. Those things are piles of bugs that need work-arounds in drivers.)
- justsid 9y ago
  Similarly: Kernel bugs! Once upon a time I spend a good week trying to reproduce a rare crash one of our users saw ever so often (just enough to get our attention, but not enough to get a repro case). Stack traces made no sense and just in general the whole crash made no sense the more I looked at it. Turns out it was a bug in XNUs pthread subsystem, a part where I would have never looked if it weren‘t for desperation, because, well, it‘s the kernel, it works, right?
  - digi_owl 9y ago
    Or at least should have been long since spotted thanks to use and abuse.
  - wbl 9y ago
    Emacs would regularly panic the kernel on one OS X version when I opened preview to look at a pdf and had TeX recompile.
    - inferiorhuman 9y ago
      The DVD player on OSX with a MacBook (polycarbonate ones) would occasionally cause a kernel panic if you had 4GB of RAM installed.
- digi_owl 9y ago
  You have some lovely stories online about these things. Like the guy tracking down a stuck bit in RAM. Or on the network level, a VPN that failed only when traversing one possible route between company offices.
dmead 9y ago
IIRC wasn't there some blog posts about how intel has cut their verification/QA drastically since 2010? is this the result?
- userbinator 9y ago
  Although it mentions 2015, I think that might be the one I linked in my original post above: http://danluu.com/cpu-bugs/ http://danluu.com/cpu-bugs/
gcb0 9y ago
releasing cpu micro code to work around bugs is very cheap.
- CountSessine 9y ago
  But that doesn't mean you necessarily get to keep the affected feature - the only 'work-around' might be to disable it. Consider TSX on Haswell and Broadwell, where Intel had to disable the whole feature because of a bug. And of course there was the 486 FP bug which couldn't be fixed by any kind of microcode update. If Intel had to completely disable hyperthreading in Skylake and Kabylake that would make the premium anyone paid for i5 vs i7 worthless.
  - gcb0 9y ago
    you mean i3 and i7. despite what cpuinfo tells you, no HT in i5. and my previous comment was ironic :)
    - CountSessine 9y ago
      But if you don't have HT in your i7, you basically have an i5 that you paid more than you needed for. Or has that changed? At one point, i7 was full-featured, i5 was an i7 with HT disabled, and i3 was i7 with HT intact but smaller caches. Is that different with Skylake/Kabylake? and my previous comment was ironic :) Ack - sorry. I must be irony-impaired. That's why I don't post very often. :-)
      - theandrewbailey 9y ago
        i3 also has half the cores.
    - happycube 9y ago
      Mobile dual-core lie5's have hyperthreading too.

by wbl 9y ago

wyager 9y ago

This seems like precisely the sort of thing that a competent manufacturer should rule out formally. Formal verification of individual FUs isn't exactly ambitious... I think we're getting to levels of complexity where the process Intel uses, with lots of different QA and testing teams doing their best to look for bugs, just isn't going to cut it. We need formally verified models transformed step-by-verified-step all the way down to the silicon. It's already feasible, with free tools, to formally verify your high-level model (using e.g. LiquidHaskell) and then transform this to RTL (using e.g. Clash). With Intel's QA/testing budget, it's well within reach to A) verify the transformation steps and B) figure out how to close the performance gap between machine-generated (but maybe slower) and hand-rolled (faster, but evidently wrong) silicon.

lorenzhs 9y ago
So it's okay for software to have bugs that get fixed (I think everybody here acknowledges that software will always have bugs), but Intel isn't allowed to have issues in their processors, even if they can fix them with a software (microcode) update?
- userbinator 9y ago
  In general, people expect hardware to be far more bug-free than all the software which depends on it. I'm disgusted enough at the current trend of continuously releasing half-baked software and "updating" it to fix some of the bugs (while introducing new bugs in the process); and yet it seems to be spreading to hardware too. From the perspective of formal verification, buggy hardware is like an incorrect axiom. but Intel isn't allowed to have issues in their processors, even if they can fix them with a software (microcode) update? They could've caught and fixed this one with some more testing, before actually releasing. Formal verification isn't necessarily going to help, if it's a statistical type of defect --- thus the concept of wafer yield, and why dies manufactured from the exact same masks can behave completely differently with respect to the clock speeds attainable and voltages required.
  - lorenzhs 9y ago
    Expectations of hardware are indeed higher than for software, but isn't it a valid trade-off for Intel to make as long as most of the issues can be fixed with a microcode update? On Windows, it's updated via Windows Update, and on most Linux distributions, a package exists for CPU microcode. Most users have an easy—if not automatic—way to obtain the updates. I believe the main issue with formally verifying everything is that reasoning about parallel code is extremely hard and might well make the entire endeavour unattainable. It would be great to have formally verified CPUs, though. > They could've caught and fixed this one with some more testing, before actually releasing. Isn't this true of any bug?
    - sqldba 9y ago
      Windows update applies CPU patches?! I know they did AMT but that was a special case and different.
      - lorenzhs 9y ago
        Seems like they do when it fixes serious bugs, a quick search yields e.g. https://support.microsoft.com/en-us/help/3064209/june-2015-intel-cpu-microcode-update-for-windows https://support.microsoft.com/en-us/help/3064209/june-2015-i... ("This update fixes several issues with Intel CPUs that could cause computer crashes or functions incorrectly.")
  - Cyph0n 9y ago
    Formal verification cannot be used to fully verify an entire Intel CPU, simply because the computational resources required to do so are astronomical. Heck, the cache coherence unit alone is basically impossible to verify. Therefore, CPU designers verify the important units (e.g., the ALU) independently of each other, and then try to verify their interaction. But a system level design verification check is simply not possible. Obviously, faults that result from fabrication can still take place, so they are tested for using BIST and JTAG. Test coverage can be pretty high, but obviously not 100%. As you can see, there are still a ton of places where hardware errors can seep through.
- AsyncAwait 9y ago
  It's funny, since many of today's software bugs are due to the legacy of C, faults of which can often times be attributed to mimicking the behaviour CPU hardware too closely. EDIT: My wording was poor, but what I meant was that it's not like hardware vendors do not make bugs happen due to deficiencies in their design, which are not only tolerated, but often reflected in software, which runs counter to OP saying that apparently hardware vendors are not allowed to have bugs, but the software ones are: > So it's okay for software to have bugs that get fixed (I think everybody here acknowledges that software will always have bugs), but Intel isn't allowed to have issues in their processors
  - blahman2 9y ago
    Go back to rust-land now :D
    - AsyncAwait 9y ago
      It was meant as a response to OP basically saying that hardware vendors make way fewer bugs that the software ones, which is true, but many bugs of software can arguably be attributed to hardware design, so it's not like they're without fault. Rust has nothing to do with it, not sure why even bring it up.
      - blahman2 9y ago
        I get it - sorry, meant to playfully Sunday afternoon troll you. Ever since I moved from C to Java (I like low level stuff but the company I joined is such) I have been having one of three major problems - logic bugs, too many frameworks, causing bugs due to lack of in depth understanding of each one of them, and GC bottlenecks. Of all of them, I hate the GC ones the most.
- throwaway2048 9y ago
  There are hardware bugs that are impossible to fix in microcode. What then?
  - baq 9y ago
    you make workarounds in software, obviously.
    - userbinator 9y ago
      ...or recall all the hardware and replace it: https://en.wikipedia.org/wiki/Pentium_FDIV_bug https://en.wikipedia.org/wiki/Pentium_FDIV_bug
  - coldtea 9y ago
    There will always be. What then? We stop producing cpus and wait for some magical new technology that prevents all bugs?
    - throwaway2048 9y ago
      Its why you can't treat hardware bugs and dismiss them flippantly like software ones.
- kutkloon7 9y ago
  Well, if a software bug leads to data corruption it is not really "allowed" as well. It is quite amazing that there are not more bugs like this. Intel spends an insane amount of money on very large teams of very smart people to work on these insanely complicated systems. I don't think this is sustainable, and I think that massive arrays of relatively simple processors. First, we will need a culture shift that learns programmers to program concurrent programs from the start, and this will take a lot of time (because technology moves a lot faster than culture).
- ComputerGuru 9y ago
  If this "fix" ends up disabling HT, how can I get a refund not just for the CPU but for the $3k laptop I spec'd around it? Without needing to sue?
  - lorenzhs 9y ago
    That's just the workaround until a fix is available for your CPU, if I understood correctly.
    - ComputerGuru 9y ago
      No, that's not what I meant. In the past, Intel's microcode updates have simply disabled the broken functionality as an official solution. http://techreport.com/news/26911/errata-prompts-intel-to-disable-tsx-in-haswell-early-broadwell-cpus http://techreport.com/news/26911/errata-prompts-intel-to-dis...
      - lorenzhs 9y ago
        You specifically said the fix might be to permanently disable HT. The TSX situation was indeed unfortunate, I have one of the affected CPUs. But it was a new feature that was broken, not something that used to work, so the bug's impact was less serious, and disabling the feature didn't have too much of an impact.
  - brianwawok 9y ago
    Contact your laptop OEM.
    - voltagex_ 9y ago
      Have you ever had to do this? The Dell XPS 9350 (Skylake) has numerous issues with GPU noise, USB-C compatibility, wifi reliability - Dell don't care unless your consumer laws are strong enough to make them care.
      - 9y ago
- sqldba 9y ago
  It would be nice if they allowed users to update rather than vendors. I have a mobile Xeon. I don't know if it's affected or not.
laydn 9y ago
I've done formal verification on several units of a microprocessor, and I can assure you, formal verification on individual FUs is very, very ambitious (think impossible) for a modern microprocessor. For example, you can not possibly formally verify the fetcher unit on its own, because the state space that you need to cover for several cycles for all the module inputs and outputs is beyond the capability of any formal verification tool. Typically, you run formal verification on sub-blocks of sub-blocks of FUs. For this particular bug, it looks like multiple functional units are involved, so it might have been missed by formal verification.
- wyager 9y ago
  > because the state space that you need to cover for several cycles for all the module inputs and outputs is beyond the capability of any formal verification tool. Then use a proof methodology that doesn't require exhaustive enumeration. This objection is actually fairly alarming to me; perhaps there is a larger disconnect between industrial formal techniques for hardware and software than I thought. Strings also occupy a "large state space", but this obviously doesn't prevent us from doing formal verification on functions over strings.
  - Confusion 9y ago
    Then use a proof methodology that doesn't require exhaustive enumeration. You may as well have said "then you use a magical tool that doesn't exist". Strings also occupy a "large state space", but this obviously doesn't prevent us from doing formal verification on functions over strings. What is your reason to think this is 'obviously' the case?
    - wyager 9y ago
      > You may as well have said "then you use a magical tool that doesn't exist". Ok, so what this tells me is that you're not aware of what modern verification techniques look like. There's not really any one resource I can point you to, but take a look at these links. I've used these or similar technologies personally, but there are others I haven't used. https://en.m.wikipedia.org/wiki/Intuitionistic_type_theory https://en.m.wikipedia.org/wiki/Intuitionistic_type_theory https://en.m.wikipedia.org/wiki/Homotopy_type_theory https://en.m.wikipedia.org/wiki/Homotopy_type_theory https://leanprover.github.io/about/ https://leanprover.github.io/about/ http://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf http://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf > What is your reason to think this is 'obviously' the case? Because I've done this, and anyone who claims to be familiar with formal methods should be at least passingly familiar with all the things I mentioned. Even if you aren't, if you've ever heard of SAT (a fairly universal CS concept) you should at least be familiar with the idea that non-exhaustive proofs are a thing.
bsder 9y ago
Formal verification of a decode unit simply will never happen. The complexity is far too high. Formally verifying something like a multiplier block is difficult but doable if you care. Formally verifying an FPU is probably at about the limit. If you want formal verification, you would have to simplify a modern microprocessor a lot.
- wyager 9y ago
  That's the whole point of doing a provably correct transformation from a simpler model domain. Even complicated OOOE engines are fairly tractable if you don't try to implement them at an RTL level... Perhaps we are imagining different formal verification methodologies. Can you tell me what kind of formal verification you're referring to?

heisenbit 9y ago

It may be far better than average software quality but far more also relies on it. The question is whether the quality is adequate in light of what is at stake.

lorenzhs 9y ago
Really? How is it different from a kernel bug that causes random behaviour? Both apparently can be fixed with a software update. They're both bad, but why should Intel be held to a higher standard if mitigation is similarly complex?
- wav-part 9y ago
  Because futher down the stack, more reliable a tech has to be. Otherwise good luck debugging. Also agree with heisenbit.
  - justinclift 9y ago
    Hmmm... on that note, if the universe is a simulation, then a bug in that could have some interesting ramifications. "Don't use the bookshelf over there, physics is broken on that shiny spot." :D
    - roywiggins 9y ago
      The problem with finding a physics bug is that it's liable to be amplifiable. Break conservation laws just a little bit and suddenly you have potential for exponential runaway leading to an unplanned reality excursion, and say goodbye to your light-cone.
      - justinclift 9y ago
        Well, by definition the behaviour would be undefined so could go any which way. ;) Modern day VM software has various levels of exception checking, and code to catch/mitigate/etc when bugs crop up. So, a universe-capable simulator might have any kind of behaviour if/when a bug occurs. It doesn't need to be an unbounded, runaway scenario. :)

autokad 9y ago

i am more willing to accept software having bugs / failing. i have 0 tolerance for hardware to have bugs

baq 9y ago
nobody has, but it ain't easy.
pshc 9y ago
I wonder if there's a CPU out there that doesn't have bugs.
- userbinator 9y ago
  It depends on how exactly you define a bug, but something like a 6502 or Z80, which has essentially all the errata well-documented since it has existed for so long, might qualify.
  - DamonHD 9y ago
    Z80 implementations for one had a whole slew of undocumented instructions, allegedly because they were buggy in some way.
- autokad 9y ago
  stop playing lawyer ball. i'm talking about the bugs that require turning off core functionality (such as hyperthreading) and/or that lead to system halts / corrupted data. yes it happens, but software bugs happen every day where as if your system blue screened every day you know dang well you'd be on the phone with the hardware vendor for a refund / new system.
  - coldtea 9y ago
    >yes it happens, but software bugs happen every day where as if your system blue screened every day you know dang well you'd be on the phone with the hardware vendor for a refund / new system. Well, since hundreds of millions of people use Skylake/Kaby Lake CPUs for 2 years now, and only now we learn about this, obviously this is not of the "system blue screens every day" variety but a very rare bug.

davidmr 9y ago

In my limited experience, their root cause analyses are really impressive as well with lots of internal attention and resources. I'm not allowed to talk about any Intel issues, but we reported a very strange issue to Nvidia, sent a couple of dozen cards back and six months later got a truly fascinating report back we with hundreds of pages of compute test result tables and electron microscope images and chemistry lab reports. Anything that hints of a manufacturing problem is taken incredibly seriously.

baruch 9y ago
I worked for a large company that used thousands of Intel CPUs every year and when we suspected a CPU bug we were mostly brushed off. We had a very persistent person on the team who kept tracking the issue to find correlations and some very good kernel developers that went on to nearly pin-point the issue and only then did Intel pay attention and it then took them still several months to acknowledge the issue give a brief report on the issue and acknowledge that our proposed workaround will indeed work. I've never seen Intel do a very good job at failure analysis or following on with failures unless prodded very hard.
- Sharlin 9y ago
  To be fair, I don't even want to think about the amount of spurious bug reports they are probably receiving.
- deleted 9y ago
  [deleted]
- magila 9y ago
  Intel likely has very thorough data on the issue, but you'll never see it unless you are one of their tier 1 customers* and have an NDA with them. In my experience working for a large hardware manufacturer they are very skittish about releasing detailed failure analysis data to outside companies. * For Intel that would be companies like Dell, Apple, HP, and maybe a couple of others.
dboreham 9y ago

ploxiln 9y ago

That's absolutely true. When it comes to CPU/memory, skilled software engineers always think, "it must be my bug, it always is". So in that super rare case of actually running into a CPU defect, it's a mindfuck, it'll drive you crazy. You'll be looking for the flaw in your algorithm which makes it fail once a week under production load. But you just can't find it, it makes no sense ... (When it comes to drivers for network/storage/graphics etc devices, it's a whole different story. Those things are piles of bugs that need work-arounds in drivers.)

justsid 9y ago
Similarly: Kernel bugs! Once upon a time I spend a good week trying to reproduce a rare crash one of our users saw ever so often (just enough to get our attention, but not enough to get a repro case). Stack traces made no sense and just in general the whole crash made no sense the more I looked at it. Turns out it was a bug in XNUs pthread subsystem, a part where I would have never looked if it weren‘t for desperation, because, well, it‘s the kernel, it works, right?
- digi_owl 9y ago
  Or at least should have been long since spotted thanks to use and abuse.
- wbl 9y ago
  Emacs would regularly panic the kernel on one OS X version when I opened preview to look at a pdf and had TeX recompile.
  - inferiorhuman 9y ago
    The DVD player on OSX with a MacBook (polycarbonate ones) would occasionally cause a kernel panic if you had 4GB of RAM installed.
digi_owl 9y ago
You have some lovely stories online about these things. Like the guy tracking down a stuck bit in RAM. Or on the network level, a VPN that failed only when traversing one possible route between company offices.

dmead 9y ago

IIRC wasn't there some blog posts about how intel has cut their verification/QA drastically since 2010? is this the result?

userbinator 9y ago
Although it mentions 2015, I think that might be the one I linked in my original post above: http://danluu.com/cpu-bugs/ http://danluu.com/cpu-bugs/

gcb0 9y ago

releasing cpu micro code to work around bugs is very cheap.

CountSessine 9y ago
But that doesn't mean you necessarily get to keep the affected feature - the only 'work-around' might be to disable it. Consider TSX on Haswell and Broadwell, where Intel had to disable the whole feature because of a bug. And of course there was the 486 FP bug which couldn't be fixed by any kind of microcode update. If Intel had to completely disable hyperthreading in Skylake and Kabylake that would make the premium anyone paid for i5 vs i7 worthless.
- gcb0 9y ago
  you mean i3 and i7. despite what cpuinfo tells you, no HT in i5. and my previous comment was ironic :)
  - CountSessine 9y ago
    But if you don't have HT in your i7, you basically have an i5 that you paid more than you needed for. Or has that changed? At one point, i7 was full-featured, i5 was an i7 with HT disabled, and i3 was i7 with HT intact but smaller caches. Is that different with Skylake/Kabylake? and my previous comment was ironic :) Ack - sorry. I must be irony-impaired. That's why I don't post very often. :-)
    - theandrewbailey 9y ago
      i3 also has half the cores.
  - happycube 9y ago
    Mobile dual-core lie5's have hyperthreading too.