Data-Centric Concurrency Control (DCCC) shifts the reasoning about concurrency restrictions from control structures to data declaration. It is a high-level declarative approach that abstracts away from the actual concurrency control mechanism(s) in use. Despite its advantages, the practical use of DCCC is hindered by the fact that it may require many annotations and/or multiple implementations of the same method to cope with differently qualified parameters. Moreover, the existing DCCC solutions do not address the use of interfaces, precluding their use in most object-oriented programs. To overcome these limitations, in this paper we present AtomiS, a new DCCC model based on a rigorously defined type-sound programming language. Programming with AtomiS requires only (atomic)-qualifying types of parameters and return values in interface definitions, and of fields in class definitions. From this atomicity specification, a static analysis infers the atomicity constraints that are local to each method, considering valid only the method variants that are consistent with the specification, and performs code generation for all valid variants of each method. The generated code is then the target for automatic injection of concurrency control primitives, by means of the desired automatic technique and associated atomicity and deadlock-freedom guarantees, which can be plugged-into the model's pipeline. We present the foundations for the AtomiS analysis and synthesis, with formal guarantees that the generated program is well-typed and that it corresponds behaviourally to the original one. The proofs are mechanised in Coq. We also provide a Java implementation that showcases the applicability of AtomiS in real-life programs.

翻译：数据中心并发控制（DCCC）将并发限制的推理从控制结构转向数据声明。这是一种高级声明式方法，抽象了实际使用的并发控制机制。尽管有其优势，DCCC的实际应用受到阻碍，因为它可能需要大量注解和/或同一方法的多个实现来处理不同限定类型的参数。此外，现有的DCCC解决方案未解决接口的使用问题，这使其无法应用于大多数面向对象程序。为克服这些限制，本文提出了AtomiS——一种基于严格定义的类型安全编程语言的新DCCC模型。使用AtomiS编程仅需在接口定义中为参数和返回值、以及在类定义中为字段指定原子性限定类型。基于此原子性规范，静态分析推断出每个方法局部的原子性约束，仅考虑与规范一致的方法变体，并为每个方法的所有有效变体生成代码。生成的代码随后通过所需的自动技术及相关的原子性和死锁自由保证，成为自动注入并发控制原语的目标，这些技术可接入模型的流水线。我们展示了AtomiS分析与综合的基础理论，并提供了形式化保证：生成的程序类型正确，且在行为上与原始程序对应。相关证明已在Coq中机械化实现。我们还提供了Java实现，展示了AtomiS在实际程序中的适用性。