Сети Петри и формальные расписания
Формальные модели - корректность параллельных программ
Граф алгоритма отвечает — "какие шаги из-за данных нельзя совместить по времени?" Сеть Петри добавляет — "сколько ресурсов (буферов, слотов, мьютексов) и кто из конкурентов получит право сработать?"
Это учебная, но полезная модель для 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.
Классический учебный пример — два взаимодействующих процесса: два конвейера с общими буферами; пока один переход "забирает" фишку из place, другой ждёт. Так же моделируют пару MPI-процессов с очередью send/recv до анализа кода на C.
Связь с параллельными вычислениями
| Концепция Петри | В программе |
|---|---|
| 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.
Разбор — 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 — от сети Петри к коду
В модели Petri выше места Empty и Full хранят "фишки" свободных и занятых слотов; переход "положить в буфер" требует фишки в Empty и увеличивает Full.
Псевдокод производителя
АЛГОРИТМ ПРОИЗВОДИТЕЛЬ(элемент)
ЖДАТЬ(счётчик_пустых > 0) // слот в буфере свободен
ЗАХВАТИТЬ_МЬЮТЕКС(буфер)
ПОЛОЖИТЬ_В_БУФЕР(элемент)
ОСВОБОДИТЬ_МЬЮТЕКС(буфер)
СИГНАЛ(счётчик_полных) // появился готовый элемент
КОНЕЦ
Псевдокод потребителя
АЛГОРИТМ ПОТРЕБИТЕЛЬ()
ЖДАТЬ(счётчик_полных > 0)
ЗАХВАТИТЬ_МЬЮТЕКС(буфер)
элемент := ВЗЯТЬ_ИЗ_БУФЕРА()
ОСВОБОДИТЬ_МЬЮТЕКС(буфер)
СИГНАЛ(счётчик_пустых)
вернуть элемент
КОНЕЦ
Семафоры реализуют ЖДАТЬ / СИГНАЛ; мьютекс защищает структуру очереди от одновременной записи и чтения.
Справочно на C (POSIX threads)
Код ITЗагрузка примера кода…
| Вызов | Роль |
|---|---|
sem_wait(&empty) | Уменьшить счётчик пустых слотов; блокировка, если буфер полон |
pthread_mutex_lock | Войти в критическую секцию |
push(item) | Добавить элемент (ваша функция) |
sem_post(&full) | Увеличить число готовых элементов |
Полный разбор потоков и mutex — в разделе C++ после изучения языка.