Metastability as a failed conditional discharge of rely-guarantee composition

Last week I wrote about modular verification of systems through open TLA+ specs and rely-guarantee discharge. In this post, I apply the same approach to study the metastability mechanics of a retry storm. Through this modeling I show that when the system is metastable, it is due to some trigger/shock that displaced the system outside the rely-guarantee discharge conditions of its components. The modelI use the retrier-server example from the "Characterizing Metastable Faults and Failures" paper and model it in TLA+ as a composition of a retrier and a server component.The shared interface between the two components consist of the following variables:qf: fresh work queued at the serverqd: duplicate (retry) work queued at the serverdone: the count of fresh requests the server completed this round, which the retrier reads and clearsturn: a flag forcing alternation between the retrier and server stepsThe retrier has one private variable, p, which denotes the pending fresh requests: the…