Однажды автор решил помочь Грэму Кристенсену в сборе средств на проект Great Slate – и подарил ему два технических поста на выбор самого Кристенсена. Затем Грэм купил у него еще один текст и попросил написать.

Что-нибудь, касающееся Nix или NixOS.

Далее – от автора.

Для меня это был тот еще вызов, ведь на тот момент я еще даже не знал, что такое Nix. Я им никогда не пользовался, до сих пор не пользуюсь и не собираюсь переходить в обозримом будущем – так как единственный компьютер, которым я сейчас пользуюсь, работает под Windows.(1) К счастью, формулировка «что-нибудь» дает некоторое поле для маневра, и я быстро сориентировался, о чем могу написать. Nix позиционируется как «полнофункциональный» менеджер пакетов. В самом деле, что же это означает? Мужайтесь, ниже речь пойдет о формализации. Я опишу некоторое множество «теоретически возможных» менеджеров пакетов, и мы обсудим, какие достоинства (и, возможно, недостатки) есть у «полнофункционального» менеджера пакетов.

Сразу оговорюсь, что в качестве языков для спецификаций я рассматривал TLA+, который блестяще описывает временные системы, а также Alloy, который особо хорош при работе с реляционными данными. Выбранная мной тема захватывает обе эти предметные области, поэтому ни один из этих вариантов я не считал однозначно приоритетным. В конце концов, я остановился на Alloy, так как:

• Там более качественные визуализации;
• На момент написания статьи только что вышла версия Alloy 5 Beta;
• Тогда я успел долго поработать с TLA+ кряду, и мне все равно нужно было переключиться.

Итак, давайте начнем. Чтобы проще было следить за логикой поста, можете скачать Alloy здесь. Если ранее вам не доводилось работать с Alloy, рекомендую сначала прочесть мою вводную статью – в ней я объясняю все термины, которые здесь использую.

Сферический менеджер пакетов в вакууме

Начнем со следующих допущений:

• Все пакеты делятся на два типа: программы – это пакеты, которые мы пытаемся установить. Обязательные пакеты – это пакеты, которых требует программа. Сами обязательные пакеты ничего не требуют.
• Все пакеты могут предусматривать или не предусматривать обновления. Обновления являются линейными и ациклическими: чаще всего одна сущность обновляется до целой программы, программа в конечном итоге не может обновиться сама до себя, т.д. Обновление не может превратить обязательный пакет в обычный и наоборот. Множество всех программ в заданном списке обновлений называется версией программы.
• Никакого бессмысленного порочного круга тут не возникает: программа не может требовать некоторую сущность сразу с ее же обновлением, не может требовать собственного обновления, т.д. Большинство из этого подразумевается в первых двух допущениях, но, если сделать первые два допущения менее строгими, то третье все равно будет в силе.

На практике соблюдение всех этих допущений не гарантировано, и, если они не соблюдаются, то спецификация считается проваленной. Тем не менее, эти допущения все равно пригодятся нам для исследования не столь тяжелых случаев, а более подробная модель может быть не столь информативной для людей, которые не совсем в теме – например, как я.(2) Давайте выразим эти допущения в коде:

open util/ordering[Time]
sig Time {}
 
abstract sig Package {
  requires: set Requirement,
  installed: set Time,
  upgrade: lone Package
} {
  lone @upgrade.this
  no requires & requires.^@upgrade
}
 
sig Program extends Package {} { upgrade in Program }
sig Requirement extends Package {} {
  no requires
  upgrade in Requirement
}
 
fun other_versions: Package -> set Package {
  ^upgrade + ^~upgrade
}
 
fun versions: Package -> set Package {
  other_versions + (Program <: iden)
}
 
fact NoCycleNonsense {
  all p: Package | p not in p.other_versions
  no (^requires + ^~requires) & versions
}

Будем ориентироваться на время. Нам известно о пакете два факта: чаще всего до него обновляется одна сущность, и он не может требовать собственного обновления. @ — это уловка, позволяющая не расширять сигнатуру; без этого знака Alloy заменит upgrade на this.upgrade. Функции просто дают нам версии (versions) в виде нуль-арных отношений, а не монадических функций. Циклические ограничения мы сами прописываем по факту, поэтому в каком угодно решении они возникнуть не могут.

Что касается нашего сферического менеджера пакетов – постулируем, что он работает следующим образом:

• За один шаг он может получить только один пакет.
• На каждом заданном шаге он выбирает пакет, которого нет в системе. Он пытается установить или обновить этот пакет так:

