Теория параллельных систем и процессов
АННОТАЦИЯ
курса “Теория параллельных систем и процессов”
Основной целью освоения дисциплины является систематизация знаний в области формальных методов и средств спецификации, анализа и верификации параллельных систем и процессов.
Современный этап развития теоретической информатики характеризуется бурным ростом активности исследований в области разработки формальных методов спецификации, анализа и моделирования параллельных/распределенных систем, имеющих сложную структурную и функциональную организацию. К таким системам относятся коммуникационные протоколы, системы управления производством, распределенные операционные системы и т.д. Разработка корректных систем такого типа - нетривиальная задача, требующая для своего успешного решения проведения комплексных фундаментальных исследований, основанных на различных формальных методах и средствах, которые варьируются в зависимости от класса моделируемых систем, степени детализации их структуры и поведения, а также характера изучаемых проблем. На основе результатов и рекомендаций теоретических исследований ведется поиск и проверка новых архитектурных принципов конструирования параллельных/распределенных систем, изучаются методы распараллеливания алгоритмов и программ, проверяются новые способы организации программ и процессов, обосновываются программные конструкции, вводимые в языки параллельного программирования, отрабатываются методы структурного и семантического анализа параллельных программ и т.д.
В течение трех последних десятилетий теория параллелизма породила большое разнообразие моделей, теорем, алгоритмов и инструментов, предназначенных для спецификации, разработки и верификации параллельных/распределенных систем. Складываются устойчивые системы базовых понятий и общепринятых методик, появляются специальные периодические издания, регулярно проводятся научные конференции, посвященные данной тематике. Всю совокупность теоретических исследований в области параллельной обработки информации будем называть теорией параллельных систем и процессов. Данный раздел теоретической информатики изучает фундаментальные понятия и законы параллельной обработки информации и на основании обнаруженных закономерностей строит более частные формальные модели исследуемых объектов, на которых ставит и решает прикладные задачи.
В начале курса делается краткий экскурс в историю изучаемой теории, рассматриваются предмет и задачи теоретических исследований в области параллельной обработки информации.
Центральное место в курсе занимает теория сетей Петри, которые в являются одним из самых популярных формализмов для описания параллельных систем и процессов. Сети Петри были разработаны и используются, в основном, для анализа и моделирования различных систем. С их помощью могут быть промоделированы аппаратное и программное обеспечение ЭВМ, физические и химические системы, социальные и экономические задачи и др. Наиболее удобны сети Петри для моделирования параллельных систем, причем параллельность моделируется естественным и адекватным образом. В курсе рассматриваются методы анализа сетей Петри, позволяющие изучать поведение и свойства моделируемых систем. Также излагаются наиболее интересные и распространенные обобщения сетей Петри, предложенные для адекватного моделирования реальных параллельных систем, имеющих сложную структуру.
Кроме того, излагается материал по таким семантическим моделям параллелизма, как системы переходов, трассы Хоара, системы переходов с независимостью, трассы Мазуркевича, сети-процессы, частично-упорядоченные множества, структуры событий. Изучаются свойства этих моделей и показываются их достоинства для спецификации и анализа поведения параллельных систем. Рассматриваются различные понятия эквивалентности параллельных процессов, определенные на основе трассового, тестового и бисимуляционного подходов. Устанавливаются взаимосвязи между перечисленными моделями и эквивалентностями с использованием методов теории категорий.
Далее, излагаются базовые понятия и законы алгебраических исчислений параллельных процессов на примере алгебры взаимодействующих процессов (CCS) Мильнера. Также, рассматривается аппарат динамических и темпоральных логик для спецификации параллельных процессов. Обсуждаются основные идеи автоматической верификации параллельных систем (механические доказатели теорем и проверка модели (model cheking)).
Методы теории параллелизма можно успешно применять в самых различных областях. Например, знание основ этой теории становится обязательным для специалистов по вычислительной технике, системному анализу, программированию и др.
Организационно-методический раздел.
1.1Название курса.
Теория параллельных систем и процессов
Направление – Прикладная математика и информатика
Раздел – общие математические и естественно-научные дисциплины
Семестры – п/год. курс
1.2Цели и задачи курса.
Дисциплина "Теория параллельных систем и процессов" предназначена как спец. курс для студентов 3–5 курсов и магистрантов механико-математических факультетов университетов.
Основной целью освоения дисциплины является систематизация знаний в области формальных методов и средств спецификации, анализа и верификации параллельных систем и процессов.
Для достижения поставленной цели выделяются задачи курса:
1) изучение теоретической части курса в соответствии с программой,
2) решение задач по моделированию и анализу поведения параллельных систем с использованием сетей Петри и их расширений в системе PEP в соответствии с учебным планом,
3) сдача экзамена в соответствии с учебным планом.
1.3Требования к уровню освоения содержания курса.
По окончании изучения указанной дисциплины студент должен
- иметь представление о месте и роли изучаемой дисциплины среди других наук;
- знать содержание программы курса, основные достижения в области формальных моделей параллельных систем и процессов;
- уметь применять методы моделирования, анализа и верификации поведения параллельных систем с использованием системы PEP.
1.4Формы контроля
Итоговый контроль. Для контроля усвоения дисциплины учебным планом предусмотрен экзамен.
Текущий контроль. В течение семестра выполняются 2 задания.
2Содержание дисциплины.
2.1Новизна.
Курс «Теория параллельных систем и процессов» концентрирует внимание на фундаментальных знаниях предметной области: современных формальных методах и средствах моделирования, анализа и верификации параллельных/распределенных систем и процессов.
2.2Тематический план курса.
| Наименование разделов и тем | К о л и ч е с т в о ч а с о в | ||||
| Лекции | Семинары | Лаборатор- ные работы | Самостоятель-ная работа | Всего часов | |
| Раздел 1. Введение. | 2 | | | | 2 |
| Раздел 2. Элементы теории сетей Петри | 20 | 20 | | 8 | 48 |
| Раздел 3. Семантические модели параллелизма | 6 | 8 | | 2 | 16 |
| Раздел 4. Алгебраические исчисления параллельных процессов | 4 | 4 | | 2 | 10 |
| Раздел 5. Логики .параллельных процессов | 4 | 4 | | 2 | 10 |
| Итого по курсу: | 36 | 36 | | 14 | 86 |
2.3Содержание отдельных разделов и тем.
Введение
Основные понятия, терминология и основополагающие законы параллельной обработки информации.
Краткий исторический обзор формальных моделей параллельных систем и процессов.
Элементы теории сетей Петри (СП)
Основные понятия и формальные определения теории СП.
Поведенческие свойства СП (живость, справедливость, ограниченность, безопасность) и их анализ.
Подклассы СП (ординарные СП, синхрографы, автоматные сети, сети со свободным выбором, элементарные сетевые системы) и анализ их свойств.
Обобщения СП (ингибиторные сети, сети с приоритетами, дискретно-временные и непрерывно-временные СП, стохастические СП, раскрашенные СП) и анализ их свойств.
Семантические модели параллелизма
Интерливинговая семантика и семантика «истинного параллелизма». Семантика «линейного времени» и семантика «ветвистого времени».
Системы-переходов как пример интерливинговой модели параллельных процессов.
Трассы Хоара и их свойства.
Системы-переходов с независимостью как пример модели с семантикой «истинного параллелизма».
Трассы Мазуркевича и их свойства.
Сети-процессы для моделирования параллельных и недетерминированных процессов.
Частично-упорядоченные множества и их свойства.
Структуры событий и их свойства.
Понятия эквивалентностей параллельных процессов (трассовый, тестовый, бисимуляционный подходы).
Сравнительный анализ параллельных моделей и эквивалетностей на основе теоретико-категорного подхода.
Алгебраические исчисления параллельных процессов
Методы композиции процессов и способы их взаимодействия на примере исчисления взаимодействующих параллельных систем (CCS) Милнера.
Структурная операционная и денотационная семантики исчисления CCS.
Полные системы аксиом.
Логики параллельных процессов
Динамические и темпоральные логики как инструмент спецификации и верификации параллельных процессов.
Методы автоматической верификации. Механические доказатели теорем. Проверка модели (model cheking).
2.4Перечень примерных контрольных вопросов и заданий для самостоятельной работы.
Рассматриваемая задача о шести обедающих философах является модификацией задачи, предложенной Дейкстрой. Шесть философов проводят свое время, размышляя и поедая макароны. Они сидят за круглым обеденным столом, вокруг которого стоят 6 стульев. На столе лежать 6 вилок так, что между каждыми двумя философами лежит одна вилка, т.е. слева и справа от каждого философа находится по вилке. Вилка с номером i находится слева от философа с номером i. Для еды философу необходимо иметь две вилки. Если философ не может немедленно взять две вилки, то он ждет, когда сможет приступить к еде. Вилки поднимаются со стола по одной, причем первой поднимается вилка с четным номером. Закончив еду, философ кладет вилки на стол. С помощью системы PEP построить раскрашенную сеть Петри, моделирующую описанное решение проблемы обедающих, выполнить симуляцию временной сети и проверить ее на свойства живости и ограниченности. Обосновать полученные результаты.
В магазине имеется два типа касс – с терминалом для пластиковых карт и без него. Заказ проходит следующие стадии: 1. чек принимается; 2. если касса оборудована терминалом для пластиковых карт, то происходит списание денег с карты через внутренний банковский терминал (доступ эксклюзивный), иначе принимаются наличные от клиента; 3. происходит регистрация чека во внутренней базе данных (доступ эксклюзивный); 4. чек печатается. С помощью системы PEP построить сеть Петри, моделирующую описанную систему, выполнить симуляцию сети и проверить ее на свойства живости и ограниченности. Обосновать полученные результаты.
Система автомат-продавец состоит из трех различных автоматов M1, M2 и M3 и двух операторов F1 и F2. Оператор F1 воздействует на автоматы M1 и M2, а оператор F2 – на M1 и M3. Заказы требуют двух стадий обработки. Сначала они должны быть обработаны автоматом M1, затем либо автоматом M2 , либо автоматом M3. Заказ может поступать только, если есть свободный оператор. С помощью системы PEP построить сеть Петри, моделирующую данную систему, выполнить симуляцию сети и проверить ее на свойства живости и ограниченности. Обосновать полученные результаты.
Протокол коммуникаций позволяет двум сторонам обмениваться сообщениями по одному через ненадежную среду. Ненадежность среды заключается в том, что сообщения и подтверждения могут теряться при передаче (т.е. не достигать получателя). Для восстановления от потерь при передаче используется механизм повторной посылки сообщения при превышении времени ожидания подтверждения, т.е. время отправления сообщения записывается, и, если по истечении определенного промежутка времени не получено подтверждение, сообщение посылается еще раз и т.д. С помощью системы PEP построить временную сеть Петри, моделирующую данную систему, выполнить симуляцию временной сети и проверить ее на свойства живости и ограниченности. Обосновать полученные результаты.
3Учебно-методическое обеспечение дисциплины
3.1Темы рефератов (курсовых работ).
Не предусмотрено.
3.2Образцы вопросов для подготовки к экзамену.
Вопросы для подготовки к экзамену практически совпадают с программой курса "Теория параллельного программирования". Ниже приводятся образец экзаменационного билета, содержащий два теоретических вопроса и задачу по теме, отличающейся от первых вопросов:
Анализ свойства ограниченности сетей Петри.
Синтаксис исчисления взаимодействующих параллельных систем (CCS) Милнера.
Установить, является ли сеть Петри со свободным выбором живой на основе метода Коммонера.
О
пределить, является ли живой временная сеть Петри.
3.3Список основной и дополнительной литературы.
Ачасова С.М., Бандман О.Л. Корректность параллельных вычислительных процессов. Новосибирск: Наука, 1990. – 252с.
В.А. Вальковский, И.Б. Вирбицкайте. Потоковые вычислительные системы. Системная информатика. Вып. 2. – Новосибирск: Наука, 1993. – 247с.
Вирбицкайте И.Б. Семантические модели параллельных программ и процессов. Уч. пос. НГУ, 1996. – 92с.
Вирбицкайте И.Б. Сети Петри: модификации и расширения. Уч. пос. НГУ, 2005. – 126с.
Карп Р.М., Миллер Р.Е. Параллельные схемы прорамм // Кибернетический сборник. Вып. 13. – М.: Мир, 1976.– с. 5–61.
Котов В.Е. Сети Петри. – М.: Наука, 1984. – 160с.
Питерсон Дж. Теория сетей Петри и моделирование систем. – М.: Мир, 1984. – 264с.
Aura T., Lilius J. Time processes for time Petri nets //Lect. Notes Comput. Sci. – 1997. – Vol. 1248. – P. 136–155.
Dezel J. Esparza J. Free-Choice Petri Nets. Cambridge Tracts in Theoretical Computer Science. – 1994.
Dezel J., Reisig W., Rosenberg G. (Eds.) Lectures on Concurrency and Petri Nets. Lect. Notes Comput. Sci. – 2004. – Vol. 3098.
Engelfriet J. Branching processes of Petri nets // Acta Informatica. – 1991. – Vol. 28. – P. 576–591.
Jensen K. Coloured Petri nets. – Springer-Verlag. – Vol.1,2,3. 1996.
Joyal A., Nielsen M., Winskel W. Bisimulation from open maps //Information and Computation. – 1996. – Vol. 127(2). – P. 164–185.
van Glabbeek R.J., Goltz U. Refinement of actions and equivalence notions for concurrent systems. Acta Informatica. – 2001. – Vol. 37. – P. 229–327.
Mazurkiewicz A. Basic notions of trace theory // Lect. Notes Comput. Sci. – 1988. – Vol. 354. – P. 285–363.
Merlin P., Faber D.J. Recoverability of communication protocols // IEEE Trans. of Communication. – 1976. – Vol. COM-24(9) – (1976).
Milner R. A Calculus of communicating systems // Lect. Notes Comput. Sci. – 1980. – Vol. 92.
Nielsen M., Rozenberg G., Thiagarajan P.S. Behavioural notions for elementary net systems // Distributed Computing. – V.4, N1. – 1990. –p. 45-57.
Pratt V.R. The pomset model of parallel processes: unifying the temporal and the spatial //
Lect. Notes Comput. Sci. – 1985. – Vol. 197. – P. 180–196.
Reisig W., Rosenberg G. (Eds.) Lectures on Petri Nets I, II. Lect. Notes Comput. Sci. – 1998. – Vol. 1491–1492.
Starke P. Some properties of timed nets under the earliest firing time // Lect. Notes Comput. Sci. – 1990. – Vol. 424 . – P. 418–432.
Valero V., de Frutos D., Cuartero F. Timed processes of timed Petri nets // Lect. Notes Comput. Sci. – 1995. – Vol. 935. – P. 490–509.
Rozenberg, J. Engelfriet. Elementary net systems. Lect. Notes Comput. Sci. – 1998. – Vol. 1491. – P. 12–121.
Virbitskaite I. An observation semantics for timed event structures // Lect. Notes Comput. Sci. – 2001. – Vol. 2244. – P. 215–225.
Winskel G. An introduction to event structures // Lecture Notes in Computer Science. – V. 354. – 1988. – p. 364-397.
Winskel G., Nielsen M. Models for concurrency // Handbook of Logic in Comput. Sci. – 1995. – Vol. 4.
3.4Для изучения дисциплин, которые предусматривают использование нормативно-правовых актов, указывать источник опубликования.
Не предусмотрено.
Программу подготовил
д.ф.-м.н., с.н.с. ИСИ СО РАН И.Б. Вирбицкайте
страница 1
скачать
Другие похожие работы: