Charles Killian, Mace: Systems and Language Support for Building Correct, High-Performance Networked Services

Building distributed systems is particularly difficult because of theasynchronous, heterogeneous, and failure-prone environment where thesesystems must run. This asynchrony makes verifying the correctness ofsystems implementations even more challenging. Tools for buildingdistributed systems must strike a compromise between reducing programmereffort and increasing system efficiency. Mace is a C++ languageextension, compiler, runtime, and toolset, that translates a concise butexpressive distributed system specification into a C++ implementation.Mace exploits a natural decomposition of distributed systems into alayered, event-driven state machine. A key design principle of Mace isto separate each service algorithm from the implementation mechanics(serialization, dispatch, synchronization, etc.), debugging code (loggingand property testing), and its utility services (lower-level servicesproviding a specified interface). Our experience indicates thatprecisely because Mace imposes limits on the design structure ofdistributed systems, it supports the implementation of a wide variety ofhigh-level supporting tools, including model checking, simulation, livedebugging, and visualization. Mace is fully operational, has been indevelopment for four years, and has been used to build a wide variety ofInternet-ready distributed systems. This talk will describe both theMace programming language design and MaceMC, the first model checkerthat can find liveness violations in unmodified systems implementations. About the speaker: Charles KillianPurdue University, Computer ScienceWest Lafayette, INCharles Killian is an Assistant Professor in the Department of Computer Scienceat Purdue University. He completed his Ph.D. in Computer Science from theUniversity of California, San Diego under the supervision of Amin Vahdat.Before transferring to UCSD in August 2004, he completed his Masters inComputer Science from Duke University with Amin Vahdat. His research is at theboundary of systems and programming languages, focusing on ways to usecompilers and language constructs to dually bridge the gap between performanceand programming expression, and to provide high-level tools for debugging,analysis, and understanding. Over the past 4 years he has implemented the Maceprogramming language and toolkit, built numerous distributed systems, anddesigned MaceMC, the first model checker capable of finding liveness violationsin unmodified systems code.