18c0693f

Параллельная семантика предусловий


Для разрешения парадокса параллельных предусловий выделим три аспекта возникшей ситуации:

Отсюда неизбежен вывод: нам все еще нужны предусловия, но у них должна быть другая семантика. Они перестают быть условиями корректности, как в последовательном случае. Примененные к сепаратным аргументам они становятся условиями ожидания. Их можно назвать "предложениями сепаратного предусловия" и они применяются ко всякому предложению предусловия, содержащему вызов, целью которого является сепаратный аргумент. Типичным предложением сепаратного предусловия является not b.full для put.

Вот соответствующее правило:

Семантика сепаратного вызова

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

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

Сепаратный объект является свободным, если он не используется в качестве фактического аргумента никакого сепаратного вызова (откуда следует, что на нем не исполняется никакая подпрограмма).

Это правило требует ожидания только для сепаратных аргументов, появляющихся в теле подпрограммы в качестве цели вызова (в нем для соответствующих объектов использовано слово "блокирующий", поскольку они могут заблокировать ее вызов в процессе выполнения).
Для программы в виде "визитной карточки":

r (x: separate SOME_TYPE) is do some_attribute := x endили в каком- либо другом виде, не содержащем вызова вида x.some_routine, не требуется ждать фактического аргумента, соответствующего x.

Если же такой вызов имеется, то для удобства авторов клиентов он должен быть отражен в краткой форме класса. Это будет указываться в заголовке подпрограммы как r (x: blocking SOME_TYPE)...
С помощью нашего правила приведенная выше версия put в классе клиента достигнет желаемого результата:

put (b: BOUNDED_BUFFER [T]; x: T) is require not b.full do b.put (x) ensure not b.empty endВызов вида put (buffer, y) из клиента-производителя будет ждать, пока buffer не станет свободным (доступным) и не полным. Если buffer свободен, но полон, то данный вызов не может выполняться, но какой-нибудь другой клиент-потребитель может получить доступ к буферу (поскольку предусловие not b.empty, интересующее потребителей, будет в данном случае выполнено); после того, как такой клиент удалит некоторый элемент, сделав буфер неполным, клиент-производитель сможет начать выполнение своего вызова.

Как реализации решить, какой из двух или более клиентов, условия запуска вызовов которых выполнены (свободны блокирующие объекты и выполнены предусловия), должен получить доступ? Некоторые люди предпочитают передавать такие решения компилятору. Предпочтительнее определить по умолчанию политику FIFO, улучшающую переносимость и равнодоступность. Разработчикам приложений и в этом случае будут доступны библиотечные механизмы для изменения принятой по умолчанию политики.
Подчеркнем еще раз, что специальная семантика предусловий как условий ожидания применяется только к тому, что мы назвали предложениями сепаратных вызовов, т. е. к предложениям, включающим условия вида b.some_property , где b - это сепаратный аргумент. Несепаратное предложение, такое как i > = 0, будет иметь обычную семантику корректности, так как к нему неприменим парадокс параллельных предусловий: если клиент обеспечивает выполнение указанного условия перед вызовом, то оно будет выполнено и в момент запуска подпрограммы, а если это условие не выполнено, то никакое ожидание не приведет к изменению ситуации.