Я вынуждена признаться: последние 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 очень помог нам на этом пути.
ссылка на оригинал статьи https://habr.com/ru/company/timeweb/blog/646409/
Добавить комментарий