This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A Decompositional Approach to the Design of Parallel Programs
December 1994 (vol. 20 no. 12)
pp. 914-932

A methodology for the derivation of parallel implementations from program specifications is developed. The goal of the methodology is to decompose a program specification into a collection of module specifications via property refinement, such that each module may be implemented independently by a subprogram. The correctness of the implementation is then deduced from the correctness of the property refinement procedure and the correctness of the individual subprograms. The refinement strategy is based on identifying frequently occurring control structures such as sequential composition and iteration. The methodology is developed in the context of the UNITY logic and the UC programming language, and illustrated through the solution of diffusion aggregation in fluid flow simulations.

[1] R. J. R. Back and K. Sere, "Stepwise refinement of parallel algorithms,"Sci. Comput. Programming, vol. 13, pp. 133-180, 1990.
[2] R. Bagrodia, K. M. Chandy, and E. Kwan, "UC: A language for the connection machine," inProc. Supercomput. 1990, Nov. 1990, pp. 525-534.
[3] R. Bagrodia and S. Mathur, "Efficient implementation of high-level parallel programs," inProc. ASPLOS-IV, Apr. 1991.
[4] R. Bagrodia and V. Austel, "UC user manual," Comput. Sci. Dep., Univ. California at Los Angeles, Tech. Rep., Oct. 1992.
[5] I. Chakravarty, M. Kleyn, T. Woo, R. Bagrodia, and V. Austel, "Unity to UC: Case studies in parallel program construction," Schlumberger Lab. Comput. Sci., Tech. Rep. TR-90-21, Nov. 1990.
[6] K. M. Chandy and J. Misra,Parallel Program Design: A Foundation. Reading, MA: Addison-Wesley, 1988.
[7] E. W. Dijkstra,A Discipline of Programming. Englewood Cliffs, NJ: Prentice-Hall, 1976.
[8] D. Gries,The Science of Programming. New York: Springer-Verlag, 1981.
[9] C. A. R. Hoare, "An axiomatic basis for computer programming,"Commun. ACM, vol. 12, no. 10, pp. 576-583, 1969.
[10] C.B. Jones,Systematic Software Development Using VDM, Prentice Hall Int'l, 1986.
[11] E. Knapp, "An exercise in formal development of parallel programs: maximum flow in graphs,"ACM Trans. Programming Languages and Syst., 12(2), pp. 203-221, Apr. 1990.
[12] S. S. Lam and A. U. Shankar, "Protocol verification via projections,"IEEE Trans. Software Eng., vol. 10, pp. 325-342, July 1984.
[13] Y. Liu, A. K. Singh, and R. L. Bagrodia, "A decompositional approach to the design of efficient parallel programs," Dep. Comput. Sci., Univ. California at Santa Barbara, Tech. Rep., Sept. 1994.
[14] N. Lynch and M. R. Tuttle, "Hierarchical correctness proofs for distributed algorithms," inProc. Sixth Annu. ACM Symp. Principles of Distrib. Comput., 1987, pp. 137-151.
[15] J. Misra, "Proving progress for program sequencing,"Notes on Unity 16-90, July 1991.
[16] J. N. Roberts and L. Schwartz, "Grain consolidation in porous media,"Phys. Rev., vol. 31, no. 9, 1985.
[17] B. Sanders, "Eliminating the substitution axiom from unity,"Formal Aspects Comput., vol. 3, pp. 189-205, 1991.
[18] A. K. Singh and R. Overbeek, "Derivation of efficient parallel programs: An example from genetic sequence analysis,"Int. J. Parallel Programming, vol. 18, no. 6, pp. 447-484, Dec. 1989.
[19] A. K. Singh, "Program refinement in fair transition systems,"Acta Informatica, vol. 30, no. 6, pp. 503-535.
[20] L. Snyder, "Applications of the 'phase abstraction' for portable and scalable parallel programming,"Languages, Compilers and Run-Time Environments, 1992.

Index Terms:
complete computer programs; program control structures; parallel programming; formal specification; program verification; flow simulation; digital simulation; diffusion; physics computing; decompositional approach; parallel program design; program specifications; parallel implementation correctness; module specifications; frequently occurring control structures; subprograms; property refinement procedure; sequential composition; iteration; UNITY logic; UC programming language; diffusion aggregation; fluid flow simulations
Citation:
Ying Liu, A.K. Singh, R.L. Bagrodia, "A Decompositional Approach to the Design of Parallel Programs," IEEE Transactions on Software Engineering, vol. 20, no. 12, pp. 914-932, Dec. 1994, doi:10.1109/32.368135
Usage of this product signifies your acceptance of the Terms of Use.