research-article

Open access

Verifying safety and accuracy of approximate parallel programs via canonical sequentialization

Authors:

Vimuth Fernando,

Sasa MisailovicAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 3, Issue OOPSLA

Article No.: 119, Pages 1 - 29

https://doi.org/10.1145/3360545

Published: 10 October 2019 Publication History

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.

Supplementary Material

a119-fernando (a119-fernando.webm)

Presentation at OOPSLA '19

Download
100.10 MB

References

[1]

R. J. Lipton. 1975. Reduction: A Method of Proving Properties of Parallel Programs. Commun. ACM 18 (1975).

[2]

J. L. Peterson. 1977. Petri nets. ACM Computing Surveys (CSUR) 3 (1977).

[3]

G. Agha and C. Hewitt. 1985. Concurrent Programming Using Actors: Exploiting Large-Scale Parallelism. Technical Report. Cambridge, MA, USA.

[4]

G. Agha. 1986. An Overview of Actor Languages. In OOPWORK.

[5]

P. Godefroid. 1996. Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Springer-Verlag.

[6]

G. Smith and D. Volpano. 1998. Secure Information Flow in a Multi-threaded Imperative Language. In POPL.

[7]

F. Huch. 1999. Verification of Erlang programs using abstract interpretation and model checking.

[8]

R. Milner. 1999. Communicating and mobile systems: the pi calculus. Cambridge university press.

Digital Library

[9]

L. Page, S. Brin, R. Motwani, and T. Winograd. 1999. The PageRank citation ranking: Bringing order to the web. Technical Report.

[10]

A. Gaffar, O. Mencer, W. Luk, P. Cheung, and N. Shirazi. 2002. Floating-point bitwidth analysis via automatic differentiation. In FPT.

[11]

J. Dean and S. Ghemawat. 2004. MapReduce: Simplified data processing on large clusters. OSDI (2004).

[12]

C. Flanagan and P. Godefroid. 2005. Dynamic Partial-order Reduction for Model Checking Software. In POPL.

[13]

S. F. Siegel. 2005. Efficient Verification of Halting Properties for MPI Programs with Wildcard Receives. In VMCAI.

[14]

S. F. Siegel and G. S. Avrunin. 2005. Modeling Wildcard-free MPI Programs for Verification. In PPoPP.

[15]

M. Rinard. 2006. Probabilistic accuracy bounds for fault-tolerant computations that discard tasks. In ICS.

[16]

L.-Å. Fredlund and H. Svensson. 2007. McErlang: a model checker for a distributed functional programming language. In ICFP.

[17]

W. Osborne, R. Cheung, J. Coutinho, W. Luk, and O. Mencer. 2007. Automatic accuracy-guaranteed bit-width optimization for fixed and floating-point systems. In FPL.

[18]

M. Rinard. 2007. Using Early Phase Termination to Eliminate Load Imbalances at Barrier Synchronization Points. In OOPSLA.

[19]

A. Lal and T. Reps. 2008. Reducing concurrent analysis under a context bound to sequential analysis. In International Conference on Computer Aided Verification. 37–51.

[20]

S. Chakradhar, A. Raghunathan, and J. Meng. 2009. Best-Effort Parallel Execution Framework for Recognition and Mining Applications. In IPDPS.

[21]

S. La Torre, P. Madhusudan, and G. Parlato. 2009. Reducing context-bounded concurrent reachability to sequential reachability. In International Conference on Computer Aided Verification. 477–492.

[22]

W. Baek and T. M. Chilimbi. 2010. Green: A Framework for Supporting Energy-Conscious Programming using Controlled Approximation. In PLDI.

Digital Library

[23]

S. Misailovic, S. Sidiroglou, H. Hoffmann, and M. Rinard. 2010. Quality of service profiling. In ICSE.

[24]

J. Ansel, Y. Wong, C. Chan, M. Olszewski, A. Edelman, and S. Amarasinghe. 2011. Language and compiler support for auto-tuning variable-accuracy algorithms. In CGO.

[25]

C. Bienia. 2011. Benchmarking modern multiprocessors.

