МОДЕЛИРОВАНИЕ СЕТЕЙ ВРЕМЕННЫХ АВТОМАТОВ С ВОЗМОЖНОСТЬЮ ДИНАМИЧЕСКОЙ РЕКОНФИГУРАЦИИ НА SYSTEMC

SIMULATION OF TIMED AUTOMATA NETWORKS WITH THE POSSIBILITY OF DYNAMIC RECONFIGURATION ON SYSTEMC

Elena Suvorova

PhD. Tech. Sciences, Associate Professor, Saint-Petersburg State University of Aerospace Instrumentation,

Russia, Saint-Petersburg

Syschikov Alexey Yurievich

Scientific researcher, Saint-Petersburg State University of Aerospace Instrumentation,

Russia, Saint-Petersburg

АННОТАЦИЯ

В большинстве современных коммуникационных сетей для высокопроизводительных вычислительных систем необходима динамическая реконфигурация: для адаптации к изменениям режимов функционирования, при парировании отказов, при масштабировании и т.д. Наряду с этим для многих задач, выполняемых в таких сетях, существуют требования реального времени. Поэтому верификация корректности функционирования в ходе динамической реконфигурации очень важна. Для проверки временных характеристик широко используются модели на базе временных автоматов. Но большинство существующих САПР не поддерживает или очень ограниченно поддерживает работу с временными автоматами с динамической реконфигурацией, использование которых необходимо для оценки рассматриваемого класса сетей. В данной статье приводится исследование возможностей SystemC по моделированию сетей с динамической реконфигурацией, показаны основные ограничения и предложен новый подход, позволяющий устранить эти ограничения.

ABSTRACT

In most modern communication networks for high-performance computing systems, dynamic reconfiguration is required for adaptation to changes in operating modes, for fault mitigation, for scaling etc. Along with this, there are real-time requirements for many tasks performed in these networks. Therefore, verification of functioning correctness during dynamic reconfiguration is very important. Timed automata networks are widely used to check time characteristics. But most existing CAD systems do not support or have very limited support for working with dynamic reconfigurable timed automata. This article presents the research of the SystemC capabilities for modelling networks with dynamic reconfiguration, it shows the main limitations, and suggests new approach that allows to eliminate these limitations.

Ключевые слова: временные автоматы, динамическая реконфигурация, системы с требованиями реального времени, адаптивность, высокопроизводительные вычислительные системы

Keywords: timed automata, dynamic reconfiguration, real time systems, adaptivity, high performance computing systems

Введение

Временные автоматы и сети на базе временных автоматов широко используются для моделирования локальных вычислительных сетей для высокопроизводительных вычислительных систем (High Performance Computing HPC) с требованиями реального времени для их формальной верификации и оценки достижимых характеристик [1, 2, 3, 4, 5]. В настоящее время в большинстве HPC сетей необходима поддержка динамической реконфигурации для динамической адаптации к изменениям характеристик потоков данных в ходе функционирования, для парирования сбоев и отказов оборудования, для обеспечения возможностей по масштабированию системы [6, 7, 8, 9]. Оценка характеристик сетей, в ходе функционирования которых может происходить динамическая реконфигурация, с использованием механизмов временных автоматов становится еще более важной вследствие необходимости соблюдения требований реального времени [6, 7, 8].

Существует несколько инструментов, позволяющих осуществлять моделирование, формальную верификацию временных автоматов и сетей на базе временных автоматов, наибольшее распространение получили UPPAAL [10], ITC [11]. Однако, возможности по динамической реконфигурации в них не поддерживаются или очень ограничены [12, 13, 14]. Кроме того, данные инструменты разработаны за рубежом, что может привести к полной невозможности их использования. В данной статье мы рассматриваем возможности по моделированию сетей временных автоматов с динамической реконфигурацией на SystemC, предлагаем подход, позволяющий осуществлять произвольные изменения временных автоматов в процессе моделирования: могут добавляться и исключаться локации, переходы, изменяться атрибуты существующих переходов.

Краткая информация об организации процесса моделирования в SystemC

SystemC представляет собой библиотеку C++, которая обеспечивает возможности по спецификации и последующему моделированию параллельных систем. Моделирование осуществляется под управлением планировщика [14, 15]. На рисунке 1 представлена схема действий, выполняемых планировщиком.

Рисунок 1. Схема действий, выполняемых планировщиком

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

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

Несмотря на то, что SystemC считается библиотекой, обеспечивающей параллельное моделирование, фактически эти процессы выполняются последовательно, в соответствии с очередностью, определяемой планировщиком. Как правило, планировщик устанавливает очередность случайным образом. В разных запусках моделирования она может оказаться различной. Фаза, в которой осуществляется очередное выполнение процессов, называется Evaluate.

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

