Graybox stabilization

Research in system stabilization has traditionally relied on the availability of a complete system implementation. As such, it would appear that the scalability and reusability of stabilization is limited in practice. Towards redressing this perception, the authors show for the first time that system stabilization may be designed knowing only the system specification but not the system implementation. We refer to stabilization designed thus as being "graybox" and identify "local everywhere-eventually specifications" as being amenable to design of graybox stabilization. We illustrate the design of graybox stabilization using timestamp-based distributed mutual exclusion as our example.