Distributed Systems Synthesis and Verification

Marc Rosen (Spring 2017)

Download the Prototype
View the Presentation
Download the Presentation in LaTeX Format

What is Genie?

Genie is a language for expressing the semantics of a distributed system, and a tool which will verify the soundness of semantics, and then generate code to run the described system.

Users can specify invariants on the state of the system, which must hold on any replica, after any successful sequence of applications of operations (in causal order). Operations can be given preconditions to ensure that invariants hold.

What do distributed system semantics look like when expressed in Genie?

The below is all that's needed to implement the final project for the Fall 2016 Distributed Systems course (minus the pretty text client; Genie automatically generates a python API).

0001 system Mail;
0003 class Message {
0004 String sender;
0005 String recipient;
0006 String subject;
0007 String contents;
0009 Bool unread = true;
0010 Bool deleted = false;
0012 [Exposed]
0013 static List<Message> listMessages(String user) {
0014 return
0015 from m in Message
0016 where m.recipient == user
0017 where !m.deleted
0018 orderby ascending
0019 select m;
0020 }
0022 [Exposed]
0023 static Message composeMessage(
0024 String sender, String recipient,
0025 String subject, String contents
0026 ) {
0027 return new Message(
0028 sender: sender,
0029 recipient: recipient,
0030 subject: subject,
0031 contents: contents,
0032 );
0033 }
0035 [Exposed]
0036 Message markAsRead() {
0037 this.unread = false;
0038 return this;
0039 }
0041 [Exposed]
0042 Unit delete() {
0043 this.deleted = true;
0044 }
0045 }

How do I use the prototype?

Click the "Download the Prototype" button above, and read the README.

How does it work?

Genie is written in Scala 2.12. Twirl is used for text templating to generate the C++ source code. ANTLR is used for parsing and lexing. Z3 is the SMT solver which is used to check program invariants. We access Z3 through the CLI through a wrapper called scala-smtlib. The generated C++ code uses Boost and Spread.

Works Cited

  1. Valter Balegas, Diogo Serra, Sergio Duarte, Carla Ferreira, Marc Shapiro, Rodrigo Rodrigues, and Nuno Preguiça. Extending eventually consistent cloud databases for enforcing numeric invariants. In Reliable Distributed Systems (SRDS), 2015 IEEE 34th Symposium on, pages 31--36. IEEE, 2015.
  2. Valter Balegas, Sérgio Duarte, Carla Ferreira, Rodrigo Rodrigues, Nuno Preguiça, Mahsa Najafzadeh, and Marc Shapiro. Putting consistency back into eventual consistency. In Proceedings of the Tenth European Conference on Computer Systems, page 6. ACM, 2015.
  3. Régis Blanc, Viktor Kuncak, Etienne Kneuss, and Philippe Suter. An overview of the leon verification system: Verification by translation to recursive functions. In Proceedings of the 4th Workshop on Scala, page 1. ACM, 2013.
  4. Eventml. Accessed: 2017-05-01.
  5. Getting started with saml. Accessed: 2017-05-01.
  6. Alexey Gotsman, Hongseok Yang, Carla Ferreira, Mahsa Najafzadeh, and Marc Shapiro. 'cause i'm strong enough: Reasoning about consistency choices in distributed systems. ACM SIGPLAN Notices, 51(1):371--384, 2016.
  7. Anders Hejlsberg, Mads Torgersen, Scott Wiltamuth, and Peter Golde. C# Programming Language. Addison-Wesley Professional, 2010.
  8. How is the consistency level configured? Accessed: 2017-05-01.
  9. Marc Shapiro—Nuno Preguiça. Designing a commutative replicated data type. arXiv preprint arXiv:0710.1784, 2007.
  10. Replication and conflict model. Accessed: 2017-05-01.
  11. Marc Shapiro, Carlos Baquero, and Marek Zawirski. A comprehensive study of convergent and commutative replicated data types. 2011.
  12. The tla home page. Accessed: 2017-05-01.
  13. Welcome! | the coq proof assistant. Accessed: 2017-05-01.
  14. Z3 smt solver. Accessed: 2017-05-01.