5 ms·

This seems like precisely the sort of thing that a competent manufacturer should rule out formally. Formal verification of individual FUs isn't exactly ambitiou

by 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?

by wyager 9y ago

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?