Building distributed systems is particularly difficult because of the asynchronous, heterogeneous, and failure-prone environment 
where these systems must run.  This asynchrony makes verifying the correctness of systems implementations even more challenging.  
Tools for building distributed systems must often strike a compromise between reducing programmer effort and increasing system 
efficiency.  In my research, we introduce a limited amount of structure and limitations to implementations to enable a wide range 
of analysis and development assistance.  Most prominently, we have built the Mace language and runtime, which translates a concise, 
expressive distributed system specification into a C++ implementation, and the Mace model checker, capable of finding liveness 
violations in systems code.  The Mace specification importantly exposes three key pieces of structure: atomic events, explicit state, 
and explicit messaging.
With a few additional structural annotations, we show how we can support intra-node parallel event processing of these atomic events 
while still preserving sequenal event consistency---even using variably available computing resources distributed across a cluster.  
By leveraging these three structural elements, we have further built tools such as a performance tester and an automated malicious 
protocol tester.  Recent research has also explored applications of these key structures in legacy software that has produced a log 
analysis tool that can detect performance problems, and a malicious fault injector that can discover successful performance attacks. 
 Mace has been in development since 2004 and has been used to build a wide variety of Internet-ready distributed systems both by myself 
and by researchers at places such as Cornell University, Microsoft Research (Redmond, Silicon Valley, and Beijing), HP Labs, UCLA, 
EPFL, and UCSD.  This talk will give an overview of my research, presenting the structure we introduce and how we use it to support 
robust and parallel event processing, malicious attack discovery, and problem diagnosis through log analysis.