Abstract
Parallel execution of a programR (intuitively regarded as a partial order) is usually modeled by sequentially executing one of the total orders (interleavings) into which it can be embedded. Our work deviates from this serialization principle by usingtrue concurrency to model parallel execution. True concurrency is represented via completions ofR tosemi total orders, called time diagrams. These orders are characterized via a set of conditions (denoted byCt), yielding orders or time diagrams which preserve some degree of the intended parallelism inR. Another way to express semi total orders is to use re-writing or derivation rules (denoted byCx) which for any programR generates a set of semi-total orders. This paper includes a classification of parallel execution into three classes according to three different types ofCt conditions. For each class a suitableCx is found and a proof of equivalence between the set of all time diagrams satisfyingCt and the set of all terminalCx derivations ofR is devised. This equivalence between time diagram conditions and derivation rules is used to define a novel notion of correctness for parallel programs. This notion is demonstrated by showing that a specific asynchronous program enforces synchronous execution, which always halts, showing that true concurrency can be useful in the context of parallel program verification.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
V. Pratt, Modeling Concurrency with Partial Orders,International Journal of Parallel Programming 15(1):33–71 (1986).
INMOS Ltd.Occam Programming Manual, Prentice Hall (1984).
United Stated Department of Defense, Reference Manual for the Ada Programming Language. ANSI MIL-STD-1815 (1983).
S. Ahuja, N. Carriero, and D. Gelernter, Linda and Friends,Computer 19(8):26–34 (1986).
A. H. Karp and R. G. Babb II, A Comparison of 12 Parallel Fortran Dialects,IEEE Software 5(5):52–67 (1988).
J. T. Kuehn and H. J. Siegel, Extensions to the C Programming Language for SIMD/MIMD Parallelism,Intl. Conf. Parallel Processing, pp. 232–235 (August 1985).
L. Lamport, How to Make a Multiprocessor Computer that Correctly Executes Multiprocess Programs,IEEE Trans. Computers C-28(9):690–691 (1979).
C. A. R. Hoar,Communicating Sequential Process, Prentice Hall (1985).
C. H. Papadimitriou, The Serializability of Concurrent Database Updates,Journal of the ACM 26(4):631–653 (1979).
W. Reisig, Concurrency Is More Fundamental Than Interleavings,EATCS Bull, Vol. 36 (1988).
V. S. Adve and M. D. Hill, Weak Ordering—A New Definition,Ann. Intl. Symp. Computer Architecture 17:2–14 (1990).
A. Pnueli, The Temporal Logic of Programs,Proc. of the 18th Symp. on the Foundations of Computer Science, ACM (November 1977).
H. Gaifamn, Modeling Concurrency by Partial Orders and Nonlinear Transition Systems, Springer Verlag,Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, Lecture Notes in Computer Science 354:467–488 (1988).
R. Janicki and M. Kountny, Structure of Concurrency,Theoretical Computer Science 112:5–52 (1993).
A. K. Deshpande and K. M. Kavi, A Review of Specification and Verification Methods for Parallel Programs, including the Dataflow Approach,Proc. IEEE 77(12):1816–1828 (December 1989).
E. R. Olderog, Nets, Terms and Formulas, Cambridge Tracts in Theoretical Computer Sciences, Vol. 23 (1991).
L. Rudolph, Software Structures for Ultraparallel Computing, Ph.D. Thesis, Courant Inst., NYU (1982).
E. Freudenthal and A. Gottlieb, Process Coordination with Fetch-and-Increment,Ann. Intl. Symp. Computer Architecture 17:2–14 (1990).Intl. Symp. Architect. Support for Prog. Lang. & Operating Syst. 4:260–268 (1991).
B. D. Lubachevsky, An Approach to Automating the Verification of Compact Parallel Coordination Programs,Acta Informatica 21:125–169 (1984).
H. E. Bal, J. G. Steiner, and A. S. Tanenbaum, Programming Languages for Distributed Computing Systems,ACM Comput. Surv. 21(3):261–322 (1989).
H. Gaifamn and V. Pratt, Partial Order Models of Concurrency and the Computation of Function,Symp. on Logic in Computer Science (1987).
M. P. Herlihy and J. M. Wing, Axioms for Concurrent Objects,JPDC 14:13–26 (1987).
U. Montanari,True Concurrency: Theory and Practice, Springer-Verlag, Proc. of Mathematics of Program Construction, Oxford (1992).
W. E. Weihl, Commutativity-based Concurrency Control for Abstract Data Types,IEEE Trans. on Computers 37(12):1488–1505 (December 1988).
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Ben-Asher, Y., Farchi, E. Using true concurrency to model execution of parallel programs. Int J Parallel Prog 22, 375–407 (1994). https://doi.org/10.1007/BF02577738
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF02577738