Verifying Safety and Accuracy of Approximate Parallel Programs via Canonical Sequentialization
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.
Fri 25 OctDisplayed time zone: Beirut change
11:00 - 12:30
|Efficient Lock-Free Durable Sets|
Yoav Zuriel Technion - Israel, Michal Friedman Technion - Israel, Gali Sheffi Technion - Israel, Nachshon Cohen Amazon, Erez Petrank Technion - IsraelDOI
|Weak Persistency Semantics from the Ground Up: Formalising the Persistency Semantics of ARMv8 and Transactional Models|
Azalea Raad MPI-SWS, Germany, John Wickerson Imperial College London, Viktor Vafeiadis MPI-SWS, GermanyDOI
|Verifying Safety and Accuracy of Approximate Parallel Programs via Canonical Sequentialization|
Vimuth Fernando University of Illinois at Urbana-Champaign, Keyur Joshi University of Illinois at Urbana-Champaign, Sasa Misailovic University of Illinois at Urbana-ChampaignDOI
|Dependence-Aware, Unbounded Sound Predictive Race Detection|
Kaan Genç Ohio State University, Jake Roemer Ohio State University, Yufan Xu Ohio State University, Michael D. Bond Ohio State UniversityDOI Pre-print