Я вынуждена признаться: последние 8 лет я избегаю Docker. И дело тут не в непонимании пользы контейнеров. Мой первый опыт использования Docker оказался очень плохим. Настолько плохим, что убедил меня в том, что я не смогу освоить эту сложную технологию до приличного уровня. Позже я узнала, что из-за характера поставленной задачи (и поскольку я была и остаюсь пользователем Mac), я, на свое несчастье, столкнулась с большинством неприятных проблем ранних версий Docker. К моменту осознания этого, я уже полностью переключилась на устаревшие технологии, где большинство моих проблем было связано с попыткой развернуть контроль версий или базовое тестирование…

Чуть позже я занялась менеджментом и казалось, что мне больше никогда не придется столкнуться со своими страхами в лице Docker! Ура!

А потом появился Fault.

Fault — это проект по разработке языка программирования. На определенном этапе его развития стало очевидно, что для выполнения спецификаций Fault потребуется SMT-решатель. Возник вопрос о том, как правильно управлять зависимостями, не связанными с основным ЯП проекта — Go. Я пробовала применять разные подходы для решения, параллельно ощущая маячащий вдалеке Docker.

В этот раз я точно понимала, как заставить Docker сделать то, что я хочу. Этот факт не мог не радовать. Единственная проблема заключалась в том, что Fault как язык программирования должен работать в командной строке. В то же время использование Docker предполагает создание веб-сервиса, который будет обмениваться информацией с остальными объектами через открытые порты. Но приложения командной строки не взаимодействуют таким образом. Я хотела сохранить интерфейс командной строки, при этом не отказываясь от преимуществ контейнеризации.

Шаг первый: многоэтапная сборка (multi-stage docker)

Основная причина использования Docker в проекте — это критическая зависимость Fault от Z3. Если на устройстве, на котором создаются спецификации Fault, не установлен и не настроен Z3, то Fault может скомпилировать их в SMTLib2 (язык SMT-решателя), но не оценить их. Это может показаться особенностью конкретно моего проекта, но, на самом деле, многие языки программирования зависят от чего-то наподобие LLVM или JVM. Типичный подход заключается в создании инсталлера, устанавливающего все зависимости (и в надежде на отсутствие конфликтов версий), либо в перекладывании всех ошибок на плечи пользователей, подталкивая их к циклу google->stackoverflow->apt-get.

В нашем случае Docker является особенно хорошим решением. Всё дело в том, что люди, которым нравится решать технические проблемы с помощью SMT-решателя чем-то похожи на фанатов драг-рейсинга. Я подразумеваю, что любители драг-рейсинга — это такое небольшое сообщество людей, уверенных, что они могут менять детали в двигателе по своему усмотрению и «выжимать» его до предела. Z3 — один из самых передовых и стабильных SMT-решателей, но некоторые пользователи неизбежно захотят создать сборки Fault с другими SMT-решателями. 

Сделать многоэтапную сборку Docker очень легко. На первом этапе официальный образ Go используется в качестве базового и с его помощью создается бинарный файл компилятора Fault. На следующем этапе в качестве базового используется образ Z3, копируется бинарный файл Fault и настраивается большая часть оставшейся конфигурации. Какой именно SMT-решатель используется в сборке Fault определяется переменной среды в контейнере. При работе со спецификацией Fault ищет эту переменную и загружает в шаблон соответствующий SMT-решатель. 

Таким образом, добавить поддержку нового SMT-решателя так же просто, как и написать для него шаблон и добавить Dockerfile.

Шаг 2: Makefile установщик

Хитрость заключается в том, что результат каждого из этапов многоэтапной сборки сохраняется в репозитории как Dockerfile, после чего установщик объединяет их в новый Dockerfile. Именно его использует команда docker build. Это всё, что делает установщик: собирает финальный Dockerfile и запускает docker build. Я решила использовать Makefile, потому что поддержка нового SMT-решателя — это просто новое правило в том же файле. Я запускаю команду make fault-z3 для билда Fault с Z3, а позже смогу запустить Fault с Yices с помощью make fault-yices.

