Return to Job offers

Masters’ internship: Correct datatypes for geo-replicated distributed applications

Description of the research

Developing a distributed application is far from trivial, because of the trade-offs between consistency and availability. All developers wish that their application is as available as possible. Still, they need to ensure that the application invariants are respected. The CISE [1] logic can check whether an application specification upholds its expected invariant. This can be used to design applications with just the right amount of consistency.

Marcelino et al. [2] have developed the CEC tool, based on the CISE logic. The user specifies the application in the Boogie language [3], extended with some tool-specific annotations. The tool analyses the specification and provides the user information on any consistency issues. An experience report of the tool usage [4] shows that writing specifications is difficult and error-prone.

The goal of this internship is to enable users to write specifications more easily.  The output will be to develop a library of common datatypes,  and write reusable templates for common cases.  The datatypes can be classified into normal data types such as set, list, graph, tree, etc. and replicated datatypes such as G-set, PN-set etc. The normal data type specifications will be verified using plain Boogie, and the replicated ones using the CEC tool. As many object types are commonly used in most specifications and it is repetitive and error-prone to define the properties of it multiple times. We will develop templates that can be reused later in writing full specifications.

How to apply

The intern must:

  • Be enrolled in a Masters’ in Computer Science / Informatics or a related field.
  • Have an excellent academic record.
  • Be strongly interested in, and have good knowledge of, distributed systems and/or formal verification methods.
  • Be motivated by experimental research.

The internship is funded, and will take place in the Delys group, at Laboratoire d’Informatique de Paris-6 (LIP6), in Paris. It will be advised by Sreeja Nair and Dr. Marc Shapiro. A successful intern will be invited to apply for a PhD.

To apply, contact Sreeja Nair <Sreeja.Nair@lip6.fr>, with the following information:

  • A resume or Curriculum Vitæ.
  • A list of courses and grades of the last two years of study (an informal transcript is OK).
  • Names and contact details of two references (people who can recommend you), whom we will contact directly.

Bibliography

[1] Alexey Gotsman, Hongseok Yang, Carla Ferreira, Mahsa Najafzadeh, and Marc Shapiro. 2016. ‘Cause I’m strong enough: Reasoning about consistency choices in distributed systems. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’16). ACM, New York, NY, USA, 371-384.  http://dx.doi.org/10.1145/2837614.2837625
[2] Gonçalo Marcelino, Valter Balegas, and Carla Ferreira. 2017. Bringing Hybrid Consistency Closer to Programmers. In Proceedings of the 3rd International Workshop on Principles and Practice of Consistency for Distributed Data (PaPoC ’17), Annette Bieniusa and Alexey Gotsman (Eds.). ACM, New York, NY, USA, Article 6, 4 pages.  https://doi.org/10.1145/3064889.3064896
[3] Boogie, https://github.com/boogie-org/boogie
[4] Sreeja S Nair, Evaluation of the CEC (Correct Eventual Consistency) Tool. Inria Research Report, RR-9111, October 2017. https://hal.inria.fr/hal-01628719