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

Как их написать? Функциональные языки неплохо приспособлены для этого. Именно это и происходит, если писать спецификацию в Quick-Check - свойства получаются функциями языка Haskell. Допустим, мы хотим проверить, что функция reverse является своей противоположностью, тогда мы напишем check reverse с типом список из А -> булевское значение. Итак, checkreverse от xs будет: reverse от reverse xs равно xs. Это функция, которая всегда оказывается верной. Функция-свойство. Но она написана на том же самом языке, и это здорово.

Теперь можно думать о статических проверках этого. Это может быть трудно, а может и легко. Но все равно, если свойство записано по всем правилам, это большое облегчение. Можно проверить его путем генерирования тестовых данных - именно это делает QuickCheck.

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

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

Пейтон-Джонс:Правильно. Но в функциональном мире у вас больше шансов. Однако мы все равно слишком долго раскачиваемся, чтобы продемонстрировать это. Так или иначе, первое - это записать свойства.

Мне кажется очень важным уйти от этого глобального подхода, “все или ничего”, в сторону очень полезного статического и динамического тестирования частичных спецификаций. Это повысит вашу уверенность в правильности программы, а на большее рассчитывать нельзя. Даже так называемые полные спецификации не учитывают вещи вроде того, что программа должна работать за 0,1 с или занимать не более 10 Кбайт памяти. Часто в них ничего не говорится о ресурсах, о времени. Даже если программа формально отвечает спецификации, из-за этих мелочей она может работать не так, как нужно. Думаю, мы обманываем себя, когда говорим, что проверили программу и все в порядке. Лучше честно сказать, что мы повышаем свою уверенность в ней. Тут все может начинаться скромно - вы повышаете уверенность на 75%, прикладывая всего 5% от общего количества усилий. Это хороший показатель.

Сейбел:Поговорим о параллелизме. Гай Стил поручил мне задать вам вопрос о транзакционной памяти - спасет она мир или все же нет?

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

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

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

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

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

Сейбел:Если есть блокировка и переменные условия, все по-другому - библиотекарь запирает библиотеку, и никто не может взять книгу до полной реорганизации. Поглядев на эту схему, вы немедленно сказали бы: “Мы не можем запереть библиотеку, пока не закончим”, - запретив выдачу книг, так что пришлось бы изобретать более сложную схему блокировки.

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

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

Пейтон-Джонс:Но кое-что остается неизменным - шифр книги, верно? Есть несколько способов решить задачу. Например, вы можете сказать, что при работе с заглушкой сама библиотека не меняется, меняется только сама книга. Вы не изменяете ее ключевое поле - только значение, где книга в данный момент находится. И теперь каталог может меняться, где бы книга ни была. Это прекрасно и поддается выражению естественным способом.

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