В конце фазы Update осуществляются присваивания новых значений и модельное время увеличивается на значение дельта. Если по результатам этих изменений на то же самое время (+ дельта) оказываются запланированными еще некоторые процессы, то происходит переход в фазу Evaluate для выполнения этих процессов. В противном случае модельное время устанавливается в значение, на которое запланировано ближайшее следующее событие (события) и запускаются процессы, запланированные на это время. Если не существует никаких запланированных на более позднее время событий, то моделирование завершается.

Необходимые возможности по динамической реконфигурации

Нами было показано в [17, 18, 19], что для обеспечения возможности моделирования динамической реконфигурации сети (изменения структуры, изменения правил функционирования), необходимо в процессе моделирования соответствующей сети на базе временных автоматов:

- добавлять и исключать локации;

- добавлять и исключать переменные;

- изменять инварианты локаций;

- изменять атрибуты переходов;

- добавлять и исключать временные автоматы;

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

Моделирование сетей временных автоматов с возможностью динамической реконфигурации

SystemC предоставляет очень широкие возможности по спецификации и моделированию параллельных систем. Но не все они согласуются с особенностями сетей временных автоматов с возможностью динамической реконфигурации. Нами были проанализированы различные потенциальные варианты представления сети временных автоматов на SystemC. Представление временного автомата как объекта моделирования (наследника класса sc_object) использоваться не может, поскольку наследники этого класса не могут создаваться в процессе моделирования. Представление временных автоматов отдельными процессами не позволяет реализовывать синхронные каналы. Передача токена (события) по синхронному каналу возможна только в том случае, если принимающий автомат находится в одной из локаций, для которых определен переход, связанный с этим синхронным каналом. Планировщик SystemC не может обеспечить такое срабатывание процесса по условию. Для моделирования асинхронных каналов потенциально могут использоваться очереди (sc_queue) SystemC.

На основе проведенного анализа нами был определен следующий подход, обеспечивающий возможность представления и моделирования динамически реконфигурируемых сетей временных автоматов на SystemC. В рамках этого подхода для представления всей сети временных автоматов используется один объект моделирования. Этот объект моделирования соответствует сети временных автоматов. Он включает в себя таблицу, включающую исходный набор локаций всех временных автоматов, соответствующих им атрибутов (инвариантов); таблицу, включающую исходный набор переходов между локациями, соответствующих им атрибутов (условий срабатывания, связанных действий); таблицу указателей на текущие локации для каждого временного автомата; таблицу с исходным набором таймеров и переменных и таблицу с исходным набором каналов между автоматами и их атрибутами (типом канала и типом предаваемых токенов/событий). Данный объект моделирования включает в себя один процесс, который определяет новые значения таймеров и переменных, срабатывания переходов в следующие локации для всех временных автоматов. Этот процесс запускается планировщиком SystemC и функционирует в соответствии с логикой функционирования сети временных автоматов. Он позволяет решить проблему несоответствия логики работы планировщика SystemC и логики функционирования сети временных автоматов. Поскольку планировщик Systemc запускает в данном случае только один процесс, это позволяет также значительно сократить количество событий SystemC, возникающих в процессе моделирования и, тем самым сократить продолжительность процесса моделирования. Взаимосвязь между классическим представлением сети временных автоматов и предложенным табличным представлением, используемым в объекте моделирования, представлена на рисунке 2.

Рисунок 2. Иллюстрация взаимосвязи между классическим представлением временных автоматов и предлагаемым табличным представлением

В [17, 18, 19] нами было определено новое действие, которое может быть связано с переходом – «Изменение». Данное действие позволяет изменять атрибуты существующих переходов и локаций, добавлять и исключать локации, переходы (в том числе добавлять новые временные автоматы, убирать существующие), переменные, каналы. В предлагаемой модели в ходе выполнения этого действия осуществляется модификация соответствующих таблиц.

В реальной сети изменения могут происходить в соответствии с решениями компонентов сети (внутренние события). Например, при увеличении загрузки сети некоторые сетевые узлы могут быть выведены из резерва. Другие изменения происходят под влиянием внешних факторов (внешние события). Например, внешние воздействия могут приводить к отказам сетевого оборудования. В соответствии с решениями извне сеть может масштабироваться, в нее могут добавляться новые компоненты.

Моделирование внутренних событий осуществляется за счет действия «Изменение». Для моделирования внешних процессов исходную сеть временных автоматов мы дополнили временным автоматом (external_manager), представляющим внешние воздействия. Для этого временного автомата может быть определен сценарий поведения, определяющий какие внешние события должны произойти в ходе моделирования. Для таких внешних событий может быть задан тип, атрибуты (в соответствии с типом), время возникновения (фиксированное или случайное). Для реализации событий используется действие «Изменение» также, как и для внутренних событий. Для external_manager наблюдаемы значения всех таймеров и переменных, используемых в основной части сети временных автоматов. Это позволяет связывать действия в сценарии с конкретными состояниями временных автоматов. В частности, это может быть использовано для исследования поведения системы в различных граничных ситуациях. Например, может быть промоделирована ситуация отказа некоторой части оборудования во время процесса динамической реконфигурации. Данный автомат включает в себя одну локацию и один переход из этой локации обратно в нее. Начальное значение инварианта локации, атрибутов перехода прочитывается из сценария. При каждом срабатывании перехода из сценария причитываются следующее значение инварианта локации и атрибутов перехода, которые применяются с использованием действия «Изменение».

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