1. Если недостает каких-либо обязательных пакетов, то они либо обновляются, либо устанавливаются. На это может уйти несколько шагов.
2. Если никакой версии нужного пакета не установлено, то требуется установить этот пакет.
3. Если установлена предыдущая версия данного пакета, то ее нужно «обновить», удалив старый пакет и установив на ее место новый.

Таким образом, если пакет предусматривает два обязательных пакета, то мы можем получить всю группу за три шага: установить обязательный пакет A, установить обязательный пакет B, установить нужный нам пакет. Также, согласно нашим правилам, в любой момент у нас может быть установлена всего одна версия пакета. Кому-то из вас уже кажется, что это какой-то кринж. Потерпите, скоро и все остальные поймут, почему такая расстановка никуда не годится.

pred install (t, t': Time, p: Package) {
  no p.versions & installed.t
  p.requires in installed.t 
 
  installed.t' = (installed.t + p)
}
 
 
pred upgrade_to (t, t': Time, p: Package) {
  p not in installed.t
  p.requires in installed.t
  some p': Package | {
	p' in (installed.t & (^upgrade).p) //old version   
	installed.t' = (installed.t + p - p')
  }
}
 
fact Trace {
  no installed.first
  all t: Time - last | let t' = t.next |
	some p: Program | {
  	install[t, t', p] or upgrade_to[t, t', p]
  	or some p': p.requires | {
    	install[t, t', p'] or upgrade_to[t, t', p']
  	}
	}
}

Вот у нас и есть утверждение, которые мы хотим проверить. Вот какое утверждение проверю я: если пакет установлен, то безусловно должны быть установлены и все другие пакеты, которых он требует. Иначе у нас возникнет нарушение требования.

assert AllRequirements {
  all t: Time | requires[installed.t] in installed.t
}
 
check AllRequirements for 4

Вероятно, вы уже видите, где здесь нарушение.



P1 требует R1, но P0 требует R0. Как только мы проведем R1 -> R0, окажется, что в системе установлены не все пакеты, обязательные для P1.(3) Вот почему в большинстве в некоторых менеджерах пакетов такой подход к обновлению файлов не практикуется. Вместо этого просто устанавливаются обе версии.

pred install (t, t': Time, p: Package) {
  p.requires in installed.t
  installed.t' = (installed.t + p)
}
 
