基于共享所有权的安全并发内存访问的动态检查
Dynamic Checking of Safe Concurrent Memory Access using Shared Ownership
摘要：
在共享存储器并发编程中，可以使用诸如监视器或通道之类的同步机制来保护共享资源。然而，这些机制和它们所保护的资源之间的联系只是隐含地给出的;这使得程序员很难正确地应用这些机制，编译器也很难检查资源是否得到了适当的保护。本文提出了一种自动检查共享内存是否被正确访问的机制，使用一种称为共享所有权的方法。与传统的所有权相比，共享所有权允许多个所有者拥有资源，从而提供了更大的灵活性。在此方法的基础上，我们定义了一个抽象的资源访问模型，提供操作来管理数据依赖关系，以及共享和访问权限的转移。该模型是严格定义的使用正式的语义，并显示是免费的数据竞争。当模拟模型和程序执行时，此属性可用于检测不安全的内存访问。该方法的表现力和效率证明了各种程序使用常见的同步机制。
英文摘要：
In shared-memory concurrent programming, shared resources can be protected using synchronization mechanisms such as monitors or channels. The connection between these mechanisms and the resources they protect is, however, only given implicitly; this makes it difficult both for programmers to apply the mechanisms correctly and for compilers to check that resources are properly protected. This paper presents a mechanism to automatically check that shared memory is accessed properly, using a methodology called shared ownership. In contrast to traditional ownership, shared ownership offers more flexibility by permitting multiple owners of a resource. On the basis of this methodology, we define an abstract model of resource access that provides operations to manage data dependencies, as well as sharing and transfer of access privileges. The model is rigorously defined using a formal semantics, and shown to be free from data races. This property can be used to detect unsafe memory accesses when simulating the model together with the execution of a program. The expressiveness and efficiency of the approach is demonstrated on a variety of programs using common synchronization mechanisms.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
