research-article

Specifying and verifying sparse matrix codes

Authors:

Mooly SagivAuthors Info & Claims

ACM SIGPLAN Notices, Volume 45, Issue 9

Pages 249 - 260

https://doi.org/10.1145/1932681.1863581

Published: 27 September 2010 Publication History

Get Access

Abstract

Sparse matrix formats are typically implemented with low-level imperative programs. The optimized nature of these implementations hides the structural organization of the sparse format and complicates its verification. We define a variable-free functional language (LL) in which even advanced formats can be expressed naturally, as a pipeline-style composition of smaller construction steps. We translate LL programs to Isabelle/HOL and describe a proof system based on parametric predicates for tracking relationship between mathematical vectors and their concrete representations. This proof theory automatically verifies full functional correctness of many formats. We show that it is reusable and extensible to hierarchical sparse formats.

Supplementary Material

JPG File (icfp-weds-1030-arnoldholzl.jpg)

Download
4.88 KB

MOV File (icfp-weds-1030-arnoldholzl.mov)

Download
118.20 MB

References

[1]

}}J. Backus. Can programming be liberated from the von Neumann style? A functional style and its algebra of programs. Communications of the ACM (CACM), 21(8):613--641, 1978.

Digital Library

Google Scholar

[2]

}}A. J. C. Bik, P. Brinkhaus, P. M. W. Knijnenburg, and H. A. G. Wijshoff. The automatic generation of sparse primitives. ACM Transactions on Mathematical Software, 24(2):190--225, 1998.

Digital Library

Google Scholar

[3]

}}G. E. Blelloch. Programming parallel algorithms. Communications of the ACM (CACM), 39(3):85--97, 1996.

Digital Library

Google Scholar

[4]

}}M. M. T. Chakravarty, R. Leshchinskiy, S. P. Jones, G. Keller, and S. Marlow. Data Parallel Haskell: a status report. In Workshop on Declarative Aspects of Multicore Programming (DAMP), pages 10--18, New York, NY, USA, 2007. ACM.

Digital Library

Google Scholar

[5]

}}J. Duan, J. Hurd, G. Li, S. Owens, K. Slind, and J. Zhang. Functional correctness proofs of encryption algorithms. In Logic for Programming, Artificial Intelligence and Reasoning (LPAR), pages 519--533, 2005.

Digital Library

Google Scholar

[6]

}}C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended static checking for Java. In Programming Languages Design and Implementation, pages 234--245, 2002.

Digital Library

Google Scholar

[7]

}}E.-J. Im. Optimizing the performance of sparse matrix-vector multiplication. PhD thesis, University of California, Berkeley, 2000.

Digital Library

Google Scholar

[8]

}}V. Kotlyar and K. Pingali. Sparse code generation for imperfectly nested loops with dependences. In International Conference on Supercomputing (ICS), pages 188--195, 1997.

Digital Library

Google Scholar

[9]

}}V. Kotlyar, K. Pingali, and P. Stodghill. A relational approach to the compilation of sparse matrix programs. In Euro-Par, pages 318--327, 1997.

Digital Library

Google Scholar

[10]

}}N. Mateev, K. Pingali, P. Stodghill, and V. Kotlyar. Next-generation generic programming and its application to sparse matrix computations. In International Conference on Supercomputing (ICS), pages 88--99, 2000.

Digital Library

Google Scholar

[11]

}}T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer-Verlag, 2002.

Digital Library

Google Scholar

[12]

}}S. Obua. Flyspeck II: The Basic Linear Programs. PhD thesis, Technische Universität München, 2008.

Google Scholar

[13]

}}M. Sagiv, T. W. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems (TOPLAS), 24(3):217--298, 2002.

Digital Library

Google Scholar

[14]

}}R. W. Vuduc. Automatic performance tuning of sparse matrix kernels. PhD thesis, University of California, Berkeley, 2004.

Digital Library

Google Scholar

[15]

}}M. Wenzel. The Isabelle/Isar Implementation. Technische Universität München. http://isabelle.in.tum.de/doc/implementation.pdf.

Google Scholar

[16]

}}M. Wildmoser and T. Nipkow. Certifying machine code safety: Shallow versus deep embedding. In International Conference on Theorem Proving in Higher-Order Logics, pages 305--320, 2004.

Crossref

Google Scholar

Cited By

View all

Zhang GHsu OKjolstad F(2024)Compilation of Modular and General Sparse WorkspacesProceedings of the ACM on Programming Languages10.1145/36564268:PLDI(1213-1238)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656426
Liu JZhao ZDing ZBrock BRong HZhang Z(2024)UniSparse: An Intermediate Language for General Sparse Format CustomizationProceedings of the ACM on Programming Languages10.1145/36498168:OOPSLA1(137-165)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649816
Du ZLi JWang YLi XTan GSun NWolf FShende SCulhane CAlam SJagode H(2022)AlphaSparseProceedings of the International Conference on High Performance Computing, Networking, Storage and Analysis10.5555/3571885.3571972(1-15)Online publication date: 13-Nov-2022
https://dl.acm.org/doi/10.5555/3571885.3571972
Show More Cited By

Index Terms

Specifying and verifying sparse matrix codes
1. Software and its engineering
  1. Software notations and tools
    1. Context specific languages
      1. Specialized application languages
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program verification

Recommendations

Specifying and verifying sparse matrix codes
ICFP '10: Proceedings of the 15th ACM SIGPLAN international conference on Functional programming

Sparse matrix formats are typically implemented with low-level imperative programs. The optimized nature of these implementations hides the structural organization of the sparse format and complicates its verification. We define a variable-free ...
Verifying higher-order functional programs with pattern-matching algebraic data types
POPL '11