fact Trace {
  no installed.first
  all t: Time - last | let t' = t.next |
	some p: Program | {
  	install[t, t', p]
  	or some p': p.requires | install[t, t', p']
	}
}

В таком виде проблема исчезает. Это и есть базовая спецификация, которую мы будем сравнивать Nix. На будущее мы дополнительно упростим спецификацию, указав, что менеджер пакетов может за один шаг установить как пакет, так и все пакеты, обязательные для него. То есть:

pred install (t, t': Time, p: Package) {
-  p.requires in installed.t
-  installed.t' = (installed.t + p)
+  p not in installed.t
+  installed.t' = (installed.t + p + p.requires)
 
fact Trace {
  no installed.first
  all t: Time - last | let t' = t.next |
    some p: Program | {
  	install[t, t', p]
-  	or some p': p.requires | install[t, t', p']
    }
}

Полнота

Одно из заявляемых достоинств Nix заключается в том, что это чисто функциональный менеджер пакетов. Он чист в том, что успешность или неуспешность сборки никак не зависит от более ранних сборок.4 Чтобы понять, почему это благо, давайте исследуем, как именно делается сборка. Разработчик вручную перечисляет, какие пакеты обязательно требуются для конкретного пакета, а затем загружает их. Устанавливая пакет, пользователь также устанавливает все пакеты, обязательные для первого. Но как нам гарантировать, что этот процесс, налаженный на машине разработчика, будет работать и на машинах у пользователей?

Один из вариантов проверки – не ограничиваться простым представлением менеджера пакетов, а выстроить «симуляцию» более обширного окружения. В данном случае мы неявно определим другого пользователя, добавив зависимый источник. Также мы создадим явное отношение, согласно которому любые пакеты, которые обязан установить разработчик, соответствуют требованиям. Сначала разработчик устанавливает обязательные пакеты. Все, что он на данном этапе устанавливает, будет иметь статус explicit для нужного пакета. Пользователь, пытаясь установить пакет, также устанавливает все в explicit. Как бы то ни было, это не должно приводить к багам. Давайте это выразим в коде.

abstract sig Package {
+  explicit: set Requirement,
+  dependent: set Time,
} {
+  explicit in requires
}
 
pred install (t, t': Time, p: Package) {
+  p.explicit = p.requires & (installed.t' - installed.t)
+  dependent.t' = dependent.t
}
 
+ pred install_to_dependent (t, t': Time, p: Package) {
+   p not in dependent.t
+   p in installed.t //чтобы гарантировать, что explicit будет определено
+   dependent.t' = dependent.t + p + p.explicit
+   installed.t' = installed.t
+ }
 
fact Trace {
+  no dependent.first
  all t: Time - last | let t' = t.next |
    some p: Program | {
+  	install[t, t', p] or install_to_dependent[t, t', p]
    }
}
 
assert AllRequirements {
  all t: Time | {
+	requires[dependent.t] in dependent.t
  }
}

Хочу отдельно обратить ваше внимание на строку to p.explicit =… в install. Выглядит как операция присваивание, но, на мой взгляд, здесь просто неверно используется нотация. Предикаты не устанавливают значений. Это просто утверждения, которые могут быть истинны либо ложны. Если install[t, t', p] истинно, то p.explicit =… также должно быть истинно. «На практике» это аналогично присваиванию. Если install[t, t', p] ложно, то нам ничего не известно о p.explicit. Там может не быть ничего, а могут быть перечислены все до одного обязательные пакеты к этой модели. Alloy может свободно обращаться с этой информацией как потребуется.

Вот почему у нас стоит p в installed.t in install_to_dependent. В контексте нашей модели p в installed.t истинно только тогда, когда истинно install[t, t', p], а это истинно лишь в случае, если p.explicit работает нормально. Итак, добавив эту дополнительную строку к install_to_dependent, мы проверяем модель только тогда, когда у нас есть ожидаемое explicit.

Эта модель также не годится.

1. Разработчик собирает P1, которая состоит из R0 и R1. P1.explicit = R0 + R1.
2. Разработчик собирает P0. Притом, что P0 требует R1, разработчик не добавляет его к explicit, так как он уже попал на компьютер к разработчику путем P1. P0.explicit = {}
3. Пользователь устанавливает P0. У него не хватает обязательного пакета, поэтому наше утверждение не выполняется.

Есть способ это исправить – просто установить set explicit = requires. Но это просто отмазка, предполагающая, что все необходимые пакеты известны разработчику заранее. Мы же пытаемся обеспечить работоспособность нашего решения, даже если разработчик будет допускать ошибки!

Давайте попробуем совершенно иной подход. Вместо того, чтобы менять способ подсчета обязательных пакетов, поменяем порядок отслеживания установок в менеджере пакетов. До сих пор мы просто делали installed пары из пакетов и значений времени на каждый пакет. Давайте лучше оперировать тройками: один пакет, одна программа и значение времени. Имеется в виду та программа, для которой был установлен пакет.

-  installed: set Time,
-  dependent: set Time,
+  installed: Package -> set Time,
+  dependent: Package -> set Time,

Теперь нам нужно изменить операции, выполняемые install и install_to_dependent:

pred install (t, t': Time, p: Package) {
-  p not in installed.t
-  installed.t' = (installed.t + p + p.requires)
+  p -> p not in installed.t
+  installed.t' = installed.t + p -> (p + p.requires)
 
//...
 
pred install_to_dependent (t, t': Time, p: Package) {
-  p not in dependent.t
-  p in installed.t //to enforce that explicit is defined
+  p -> p not in dependent.t
+  p -> p in installed.t //to enforce that explicit is defined
+  dependent.t' = dependent.t + p -> (p + p.explicit)

Оператор -> здесь обозначает отношение: p -> p значит, что p отображается само на себя. p -> (p + p.requires) эквивалентно (p -> p) + p -> p.requires. Наконец, нам нужно и переформулировать утверждение, чтобы корректно выразить в нем все требования.

assert AllRequirements {
  all t: Time | {
-  	requires[installed.t] in installed.t
-  	requires[dependent.t] in dependent.t
+  	Program.(installed.t).requires in Program.installed.t
+  	Program.(dependent.t).requires in Program.dependent.t
  }
}

Запускаем этот код и видим, что никаких ошибок не осталось! Дело в том, что теперь разработчику мало поставить обязательные пакеты только на своем компьютере. Поскольку мы устанавливаем обязательные пакеты с привязкой к соответствующей программе, установить требуется полную копию каждого из обязательных пакетов – и только тогда получится программа. Таким образом, явные зависимости всегда соответствуют фактическим требованиям.

Именно так и построена работа в Nix. Обеспечивая изоляцию всех требований, вы получаете детерминированную сборку. Если она работает на вашей машине, то (в идеале) должна работать и на других машинах, независимо от их текущего состояния.

Вот окончательная версия спецификации:

open util/ordering[Time]
sig Time {}
 
abstract sig Package {
  requires: set Requirement,
  explicit: set Requirement,
  installed: Package -> set Time,
  dependent: Package -> set Time,
  upgrade: lone Package
} {
  lone @upgrade.this
  no requires & requires.^@upgrade
  explicit in requires
}
 
sig Program extends Package {} { upgrade in Program }
sig Requirement extends Package {} {
  no requires
  upgrade in Requirement
}
 
fun other_versions: Package -> set Package {
  ^upgrade + ^~upgrade
}
 
fun versions: Package -> set Package {
  other_versions + (Program <: iden)
}
 
fact NoCycleNonsense {
  all p: Package | p not in p.other_versions
  no (^requires + ^~requires) & versions
}
 
 
pred install (t, t': Time, p: Package) {
  p -> p not in  installed.t
  installed.t' = installed.t + p -> (p + p.requires)
  p.explicit = p.requires & p.(installed.t' - installed.t)
  dependent.t' = dependent.t
}
 
pred install_to_dependent (t, t': Time, p: Package) {
  p -> p not in dependent.t
  p -> p in installed.t //to enforce that explicit is defined
  dependent.t' = dependent.t + p -> (p + p.explicit)
  installed.t' = installed.t
}
 
fact Trace {
  no installed.first
  no dependent.first
  all t: Time - last | let t' = t.next |
	some p: Program | {
  	install[t, t', p] or install_to_dependent[t, t', p]
	}
}
 
assert AllRequirements {
  all t: Time | {
  	Program.(installed.t).requires in Program.installed.t
  	Program.(dependent.t).requires in Program.dependent.t
  }
}
 
check AllRequirements for 4

Заключение

Написав спецификацию системы, видим пару распространенных сценариев отказа, которые случаются с менеджерами пакетов. Также мы разобрались, как Nix справляется с одной из этих бед. Формальные методы – очень мощное средство для поиска багов! Кроме того, как я указывал ранее, они очень хороши в случаях, когда требуется понять предметную область, к которой относится ваша задача. Думаю, теперь я сам гораздо лучше представляю, как работает Nix.(5)

Nix находится здесь, а Alloy, конечно же, здесь. Если вы еще не наигрались с этой моделью, то можете поупражняться еще на следующих задачах:

• Что произойдет, если мы разрешим всем обязательным пакетам иметь requires? По-прежнему ли все будет работать? Если нет, то как это можно исправить?
• В Nix есть фича под названием профили. Допустим, у вас есть два пакета для Python, но пользователь, возможно, захочет, чтобы в каждый момент времени в системе присутствовал ровно один пакет: например, python bar.py, а не vp969yhdq-python bar.py. Как представить такую ситуацию в Alloy?
• Еще в Nix есть фича под названием откат, позволяющая вернуть систему к более раннему состоянию (значению Time). Какие свойства откатов стоит проверять? Помогает ли вообще в данном случае структура Nix? Не забывайте, что можно создавать предикаты в t.prev или t.next.next.
• Часто в программах в качестве требований указываются некоторые диапазоны. Например, программа может работать с любой из версий 2, 3, 4. Как это представить? Возможно, примерно так, как сделано здесь.

На самом деле, я ничего этого не делал, поэтому любая задача может оказаться как тривиальной, так и невыполнимой. Удачи!

Дополнение

Мне неоднократно писали, что большинство менеджеров пакетов плохо справляется с обновлениями. Видимо, многие просто пытаются найти версию, соответствующую всем требованиям – и надеются на лучшее. Что мне сразу приходит на ум в ответ:

1. aaaaaaaaaaaaaaaa
2. Что ж, а это еще один плюс от использования Nix
3. aaaaaaaaaaaaaaaa

Но, думаю, это также лишний раз подчеркивает, насколько сильны формальные методы. Мысль «а с обновлениями работать непросто» возникла у меня через несколько минут после того, как я приступил к работе над спецификацией. Похожие вещи замечал и с TLA+, и даже с неформальным моделированием в graphviz: если просто найти способ, позволяющий четко осмыслить вашу систему, то общее качество системы резко возрастает.

1. С одной стороны, это медленно, и ничего не работает. С другой стороны — AutoHotKey! [return]
2. Мне сложно уделить 50+ часов на то, чтобы разобраться в проблемах работы с менеджерами пакетов, особенно ради поста на 2000 слов. [return]
3. Если вы увидите что-либо гораздо более путаное, попробуйте сделать проекцию на Time и скрыть versions и other_versions. [return]
4. Это используется слеееегка небрежно, поскольку меняет состояние вашей системы. [return]
5. Еще один урок, который я из этого извлек – в самом деле, стоит сделать шпаргалку по Alloy. Искать ответы на все синтаксические вопросы в бумажной книге – настоящая мука. [return]