Заключение

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

Благодарности

Работа выполнена при финансовой поддержке Министерства науки и высшего образования Российской Федерации, соглашение № FSRF-2023-0003, "Фундаментальные основы построения помехозащищенных систем космической и спутниковой связи, относительной навигации, технического зрения и аэрокосмического мониторинга".

Список литературы:

1. Alur R., Dill D. A Theory Of Timed Automata. Theoretical Computer Science. V. 126 (2). № 183. - 1994. - 235 p.
2. Карпов Ю. Г. Model Checking. Верификация параллельных и распределенных программных систем // СПб.: БХВ-Петербург. - 2010. - 560 с.
3. Вельдер С. Э., Лукин М. А., Шалыто А. А., Яминов Б. Р. Верификация автоматных программ // СПб.: Наука, - 2011. 247 с.
4. Alur R., La Torre S., Pappas G. Optimal Paths In Weighted Timed Automata // Lecture Notes in Computer Science. - 2021. № 2034. - pp. 49–62.
5. Andre E., Lime D., Roux O. H. Decision Problems for Parametric Timed Automata // ICFEM Journal. - 2016. - pp. 400–416.
6. Angel J., Keziah A., Saritakumar N. A Survey on Software Defined Networks:Technical Challenges, Recent Advances and Security Issues // International Journal of Engineering Research & Technology (IJERT). – 2017. № 5. – pp. 1 – 10.
7. Ferrer A. J., Marquès J. M., Jorba J. Towards the decentralised cloud: Survey on approaches and challenges for mobile, ad hoc, and edge computing // ACM Computing Surveys. – 2019. № 6. – pp. 1 – 36.
8. Xiao J., Pan X., Liu J., Wang J., Zhang P., Abualigah L. Load Balancing Strategy for SDN Multi-controller ClustersBased on Load Prediction // The Journal of supercomputing. – 2023. № 1. – pp. 1 – 24.
9. Trúchly P., Kubica J. Communication Networks with Multiple SDN Controllers // International Symposium ELMAR. – 2023. – pp. 29 – 32.
10. Home | UPPAAL. - UPPAAL Home URL: https://uppaal.org/ (дата обращения: 22.10.2024)
11. Timed Automata | ITS Tools. - URL: https://lip6.github.io/ITSTools-web/ta.html (дата обращения: 22.10.2024)
12. Tigane S., Guerrouf F., Hamani N. Dynamic Timed Automata for Reconfigurable System Modeling and Verification // Axioms. - 2023. Vol. 12. - pp. 1–230.
13. Bettira R., Kahloul L., Khalgui M., Li Z.Reconfigurable Hierarchical Timed Automata: Modeling and Stochastic Verification / // IEEE International Conference on Systems, Man and Cybernetics. - 2019. - pp. 2364–2371.
14. Bettira R., Kahloul L., Khalgui M. A Novel Approach for Repairing Reconfigurable Hierarchical Timed Automata // 15th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE 2020). - 2020. pp. 398–406.
15. Ventroux N., Peeters J., Sassolas T., Hoe J. C. Highly-parallel special-purpose multicore architecture for SystemC/TLM simulations // International Conference on Embedded Computer Systems: Architectures, Modeling, and Simulation (SAMOS XIV). – 2014. -pp. 250–257.
16. Weinstock J. H., Bucs R. L., Walbroel F., Leupers R., Ascheid G. Work-in-Progress: AMVP - A High Performance Virtual Platform using Parallel SystemC for Multicore ARM Architectures // International Conference on Hardware/Software Codesign and System Synthesis (CODES+ISSS). - 2018. - pp. 1–2.
17. Суворова Е. А. Оценка характеристик программно-реконфигурируемых сетей. СПб.: ГУАП, 2023. 80 с.
18. Суворова Е. А., Чумакова Н. Ю. Методы оценки времени распространения широковещательных сообщений в сетях SpaceFibre в условиях сбоев и отказов с различными вариантами пространственного резервирования // Наукоемкие технологии в космических исследованиях Земли. 2023. Т. 15, № 5. С. 39–56.
19. Olenev V., Suvorova E., Chumakova N. Broadcast Propagation Time in SpaceFibre Networks with Various Types of Spatial Redundancy // Sensors. -2023. 23 p.