Introduction

The Purely Functional Software Deployment Model¹ by Eelco Dolstra (herein referred to as "the thesis") is often pointed to as a great resource for learning about nix, albeit technical and formal. I wanted to read it myself, and see if it was as good as people said. I found that the thesis was very accessible, remarkably relevant given its age, and that a significant portion of the content was philosophical rather than technical. Therefore, my aspiration for this blog post is to crystallize some of the insights from the thesis into short form content. Hopefully this post will inspire you to go on and read the full text, or at least provide an expedient proxy for doing so.

Table of Contents

• Correct Software Deployment
  • Correctness
  • Software Deployment
  • Bonus: Manageability & Usability
• Problems With Existing Solutions
• The Benefits of Nix
• Implementation Details
  • The Nix Store
  • Filesystem As Memory
  • Purely Functional Model
• Nix Principles
• Topics Not Covered
• Footnotes

Correct Software Deployment

I'm going to start at the end of the thesis. Dolstra, summarizing the thesis in the conclusion, says that the purpose of the project was to achieve a system for correct software deployment. He then goes on to explain that correctness is achieved through two main vehicles. First, through a precise naming scheme that leverages cryptographic hashes to concisely summarize the software identified by said name. This naming schema helps us achieve a much richer notion of equality than conventional naming schema (i.e. openssl-3.0.8). A "purely functional model" of software deployment. What exactly is meant by "purely functional model" is slightly unclear, but my understanding is that it boils down to immutable build artifacts, pure build processes (depend only on their inputs) that admit no side-effects, and compositionality of software components.² The purely functional bit is particularly confusing because the nix expression language is itself purely functional, but the really critical piece is the functional principles applied to build and deployment strategies.

One ambiguity that might lead to confusion is that there is a distinction between the philosophical aspects of the thesis (i.e. an ontology of software deployment, and what constitutes correct software deployment), and the techniques / implementations that are guided by the theory. The Implementation Details section will try to explain how constructs (such as the cryptographic naming scheme, and purely functional deployment model) connect to the theory, albeit with less formality than the original thesis. The current section will look at the philosophy, and focusing on:

• What is meant by correctness?
• What does software deployment entail?
• What are some desirable qualities of a correct system?

Correctness

The simplest way to summarize correctness as it pertains to software deployments is through this formula correctness = complete + no interference. Completeness refers to the presence of all dependencies. Interference refers to the case where two different software components occupy the same namespace, and are therefore indistinguishable to the component that depends on one of them.

Note: The notion of equality mentioned earlier is important here. When we say "two different" we mean that there is some equivalence relation that does not hold, but the fact that they occupy the same namespace means there is some nominal equivalence relationship that does hold, but it is wrong in some sense.

There are plenty of examples of bipartite definitions of correctness that rhyme with this one (soundness and completeness in logic), but I am going to steal the imagery from a classic example in discrete mathematics; bijectivity. For the following images the circle on the left represents the set of software components in the environment available to us. The circle on the right represents the set of dependencies that are actually required to build the software component of interest. An arrow from left to right means that the component on the left has been identified as corresponding to the dependency required on the right.

Terminology: In the thesis Dolstra refers to discrete units of software as components. These can be software that we are building, or software that has already been built. These can be composed together through dependency relations. Put another way: components can be the build inputs of other components.

The diagram below illustrates a situation where there is no interference. This means that there are no components in the environment on the left that could be accidentally mixed up when provided to the build. In other words there is a 1:1 correspondence between the components we have identified in the environment and the ones that we actually want.

Non-interference is not enough, however. You probably noticed that there is a required dependency on the right that is unfulfilled. This is where completeness comes in; it entails that all required dependencies on the right are provided and accounted for on the left.

The next diagram demonstrates the case where we have a complete deployment. Every required dependency on the right is provided by at least one component in the environment on the left. However, the catch here is that there is ambiguity, there are two components that have both been identified as fulfilling a dependency requirement, but by some notion of equality they are different (i.e. perhaps they are the same software by name, at the same version, but one is compiled with a threaded runtime and the other with a synchronous runtime). This is an example of interference, there is no way to tell that we will get the input that we really mean.

