Мой поиск принципиального решения для метастабильных отказов вернул меня к самоподдержке. Недавняя статья связала проблему с композицией самоподдерживающихся систем, но поиск в литературе не дал ничего полезного. Слоистая стабилизация уже существовала к началу 2000-х, и с тех пор, похоже, ничего фундаментального не добавлено.

Я атаковал проблему, используя конкретный пример: модель TLA+ зависимости-гарантии для шторма повторных попыток как двух компонентов с контрактами. Эта модель воспроизводит метастабильный отказ, потому что композиция работала из хороших состояний, но терпела неудачу, когда большой шок удалял базовый случай. Поиск композиции зависимости-гарантии из каждого состояния привел к статье по теории управления 2017 года Kim, Arcak и Seshia, «A Small Gain Theorem for Parametric Assume-Guarantee Contracts». Эта статья делает примерно то, что я хочу: разряжает циклическое рассуждение между двумя компонентами без слоев или блокировки. Но у нее есть серьезные ограничения. Компонент — это отношение вход-выход на сигналах, а контракты связывают границу входа с границей выхода. Этот безпамятный взгляд не может выразить накопленный бэклог от предыдущих раундов, исключая очереди. Он также не связан со стабилизацией.

Тем не менее, некоторые части стоит украсть для композиционной теории самоподдержки и метастабильности. Ниже я пытаюсь это разработать... несколько безуспешно.

В нашей исходной модели гарантия повторяющего была условной: «если очередь ниже 6, я не отправляю повторных попыток». Большая идея параметрической статьи предположение-гарантия — написать семейство контрактов, покрывающих везде. Константы: S=3 емкость сервера, A_max=2 новые поступления, T=2 тайм-аут, порог задержки S·T=6. Это дает λ(L) = ⌊(L-6)/2⌋. Старый контракт — верхняя строка: λ(6)=0. Каждая строка получает обещание, поэтому мы получаем набор обычных контрактов, по одному на уровень плохости p: φ_a = ∨_p ψ_a(p); φ_g = ∧_p (ψ_a(p) ⇒ ψ_g(λ(p))). Сторона предположения — это дизъюнкция, потому что уровни — альтернативы. Сторона гарантии — конъюнкция; обязательства кумулятивны. Строки, условие которых ложно, ничего не стоят; вложенные уровни означают, что побеждает самый строгий.

Ключевые сущности: Люди: Kim, Arcak, Seshia