[TYPES/announce] Post-doc: applying verification techniques to consistency in planet-scale storage

[Pierre-Evariste Dagand]

[forwarding on behalf of Marc Shapiro <marc.shapiro at acm.org>]

In cloud storage systems, which geo-replicate data for performance and
fault tolerance, the CAP theorem points out an inherent trade-off
between consistency and availability: strong consistency provides good
guarantees but is slow and blocks when the network is down; weak
consistency is always available but can expose concurrency anomalies.

The research of the Regal group aims to bridge the gap, thanks to a
“Just-Right Consistency” hybrid approach, aiming to tailor consistency
to the specific requirements of the applications, in order to provide
the highest possible performance and availability at the lowest cost.
Getting this right is difficult: too much synchronisation and the
system crawls to a halt; not enough and data is corrupted.

Therefore, we leverage the CISE static analysis [POPL 2016] to ensure
that the application remains correct, ensuring that (only) the
specific operations that are essential to correctness are
synchronised.

This post-doc aims to consolidate our preliminary results and to
advance the theory and practice of just-right consistency.  Ultimately
our results and tools should be practically available to application
developers. The post-docs shall aim to increase the coverage of the
CISE logic and analysis and to decompose consistency into its
primitive components.  The result of the post-docs will be actual
tools that can be used by application programmers.  This research will
be applied to increasingly demanding, practical large-scale
applications; in particular we shall design, prove correct, implement
and evaluate a petabyte-scale geo-replicated file system and the
applications using it.

Two post-doc positions are potentially available, supported by a joint
research grant with industry (ANR RainbowFS), and by a grant
supporting the productisation of our JRC tools. The research has both
a fundamental and an applied aspect and aims for practical results.
Candidates to these positions should hold a PhD in Computer
Science/Informatics or a related field. They should have an excellent
academic record and experience in distributed systems, distributed
databases, and/or compilation and verification tools. In addition to
research experience, he or she should be a good developer and
experimentor at large scale, and have teamwork and communication
skills. Industrial experience and good knowledge of Erlang and/or
node.js is a plus.

For more information and application procedure, see here:
https://team.inria.fr/regal/job-offers/two-post-doc-positions-practical-just-right-consistency-and-planet-scale-storage/

-------------------------------------------------------------------------------
Marc Shapiro, INRIA & LIP6, BC 169                  mailto:marc.shapiro at acm.org
UPMC, 26-00/211, 4 place Jussieu                   http://lip6.fr/Marc.Shapiro/
75252 Paris Cedex 05, France                               tél: +33 1 4427 7093
-------------------------------------------------------------------------------