Ошибка процессора Intel в 90-х
Мой учитель, который преподает «Логику» в университете, рассказал нам историю о процессорах Intel, которая гласит: в 90-х у Intel была ошибка в вычислении математических функций, таких как sin / cos, закодированных в процессоре. Эта ошибка приводила к несоответствиям в некоторых банковских счетах, в результате чего Intel нанимала логиков, чтобы продемонстрировать правильность кода.
Я попытался поискать эту историю в Интернете, но ничего не нашел. Кто-нибудь знает что-нибудь об этом или может кто-нибудь дать мне какие-то источники?
Ответы
Я подозреваю , что учитель имел в вид на FDIVошибку Pentium , что привело к большому резонансу в средствах массовой информации в то время , и для которых Intel выпустил отзыв.
Эта ошибка приводила к тому, что деление с плавающей запятой в некоторых случаях возвращало неверные результаты. Это не повлияло только на FDIVнекоторые связанные инструкции: другие инструкции деления и остатка, FPTANи FPATAN. К другим тригонометрическим инструкциям относились с подозрением, но в конечном итоге они были очищены, в том числе FSINи FCOS.
Однако кажется маловероятным, что это вызовет проблемы в банках: финансовые приложения обычно избегают представлений с плавающей запятой, поэтому ошибки в инструкции с плавающей запятой вряд ли повлияют на них.
См. Также запись в Википедии об этой ошибке . Другой известной ошибкой Pentium была ошибка F00F , которая не вызывала ошибок вычислений; это могло привести к зависанию, и его обходили специальной обработкой в операционных системах.
Стивен Китт уже дал хороший ответ относительно ошибки FDIV. Я дополню некоторые подробности о том, как Intel нанимает логиков:
Из-за этой ошибки Intel пришлось заменить много процессоров, что было очень дорого. Не желая повторять это, они наняли несколько компьютерных ученых с опытом работы в формальной логике, чтобы доказать правильность алгоритмов, которые будут реализованы в преемниках Pentium. Если вы хотите узнать больше об их исследованиях, ознакомьтесь с публикациями двух из этих ученых:https://www.cl.cam.ac.uk/~jrh13/papers/index.html, https://scholar.google.com/citations?user=MACCA0cAAAAJ&hl=en
У Intel было довольно сложное оборудование для вычисления частного с плавающей запятой таким образом, чтобы получать два бита на итерацию, что требовало наличия довольно большой таблицы, в которой перечислялись все комбинации битовых шаблонов, где часть частного должна быть равна 11 [а не перечисляя все шаблоны по отдельности, в таблице были бы записи, в которых каждый бит может быть 0, 1 или X, так что, например, битовый шаблон 100X01X будет соответствовать 1000010, 1000011, 1001010 или 1001011, поэтому таблица не нуждается в невозможно огромное количество записей]. К сожалению, часть таблицы была повреждена, когда она переносилась из любого инструмента, который использовался для ее создания, в конструкцию микросхемы.
Я нахожу этот подход к делению несколько любопытным, поскольку можно было бы быстро изучить делитель и получить значение, которое при умножении как на делитель (округление в большую сторону), так и на делимое (округление в меньшую сторону) заставило бы новый делитель иметь свой старшие биты равны 0,1111 или 0,11111111, что упрощает извлечение 4 или 8 бит за итерацию. Конечное частное, вероятно, будет немного меньше правильного значения (никогда не больше, учитывая направления округления ранее), но оно будет достаточно близко, чтобы в конце потребовались всего две или три пары шагов последовательного приближения, чтобы очистить вещи. вверх.
В любом случае, высшая ирония с ошибкой Intel FDIV заключается в том, что раньше, в эпоху 386/387, был конкурирующий продукт Weitek, который мог выполнять вычисления с плавающей запятой с одинарной точностью намного быстрее, чем чипы Intel, но этого не произошло. Я вообще не занимаюсь математикой с двойной точностью. Некоторые программы, которые обычно использовали математику двойной точности, поставлялись с версиями для Weitek, которые использовали математику одинарной точности и, таким образом, давали менее точные результаты. Маркетинговая группа Intel решила использовать эту (разработанную и считавшуюся приемлемой) неточность, выпустив рекламу, в которой была показана материнская плата с калькулятором в десять центов, украшенная клоунской графикой там, где должен был стоять процессор, и с надписью «Спросите подлинный Математические сопроцессоры Intel, или кто знает, на какую математику вам придется рассчитывать ".
Я думаю, это, вероятно, относится к ошибке Pentium FDIV (ошибка деления с плавающей запятой).
Я не припоминаю особых проблем с инструкциями по тригонометрии.