Сети Петри и формальные расписания

НЕ ОБЯЗАТЕЛЬНО

Архитектору Инженеру

Формальные модели - корректность параллельных программ

Граф алгоритма отвечает: «какие шаги из-за данных нельзя совместить по времени?» Сеть Петри добавляет: «сколько ресурсов (буферов, слотов, мьютексов) и кто из конкурентов получит право сработать?»

Это учебная, но полезная модель для deadlock, ограниченных очередей и pipeline с конечной ёмкостью.

---

Элементы сети Петри

Представьте фишки (tokens) как разрешения или заполненные слоты буфера.

Элемент	Обозначение	Смысл
Place (позиция)	○	Условие, буфер, состояние
Transition (переход)	▭	Событие, операция
Token (фишка)	•	Ресурс, факт «условие выполнено»
Arc (дуга)	→	Связь place↔transition

Правило срабатывания: переход enabled, если во всех входных places достаточно фишек. Fire — снять фишки с входов, положить на выходы.

---

Простой пример — producer–consumer

  [P_empty] ──► (Produce) ──► [P_full] ──► (Consume) ──► [P_empty]
                    ▲                                              │
                    └──────────────────────────────────────────────┘

• Одна фишка в P_empty — слот свободен.
• Produce кладёт в P_full; Consume забирает.

Параллелизм: несколько слотов — несколько фишек; конфликт — два перехода борются за одну фишку в одном place.

---

Связь с параллельными вычислениями

Концепция Петри	В программе
Token	Доступный буфер / разрешение
Transition	Оператор / kernel
Conflict	Несколько enabled переходов — выбор
Synchronization	Несколько входов — join (barrier)
Invariant	Сохранение числа фишек — deadlock-free проверки

Invariant analysis находит, например, что сумма фишек в «буферных» places ≤ K — bounded buffer.

---

Диаграмма расписания (Gantt)

Для детерминированного плана на p процессоров — Gantt chart (см. модели):

       t=0    1    2    3    4
CPU0:  [===A===][==C==]
CPU1:       [==B==][==D==]

Сети Петри + временные метки на transitions → Timed Petri nets — модель для оценки makespan при ограниченных ресурсах.

---

Сравнение с графом алгоритма

	DAG алгоритма	Сеть Петри
Фокус	Зависимости данных	Ресурсы и конкуренция
Ветвление	Меньше явно	Conflict / choice
Deadlock	Редко моделируется	Анализ reachability
Применение	Распараллеливание loop	Pipeline, OS, protocols

На практике комбинируют: DAG для «что можно параллелить», Петри — для «сколько экземпляров одновременно».

---

Инструменты

• CPN Tools — Colored Petri Nets для прототипов.
• TINA, LoLA — verification.
• В индustry чаще simulation + metrics, но Петри учат для мышления о concurrency.

---

Мини-задача для закрепления

Смоделируйте 2 workers, 1 queue, capacity 3:

• Places: FreeSlots, JobsInQueue, Processing.
• Transitions: Enqueue, StartJob, FinishJob.

Сколько фишек в FreeSlots initially? При каком расписании queue переполнится?

---

---

Разбор — bounded buffer (ёмкость 2)

Producer–consumer с буфером на 2 слота:

Places:  Empty(2 фишки), Full(0), Ready(0)
Transitions: Produce, Consume

Produce enabled ⟺ есть фишка в Empty. Fire: −1 Empty, +1 Full, положить элемент в буфер.

Consume enabled ⟺ есть фишка в Full. Fire: −1 Full, +1 Empty.

Шаг	Empty	Full	Действие
0	2	0	начало
1	1	1	Produce
2	0	2	Produce (буфер полон)
3	0	2	Produce disabled — блокировка producer
4	1	1	Consume → снова можно Produce

Invariant: Empty + Full + (занятые слоты в буфере) = 2 — переполнение невозможно в корректной сети.

---

Dining Philosophers (учебная классика)

5 философов, 5 вилок; чтобы есть — нужны обе соседние вилки.

• Наивная модель: каждый берёт левую, ждёт правую → deadlock (все держат левую).
• Решение: ordered resource acquisition (сначала вилка с меньшим номером) или ограничение числа одновременно сидящих.

В Petri: вилки = фишки в places; conflict за вилку моделирует mutex. Reachability analysis проверяет, достижимо ли состояние «все ждут».

---

Timed Petri nets

К переходу добавляют время срабатывания τ(t). Makespan = минимальное время до маркировки «все работы выполнены» при ограничении одного экземпляра перехода (один CPU).

Связь с EST/LFT: критический путь в DAG ≈ longest path в timed Petri без resource conflicts.

---

Producer–consumer в коде (POSIX)

sem_t empty, full;
pthread_mutex_t buf_mutex;

// producer
sem_wait(&empty);
pthread_mutex_lock(&buf_mutex);
  push(item);
pthread_mutex_unlock(&buf_mutex);
sem_post(&full);

Семафоры = счётчики фишек в places Empty/Full; mutex = взаимное исключение при доступе к структуре буфера.

---

Что дальше

• Граф алгоритма
• Временной анализ
• Итоги раздела

---