This project investigates the foundational aspects of an alternative approach to the specification, implementation and management of concurrent activities which is referred to as data-centric synchronization. Traditional approaches take an operational view of concurrency control, they burden the programmer with the need to identify sets of control flow paths in their program which must not interfere. This has been shown to be difficult to get right and, more often than not, to inhibit scalability to multicore systems as the code is over-synchronized. This EAGER project explores the foundations of data-centric synchronization with an emphasis on establishing a type theoretic foundation based on the notion of ownership types. Ownership types give programmers a simple notation for describing the shape and extent of heap-based data structures. Thus an ownership type system can be seen as the basic mechanism for specifying the groups of data items that must be manipulated synchronously.
Writing correctly synchronized concurrent programs is challenging. Whenevertwo threads access the same memory location there is the potential for adata race and for inconsistent results. Traditional techniques forconcurrent programming have an operational, control-centric,flavor. Programmers must ensure that any access to a shared data location isprotected by synchronized blocks or other system-specific concurrencycontrol primitives. The challenge is that protecting all accesses to sharedlocations requires non-local reasoning: All control flow paths leading to amemory operation on shared data must be dominated by a synchronizationoperation. A data race may occur if the programmer forgets to synchronizeeven a single path. To make matters worse, even if every access to shared data isprotected, the program may still end up in an inconsistent state due to ahigh-level data race. This can occur when there exists aconsistency relation between multiple memory locations and the programmer'suse of synchonization fails to ensure that this relation is maintained atevery instant. Analysis of real world software defects suggests that these kinds ofraces occur frequently. Avoiding high-level data races requiresthe same kind of non-local reasoning but is further complicated by the factthat multiple locks may have to be acquired in a specific order. Data-centric synchronization is a declarative approach to concurrencycontrol first. Data-centric synchronizationadvocates that instead of focusing on the flow of control, programmersshould identify sets of memory locations that share some consistencyproperty and group those locations in atomic sets that will be updatedatomically. Programmers need not specify where or what kind ofsynchronization operations to insert; instead, each atomic set has an associatedset of units of work, code fragments that preserve the consistency oftheir associated atomic set. Synchronization code is automatically generatedby a compiler which is free to choose where and what type of synchronizationto insert. Such a declarative approach has the benefit that it is possibleto change the concurrency-control mechanism, e.g., going from standard locksto read/write locks or even to transactional memory, without changing theprogram's source code. In a data-centric approach, the non-local reasoningthat permeates traditional approaches to synchronization is replaced by afocus on shared data. High-level data races are naturally avoided as an ascan protect multiple locations and multiple atomic sets can be manipulatedatomically within the same unit of work. This project investigated a variant of the atomic set model, introduced a new mechanism for constructing atomic sets that span multiple objects and for internal objects that providestrong encapsulation for data whose concurrency is managed externally. Thenew approach obviates the need for whole-program analysis with a type systemthat guarantees that any well-typed program is atomic-set serializable,which means that all operations performed on locations that belong to an atomic setare serializable. To empirically evaluate the applicability of our ideas onreal-world code, we implemented the AJ language within the Eclipse developmentenvironment. Experiments suggest that atomic sets are promising way to write concurrent applications.
