Кодеры за работой. Размышления о ремесле программиста - Сейбел Питер

Стил: Такое случается. Не уверен даже, что столь уж редко, ведь вы конструируете доказательства, отражающие структуру кода. И наоборот, если при написании кода вы держите в уме доказательства, это повлияет на структуру вашей программы. Поэтому нельзя говорить о взаимной независимости кода и доказательства в вероятностном смысле. Но можно задействовать разные инструменты, разные способы мышления.

Программируя, вы погружаетесь в разные локальные мелочи, а инварианты дают глобальный взгляд на программу. И доказательства заставляют эти два взгляда взаимодействовать. Вы видите, как локальные шаги воздействуют на глобальный инвариант, который нужно поддержать.

Вот один из самых интересных случаев в моей практике. Меня попросили написать отзыв на статью Дэвида Гриса для «САСМ». Грис писал о доказательстве правильности параллельного алгоритма сборки мусора. Сьюзен Овицки была студенткой Гриса и разработала кое-какие инструменты для доказательства корректности параллельных программ. А Грис решил применить их к параллельному сборщику мусора, разработанному Дейкстрой. Код занимал где-то полстраницы. А остальная часть статьи содержала доказательство его корректности.

Я зарылся в это доказательство и стал проверять его шаг за шагом. Трудность состояла в том, что каждое выражение в программе могло нарушить любой инвариант, поскольку программа была параллельной. Поэтому Овицки предлагала перекрестную проверку в каждой точке. Потратив на это около 25 часов, я обнаружил, что пару шагов я пройти не могу. И сообщил об этом — оказалось, что в этих местах алгоритма были ошибки.

Сейбел: Итак, алгоритм содержал ошибки, и доказательство их пропустило.

Стил: Да, получилось, что доказательство некорректно. Что-то где-то было упущено. Какие-то детали работы с формулой — формула была почти правильна, но именно «почти». Дело было лишь в том, чтобы поменять местами, например, две строки кода.

Сейбел: Итак, 25 часов ушло на то, чтобы проанализировать доказательство. Вы бы смогли найти ошибку в коде за 25 часов, имея перед собой только код и больше ничего?

Стил: Вряд ли бы я даже понял, что там есть ошибка. Алгоритм был довольно мудреным: я посмотрел бы на код, понял его общий смысл — и не заметил бы неточности. Нужна была очень маловероятная последовательность действий, чтобы она проявилась.

Сейбел: И все выявилось в процессе доказательства, то есть вам не надо было рассматривать различные сценарии типа «что, если» для обнаружения проблемы.

Стил: Верно. Доказательства позволяют представить глобальную точку зрения и предусмотреть все возможности, резюмируя их при помощи очень сложной формулы. И чтобы это получить, приходится проработать кучу формул. Автор переработал статью, она снова вернулась ко мне на рецензию — и хотя я уже проделал это упражнение, пришлось опять потратить 25 часов на проверку доказательства. На этот раз, кажется, все было нормально.

Статья вышла, никто больше не находил в этом алгоритме ошибок. Есть ли они там сейчас? Не знаю. Но доказательство дает мне куда больше уверенности в том, что с алгоритмом теперь все нормально. Надеюсь, я не единственный рецензент, разобравшийся в доказательстве.

Сейбел: Дейкстра говорил, что тестирование не позволяет считать программу свободной от ошибок. Вы всего лишь показали, что ваши тесты ошибок не нашли. Но ведь с доказательствами то же самое — вы всего лишь можете сказать, что ваше доказательство не выявило ошибок.

Стил: Это правда. И вот почему есть отрасль компьютерных наук, изучающая автоматическую проверку доказательств. Надежда на то, что программа проверки доказательства окажется корректной. А она будет корректной при небольшом размере. И сделать ее небольшой гораздо проще, чем проверять доказательство какой-либо достаточно большой программы.

Сейбел: И программа автоматической проверки, проверенная вручную, может сэкономить 25 часов, потраченные вами на изучение доказательства фрагмента кода?

Стил: Да. Точно.

