понедельник, 5 октября 2009 г.

[comp.prog] Void safety в языке Eiffel

Примечание. Все описанное ниже является моим вольным пересказом статьи Avoid a Void: The eradiction of null dereferencing. Так что, если в моем тексте что-то не понятно, то милости прошу в первоисточник :)

Итак, в недавно вышедшей версии 6.4 продукта EiffelStudio (компилятор языка Eiffel + среда разработки) реализованы изменения в языке Eiffel, которые позволяют устранить проблему обращения по нулевым ссылкам. В языке Eiffel нулевая ссылка – это значение Void. Отсюда и название – Void safety. Изменения в языке Eiffel обеспечивают гарантию того, что обращение вида x.f или x.f(…) будет невозможным для нулевых x.

Обеспечивается это за счет следующих вещей:

  • введением понятия attached и detacheable ссылок;
  • введением понятия Certified Attachment Patterns (CAP) – специальных конструкций языка, которые гарантируют ненулевое значение ссылки;
  • введением специальных конструкций языка – object test-ов, check-инструкций и stable-атрибутов.

Пойдем по порядку. Eiffel – это язык со сборкой мусора. Поэтому практически все пользовательские объекты – это динамически созданные объекты (за исключением т.н. extended-типов, но с ними просто – для них не может быть ссылок, только значения), а доступ к объектам осуществляется через ссылки. Для ссылок ранее было разрешено значение Void (аналог NULL в C-подобных языках). Более того, ранее Void было значением по умолчанию для ссылок.

Сейчас, по умолчанию, ссылки не могут быть нулевыми. Т.е. объявление ссылки вида:

r: MY_TYPE

обозначает, что r не может принимать значения Void (т.е. NULL). А компилятор не позволяет обращаться к r до ее инициализации:

some_method is
  r: MY_TYPE
do
  r.f -- Здесь теперь возникнет ошибка компиляции.
end

Ссылку, которая не может принимать значения Void, можно так же объявить с помощью модификатора attached:

some_method is
  r: attached MY_TYPE
do
  create r
  r.f -- Этот вызов корректен, т.к. ему предшествует инициализация.
end

Если же нужна ссылка, для которой значения Void разрешены, то она объявляется явно как detachable:

r: detacheable MY_TYPE

По умолчанию, все локальные переменные, параметры методов и атрибуты объектов являются attached ссылками. Что, по мнению разработчиков языка, существенно повышает безопасность программирования. А язык берет на себя контроль за тем, чтобы обращение к attached ссылке не происходило без ее инициализации (т.е. присваивания начального значения локальным переменным и атрибутам класса, передачи не-Void значений в качестве аргументов методов).

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

Первой частью этого механизма является CAP (Certified Attachement Patterns) – конструкции языка, которые гарантированно обеспечивают отсутствие Void в переменной-ссылке. Такими CAP служат проверки на равенство/неравенство Void:

x /= Void and then ...
x = Void or else ...

Такие конструкции гарантируют, что в действиях, которые стоят на месте многоточия, ссылка x не может быть нулевой (только если x не является атрибутом объекта, но об этом ниже).

CAP-ы широко применяются для гарантий отсутствия Void в ссылке. Они могут использоваться как в обычных if-ах или условиях циклов, так и в контрактах (пред-, постусловиях и инвариантах циклов и классов). Например, если в предусловии записано:

some_feature (a: detacheable MY_TYPE) is
  require
    a /= Void
    a.f /= 0 -- это обращение к f() безопасно.
do
  ...
end

Здесь обращение a.f во втором предложении контракта гарантированно безопасно, поскольку первое предложение – это CAP, который проверил не равенство Void-у.

Но одних CAP-ов недостаточно, поскольку они не распространяются на атрибуты объекта. А не распространяются потому, что в условиях многопоточности значение атрибута может измениться между двумя соседними точками программы. Например, пусть t – это атрибут класса DEMO. Тогда следующая конструкция не обеспечивает void safety:

if t /= Void then
  t.f -- здесь могут быть проблемы!
end

Поскольку после проверки атрибута t в if-е, вторая нить может вытеснить первую, и изменить значение t. Чтобы этого не происходило, значение t нужно скопировать в новую локальную переменную. И проверять на равенство Void уже эту локальную переменную. Эти действия в языке Eiffel объединены в специальную конструкцию, называемую object test. Вот как это выглядит:

if attached t as l then
  l.f -- здесь обеспечивается Void safety.
end

