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; | |
| 0002 | ||
| 0003 | class Message { | |
| 0004 | String sender; | |
| 0005 | String recipient; | |
| 0006 | String subject; | |
| 0007 | String contents; | |
| 0008 | ||
| 0009 | Bool unread = true; | |
| 0010 | Bool deleted = false; | |
| 0011 | ||
| 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 m.id ascending | |
| 0019 | select m; | |
| 0020 | } | |
| 0021 | ||
| 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 | } | |
| 0034 | ||
| 0035 | [Exposed] | |
| 0036 | Message markAsRead() { | |
| 0037 | this.unread = false; | |
| 0038 | return this; | |
| 0039 | } | |
| 0040 | ||
| 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
- 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.
- 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.
- 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.
- Eventml. http://www.nuprl.org/software/. Accessed: 2017-05-01.
- Getting started with saml. http://rise4fun.com/SAML/tutorial/tutorial. Accessed: 2017-05-01.
- 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.
- Anders Hejlsberg, Mads Torgersen, Scott Wiltamuth, and Peter Golde. C# Programming Language. Addison-Wesley Professional, 2010.
- How is the consistency level configured? http://docs.datastax.com/en/dse/5.1/dse-arch/datastax_enterprise/dbInternals/dbIntConfigConsistency.html. Accessed: 2017-05-01.
- Marc Shapiro—Nuno Preguiça. Designing a commutative replicated data type. arXiv preprint arXiv:0710.1784, 2007.
- Replication and conflict model. http://docs.couchdb.org/en/2.0.0/replication/conflicts.html. Accessed: 2017-05-01.
- Marc Shapiro, Carlos Baquero, and Marek Zawirski. A comprehensive study of convergent and commutative replicated data types. 2011.
- The tla home page. http://lamport.azurewebsites.net/tla/tla.html. Accessed: 2017-05-01.
- Welcome! | the coq proof assistant. https://coq.inria.fr/. Accessed: 2017-05-01.
- Z3 smt solver. https://github.com/Z3Prover/z3. Accessed: 2017-05-01.