勿坐视观望:一种自动插入内存屏障的静态分析方法
计算机科学中的逻辑
2014-06-10 v2 软件工程
摘要
现代架构依赖内存屏障来防止内存一致性出现不必要的弱化。由于屏障的语义可能十分微妙,其放置的自动化显得尤为可取。然而,用于恢复一致性的精确方法难以扩展到已部署的系统代码中。我们选择牺牲部分精度以换取真正的可扩展性:我们的技术适用于大型代码库。我们将该技术实现在新的 musketeer 工具中,并详细介绍了在 Debian Linux 7.1 中发现的软件包的超过 350 个可执行文件上的实验,例如 memcached(约 10000 行代码)。
引用
@article{arxiv.1312.1411,
title = {Don't sit on the fence: A static analysis approach to automatic fence insertion},
author = {Jade Alglave and Daniel Kroening and Vincent Nimal and Daniel Poetzl},
journal= {arXiv preprint arXiv:1312.1411},
year = {2014}
}
备注
19 pages, 19 figures