Шаг 3: Размещение CLI в PATH хоста

С помощью команд ENTRYPOINT и CMD в Dockerfile можно “докеризировать” инструменты командной строки. ENTRYPOINT передаёт в Docker команду, которую необходимо инициировать при запуске контейнера CMD, а также передает значения по умолчанию для любых необходимых аргументов или флагов. 

Бинарный файл Fault на вход требует три аргумента:

• расположение входного файла;
• input или тип входного файла. Компилятор будет анализировать спецификации написанные на Fault (.fspec), а также написанный вами код SMT и отправлять их SMT-решателю;
• mode — пользователь может остановить компилятор на ранней стадии и узнать текущее состояние входных данных. 

Вот как это выглядит в Dockerfile. mode и input имеют значение по умолчанию, а требуемый аргумент по умолчанию является пустой строкой. Пустая строка вызывает обработанную ошибку и передает её хосту.

ENTRYPOINT [ "./fcompiler"]
CMD [ "-mode=check", "-input=fspec", ""]

Теперь мы можем запустить компилятор Fault на машине-хосте следующим образом:

docker run fault-lang/fault-z3 -filepath=test.fspec

Docker запускает контейнер, выполняет компиляцию и закрывает контейнер, когда компилятор возвращает результат. Отлично… За исключением того, строка получилась слишком длинной и неказистой. Я не хочу, чтобы пользователи использовали команду docker run для работы с Fault. Я хочу видеть что-то наподобие fault -filepath=...

Для решения этого вопроса подойдёт простой скрипт bash, который можно добавить в PATH хост-компьютера:

#!/bin/bash
while getopts f:m:i: flag
do
    case "${flag}" in
        f) file=${OPTARG};;
        m) mode=${OPTARG};;
        i) input=${OPTARG};;
    esac
done
if [ -z "$file" ]
then
    echo "You must specify a spec file."
else
    docker run fault-lang/fault-z3 -mode=$mode -filepath=$file
    -input=$input
fi

Я предпочла выбрать bash из-за удобства, но на самом деле это можно сделать на любом скриптовом языке.

Все, что осталось сделать — добавить строку в Makefile, скопировав скрипт из репозитория Fault в /usr/local/bin с названием fault без расширения.

Шаг 4: Файловая система хоста

Место, где Fault будет искать файл спецификации, находится внутри контейнера, а именно в файловой системе хост-компьютера. Для того чтобы это работало, Docker должен смонтировать всю или часть файловой системы хоста. К счастью, подобная манипуляция — это довольно простое изменение скрипта на bash:

docker run -v ${HOME}:/host:ro fault-lang/fault-z3 -mode=$mode -filepath=$filepath -input=$input

-v ${HOME}:/host монтирует домашний каталог в каталог в контейнере с названием host. У меня были мысли о том, чтобы установщик настраивал определенный каталог и монтировал его вместо этого, примерно так же, как в старых версиях Go требовалось, чтобы все файлы go находились в директории GOPATH. Но большинство разработчиков предпочитают сохранять файлы спецификаций с исходных кодом, который эти спецификации и определяет. Конечно, при монтировании такой большой части файловой системы хоста возникают некоторые вопросы касательно безопасности, однако Fault только читает файлы спецификации, поэтому я ограничилась установкой режима “только чтение” (:ro) между хостом и контейнером и двинулась дальше.

Одна из вещей, которую я избегала — запись зависимости от Docker в компилятор. Помимо того, что вы должны иметь возможность запустить Fault в Docker, вы также должны иметь возможность запустить его вне контейнера, при условии наличия на компьютере установленных LLVM и Z3.

Монтирование $HOME каталога в /host подразумевает, что заключительный этап этого шага — это небольшой хакинг. Компилятору необходимо определить, находиться он в контейнере или нет, а затем соответствующем образом изменить пути. Я решила эту проблему установив с помощью переменной среды, определяющей путь к хосту. Если Fault работает в контейнере, то необходимо изменить путь к файлам, прежде чем пытаться их открыть. В противоположном случае компилятор оставляет всё в покое.

