Параллельная семантика предусловий
Для разрешения парадокса параллельных предусловий выделим три аспекта возникшей ситуации:
- A1 Поставщикам нужны предусловия для защиты тел их подпрограмм. Например, put из классов BOUNDED_BUFFER и BOUNDED_QUEUE требует гарантии неполноты входной очереди.
- A2 Сепаратные клиенты не могут рассчитывать на обычную (последовательную) семантику предусловий. Проверка полноты full перед вызовом буфера еще не дает гарантий.
- A3 Так как каждый клиент может соперничать с другими за доступ к ресурсам, то клиент должен быть готов ждать получения требуемых ресурсов. Наградой за ожидание является гарантия корректной обработки.
Отсюда неизбежен вывод: нам все еще нужны предусловия, но у них должна быть другая семантика. Они перестают быть условиями корректности, как в последовательном случае. Примененные к сепаратным аргументам они становятся условиями ожидания. Их можно назвать "предложениями сепаратного предусловия" и они применяются ко всякому предложению предусловия, содержащему вызов, целью которого является сепаратный аргумент. Типичным предложением сепаратного предусловия является 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 (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, улучшающую переносимость и равнодоступность. Разработчикам приложений и в этом случае будут доступны библиотечные механизмы для изменения принятой по умолчанию политики. |
