×

Transformations of sequential specifications into concurrent specifications by synchronization guards. (English) Zbl 0717.68065

Summary: A transformation \({\mathbb{C}}\) of sequential specifications into concurrent specifications is defined. The sequential specification is in the form of a regular expression extended with a declaration of the actions that are independent and have the potential for concurrent execution. The concurrent specification is in the form of a product of regular expressions. It is proved that a concurrent specification resulting from the application of the transformation \({\mathbb{C}}\) to a sequential specification modified by inserting special actions, called synchronization guards, is behaviorally equivalent to the original specification. The programming language representation of a sequential specification is exemplified in a Pascal-like language, Banach.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
68Q45 Formal languages and automata

Software:

Modula
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Back, R. J.R., A Method for Refining Atomicity in Parallel Algorithms, (Lecture Notes in Computer Science, 366 (1989), Springer: Springer Berlin), 199-216
[2] Best, E., COSY: Its Relation to Nets and CSP, (Lecture Notes in Computer Science, 255 (1986), Springer: Springer Berlin), 416-440
[3] Birtwistle, G.; Dahl, O.-J.; Myhrhaug, B.; Nyggard, K., Simula Begin (1979), Chartwell-Batt Ltd
[4] Bose, P., Heuristic rule-based transformations for enhanced vectorization, (Proc. 17th Internat. Conf. on Parallel Processing, Vol II (1988), Pen. State Press), 63-66
[5] Hansen, P. Brinch, Operating System Principles (1973), Prentice Hall: Prentice Hall Englewood Cliffs, NJ · Zbl 0308.68007
[6] Hansen, P. Brinch, Joyce—a programming language for distributed systems, Software Practice and Experience, 17, 1, 29-50 (1987) · Zbl 0601.68011
[7] Cartier, P.; Foata, D., Problemes Combinatoires de Commutation et Rearrangements, (Lecture Notes in Mathematics, 85 (1969), Springer: Springer Berlin) · Zbl 0186.30101
[8] Crookes, D.; Elder, J. W.G., An experiment in language design for distributed systems, Software Practice and Experience, 14, 957-971 (1984) · Zbl 0542.68019
[9] Dietz, H. G., Finding large-grain parallelism in loops with serial control dependencies, (Proc. 17th Internat. Conf. on Parallel Processing, Vol II (1988), Pen. State Press), 114-121
[10] Dijkstra, E. W., Hierarchical ordering of sequential process, Acta Inform, 1, 115-138 (1971)
[11] Garland, S. J.; Luckham, D. C., Program schemas, recursion schemas, and formal languages, J. Comput. System Sci., 7, 119-160 (1973) · Zbl 0369.68014
[12] Hey, T., Experiments in MIMD Parallelism, (Lecture Notes in Computer Science, 366 (1989), Springer: Springer Berlin)
[13] Hoare, C. A.R., Communicating Sequential Processes (1985), Prentice Hall: Prentice Hall Englewood Cliffs, NJ · Zbl 0637.68007
[14] Holt, R. C., A short introduction to concurrent Euclid, ACM Sigplan Notices, 17, 60-79 (1982)
[15] occam Programming Manual (1982), Prentice Hall: Prentice Hall Englewood Cliffs, NJ
[16] Janicki, R., A Construction of Concurrent Systems by means of Sequential Solutions and Concurrency Relations, (Lecture Notes in Computer Science, 107 (1981), Springer: Springer Berlin), 327-334
[17] Janicki, R., On the design of concurrent systems, (Proc. 2nd. Conf. on Distributed Computing Systems. Proc. 2nd. Conf. on Distributed Computing Systems, Paris (1981), IEEE Press: IEEE Press New York), 455-466
[18] Janicki, R., A Method for Developing Concurrent Systems, (Lecture Notes in Computer Science, 167 (1984), Springer: Springer Berlin), 155-166
[19] Janicki, R., Transforming sequential systems into concurrent systems, Theoret. Comput. Sci., 36, 25-58 (1985) · Zbl 0559.68032
[20] Janicki, R., How to relieve a programmer from synchronization details, Atlanta, GA. Atlanta, GA, Proc. 16th Ann. ACM Computer Science Conf. (1988)
[21] Janicki, R.; Müldner, T., Sequential specifications and concurrent executions of Banach programs, Edmonton, Canada. Edmonton, Canada, CIPS’ 88 (1988)
[22] Janicki, R.; Müldner, T., Complete sequential specifications allows for a concurrent execution, Louisville, KY. Louisville, KY, ACM 1989 Computer Science Conf. (1989)
[23] Janicki, R.; Müldner, T., On algebraic transformations of sequential specifications, Iowa City, IA. Iowa City, IA, AMAST 89 (1989)
[24] Janicki, R.; Müldner, T., A simple realization of parallel devices recognizing regularly defined trace languages, Washington, DC. Washington, DC, ACM 1990 Computer Science, Conf. (1990)
[25] Janicki, R.; Lauer, P. E.; Koutny, M.; Devillers, R., Concurrent and maximally concurrent evolution of non-sequential systems, Theoret. Comput. Sci., 43, 213-238 (1985) · Zbl 0565.68020
[26] Janicki, R.; Lauer, P., Specifications and Analysis of Concurrent Systems: The COSY Approach (1990), Springer: Springer Berlin, to be published.
[27] Jazayeri, M., CSP/80: A language for communicating sequential processes, IEEE Compcon, 736-740 (1980)
[28] Lallement, G., Semigroups and Combinatorial Applications (1979), John Wiley: John Wiley New York · Zbl 0421.20025
[29] Lampson, B. W.; Redell, D. D., Experience with processes and monitors in Mesa, Comm. ACM, 23, 105-117 (1980)
[30] Lauer, P. E., The COSY approach to distributed computing systems, (Duce, D. A., Distributed Systems Programs (1984), P. Peregrinus: P. Peregrinus London), 107-126
[31] Lauer, P. E.; Janicki, R., An introduction to the MACRO COSY notation, (Voss, K.; Genrich, H. J.; Rozenberg, G., Concurrency and Nets (1987), Springer: Springer Berlin), 287-314 · Zbl 0639.68052
[32] Lengauer, C., A methodology for programming concurrency: the formalism, Sci. Comput. Programm., 2, 19-52 (1982) · Zbl 0491.68006
[33] Lengauer, C.; Hehner, E. C.R., A methodology for programming concurrency: an informal approach, Sci. Comput. Programm, 2, 1-18 (1982) · Zbl 0491.68005
[34] Mazurkiewicz, A., Recursive algorithms and formal languages, Bull. Acad. Polon. Sci. Ser. Math. Astronom. Phys., 20, 799-803 (1972) · Zbl 0259.68033
[35] Mazurkiewicz, A., Concurrent program schema and their interpretations, (Report DAIMI-PB-78 (1977), Aarhus University)
[36] Mazurkiewicz, A., Trace Theory, (Lecture Notes in Computer Science, 255 (1986), Springer: Springer Berlin), 297-324
[37] Müldner, T.; Prószyński, P., Sequential specification of the dining philosophers problem, Fredericton, NB. Fredericton, NB, APICS’89 Computer Science Conf. (1989), also published as a Technical Report, Acadia University.
[38] Osterhaug, A., Guide to Parallel Programming on Sequent Computer Systems (1986), Sequent Computer Systems Inc
[39] Reisig, W., Petri Nets (1985), Springer: Springer Berlin · Zbl 0521.68057
[40] Reference Manual for the Ada Programming Language (1982), United States Department of Defense (U.S. Government Printing Office): United States Department of Defense (U.S. Government Printing Office) Washington, DC 20402
[41] Smith, K.; Appelbe, W. F., FAT—An interactive Fortran parallelizing tool, (Proc. 17th Internat. Conf. on Parallel Processing, Vol II (1988), Pen. State Press), 58-62
[42] Shields, M. W., Adequate Path Expressions, (Lecture Notes in Computer Science, 70 (1979), Springer: Springer Berlin), 249-265 · Zbl 0429.68058
[43] Shields, M. W., Concurrent machines, The Computer Journal, 25, 449-466 (1985) · Zbl 0573.68026
[44] Welsh, J.; Bustard, D. W., Pascal-Plus—another language for modular multiprogramming, Software Practice and Experience, 9, 947-957 (1979) · Zbl 0411.68025
[45] Wirth, N., Modula—a language for modular multiprogramming, Software Practice and Experience, 7, 3-35 (1977) · Zbl 0346.68012
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.