Еще одной конструкцией, для работы атрибутами объекта являются т.н. stable атрибуты. Если атрибут в классе помечен как stable, то он не может получать значения от detacheable ссылок и выражений. Т.е. контролируется, что если stable-атрибут используется в левой части присваивания, то в правой части присваивания обязательно будет attached значение. Что позволяет использовать stable-атрибут без дополнительных проверок. (Впрочем, данная возможность даже авторами статьи объявляется неоднозначной и, возможно, со временем она видоизменится).

И последняя специальная конструкция для работы с ссылками для обеспечения Void safety является конструкция check. В предыдущих версиях Eiffel она была чем-то вроде assert-а в C-подбных языках и, если не ошибаюсь, могла деактивироваться при компиляции в release-режиме. Для поддержки Void safety эта инструкция получила новую форму:

check attached x as l then
  ... -- какие-то действия над l
end

Т.е. проверяется, равно ли x значению Void. Если равно, то порождается исключение. Если не равно, то значение x присваивается локальной переменной l и выполняются действия внутри then…end.

Вот, пожалуй, и все основные изменения в самом языке. Еще нужно сказать, что, поскольку язык Eiffel поддерживает обобщенное программирование, то теперь при указании параметров шаблонов (используя С++ную терминологию), можно указывать, является ли параметр attached- или detacheable-конструкцией. Т.е. можно написать LINKED_LIST[MY_TYPE] или аналогичный по смыслу LINKED_LIST[attached MY_TYPE], либо LINKED_LIST[detacheable MY_TYPE].

Отдельно проблема шаблонов проявилась в таком библиотечном классе, как ARRAY[T]. Теперь невозможно создать ARRAY без начального значения для всех элементов, если Т является attached параметром – обязательно нужно будет предоставить не равное Void начальное значение.


Теперь несколько слов о том, почему я решил затронуть эту тему.

Во-первых, потому, что разработчики Eiffel утверждают, что Eiffel стал первым промышленным языком программирования, в котором проблема Void safety решена на уровне языка. И, наверное, они правы. Раньше я слышал об аналогичных решениях в Spec# (на который ссылаются и авторы статьи), а так же видел подобное в языке Nice. Но и Spec#, и Nice являются экспериментальными языками, тогда как на Eiffel уже давно пишут серьезный софт в разных прикладных нишах.

Во-вторых, интересен сам факт того, что люди решились на серьезные изменения в языке, которому больше 20 лет от роду. И при этом не потеряли слишком много в совместимости. Так, авторы статьи приводят статистику: при адаптации стандартной библиотеки EiffelBase было исправлено ~11% кода (9093 строки из 82459), а при адаптации оконной библиотеки EiffelVision – меньше 3% (10909 и 376592). Предположительно, в прикладном коде изменений должно быть еще меньше, т.к. работа с Void значениями более характерна для библиотечного кода.

В-третьих, мне понравилось то, какие цели ставили перед собой разработчики Eiffel-я, работая над решением задачи Void safety. Приведу несколько характерных цитат.

Требования к механизму обеспечения Void safety:

1. Static: полная безопасность обеспечивается во время компиляции.
2. General: применим к обобщенным типам и многопоточности.
3. Simple: нет таинственным правилам; для программистов – легкость освоения; для разработчиков компиляторов – легкость воплощения.
4. Compatible: минимальное расширение языка; следование духу языка; отличное сочетание с другими конструкциями; не ограничивает выразительность для программиста; минимальные изменения для существующего кода.

В пояснениях к этим требованиям мне понравилась фраза:

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

Вполне заслуженный камень в огород C++, имхо. Да и современным объектно-функциональным гибридам так же есть о чем подумать (с намеком на контравариантность в Scala).

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

17 комментариев:

Rustam комментирует...

В других языках проблему решают просто запретив NULL. А для алгоритмов требующих NULL например в OCaml есть тип option который может принимать значения Some 'a или None. При использовании ты хочешь не хочешь а будешь "распаковывать" option. Вместо check attached x as l then будет

| Some x -> работаем с x
| None -> обрабатываем NULL.

Хотя то как выковыряли NULL из эйфеля впечатляет :)

eao197 комментирует...

Мне кажется, что Option -- это несколько более общее решение, чем просто защита от NULL. (Кстати, аналогичный Option есть и в Scala -- видимо, это повелось в функциональных языках еще из ML).

А вот как строить односвязный список без NULL, я как-то не очень представляю. Или там так же Option Node стоит в качестве ссылки?

Rustam комментирует...

Нет option не стоит, но самому легко конструировать типы наподобие option, например односвязный список

type 'a lst = Nil | Cons of 'a * 'a lst;;

eao197 комментирует...

