Skip to content
Tim Jungnickel edited this page May 30, 2017 · 8 revisions

Disclamer: This page contains our thoughts about the vision of the pluto project. We are excited to discuss promising directions for pluto. Feel free to leave a comment or an issue to get in touch. Also note, that this reflects the initial motivation. Elements might change or get dropped completely as the semester progresses.

Contributions

With pluto, we aim to contribute novel approaches in the fields of Cloud Engineering, Fault Tolerance, Verification, and ultimately Distributed Systems research. The pluto project is a research project in the first place. However, instead of only developing a new concept, we are committed to bring our ideas to life by providing well-engineered software based on strong concepts and literally proven mechanisms.

Therefore, we plan to contribute the following:

Verification

  • Propose an IMAP CRDT - we model IMAP commands as operations on a CRDT. The proposed datatype enables a more flexible way to handle application state in an IMAP system.
  • Verify its convergence - we give certainty that the application state converges and that our promises hold. We provide an adequate system model and propose the necessary definitions and lemmas to express pluto's behavior. All propositions are formally verified and maybe even machine-checked.
  • Prove the OR-Set (op-based) - since our IMAP CRDT is based on multiple OR-Sets, we start by verifying the necessary properties of the op-based OR-Set, i.e. operations commute. We plan to implement the proof in Isabelle/HOL or another proof system.

Engineering

  • Propose a novel solution for planet-scale replication of an IMAP service - our system design is resilient to high transmission delays between application and storage layer, enabling short response times to users due to geographically close processing.
  • Introduce a novel approach for IMAP services to deal with partitions and failures - this relates to the CAP-gap, which we plan to bridge with a new, CRDT-powered approach. We plan to discuss what other approaches feature application-level fault tolerance and whether there has already been a solution utilizing CRDTs.
  • Present a messaging middleware that fulfills the requirements for convergence - because CmRDTs expect the messaging middleware to provide certaing delivery guarantees, we reason about how our implementation fulfills these requirements.
  • Discuss how an IMAP service with a stateful application layer can elastically grow and shrink - in other words, how we can scale our stateful application at runtime. We plan to discuss the current way to handle this issue and present a comparison between existing(?) models and our proposal.

Evaluation

  • Introduce a benchmark for IMAP services - because there is no common IMAP benchmark or dataset that enables reasoning about the performance of write requests and their impact on consistency from a user's perspective, we propose our own.
  • Explore the reliability and performance of planet-scale IMAP services on public clouds - we evaluate pluto against state-of-the-art Dovecot setups and show how all systems perform on planetary scale.
  • Evaluate the boundaries of pluto's and Dovecot's synchronization mechanisms - e.g. what is the average time for an operation to become visible on all nodes. Is there a threat to our system/queuing model?

Deployment

  • Propose a Kubernetes based Deployment for planet-scale Dovecot - we compare pluto against Dovecot. Hence, we provide different Dovecot setups for a planet-scale IMAP service.

Implementation

  • Propose an adoption of Prometheus to evaluate the behavior of IMAP systems - for now, Prometheus is mainly used to monitor health and status of software services. We plan to use Prometheus not only to monitor, but also to evaluate our software. We demonstrate how the measured metrics can be extracted from Prometheus and processed with further tools.

Things that are out of scope (for now)

  • Propose a verification environment (in Isabelle?) for CmRDTs. This would include a complete formalization of the CRDT paper. However, we think this would be a valuable contribution.
Clone this wiki locally