Semantic parallelization: a practical exercise in abstract interpretation

ABSTRACT

The parallelization of sequential programs is an adequate approach for the easy use of architectural features provided on parallel computers. We propose to enhance this technique with the notion of semantic parallelization. The principle is to consider the transformations of programs induced by parallelization as non-standard denotational semantics of the source programming language. We show how to apply this concept to detect, in a toy language ALL, parallelizable complex commands and to deal with some type of programs using indirections. Thanks to results in domain theory and abstract interpretation, we give correctness proofs for these transformations with respect to ALL standard semantic. A byproduct of our approach is that a denotational specification is also an executable prototype ;hence, we were able to implement a semantic parallelizer in the ML functional language. Running examples are supplied.

REFERENCES

• Aho86: Aho, A., Sethi, R., and Ullman, J. D., Compilers, Addison-Wesley, 1986.
• Allen82: Allen, J. R. and Kennedy, K., PFC : a Program to Convert Fortran to a Parallel Form, Supercomputers, Design and Applications, COMPSAC, IEEE, 1982.
• Allia85: Alliant,, A/ZJANT FX/Series : Product Swmnary, Aeton, June 1985.
• Berns66: Bernstein, A. J., "Analysis of Programs for Parallel Processing," IEEE Trans. on Elec. Comp., vol. 15, pp. 757-763, October 1966.
• Carde85: Cardelli, L., "Basic Polymorphic Typeeh~cking," Polymorphism 1, vol. II, Bell Labs, January 1985.
• Clark86: Keith Clark , Steve Gregory, PARLOG: parallel programming in logic, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.1, p.1-49, Jan. 1986 [doi>10.1145/5001.5390]
• Coope72: Cooper, D. C., Theorem Proving in Arithmetic without Multiplication, M~h.Intell.7, 1972.
• Cousi85: Cousineau, G., "The ML Handbook," (draft 1NRIA), May 1985.
• Couso78b: Cousot, P., M~hodes It~ratives de Construction de Points Fixes d'Opkrateurs Monotones sur un Trefflis, Analyse S~mantique des Programmes, Thesis, U.S.M.G, Grenoble, 1978.
• Couso77: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• Couso78a: Patrick Cousot , Nicolas Halbwachs, Automatic discovery of linear restraints among variables of a program, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.84-96, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512770]
• Duffi74: Duffin, R. J., "On Fourier's Analysis of Linear Inequality Systems," Mathematical ProgSt., vol. 1, North-Holland, 1974.
• Fishe84: Joseph A. Fisher , John R. Ellis , John C. Ruttenberg , Alexandru Nicolau, Parallel processing: a smart compiler and a dumb machine, ACM SIGPLAN Notices, v.19 n.6, p.37-47, June 1984
• Floyd67: Floyd, R. W., Assigning Meanings to Programs, 19- th Syrup. in Applied Maths., American Mathematical Society, 1967.
• Forte85: Fortes, J. A. B. and Moldovan, D.I., "Parallelism Detection and Transformation Techniques Useful for VLSI Algorithms," J. of Parallel and Distributed Computing, vol. 2, pp. 277-301, Academic Press, 1985.
• Gordo79b: Michael J. C. Gordon, The Denotational Description of Programming Languages: An Introduction, Springer-Verlag New York, Inc., Secaucus, NJ, 1979
• Gordo79a: Gordon, M. J. C. and Milner, R., Edinburgh LCF, LNCS 78, Springer-Verlag, 1979.
• Hilli85: W. Daniel Hillis, The connection machine, MIT Press, Cambridge, MA, 1986
• Johns78: Johnson, S. C., YACC: Yet Another Compiler- Compiler, Bells Labs, Murray Hills, July 1978.
• Jouve86c: Jouvelot, P., Parallkiisation Sbnantique, PhD. Thesis (expected, in French), Univ. of Paris 6, 1986.
• Jouve86a: P Jouvelot, Parallelization by semantic detection of reductions, Proc. of the European symposium on programming on ESOP 86, p.223-236, March 1986, Saarbru:9Aicken, Germany
• Kreis67: Kreisel, G. and Krivine, J. L., Elements de Logique Math~matique, Dunod, 1967.
• Kuck77: David J. Kuck, A Survey of Parallel Machine Organization and Programming, ACM Computing Surveys (CSUR), v.9 n.1, p.29-59, March 1977 [doi>10.1145/356683.356686]
• Li86: Kuo-Cheng Li, A note on the vector C language, ACM SIGPLAN Notices, v.21 n.1, p.49-57, Jan 1986 [doi>10.1145/382282.382422]
• MacQu83: MacQueen, D., "Modules for SML," Polymorphism, vol. I, Bell Labs, December 1983.
• Nicol84: Nieolau, A. and Fisher, J. A., "Measuring the Parallelism Available for Very Long Instruction Word Architectures," IEEE Tr. on Computers, vol. C-33, November 1984.
• Niels85: Flemming Nielson, Program transformations in a denotational setting, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.3, p.359-379, July 1985 [doi>10.1145/3916.3917]
• Oppen78: Oppen, D. C., "A 22~ Upper Bound on the Complexity of Presburger Arithmetic," JCSS, vol. 16, pp. 323-332, 1978.
• Perro79: R. H. Perrott, A Language for Array and Vector Processors, ACM Transactions on Programming Languages and Systems (TOPLAS), v.1 n.2, p.177-195, Oct. 1979 [doi>10.1145/357073.357075]
• Schwa80: Jacob T. Schwartz, Ultracomputers, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.4, p.484-521, Oct. 1980 [doi>10.1145/357114.357116]
• Scott72: Scott, D., The Lattice of Flow Diagrams, Symposium on Semantics of Algorithmic Language, Springer- Verlag, 1972.
• Suzuk77: Suzulo, N. and Jefferson, D., Verification Decidability of Presburger Array Programs, Proe.on Theoretical Computer Science, Waterloo, 1977.
• Triol86a: R Triolet , P Feautrier , F Irigoin, Automatic parallelization of FORTRAN programs in the presence of procedure-calls, Proc. of the European symposium on programming on ESOP 86, p.210-222, March 1986, Saarbru:9Aicken, Germany
• Triol86b: Rémi Triolet , Francois Irigoin , Paul Feautrier, Direct parallelization of call statements, ACM SIGPLAN Notices, v.21 n.7, p.176-185, July 1986

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.2 Modes of Computation
          Subjects: Parallelism and concurrency

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Concurrent programming structures
      D.3.4 Processors
          Subjects: Compilers

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Denotational semantics

General Terms:
Algorithms, Languages, Theory