Ну так если у тебя есть lst, элементом которого может быть Nil, то не так уж и сложно ошибиться и попытаться обратиться к терминатору списка как к существующему элементу. Если только мне не изменяет мой склероз в OCaml-е.

Rustam комментирует...

Это невоможно :)
Nil тут конструктор типа и его нельзя подсунуть вместо элемента 'a, получить доступ к элементу lst возможно только распарсив через паттерн матчинг:

let rec len = function
| Cons (a, l) -> 1 + len l
| Nil -> 0;;

eao197 комментирует...

Правильно ли я понял, что в OCaml любая структура, где требуется Nil, будет нуждаться в pattern matching-е для работы с ней? И, тем самым, программист вынужден специальным образом обрабатывать Nil значения.

Dmitry Vyukov комментирует...

В мире С++ идея не новая. Достаточно поглядеть на умный указатель из Loki. Его можно параметризовать в том числе политиками, следящими за NULL. Там их штук 5 как минимум, есть и detacheable, и attached, и stable.
Кстати, вот это:
1. Static: полная безопасность обеспечивается во время компиляции.
я так понимаю не выполнено. Да его и не возможно выполнить, оставив язык пригодным для реальной жизни (по крайней мере для императивных). Это работает только для stable, а например преобразование из detacheable в attached всё равно будет проверяться в ран-тайм.

Dmitry Vyukov комментирует...

Вот ссылочка на код из Loki:
http://loki-lib.cvs.sourceforge.net/loki-lib/loki/include/loki/SmartPtr.h?view=markup

Dmitry Vyukov комментирует...

Кстати, что-то подобное я применяю в своём "прототипе SO5". Там у меня есть/предполагается ptr, null_ptr, var_ptr, var_null_ptr. ptr/null_ptr - фактически аналоги attached/detachable.
А ptr/var_ptr отвечают за мутабельность объекта. Это связано с многопоточностью, что бы ран-тайм понимал, когда надо копировать объект, а когда можно безопасно разделять.

eao197 комментирует...

2Dmitry Vyukov: в C++ проблема обращения по NULL -- это не самая большая проблема. Поскольку в C++ есть еще и битые, и повисшие указатели.

А под Static-ом подразумевается, что если компилятор в Eiffel разрешил вызов x.f, значит в этом месте x гарантированно не Void. А то, что этому должны предшествовать run-time проверки, так это очевидно.

Я так понимаю, что выигрыш здесь есть по сравнению с другими языками вот в какой ситуации:

if x /= Void then
x.f
x.g
x.i
x.j
x.k
...
end

При выполнении этих вызовов не нужно проверять x на равенство Void. Тогда как в языке без Void safety проверки могли бы предшествовать каждому вызову. Если только компилятор не применяет какой-либо хитрый алгоритм проверки этой гарантии.

Rustam комментирует...

Правильно ли я понял, что в OCaml любая структура, где требуется Nil, будет нуждаться в pattern matching-е для работы с ней? И, тем самым, программист вынужден специальным образом обрабатывать Nil значения.

Да.

Rustam комментирует...

Dmitry Vyukov

В мире С++ идея не новая.

Угу например тот же Boost.Optional, но проблема в том что не заставишь его работать принудительно.

Да его и не возможно выполнить, оставив язык пригодным для реальной жизни (по крайней мере для императивных).

Можно и в императивных вполне, те же алгебраические типы почти никак на функциональность языка не завязаны, вот в низкоуровневых сложнее.

Kodt комментирует...

Правильно ли я понял, что в OCaml любая структура, где требуется Nil, будет нуждаться в pattern matching-е для работы с ней? И, тем самым, программист вынужден специальным образом обрабатывать Nil значения.

Можно и неисчерпывающий паттерн-матчинг сделать...
match xz with Some x -> работаем с x
к этому компилятор мысленно пририсует ветку
| _ -> матперемат
и предупредит о неисчерпывающем ветвлении.

Kodt комментирует...

В хаскелле, кстати, пошли дальше. Там option = Maybe является монадой+. Соответственно, находясь внутри монады, нарваться на внезапный Nothing нельзя.

Rustam комментирует...

Kodt

В OCaml тоже есть флажок -warn-error P, тогда любые незавершенне матчинги будут ошибкой.

eao197 комментирует...

2Kodt

>Соответственно, находясь внутри монады, нарваться на внезапный Nothing нельзя.

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

eao197 комментирует...

Кстати о простых правилах определения Void/Null значений. Свежая новость о релизе DMD 1.048 и 2.033: Compiler now detects some cases of illegal null dereferencing when compiled with -O

Какие это случаи, по каким правилам идет определение... Фиг знает.