Modelling concurrent objects running on the TSO and ARMv8 memory models
Modelling concurrent objects running on the TSO and ARMv8 memory models
复制标题
DOI：
10.1016/j.scico.2019.102308
复制
发表时间：
2019-10
期刊：
影响因子：
--
通讯作者：
Kirsten Winter;Graeme Smith;J. Derrick
中科院分区：
文献类型：
--
作者：
Kirsten Winter;Graeme Smith;J. Derrick
硬件弱内存模型，如TSO和ARM，用于通过允许程序指令以不同于软件指定的顺序在硬件上执行来提高并发程序的性能。这给这些程序中使用的并发对象的验证带来了挑战，因为需要考虑执行中的变化。有许多方法可以验证并发对象以及相关的工具支持。特别是，我们重点介绍了使用模型检查器检查线性化的线程局部方法，线性化是并发对象的标准正确性条件。与大多数其他方法一样，此方法不支持弱内存模型。为了重用这种已有的方法，我们展示了如何使用弱内存模型的语义来直接推导出在其下运行的并发对象的转换系统。我们对TSO和最新版本的ARM ARMv8都这样做了。因为TSO有一个简单的实现，所以我们在我们的转换系统中反映了这一点，该系统包括一个写入内存的缓冲区，该缓冲区镜像TSO的存储缓冲区。我们使用该方法生成的转换系统上的模型检验来说明线性化检验，而更复杂的ARMv8体系结构的实现不那么明显。在这种情况下，我们从现有的操作语义中派生出我们的转换系统，该语义与在ARM硬件上运行的数千个Litmus测试的结果一致。
Hardware weak memory models, such as TSO and ARM, are used to increase the performance of concurrent programs by allowing program instructions to be executed on the hardware in a different order to that specified by the software. This places a challenge on the verification of concurrent objects used in these programs since the variations in the executions need to be considered.Many approaches exist for verifying concurrent objects along with associated tool support. In particular, we focus on a thread-local approach to checkinglinearizability, the standard correctness condition for concurrent objects, using a model checker. This approach, like most others, does not support weak memory models. In order to reuse this existing approach, therefore, we show how to use the semantics of a weak memory model to directly derive a transition system of concurrent objects running under it.We do this for both TSO and the latest version of ARM, ARMv8. Since there is a straightforward implementation of TSO, we reflect this in our transition system which includes a buffer of writes to memory mirroring the store buffer of TSO. We illustrate linearizability checking using model checking on a transition system generated by this approach.The implementation of the significantly more complex ARMv8 architecture is less obvious. We derive our transition system in this case from an existing operational semantics that is consistent with the results of thousands of litmus test run on ARM hardware.