A Formal Model of a System for Automated Program Parallelization

摘要

In the paper, the T-system-an approach to automated program parallelization that has several implementations-is studied. In the absence of formal justification, these implementations have a number of disadvantages, which results in incorrect operation of programs. In the paper, a mathematical model of the T-system is constructed, and, in the framework of this model, correctness of parallelization is proved. The model makes it possible to reveal a number of inaccuracies in the latest version of the T-system OpenTS and suggest ways to eliminate them. The use of the formal model in the development of NewTS, a new version of the T-system, is described.