For the 150th reading group paper, we read “Model Checking Guided Testing for Distributed Systems” EuroSys’23 paper by Dong Wang, Wensheng Dou, Yu Gao, Chenao Wu, Jun Wei, and Tao Huang. We had a nice presentation of the paper, and I will be extremely short in my summary.

The authors present and evaluate Mocket, a framework for testing distributed systems that tries to link together the formal specs of the systems and their implementations. This is a common problem with formal specifications, as these specs tend to drift away from the implementations over time.

Mocket uses the state exploration traces provided by the checker (in this case, they use TLA+ for specification and TLC for the checker) to drive the tests running the real implementation. The high-level idea is that if the implementation is correct, then it refines the spec, so the sequence of state transitions pulled from some TLC execution traces should also happen in the “real world.” Mocket relies on code annotations to map variables and functions to TLA variables and actions to allow it to map the model to the code and check the implementation. Upon testing the system reports inconsistencies in the state between the implementation and the model, as these inconsistencies may indicate a bug as the state of the model and code diverged.

Reading Group

Our reading group takes place over Zoom every Thursday at 1:00 pm EST. We have a slack group where we post papers, hold offline discussions, and most importantly manage Zoom invites to paper presentations. Please join the slack group to get involved!