Сейбел: О чем еще вы бы хотели поговорить?

Стил: Мы не коснулись такой темы, как красота программ. А мне хочется сказать об этом пару слов. Некоторые программы буквально поражали меня своей красотой. Например, ТеХ, то есть исходный код ТеХ. METAFONT — в меньшей степени, но не знаю, почему: то ли потому, что я работал с ним меньше, то ли потому, что мне и вправду меньше нравятся структура кода и архитектура программы.

Есть великолепные алгоритмы, которыми я просто восхищался. Я видел чудесные программы для сжатия кода — в те времена у тебя был всего один мегабайт памяти, и это имело значение. Было важно, сколько слов ты используешь — 40 или 30, и люди временами серьезно работали над тем, чтобы ужать программу. Билл Госпер писал эти шедевры из четырех строк, и они творили потрясающие вещи, например с усилителем, подключенным к младшим битам аккумулятора, который в это время тасовал биты.

Это может показаться бессмысленной тратой сил, но одним из лучших моментов в моей карьере был тот, когда я смог сократить программу Госпера из 11 слов до 10. И это — ценой лишь небольшого увеличения времени выполнения программы, ценой малой доли машинного цикла. Я нашел способ сократить код на одно слово, и на это у меня ушло всего лишь 20 лет.

Сейбел: И вот, спустя 20 лет, вы сказали: «Привет, Билл, а представляешь?..»

Стил: Ну, собственно, я не занимался этим все 20 лет, просто 20 лет спустя я вернулся к этой программе, и ко мне пришло озарение: я понял, что, изменив один код операции, я получу константу с плавающей запятой, близкую к тому, что мне нужно. И смогу использовать инструкцию и как инструкцию, и как константу с плавающей запятой.

Сейбел: Прямо «История Мэла, настоящего программиста».

Стил: Точно. Я не хотел бы заниматься этим в жизни, но это был единственный раз, когда мне удалось сократить код Госпера. Это была победа. И это был красивейший кусок кода — рекурсивная подпрограмма для вычисления синусов и косинусов.

Вот такие вещи нас тогда волновали. Во времена IBM 1130 были загрузочные перфокарты: это одна перфокарта, которую надо было класть на верх стопки. Надо было нажать кнопку запуска, машина считывала первую карту и размещала ее содержимое в первых 80 ячейках памяти. Потом она запускала выполнение по указанному адресу. На первой карте была программа для чтения остальных карт. Так и происходила загрузка.

С IBM 1130 трудность состояла в том, что на перфокарте 12 строк, а в машинном слове было 16 бит. Так что на 16-битную инструкцию приходилось 12 бит, то есть некоторые инструкции не помещались на перфокарте. Такие инструкции приходилось собирать с помощью тех инструкций, которые помещались на перфокарте. Возникала сложная система компромиссов, какие инструкции можно использовать: если я использую вот эту инструкцию, мне нужны будут еще вот эти инструкции на перфокарте, просто чтобы собрать ее. Огромная нагрузка плюс размер функции не мог превышать 80 слов. Поэтому приходилось использовать некоторые инструкции и как данные, использовать данные повторно для других целей. Если удавалось впихнуть эту функцию в память, то ее адрес мог использоваться как константа. Такой вот стиль программирования — не то оригами, не то хайку. Я этим занимался несколько лет.

Сейбел: Как вы думаете, те, кто прошел через это, сейчас справляются лучше или хуже других программистов?

Стил: Они приучены работать с ограниченными ресурсами и умеют точно их оценивать.

Сейбел: Точная оценка — полезный навык. Но он может оказаться и вредным, в смысле развития ненужных сегодня навыков.

Стил: Да, можно легко зациклиться на оптимизации чего только можно, даже если такая задача не стоит. Я рад, что мой сын в старшей школе освоил программирование на калькуляторах TI, где тоже были серьезные ограничения по памяти. Он научился представлять данные в сжатом виде, чтобы они подходили для калькулятора. Я не хочу, чтобы ему пришлось заниматься этим все время, но все равно опыт ценный.