Содержание к диссертации
Введение
1. Логический вывод и верификация параллельных алгоритмов 13
1.1. Подходы к верификации 13
1.2. Формальная верификация алгоритмов и программ 16
1.2.1. Техника дедуктивного анализа 17
1.2.2. Техника проверки эквивалентности 18
1.2.3. Техника проверки моделей 18
1.3. Классическая схема верификации с применением техники проверки моделей 21
1.4. Обзор инструментальных систем формальной верификации 24
1.5. Применение логического вывода для сопоставления реализации и спецификации 31
1.6. Классификация методов логического вывода 32
1.7. Сравнительный анализ методов логического вывода 33
1.8. Выводы 35
2. Формальная верификация параллельных алгоритмов с применением техники проверки моделей и методов логического вывода 37
2.1. Алгоритм формирования базы знаний на основе структуры Крипке и формулы темпоральной логики 37
2.2. Постановка логической задачи формальной верификации 41
2.3. Метод логического вывода для проверки эквивалентности моделей алгоритма и спецификации 41
2.3.1. Унификация литералов 42
2.3.2. Процедуры полного и ограниченного образования остатков 43
2.3.3. Процедура деления дизъюнктов 46
2.3.4. Метод логического вывода делением дизъюнктов на основе определяющего элемента
2.3.5. Схема процесса логического вывода 51
2.3.6. Оценка эффективности метода 55
2.3.7. Анализ особенностей структуры правил в базе знаний 56
2.4. Формирования модели алгоритма 61
2.5. Построение дерева грамматического разбора LTL-спецификации 62
2.5.1. Алгоритм построения дерева грамматического разбора формулы темпоральной логики линейного времени 62
2.5.2. Оптимизация дерева грамматического разбора формулы темпоральной логики линейного времени 67
2.5.3. Метод построения оптимизированного дерева грамматического разбора формулы темпоральной логики линейного времени 75
2.6. Выводы 76
3. Комплекс и машина логического вывода для верификации параллельных алгоритмов 77
3.1. Структура комплекса для формальной верификации параллельных алгоритмов 77
3.2. Модель логического вывода 81
3.2.1. Анализ степени параллелизма используемого метода логического
вывода 81
3.2.2. Древовидное представление модели логического вывода 82
3.2.3. Анализ особенностей модели логического вывода 87
3.2.4. Состояния процессов 91
3.2.5. Типы сообщений 92
3.2.6. Выбор модели вычислений 94
3.2.7. Характеристика модели логического вывода 94
3.3. Машина логического вывода 96
3.3.1. Структура машины 97
3.3.2. Формат фрейма процесса 102
3.3.3. Форматы служебных пакетов и сообщений 105
3.3.4. Форматы данных 108
3.3.5. Принципы организации работы процессора команд 113
3.3.6. Подпрограммы обработки процессов 119
3.3.7. Унификация литералов 122
3.3.8. Начальная инициализация и цикл работы машины 126
3.3.9. Формирование контрпримера 131
3.3.10. Особенности практической реализации машины 131
3.4. Выводы 134
4. Исследование аппаратно-программных реализаций машины логического вывода 136
4.1. Аналитические оценки основных характеристик машины 136
4.2. Программная реализация машины логического вывода 141
4.3. Реализация группы исполнительных процессоров на GPU 144
4.4. Реализация блока унификации на ПЛИС 145
4.5. Оценка производительности реализаций машины логического вывода на тестовых примерах ИС SPIN 148
4.6. Рекомендации по выбору архитектурно-структурных решений машины логического вывода 151
4.7. Выводы 154
Заключение 156
Список использованной литературы 158
- Техника дедуктивного анализа
- Процедуры полного и ограниченного образования остатков
- Древовидное представление модели логического вывода
- Реализация группы исполнительных процессоров на GPU
Техника дедуктивного анализа
Один из подходов – техника дедуктивного анализа – ориентирован на доказательство соответствия логико-алгебраических моделей проверяемых объектов спецификациям, также заданным в виде логико-алгебраических моделей. Суть подхода заключается в анализе справедливости сформулированных теорем, описывающих требования к объекту верификации в выбранной логической системе.
Первые методы дедуктивного анализа были предложены Флойдом и Хоаром в 60-ых годах прошлого века [44]. Способ, предложенный Флойдом, основан на проверке истинности некоторой формулы логики высказываний на всевозможных линейных путях между парами точек сечений, полученных при декомпозиции блок-схемы проверяемого алгоритма [22]. Данный способ обладает существенными ограничениями: в алгоритме не должны использоваться массивы, указатели, подпрограммы и т.д. Впоследствии на основе идей Флойда были разработаны другие методы для более сложных моделей, позволяющие проверять в том числе и параллельные вычисления [2]. Однако общая тенденция осталась неизменной: чем выразительнее используемый логический аппарат, тем удобнее формулировать проверяемые требования и тем более сложной является задача проверки их доказуемости.
Несомненным преимуществом дедуктивного анализа является возможность эффективной проверки моделей с бесконечным числом состояний. Однако существует серьезное препятствие к массовому применению данного подхода – проблема неразрешимости. Обычно в процессе верификации даже относительно простых моделей возникает необходимость во введении и доказательстве ряда вспомогательных теорем. В связи с этим, процесс исследования корректности с использованием данной техники не может быть полностью автоматизирован. Кроме того, применение методов дедуктивной верификации требует серьезной теоретической подготовки и зачастую может осуществляться только экспертами в области математической логики.
Второй подход – техника проверки эквивалентности – применяется в основном для верификации аппаратных систем [44]. Хотя некоторые идеи, заложенные в нем, используются и для проверки корректности программного обеспечения. Задача верификации сводится к проверке согласованности спецификации (то, что требуется от системы) и реализации (то, как система работает на самом деле). При этом как спецификация, так и реализация выражаются с помощью удобных, с точки зрения представления аппаратуры, исполняемых моделей.
В общем случае, проверяемый объект может быть преобразован в отмеченную систему переходов (абстрактную машину), после чего техника проверки эквивалентности применима к нему тем же самым образом, что и к аппаратной системе. Часто задача верификации может быть сведена к задаче выполнимости булевых формул. Для уменьшения вычислительной сложности процесса данные, как правило, представляются в виде специализированных структур [22].
Третий подход – техника проверки моделей (model checking) – может быть охарактеризован как строгая методология, включающая три компонента: исполняемую модель верифицируемой программы или алгоритма, требования, выраженные в виде логико-алгебраической модели, и способ установления соответствия модели объекта анализа предъявляемым требованиям [16, 20]. Проверка моделей, в сравнении с другими подходами, обладает двумя важными преимуществами. Во-первых, вследствие своей универсальности и относительной простоты, процесс верификации может быть полностью автоматизирован. Большая часть основанных на этой технике методов требуют участия специалиста только на этапах описания модели объекта проверки и спецификации. Следствием этой особенности является чрезвычайно высокая вычислительная сложность используемых алгоритмов и большой размер моделей. Другими словами, все формальные методы балансируют между степенью зависимости от эксперта (препятствие для автоматизации; данные могут быть представлены максимально компактно) и вычислительной сложностью (можно автоматизировать; большой объем данных). Model checking позволяет исключить (в некоторых случаях -свести к минимуму) участие человека в процессе верификации. Во-вторых, практически все применяемые способы сопоставления модели и требований в случае получения отрицательного результата позволяют также построить контрпример - последовательность состояний, приводящую к нарушению спецификации. Данный факт значительно облегчает процесс отладки как модели, так и объекта верификации.
Важно понимать, что не существует средств, способных гарантировать корректность анализируемого объекта [16, 20, 44]. Формальная верификация позволяет установить факт соответствия только проверяемым требованиям. Если эти требования не полны, то ошибка может остаться необнаруженной. Тем не менее, формальная верификация часто бывает предпочтительнее тестирования, так как она однозначно устанавливает факт соответствия или несоответствия требованиям. Кроме того, результат верификации с помощью техники проверки моделей точен настолько, насколько точна модель. Возможна ситуация, когда отрицательный результат проверки связан не с ошибкой алгоритма, а с ошибкой построения модели. В таком случае, как правило, исследование причин сбоя обнаруживает погрешность модели. После устранения неточности потребуется перепроверка всех успешно верифицированных ранее свойств. Такой сценарий приводит всего лишь к дополнительным временным затратам. Тогда как противоположная ситуация (положительный результат верификации вследствие погрешности модели) приводит к необнаруженной ошибке. Поэтому важным этапом верификации является этап построения модели объекта исследования достаточного уровня детализации [63].
Однако необходимо помнить, что избыточность усиливает вторую проблему model checking – взрыв числа состояний модели, количество которых растет экспоненциально относительно количества процессов анализируемой программы. Так, например, модели некоторых программ могут насчитывать более чем 10100 – 10200 состояний [16]. Для работы с такими объемами данных используются различные приемы: ленивые способы построения модели, компактные представления данных и т.д.
Известно также несколько высокоэффективных методов формальной верификации, основанных на технике проверки моделей (bounded model checking, probabilistic model checking и т.д.). К сожалению, их общим недостатком является ограниченная применимость. Например, символьные методы оказываются эффективными только в тех случаях, когда удается построить компактную бинарную решающую диаграмму [61], соответствующую объекту верификации. Тем не менее, именно проверка моделей является самой перспективной для массового применения техникой формальной верификации. Доказательством этого утверждения является тот факт, что ее авторы, Эдмунд М. Кларк, Ален Эмерсон и Иосиф Сифакис, в 2007 году были удостоены премии Тьюринга «за их роль в развитии проверки моделей – высокоэффективную технику верификации программ, широко применяемую при разработке как программного, так и аппаратного обеспечения».
Процедуры полного и ограниченного образования остатков
Изображения используемых акторов Композиция введенных типов акторов позволяет получить укрупненную схему логических вычислений для рассматриваемого метода (представлена на рисунке 3.5), которая может быть наглядно изображена в виде ориентированного графа. Связи между вершинами отражают передачу сообщений. Стрелки указывают направление от вершин-родителей к наследникам.
Предлагаемая схема может быть описана на верхнем уровне как группа взаимодействующих V -процессов. В ходе проверки выводимости целевого утверждения d возможно возникновение ситуации, когда для его доказательства потребуется проанализировать истинность некоторых дополнительных утверждений. В этом случае V -процесс инициирует создание вспомогательных V -процессов (наследников по отношению к исходному), выполняя переадресацию на каждый из них решения одной подзадачи (вывод одного вспомогательного утверждения). После этого исходный V -процесс переходит в состояние ожидания и пребывает в нем до тех пор, пока процессы-наследники не завершат свою работу. Выводимость или невыводимость d определяется путем анализа результатов, полученных от процессов-наследников.
Процесс логического вывода завершается, когда заканчивает свою работу активированная первой V -вершина. Результат вывода может быть получен на выходе P данной вершины.
После активации актора V всегда происходит порождение группы из N -процессов и, иногда, группы из M -процессов. Каждый M -процесс способен также порождать группу M -процессов. Кроме того, и N -процесс, и M -процесс инициируют создание группы U -процессов.
На основе укрупненной схемы логических вычислений и блок-схем из приложения Ж может быть построена схема потока логических вычислений, раскрывающая содержание V-, N- и M -процессов. Схема представлена на рисунке 3.6.
После активации V -процесса происходит выборка базовых правил из всего множества утверждений, содержащихся в базе знаний. На данном этапе по ряду эвристических признаков могут быть отсеяны правила, деление которых на цель d гарантированно приведет к получению результата q = 1 (делитель и делимое не имеют одноименных литералов). Затем V -процесс создает группу из N-процессов, каждому из которых передается свое базовое правило и цель вывода d, после чего V -процесс переходит в состояние ожидания результатов работы порожденных вершин.
Каждый N -процесс выполняет построение матрицы частных производных для процедуры ограниченного образования остатков, анализирует полученные результаты и передает их родительской V -вершине. Возобновивший, после получения всех результатов, работу V -процесс выполняет комплексный анализ полученных от всех N -потомков данных. После этого возможен один из трех вариантов действий.
Имеются N -процессы, завершившиеся с результатом q = 1 и непустым множеством остатков. В таком случае будет выполнена операция разбиения дизъюнкта d, сформировано выходное множество текущих остатков C и построено множество Md, включающее в себя вспомогательные цели, полученные в результате разбиения d.
В последнем случае производится выборка необходимых фактов из базы знаний и дополнение полученных в результате работы N -процессов остатков-делителей их инверсиями. V -процессом создается группа из М -процессов, каждому из которых на вход передается своя пара из остатка-делимого и остатка-делителя, после чего V -процесс переходит в состояние ожидания результатов работы вершин-наследников.
М -процессы выполняют построение матрицы частных производных для процедуры полного образования остатков и анализируют полученные результаты. В итоге происходит или передача полученного от деления множества остатков родительской V -вершине (если q = О или q = 1), или инициируется запуск группы вспомогательных М-процессов (если q = g). В обоих случаях М-процесс завершается. После завершения всех порожденных М -процессов, V -вершина возобновляет свою работу.
Полученные от М -процессов остатки обрабатываются в соответствии с формальным описанием метода вывода. Если это возможно, выносится заключение о выводимости утверждения d. В противном случае выполняется построение конъюнкция остатков, формируется множество Md и подготавливается выходное множество текущих остатков.
Элементы множества Md являются вспомогательными целями, доказательство которых необходимо для формирования заключения о выводимости d. Таким образом, выполняемая V -вершина порождает группу вспомогательных V -вершин, задачей каждой из которых будет доказательство своего утверждения из Md. Родительская V -вершина при этом перейдет в состояние ожидания.
Древовидное представление модели логического вывода
Анализ потока логических вычислений позволяет сделать следующие выводы. Степень параллелизма предлагаемой модели логического вывода определяется степенью параллелизма используемого метода: распараллеливание сохраняется на всех уровнях (от V - до U -процессов). Момент готовности к активации вершины определяется исключительно готовностью входных данных. При этом факты и утверждения базы знаний статичны, то есть неизменны в процессе вывода. Это делает возможным подачу множеств KBf и KBr на входы всех V -вершин в начале вычислений, что позволят значительно снизить затраты на коммуникационные расходы.
Процесс выполнения V -вершины нетривиален, и не сводится к линейным вычислениям. В зависимости от полученных из вершин-наследников результатов ход работы данного актора может изменяться. Вследствие этого, при переходе V -вершины к ожиданию требуется сохранять внутреннее состояние актора для последующего восстановления при продолжении исполнения. Аналогичные рассуждения справедливы в отношении N - и M -акторов.
Этап анализа полученных результатов в V -вершине может выполняться в соответствии с двумя стратегиями: полный анализ после завершения работы всех процессов-наследников или частичный анализ после завершения работы каждого процесса-наследника. Первый вариант позволяет сократить трафик сообщений, однако потенциально способен повлечь лавинообразное увеличение числа процессов (вершины, результат которых уже не является необходимым, продолжают свою работу). Второй вариант предполагает вывод родительского процесса из состояния ожидания для определения возможности формирования заключения и остановки прочих выполняемых наследников после завершения каждого процесса-наследника, что в некоторых случаях приводит к сокращению числа процессов, требующих обработки, за счет увеличения трафика сообщений. Допускается также гибридное совмещение описанных стратегий – в соответствии с заданным эвристическим критерием процессы-наследники при своем завершении посылают или не посылают родительскому процессу сообщение о необходимости частичного анализа результатов. Эффективность гибридной стратегии полностью определяется используемым критерием. Примером более или менее удачного критерия может служить правило: «Если текущий V -процесс завершился с заключением P = 1, а целевое утверждение d представляет собой инверсию литерала, полученного при выполнении операции разбиения дизъюнкта, то следует инициировать частичный анализ результатов для родительской вершины». Применение более сложного критерия может привести к большему сокращению издержек, однако, необходимо принимать во внимание и повышение затрат на проверку его выполнимости.
Целесообразность выбора конкретной стратегии имеет прямую зависимость как от характеристик аппаратно-программной платформы, на которой реализуется метод, так и от особенностей задач предметной области. В каждом случае приблизительные оценки эффективности могут быть получены путем предварительного программного моделирования.
В ходе выполнения логического вывода каждый существующий процесс может находиться в одном из следующих состояний. - RUN - процесс находится на выполнении. Данное состояние означает, что процесс исполняет некоторые действия и занимает вычислительные ресурсы. - READY - процесс находится в состоянии готовности. Данное состояние означает, что процесс готов к выполнению, однако в системе нет необходимого количества свободных вычислительных ресурсов для перевода процесса в состояние RUN. Совокупность всех готовых к выполнению процессов образует очередь задач. - WAIT - процесс находится в состоянии ожидания. Данное состояние означает, что ранее процессом были порождены процессы-наследники и в настоящий момент ожидается их завершение. Полученные от наследников результаты необходимы для дальнейшего продолжения работы. В состоянии WAIT могут находиться только V -, N - и M -процессы.
Выполнение V -актора представляет собой цикл из последовательно сменяющихся состояний READY-RUN-WAIT. N- и M -акторы последовательно проходят состояния READY-RUN-WAIT-READY-RUN. U-актор единожды пребывает в состоянии READY, после чего переходит в состояние RUN.
Механизм передачи сообщений между акторами обеспечивает согласованную работу процессов. В структуре сообщения может быть выделено два уровня. Информационный - на этом уровне происходит передача данных между родителем и наследником, и обратно. Управляющий - на этом уровне происходит передача сигналов, оказывающих влияние на состояния взаимодействующих акторов.
Таким образом, сообщения могут рассматриваться как информационно-управляющие связи между находящимися в отношении родитель-наследник вершинами модели логического вывода.
Для рассматриваемой модели оказывается достаточным двух типов сообщений, впервые введенных при разработке классической модели И-ИЛИ процессов Конери [54].
Порождение вспомогательных процессов производится посредством сообщения CREATE. При этом на информационном уровне происходит передача данных из соответствующих полей сообщения в контекст создаваемого процесса. На управляющем уровне происходит два события. Во-первых, осуществляется диспетчеризация процессов. Только что активированный путем подачи на его вход всех данных процесс переходит в состояние READY и помещается в очередь задач. Если в системе присутствует требуемое количество свободных ресурсов, то процесс может быть сразу же передан на выполнение (переходит в состояние RUN ). Во-вторых, в некоторых ситуациях изменяется число процессов наследников, в состоянии ожидания результатов от которых находится родительский актор. Так, при порождении M -вершиной группы вспомогательных M -вершин, требуется соответствующим образом увеличить число наследников родительской V -вершины.
Передача результатов от актора-наследника к актору-родителю обеспечивается сообщением END. На информационном уровне наследник передает данные в специально отведенную область сбора результатов родительского процесса. На управляющем уровне, если были получены отклики от всех процессов-наследников (или же применяется стратегия частичного анализа), родительский процесс переводится в состояние READY и осуществляется диспетчеризация.
Кроме того, для экстренной остановки «ненужных» процессов необходимо использовать сообщение CA NCE L. При этом передача данных на информационном уровне не выполняется. На управляющем уровне происходит полное освобождение занятых останавливаемым процессом и его наследниками ресурсов без анализа каких-либо результатов. Однако следует заметить, что «ненужными» могут являться только вспомогательные по отношению к какому-либо актору процессы. Также остановка процессов выполняется одновременно с завершением этого актора и передачей его результатов родителю. Поэтому сообщение CA NCE L может быть успешно совмещено с сообщением E ND.
Реализация группы исполнительных процессоров на GPU
В качестве тестового пакета для оценки производительности реализаций предложенной МЛВ и подтверждения корректности полученных результатов использовался набор из десяти тестовых примеров ИС SPIN.
Взаимное исключение с помощью мьютекса. Для реализации мьютекса [88] проверялось свойство класса живости: «каждый клиентский процесс рано или поздно обязательно получит доступ к разделяемому ресурсу». Процесс верификации данного примера рассмотрен в приложении М.
Взаимное исключение с помощью дополнительных переменных. Реализация [93] исследовалась на соблюдение свойства безопасности: «доступ к разделяемому ресурсу в каждый момент времени будет иметь не более чем один клиент».
Алгоритм работы сетевого генератора данных. В алгоритме работы сетевого генератора данных [93], посылающего циклически через фиксированный временной промежуток в буферизированный канал сообщение одного из двух возможных типов, устанавливалась достижимость ситуации, когда буфер канала будет полностью занят сообщениями первого типа. Данный пример рассмотрен подробнее в приложении М.
Протокол альтернирующего бита (ABP). Предложенная в [88] реализация протокола обмена информацией между двумя процессами (А – отправитель, B – получатель) проверялась на соответствие условию корректной работы: «каждое сообщение, генерируемое процессом А, будет отправлено без ошибки хотя бы один раз и будет принято процессом B не более одного раза». Кроме того, определялась достижимость циклов без прогресса: «процесс А не посылает сообщения, а процесс B не принимает сообщения».
Протокол с положительным подтверждением и повторением передачи (PAR). Реализация протокола PAR [16], являющегося модификаций ABP, исследовалась на соответствие следующей спецификации: «Если процесс А послал сообщение, то пока процесс B не примет это сообщение, А не будет посылать следующее, и, если процесс В принял сообщение, то он не будет принимать другого сообщения, пока процесс А не пошлет следующее; кроме того, если процесс А послал сообщение, то когда-нибудь в будущем он обязательно сможет послать следующее сообщение».
Алгоритм двухфазной фиксации. Для реализации [16] алгоритма двухфазной фиксации, применяемого в распределенных базах данных для обеспечения целостности, устанавливалась истинность того факта, что решение о фиксации или отклонении транзакции, реализуемое каждым из серверов, всегда совпадает с глобальным решением, принятым менеджером транзакций.
Алгоритм планирования sleep-wakeup. Реализация алгоритма [93] исследовалась на соответствие свойству класса живости: «клиентский процесс никогда не останется навсегда в состоянии ожидания». Верификация данного алгоритма рассмотрена подробнее в приложении М. I-протокол Тэйлора. Предназначенная для минимизации числа управляющих сообщений и ретрансляций свободная версия GNU UUCP протокола проверялась на достижимость тупиковых ситуаций. Подробное описание модели представлено в работе [58].
Алгоритм функционирования устройства управления парогенератором. Реализация алгоритма, предложенная в работе [103], исследовалась на предмет отсутствия ситуаций взаимоблокировок (deadlock и livelock). Кроме того, осуществлялась проверка набора выраженных с помощью формул LTL свойств, подробное описание которых также содержится
Протокол обмена данными сети Cambridge Ring. В реализации протокола [93] осуществлялась проверка условий корректной передачи сообщений.
Исходные описания задач на языке Promela были преобразованы в эквивалентные структуры Крипке. После чего оценивалось время решения каждой задачи в ИС SPIN и с помощью различных реализаций МЛВ (для реализаций на CPU и CPU+GPU - экспериментально, для реализации на ПЛИС -по аналитической формуле (4.4) при CEPFPGA =16).
Тестирование выполнялось на ЭВМ с представленной в пункте 4.4 конфигурацией. При верификации в ИС SPIN применялась редукция частичных порядков, выполнялся подбор оптимальных размеров стека и хэш-таблицы. Прочие оптимизации не использовались. SPIN функционировал в многопоточном режиме (применялась директива _DNCORE=4). В состав CPU и CPU+GPU программных реализаций МЛВ были включены четыре и шестнадцать ИП соответственно. Сбор статистики и отладочной информации не выполнялся. Использовалась консольная реализация CPU+GPU МЛВ.
Каждый тестовый пример верифицировался 120 раз, после чего отбрасывались десять наилучших и наихудших временных результатов. Итоговое время рассчитывалось как среднее арифметическое оставшихся величин. Полученные в ходе экспериментов результаты совпали с результатами SPIN с точностью до контрпримера, что является доказательством корректности предложенного подхода. Полученные значения времени выполнения верификации представлены в таблице 4.3. Для реализаций МЛВ в скобках приведено ускорение.
Анализ результатов показывает, что при программной реализации МЛВ время решения тестовых задач, в целом, сравнимо с временем верификации в ИС SPIN (превосходство программной реализации МЛВ в среднем составляет 15%). Реализация группы ИП на GPU также приносит незначительный положительный эффект при верификации задач относительно большого размера. Серьезного превосходства над ИС SPIN удается добиться при аппаратной реализации МЛВ на ПЛИС (или, в дальнейшем, на заказной СБИС).
Эффективным решением для предотвращения возникающего на некоторых примерах экспоненциального роста числа литералов в выводимых дизъюнктах является выборочный (при превышении порогового значения) отказ от формирования конъюнкции полученных остатков и порождения вспомогательных F-акторов в пользу порождения инверсных К-акторов для каждого полученного остатка.
Расчет значений коэффициентов и и и" целесообразно выполнять с применением математического аппарата теории вероятностей. При этом допустимо считать, что величины Sc и SP подчиняются равномерному распределению, а величина 5Ь - распределению Вейбулла.
При условии применения гарантированно результативных эвристик для инициирования частичного анализа результатов коэффициент у, определяющий частоту неуспешного анализа, принимается равным нулю. Таким образом, множитель (1 + у), входящий в состав формул (4.2) и (4.4) может быть опущен. Примером результативной эвристики, наряду с приведенным в пункте 3.2.3 критерием, является следующее правило: «Если при завершении М-актора был получен результат q = 0, то следует инициировать частичный анализ результатов для родительской вершины».
В целях сокращения времени ожидания ответов на запросы динамическая область РП может быть реализована в виде нескольких независимых банков, при этом группа исполнительных процессоров разделяется на подгруппы, каждой из которых сопоставляется свой банк. Процессору команд предоставляется доступ ко всем банкам. Недостатком данной схемы является необходимость введения дополнительных устройств для организации взаимодействия между банками, исполнительными процессорами, процессором команд и диспетчером памяти.