Type-based model checking algorithms for higher-order recursion schemes have recently emerged as a promising approach to the verification of functional programs. We introduce pattern-matching recursion schemes (PMRS) as an accurate model of computation ...
Verifying concurrent probabilistic systems using probabilistic-epistemic logic specifications

In this paper, we address the problem of verifying probabilistic and epistemic properties in concurrent probabilistic systems expressed in PCTLK. PCTLK is an extension of the Probabilistic Computation Tree Logic (PCTL) augmented with Knowledge (K). In ...

Reviews

Reviewer: Jacques Carette

It is increasingly recognized that the heroics involved in coding efficient, low-level, imperative programs for various tasks are not sustainable. While the gain in efficiency might be quite real, the loss of certainty (with respect to correctness) is just as real. A promising, recent line of research is to instead use a focused, purely functional, higher-level domain-specific language (DSL). The use of a focused DSL, here referred to as a "little language,"? presents opportunities to encode the complex invariants that are natural in a domain in ways that are typically unavailable in general-purpose, imperative languages. In this paper, the domain choices are sparse matrix formats and associated (simple) operations. The result of picking the right abstractions (for example, those that are derived from the natural semantics of the domain) and omitting general-purpose abstractions is a language that can be fruitfully used to generate low-level implementations; in addition, its correctness can be mechanically verified (the authors choose Isabelle/HOL for this purpose). The authors present their work in a very readable manner, with well-chosen and well-illustrated examples. The material is appropriately motivated, with a pleasant mix of conceptual illustration and formal presentation. Several nice ideas are presented, including a shift to relations rather than representation functions. The authors also use solid engineering details to simplify their proofs. This work might have been better had the authors been more aware of related works such as single-assignment C, computer algebra, and the Spiral project. Furthermore, their (ab)use of lists and predicates (like their indexed lists and associative lists) lies at a somewhat lower level of abstraction than would be optimal. The use of rewrite rules also makes certain parts feel more ad hoc than seems necessary. Nevertheless, this represents an excellent step forward in the quest for liberating efficient sparse matrix codes from the tyranny of low-level languages and moving those codes into the realm of modular specification and verification. Online Computing Reviews Service

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ACM SIGPLAN Notices Volume 45, Issue 9

ICFP '10

September 2010

382 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1932681

Issue’s Table of Contents

ICFP '10: Proceedings of the 15th ACM SIGPLAN international conference on Functional programming
September 2010
398 pages
ISBN:9781605587943
DOI:10.1145/1863543
General Chair:
Paul Hudak
Yale University, USA
,
Program Chair:
Stephanie Weirich
University of Pennsylvania, USA

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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 27 September 2010

Published in SIGPLAN Volume 45, Issue 9

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

34
Total Citations
View Citations
340
Total Downloads

Downloads (Last 12 months)9
Downloads (Last 6 weeks)2

Reflects downloads up to 12 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Zhang GHsu OKjolstad F(2024)Compilation of Modular and General Sparse WorkspacesProceedings of the ACM on Programming Languages10.1145/36564268:PLDI(1213-1238)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656426
Liu JZhao ZDing ZBrock BRong HZhang Z(2024)UniSparse: An Intermediate Language for General Sparse Format CustomizationProceedings of the ACM on Programming Languages10.1145/36498168:OOPSLA1(137-165)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649816
Du ZLi JWang YLi XTan GSun NWolf FShende SCulhane CAlam SJagode H(2022)AlphaSparseProceedings of the International Conference on High Performance Computing, Networking, Storage and Analysis10.5555/3571885.3571972(1-15)Online publication date: 13-Nov-2022
https://dl.acm.org/doi/10.5555/3571885.3571972
Du ZLi JWang YLi XTan GSun N(2022)AlphaSparse: Generating High Performance SpMV Codes Directly from Sparse MatricesSC22: International Conference for High Performance Computing, Networking, Storage and Analysis10.1109/SC41404.2022.00071(1-15)Online publication date: Nov-2022
https://doi.org/10.1109/SC41404.2022.00071
Zhang P(2020)Characterizing several properties of high-dimensional random Apollonian networksJournal of Complex Networks10.1093/comnet/cnaa0388:4Online publication date: 16-Dec-2020
https://doi.org/10.1093/comnet/cnaa038
Dyer TAltuntas ABaugh J(2019)Bounded Verification of Sparse Matrix Computations2019 IEEE/ACM 3rd International Workshop on Software Correctness for HPC Applications (Correctness)10.1109/Correctness49594.2019.00010(36-43)Online publication date: Nov-2019
https://doi.org/10.1109/Correctness49594.2019.00010
Baugh JAltuntas A(2018)Formal methods and finite element analysis of hurricane storm surge: A case study in software verificationScience of Computer Programming10.1016/j.scico.2017.08.012158(100-121)Online publication date: Jun-2018
https://doi.org/10.1016/j.scico.2017.08.012
Laird ALiu BBjørner NDehnavi M(2024)SpEQ: Translation of Sparse Codes using EquivalencesProceedings of the ACM on Programming Languages10.1145/36564458:PLDI(1680-1703)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656445
Gladshtein VZhao QAhrens WAmarasinghe SSergey I(2024)Mechanised Hypersafety Proofs about Structured DataProceedings of the ACM on Programming Languages10.1145/36564038:PLDI(647-670)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656403
Liu JZhao ZDing ZBrock BRong HZhang Z(2024)UniSparse: An Intermediate Language for General Sparse Format CustomizationProceedings of the ACM on Programming Languages10.1145/36498168:OOPSLA1(137-165)Online publication date: 29-Apr-2024
https://doi.org/10.1145/3649816
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

EPUB

View this article in ePub.

ePub

Abstract

Supplementary Material

References

Cited By

Index Terms

Recommendations