After many years at Cornell University, I have finally completed my PhD journey! My dissertation, entitled “Programming Safely with Weak (And Strong) Consistency”, is now available via ProQuest (or directly from me).
That document is 364 pages, is there a summary?
Sure! The unifying theme of my dissertation is that writing programs against weak consistency is inherently difficult. My dissertation makes the job of writing safe programs against weak consistency easier, by introducing programming languages in which strong guarantees are defended from weakly-consistent influence, and in which programmers can write consistent-by-construction programs atop underlying weakly-consistent replication.
The first of these languages is MixT, a new language for writing mixed-consistency transactions. These atomic transactions can operate against data at multiple consistency levels simultaneously, and are equipped with an information-flow type system which guarantees weakly-consistent observations cannot influence strongly-consistent actions.
While mixed-consistency transactions can defend strong data from weak observations, they cannot ensure that fully-weak code is itself correct. To address this, we leverage monotonic data types to introduce a core language of datalog-like predicates and triggers. In this language, programmers can write monotonic functions over a set of monotonic shared objects, ultimately resulting in a boolean. These monotonic, boolean-returning functions are stable predicates: once they have become true, they remain true for all time. Actions which are predicated on these stable predicates cannot be invalidated by missed or future updates.
This monotonic language sits at the core of Derecho, a new system for building strongly-consistent distributed systems via replicated state machines. Derecho’s Shared State Table (SST) implements monotonic datatypes atop Remote Direct Memory Access (RDMA), resulting in a high-performance, asynchronous substrate on which to build Derecho’s monotonic language. Using this SST, we have rephrased the Paxos delivery condition monotonically, granting strong consistency despite the underlying asynchronous replication.
Finally Gallifrey exposes the monotonic reasoning properties of Derecho’s core language directly to the user, safely integrating monotonic datatypes into a traditional Java-like programming language. Gallifrey allows any object to be asynchronously replicated via Restrictions to its interface, allowing only those operations which are safe to call concurrently. Datatypes shared under these restrictions can be viewed monotonically, using a language of predicates and triggers similar to that at the core of Derecho. A novel linear region-based type system enforces that shared object restrictions are respected.
A PhD Takes a Village
And mine is no exception. The kindness and generosity of the people who have surrounded me during my PhD never ceases to amaze. Without the community surrounding me, attaining a PhD would be nearly impossible. While my research and academic life has been touched by innumerable hands, I would like to specifically highlight the enormous assistance I have received from Andrew Myers, Ken Birman, Fabian Muehlboeck, Patrick LaFontaine and Danny Yang. It is no exaggeration to say that without their help and guiding presence, I could never have completed this PhD.
To everyone who has helped me on this journey: thank you. Sincerely, thank you.
~Mae
