一句话：为采用自失效/自降级的一致性协议建立形式语义，并给出面向安全性的最小代价栅栏插入方法。
基于自失效与自降级的一致性协议因简单、潜在高性能和低能耗而受到关注，但它们会导致内存指令重排序，产生程序员非预期的额外程序行为。本文提出一种新的形式模型，刻画此类协议下程序运行的语义，并引入与一致性层交互的多种栅栏。基于该模型，作者设计了可达性分析与安全性属性检查算法，用于判断当前栅栏集合下程序是否满足给定安全性质。进一步提出反例引导的栅栏插入方法，可插入最优栅栏集合以保证程序正确性，并能处理成本各异的栅栏，从而优化总代价而非仅栅栏数量。作者实现了原型系统，在大量示例与基准上验证方法，并通过模拟评估插入栅栏后程序的性能。
Cache coherence protocols based on self-invalidation and self-downgrade have recently seen increased popularity due to their simplicity, potential performance efficiency, and low energy consumption. However, such protocols result in memory instruction reordering, thus causing extra program behaviors that are often not intended by the programmers. We propose a novel formal model that captures the semantics of programs running under such protocols, and features a set of fences that interact with the coherence layer. Using the model, we design an algorithm to analyze the reachability and check whether a program satisfies a given safety property with the current set of fences. We describe a method for insertion of optimal sets of fences that ensure correctness of the program under such protocols. The method relies on a counter-example guided fence insertion procedure. One feature of our method is that it can handle a variety of fences (with different costs). This diversity makes optimization more difficult since one has to optimize the total cost of the inserted fences, rather than just their number. To demonstrate the strength of our approach, we have implemented a prototype and run it on a wide range of examples and benchmarks. We have also, using simulation, evaluated the performance of the resulting fenced programs.
@article{paperbot435,
title = {Mending Fences with Self-Invalidation and Self-Downgrade},
author = {Parosh Aziz Abdulla and Mohamed Faouzi Atig and Stefanos Kaxiras and Carl Leonardsson and Alberto Ros and Yunyun Zhu},
journal = {Logical Methods in Computer Science},
volume = {Volume 14, Issue 1},
year = {2018},
doi = {10.23638/lmcs-14(1:6)2018}
}