О преподавании формальных моделей и алгоритмов анализа параллельных систем


https://doi.org/10.18255/1818-1015-2015-6-783-794

Полный текст:


Аннотация

В настоящее время наблюдается огромный практический интерес к параллельному программированию. Этот интерес обусловлен доступностью супер-ЭВМ, компьютерных кластеров и мощных графических процессоров для массового использования в вычислительной математике и компьютерном моделировании. Кроме того, такие технологии параллельного программирования, как MPI, OpenMP и CUDA, позволяют использовать безопасным образом опыт программирования на классических языках Си и FORTRAN для ускорения вычислений, избегая конфликтов (“гонок”) из-за ресурсов. Однако такой прогресс параллельного программирования не означает, что конкуренция из-за ресурсов не может возникать в параллельных общего вида, в так называемых распределенных системах в частности. Поэтому остается актуальным изучение и преподавание формальных моделей параллелизма и средств верификации поведенческих свойств параллельных (распределенных) систем. В статье представлен опыт преподавания специального курса по формальным моделям параллелизма для магистрантов и аспирантов, специализирующихся в области высокопроизводительных вычислений. Сначала в статье дан обзор курса в целом, предварительных знаний, необходимых для этого курса, целей и задач курса, представлен план лекций и список рекомендованной литературы. Затем представлен пример одной поучительной головоломки (на достижимость в пространстве состояний) и ее формализации средствами семантических, синтаксических и логических моделей, как-то: сетями Петри, средствами исчисления параллельных взаимодействующих процессов (CCS) и темпоральной логики CTL. Эта головоломка — хороший пример для того, чтобы показать специфику и пользу каждого из рассмотренных формализмов.

Статья представляет собой расширенную версию доклада на VI Международном семинаре “Program Semantics, Specification and Verification: Theory and Applications”, Казань, 2015.

Статья публикуется в авторской редакции.


Об авторе

Н. В. Шилов
Институт систем информатики им. А. П. Ершова СО РАН
Россия

канд. физ.-мат. наук, старший научный сотрудник,

630090 г. Новосибирск, пр. Лаврентьева, 6



Список литературы

1. Handbook of Process Algebra, eds. J. A. Bergstra, A. Ponse, S. A. Smolka, Elsevier, Amsterdam, 2001.

2. L. Cardelli, A. D. Gordon, “Mobile ambient”, Lecture Notes in Computer Science, 1378, Springer-Verlag, Berlin, Heidelberg, 1998, 140–155.

3. L. Cardelli, “Mobility and Security.”, Foundations of Secure Computation, Proceedings of the NATO Advanced Study Institute on Foundations of Secure Computation, IOS Press, Amsterdam, 2000, 3–37.

4. E. M. Jr. Clarke, O. Grumberg, D. A. Peled, Model Checking, MIT Press, Cambridge, Massachusetts, 1999.

5. R.W. Floyd, “The paradigms of Programming”, Communications of ACM, 22 (1979), 455–460.

6. D. Grossman, “Ready-For-Use: 3 Weeks of Parallelism and Concurrency in a Required Second-Year Data-Structures Course”, SPLASH 2010 Workshop on Curricula for Concurrency and Parallelism (Reno, Nevada, USA, Oct. 17, 2010), https://homes.cs.washington.edu/~djg/papers/grossmanSPAC_position2010.pdf.

7. C. A. R. Hoare, Communicating Sequential Processes, Prentice Hall, Upper Saddle River, New Jersey, 1985, (This book was updated by Jim Davies at the Oxford University Computing Laboratory in 2004 and the new edition is available at the http://www.usingcsp.com/).

8. Yu. G. Karpov, Model Checking. Verificaciya parallelnyh i raspredelennyh programmnyh system, BHV-Peterburg, Saint Petersburg, 2010, (In Russian).

9. V. E. Kotov, Seti Petri, Nauka, Moscow, Russia, 1987, (In Russian).

10. Z. Manna, A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag,, New York, 1992.

11. T. S. Kuhn, The structure of Scientific Revolutions, Univ. of Chicago Press, Chicago and London, 1996, (3rd Edition).

12. R. Milner, Communicating and Mobile Systems: the Pi-Calculus, Cambridge University Press, Cambridge, England, 1999.

13. R. Milner, A Calculus of Communicating Systems, Lecture Notes in Computer Science, 92, Springer-Verlag, Berlin, Heidelberg, 1980.

14. J. L. Peterson, Petri Net Theory and the Modeling of Systems, Prentice Hall, Upper Saddle River, New Jersey, 1981.

15. W. Reisig, A Primer in Petri Net Design, Springer-Verlag, Berlin, Heidelberg, 1992.

16. P. van Roy, “Programming Paradigms for Dummies: What Every Programmer Should Know”, New Computational Paradigms for Computer Music,, eds. G. Assayag, A. Gerzso, IRCAM/Delatour, France, 2009, 9–38.

17. N. V. Shilov, K. Yi, “How to Find a Coin: Propositional Program Logics Made Easy”, Current Trends in Theoretical Computer Science. V. 2, World Scientific, Singapore, 2004, 181–214.

18. N. V. Shilov et al., “Development of the Computer Language Classification Knowledge Portal”, Ershov Informatics Conference PSI’11, Lecture Notes in Computer Science, 7162, Springer-Verlag, Berlin, Heidelberg, 2012, 340–348.

19. C. Stirling, Modal and Temporal Properties of Processes, Springer-Verlag, New York, 2001.


Дополнительные файлы

Для цитирования: Шилов Н.В. О преподавании формальных моделей и алгоритмов анализа параллельных систем. Моделирование и анализ информационных систем. 2015;22(6):783-794. https://doi.org/10.18255/1818-1015-2015-6-783-794

For citation: Shilov N.V. Teaching Formal Models of Concurrency Specification and Analysis. Modeling and Analysis of Information Systems. 2015;22(6):783-794. (In Russ.) https://doi.org/10.18255/1818-1015-2015-6-783-794

Просмотров: 367

Обратные ссылки

  • Обратные ссылки не определены.


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)