Verifying safety and accuracy of approximate parallel programs via canonical sequentialization
Verifying safety and accuracy of approximate parallel programs via canonical sequentialization
复制标题
通过规范序列化验证近似并行程序的安全性和准确性
DOI：
10.1145/3360545
复制
发表时间：
2019
影响因子：
--
通讯作者：
Misailovic, Sasa
中科院分区：
文献类型：
--
作者：
Fernando, Vimuth;Joshi, Keyur;Misailovic, Sasa
我们提出parallel，一种编程语言和一个系统来验证并行消息传递程序中的近似。parallel语言可以表达各种软件和硬件级近似，以牺牲结果精度为代价减少计算和通信开销。并行的安全性分析可以证明在近似计算中不存在死锁，其类型系统可以保证近似值不干扰精确值。并行的定量精度分析可以推断出误差的频率和大小。为了支持这样的分析，parallel提供了一种近似感知版本的规范序列化，这是一种最近提出的验证技术，它生成的顺序程序可以捕获结构良好的并行程序（即满足对称非确定性属性的程序）的语义。据我们所知，parallel是第一个用于分析并行近似程序的系统。我们在图形分析、图像处理和数值分析领域的八个基准应用程序上展示了parallel的有效性。我们还从文献中编码和研究了五种近似机制。我们的parallel实现自动有效地证明了近似基准的类型安全性、可靠性和准确性。
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.