...
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Science of Computer Programming >Modelling concurrent objects running on the TSO and ARMv8 memory models
【24h】

Modelling concurrent objects running on the TSO and ARMv8 memory models

机译：对在TSO和ARMv8内存模型上运行的并发对象进行建模

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

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 checking linearizability, 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. (C) 2019 Elsevier B.V. All rights reserved.
机译：诸如TSO和ARM之类的硬件弱存储器模型用于通过允许以与软件指定顺序不同的顺序在硬件上执行程序指令来提高并发程序的性能。由于需要考虑执行方式的变化，因此对验证这些程序中使用的并发对象提出了挑战。存在许多用于验证并发对象以及相关工具支持的方法。特别是，我们专注于使用模型检查器检查线性化性（并发对象的标准正确性条件）的线程局部方法。与大多数其他方法一样，此方法不支持弱内存模型。因此，为了重用这种现有方法，我们展示了如何使用弱内存模型的语义直接导出在其下运行的并发对象的过渡系统。我们对TSO和最新版本的ARM ARMv8都这样做。由于TSO的实现很简单，因此我们在过渡系统中反映了这一点，该过渡系统包括对内存的写缓冲区和TSO的存储缓冲区的镜像。我们通过在此方法生成的过渡系统上使用模型检查来说明线性化检查。明显更复杂的ARMv8架构的实现不太明显。在这种情况下，我们从现有的操作语义派生出过渡系统，该语义与在ARM硬件上运行的数千个石蕊测试的结果一致。 （C）2019 Elsevier B.V.保留所有权利。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号