Everything Everywhere All At Once: Efficient Cross-Service Program Analysis with OverSeer

Microservice applications often encounter failures due to cross-service assumptions that are challenging to reason about, such as timing, data formats, and semantic changes. These problems can arise as individual teams update and roll back their services independently, causing implicit assumptions about service interaction to become invalid. To prevent such issues, teams must ensure the validity of service interactions across all services and all combinations of versions that may coexist in production, which is both difficult and error-prone to do manually. In this paper, we argue for richer specifications and automated analysis of properties in cross-service programs. We present OverSeer, a framework for cross-service program analysis that can check a wide range of useful program properties efficiently across possible combinations of service versions. OverSeer avoids the combinatorial explosion caused by versioning of services by leveraging the lattice structure of many program properties, including properties about types, timing, and effects. We evaluate OverSeer’s scalability on synthetic benchmarks and show it can analyze large systems with 4,000 services and 16,000 endpoints in less than a second.