Шаг 5: VERSION и HELP

Для более эффективного использования ресурсов, некоторые аргументы, такие как получение справочного меню или проверка версии, желательно не пропускать через Fault и контейнер, запуск которого занимает некоторое время. Поэтому я решила изменить скрипт bash, чтобы обрабатывать эти ситуации, при этом никак не взаимодействуя с Fault. Справка — это простая функция, которая выводит отформатированное справочное руководство для пользователей:

Help()
{
# Display Help
echo "###########################################################"
echo "Fault: a language and model checker for dynamic systems"
echo "###########################################################"
echo
echo "-f [filepath]    spec file."
echo "-h               print this help guide."
echo "-m [mode]        stop compiler at certain milestones: ast,"
echo "                 ir, smt, or check (default: check)"
echo
echo "-i [input]       format of the input file (default: fspec)"
echo "-V               print software version and exit."
echo
}
####################################################################
# Main program                                                                 #
####################################################################
while getopts f:m:i:h flag
do
    case "${flag}" in
        f) file=${OPTARG};;
        m) mode=${OPTARG};;
        i) input=${OPTARG};;
        h) Help
           exit;;
    esac
done
if [ -z "$file" ]
then
    echo "You must specify a spec file."
else
    docker run fault-lang/fault-z3 -mode=$mode -filepath=$file
    -input=$input
fi

Вопрос с версией ПО был немного интереснее. Обычной практикой является хранение информации о версии в тегах git, но в финальном Docker хранится бинарник Fault, а не исходный код. Поскольку мы создаем образ контейнера, необходимо добавить информацию о версии в LABEL и, дабы быть любезными перед будущими разработчиками, я хочу следовать стандарту OCI (Open Container Iniciative) для этого типа метаданных:

LABEL org.opencontainers.image.vendor="Fault-lang"
LABEL org.opencontainers.image.authors="Marianne Bellotti"
LABEL org.opencontainers.image.created=${BUILD_DATE}
LABEL org.opencontainers.image.version=${BUILD_VERSION}
LABEL org.opencontainers.image.licenses="MIT"
LABEL org.opencontainers.image.description="Fault using Z3Solver as its engine"

Значения BUILD_DATE и BUILD_VERSION передаются с помощью флага --build-arg, поэтому Makefile ожидает небольшая корректировка:

VERSION := $$(git describe --tags --abbrev=0)
fault-z3:
     $(shell touch "fault.Dockerfile")
     cat Dockerfile ./solvers/z3.Dockerfile > fault.Dockerfile
     @docker build -t ${NAME}-z3:${TAG} --no-cache --build-arg
         BUILD_VERSION=${VERSION} --build-arg BUILD_DATE=$(date) -f
         fault.Dockerfile .
     @docker tag ${NAME}-z3:${TAG} ${NAME}-z3:latest
     @rm fault.Dockerfile
     @cp fault-lang.sh /usr/local/bin/fault

Теперь в скрипте bash я создаю функцию Version():

Version()
{
   # Lookup the current version of Fault
   docker inspect fault-lang/fault-z3 -f='{{ index .Config.Labels
   "org.opencontainers.image.version" }}'
}

Вуаля! Теперь, когда пользователь инициирует команду make fault-z3 создается двоичный файл Fault, который поступает в контейнер с SMT-решателем. В PATH добавляется bash скрипт, который предоставляет пользователю чистый интерфейс и избавляет от гадания, работает Docker или нет. 

Однако Fault ещё не готов полностью. Я проделала эту работу в стремлении подготовить Fault к работе для других людей. Предстоит пройти ещё большой путь, но Fault становится всё ближе к тому, чтобы пользователи могли его запускать на своих компьютерах каждый день, и Docker очень помог нам на этом пути.