Verifying safety and accuracy of approximate parallel programs via canonical sequentialization
- 10 October 2019
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in Proceedings of the ACM on Programming Languages
- Vol. 3 (OOPSLA), 1-29
- https://doi.org/10.1145/3360545
Abstract
We present Parallely, a programming language and a system for verification of approximations in parallel message-passing programs. Parallely's language can express various software and hardware level approximations that reduce the computation and communication overheads at the cost of result accuracy. Parallely's safety analysis can prove the absence of deadlocks in approximate computations and its type system can ensure that approximate values do not interfere with precise values. Parallely's quantitative accuracy analysis can reason about the frequency and magnitude of error. To support such analyses, Parallely presents an approximation-aware version of canonical sequentialization, a recently proposed verification technique that generates sequential programs that capture the semantics of well-structured parallel programs (i.e., ones that satisfy a symmetric nondeterminism property). To the best of our knowledge, Parallely is the first system designed to analyze parallel approximate programs. We demonstrate the effectiveness of Parallely on eight benchmark applications from the domains of graph analytics, image processing, and numerical analysis. We also encode and study five approximation mechanisms from literature. Our implementation of Parallely automatically and efficiently proves type safety, reliability, and accuracy properties of the approximate benchmarks.Funding Information
- Defense Advanced Research Projects Agency (Contract No. HR0011-18-C-0122)
- National Science Foundation (CCF-1629431, CCF-1703637, CCF-1846354,)
This publication has 69 references indexed in Scilit:
- Natural proofs for asynchronous programs using almost-synchronous reductionsACM SIGPLAN Notices, 2014
- Stochastic optimization of floating-point programs with tunable precisionACM SIGPLAN Notices, 2014
- Parallelizing Sequential Programs with Statistical Accuracy TestsACM Transactions on Embedded Computing Systems, 2013
- Automatic Verification of Erlang-Style ConcurrencyPublished by Springer Science and Business Media LLC ,2013
- FlikkerACM SIGPLAN Notices, 2011
- Dynamic knobs for responsive power-aware computingACM SIGPLAN Notices, 2011
- Probabilistically Accurate Program TransformationsLecture Notes in Computer Science, 2011
- Formal Analysis of Message PassingLecture Notes in Computer Science, 2011
- Efficient Verification of Halting Properties for MPI Programs with Wildcard ReceivesLecture Notes in Computer Science, 2005
- Concurrent programming using actors: Exploiting large-scale parallelismLecture Notes in Computer Science, 1985