Dynamic Checking of Safe Concurrent Memory Access using Shared Ownership
This addresses the difficulty for programmers and compilers in correctly applying synchronization mechanisms to protect shared resources in concurrent programming, though it appears incremental as it builds on ownership concepts with added flexibility.
The paper tackles the problem of ensuring safe concurrent memory access in shared-memory programming by introducing a shared ownership mechanism that automatically checks for proper protection, and it demonstrates the approach's expressiveness and efficiency on various programs while proving freedom from data races.
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.