Migrating from monoliths to microservices: enforcing correct coordination

A current trend in service-oriented architectures is to break coarse-grained monolith systems, encapsulating all function capabilities, down into small-scale and fine-grained microservices, which work in concert. The microservices resulting from the decomposition can be independently deployed on physically distributed machines, and an extremely challenging and complex task is to ensure that the behavior emerging from their distributed interaction is equivalent to the original monolith system. Specifically, the price to be paid for the gained distribution is that the emerging microservices interaction may exhibit not only deadlocking behavior, but also extra behavior, which is undesired with respect to the original monolith. In this paper, we propose a method for automatically (i) detecting both deadlocking interactions and extra behavior, and (ii) synthesizing distributed coordinators that when interposed among the resulting microservices avoid deadlocks and undesired interactions.