— Замечаем, что свободная память куда-то внезапно съёбывается. killall -STOP firefox-bin — Уходим с воркспейса с браузером. Память возвращается. Firefox всё ещё в T state. — Возвращаемся в предыдущий воркспейс. Память опять куда-то девается. — Дампим smaps_rollup всех процессов, сравниваем. Разница копеечная. Неважно, Rss, Pss, firefox-bin, Xorg, i3 — да вообще всех метрик и по всем процессам. — Дампим meminfo. Разница только в гигабайтищах, на которые похудели MemFree и MemAvailable. slabinfo и df -h /dev/shm на таком фоне даже нет смысла сравнивать (но всё равно сравниваем и не видим ничего интересного). Что, бля, происходит нахуй?!

OOM всё чаще стал приходить в момент, когда памяти, казалось бы, ещё дофига. Кажется, я начинаю догадываться, почему: MemFree: 1940452 kB MemAvailable: 3082928 kB Buffers: 30792 kB Cached: 7696368 kB Dirty: 256 kB Writeback: 0 kB С каких пор Available стал меньше Free+Buffers+Cached-Dirty-Writeback? Кто и зачем спиздил у меня эти 6,5 гигов памяти?

После `swapoff *` количество занятой памяти уменьшилось на (29,6+29,4)—44 = 15 ГБ. WTF? Для накладных расходов на поиск страниц соотношение 1:2 какое-то дохуя жирное. В SwapCached столько не было; точно не помню, но где-то меньше пяти гигов.

Где-нибудь вообще можно почитать про использование TLA⁺ без ебанутой гуйни, которая ломается даже от простого GTK_IM_MODULE=xim?

Что в 2020 стоит читать нублолам про формальную верификацию? Стоит ли бежать за толпой и дрочить на TLA⁺/PlusCal? Вымирают ли агды да идрисы с петухами? Где я мог наткнуться на ATS и какого чёрта его название засело у меня в голове? Почему Microsoft Research пилит аж два прувера? Ну и всё такое.