[26]

S. Chaudhuri, S. Gulwani, R. Lublinerman, and S. Navidpour. 2011. Proving Programs Robust. In ESEC/FSE.

[27]

H. Hoffmann, S. Sidiroglou, M. Carbin, S. Misailovic, A. Agarwal, and M. Rinard. 2011. Dynamic Knobs for Responsive Power-Aware Computing. In ASPLOS.

[28]

S. Liu, K. Pattabiraman, T. Moscibroda, and B. G. Zorn. 2011. Flikker: saving DRAM refresh-power through critical data partitioning. (2011).

[29]

S. Misailovic, D. Roy, and M. Rinard. 2011. Probabilistically Accurate Program Transformations. In SAS.

[30]

B. Recht, C. Re, S. Wright, and F. Niu. 2011. Hogwild: A lock-free approach to parallelizing stochastic gradient descent. In Advances in neural information processing systems.

[31]

A. Sampson, W. Dietl, E. Fortuna, D. Gnanapragasam, L. Ceze, and D. Grossman. 2011. EnerJ: Approximate data types for safe and general low-power computation. In PLDI.

[32]

S. Sidiroglou, S. Misailovic, H. Hoffmann, and M. Rinard. 2011. Managing Performance vs. Accuracy Trade-offs With Loop Perforation. In FSE.

[33]

S. F. Siegel and G. Gopalakrishnan. 2011. Formal Analysis of Message Passing. In VMCAI.

[34]

A. Udupa, K. Rajan, and W. Thies. 2011. ALTER: Exploiting Breakable Dependences for Parallelization. In PLDI.

Digital Library

[35]

M. Carbin, D. Kim, S. Misailovic, and M. Rinard. 2012. Proving Acceptability Properties of Relaxed Nondeterministic Approximate Programs. In PLDI.

[36]

L. Renganarayana, V. Srinivasan, R. Nair, and D. Prener. 2012. Programming with relaxed synchronization. In Relax Workshop.

[37]

Z. Zhu, S. Misailovic, J. Kelner, and M. Rinard. 2012. Randomized Accuracy-Aware Program Transformations for Efficient Approximate Computations. In POPL.

[38]

M. Carbin, D. Kim, S. Misailovic, and M. Rinard. 2013a. Verified integrity properties for safe approximate program transformations. In PEPM.

[39]

M. Carbin, S. Misailovic, and M. C. Rinard. 2013b. Verifying Quantitative Reliability for Programs That Execute on Unreliable Hardware. In OOPSLA.

[40]

E. D’Osualdo, J. Kochems, and C.-H. L. Ong. 2013. Automatic verification of Erlang-style concurrency. In International Static Analysis Symposium.

[41]

S. Misailovic, D. Kim, and M. Rinard. 2013. Parallelizing Sequential Programs With Statistical Accuracy Tests. ACM TECS Special Issue on Probabilistic Embedded Computing (2013).

[42]

C. Rubio-González, C. Nguyen, H. Nguyen, J. Demmel, W. Kahan, K. Sen, D. Bailey, C. Iancu, and D. Hough. 2013. Precimonious: Tuning assistant for floating-point precision. In SC.

Digital Library

[43]

P. Abdulla, S. Aronis, B. Jonsson, and K. Sagonas. 2014. Optimal Dynamic Partial Order Reduction. In POPL.

[44]

J. Ansel, S. Kamil, K. Veeramachaneni, J. Ragan-Kelley, J. Bosboom, U. M. O’Reilly, and S. Amarasinghe. 2014. Opentuner: An extensible framework for program autotuning. In PACT.

Digital Library

[45]

A. Desai, P. Garg, and P. Madhusudan. 2014. Natural Proofs for Asynchronous Programs Using Almost-synchronous Reductions. In OOPSLA.

[46]

S. Misailovic, M. Carbin, S. Achour, Z. Qi, and M. C. Rinard. 2014. Chisel: Reliability- and Accuracy-aware Optimization of Approximate Computational Kernels. In OOPSLA.

Digital Library

[47]

