2. Research Projects

This page outlines the goals of the project part of the module, discusses their assessment and lists some high-level ideas.

This part of the is open-ended: you are encouraged to explore your own ideas in the space of specification and verification of distributed systems.

The most important part for the project is to be interesting, related to distributed systems and verifications, and to be developed to a certain level of maturity. For instance, if you are specifying a real-world system in TLA+, you may wish to break it to multiple components and work on them separately to have some of them fully specified and model-checked at the end, while the others being sketched enough to be convincing.

2.1. Types of Projects

Tentatively, two kinds of projects are envisioned:

  • Specification/verification case studies: You are expected pick an existing protocol and specify/verify it in one of the available tools: TLA+/PlusCal, Ivy, Dafny, Coq, etc. When you pick your verification target, make sure that there is no available formalisations on the internet. In your report you will have to focus on the simplifications/assumptions you’ve made to encode your model in a formal framework. These kinds of projects are expected to be completed individually.
  • Infrastructure projects: These are more ambitious projects, in which you utilise existing formalisations tools to facilitate verification of some common scenarios in some systems (it’s up to you to define the scope of the project). These projects will typically require some knowledge on building translators/compilers, very careful planning of the workload and a good choice of motivating examples. These projects can be done in teams of two.

2.2. Grading

The research project amounts to 25% of your grade. This score is combined from:

  • Initial project proposal: 5% (why the problem is interesting, why feasible)
  • Code quality: 5% (well-documented, corresponds to the text in the report)
  • Written report: 10% (evaluated based on structure, clarity)
  • Presentation: 5% (you should be able to explain your design choices)

Please, email your project proposals (2-3 page documents) to me by Monday, March 29. You will have to upload your implementation and report to LumiNUS (deadline in late April TBA). Presentations of the projects will take place some time on the exam week of April 19, 2021.

2.3. On Incomplete Deliverables

If your project turned out to be a larger undertaking than you were planning, it is acceptable to have it not fully completed. That said, your final artefact should still present some amount of non-trivial effort, possibly packaged with instructions on how one could build on it; your report should clearly list the obstacles that prevented you from finishing your initially planned agenda.

2.4. Some Ideas for Projects

One-person specification/checking projects

At the time of this writing the following published systems did not have a machine-checked formalisation:

  • Distributed transactions:
    • Spanner: Google’s Globally Distributed Database
    • Building Consistent Transactions with Inconsistent Replication
  • Chain replication:
    • Chain Replication for Supporting High Throughput and Availability
  • Distributed lock service:
    • The Chubby Lock Service for Loosely-Coupled Distributed Systems
  • Systems with weaker consistency guarantees:
    • Don’t settle for Eventual: Scalable Causal Consistency for Wide-Area Storage with COPS
    • Making Geo-Replicated Systems Fast as Possible, Consistent when Necessary
    • Dynamo: Amazon’s Highly Available Key-Value Store
  • Blockchains and BFT:
    • A Secure Sharding Protocol For Open Blockchains
    • Byzantine Ordered Consensus without Byzantine Oligarchy

Two-Person Infrastructure Projects

The following are very high-level ideas.

  • Optimising TLA+ implementations for faster checking by inferring constraints and symmetry conditions
  • Checking that real-world implementations obey their TLA+ models (via run-time monitoring and testing)
  • Support for refinement checking in Scilla smart contracts (based on Scilla-TLA project, available on demand)