Язык спецификации моделей систем Promela

Контрольные вопросы

БИБЛИОГРАФИЧЕСКИЙ СПИСОК

[tcltk] Tcl Developer Xchange. URL: https://www.tcl.tk/ (дата обращения: 28.03.16).

[msc] Message Sequence Chart (MSC): Recommendation ITU-T Z.120 // International Telecommunication Union, 2011. URL: http://www.itu.int/rec/T-REC-Z.120-201102-I/en (дата обращения: 30.03.16).

[emrath] Emrath P. A., Padua D. A. Automatic detection of nondeterminacy in parallel programs // Proceedings of the 1988 ACM SIGPLAN and SIGOPS workshop on Parallel and distributed debugging. PADD ’88. 1988. Pp. 89–99.

[netzer] Netzer R. H. B., Miller B. P. What are race conditions?: Some issues and formalizations // ACM Lett. Program. Lang. Syst. 1992. — March. Vol. 1, no. 1. Pp. 74–88.

[afek] Afek Y., Attiya H., Dolev D. et al. Atomic snapshots of shared memory // J. ACM. 1993. — September. Vol. 40, no. 4. Pp. 873–890.

[kuck] Kuck D. J., Kuhn R. H., Padua D. A. et al. Dependence graphs and compiler optimizations // Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. POPL ’81. 1981. Pp. 207–218.

[kulyamin] Кулямин В.В. Методы верификации программного обеспечения / Всероссийский конкурсный отбор обзорно-аналитических статей по приоритетному направлению "Информационно-телекоммуникационные системы", 2008. - 117 с.

[karpov] Ю.Г. Карпов. Model checking: верификации параллельных и распределенных программных систем. Изд-во БХВ-Петербург, 2010, 552 с.

[spin] Verifying Multi-threaded Software with Spin. URL: https://www.spinroot.com/ (дата обращения: 08.04.16).

[tel] Тель Ж. Введение в распределенные алгоритмы. М.: Изд-во МЦНМО, 2009. ISBN: 9785940575153. 616 с.

[dijkstra] Dijkstra E. W. Solution of a problem in concurrent programming control // Commun. ACM. 1965. — September. Vol. 8, no. 9. P. 569.

[taubenfeld] Taubenfeld G. Shared Memory Synchronization // Bulletin of the EATCS. 2008. Vol. 96. Pp. 81–103.

[peterson] Peterson G. L. Myths About the Mutual Exclusion Problem // Inf. Process. Lett. 1981. Vol. 12, no. 3. Pp. 115–116.

[lamport] Lamport L. A new solution of Dijkstra’s concurrent programming problem // Commun. ACM. 1974. — August. Vol. 17, no. 8. Pp. 453–455.

[mcs] Mellor-Crummey J. M., Scott M. L. Algorithms for Scalable Synchronization on Shared-memory Multiprocessors // ACM Trans. Comput. Syst. 1991. — February. Vol. 9, no. 1. Pp. 21–65.

[clh] Magnusson P. S., Landin A., Hagersten E. Queue Locks on Cache Coherent Multiprocessors // Proceedings of the 8th International Symposium on Parallel Processing, Canc ́ un, Mexico, April 1994. 1994. Pp. 165–171.

[boyd] Boyd-wickizer S., Kaashoek M. F., Morris R., Zeldovich N. Non-scalable locks are dangerous // In the Proceedings of the Linux Symposium, Ottawa, Canada. 2012.

[fu] Fu S. S., Tzeng N.-F., Li Z. Empirical Evaluation of Distributed Mutual Exclusion Algorithms // Proceedings of the 11th International Symposium on Parallel Processing. IPPS ’97. 1997. Pp. 255–259.

[bertier] Bertier M., Arantes L., Sens P. Distributed mutual exclusion algorithms for grid applications: A hierarchical approach // J. Parallel Distrib. Comput. 2006. — January. Vol. 66, no. 1. Pp. 128–144.

[lamport2] Lamport L. Time, clocks, and the ordering of events in a distributed system // Commun. ACM. 1978. — July. Vol. 21, no. 7. Pp. 558–565.

[ehter] Эхтер Ш., Робертс Д. Многоядерное программирование. СПб.: Питер, 2010. ISBN: 978-5-388-00091-0. 316 с.

[fraser] Fraser K. Practical lock-freedom: Tech. Rep. UCAM-CL-TR-579: University of Cambridge, Computer Laboratory, 2004. — February. URL http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-579.pdf (дата обращения: 11.04.2016).

[dechev] Dechev D., Pirkelbauer P., Stroustrup B. Understanding and Effectively Preventing the ABA Problem in Descriptor-Based Lock-Free Designs // Proceedings of the 2010 13th IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing. ISORC ’10. 2010. Pp. 185–192.

[shann] Shann C.-H., Huang T.-L., Chen C. A Practical Nonblocking Queue Algorithm Using Compare-and-Swap // Proceedings of the Seventh International Conference on Parallel and Distributed Systems. ICPADS ’00. 2000. Pp. 470–.

[hendler] Hendler D., Shavit N., Yerushalmi L. A scalable lock-free stack algorithm // Proceedings of the sixteenth annual ACM symposium on Parallelism in algorithms and architectures. SPAA ’04. 2004. Pp. 206–215.

[kogan] Kogan A., Petrank E. Wait-free queues with multiple enqueuers and dequeuers // Proceedings of the 16th ACM symposium on Principles and practice of parallel programming. PPoPP ’11. 2011. Pp. 223–234.

[shalev] Shalev O., Shavit N. Split-ordered lists: Lock-free extensible hash tables // J. ACM. 2006. — May. Vol. 53, no. 3. Pp. 379–405.

[herlihy] Herlihy M., Moss J. E. B. Transactional memory: architectural support for lock-free data structures // SIGARCH Comput. Archit. News. 1993. — May. Vol. 21, no. 2. Pp. 289–300.

[lomet] Lomet D. B. Process structuring, synchronization, and recovery using atomic actions // SIGOPS Oper. Syst. Rev. 1977. — March. Vol. 11, no. 2. Pp. 128–137.

[liskov] Liskov B., Scheifler R. Guardians and Actions: Linguistic Support for Robust, Distributed Programs // ACM Trans. Program. Lang. Syst. 1983. — July. Vol. 5, no. 3. Pp. 381–404.

[hoare] Hoare C. A. R. Monitors: an operating system structuring concept // Commun. ACM. 1974. — October. Vol. 17, no. 10. Pp. 549–557.

[reinders] Reinders J. Transactional Synchronization in Haswell. URL http://software.intel.com/en-us/blogs/2012/02/07/transactional-synchronization-in-haswell/ (дата обращения: 12.04.2016).

[merrit] Merritt R. IBM plants transactional memory in CPU. URL http://www.eetimes.com/electronics-news/4218914/IBM-plants-transactional-memory-in-CPU/ (дата обращения: 12.04.2016).

[shavit] Shavit N., Touitou D. Software transactional memory // Proceedings of the fourteenth annual ACM symposium on Principles of distributed computing. PODC ’95. 1995. Pp. 204–213.