Приклад 3.1

Формалізоване зображення моделі за допомогою мережі Петрі

Один із найскладніших етапів створення моделі — це вибір методу її формалізації. Зазвичай існує кілька підходів до зображення моделі системи і мережі Петрі. Продемонструємо на прикладах, як перейти від змістовної постановки задачі до формальної моделі.

Покажемо, як за допомогою мережі Петрі можна синхронізувати кілька асинхронних обчислювальних процесів, що виконуються в пам'яті комп'ютера. Розглянемо роботу комп'ютерної системи, в якій два обчислювальні процеси П ₁ і П ₂ намагаються одночасно записати дані в область пам'яті (П ₁) і зчитати з неї дані (П ₂). Проблема, яку потрібно вирішити — синхронізація доступу процесів до пам'яті. Щоб запобігти суперечності, необхідно заборонити одночасний доступ процесів до одної і тої ж області пам'яті. Це означає, що активним може бути тільки один процес, який виконує операцію доступу до пам'яті.

Для формалізації модельованої системи скористаємося семафором, який буде розділяти доступ до області пам'яті. Побудуємо просту мережу Петрі (рис. 3.9), яку можна буде використати для синхронізації цих процесів, і розглянемо її роботу.

Рис. 3.9. Застосування мережі Петрі для синхронізації асинхронних процесів

Кожний обчислювальний процес може перебувати в одному з двох станів: активному або пасивному, які відповідно позначені двома вузлами. Розташування маркерів у мережі, зображеній на рис. 3.7, показує, що в даний момент обидва процеси знаходяться в пасивному стані. Кожний процес може змінити свій стан за допомогою спрацювання переходу. Зміна стану мережі залежить від вузла семафора — S. Розмітка вихідного стану мережі М = [1, 0, 1, 0, 1]. Якщо один процес, наприклад П ₁, намагається змінити свій стан на активний (записати дані), то він збуджує свій перехід і змінює розмітку мережі на М = [0, 1, 0, 0, 1]. Таким чином, збудження переходу процесу П ₂ (зчитування даних з тієї ж області) не станеться доти, доки процес П ₁, не перейде в пасивний стан і розмітка мережі знову не зміниться на М = [1, 0, 1, 0, 1].

Дата добавления: 2014-01-05