About

Parallelism is omnipresent in today's computational systems, from cloud infrastructures, to personal computers and handheld devices. However, concurrent code is difficult to write and its correctness complex to assess, being the source of many execution errors. This difficulty is exacerbated when tackling replicated systems, such as the ones supporting social networks, online stores and mobile collaborative systems. In these contexts, data consistency is bound to the order on which operations are executed at each replica, resulting in a tension between correctness and performance. Current research is tackling this tension by allowing different operations to execute under different consistency levels.

Classically, expressing concurrency constraints requires conveying information about (blocks of) instructions. The approach is prone to the dispersal of concurrency related bugs, hampering reasoning about correctness as the code scales: a single missing lock operation or annotation of a data consistency requirement may silently adulterate an application's behaviour and/or expose bugs exploitable by hackers. Recent advances in replicated contexts focus on providing specifications that enable the automatic inference of the consistency level to assign to each operation, but there are no correctness guarantees. It is up to the programmer to keep track of all accesses to data items, and write the specification accordingly. A single missed access may render the specification incorrect.

Our insight is to shift the specification from code to data declaration, and, with that, take control over specification correctness. Data-centric concurrency control promotes local rather than distributed reasoning by centralizing concurrency management on data declaration. In 2016 we proposed the RC3 data-centric concurrency control model for shared memory programming: the programmer just has to annotate the data that must be atomically accessed, and a typing system will guarantee progress and atomicity.

The main goals of the DeDuCe project are to:

- Extend RC3 to cope with replicated systems, providing the means to express consistency relationships between data, and from that deduce to which consistency level must a given operation comply to, while formally guaranteeing the correctness of the specification.

- Prototype RC3 with special focus on mobile applications. We want to build on previous work on mobile edge computing to present a solution for the development of future collaborative mobile applications that leverage the computing and storage facilities that will arrive with 5G cellular networking.