Powered by
7th ACM SIGPLAN International Workshop on Functional High-Performance Computing (FHPC 2018),
September 29, 2018,
St. Louis, MO, USA
7th ACM SIGPLAN International Workshop on Functional High-Performance Computing (FHPC 2018)
Message from the Chairs
Welcome to the 7th ACM SIGPLAN Workshop on Functional High Performance
Computing (FHPC 2018), September 29, St. Louis, Missouri, USA, co-located with
the 23rd ACM SIGPLAN International Conference on Functional Programming and
Strange Loop. We seek to bring together researchers and practitioners exploring
uses of functional (or more generally, declarative or high-level) programming
systems or concepts in application domains where high performance is essential.
The aim of the meeting is to enable sharing of results, experiences, and novel ideas
about how high-level, declarative specifications of computationally challenging
problems can serve as maintainable and portable code that approaches (or even
exceeds) the performance of machine-oriented imperative implementations.
Info
HELIX: A Case Study of a Formal Verification of High Performance Program Generation
Vadim Zaliva and Franz Franchetti
(Carnegie Mellon University, USA)
In this paper, we present HELIX, a formally verified operator language and rewriting engine for generation of high-performance implementation for a variety of linear algebra algorithms. Based on the existing SPIRAL system, HELIX adds the rigor of formal verification of its correctness using Coq proof assistant. It formally defines two domain-specific languages: HCOL, which represents a computation data flow and Σ-HCOL, which extends HCOL with iterative computations. A framework for automatically proving semantic preservation of expression rewriting for both languages is presented. The structural properties of the dataflow graph which allow efficient compilation are formalized, and a monadic approach to tracking them and to reasoning about structural correctness of Σ-HCOL expressions is presented.
@InProceedings{FHPC18p1,
author = {Vadim Zaliva and Franz Franchetti},
title = {HELIX: A Case Study of a Formal Verification of High Performance Program Generation},
booktitle = {Proc.\ FHPC},
publisher = {ACM},
pages = {1--9},
doi = {10.1145/3264738.3264739},
year = {2018},
}
Publisher's Version
Modular Acceleration: Tricky Cases of Functional High-Performance Computing
Troels Henriksen, Martin Elsman, and
Cosmin E. Oancea
(University of Copenhagen, Denmark)
This case study examines the data-parallel functional implementation
of three algorithms: generation of quasi-random Sobol numbers,
breadth-first search, and calibration of Heston market parameters
via a least-squares procedure. We show that while all these
problems permit elegant functional implementations, good performance
depends on subtle issues that must be confronted in both the
implementations of the algorithms themselves, as well as the
compiler that is responsible for ultimately generating
high-performance code. In particular, we demonstrate a modular
technique for generating quasi-random Sobol numbers in an efficient
manner, study the efficient implementation of an irregular graph
algorithm without sacrificing parallelism, and argue for the utility
of nested regular data parallelism in the context of nonlinear
parameter calibration.
@InProceedings{FHPC18p10,
author = {Troels Henriksen and Martin Elsman and Cosmin E. Oancea},
title = {Modular Acceleration: Tricky Cases of Functional High-Performance Computing},
booktitle = {Proc.\ FHPC},
publisher = {ACM},
pages = {10--21},
doi = {10.1145/3264738.3264740},
year = {2018},
}
Publisher's Version
proc time: 0.48