Построение формальной модели Т-системы и исследование ее корректности
Ключевые слова:
формальная модель
Т-система
динамическое распараллеливание
корректность
параллельные программы
Аннотация
В статье исследуются методы распараллеливания программ, применяемые в Т-системе средстве автоматического динамического распараллеливания вычислительных приложений. Отличительная особенность Т-системы от аналогичных средств ориентация на программы, написанные на широко распространенных языках C, C++. В работе построена формальная модель для базовых конструкций Т-системы с помощью операционного подхода. В рамках модели доказывается корректность используемых механизмов. Разработанная модель была положена в основу новой реализации Т-системы.
Загрузки
Опубликован
2006-09-20
Выпуск
Раздел
Раздел 2. Программирование
Библиографические ссылки
- Абрамов С.М., Адамович А.И., Коваленко М.Р. Т-система -среда программирования с поддержкой автоматического динамического распараллеливания программ. Пример реализации алгоритма построения изображений методом трассировки // Программирование. 1999. 2. 100-107.
- Абрамов С.М., Васенин В.А., Мамчиц Е.Е., Роганов В.А., Слепухин А.Ф. Динамическое распараллеливание программ на базе параллельной редукции графов. Архитектура программного обеспечения новой версии Т- системы // Труды Всероссийской научной конференции (30 октября-2 ноября 2000 г., г. Черноголовка). М.: Изд-во МГУ, 2000. 261-265.
- Васенин В.А., Роганов В.А. GRACE: распределенные приложения в Интернет // Открытые системы. 2001. № 5, 6.
- Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. На пути к верификации С-программ. Часть 1. Язык C-light. Препринт ИСИ СО РАН, № 84. Новосибирск, 2001.
- Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. На пути к верификации С-программ. Часть 2. Язык C-light-kernel и его аксиоматическая семантика. Препринт ИСИ СО РАН, № 87. Новосибирск, 2001.
- Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. На пути к верификации С программ. Язык C- light и его формальная семантика // Программирование. 2002. № 6. 1-13.
- Промский А.В. Формальная семантика С-light программ и их верификация методом Хоара. Диссертация на соискание ученой степени к.ф.-м.н. Новосибирск, 2004.
- Abramov S., Adamovich A., Inyukhin A., Moskovsky A., Roganov V., Shevchuk E., Shevchuk Yu., Vodomerov A. OpenTS: An outline of dynamic parallelization approach // Lecture Notes in Computer Science. Vol. 3606. New York-Heidelberg-Berlin: Springer-Verlag, 2005. 303-312.
- Baker H. G., Hewitt C. The incremental garbage collection of processes // ACM Conference on AI and Programming Languages. New York, 1977. 55-59.
- Flanagan C., Felleisen M. The semantics of future and its use in program optimization // 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Houston, 1995.
- Foster I., Kesselman C., Tuecke S. The anatomy of the GRID. Enabling scalable virtual organizations. Lecture Notes in Computer Science. Vol. 2150. New York-Heidelberg-Berlin: Springer-Verlag, 2001.
- Halstead R.H., Jr. Implementation of Multilisp: Lisp on a multiprocessor // Proc. ACM Symposium on Lisp and Functional Programming. Austin, 1984. 9-17.
- Moreau L. The semantics of future in the presence of first-class continuations and side-effects. Southampton (United Kingdom), 1995.
- Norrish M. C formalised in HOL. Technical Report UCAM-CL-TR-453. University of Cambridge, Computer Laboratory. Cambridge, 1998.
- Papaspyrou N.S. A formal semantics for the C programming language. Doctoral Disseration. National Technical University of Athens. Athens (Greece), 1998.
- Plotkin G.D. A structural approach to operational semantics. Technical Report DAIMI FN-19. University of Aarhus, Computer Science Department. Aarhus (Denmark), 1981.
