Formally specifying and analyzing a parallel virtual machine for lazy functional languages using Maude
Pages 19 - 26
Abstract
Pure lazy functional languages are a promising programming paradigm for harvesting massive parallelism, as their abstraction features and lack of side effects support the development of modular programs without unneeded serialization. We give a new formal message passing semantics for implicitly parallel execution of a lazy functional programming language, based on the intensional transformation that converts programs in functional style to a form that can be executed in a dataflow paradigm. We use rewriting logic to define the semantics of our parallel virtual machine and we use the Maude tool to formally analyze our model. We also briefly discuss a prototype parallel implementation of our model in Erlang.
References
[1]
J. Armstrong. Programming Erlang: Software for a Concurrent World. Pragmatic Bookshelf, 2007.
[2]
Arvind and R. S. Nikhil. Executing a program on the MIT tagged-token dataflow architecture. IEEE Trans. Comput., 39: 300--318, 1990. 10.1109/12.48862.
[3]
C. Baker-Finch, D. J. King, and P. Trinder. An operational semantics for parallel lazy evaluation. SIGPLAN Not., 35: 162--173, 2000. 10.1145/357766.351256.
[4]
G. Boudol. Some chemical abstract machines. In A Decade of Concurrency Reflections and Perspectives, volume 803 of LNCS. Springer, 1994.
[5]
A. Charalambidis, A. Grivas, N. S. Papaspyrou, and P. Rondogiannis. Efficient intensional implementation for lazy functional languages. phMathematics in Computer Science, 2 (1): 123--141, 2008. 10.1007/s11786-008-0047-5.
[6]
M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and C. L. Talcott, editors. All About Maude, volume 4350 of LNCS, 2007. Springer.
[7]
C. Flanagan and R. S. Nikhil. pHluid: The Design of a Parallel Functional Language Implementation on Workstations. In Proc. ICFP'96. ACM, 1996.
[8]
G. Fourtounis, N. Papaspyrou, and P. Rondogiannis. The Intensional Transformation for Functional Languages with User-Defined Data Types. In Proc. of the 8th Panhellenic Logic Symposium, 2011.
[9]
F. Gava and F. Loulergue. Verifying functional bulk synchronous parallel programs using the Coq system. Technical Report TR-LACL-2003-02, LACL (Laboratory of Algorithms, Complexity and Logic), University of Paris-Est (Paris 12), 2003.
[10]
D. Gelernter. Generative communication in Linda. ACM Trans. Program. Lang. Syst., 7: 80--112, 1985. 10.1145/2363.2433.
[11]
K. Hammond and G. Michelson, editors. Research Directions in Parallel Functional Programming. Springer, 2000.
[12]
B. Han, S. A. Mokhov, and J. Paquet. Advances in the Design and Implementation of a Multi-tier Architecture in the GIPSY Environment with Java. In Proc. SERA'10. IEEE, 2010. 10.1109/SERA.2010.40.
[13]
T. Harris and S. Singh. Feedback directed implicit parallelism. SIGPLAN Not., 42: 251--264, 2007. 10.1145/1291220.1291192.
[14]
M. Hidalgo-Herrero and Y. Ortega-Mallén. A Distributed Operational Semantics for a Parallel Functional Language. In phProc. SFP'00. Intellect Books, 2000.
[15]
S. P. Jones, R. Leshchinskiy, G. Keller, and M. M. T. Chakravarty. Harnessing the multicores: Nested data parallelism in Haskell. In Proc. FSTTCS'08, volume 2 of Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2008. 10.4230/LIPIcs.FSTTCS.2008.1769.
[16]
H.-W. Loidl. phGranularity in Large-Scale Parallel Functional Programming. PhD thesis, Department of Computing Science, University of Glasgow, 1998.
[17]
R. Loogen, Y. Ortega-Mallén, and R. Pena Marí. Parallel functional programming in Eden. J. Funct. Program., 15: 431--475, 2005. 10.1017/S0956796805005526.
[18]
S. Marlow, S. Peyton Jones, and S. Singh. Runtime support for multicore Haskell. In phProc. ICFP'09. ACM, 2009. 10.1145/1596550.1596563.
[19]
J. Meseguer. Conditional rewriting logic as a unified model of concurrency. Theor. Comput. Sci., 96: 73--155, 1992. 10.1016/0304-3975(92)90182-F.
[20]
J. Peterson, V. Trifonov, and A. Serjantov. Parallel functional reactive programming. In PADL'00, volume 1753 of phLNCS. Springer, 2000.
[21]
J. Plaice. Multidimensional Lucid: Design, Semantics and Implementation. In phProc. DCW'00, volume 1830 of LNCS. Springer, 2000.
[22]
J. Plaice, B. Mancilla, G. Ditu, and W. W. Wadge. Sequential demand-driven evaluation of Eager TransLucid. In Proc. COMPSAC'08. IEEE, 2008. 10.1109/COMPSAC.2008.191.
[23]
R. Plasmeijer and M. v. Eekelen. Functional Programming and Parallel Graph Rewriting. Addison-Wesley, 1993.
[24]
T. Rahilly and J. Plaice. A multithreaded implementation for TransLucid. In Proc. COMPSAC'08. IEEE, 2008. 10.1109/COMPSAC.2008.192.
[25]
J. C. Reynolds. Definitional interpreters for higher-order programming languages. In Reprinted from the proceedings of the 25th ACM National Conference. ACM, 1972.
[26]
P. Rondogiannis and W. W. Wadge. First-order functional languages and intensional logic. J. Funct. Program., 7: 73--101, 1997. 10.1017/S0956796897002633.
[27]
P. Rondogiannis and W. W. Wadge. Higher-order functional languages and intensional logic. J. Funct. Program., 9 (5): 527--564, 1999.
[28]
P. v. Roy and S. Haridi. Concepts, Techniques, and Models of Computer Programming. MIT Press, 2004.
[29]
P. W. Trinder, K. Hammond, J. S. Mattson Jr., A. S. Partridge, and S. L. Peyton Jones. GUM: a portable implementation of Haskell. In Proc. PLDI'96, 1996.
[30]
strategiesP. W. Trinder, K. Hammond, H.-W. Loidl, and S. L. Peyton Jones. Algorithm + Strategy = Parallelism. J. of Funct. Program., 8 (1): 23--60, 1998.
[31]
P. W. Trinder, H.-W. Loidl, and R. F. Pointon. Parallel and distributed Haskells. J. Funct. Program., 12: 469--510, 2002. 10.1017/S0956796802004343.
[32]
E. Vassev and J. Paquet. A general architecture for demand migration in a demand-driven execution engine in a heterogeneous and distributed environment. In Proc. CNSR'05, 2005. 10.1109/CNSR.2005.9.
Index Terms
- Formally specifying and analyzing a parallel virtual machine for lazy functional languages using Maude
Recommendations
Using Maude and Its Strategies for Defining a Framework for Analyzing Eden Semantics
Eden is a parallel extension of the functional language Haskell. On behalf of parallelism Eden overrides Haskell's pure lazy approach, combining a non-strict functional application with eager process creation and eager communication. We desire to ...
Maude MSOS Tool
Modular structural operational semantics (MSOS) is a new framework that allows structural operational semantics (SOS) specifications to be made modular in the sense of not imposing the redefinition of transition rules, which is the case in SOS ...
Two case studies of semantics execution in Maude: CCS and LOTOS
We explore the features of rewriting logic and, in particular, of the rewriting logic language Maude as a logical and semantic framework for representing and executing inference systems. In order to illustrate the general ideas we consider two ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © 2011 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 18 September 2011
Check for updates
Author Tags
Qualifiers
- Research-article
Conference
ICFP '11
Sponsor:
ICFP '11: ACM SIGPLAN International Conference on Functional Programming
September 18, 2011
Tokyo, Japan
Upcoming Conference
ICFP '25
- Sponsor:
- sigplan
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 121Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 24 Jan 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in