M. Samadi, D. A. Jamshidi, J. Lee, and S. Mahlke. 2014. Paraprox: Pattern-based Approximation for Data Parallel Applications. In ASPLOS.

Digital Library

[48]

E. Schkufza, R. Sharma, and A. Aiken. 2014. Stochastic optimization of floating-point programs with tunable precision. In PLDI.

[49]

S. Achour and M. Rinard. 2015. Energy Efficient Approximate Computation with Topaz. In OOPSLA.

[50]

M. Ahmad, F. Hijaz, Q. Shi, and O. Khan. 2015. CRONO: A Benchmark Suite for Multithreaded Graph Algorithms Executing on Futuristic Multicores. In IISWC.

[51]

S. Blom, S. Darabi, and M. Huisman. 2015. Verification of loop parallelisations. In International Conference on Fundamental Approaches to Software Engineering. 202–217.

[52]

B. Boston, A. Sampson, D. Grossman, and L. Ceze. 2015. Probability type inference for flexible approximate programming. (2015).

[53]

S. Campanoni, G. Holloway, G.-Y. Wei, and D. Brooks. 2015. HELIX-UP: Relaxing program semantics to unleash parallelization. In CGO.

[54]

Y. Ding, J. Ansel, K. Veeramachaneni, X. Shen, U. M. O’Reilly, and S. Amarasinghe. 2015. Autotuning Algorithmic Choice for Input Sensitivity. In PLDI.

[55]

I. Goiri, R. Bianchini, S. Nagarakatte, and T. Nguyen. 2015. ApproxHadoop: Bringing Approximations to MapReduce Frameworks. In ASPLOS.

[56]

A. Sampson, A. Baixo, B. Ransford, T. Moreau, J. Yip, L. Ceze, and M. Oskin. 2015. ACCEPT: A Programmer-Guided Compiler Framework for Practical Approximate Computing. Technical Report.

[57]

M. Abadi, P. Barham, J. Chen, Z. Chen, A. Davis, J. Dean, M. Devin, S. Ghemawat, G. Irving, M. Isard, M. Kudlur, J. Levenberg, R. Monga, S. Moore, D. G. Murray, B. Steiner, P. Tucker, V. Vasudevan, P. Warden, M. Wicke, Y. Yu, and X. Zheng. 2016. TensorFlow: A System for Large-Scale Machine Learning. In OSDI.

[58]

R. Akram, M. M. U. Alam, and A. Muzahid. 2016. Approximate Lock: Trading off Accuracy for Performance by Skipping Critical Sections. In ISSRE.

[59]

A. Bakst, K. v. Gleissenthall, R. G. Kici, and R. Jhala. 2017. Verifying Distributed Programs via Canonical Sequentialization. In OOPSLA.

[60]

R. Boyapati, J. Huang, P. Majumder, K. H. Yum, and E. J. Kim. 2017. APPROX-NoC: A Data Approximation Framework for Network-On-Chip Architectures. In ISCA.

[61]

A. Canino and Y. D. Liu. 2017. Proactive and Adaptive Energy-aware Programming with Mixed Typechecking. In PLDI.

[62]

W.-F. Chiang, M. Baranowski, I. Briggs, A. Solovyev, G. Gopalakrishnan, and Z. Rakamarić. 2017. Rigorous floating-point mixed-precision tuning. In POPL.

[63]

M. Huisman. 2017. A Verification Technique for Deterministic Parallel Programs. In PPDP.

[64]

V. Magron, G. Constantinides, and A. Donaldson. 2017. Certified Roundoff Error Bounds Using Semidefinite Programming. ACM Trans. Math. Software 43, 4 (Jan. 2017).

Digital Library

[65]

S. Mitra, M. K. Gupta, S. Misailovic, and S. Bagchi. 2017. Phase-aware optimization in approximate computing. In CGO.

[66]

B. Nongpoh, R. Ray, S. Dutta, and A. Banerjee. 2017. AutoSense: A Framework for Automated Sensitivity Analysis of Program Data. IEEE Transactions on Software Engineering 43 (2017).

[67]

