UC Riverside

Ensuring our increasingly complicated distributed systems are simultaneously reliable and efficient is challenging. Rigorous formal analyses can help make the design and implementation of complex systems both more reliable and efficient, and safeguard organizations from unwanted incidents. As a result, program synthesis has always been an area of interest for computer scientists. Traditionally, program synthesis has only been applied to limited domains and has not been studied at the scale of distributed systems. This dissertation investigates the application of program synthesis in the domain of distributed systems, a domain that can benefit from program synthesis because of its complexities and nuances. We show that the synthesized systems generally provide better performance and significantly reduce the programmer’s efforts. In particular, we apply program synthesis to replication coordination, graph analytics, and tensor computation.

In our first work, Hamsaz, we present a novel sufficient condition for the correctness of the replicated data types called well-coordination, which requires total order between conflicting and causal order between dependent operations. Given the sequential specification and integrity properties of an object, Hamsaz uses solvers for the theory of sets and relations to automatically find the conflicting and dependent pairs of operations. It then reduces coordination minimization to graph optimization problems and automatically synthesizes correct-by-construction message-passing protocols that simultaneously guarantee integrity and convergence. Our results show that well-coordinated replicated data types are significantly more responsive than the strongly consistent baseline.

Compared to traditional data centers built with message-passing network adaptors, modern RDMA networks significantly reduce the response time. In our second work, Hamband, we present coordination synthesis for the RDMA network model. We present RDMA well-coordinated replicated data types, the first hybrid replicated data types for the RDMA network model as well as operational semantics for these data types that capture their required coordination. In particular, calling processes execute and summarize reducible method calls before updating other processes by directly writing summaries into their memories. We formally prove that the replicated objects preserve the convergence and integrity properties. The empirical evaluation shows that Hamband outperforms the throughput of existing message-based and strongly consistent implementations by more than 17x and 2.7x respectively.

Graph analytics elicits insights from large graphs to inform critical decisions for business, safety, and security. However, implementation and especially the optimization of graph analytics are error-prone and time-consuming tasks. The next chapter of this dissertation focuses on the synthesis of graph analytics. GraFS is a high-level declarative specification language for graph analytics and a synthesizer that automatically generates efficient code for various high-performance graph processing frameworks. It features novel semantics-preserving fusion transformations that optimize the specifications and reduce them to three primitives of graph analytics, namely, reduction over paths, mapping over vertices, and reduction over vertices. Reductions over paths are commonly calculated based on push or pull models that iteratively apply kernel functions at the vertices. This project presents parametric conditions for the correctness and termination of the iterative models and uses these conditions as specifications to synthesize the kernel functions. Experimental results show that the synthesized code matches or outperforms handwritten code, and fusion accelerates execution.

Finally, in collaboration with Google Brain, we took the first step towards synthesizing rewriting transformations for tensor computation. Optimizing compilers for machine learning applications rewrite the computational graphs of tensor programs. We present TensorRight, a verified tensor graph rewrite system. It includes a formal tensor language and its denotational semantics to verify tensor optimization rewrite rules. TensorRight uses symbolic execution based on the semantics of tensor operations and novel dimension definitions to generate verification conditions sufficient to prove the equivalence of rewrites on input tensors with unbounded rank and dimension sizes. We show that TensorRight can represent and prove a comprehensive set of the XLA rewrite rules already used in production rewrite engines.