Abstract
Transformation rules of imperative concurrent programs, based on congruence and refinement relations between statements, are presented. They introduce and/or eliminate synchronous communication statements and parallelism in these programs. The development is made within a subset of SPL, a good representative of imperative notations for concurrent and reactive programs introduced by Manna and Pnueli. The paper shows that no finite set of transformation rules suffices to eliminate synchronous communication statements from programs involving the concatenation and parallelism operators only. An infinite set is given to suit this purpose, which can be applied recursively. As an important complement for the applications, a collection of tactics, for the acceleration of broader transformations, is described. Tactics apply a sequence of rules to a program with a specific transformation objective. The transformation rules and the tactics could be used in formal design to derive new programs from verified ones, preserving their properties, and avoiding the repetition of verifications for the transformed programs. As an example, the formal parallelization of a non-trivial distributed fast Fourier transform algorithm is outlined.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
R.-J. Back, J. von Wright, Refinement Calculus. A Systematic Introduction. Springer-Verlag 1998.
S. Bensalem, M. Bozga, J.C. Fernandez, L. Ghirvu, Y. Lakhnech, A Transformational Approach for Generating Non-Linear Invariants. In J. Palsberg (Ed.), Static Analysis, Proc. 7th Intl. Symp. SAS 2000, Santa Barbara, CA, USA, June 29–July 1, 2000. LNCS Vol. 1824, Springer, 2000, pp. 58–74.
M. Bertran, F. Alvarez-Cuevas, A. Duran, Communication Extended Abstract Types in the Refinement of Parallel Communicating Processes, in Transformation-Based Reactive Systems Development, LNCS v. 1231, Springer, 1997.
N.S. Bjørner, A. Browne, M. Colón, B. Finkbeiner, Z. Manna, H.B. Sipma, and T.E. Uribe. Verifying Temporal Properties of Reactive Systems: A STeP Tutorial. Formal Methods in System Design, 16, 227–270, June 2000.
N.S. Bjørner, A. Browne, E. Chang, M. Colón, A. Kapur, Z. Manna, H.B. Sipma, and T.E. Uribe. STeP: The Stanford Temporal Prover, User’s Manual. Technical Report STAN-CS-TR-95-1562, Computer Science Department, Stanford University, November 1995.
S.D. Brookes. ‘Full abstraction for a shared variable parallel language’, Information and Computation, 127(2):145–163, June 1996.
M. Broy, ‘Functional Specification of Time-Sensitive Communicating Systems’, ACM Transactions on Software Engineering and Methodology, 2(1),: 1–46, January 1993.
M. Broy, ‘Refinement of Time’, in M. Bertran and T. Rus (eds.), Transformation-Based Reactive Systems Development, Springer-Verlag, Lecture Notes in Computer Science 1231, 1997, pp. 44–63.
M. Broy, ‘A Logical Basis for Component-Based Systems Engineering’, Tech. Report Inst. fr Informatik, Tech. Univ. Munchen, Germany.
K.M. Chandy and J. Misra, Parallel Program Design, Addison Wesley, 1988.
Wei-Ngan Chin, Sian-Cheng Khoo, Z. Hu, M. Takeidu, Deriving Parallel Codes via Invariants. In J. Palsberg (Ed.), Static Analysis, Proc. 7th Intl. Symp. SAS 2000, Santa Barbara, CA, USA, June 29–July 1, 2000. LNCS Vol. 1824, Springer, 2000, pp. 75–94.
E.M. Clarke, O. Grumberg, D.A. Peled, Model Checking, The MIT Press, 1999.
J. Dingel, ‘A Trace-Based Refinement Calculus for Shared-Variable Parallel Programs’, in A.Martin Haeberer (Ed.) Algebraic Methodology and Software Technology, AMAST’98, LNCS 1548, Springer-Verlag, pp. 231–247, 1998.
B. Finkbeiner, Z. Manna, H. Sipma, Deductive Verification of Modular Systems. In Compositionality: The Significant Difference, COMPOS’97, LNCS v. 1536, pp. 239–275, Springer 1998.
M. Gordon, A.J. Milner, Ch. P. Wadsworth, Edinburgh LCF, LNCS v. 78, Springer-Verlag, 1979.
C.A.R. Hoare, ‘Communicating Sequential Processes’, Communications of ACM, Vol 21, pp 666–677, 1978.
C.A.R. Hoare, Communicating Sequential Processes, Prentice-Hall, Englewood Cliffs, N.J., 1985.
Gerald Holtzmann, Design and Validation of Computer Protocols, Prentice Hall, 1991.
J. Hooman, ‘Extending Hoare Logic to Real-Time’, Formal Aspects of Computing, 6A: 801–825, BCS, 1994.
Y. Kesten, Z. Manna, A. Pnueli, ‘Temporal Verification of Simulation and Refinement’, In REX Symposium A Decade of Concurrency, Lecture Notes in Computer Science 803, pp. 273–346, Springer-Verlag, 1994.
L. Lamport, ‘The Temporal Logic of Actions’, ACM Trans. Progr. Lang. and Sys., 16(3):872–923.
B. Mahony, ‘Using the Refinement Calculus for Dataflow Processes’. Tech. Report 94-32, Soft. Verification Research Centre, University of Queensland, October 94.
Z. Manna, A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems. Specification. Springer-Verlag, 1991.
Z. Manna, A. Pnueli, Temporal Verification of Reactive Systems. Safety. Springer-Verlag, 1995.
K.L. McMillan, and D.L. Dill, Symbolic Model Checking: An Approach to the State Explosion Problem, Kluwer Academic, 1993.
R. Milner, A Calculus of Communicating Systems, Springer-Verlag, 1980.
R. Milner, Communication and Concurrency, Prentice-Hall 1989.
M. Muller-Olm, D.A. Schmit, B. Steffen, Model Checking: A Tutorial Introduction. In A Cortesi, G File (Eds.), Static Analysis, Proc. 6th Intl. Symp. SAS’99, Venice, Italy, September 22–24, 1999. LNCS, Vol 1694, Springer, 1999, pp. 330–354.
Wei-Ngan Chin, Sian-Cheng Khoo, Z. Hu, M. Takeidu, Deriving Parallel Codes via Invariants. In J. Palsberg (Ed.), Static Analysis, Proc. 7th Intl. Symp. SAS 2000, Santa Barbara, CA, USA, June 29–July 1, 2000. LNCS Vol. 1824, Springer, 2000, pp. 75–94.
A.V. Oppenheim, R.W. Shafer, Digital Signal Processing, Prentice Hall, N.J., 1975.
A. Papoulis, Signal Analysis, McGraw-Hill, N.Y., 1977.
A. Podelski, Model Checking as Constraint Solving. In J. Palsberg (Ed.), Static Analysis, Proc. 7th Intl. Symp. SAS 2000, Santa Barbara, CA, USA, June 29–July 1, 2000. LNCS Vol. 1824, Springer, 2000, pp. 22–37.
L.R. Rabiner, B. Gold, Theory and Application of Digital Signal processing, Prentice Hall, N.J., 1975.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bertran, M., Babot, F., Climent, A., Nicolau, M. (2001). Communication and Parallelism Introduction and Elimination in Imperative Concurrent Programs. In: Cousot, P. (eds) Static Analysis. SAS 2001. Lecture Notes in Computer Science, vol 2126. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-47764-0_2
Download citation
DOI: https://doi.org/10.1007/3-540-47764-0_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42314-0
Online ISBN: 978-3-540-47764-8
eBook Packages: Springer Book Archive