Harnessing Docker for Programming Language Deployment
Written on
Chapter 1: Introduction to Docker and Fault
I have a confession: for the past eight years, I have steered clear of Docker. It’s not that I lack comprehension of container technology; rather, my initial encounter with Docker was overwhelmingly negative. This experience led me to believe that mastering it was beyond my capabilities. I later realized that my difficulties stemmed from the specific tasks I was attempting to perform with Docker, combined with my primary use of a Mac. I encountered many of the early complications that troubled users back then. By the time I understood this, I had transitioned to legacy technologies, where my focus shifted to version control and basic testing—Docker was not on my radar.
After a while, I moved into management, thinking I had escaped the need to confront my Docker fears. However, that all changed with the introduction of Fault.
Fault is the programming language I am developing. As I refined its design, it became clear that executing Fault specifications would necessitate a SMT Solver. This raised the question of how to manage the non-Go dependencies within a Go codebase effectively. I experimented with several strategies, achieving varying degrees of success, all while knowing Docker was looming in the background.
This time, however, I found it surprisingly straightforward to get Docker to perform as needed, which was a huge relief! With Go binaries built and the solver operational, I was ready to move forward.
The challenge was that Fault, as a programming language, is intended to run in a command-line environment. Docker typically operates under the assumption that applications are web services communicating over open ports. I wanted to preserve the command-line interface (CLI) experience while benefiting from containerization.
Section 1.1: Multi-Stage Docker Builds
The necessity of Docker arose due to Fault's critical dependency on Z3. Without Z3 installed and configured on the development machine, while Fault can compile specifications to SMTLib2 (the language of SMT Solvers), it cannot evaluate them. This issue may appear unique to my project, but most programming languages rely on backends like LLVM or JVM.
Traditionally, developers either create an installer that manages these dependencies (hoping to avoid version conflicts) or encounter errors that push them into a cycle of Google searches, StackOverflow, and package installations.
For my case, Docker proved to be an excellent solution. The community of SMT solver enthusiasts is akin to those who enjoy customizing and racing hotrods. They expect to interchange components and push boundaries. Z3 is the most established and reliable SMT solver, but users often desire custom builds of Fault with different solvers.
Docker's multi-stage builds simplified this process significantly. The initial stage utilizes an official Go image as a base to compile the Fault compiler into a binary. The subsequent stage employs Z3's image, transferring the Fault binary and configuring the rest. The choice of solver for the Fault build is determined by an environment variable within the container. When evaluating specifications, Fault checks this variable to load the appropriate command execution template.
Thus, adding a new solver support becomes as easy as crafting a corresponding template and updating the Dockerfile.
Section 1.2: Crafting the Installer Makefile
Each step within the multi-stage build resides in its own Dockerfile within the repository. The installer script generates a new Dockerfile that combines the Fault binary stage Dockerfile with the solver Dockerfile, which is then utilized by the docker build process. I chose to implement this using make, as I find Makefiles comforting. Each new solver is merely an additional rule in the same file. For instance, executing make fault-z3 builds Fault configured for Z3, while a future command make fault-yices could yield a Yices-based build.
Subsection 1.2.1: Integrating CLI with the Host's PATH
Dockerizing command-line tools is achievable through the use of ENTRYPOINT and CMD in the Dockerfile. ENTRYPOINT specifies the command Docker should execute upon container startup, while CMD provides default arguments or flags.
The Fault binary requires three key pieces of information from the user:
- The location of the input file (mandatory)
- The input format of the file (optional)
- A mode to halt the compiler at specific points
By default, Fault translates to LLVM IR, writes SMT code, and verifies the model with an SMT solver.
Here’s how it is represented in the Dockerfile:
ENTRYPOINT [ "./fcompiler"]
CMD [ "-mode=check", "-input=fspec", ""]
Now, running the Fault compiler on the host machine can be executed as follows:
docker run fault-lang/fault-z3 -filepath=test.fspec
While this works, it is cumbersome to type. I want users to simply execute fault -filepath=... like they would with any programming language.
To address this, I created a simple bash script to place in the host machine's PATH:
#!/bin/bash
while getopts f:m:i: flag
do
case "${flag}" in
- file=${OPTARG};;
- mode=${OPTARG};;
- 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
Section 1.3: File System Interaction
The Fault compiler requires access to spec files, which reside on the host filesystem. Docker must therefore mount the relevant portions of the host’s filesystem. This adjustment is straightforward in the bash script:
docker run -v ${HOME}:/host:ro fault-lang/fault-z3 -mode=$mode -filepath=$filepath -input=$input
Here, ${HOME}:/host mounts the home directory to a directory named host within the container. While I considered having the installer set up a specific directory for mounting, most developers prefer keeping their spec files alongside the source code.
Though there are security concerns regarding mounting extensive parts of the host filesystem, I felt comfortable making the bind read-only since Fault only needs to access spec files.
One crucial aspect was ensuring that the compiler does not become dependent on Docker. Users should be able to run Fault in Docker, but if they have LLVM and Z3 installed on their host, they should also be able to build and run the compiler independently of the container.
By mounting the $HOME directory under /host, the final phase of this step involves some path adjustments. The compiler needs to determine if it’s operating within a container and adjust the file paths accordingly. I accomplished this by setting a specific environment variable that indicates when Fault is running in a container.
Chapter 2: Enhancing User Experience
Section 2.1: Adding Versioning and Help Functionality
Certain arguments should not be passed to Fault when running in a container, as starting the container incurs a delay (Z3 is quite large), which is inefficient for tasks like displaying help or checking the version.
To optimize this, I modified the bash script to handle those requests without engaging Fault. The help function generates a well-formatted help guide:
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
}
For versioning, I utilized git tags to store version information. The final Docker container should only contain the binary, not the source code. Therefore, the version data must be incorporated into a LABEL during container image construction, adhering to Open Containers standards:
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"
The BUILD_DATE and BUILD_VERSION values are supplied via the --build-arg flag, necessitating slight adjustments to the Makefile installer.
In the bash script, I introduced a function to retrieve the current version:
Version()
{
docker inspect fault-lang/fault-z3 -f='{{ index .Config.Labels "org.opencontainers.image.version" }}'
}
As a result, when users execute make fault-z3, the Fault binary is built, transferred into a container with the pre-installed solver, and a bash script providing a clean user interface is added to the PATH.
While Fault is not yet fully ready for widespread use, these enhancements were part of my efforts to prepare it for future contributors. Significant work remains, and the complete Fault grammar is only partially implemented. Nevertheless, we are moving closer to making it accessible for everyday use, with Docker playing a vital role in this journey.