To make the example more concrete: perhaps the purple dot on the left is openssl-3.0.8 and the orange dot is openssl-1.1, and the blue dot on the right is just a requirement for openssl, and the arrows from the purple and orange dot are a lookup on $PATH for /usr/bin/openssl. Well, since both versions of openssl can live at that location, we are not sure which we will get, and therefore we might get a different component than the one that we actually mean, the way that we identify components in this example is too coarse grained.

This diagram demonstrates what is meant by correct deployment. There is exactly one software component corresponding to every dependency requirement.

If you are familiar with functions from discrete mathematics, you probably noticed that I hand-waved away the existence of components in the environment on the left that are not required dependencies on the right. If you are unsatisfied you can imagine a pruning function that eliminates superfluous components that can be pre-composed with this function.

To reiterate, correctness = completeness + no intereference:

• To ensure completeness we must guarantee that at least one component is identified for every required dependency
• To ensure non-interference we must guarantee that there is at most one component identified for every required dependency, and that the component identified is the one that we really mean

Software Deployment

Software deployment is the distribution of software; the acquisition, installation, upgrading, and uninstallation process.³ There are two broad classes of problems with software deployment: managing the environment and correctness as discussed in the previous section, and manageability / usability as discussed in the next section.

While the previous section broke down the fundamental requirements for correctness, it didn't really explain how correctness problems arise in user environments. Here are some examples compiled from the thesis⁴:

• Dependency identification, compatibility of the software provided with dependency requirements, and location on the system (finding the dependency)
• Implicit environment state: configuration files, an initialized database, system architectures.
• Distinguishing between build time and runtime dependencies.

These problems can be classed into two broader buckets: identification and realization.⁵ I think that identification is more closely related to correctness, in the sense that correctness starts from a correct plan for deploying a software component. However, correct identification is inert without realization, and correctness must be preserved throughout the realization process.

Bonus: Manageability & Usability

The reason that I consider this section a "bonus" is that, by the end of the thesis, manageability isn't really mentioned as much. There are some nice aspects of nix that, in service of correctness, end up improving user experience. Manageability and usability are concerned with the operations associated with software deployment. This effectively amounts to the user experience of the individual trying to orchestrate the deployment. Here are some desiderata mentioned in the thesis⁶:

• Is uninstallation complete and sound: does it remove every artifact of the initial installation while not breaking other software deployments on the system?
• Upgrades should preserve correctness of the system (see DLL hell)
• Upgrade granularity (i.e. upgrade all machines in a network, only upgrade vim on my machine).
• Rolling back upgrades is desirable (requires some form of immutability)
• In order to effectively stay up to date with security upgrades one needs: to know what software is in use, whether updates are available, whether the update should be performed.
• Availability of source distribution vs binary distribution.
• Exposing software variability as configuration options to end users.

Problems With Existing Solutions

In the thesis, Dolstra does an analysis of several existing package management / software deployment systems; low level tools like RPM, Source Deployment Models like FreeBSD Ports and Gentoo, monolithic deployment models like Windows / MacOS. Here is a compiled list of some of the problems one might face on these systems⁷:

• Non-atomic upgrades / inability to rollback.
• Applications must be monolithic and statically contain all dependencies (leads to large bundle sizes, and inflexibility).
• Component composition is manual.
• Adapting components is difficult (i.e. slightly altering configurations like compiling with a different flag).
• The nominal dependency problem; referencing components by name or name and version only.⁸
• Polluted environments lead to interference.⁹
• Incomplete deployment.¹⁰

All of these issues appear in the most widely used operating systems today. When you enumerate the list it's pretty surprising that end users put up with these difficulties. In fact Dolstra comments that the system that comes closest to correct deployment is not actually a classical deployment system but "developer side" Software Configuration Management tools which are basically version control software (like git) with build management integrated.¹¹

The Benefits of Nix

I have often said, when asked to describe Nix, that the single greatest insight of the Nix approach to software deployment is that it gets the "naming" of software right. The thesis offers a much more nuanced perspective on this framing.

