SemantiX: A Compatibility Checker between Applications and Compositions of Distributed Systems

Modern distributed applications compose multiple services with different consistency guarantees. Mismatches between application requirements and chosen system semantics can introduce subtle bugs, but verifying compatibility across complex applications is both challenging and time-consuming. In particular, existing testing approaches or rigorous formal verification lacks flexibility and cannot promptly provide correctness guarantees on multi-semantic compositions. We present SemantiX, a framework for checking semantic compatibility between applications and compositions of distributed systems with heterogeneous consistency models. SemantiX embeds formally defined distributed system modules of consistency semantics which include the first formal definition of visibility constraints. SemantiX introduces the AppGraph approach for systematically modeling complex applications. Applications modeled using AppGraphs can be checked for their compatibility against a combination of distributed system modules that the user is considering. Alternatively, SemantiX can search for combinations of modules compatible with the application. We present three case studies on a movie streaming service, an e-commerce platform, and a cross-service causal distributed storage service. We demonstrate that SemantiX can capture complex service compositions with minimal encoding effort and quickly check compositional compatibility with underlying systems or find the compatible system configurations. SemantiX enables developers to efficiently verify distributed application designs and explore alternative consistency configurations, supporting more agile development.