The construction of a T-system formal model and the proof of its correctness

Authors

  • A.N. Vodomerov

Keywords:

формальная модель
Т-система
динамическое распараллеливание
корректность
параллельные программы

Abstract

We study the methods of program parallelization used in the T-system (an automatic parallelization tool for applied programs). A distinguishing feature of the T-system is that it is designed for programs written in the widespread languages C and C++. In this paper we present a formal model describing the T-system basic constructions on the basis of operational approach. Our model is used to prove the correctness of T-system mechanisms.

New computational technologies

Downloads

Published

2006-09-20

Issue

Vol. 7 (2006): Issue 3.

Section

Section 2. Programming

Author Biography

A.N. Vodomerov

Lomonosov Moscow State University,
Institute of Mechanics

References

  1. Абрамов С.М., Адамович А.И., Коваленко М.Р. Т-система -среда программирования с поддержкой автоматического динамического распараллеливания программ. Пример реализации алгоритма построения изображений методом трассировки // Программирование. 1999. 2. 100-107.
  2. Абрамов С.М., Васенин В.А., Мамчиц Е.Е., Роганов В.А., Слепухин А.Ф. Динамическое распараллеливание программ на базе параллельной редукции графов. Архитектура программного обеспечения новой версии Т- системы // Труды Всероссийской научной конференции (30 октября-2 ноября 2000 г., г. Черноголовка). М.: Изд-во МГУ, 2000. 261-265.
  3. Васенин В.А., Роганов В.А. GRACE: распределенные приложения в Интернет // Открытые системы. 2001. № 5, 6.
  4. Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. На пути к верификации С-программ. Часть 1. Язык C-light. Препринт ИСИ СО РАН, № 84. Новосибирск, 2001.
  5. Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. На пути к верификации С-программ. Часть 2. Язык C-light-kernel и его аксиоматическая семантика. Препринт ИСИ СО РАН, № 87. Новосибирск, 2001.
  6. Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. На пути к верификации С программ. Язык C- light и его формальная семантика // Программирование. 2002. № 6. 1-13.
  7. Промский А.В. Формальная семантика С-light программ и их верификация методом Хоара. Диссертация на соискание ученой степени к.ф.-м.н. Новосибирск, 2004.
  8. 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.
  9. Baker H. G., Hewitt C. The incremental garbage collection of processes // ACM Conference on AI and Programming Languages. New York, 1977. 55-59.
  10. 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.
  11. 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.
  12. Halstead R.H., Jr. Implementation of Multilisp: Lisp on a multiprocessor // Proc. ACM Symposium on Lisp and Functional Programming. Austin, 1984. 9-17.
  13. Moreau L. The semantics of future in the presence of first-class continuations and side-effects. Southampton (United Kingdom), 1995.
  14. Norrish M. C formalised in HOL. Technical Report UCAM-CL-TR-453. University of Cambridge, Computer Laboratory. Cambridge, 1998.
  15. Papaspyrou N.S. A formal semantics for the C programming language. Doctoral Disseration. National Technical University of Athens. Athens (Greece), 1998.
  16. Plotkin G.D. A structural approach to operational semantics. Technical Report DAIMI FN-19. University of Aarhus, Computer Science Department. Aarhus (Denmark), 1981.