The core principles of the Nix deployment approach are to¹²: 1. Isolate components from each other, in a central store. 2. Choose a naming schema (cryptographic hash) that summarizes the semantics of what we mean when we name a component. 3. The semantics of the naming schema need to prevent undeclared dependencies and allow for multiple variants of software to co-exist.

I will try and break these three principles down, but they are extensively interrelated, so it can be difficult to disambiguate them.

The central store is critical for the "realization" of components (as mentioned in the Software Deployment section), it gives us a single place to look to find the dependencies that have already been identified. The isolation of components mitigates against the potential downside of a single store, namely interference.

The naming schema is critical for the "identification" of components. Cryptographic hashes mean that we have a massive collision free namespace to work with, and those hashes can concisely summarize information that we wish to encode in the name.

The semantics of the naming schema is important for ensuring correctness. Since the cryptographic hash is generated from all the inputs (think dependencies) required to build the software, we have a robust notion of equality with which to distinguish components. Additionally, Nix uses this knowledge of all the inputs to ensure that there are no undeclared dependencies at build time.

A notable aside here is that we have mostly been talking about Nix's notion of equality to distinguish components. But it is desirable that we share as many components as possible, and don't need to rebuild components that are equal. So this notion of equality prevents interference, but it can also be used to optimize builds by sharing dependencies across components. In the thesis this is referred to as maximal sharing.¹³

In addition to the core principles, Nix uses a purely functional model where all software in the central store is immutable. This means that it cannot be modified in a breaking way. Nix also prevents side effects in the build process which means that software components are built deterministically. This is important for ensuring that the name (which is based on the inputs to a component) directly corresponds to the output of a build (the actual component).

The Nix approach yields these benefits, which are cited in the thesis as its main contributions¹⁴:

• Complete deployment and non-interference (i.e. correct software deployment)
• Atomic upgrades
• O(1) rollbacks
• Transparent source / binary distribution.¹⁵
• Inefficiencies due to purely functional / immutable model are amortized through optimizations like caching and sharing.
• Nix component language (the language used for expressing software components) makes composition trivial and supports it first class.
• Distributed multi-platform builds; a remote build is indistinguishable from a local build.

These benefits are a great boon to usability, and the principles mentioned earlier in the section ensure correctness. A great illustration of where Nix shines is in managing CI environments, which are notoriously inconsistent.¹⁶

Implementation Details

We had to briefly get into the low level details (cryptographic hashing, immutable build artifacts, centralized store) of Nix's approach to software deployment previous section. This section will expand on those details and try to connect the "how" to the "why".

The Nix Store

How does the Nix store actually work under the hood? It stores software components as directories (named using the hashing schema mentioned before) in a root directory (usually /nix/store). Its worth mentioning that Nix has an extremely weak notion of what constitutes a component; it could be a static configuration file, a compiled binary, source code, a single javascript file that can be interpreted and run¹⁷. As long as it can be stored in a filesystem it is a viable candidate for being a software component. As mentioned before, this naming convention prevents interference and guarantees completeness. We will look at how that works.

Preventing interference

The cryptographic hash for a component is computed based on its inputs. Therefore if components differ in any way at all it will be reflected in the hash. This means that installation or uninstallation will not affect any other components. Since inputs themselves have hashes, and if these hashes change then the hash of the component that depends on the input changes, this means that hashes are effectively computed recursively. Therefore changes to inputs "propagate" through a dependency graph, another way to put it is that changes to transitive dependencies will be reflected in the upstream component.¹⁸

Completeness

Nix guarantees that all dependencies are identified at build time. In other systems, dependencies are usually declared nominally (like RPM) and can be forgotten, or they are passed in dynamically like linking a C module. Since Nix stores components in isolation, there is no way to leverage global namespaces to implicitly provide an input. This means that if you are depending on the presence of a dependency implicitly then the build will just fail.¹⁹

I think this is one of the reasons that nix gets a bad wrap, because it forces you to do things in a principled way and fails early it can seem like it causes friction at first. What seems frustrating at first is really nix giving you feedback that the current approach being taken may fail silently in the future, or just not work in a different environment.

