... Research | Personal | Nerdy Fun
Research » Projects
Since my arrival at Caltech, I have contributed to a number of research projects in the area of software reliability. Below, I include brief descriptions of each of the projects to which I have made a significant contribution; more information on these projects (when available) can be accessed via the corresponding entry on the link panel to the left. Also be sure to check out my Publications page.
MojaveFS is a mutable distributed filesystem designed for massively distributed decentralized deployment, high availability/performance, and fault tolerance. While there exist other filesystems that aspire to the same set of lofty goals, one feature that sets MojaveFS apart from other competitors is that MojaveFS also preserves traditional (sequentially consistent) file access semantics transparently to its users.
One product of the work on MojaveFS has been the development of a general-purpose group communication protocol, called MojaveComm. From a high-level perspective, MojaveComm introduces a new "group" abstraction on top of traditional network transport protocols, allowing MojaveComm to provide certain message ordering guarantees with respect to group membership. In particular, the aim of this project is to provide a new high-level communication protocol that helps facilitate (and accelerate) the development of distributed applications by providing communication primitives with semantics more amenable to such an environment.
The primary goal of the FixD project is to develop a tool that addresses some of the inherent deficiencies in the application of model checking techniques to large (and/or distributed) systems. In particular, FixD is concerned with solving the feasibility problem (wrt. processing time and memory usage) of such exhaustive state exploration at development stages prior to application deployment. Thus, rather than trying to exhaustively verifying the correctness of all possible application behavior ahead of time, FixD takes the novel approach of pushing this verification step to run-time and using the actual execution path of a running instance of the application to direct the model checker (and to dynamically avoid runtime errors as they are discovered).
The inception of modelD initially started as a class project whereby I wanted to develop a new model checker that employed a specification language highly amenable to the specification of distributed systems. However, as modelD was implemented cleanly in two separate components (a front-end that provides the compiler for the specification language, and a back-end that delivers the low-level model checking engine), modelD has also become the basis for the model checking component of FixD.