A. Yazdanbakhsh, D. Mahajan, H. Esmaeilzadeh, and P. Lotfi-Kamran. 2017. AxBench: A Multiplatform Benchmark Suite for Approximate Computing. IEEE Design Test 34, 2 (April 2017).

[68]

F. Betzel, K. Khatamifard, H. Suresh, D. J. Lilja, J. Sartori, and U. Karpuzcu. 2018. Approximate Communication: Techniques for Reducing Communication Bottlenecks in Large-Scale Parallel Systems. ACM Computing Surveys (CSUR) 51 (2018).

Digital Library

[69]

B. Boston, Z. Gong, and M. Carbin. 2018. Leto: verifying application-specific hardware fault tolerance with programmable execution models. In OOPSLA.

[70]

E. Darulova, A. Izycheva, F. Nasir, F. Ritter, H. Becker, and R. Bastian. 2018. Daisy-Framework for Analysis and Optimization of Numerical Programs (Tool Paper). In TACAS.

[71]

E. A. Deiana, V. St-Amour, P. A. Dinda, N. Hardavellas, and S. Campanoni. 2018. Unconventional Parallelization of Nondeterministic Applications. In ASPLOS.

[72]

S. He, S. K. Lahiri, and Z. Rakamarić. 2018. Verifying relative safety, accuracy, and termination for program approximations. Journal of Automated Reasoning 60, 1 (2018).

Digital Library

[73]

S. K. Khatamifard, I. Akturk, and U. R. Karpuzcu. 2018. On Approximate Speculative Lock Elision. IEEE Transactions on Multi-Scale Computing Systems 2 (2018).

[74]

J. Lidman and S. A. Mckee. 2018. Verifying Reliability Properties Using the Hyperball Abstract Domain. ACM Transactions on Programming Languages and Systems (TOPLAS) 40, 1 (2018), 3.

Digital Library

[75]

P. Stanley-Marbell and M. Rinard. 2018. Perceived-Color Approximation Transforms for Programs that Draw. IEEE Micro 38, 4 (2018), 20–29.

[76]

J. R. Stevens, A. Ranjan, and A. Raghunathan. 2018. AxBA: an approximate bus architecture framework. In ICCAD.

[77]

R. Xu, J. Koo, R. Kumar, P. Bai, S. Mitra, S. Misailovic, and S. Bagchi. 2018. Videochef: efficient approximation for streaming video processing pipelines. In USENIX ATC.

[78]

V. Fernando, A. Franques, S. Abadal, S. Misailovic, and J. Torrellas. 2019a. Replica: A Wireless Manycore for CommunicationIntensive and Approximate Data. In ASPLOS.

Digital Library

[79]

V. Fernando, K. Joshi, D. Marinov, and S. Misailovic. 2019c. Identifying Optimal Parameters for Randomized Approximate Algorithms. In Workshop on Approximate Computing Across the Stack.

[80]

V. Fernando, K. Joshi, and S. Misailovic. 2019b. Appendix to Parallely https://vimuth.github.io/parallely/appendix.pdf.

[81]

K. Gleissenthall, R. G. Kici, A. Bakst, D. Stefan, and R. Jhala. 2019. Pretend Synchrony. In POPL.

[82]

K. Joshi, V. Fernando, and S. Misailovic. 2019. Statistical Algorithmic Profiling for Randomized Approximate Programs. In ICSE.

[83]

E. Michael, D. Woos, T. Anderson, M. D. Ernst, and Z. Tatlock. 2019. Teaching Rigorous Distributed Systems With Efficient Model Checking. In EuroSys.

Cited By

Misailovic S(2022)Accuracy-Aware CompilersApproximate Computing Techniques10.1007/978-3-030-94705-7_7(177-214)Online publication date: 3-Jan-2022
https://doi.org/10.1007/978-3-030-94705-7_7
Jakobs MPauck FPlatzner MWehrheim HWiersema T(2021)Software/Hardware Co-Verification for Custom Instruction Set ProcessorsIEEE Access10.1109/ACCESS.2021.31312139(160559-160579)Online publication date: 2021
https://doi.org/10.1109/ACCESS.2021.3131213
Fernando VJoshi KLaurel JMisailovic S(2021)Diamont: Dynamic Monitoring of Uncertainty for Distributed Asynchronous ProgramsRuntime Verification10.1007/978-3-030-88494-9_10(184-206)Online publication date: 6-Oct-2021
https://doi.org/10.1007/978-3-030-88494-9_10
Show More Cited By