The key to this is that, if a dependency is not explicitly declared, then the component will fail deterministically.²⁰

The cryptographic hash ensures that all build time dependencies are accounted for, but you might be wondering about runtime dependencies. Runtime dependencies will be referenced in the actual component, and will be distinctive since it must reference a Nix Store path (which necessarily contains a high entropy string, a cryptographic hash). Nix can scan for these distinctive strings and keep track of required runtime dependencies. This means that all dependencies for a component are tracked.²¹

The final concept that nix leverages to facilitate complete deployments is called a closure. The closure refers to the entire graph of transitive dependencies tracked for a component. This "closure" is what needs to be provided in order to ensure safe, correct deployment.²² Nix provides a method for computing these closures and handling them in an ergonomic way.

Filesystem As Memory

The "Filesystem as memory" analogy was really impactful on me while reading the Nix thesis. It is a bit unfortunate that going over it will re-state a lot of what we have already covered. However, I think it is worthwhile to examine it to drive home the points about correctness. Additionally it will motivate a concept that is core to nix, and critical for mitigating the space burden of guaranteeing completeness.

This table represents the meat of the analogy. The major upshot of this is that component interference due to file overwriting can be viewed as address collision. Component incompleteness, or "the inability to dereference a pointer" because a file doesn't exist, is the deployment equivalent of a dangling pointer.²³

Understanding how pointers can be dereferenced is critical to preventing dangling pointers, so we will enumerate them below. The examples are in typescript and adapted from the original Java versions in the thesis, the class in the example is called Buildtime to denote that construction of the class represents build time, and there is a method called runtime to denote that the execution of that method represents runtime.²⁴

Obtained and dereferenced at runtime

The filesystem corollary for the code below is similar to acquiring and using a component from the $PATH search path, or as a program argument (maybe passed in via CLI).

class BuildTime {
    constructor(){}

    runtime(y: Bar){
        return y.exec()
    }
}

Obtained and dereferenced at build time

This example cannot cause a dangling pointer because the pointer is dereferenced at build time: similar to static libraries, a compiler, or other things that are not usually retained in the build result.

class BuildTime {
    x: number

    constructor(y: Bar){
        this.x = y.exec()
    }

    runtime(){
        return this.x
    }
}

Obtained at build time, dereferenced at runtime

This example represents Unix style dynamically linked libraries, for example storing the full path of a program in the RPATH of an application binary.

class BuildTime {
    x: Bar

    constructor(y: Bar){
        this.x = y
    }

    runtime(){
        return this.x.exec()
    }
}

These three examples serve to demonstrate how hard it is to ensure that there are no dangling pointers. Pointers may exist at runtime (i.e. in the source) similar to the first example. Pointers may be passed in and dereferenced at build time similar to the second example, but in this case we want to make sure we don't distribute them with the component, since they have already done their job. However, we need to be careful, since some pointers passed in at build time are still required at runtime, like dynamically linked libraries (as shown in the third example). A final consideration is that there is a particularly circumstance were a new pointer is obtained through pointer arithmetic, the filesystem analogy would be to use string manipulation to find a filepath.²⁵

Closures (as mentioned before) are the solution to dangling pointers, by definition they do not contain any.²⁶ But there is another issue, and that is keeping our closures from growing unnecessarily large.

The solution in this case is conservative garbage collection. We have to scan components for potential runtime dereferences, and anything that looks like a valid pointer will be kept. There may be false positives, but that is an acceptable tradeoff. It is unacceptable to have a dangling pointer, considering we want to guarantee correctness. Nix imposes a pointer discipline through its hash-based naming schema which allows pointers to be recognizable within components, and the pointers are isolated from one another within the nix store by virtue of component isolation.²⁷

Purely Functional Model

There are two main facets of Nix that make it a "purely functional" model for software deployment. The first is immutability in the store. The second is purity of the build process; the build process admits no side-effects.

Because the nix store is immutable, it means that there are no destructive upgrades. Upgrading only happens by rebuilding the component and its dependencies. Nix ensures that components never change after they have been built by marking them as "read-only".²⁸

