Правила обоснования корректности: разоблачение предателей
Так как для сепаратных и несепаратных объектов семантика вызовов различна, то важно гарантировать, что несепаратная сущность (объявленная как x: T для несепаратного T) никогда не будет присоединена к сепаратному объекту. В противном случае, вызов x.f (a) был бы неверно понят - в том числе и компилятором - как синхронный, в то время как присоединенный объект, на самом деле, является сепаратным и требует асинхронной обработки. Такая ссылка, ошибочно объявленная несепаратной, но хранящая верность другой стороне, будет называться ссылкой-предателем (traitor). Нам нужно простое правило обоснования корректности, чтобы гарантировать отсутствие предателей в ПО, а именно, что каждый представитель или лоббист сепаратной стороны надлежащим образом зарегистрирован как таковой соответствующими властями.
У этого правила будут четыре части. Первая часть устраняет риск создания предателей посредством присоединения, т. е. путем присваивания или передачи аргументов:
|
Правило (1) корректности сепаратности Если источник присоединения (в инструкции присваивания или при передаче аргументов) является сепаратным, то его целевая сущность также должна быть сепаратной. |
Присоединение цели x к источнику y является либо присваиванием x := y , либо вызовом f (..., y, ..), в котором y - это фактический аргумент, соответствующий x. Такое присоединение, в котором y сепаратная, а x нет, делает x предателем, поскольку сущность x может быть использована для доступа к сепаратному объекту (объекту, присоединенному к y) под несепаратным именем, как если бы он был локальным объектом с синхронным вызовом. Приведенное правило это запрещает.
|
Отметим, что синтаксически x является сущностью, а y может быть произвольным выражением. Поэтому нам следует определить понятие "сепаратного выражения". Простое выражение - это сущность; более сложные выражения являются вызовами функций (напомним, в частности, что инфиксное выражение вида a + b формально рассматривается как вызов: нечто вроде a.plus (b)). Отсюда сразу получаем определение: выражение является сепаратным, если оно является сепаратной сущностью или сепаратным вызовом. |
p> Как станет ясно из последующего обсуждения, присоединение несепаратного источника к сепаратной цели безвредно, хотя, как правило, не очень полезно.
Нам нужно еще дополнительное правило, охватывающее случай, когда клиент передает сепаратному поставщику ссылку на локальный объект. Пусть имеется сепаратный вызов:
x.f (a),в котором a типа T не является сепаратной, а x является. Объявление процедуры f в классе, порождающем x, будет иметь вид:
f (u:SOME_TYPE)а тип T сущности a должен быть совместен с SOME_TYPE. Но этого недостаточно! Глядя с позиций поставщика (т. е. обработчика x) объект O1, присоединенный к a, расположен на другой стороне - имеет другого обработчика, поэтому, если не объявить соответствующий формальный аргумент u как сепаратный, он станет предателем, так как даст доступ к сепаратному объекту так, как будто он несепаратный:
Рис. 12.5. Передача ссылки в качестве аргумента сепаратному вызову
Таким образом, SOME_TYPE должен быть сепаратным, например, это может быть separate T. Отсюда получаем второе правило корректности:
|
Правило (2) корректности сепаратности Если фактический аргумент сепаратного вызова имеет тип ссылки, то соответствующий формальный аргумент должен быть объявлен как сепаратный. |
Иллюстрируя эту технику, рассмотрим объект, порождающий большое число сепаратных объектов, наделяя их возможностью обращаться в дальнейшем к его ресурсам, т. е. говоря им: "Вот вам моя визитная карточка, звоните мне, если потребуется". Типичным примером будет ядро операционной системы, которое создает сепаратные объекты, оставаясь готовым выполнять операции по их запросам. Создание объектов будет иметь вид:
create subsystem.make (Current, ... Другие аргументы ...),где Current - это визитная карточка, позволяющая subsystem запомнить своего создателя (progenitor) и в случае необходимости попросить у него помощь.
Поскольку Current - это ссылка, то соответствующий формальный аргумент в make должен быть объявлен как сепаратный. Чаще всего make будет иметь вид:
make (p: separate PROGENITOR_TYPE; ... Другие аргументы ...) is do progenitor := p ... Остальные операции инициализации ... endпри котором значение аргумента создателя запоминается в атрибуте progenitor объемлющего класса. Второе правило корректности сепаратности требует, чтобы p была объявлена как сепаратная, а первое правило требует того же от атрибута progenitor. Тогда вызовы ресурсов создателя вида progenitor.some_resource (...) будут корректно трактоваться как сепаратные.
Аналогичное правило нужно и для результатов функций.
|
Правило (3) корректности сепаратности Если источник присоединения является результатом вызова функции, возвращающей тип ссылки, то цель должна быть объявлена как сепаратная. |
|
Правило (4) корректности сепаратности Если фактический аргумент или результат сепаратного вызова имеет развернутый тип, то его базовый класс не может содержать непосредственно или опосредовано никакой несепаратный атрибут ссылочного типа. |
Рис. 12.6 иллюстрирует случай, когда формальный аргумент u является развернутым. Тогда при присоединении поля объекта O1 просто копируются в соответствующие поля объекта O'1, присоединенного к u (см. лекцию 8 курса "Основы объектно-ориентированного программирования"). Если разрешить O1 содержать ссылку, то это приведет к полю-предателю в O'1. Та же проблема возникнет, если в O1 будет подобъект со ссылкой; это отмечено в правиле фразой "непосредственно или опосредовано".
Рис. 12.6. Передача объекта со ссылками сепаратному вызову
Если формальный аргумент u является ссылкой, то присоединение является клоном; вызов будет создавать новый объект O'1, как показано на последнем рисунке, и присоединять к нему ссылку u. В этом случае можно предложить перед вызовом явно создавать клон на стороне клиента:
a: expanded SOME_TYPE; a1: SOME_TYPE ... a1 := a; -- Это клонирует объект и присоединяет a1 к клону x.f (a1)Согласно второму правилу корректности формальный аргумент u должен иметь тип, согласованный с типом сепаратной ссылки separate SOME_TYPE. Вызов в последней строке делает u сепаратной ссылкой, присоединенной ко вновь созданному клону на стороне клиента.
