ABSTRACT
The ML family of languages and LCF-style interactive theorem proving have been closely related from their beginnings about 30 years ago. Here we report on a recent project to adapt both the Poly/ML compiler and the Isabelle theorem prover to current multicore hardware. Checking theories and proofs in typical Isabelle application takes minutes or hours, and users expect to make efficient use of "home machines" with 2-8 cores, or more.
Poly/ML and Isabelle are big and complex software systems that have evolved over more than two decades. Faced with the requirement to deliver a stable and efficient parallel programming environment, many infrastructure layers had to be reworked: from low-level system threads to high-level principles of value-oriented programming. At each stage we carefully selected from the many existing concepts for parallelism, and integrated them in a way that fits smoothly into the idea of purely functional ML with the addition of synchronous exceptions and asynchronous interrupts.
From the Isabelle/ML perspective, the main concept to manage parallel evaluation is that of "future values". Scheduling is implicit, but it is also possible to specify dependencies and priorities. In addition, block-structured groups of futures with propagation of exceptions allow for alternative functional evaluation (such as parallel search), without requiring user code to tackle concurrency. Our library also provides the usual parallel combinators for functions on lists, and analogous versions on prover tactics.
Despite substantial reorganization in the background, only minimal changes are occasionally required in user ML code, and none at the Isabelle application level (where parallel theory and proof processing is fully implicit). The present implementation is able to address more than 8 cores effectively, while the earlier version of the official Isabelle2009 release works best for 2-4 cores. Scalability beyond 16 cores still poses some extra challenges, and will require further improvements of the Poly/ML runtime system (heap management and garbage collection), and additional parallelization of Isabelle application logic.
- A.W. Appel, J.R. Ellis, and K. Li. Real-time concurrent collection on stock multiprocessors. In ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation (PLDI), 1988. Google ScholarDigital Library
- J. Armstrong, R. Virding, C. Wikström, and M. Williams. Concurrent Programming in Erlang. Prentice Hall, 1996. Google ScholarDigital Library
- D. Berry, R. Milner, and D.N. Turner. A semantics for ML concurrency primitives. In 17th ACM Symposium on Principles of Programming Languages (POPL). ACM, 1992. Google ScholarDigital Library
- P. Brinch Hansen. Monitors and concurrent Pascal: a personal history. In ACM SIGPLAN conference on History of programming languages (HOPL-II). ACM, 1993. Google ScholarDigital Library
- E.W. Dijkstra, L. Lamport, A.J. Martin, C.S. Scholten, and E.F.M. Steffens. On-the-fly garbage collection: An exercise in cooperation. Commun. ACM, 21 (11): 966--975, 1978. Google ScholarDigital Library
- D. Doligez and X. Leroy. A concurrent, generational garbage collector for a multithreaded implementation of ML. In 20th ACM Symposium on Principles of Programming Languages (POPL). ACM press, 1993. Google ScholarDigital Library
- C.H. Flood, D. Detlefs, N. Shavit, and X. Zhang. Parallel garbage collection for shared memory multiprocessors. In Java Virtual Machine Research and Technology Symposium (JVM'01), pages 21--21, Berkeley, CA, USA, 2001. USENIX Association. Google ScholarDigital Library
- A. Giacolone, P. Mishra, and S. Prasad. Facile: A symmetric integration of concurrent and functional programming. International Journal of Parallel Programming, 18 (2), 1989. Google ScholarDigital Library
- M. Gordon, R. Milner, L. Morris, M.C. Newey, and C.P. Wadsworth. A metalanguage for interactive proof in LCF. In Principles of programming languages (POPL), 1978. Google ScholarDigital Library
- P. Haller and M. Odersky. Event-based programming without inversion of control. In Joint Modular Languages Conference, Springer LNCS, 2006.Google ScholarDigital Library
- P. Haller and M. Odersky. Scala actors: unifying thread-based and event-based programming. Theoretical Computer Science, 2008. Google ScholarDigital Library
- R.H. Halstead, Jr. Multilisp: A language for concurrent symbolic computation. ACM Trans. Program. Lang. Syst., 7 (4), 1985. Google ScholarDigital Library
- T. Harris, S. Marlow, and S. Peyton Jones. Haskell on a shared-memory multiprocessor. In ACM SIGPLAN workshop on Haskell. ACM Press, September 2005. Google ScholarDigital Library
- T. Harris, S. Marlow, S. Peyton Jones, and M. Herlihy. Composable memory transactions. Commun. ACM, 51 (8), 2008. Google ScholarDigital Library
- S. Marlow, T. Harris, R.P. James, and S. Peyton Jones. Parallel generational-copying garbage collection with a block-structured heap. In International Symposium on Memory Management, 2008. Google ScholarDigital Library
- D.C.J. Matthews. Concurrency in Poly/ML. In ML with Concurrency, Monographs in Computer Science. Springer Verlag, 1996.Google Scholar
- D.C.J. Matthews and T. Le Sergent. Lemma: A distributed shared memory with global and local garbage collection. In H.G. Baker, editor, Memory Management, International Workshop (IWMM), Kinross, UK, September 1995. Google ScholarDigital Library
- R. Milner, M. Tofte, and R. Harper. The definition of Standard ML. MIT Press, Cambridge, MA, USA, 1990. Google ScholarDigital Library
- R. Milner, M. Tofte, and D. Macqueen. The Definition of Standard ML. MIT Press, Cambridge, MA, USA, 1997. Google ScholarDigital Library
- J.G. Morrisett and A. Tolmach. Procs and locks: a portable multiprocessing platform for Standard ML of New Jersey. In 4th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPOPP). ACM, 1993. Google ScholarDigital Library
- M. Odersky et al. An overview of the Scala programming language. Technical Report IC/2004/64, EPF Lausanne, 2004.Google Scholar
- J. Reppy. CML: A higher-order concurrent language. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), volume 26. ACM, 1991. Google ScholarDigital Library
- J. Reppy and Y. Xiao. Toward a parallel implementation of Concurrent ML. In Workshop on Declarative Aspects of Multicore Programming (DAMP), January 2008.Google Scholar
- J. Reppy, C. Russo, and Y. Xiao. Parallel Concurrent ML. In ACM SIGPLAN International Conference on Functional Programming (ICFP 2009), September 2009. Google ScholarDigital Library
- A. Rossberg, D. Le Botlan, G. Tack, T. Brunklaus, and G. Smolka. Alice through the looking glass. In Trends in Functional Programming, volume 5. Intellect Books, Bristol, UK, 2006.Google Scholar
- C.P. Thacker and L.C. Stewart. Firefly: a multiprocessor workstation. SIGARCH Comput. Archit. News, 15 (5): 164--172, 1987. Google ScholarDigital Library
- M. Wenzel. Parallel proof checking in Isabelle/Isar. In G. Dos Reis and L. Théry, editors, ACM SIGSAM Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS 2009). ACM Digital Library, 2009.Google Scholar
Index Terms
- Efficient parallel programming in Poly/ML and Isabelle/ML
Recommendations
Programming and verifying a declarative first-order prover in Isabelle/HOL
We certify in the proof assistant Isabelle/HOL the soundness of a declarative first-order prover with equality. The LCF-style prover is a translation we have made, to Standard ML, of a prover in John Harrison’s Handbook of Practical Logic and Automated ...
A Formalization and Proof Checker for Isabelle’s Metalogic
AbstractIsabelle is a generic theorem prover with a fragment of higher-order logic as a metalogic for defining object logics. Isabelle also provides proof terms. We formalize this metalogic and the language of proof terms in Isabelle/HOL, define an ...
A Completeness Proof for Bisimulation in the pi-calculus Using Isabelle
We use the interactive theorem prover Isabelle to prove that the algebraic axiomatization of bisimulation equivalence in the pi-calculus is sound and complete. This is the first proof of its kind to be wholly machine checked. Although the result has ...
Comments