Originally Posted by
Ian W
Someone made the decision that computers for safety critical systems had to be 'formally proved' by mathematics. This was difficult but just about achievable with 'simple' 286 chips with a single core and nothing really clever in its operation. However, with multicore CPUs which are effectively a set of computers working together all dropping and picking up threads of programs, pre-fetching expected code branches based on algorithms, being pre-empted and picking up a new thread etc etc., formal proof becomes impossible or at least an nP problem. Certification testing is going to have to change as it makes no sense to restrict the capability of the CPU in the FMC in this way.
The trend now is towards voting systems, so if one gets it wrong due to a glitch, it gets outvoted. I think the space shuttle had multiple systems with the proviso that one was built by someone else to the same spec but was otherwise completely different just in case the other four processors had a common bug.
It is way harder to have a formally-proven system because quite a bit of what is taken for granted in most computer gear is not allowed because it can't be reliably modelled.