Resource-sensitive synchronization inference by abduction
Resource-sensitive synchronization inference by abduction
复制标题
通过溯因推理进行资源敏感的同步推断
DOI：
10.1145/2103621.2103694
复制
发表时间：
2012
影响因子：
--
通讯作者：
Botincan M
中科院分区：
文献类型：
--
作者：
Botincan M
我们提出了一个分析，它作为其输入的顺序程序，增加注释表明潜在的并行化的机会，和顺序证明，写在分离逻辑，并产生一个正确同步的并行程序和证明该程序。与以前的工作不同，我们不是一个独立的分析，我们插入同步结构，以保持相关的依赖关系中发现的顺序程序，否则可能会违反一个天真的翻译。分离逻辑允许我们并行化细粒度的资源使用模式，超越简单的分析点。我们的分析通过使用顺序证明来发现程序不同部分之间的依赖关系。它利用这些发现的依赖关系来指导同步原语插入到并行化程序中，并确保所得到的并行化程序满足与原始顺序程序相同的规范，并表现出相同的顺序行为。我们的分析是建立使用框架推理和溯因，两种技术支持越来越多的分离逻辑工具。
We present an analysis which takes as its input a sequential program, augmented with annotations indicating potential parallelization opportunities, and a sequential proof, written in separation logic, and produces a correctly-synchronized parallelized program and proof of that program. Unlike previous work, ours is not an independence analysis; we insert synchronization constructs to preserve relevant dependencies found in the sequential program that may otherwise be violated by a naive translation. Separation logic allows us to parallelize fine-grained patterns of resource-usage, moving beyond straightforward points-to analysis. Our analysis works by using the sequential proof to discover dependencies between different parts of the program. It leverages these discovered dependencies to guide the insertion of synchronization primitives into the parallelized program, and to ensure that the resulting parallelized program satisfies the same specification as the original sequential program, and exhibits the same sequential behaviour. Our analysis is built using frame inference and abduction, two techniques supported by an increasing number of separation logic tools.
登录
查看更多内容
确定性并行的模块化推理
影响因子：
--
作者：
Dodds M
通讯作者：
Dodds M
减少 DOACROSS 循环嵌套的数据通信开销
影响因子：
2.8
作者：
P. Tang;J. Zigman
通讯作者：
J. Zigman
通过证明重写实现程序的自动并行化和优化
DOI：
10.1007/978-3-642-03237-0_6
发表时间：
2009
期刊：
ArXiv
影响因子：
--
作者：
C. Hurlin
通讯作者：
C. Hurlin
DOI：
10.2168/lmcs-7(3:10)2011
发表时间：
2010
期刊：
Log. Methods Comput. Sci.
影响因子：
--
作者：
Jyotirmoy V. Deshmukh;G. Ramalingam;Venkatesh Prasad Ranganath;K. Vaswani
通讯作者：
K. Vaswani
使用 Heap-Hop 跟踪跳跃的堆
DOI：
10.1007/978-3-642-12002-2_23
发表时间：
2010
期刊：
Proceedings of the 7th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering
影响因子：
--
作者：
Jules Villard;É. Lozes;Cristiano Calcagno
通讯作者：
Cristiano Calcagno