Index Terms

Verifying safety and accuracy of approximate parallel programs via canonical sequentialization
1. Computing methodologies
  1. Parallel computing methodologies
    1. Parallel programming languages
2. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification

Recommendations

Compiling machine-independent parallel programs

Initial evidence is presented that explicitly parallel, machine-independent programs can automatically be translated into parallel machine code that is competitive in performance with hand-written code.The programming language used is Modula-2*, an ...
Compiling data-parallel programs for clusters of SMPs: Research Articles
Compilers for Parallel Computers

Clusters of shared-memory multiprocessors (SMPs) have become the most promising parallel computing platforms for scientific computing. However, SMP clusters significantly increase the complexity of user application development when using the low-level ...
Parallel Solution of the Wave Equation Using Higher Order Finite Elements
MPIDC '96: Proceedings of the Second MPI Developers Conference

Abstract: We present a parallel solver for wave propagation problems based on the higher-order explicit finite elements developed by Cohen et al. (1995) These elements were introduce to allow mass-lumping while preserving high accuracy. Our approach is ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 3, Issue OOPSLA

October 2019

2077 pages

EISSN:2475-1421

DOI:10.1145/3366395

Issue’s Table of Contents

Copyright © 2019 Owner/Author.

Permission to make digital or hard copies of part or all 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 third-party components of this work must be honored. For all other uses, contact the Owner/Author.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 10 October 2019

Published in PACMPL Volume 3, Issue OOPSLA

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
473
Total Downloads

Downloads (Last 12 months)60
Downloads (Last 6 weeks)10

Reflects downloads up to 15 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Misailovic S(2022)Accuracy-Aware CompilersApproximate Computing Techniques10.1007/978-3-030-94705-7_7(177-214)Online publication date: 3-Jan-2022
https://doi.org/10.1007/978-3-030-94705-7_7
Jakobs MPauck FPlatzner MWehrheim HWiersema T(2021)Software/Hardware Co-Verification for Custom Instruction Set ProcessorsIEEE Access10.1109/ACCESS.2021.31312139(160559-160579)Online publication date: 2021
https://doi.org/10.1109/ACCESS.2021.3131213
Fernando VJoshi KLaurel JMisailovic S(2021)Diamont: Dynamic Monitoring of Uncertainty for Distributed Asynchronous ProgramsRuntime Verification10.1007/978-3-030-88494-9_10(184-206)Online publication date: 6-Oct-2021
https://doi.org/10.1007/978-3-030-88494-9_10
Stanley-Marbell PAlaghi ACarbin MDarulova EDolecek LGerstlauer AGillani GJevdjic DMoreau TCacciotti MDaglis AJerger NFalsafi BMisailovic SSampson AZufferey D(2020)Exploiting Errors for EfficiencyACM Computing Surveys10.1145/339489853:3(1-39)Online publication date: 12-Jun-2020
https://dl.acm.org/doi/10.1145/3394898
Joshi KFernando VMisailovic SMars JTang LXue JWu P(2020)Aloe: verifying reliability of approximate programs in the presence of recovery mechanismsProceedings of the 18th ACM/IEEE International Symposium on Code Generation and Optimization10.1145/3368826.3377924(56-67)Online publication date: 22-Feb-2020
https://dl.acm.org/doi/10.1145/3368826.3377924
Leon VHanif MArmeniakos GJiao XShafique MPekmestzi KSoudris D(undefined)Approximate Computing Survey, Part II: Application-Specific & Architectural Approximation Techniques and ApplicationsACM Computing Surveys10.1145/3711683
https://dl.acm.org/doi/10.1145/3711683

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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 Article

Figures

Tables

Media

View Issue’s Table of Contents