ВЕРИФИКАЦИЯ АЛГОРИТМА ДИСПЕТЧЕРИЗАЦИИ ЗАДАЧ МНОГОПРОЦЕССОРНОЙ СИСТЕМЫ С ИСПОЛЬЗОВАНИЕМ СРЕДСТВ STATEFLOW Вашкевич Н.П.,Бикташев Р.А.,Киселев С.В.

Пензенский государственный университет


Номер: 12-1
Год: 2014
Страницы: 42-46
Журнал: Актуальные проблемы гуманитарных и естественных наук

Ключевые слова

системы реального времени, диспетчеризация задач, недетерминированный автомат, модель, верификация, real-time systems, scheduling tasks, nondeterministic automaton, model, verification

Просмотр статьи

⛔️ (обновите страницу, если статья не отобразилась)

Аннотация к статье

В статье рассмотрен алгоритм диспетчеризации с временным разделением задач. Представлено формальное описание алгоритма с использованием аппарата недетерминированных автоматов. Проведена верификация автоматной модели средствами Matlab Stateflow.

Текст научной статьи

Один из подходов, приводящих к значительному повышению производительности современных операционных систем реального времени, состоит в аппаратной поддержке функции диспетчеризации, которая в значительной степени уменьшает время реакции системы на запрос приложения. При этом попутно достигается увеличение надежности и безопасности операционной системы из-за возможности тщательной отладки аппаратуры современными средствами проектирования ПЛИС. Аппаратная поддержка заключается в том, что диспетчер задач должен быть выполнен в виде независимого устройства (сопроцессора) в составе многопроцессорной системы, в аппаратных средствах выполняющего системные вызовы, связанные с переключением контекста [1]. Эффективность такой реализации определяется эффективностью формального описания алгоритма диспетчеризации. Известно, что одним из самых простых, наглядных, компактных и функциональных подходов к формальному описанию алгоритмов управления, в том числе алгоритмов диспетчеризации задач, является метод недетерминированных автоматов (НДА), который кроме всего прочего обеспечивает структурную реализацию управляющего алгоритма [2]. В общем случае алгоритм диспетчеризации в явном виде связан с взаимодействием процессов. С одной стороны задачи, требующие своего выполнения, с другой стороны - обслуживающие их процессорные узлы. Эти действия необходимо синхронизировать таким образом, чтобы обеспечить так называемое «рандеву», когда j - й процессорный узел должен дождаться поступления задачи, а i-я задача - освобождения одного из процессоров, после чего она будет обслуживаться в течение некоторого времени. Следует учесть обстоятельство, что при освобождении нескольких процессоров они могут одновременно обратиться к общей очереди задач, вызывая тем самым конфликт, который разрешается методом взаимных исключений с использованием приоритетов задач. Традиционный подход, связанный с таким обслуживанием аналогичен задаче «спящего парикмахера» [3], который широко применялся для вычислительных систем с одним процессором. Для многопроцессорных систем такой подход должен быть расширен до задачи, которую можно назвать «работа парикмахерской». Эта задача иллюстрирует отношения «клиент-сервер», которые имеют место между процессами в многопроцессорных вычислительных системах. Причем аналогом процессоров являются коллектив парикмахеров, а аналогом задач выступают клиенты парикмахерской [4]. Автоматная модель диспетчеризации задач представляется в виде систем канонических уравнений, описывающих все реализуемые события управляющего алгоритма. Алгоритм работы диспетчера содержит три части: клиентскую (постановка задачи в очередь), серверную (обслуживание процессорами) и «рандеву» (наличие задачи и готовность одного из процессоров к обслуживанию этой задачи) [5]. Для описания алгоритма введены основные частные события, представленные в таблице 1. Таблица 1 Обозначение события Описание частного события в НДА-модели Поступление задачи извне В очереди имеются свободные места Задача в очереди Запрос j-го процессора диспетчером Задача готова к обслуживанию в j-м процессоре, j-й процессор помещается в пул занятых j-й процессор выдал сигнал подтверждение запроса j-й процессор помещается в пул свободных В процессорном пуле имеются свободные процессоры j-й процессор задачу принял j-й процессор выбран для обслуживания задачи j-й процессор выполняет обслуживание задачи Удалить задачу из очереди Снять задачу с исполнения Выполнение задачи закончено Выдача результата выполнения текущей задачи На основании словесного описания алгоритма управления процессами [5] и введенных событий, реализуемых в этом алгоритме, система канонических уравнений, описывающих эти события, будет иметь следующий вид: (t+1) = ; ( t+1) = (t+1) = . (1) - для процесса «сервер», реализуемого процессором до момента рандеву: (t+1) =; (t+1) = . (2) Система канонических уравнений, описывающая события после рандеву (t+1) = ; (t+1)= ; (t+1)= ; (t+1)=; (t+1)=. (3) Для целей верификации проведено моделирование недетерминированного автомата с использованием пакета Stateflow Matlab, описывающего работу диспетчера задач с временным разделением. Автомат разделяется на две части (рис.1): до и после рандеву (до того, как задача поступила в процессор и он готов к её исполнению, и после). В части до рандеву параллельно выполняются две ветви: клиент и сервер. Со стороны клиента происходит выборка задачи и запрос свободного процессора. Со стороны сервера - выбор процессора и принятие задачи на исполнение. Рис.1. Общая модель автомата в Stateflow Клиентская и серверная части алгоритма в Stateflow представлены на рис.2. В клиентской части блок InTask означает поступление задачи в диспетчер извне (моделируется событием ). Блок TaskInQueue означает, что задача помещена в очередь (). Событие QueueNotEmpty () означает, что в очереди есть задачи, ожидающие обслуживания. Блок jProcRequest () означает запрос процессора диспетчером. Событие jProcRequest означает то же самое и используется для осуществления перехода в параллельной ветви. Блок и событие Task_in_Proc () означают, что задача поступила на обслуживание в свободный процессор. Рис. 2. Клиентская и серверная части автомата в Stateflow В серверной части блок FreeProcChoise () означает выбор свободного процессора из их множества. Событие SelectedjProc () означает, что процессор выбран. Блок TaskRequest () означает запрос наличия задачи в очереди. Сигнал [proc_rqstd()] является функцией, которая представляет собой конъюнкцию двух событий: очередь не пуста и диспетчер запрашивает свободный процессор (QueueNotEmpty и jProcRequest). Блок и событие jProcRequested () означают, что свободный процессор ответил на запрос и готов к чтению задачи из очереди. Блок и событие ProcTaskReaded () означает, что задача прочитана процессором и находится на обслуживании. В момент рандеву (см. рис.1) выполняется функция Randezvous(), которая представляет собой конъюнкцию двух событий: задача из очереди поступила на обслуживание в процессор и процессор прочитал задачу из очереди (Task_in_Proc и ProcTaskReaded). Блок jProcessing () означает выполнение задачи в процессоре. Освобождение процессора от задачи реализуется в модели блоками, показанными на рис. 3. Рис. 3. Завершение задачи и освобождение процессора Блок и событие TaskStop () означают, что процессор завершил выполнение задачи. Блок QTaskDelete () означает, что задача удалена из очереди. Запись результатов производится блоками, показанными на рисунке 5. Блок и событие SetResults () означают, что результаты выполнения задачи записаны в память. Блок jProcIsFree () означает, что процессор помещается в пул свободных. В Stateflow можно запустить отладку и наблюдать за работой автомата в целом. Для этого необходимо объявить все сигналы переходов и задать между ними соответствия. После реализации модель была отлажена. Stateflow позволяет создавать различные отчеты по результатам компиляции и отладки. Наибольший интерес вызывает отчет о верификации, представленный на рис. 4. Рис. 4. Результаты верификации автоматной модели Из рисунка можно сделать вывод о том, что все состояния автомата достижимы, все связи и сигналы верные, т.е. алгоритм функционирует правильно. Кроме того могут быть представлены и другие отчеты, например, отчет об ошибках в модели и др. Таким образом, в результате выполнения работы был рассмотрен алгоритм диспетчеризации с временным разделением задач и его НДА-модель, верифицированная с использованием средств Matlab Stateflow. В дальнейшем НДА-модель может быть преобразована в VHDL-модель аппаратного диспетчера задач [1].

Научные конференции

 

(c) Архив публикаций научного журнала. Полное или частичное копирование материалов сайта возможно только с письменного разрешения администрации, а также с указанием прямой активной ссылки на источник.