Сети Петри: Моделирование параллельных и асинхронных процессов
По мере развития компьютерных архитектур многоядерные процессоры и распределенные системы стали стандартом. Однако программирование параллельных систем породило новые, сложнейшие классы ошибок: взаимные блокировки (Deadlocks) и состояния гонки (Race conditions). Для строгого математического моделирования и анализа асинхронных, параллельных и недетерминированных систем в дискретной математике был создан мощный аппарат — Сети Петри, предложенные Карлом Адамом Петри в 1962 году.
Сеть Петри графически представляется как двудольный ориентированный мультиграф. В ней существуют элементы ровно двух типов:
- Места (Позиции, Places): обозначаются кружками. Представляют собой состояния системы или условия (например, «буфер свободен», «файл открыт», «ожидание ввода»).
- Переходы (Transitions): обозначаются прямоугольниками или планками. Представляют события или действия, которые могут изменить состояние системы (например, «запись данных», «отправка сообщения»).
Эти элементы соединены направленными дугами (дуги могут идти только от мест к переходам или от переходов к местам). Ключевая особенность Сетей Петри, отличающая их от обычных конечных автоматов, — это маркировка (токены). В местах могут находиться динамические маркеры (точки). Распределение токенов по местам в данный момент времени задает текущее глобальное состояние всей сложной системы.
Динамика системы описывается строгими математическими правилами срабатывания переходов. Переход считается «активным» (готовым сработать), только если во всех его входных местах есть хотя бы по одному токену (выполнены все необходимые условия). При срабатывании перехода он изымает по одному токену из каждого входного места и добавляет по одному токену в каждое выходное место. Поскольку в сети может быть активно сразу несколько переходов, они могут срабатывать параллельно или в недетерминированном порядке, что идеально отражает суть потоков (threads) в операционных системах.
Математический анализ графа достижимости Сети Петри позволяет до запуска кода в продакшен ответить на критические вопросы: обладает ли система свойством живости (liveness) (гарантия того, что система не зависнет навсегда), является ли она ограниченной (не произойдет ли переполнение памяти) и есть ли риск тупиков. Этот аппарат активно применяется при проектировании сложных промышленных контроллеров, протоколов сетевого обмена и верификации бизнес-процессов (BPMN).
