Pencarian saya akan solusi berbasis prinsip untuk kegagalan metastabil telah membawa saya kembali ke stabilisasi-diri. Sebuah makalah terbaru menghubungkan masalah ini dengan komposisi sistem stabilisasi-diri, tetapi pencarian literatur tidak menghasilkan apa pun yang berguna. Stabilisasi berlapis sudah ada pada awal tahun 2000-an, dan tampaknya tidak ada yang fundamental ditambahkan sejak itu.

Saya menyerang masalah ini menggunakan contoh konkret: model TLA+ rely-guarantee dari badai percobaan ulang sebagai dua komponen dengan kontrak. Model itu mereproduksi kegagalan metastabil karena komposisi bekerja dari keadaan baik tetapi gagal ketika guncangan besar menghilangkan kasus dasar. Mencari komposisi rely-guarantee dari setiap keadaan menemukan makalah teori kontrol tahun 2017 oleh Kim, Arcak, dan Seshia, "A Small Gain Theorem for Parametric Assume-Guarantee Contracts". Makalah ini kira-kira melakukan apa yang saya inginkan: melepaskan penalaran sirkular antara dua komponen tanpa pelapisan atau pemblokiran. Tetapi ia memiliki keterbatasan serius. Komponen adalah relasi input-output pada sinyal, dan kontrak menghubungkan batas input ke batas output. Pandangan tanpa memori ini tidak dapat mengekspresikan tumpukan yang terakumulasi dari putaran sebelumnya, sehingga mengecualikan antrian. Ia juga tidak memiliki koneksi ke stabilisasi.

Namun, beberapa bagian layak dicuri menuju teori komposisional stabilisasi-diri dan metastabilitas. Di bawah ini saya mencoba menguraikannya... agak tidak berhasil.

Dalam model asli kami, jaminan si pengulang bersifat kondisional: "jika antrian di bawah 6, saya tidak mengirim percobaan ulang". Ide besar dari makalah asumsi-jaminan parametrik adalah menulis keluarga kontrak yang mencakup di mana-mana. Konstanta: S=3 kapasitas server, A_max=2 kedatangan baru, T=2 timeout, ambang latensi S·T=6. Ini memberikan λ(L) = ⌊(L-6)/2⌋. Kontrak lama adalah baris teratas: λ(6)=0. Setiap baris mendapat janji, jadi kami mendapatkan bundel kontrak biasa, satu per tingkat keburukan p: φ_a = ∨_p ψ_a(p); φ_g = ∧_p (ψ_a(p) ⇒ ψ_g(λ(p))). Sisi asumsi adalah disjungsi karena tingkat adalah alternatif. Sisi jaminan adalah konjungsi; kewajiban bersifat kumulatif. Baris yang kondisinya salah tidak memakan biaya; tingkat bersarang berarti yang paling ketat menang.

Entitas Kunci: Orang: Kim, Arcak, Seshia