Automatic Parallelization and Optimization of Programs by Proof Rewriting
Automatic Parallelization and Optimization of Programs by Proof Rewriting
复制标题
通过证明重写实现程序的自动并行化和优化
DOI：
10.1007/978-3-642-03237-0_6
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
C. Hurlin
中科院分区：
文献类型：
--
作者：
C. Hurlin
我们展示了如何给定一个程序及其分离逻辑证明，可以并行化和优化该程序并同时转换其证明以获得经过验证的并行和优化的程序。为了实现此目标，我们提出了新的证明规则，以生成证明树和在证明树上的重写系统。
We show how, given a program and its separation logic proof, one can parallelize and optimize this program and transform its proof simultaneously to obtain a proven parallelized and optimized program. To achieve this goal, we present new proof rules for generating proof trees and a rewrite system on proof trees.