There are many measures taken to ensure that the build process for nix is hermetic. The environment variables are cleared, which means that $PATH is empty. Linux systems use a patched dynamic linker that doesn't search in default locations. $HOME is set to a non-existent folder called "/homless-shelter", so no program can use it for dereferencing via pointer arithmetic (to use the memory analogy).²⁹ Pure builds are important because they mean that each build is deterministic; the inputs to a component (or its dependencies) determine the output.

The combination of immutable store paths and determinism is powerful. It means that the cryptographic hash identifies the contents of a component at all times. Which furnishes Nix with strong correctness guarantees.³⁰

Nix Principles

There were a couple principles mentioned in the thesis, that represent guidelines or patterns for using Nix. I thought it was interesting that a section like this was included, and also really informative for Nix users today.

Static compositions are good

Dynamic composition, or "late binding", is when a dependency is specified at runtime. A composition is when a nix-specified-component is used as the input to the build process for another component. An example of late binding would be this program that references foo dynamically at runtime execlp("foo", args). However, if the path is specified at build time (as Nix enforces), then this is becomes a static composition. Another way of phrasing this, is that Nix will require you to specify foo at build time, and therefore it enforces static compositions.

There is a tradeoff here: dynamic means the ability to upgrade (perhaps fix) everything at once, but it also means the ability to break everything at once. Nix chooses correctness at the cost of expedience.³¹

Static compositions are good. Late compositions are better.

Static composition is obviously expensive, since a component needs to be re-built if any of its dependencies (previous compositions) changes, no matter how small. Late static composition is a technique where a "wrapper component", instead of the program in question, accepts all of the components to be composed as inputs and dynamically links them. A famous example in nixpkgs is firefox, where things like flashplayer and other firefox plugins are linked in the wrapper component, which is really just a shell script that provides the plugins via environment variables. Nix's hermetic environments make this possible without the risk of interference. Since the wrapper component can be generated very quickly, changing a small part of the composition remains cheap.³²

You can still see artifacts of the "wrapping" approach in nixpkgs today; the wrapped firefox component is provided under the name firefox but the unwrapped version still exists as firefox-unwrapped

User environments are not a composition mechanism

User environments can be used as a composition mechanism. This is an abuse of user environments, and should be avoided at all costs. Dependencies should be expressed through Nix as inputs. The abuse of user environments is one of the causes of trouble within existing software deployment systems.³³

Fine-grained components are better than coarse-grained components

Fine grained components are more compositional, they offer better re-use, and they help to mitigate unnecessarily large closures.³⁴

Topics Not Covered

There were many topics that were interesting in the thesis, but were either too technical to write about or there wasn't enough written about them at that point in Nix's history. I will list them here for the interested reader:

Intensional vs extensional model

The extensional model is the Nix that we are used to today, but there is active work on making the intensional model happen. The main difference is the notion of equality. For the extensional model the name (including the hashes) of the inputs are all we care about, but you can have an even more granular definition, where the actual content of the inputs is hashed. This provides greater security guarantees, facilitates optimizing redundant builds, but also makes some other things harder. The intensional model is called content-addressed derivations these days and you can track its progress today

Binary patching

Binary patching is extremely interesting, it offers a solution for reducing the computational overhead of rebuilding large portions of a components dependency graph. It does so, as the name suggest, by applying a patch to the binary of an existing component on disk rather than rebuilding from scratch. The relevant section in the thesis is 7.5.

A language for builders

This is mentioned in future work, and it is definitely something that I find painful today about nix. Bash scripts are not exactly the paragon of correctness. There are however, attempts to provide alternative ways to construct builders by way of altering something called the "standard environment" (which just provides conveniences for making builders and derivations).

A type system for the nix expression language

This is also brought up in the future work section, and there has been lots of interest in this from the community. As far as I can tell there are have been a couple of attempts. The first is nickel which seems to be marketing itself as a general purpose configuration language for more than just nix. The second is purenix which uses the Purescript frontend language, and provides a backend that compiles to nix. While I would love to see either of these succeed, neither has reached critical adoption.

If you would like to comment on this post, the comments section is here

Footnotes