Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Specifying and verifying sparse matrix codes
Arnold G., Hölzl J., Köksal A., Bodík R., Sagiv M. ACM SIGPLAN Notices45 (9):249-260,2010.Type:Article
Date Reviewed: Nov 7 2011

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.

Reviewer:  Jacques Carette Review #: CR139566 (1204-0383)
Bookmark and Share
  Featured Reviewer  
 
Specialized Application Languages (D.3.2 ... )
 
 
Mechanical Verification (F.3.1 ... )
 
Would you recommend this review?
yes
no
Other reviews under "Specialized Application Languages": Date
An experimental study of people creating spreadsheets
Brown P., Gould J. ACM Transactions on Information Systems 5(3): 258-272, 1987. Type: Article
Jul 1 1988
Types and persistence in database programming languages
Atkinson M., Buneman O. ACM Computing Surveys 19(2): 105-170, 1987. Type: Article
Apr 1 1989
Programming languages for distributed computing systems
Bal H., Steiner J., Tanenbaum A. ACM Computing Surveys 21(3): 261-322, 1989. Type: Article
Aug 1 1990
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy