As mentioned in our Tezos Storage / Irmin Summer 2021 Update on the Tezos Agora forum, the Irmin team's goal has been to improve Irmin's performance in order to speed up the Baking Account migration process in Octez, and we managed to make it 10x faster in the first quarter of 2021. Since then, we've been working on a new benchmark program for Irmin that's based on the interactions between Irmin and Octez. This won't just help make Irmin even faster, it will also help speed up the Tezos blockcha…

As mentioned in our Tezos Storage / Irmin Summer 2021 Update on the Tezos Agora forum, the Irmin team's goal has been to improve Irmin's performance in order to speed up the Baking Account migration process in Octez, and we managed to make it 10x faster in the first quarter of 2021. Since then, we've been working on a new benchmark program for Irmin that's based on the interactions between Irmin and Octez. This won't just help make Irmin even faster, it will also help speed up the Tezos blockchain process and enable us to monitor Irmin's behavior in Octez.

Octez is the Tezos node implementation that uses Irmin to store the blockchain state, so Irmin is a core component of Octez that's responsible for virtually all the filesystem operations. Whether a node is launched to produce new blocks (aka “bake”) or just to participate in peer-to-peer sharing of existing blocks, it must first update itself by rebuilding blocks individually until it reaches the head of the blockchain. This first phase is called bootstrapping, and once it reaches the blockchain head, we say it has been bootstrapped. Currently, the bootstrapped phase processes 2 block per minute, which is the rate at which the Tezos blockchain progresses. The next goal is to increase that rate to 12 blocks per minute.

Irmin stores the content of the Tezos blockchain on a disk using the irmin-pack library. There is one-to-one correspondence between the Tezos block and the Irmin commits. Each time Tezos produces a block, Irmin produces a commit, and then the Tezos block hash is computed using the Irmin commit hash. The Irmin developers are working on improving the irmin-pack performance which in turn will improve the performance of Octez.

A benchmark program is considered “fair” when it's representative of how the benchmarked code is used in the real world—for example, the access-patterns to Irmin. A standard database benchmark would first insert random data and then remove it. Such a synthetic benchmark would fail to reproduce the bottlenecks that occur when the insertions and removal are interleaved. Our solution to “fairness” is radical: replaying. Within a sandboxed environment, we replay a real world situation.

Basically, our new benchmark program makes use of a benchmarked code and records statistics for later analysis. The program is stored in the irmin-bench library and makes use of operation traces (called action traces) when Octez runs with Irmin. Later, the program replays the recorded operations one at a time while simultaneously recording tonnes of statistics (called stat traces). Data analysis of the stat traces may reveal many interesting facts about the behaviour of Irmin, especially if we tweak:

• the configuration of Irmin (e.g., what’s the impact of doubling the size of a certain cache?)
• the replay parameters (e.g., does Irmin's performance decay over time? Does irmin-pack perform as well after 24 hours of replay as after 1 minute of replay?)
• the hardware (e.g., does irmin-pack perform well on a Raspberry Pi?)
• the code of Irmin (e.g., does this PR have an impact on performance?)

This benchmarking process is similar to the record-replay feature available with TezEdge.

Recording the Action Trace

By adding logs to Tezos, we can record the Tezos-Irmin interactions and thus capture the Irmin “view” of Tezos. We’ve recorded action traces during the bootstrapping phase of Tezos nodes, which started from Genesis—the name of the very first Tezos block inserted into an empty Irmin store.

The interaction surface between Irmin and Octez is quite simple, so we were able to reduce it to eight (8) elementary operations:

• checkout, to pull an Irmin tree from disk;
• find, mem and mem_tree, read only operations on an Irmin tree;
• add, remove and copy, write only operations on an Irmin tree;
• commit, to push an Irmin tree to disk.

It’s important to remember that Irmin behaves much like Git. It has built-in snapshotting and is compatible with Git itself when using the irmin-git library. In fact, these operations are very similar to Git, too.

Sequence of Operations

To illustrate further, here's a concrete example of an operation sequence inside an action trace:

This shows Octez’s first interaction with Irmin at the very beginning of the blockchain! The first block, Genesis, is quite small (it ends at operation #5), but the second one is massive (it ends at operation #309273). It contains no transactions because it only sets up the entire structure of the tree. It precedes the beginning of Tezos's initial protocol called “Alpha I”.

Benchmark Benefits

Our benchmark results convey the sheer magnitude of the Tezos blockchain and the role that Irmin plays within it. We’ve recorded a trace that covers the blocks from the beginning the blockchain in June 2018 all the way up to May 2021. It weighs 96GB.

Although it took 34 months for Tezos to reach that state, bootstrapping so far takes only 170 hours, and replaying it takes a mere 37 hours on a section of the blockchain that contains 1,343,486 blocks. On average, this corresponds to 1 per minute when the blocks were created, 132 per minute when bootstrapping, and 611 per minute during replay.

On this particular section of the blockchain, Octez had 1,089,853,521 interactions with Irmin. On average, this corresponds to 12 per second when the blocks were created, 1782 per second during bootstrapping, and 8258 per second during replay.

The chart below demonstrates how many of each Irmin operation occur per block (on average):

This next chart displays where the time is spent during replay:

With irmin-pack, an OCaml thread managed by the index library is running concurrently to the main thread (i.e., the merge thread), a fraction of the durations (shown above) are actually spent in that thread. Refer to this blog post for more details on index's merges.

The following chart illustrates how memory usage evolves during replay:

On a logarithmic scale, this last chart shows the evolution of the write amplification, which indicates the amount of rewriting (e.g., at the end of the replay, 20TB of data have been written to disk in order to create a store that weighs 73GB).

The merge operations of the index library are the source of this poor write amplification. The Irmin team is working hard on improving this metric:

• on the one hand, the new structured keys feature of the upcoming Irmin 3.0 release will help to reduce the pressure on the index library,
• on the other hand, we are working on algorithmic improvements of index itself.

Another nice way to use the trace is for testing. When replaying a trace, we can recompute the commit hashes and check that they correspond to the trace hashes, so the benchmark acts as additional tests to ensure we don't compromise the hashes computed in Tezos.

Complex changes to Tezos can be simulated first in Irmin. For example, the path flattening in Tezos feature (merged in August 2021) can now be tested earlier in the process with our benchmark. Prior to the trace benchmarks, we first had to make the changes in Tezos to understand their repercussions on Irmin directly from the Tezos benchmarks.

Lastly, we continue to test alternative libraries and compare them with the ones integrated in Tezos; however, using these alternative libraries to build Tezos nodes has proven to be more complicated than merely adding them in Irmin and running our benchmarks. While testing continues on most new libraries, we can definitely use replays to compare our new cactus library as a replacement for our index library.

Future Directions

While the action trace recording was only made possible on a development branch of Octez, we would next like to upstream the feature to the main branch of Octez, which would give all users the option to record Tezos-Irmin interactions. This would simplify bug reporting overall.

Although the first version only deals with the bootstapping phase of Tezos, an upcoming goal is to make it possible to benchmark the boostrapped phase of Tezos as well. Additionally, we plan to replay the multiprocess aspects of a Tezos node in the near future.

The first stable version of this benchmark has existed in Irmin’s development branch since Q2 2021, and we will release it as part of irmin-bench for Irmin 3.0 in Q4 2021. This release will allow integration into the Sandmark OCaml benchmarking suite.

Follow the Tarides blog for future Irmin updates.

The OCaml typechecker is an important piece of the OCaml compiler pipeline which accounts for a significant portion of time spent on compiling an OCaml program (see the appendices).

The code of the typechecker is also quite optimised, sometime…

The OCaml typechecker is an important piece of the OCaml compiler pipeline which accounts for a significant portion of time spent on compiling an OCaml program (see the appendices).

The code of the typechecker is also quite optimised, sometimes to the detriment of the readability of the code. Recently, Jacques Garrigue and Takafumi Saikawa have worked on a series of pull requests to improve the readability of the typechecker (#10337, #10474, #10541). Unfortunately, those improvements are also expected to increase the typechecking time of OCaml programs because they add abstraction barriers, and remove some optimisations that were breaking the abstraction barriers.

The effect is particularly pronounced on #10337. Due to the improvement of the readability of the typechecker, this pull request has been merged after some quick tests to check that the compilation time increase was not too dire.

However, the discussion on this pull request highlighted the fact that it was difficult to measure OCaml compilation time on a scale large enough to enable good statistical analysis and that it would be useful.

Consequently, I decided to try my hand at a statistical analysis of OCaml compilation time, using this pull request #10337 as a case study. Beyond this specific PR, I think that it is interesting to write down a process and a handful of tools for measuring OCaml compilation time on the opam ecosystem.

Before doing any kind of analysis, the first step is to find an easy way to collect the data of interest. Fortunately, the OCaml compiler can emit timing information with flag -dtimings. However, this information is emitted on stdout, whereas my ideal sampling process would be to just pick an opam package, launch a build process and recover the timing information for each file. This doesn’t work if the data is sent to the stdout, and never see again. This first step is thus to create a version of the OCaml compiler that can output the timing information of the compilation to a specific directory. With this change (#10575), installing an opam package with

OCAMLPARAM=",_,timings=1,dump-dir= /tmp/pkgnname" opam install pkgname

outputs all profiling information to /tmp/pkgname.

This makes it possible to collect large number of data points on compilation times by using opam, and the canonical installation process of each package without the need of much glue code.

For this case study, I am using 5 core packages containers, dune, tyxml, coq and base. Once their dependencies are added, I end up with

• ocamlfind
• num
• zarith
• seq
• containers
• coq
• dune
• re
• ocamlbuild
• uchar
• topkg
• uutf
• tyxml
• sexplib0
• base

Then it is a matter of repeatedly installing those packages, and measuring the compilation times before and after #10337.

In order to get more reliable statistics on each file, each package was compiled 250 times leading to 1,6 millions of data points (available here) after slightly more than a week-end of computation.

In order to try to reduce the noise induced by the operating system scheduler, the compilation process is run with OPAMJOBS=1. Similarly, the compilation process was isolated as much as possible from the other process using the cset Linux utility to reserve one full physical core to the opam processes.

The code for collecting samples, analyzing them, and plotting the graphs below is available at https://github.com/Octachron/ocaml-perfomance-monitoring.

Comparing averages, files by files

With the data at hand, we can compute the average compilation by files, and by stage of the OCaml compiler pipeline. In our case, we are mostly interested in the typechecking stage, and global compilation time, since #10337 should only alter the time spent on typechecking. It is therefore useful to split the compilation time into typechecking + other=total. Then for each files in the 15 packages above, we can can compute the average time for each of those stages and the relative change of average compilation time: time after/time before.

Rendering those relative changes for the typechecking time, file by file (with the corresponding 90% confidence interval) yields

To avoid noise, I have removed files for which the average typechecking time was inferior to one microsecond on the reference version of the compiler.

In the graph above, there are few remarkable points:

• As expected, the average typechecking time increased for almost all files
• A significant portion of points are stuck to the line “after/before=1”. This means that for those files there was no changes at all of the typechecking times.
• The standard deviation time varies wildly across packages. The typechecking of some dune files tend to have a very high variances. However outside of those files, the standard deviation seems moderate, and the mean estimator seem to have converged.
• For a handful a files for which the typechecking time more than doubled. However the relative typechecking time does seem to be confined in the [1,1.2] range for a majority of files.

Since the data is quite noisy, it is useful before trying to interpret it to check that we are not looking only at noise. Fortunately, we have the data on the time spent outside of the typechecking stage available, and those times should be mostly noise. We have thus a baseline, that looks like

This cloud of points look indeed much noisier. More importantly, it seems centred around the line after/before=1. This means that our hypothesis that the compilation time outside of the typechecking stage has not been altered is not visibly invalidated by our data points. An other interesting point is that the high variance points seems to be shared between the typechecking and other graphs.

We can even check on the graphs for the average total compilation (file by file)

that those points still have a high variance here. However, outside of this cluster of points, we have a quite more compact distribution of points for the total compilation time: it seems that we have a quite consistent increase of the total compilation time of around 3%.

And this is reflected in the averages:

There is thus an increase of around 6.6% of typechecking time which translates to an increase of 3.3% of total time. However, the non-typechecking time also increased by 1.7% in average. The average is thus either tainted by some structural bias or the relative variance (mean/ratio) is still enough for the distribution of the ratio to be ill-behaved (literature seems to indicate that a relative variance < 10% is required for the distribution of ratio to be Gaussian-like). Anyway, we probably cannot count on a precision of more than 1.7%. Even with this caveat, we still have a visible effect on the total compilation time.

We might better served by comparing the geometric average. Indeed, we are comparing ratio of time, with possibly a heavy-tailed noise. By using the geometric average (which compute the exponential of the arithmetic mean of the logarithms of our ratio), we can check that rare events don’t have an undue influence on the average. In our case the geometric means looks like

All geometric averages have decreased compared to the arithmetic means, which is a sign that the compilation time distribution is skewed towards high compilation times. However, the changes are small and do not alter our previous interpretation.

We can somewhat refine those observations by looking at the medians (which are even less affected by the heavy-tailness of distributions)

Here, the non-typechecking times seems far less affected by the structural bias (with an increase of 0.9%) whereas the increase of typechecking time and total compilation time are reduced but still here at 3.8% and 2.5% respectively.

Comparing averages, quantiles

We can refine our analysis by looking at the quantiles of those relative changes of compilation time

Here we see that the typechecking time of around 25% of files is simply not affected at all by the changes. And for half of the files, the compilation time is inferior to 9%. Contrarily, there is 1% of files for which the typechecking time increases by more than 50% (with outliers around 200%-400% increase).

However, looking at the total compilation does seems to reduce the overall impact of the change

Indeed, we still have 25% of files not impacted, but for 65% of files the relative increase of compilation time is less than 8%. (and the outliers stalls at a 50% increase)

We can also have a quick look at the quantiles for the non-typechecking time

but here the only curiosity if that the curve is more symmetric and we have 25% of files for which the non-typechecking compilation time decrease randomly.

Noise models and minima

One issue with our previous analysis is the high variance which is observable in the non-typechecking average times across files. A possibility to mitigate this issue is to change our noise model. Using an average, we implicitly assumed that the compilation time was mostly:

observable_compilation_time = theoretical_computation_time + noise

where noise is a random variable with at least a finite variance and a mean of 0. Indeed, with this symmetry hypothesis the expectation of the observable computation time aligns with the theoretical compilation time:

E[observable_computation_time] = E[theoretical_computation_time] + E[noise] = theoretical_computation_time

and the variance Var[observable_computation_time] is exactly the variance of the noise Var[noise]. Then our finite variance hypothesis ensure that the empirical average hypothesis converges relatively well towards the theoretical expectation.

However, we can imagine another noise model with a multiplicative noise (due to CPU scheduling for instance),

observable_compilation_time = scheduling_noise * theoretical_computation_time + noise

with both scheduling_noise>1 and noise>1. With this model, the expectation of the observable compilation time does not match up with the theoretical computation time:

E[observable_computation_time] - theoretical_computation_time =
  (E[scheduling_noise]-1) * theoretical_computation_time + E[noise]

Thus, in this model, the average observable computation time is a structurally biased estimator for the theoretical computation time. This bias might be compensated by the fact that we are only looking to ratio. Nevertheless, this model also induces a second source of variance

Var[observable_computation_time] = theoretical_computation_time^2 Var[scheduling_noise] + Var[noise]

(/assuming the two noises are not correlated), and this variance increases with the theoretical computation time. This relative standard deviation might be problematic when computing ratio.

If this second noise model is closer to reality, using the empirical average estimators might be not ideal. However, the positivity of the noise opens another avenue for estimators: we can consider the minima of a series of independent realisations. Then, we have

min(observable_compilation_time) = min(scheduling_noise * theoretical_computation_time) + min(noise) = theoretical_computation_time

if the min(scheduling_noise)=1 and min(noise)=0.

This model has another advantage: by assuming that the (essential) support of the noise distribution has finite lower bound, we know that the empirical minima will converge towards a three-parameter Weibull distribution with a strictly positive support. (To be completely explicit, we also need to assume some regularity of the distribution around this lower bound too).

This means that the distribution ratio of the empirical minima will not exhibits the infinite moments of the ratio of two Gaussians. Without this issue, our estimator should have less variance.

However, we cannot use Gaussian confidence intervals for the empirical minima. Moreover, estimating the confidence interval for the Weibull distribution is more complex. Since we are mostly interested in corroborating our previous result, we are bypassing the computation of those confidence intervals.

Comparing minima

We can then restart out analysis using the minimal compilation time file-by-file. Starting with the minimal typechecking time, we get

There are notable differences with the average version: - a very significant part of our points takes the same time to typecheck before and after #10337 - there is a discretization effects going on: data points tend to fall on exactly the same value of the ratio

Beyond those changes, there is still a visible general increase of typechecking time.

The same differences are visible for the non typechecking compilation time

and the total compilation time

but overall the minimal total compilation and non-typechecking time mirrors what we had seen with the average. The distribution of the non-typechecking times is maybe more evenly centred around a ratio of 1.

We can have a look at the averages and median (across files) to have more global point of view

A striking change is that the median for the typechecking and total compilation time is equal to one: more than half of files are not affected by the changes when looking at the minimal compilation time. This might be an issue with the granularity of time measurement, or it could be a genuine fact.

More usefully, we still have an increase of average typechecking time between 6% and 6.9% depending on the averaging methods, which translates to a total compilation time increase between 2.7% and 3.3%. And this time, the increase of unrelated compilation time is between 0.7% to 0.9%. This seems to confirms that do have a real increase of average compilation time and 3% increase time is a reasonable number.

Comparing minima, quantiles

With the discretization, the quantiles of the compilation time are quite interesting and uncharacteristic.

For instance the typechecking quantiles,

are stuck to 1 between the first and 50th centile. In other words the minimal typechecking time of more than 50% of the files in our experiment is unchanged. For 40% of the files, the increase is less than 20%. And the most extreme files see only an increase of 100% of the typechecking time. On the higher quantiles, the presence of multiple jumps is the consequence of the discretization of ratio that was already visible on the raw data.

When looking at the time spent outside of typechecking,

we observe that the non-typechecking relation compilation time for more than 80% of file is unaffected by the change (or somehow accelerated for 10% of files).

The quantiles for the total compilation time,

mostly reflects the trends set by the typechecking time: 55% of files are unaffected. For 90% of file the increase is less than 10%, and the maximal impact on the compilation time peaks at a 40% relative increase.

Conclusion

To sum up, with the available data at hands, it seems sensible to conclude that #10337 resulted in an average increase of compilation time of the order of 3%, while the average relative increase of typechecking time is around 6%. Moreover, for the most impacted files (at the ninth decile), the relative increase in compilation time ranges between 10% to 40%.

Appendices

Compilation profile

Since we have data for both typechecking time and non-typechecking times for a few thousand files, it is interesting to check how much time is spent on typechecking. We can start by looking at the data points files by files:

We have here a relatively uniform cloud of points between 20-60% of time spent in typechecking compared to total compilation time. This is is reflected on the average and median

Both value are quite comparable, the distribution doesn’t seem significantly skewed.

However, we have a clear cluster of files for which typechecking accounts for 90% of the total compilation time. Interestingly, this cluster of points corresponds to the dune cluster of files with a very variance that we had identified earlier. This explains why those files have essentially the same profile when looking at the total and typechecking compilation time: in their case, typechecking accounts for most of the work done during compilation.

This relatively uniform distribution is visible both on the quantiles (with an affine part of the quantiles)

and on the histogram of the relative time spent in typechecking

Histograms

Histogram versions for the quantile diagrams are also available. Due to the mixture of continuous and discrete distributions they are not that easy to read. Note that those histograms have equiprobable bins (in other words, constant area) rather than constant width bins.

Average compilation time histograms

An interesting take-away for those histograms is that the typechecking and total compilation time distribution are clearly skewed to the right: with very few exceptions, compilation increases. Contrarily the non-typechecking time distribution is much more symmetric. Since the change here is due to noise, there is no more reason for the compilation time to increase or decrease.

Minimal compilation time histograms

There is no much change when looking at the histogram for the minimal compilation time for a file

The most notable difference is that the non-typechecking histogram is completely dominated by the dirac distribution centred at x=1.

Defining instructions semantics using Primus Lisp (Tutorial)

Introduction

So you found a machine instruction that is not handled by BAP and you wonder how to add it to BAP. This is the tutorial that will gently guide you through the whole process of discovering the instruction, studying its semantics, encoding it, testing, and finally submitting to BAP. The latter is optional but highly appreciated.

In modern BAP, the easiest option is to use Primus Lisp to define new instructions. The idea i…

Defining instructions semantics using Primus Lisp (Tutorial)

Introduction

So you found a machine instruction that is not handled by BAP and you wonder how to add it to BAP. This is the tutorial that will gently guide you through the whole process of discovering the instruction, studying its semantics, encoding it, testing, and finally submitting to BAP. The latter is optional but highly appreciated.

In modern BAP, the easiest option is to use Primus Lisp to define new instructions. The idea is that for each instruction, you describe its effects using Primus Lisp. No recompilation or OCaml coding is required. For example here is the semantics of the tst instruction in the thumb mode taken from BAP,

(defun tTST (rn rm _ _)
  "tst rn, rm"
  (let ((rd (logand rn rm)))
    (set ZF (is-zero rd))
    (set NF (msb rd))))

You now probably have the question: what is tTST and why it has four parameters? We use LLVM (and now Ghidra) as the disassembler backend and when we write a lifter (i.e., when we define the semantics of instructions) we rely on the representation of instructions that are provided by the backend. In LLVM it is MC Instructions, which more or less corresponds to LLVM MIR.

Picking an instruction

So let’s find some ARM instruction that is not yet handled by BAP and use it as a working example. The bap mc command is an ideal companion in writing lifters (mc - stands for machine code), as it lets you work with individual instructions. Besides, I wasn’t able to find any ARM instruction that we do not handle (except co-processors instructions, which are not interesting from the didactic perspective) so we will be working with the thumb2 instruction set. So first of all, we need a binary encoding for the instruction that we would like to lift. If you don’t have one then use llvm-mc (or any other assembler). The encoding (which I found from some wild-caught arm binary is 2d e9 f8 43 and we can disassemble it using bap mc

$ bap mc --arch=thumb --show-insn=asm -- 2d e9 f8 43
push.w {r3, r4, r5, r6, r7, r8, r9, lr}

Or, if we want to go the other way around, from assembly to binary encoding then here is the llvm-mc command-line,

$ echo "push.w {r3, r4, r5, r6, r7, r8, r9, lr}" | llvm-mc -triple=thumb -mattr=thumb2 --show-inst -show-encoding
    .text
    push.w    {r3, r4, r5, r6, r7, r8, r9, lr} @ encoding: [0x2d,0xe9,0xf8,0x43]
                                        @ <MCInst #4118 t2STMDB_UPD
                                        @  <MCOperand Reg:15>
                                        @  <MCOperand Reg:15>
                                        @  <MCOperand Imm:14>
                                        @  <MCOperand Reg:0>
                                        @  <MCOperand Reg:75>
                                        @  <MCOperand Reg:76>
                                        @  <MCOperand Reg:77>
                                        @  <MCOperand Reg:78>
                                        @  <MCOperand Reg:79>
                                        @  <MCOperand Reg:80>
                                        @  <MCOperand Reg:81>
                                        @  <MCOperand Reg:13>>

Now we need to get full information about the instruction name. In BAP, all instruction names are packaged in namespaces to enable multiple backends. To get full information about the instruction encoding and decoding we will use the –show-knowledge option of bap mc. This command-line option will instruct BAP to dump the whole knowledge base, so it will have everything that bap knows so far about the instruction. The property that we’re looking for, is bap:lisp-name and bap:insn. The first will give us the true name and the last will show us how the instruction and operands are represented, e.g.,

$ bap mc --arch=thumb --show-knowledge -- 2d e9 f8 43 | grep lisp-name
   (bap:lisp-name (llvm-thumb:t2STMDB_UPD))
$ bap mc --arch=thumb --show-knowledge -- 2d e9 f8 43 | grep bap:insn
   (bap:insn ((t2STMDB_UPD SP SP 0xe Nil R3 R4 R5 R6 R7 R8 R9 LR)))

Writing the stub semantics

Okay, now we have nearly all the knowledge so we can start writing the semantics. Let’s start with some stub semantics, we will later look into the instruction set manual and learn the instruction semantics, but we want to make sure that BAP loads our files and calls our semantics function.

BAP searches for the semantics file in a number of predefined locations (see bap --help and search for --primus-lisp-semantics option for more details). The default locations include you $HOME/.local/share/bap/primus/semantics and the system-wide location that is usually dependent on your installation (usually it is in an opam switch in <opam-switch>/share/bap/primus/semantics. So you can either place your file in the home location or just pick an arbitrary location and tell bap where to search for it using --bap-primus-semantics=<dir>. In our example, we use the current folder (denoted with . in Unix systems) where we create a file named extra-thumb2.lisp (the name of the file doesn’t really matter for the purposes of example, as long as it has the .lisp extension).

Now, we can create the stub definition of the instruction,

$ cat extra-thumb2.lisp
(defun llvm-thumb:t2STMDB_UPD (_ _ _ _ _ _ _ _ _ _ _ _)
  (msg "yay, it works"))

and let’s check that bap properly dispatches the semantics,

$ bap mc --arch=thumb --primus-lisp-semantics=. --show-bil -- 2d e9 f8 43
yay, it works
{

}

Learning the instruction semantics

So what does this series of _ _ _ _ ... mean? We see that bap applies t2STMDB_UPD as

bap mc --arch=thumb --show-knowledge -- 2d e9 f8 43 | grep bap:insn
   (bap:insn ((t2STMDB_UPD SP SP 0xe Nil R3 R4 R5 R6 R7 R8 R9 LR)))

So it has 12 operands. We haven’t yet learned their semantics so we just ignored them. In Primus Lisp, like in OCaml, you can use the wildcard character as the argument name, if you’re not using it. Now it is time to figure out what do they mean. The encoding of the llvm machine instruction is defined in the LLVM target description (*.td) files, which we can find in the LLVLM GitHub repository, namely, we can learn,

// PUSH/POP aliases for STM/LDM
def : t2InstAlias<"push${p}.w $regs", (t2STMDB_UPD SP, pred:$p, reglist:$regs)>;

So now we know that push.w regs is an alias (syntactic sugar) to stmdb sp!, {r3, r4, r5, r6, r7, r8, r9, lr} (or even stmdb sp!, {r3-r9, lr}. Let’s check that our gues is correct using llvm-mc,

$ echo 'stmdb sp!, {r3-r9, lr}' | llvm-mc -triple=thumb -mattr=thumb2 -show-encoding
    .text
    push.w    {r3, r4, r5, r6, r7, r8, r9, lr} @ encoding: [0x2d,0xe9,0xf8,0x43]

Indeed, the encoding is the same. So now it is time to download an instruction reference and look for the stm instruction. It is on page 357 of the pdf version, in section c2.141, and it says that instruction stores multiple registers. The db suffix is the addressing mode that instructs us to Decrement the address Before each store operation. And the ! suffix (encoded as _UPD in llvm) prescribes us to store the final address back to the destination register. This is a high-level reference intended for asm programmers, so if we need more details with the precisely described semantics we can also look into the ARM Architecture Reference Manual (the pdf file). Here is the semantics obtained from this reference, which is described in the ARM pseudocode,

(I had to screen-shot it, as the indentation matters in their pseudo-code but it could not be copied properly from the pdf file).

Learning Primus Lisp

So we’re now ready to write some lisp code. You may have already skimmed through the Primus Lisp documentation that describes the syntax and semantics of the language. If you didn’t don’t worry (but it is still advised to do this eventually). Primus Lisp is a Lisp dialect that looks much like Common Lisp. Since it is Lisp, it has a very simple syntax - everything is an s-expression, i.e., either an atom, e.g., 1, ‘hello, r0, or an application of a name to a list of arguments, e.g., (malloc 100) or (malloc (sizeof ptr_t)). The semantics of Primus Lisp is very simple as well. Basically, Primus Lisp is a universal syntax for assemblers. There is no other data type than bitvectors. From the perspective of the type system we distinguish bitvectors by their sizes, e.g., 0x1:1 is a one-bitvector with the only bit set to 1 and 0x1:16 is a 16-bitvector which has different size and different value and is a 16-bit word with the lower bit set to 1. All operations evaluate to words and accept words. Now what operations you can use? We can use BAP to get the up-to-date documentation for Primus Lisp. For this we will use the primus-lisp-documentation command (we need to pass the –semantics option as we have two interperters for Primus Lips, one for dynamic execution and another for static execution, which have different libraries and slightly different set of primitives),

bap primus-lisp-documentation --semantics > semantics.org

This command will generate the API documentation in the emacs org-mode. If you don’t want to use Emacs to read this file then you can use pandoc to transform it to any format you like, e.g.,

pandoc semantics.org -o semantics.pdf

That will generate the following document.

Encoding semantics (the first attempt)

Now, after we skimmed through the documentation, let’s make our first ugly (and may be incorrect) attempt to describe the semantics of the instruction,

(defun llvm-thumb:t2STMDB_UPD (dst base _pred _? r1 r2 r3 r4 r5 r6 r7 r8)
  (let ((len 8)
        (stride (sizeof word-width))
        (ptr (- base (* len stride))))
    (store-word (+ ptr (* stride 0)) r1)
    (store-word (+ ptr (* stride 1)) r2)
    (store-word (+ ptr (* stride 2)) r3)
    (store-word (+ ptr (* stride 3)) r4)
    (store-word (+ ptr (* stride 4)) r5)
    (store-word (+ ptr (* stride 5)) r6)
    (store-word (+ ptr (* stride 6)) r7)
    (store-word (+ ptr (* stride 7)) r8)
    (set$ dst ptr)))

and before getting into the details, let’s see how bap translates this semantics to BIL,

$ bap mc --arch=thumb --primus-lisp-semantics=. --show-bil -- 2d e9 f8 43
{
  #3 := SP - 0x20
  mem := mem with [#3, el]:u32 <- R3
  mem := mem with [#3 + 4, el]:u32 <- R4
  mem := mem with [#3 + 8, el]:u32 <- R5
  mem := mem with [#3 + 0xC, el]:u32 <- R6
  mem := mem with [#3 + 0x10, el]:u32 <- R7
  mem := mem with [#3 + 0x14, el]:u32 <- R8
  mem := mem with [#3 + 0x18, el]:u32 <- R9
  mem := mem with [#3 + 0x1C, el]:u32 <- LR
  SP := #3
}

The result looks good and, maybe even correct, but let’s explore the lisp code.

The first thing to notice is that instead of using _ _ ... placeholders we gave each parameter a name. The first parameter is the destination register (it is the llvm rule that all functions that update a register have this register as the first parameter), then we have the base register (in our working example the destination and the base register are the same). Next, we have the _pred which we currently ignore, but will return later. We use the _ prefix to indicate that it is unused. Then there is an operand of unknown purpose, which we denoted as _? (I usually just blank them with _, but this is to show that lisp allows you to use any non-whitespace characters in the identifier). Finally, we have r1 til r8, which binds the passed registers. Here, r1 denotes not the register r1 of ARM but the first register passed to the function, i.e., r3 in our example. (It is to show that you can pick any names for your parameters and that they can even shadow the globally defined target-specific register names, which is probably a bad idea from the readability perspective, choosing something like xN would be probably a better idea).

Now it is time to look into the body of the function. First of all, we used (let (<bindings>) <body>) construct to bind several variables. Each binding has the form (<varN> <exprN>) and it evaluates <exprN> and binds its value to <varN> and make it available for expressions <exprN+1> and in the <body>, e.g., in the full form,

(let ((<var1> <expr1>)
      (<var2> <expr2>)
      ....
      (<varN> <exprN>))
   <body>)

we can use <var1> in <expr2>, ..., <exprN>, and in the <body>, i.e., this is the lexical scope of <var1>. Once the let expression is evaluated <var1> becomes unbound (or bound to whatever it was bound before. In other words, normal lexical scoping, which is totally equivalent to the OCaml,

let var1 = expr1 in
let var2 = expr2 in
...
let varN = exprN in
body

The let-bound variables are reified into temporary variables in BIL. You may also notice that Primus Lisp Semantic compiler is clever enough and removed the constants. Let’s go through the variables.

The first variable is len is a constant equal to 8, which is the number of registers passed to the function. Unfortunately, llvm encodes the 15 registers not with a bitset (as it is actually represented in the instruction) but as a list of operands. So instead of writing one function, we will need to write 15 overloads per each number of registers in the list.

The next variable is also a constant, but we use a complex expression to describe it, (sizeof word-width). The Primus Lisp Semantics Compiler is a meta-interpreter and it computes all values that are known in the static time. As a result, we don’t see this constant in the reified code.

Unleashing the macro power

Now let’s deal with the body. It goes without saying that it is ugly. We have to manually unfold the loop since we don’t have a program variable that denotes the set of registers that we have to store, but instead, llvm represents this instruction as a set of 15 overloads. BAP Primus Lisp supports overloads as well, but we definitely won’t like to write 15 overloads with repetitive code, it is tedious, error-prone, and insults us as programmers.

Here comes the macro system. Primus Lisp employs a very simple macro system based on term rewriting. For each application (foo x y z) the parser looks for a definition of macro foo that has the matching number of parameters. If an exact match is found then (foo x y z) is rewritten with the body of the match. Otherwise, a match with the largest number of parameters is selected and the excess arguments are bound to the last parameter, e.g., if we have

(defmacro foo (x xs) ...)

then it will be called with x bound to a and xs bound to (b c) if applied as (foo a b c), where a, b, c could be arbitrary s-expressions.

The body of the macro may reference itself, i.e., it could be recursive. To illustrate it let’s write the simplest recursive macro that will compute the length of the list,

(defmacro length (r) 1)
(defmacro length (_ rs) (+ 1 (length rs)))

and now we can check that it works by adding

(msg "we have $0 registers" (length r1 r2 r3 r4 r5 r6 r7 r8))

to the body of our definition. It will print,

we have 0x8 registers

Note that macros do not perform any compuations on bitvectors, unlike the Primus meta compiler. The macro engine operates on s-expressions, and (length r1 r2 r3 r4 r5 r6 r7 r8) is rewritten (+ 1 (+ 1 (+ 1 (+ 1 (+ 1 (+ 1 (+ 1 1))))))) on the syntatic level and is later reduced by the Primus Meta Compiler into 8.

To solidify the knowledge and to move forward let’s write a macro store-registers that will take an arbitrary number of registers, e.g., (store-registers base stride off r1 r2 r3 .... rm) which will unfold to a sequence of stores, where each register rN is stored as (store-word (+ base (* stride N)) rN).

First, let’s define the base case of our recursion,

(defmacro store-registers (base stride off reg)
  (store-word (+ base (* stride off)) reg))

and now the recursive case,

(defmacro store-registers (base stride off reg regs)
  (prog
     (store-registers base stride off reg)
     (store-registers base stride (+ off 1) regs)))

Notice, that the body of the macro must be a single s-expression. There is no so-called implicit body and if we need to chain two expressions we have to explicitly use the prog construct. This construct has a very simple semantics, (prog s1 s2 ... sN) means evaluate s1, then s2, and so on until sN and make the result of the whole form equal to the result of the evaluation of the last expression.

And a better representation of the body will be,

(defun llvm-thumb:t2STMDB_UPD (dst base _pred _? r1 r2 r3 r4 r5 r6 r7 r8)
  (let ((len 8)
        (stride (sizeof word-width))
        (ptr (- base (* len stride))))
    (store-registers ptr stride 0 r1 r2 r3 r4 r5 r6 r7 r8)
    (set$ dst ptr)))

And let’s double-check that we still have the same reification to BIL with

$ bap mc --arch=thumb --primus-lisp-semantics=. --show-bil -- 2d e9 f8 43
{
  #3 := SP - 0x20
  mem := mem with [#3, el]:u32 <- R3
  mem := mem with [#3 + 4, el]:u32 <- R4
  mem := mem with [#3 + 8, el]:u32 <- R5
  mem := mem with [#3 + 0xC, el]:u32 <- R6
  mem := mem with [#3 + 0x10, el]:u32 <- R7
  mem := mem with [#3 + 0x14, el]:u32 <- R8
  mem := mem with [#3 + 0x18, el]:u32 <- R9
  mem := mem with [#3 + 0x1C, el]:u32 <- LR
  SP := #3
}

In fact, we can also put into a macro the body of our function, and our length macro will be of use here, e.g.,

(defun llvm-thumb:t2STMDB_UPD (dst base _pred _? r1 r2 r3 r4 r5 r6 r7 r8)
  (stmdb_upd dst base r1 r2 r3 r4 r5 r6 r7 r8))

(defmacro stmdb_upd (dst base regs)
  (let ((len (length regs))
        (stride (sizeof word-width))
        (ptr (- base (* len stride))))
    (store-registers ptr stride 0 regs)
    (set$ dst ptr)))

A side-note on the macro resolution mechanism

A small notice on the macro resolution process. Another way of describing it is that the rewriting engine picks the most specific definition. In fact, this is true for the definitions also. The resolution mechanism collects all definitions for the given name that matches the given context and selects the most specific. The context is defined using the Primus Lisp type class mechanism. The only difference between macros and functions (beyond that macros operate on the syntax tree level) is that macros add the number of arguments (arity) to the context so that the definition with the highest arity is ordered after (have precedence over) all other definitions. This is described more thoroughly in the reference documentation. Another important takeaway for us is that when we write a lifter we end up referencing target-specific functions and registers. So we would like to limit the context of the applicability of our functions to the specified target. (Otherwise, our functions will be loaded and type-checked for all architectures, e.g., when an x86 binary is parsed, and we don’t want this). Therefore, we should start our lifter with the context declaration that will be automatically attached to each definition in the file,

(declare (context (target arm)))

Taming names with namespaces and packages

Now, let’s look into the packages. A package is the Common Lisp (and Lisp in general) name for a namespace. A namespace is just a set of names, and each name in Primus Lisp has a package. In fact, when we write (defmacro stmdb_upd () ...), i.e., without specifying the namespace, the name is automatically prefixed with the current namespace/package. By default, it is the user package. So our definition was read by the Lisp reader as (defmacro user:stmdb_upd ...). It is not only the macro or function names that are packaged. Any identifier is properly namespaced. So that (store-registers ptr stride 0 regs) is read as (user:store-registers user:ptr user:stride 0 user:regs).

The namespaces are also thoroughly described in the documentation but the rendered documentation is outdated because our bot is broken (I really need to fix it), so right now I can only refer you to the sources of the documentation in the mli file. And if you have bap installed in opam, then you can also install odig and odoc and use odig doc bap to generate and read the documentation on your machine. (It will spill an error but just repeat and it will show the correctly rendered documentation, it is a bug upstream that we have reported but… well I have diverged).

what we will do now, we will define the thumb package and llvm-thumb package. The first package will be our working package where we will put all our definitions. And the second package will be specific to llvm,

(defpackage thumb (:use core target arm))
(defpackage llvm-thumb (:use thumb))

(in-package thumb)

The (:use core target arm) stanza means that all definitions in these packages are imported (read “copied”) into the thumb package. And the same for llvm-thumb, basically, (defpackage llvm-thumb (:use thumb)) means copy (export) all definitions from thumb to llvm-thumb.

Both thumb and llvm-thumb packages are already defined in BAP, so we can just say

(in-package thumb)

Unlike Common Lisp, in Primus Lisp, the same package could be defined multiple times and even used before defined. The packages may even mutually import each other. The package system resolves it and finds the least fixed point, but it is probably too much for such a simple tutorial. For us, the main takeaway is that we don’t need to write llvm-thumb and are no longer polluting the namespace with our definitions thanks to packaging and contexts.

The final step, writing overloads

Unfortunately, there is no macro mechanism that will operate on the definition level and generate definitions from some pattern. We probably will develop something for that, but right now for each overload we still need to write a corresponding function, e.g.,

(defun t2STMDB_UPD (dst base _pred _?
                      r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12 r13 r14 r15)
  (stmdb_upd dst base r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12 r13 r14 r15))
....
(defun t2STMDB_UPD (dst base _pred _?
                      r1)
  (stmdb_upd dst base r1))

So that the final version of our code will look like this (see also the gist version)

(declare (context (target arm)))

(in-package thumb)

(defun t2STMDB_UPD (dst base _pred _?
                      r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12 r13 r14 r15)
  (stmdb_upd dst base r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12 r13 r14 r15))

(defun t2STMDB_UPD (dst base _pred _?
                      r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12 r13 r14)
  (stmdb_upd dst base r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12 r13 r14))

(defun t2STMDB_UPD (dst base _pred _?
                      r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12 r13)
  (stmdb_upd dst base r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12 r13))

(defun t2STMDB_UPD (dst base _pred _?
                      r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12)
  (stmdb_upd dst base r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11 r12))

(defun t2STMDB_UPD (dst base _pred _?
                      r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11)
  (stmdb_upd dst base r1 r2 r3 r4 r5 r6 r7 r8 r9 r10 r11))

(defun t2STMDB_UPD (dst base _pred _?
                      r1 r2 r3 r4 r5 r6 r7 r8 r9 r10)
  (stmdb_upd dst base r1 r2 r3 r4 r5 r6 r7 r8 r9 r10))

(defun t2STMDB_UPD (dst base _pred _?
                      r1 r2 r3 r4 r5 r6 r7 r8 r9)
  (stmdb_upd dst base r1 r2 r3 r4 r5 r6 r7 r8 r9))

(defun t2STMDB_UPD (dst base _pred _?
                      r1 r2 r3 r4 r5 r6 r7 r8)
  (stmdb_upd dst base r1 r2 r3 r4 r5 r6 r7 r8))

(defun t2STMDB_UPD (dst base _pred _?
                      r1 r2 r3 r4 r5 r6 r7)
  (stmdb_upd dst base r1 r2 r3 r4 r5 r6 r7))

(defun t2STMDB_UPD (dst base _pred _?
                      r1 r2 r3 r4 r5 r6)
  (stmdb_upd dst base r1 r2 r3 r4 r5 r6))

(defun t2STMDB_UPD (dst base _pred _?
                      r1 r2 r3 r4 r5)
  (stmdb_upd dst base r1 r2 r3 r4 r5))

(defun t2STMDB_UPD (dst base _pred _?
                      r1 r2 r3 r4)
  (stmdb_upd dst base r1 r2 r3 r4))

(defun t2STMDB_UPD (dst base _pred _?
                      r1 r2 r3)
  (stmdb_upd dst base r1 r2 r3))

(defun t2STMDB_UPD (dst base _pred _?
                      r1 r2)
  (stmdb_upd dst base r1 r2))

(defun t2STMDB_UPD (dst base _pred _?
                      r1)
  (stmdb_upd dst base r1))

(defmacro stmdb_upd (dst base regs)
  (let ((len (length regs))
        (stride (sizeof word-width))
        (ptr (- base (* len stride))))
    (store-registers ptr stride 0 regs)
    (set$ dst ptr)))

(defmacro store-registers (base stride off reg)
  (store-word (+ base (* stride off)) reg))

(defmacro store-registers (base stride off reg regs)
  (prog
     (store-registers base stride off reg)
     (store-registers base stride (+ off 1) regs)))

(defmacro length (r) 1)
(defmacro length (_ rs) (+ 1 (length rs)))

I think on this we can conclude our tutorial. I will later polish it, but it covers most of the features of Primus Lisp and writing lifters.

Except for the last step - which is making a PR to BAP with the file. Please, once you wrote a semantics for a machine instruction do not hesitate and PR it to the main repository. It should go to plugins//semantics/, or you can just add the lisp code to an existing lisp file in this folder if you think it would be easier to maintain. This will be highly appreciated.

Happy lifting!

The Bonus Track - Recitation

And as the final accord and recitation, let’s check how we can lift push {r1-r12,r14}.

1) We will use llvm-mc to obtain the binary encoding,

$ echo 'push {r1-r12,r14}' | llvm-mc -triple=thumb -mattr=thumb2 -show-encoding
    .text
    push.w    {r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, lr} @ encoding: [0x2d,0xe9,0xfe,0x5f]

2) next we check that our overload is correctly picked up,

$ bap mc --arch=thumb --primus-lisp-semantics=. --show-bil -- 0x2d,0xe9,0xfe,0x5f
{
  #3 := SP - 0x34
  mem := mem with [#3, el]:u32 <- R1
  mem := mem with [#3 + 4, el]:u32 <- R2
  mem := mem with [#3 + 8, el]:u32 <- R3
  mem := mem with [#3 + 0xC, el]:u32 <- R4
  mem := mem with [#3 + 0x10, el]:u32 <- R5
  mem := mem with [#3 + 0x14, el]:u32 <- R6
  mem := mem with [#3 + 0x18, el]:u32 <- R7
  mem := mem with [#3 + 0x1C, el]:u32 <- R8
  mem := mem with [#3 + 0x20, el]:u32 <- R9
  mem := mem with [#3 + 0x24, el]:u32 <- R10
  mem := mem with [#3 + 0x28, el]:u32 <- R11
  mem := mem with [#3 + 0x2C, el]:u32 <- R12
  mem := mem with [#3 + 0x30, el]:u32 <- LR
  SP := #3
}

So, yay, it works! :)

Last year, Tarides had the honour of winning the “Coup de Coeur” Startup Award at the International Cybersecurity Forum (FIC). It’s the leading cybersecurity event in the EU. It’s both a forum, to present and discuss innovations and reflect on the state of the European cybersecurity ecosystem, and a trade fair, where cybersecurity and other tech professionals can meet and network.

This year, Tarides returns to FIC with their own booth! Our representatives, including founder and CEO of Ta…

Last year, Tarides had the honour of winning the “Coup de Coeur” Startup Award at the International Cybersecurity Forum (FIC). It’s the leading cybersecurity event in the EU. It’s both a forum, to present and discuss innovations and reflect on the state of the European cybersecurity ecosystem, and a trade fair, where cybersecurity and other tech professionals can meet and network.

This year, Tarides returns to FIC with their own booth! Our representatives, including founder and CEO of Tarides, Thomas Gazagnaire, look forward to making new connections, looking for collaborators, and catching up with colleagues.

The FIC theme for 2021 centres on encouraging “a collective and collaborative cybersecurity.” From the FIC Website:

”Collective, because each stakeholder is responsible not only for its own security but also for the security of every other stakeholder, and therefore of the whole. Collaborative, because cooperation and information sharing are essential to compensate the asymmetry between the «attacker» and the «defender»…FIC 2021 will focus on the major operational, industrial, technological, and strategic challenges of cooperation”

Solutions for most cybersecurity issues already exist, and we at Tarides are happy to consult on our many solutions that can make your systems more secure. From secure emails to runtime protection to secure IoT protocols, our representatives can help!

So stop by the Tarides booth at FIC to chat about your options. We’ll have snacks and other goodies, too!

Distributing OCaml software on opam is great (if I dare say so myself), but sometimes you need to provide your tools to an audience outside of the OCaml community, or just without recompilations or in a simpler way.

However, just distributing the locally generated binaries requires that the users have all the needed shared libraries installed, and a compatible libc. It’s not something you can assume in general, and even if you don’t need any C shared library or are confident enough i…

Distributing OCaml software on opam is great (if I dare say so myself), but sometimes you need to provide your tools to an audience outside of the OCaml community, or just without recompilations or in a simpler way.

However, just distributing the locally generated binaries requires that the users have all the needed shared libraries installed, and a compatible libc. It’s not something you can assume in general, and even if you don’t need any C shared library or are confident enough it will be installed everywhere, the libc issue will arise for anyone using a distribution based on a different kind, or a little older than the one you used to build.

There is no built-in support for generating static executables in the OCaml compiler, and it may seem a bit tricky, but it’s not in fact too complex to do by hand, something you may be ready to do for a release that will be published. So here are a few tricks, recipes and advice that should enable you to generate truly portable executables with no external dependency whatsoever. Both Linux and macOS will be treated, but the examples will be based on Linux unless otherwise specified.

Example

I will take as an example a trivial HTTP file server based on Dream.

Sample code

fserv.ml

let () = Dream.(run @@ logger @@ static ".")

fserv.opam

opam-version: "2.0"
depends: ["ocaml" "dream"]

dune-project

(lang dune 2.8)
(name fserv)

The relevant part of our dune file is just:

(executable
  (public_name fserv)
  (libraries dream))

This is how we check the resulting binary:

$ dune build fserv.exe
      ocamlc .fserv.eobjs/byte/dune__exe__Fserv.{cmi,cmo,cmt}
    ocamlopt .fserv.eobjs/native/dune__exe__Fserv.{cmx,o}
    ocamlopt fserv.exe
$ file _build/default/fserv.exe
_build/default/fserv.exe: ELF 64-bit LSB pie executable, x86-64, version 1 (SYSV), dynamically linked, interpreter /lib64/ld-linux-x86-64.so.2, BuildID[sha1]=1991bb9f1d67807411c93f6fb6ec46b4a0ee8ed5, for GNU/Linux 3.2.0, with debug_info, not stripped
$ ldd _build/default/fserv.exe
        linux-vdso.so.1 (0x00007ffe97690000)
        libssl.so.1.1 => /usr/lib/x86_64-linux-gnu/libssl.so.1.1 (0x00007fd6cc636000)
        libcrypto.so.1.1 => /usr/lib/x86_64-linux-gnu/libcrypto.so.1.1 (0x00007fd6cc342000)
        libev.so.4 => /usr/lib/x86_64-linux-gnu/libev.so.4 (0x00007fd6cc330000)
        libpthread.so.0 => /lib/x86_64-linux-gnu/libpthread.so.0 (0x00007fd6cc30e000)
        libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007fd6cc1ca000)
        libdl.so.2 => /lib/x86_64-linux-gnu/libdl.so.2 (0x00007fd6cc1c4000)
        libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007fd6cbffd000)
        /lib64/ld-linux-x86-64.so.2 (0x00007fd6cced7000)

(on macOS, replace ldd with otool -L; dune output is obtained with (display short) in ~/.config/dune/config)

So let’s see how to change this result. Basically, here, libev, libssl and libcrypto are required shared libraries that may not be installed on every system, while all the others are part of the core system:

• linux-vdso, libdl and ld-linux are concerned with the dynamic loading of shared objects ;
• libm and libpthread are extensions of the core libc that are tightly bound to it, and always installed.

Statically linking the libraries

In simple cases, static linking can be turned on as easily as passing the -static flag to the C compiler: through OCaml you will need to pass -cclib -static. We can add that to our dune file:

(executable
  (public_name fserv)
  (flags (:standard -cclib -static))
  (libraries dream))

… which gives:

$ dune build fserv.exe
      ocamlc .fserv.eobjs/byte/dune__exe__Fserv.{cmi,cmo,cmt}
    ocamlopt .fserv.eobjs/native/dune__exe__Fserv.{cmx,o}
    ocamlopt fserv.exe
/usr/bin/ld: /usr/lib/gcc/x86_64-linux-gnu/10/../../../x86_64-linux-gnu/libcrypto.a(dso_dlfcn.o): in function `dlfcn_globallookup':
(.text+0x13): warning: Using 'dlopen' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
/usr/bin/ld: ~/.opam/4.11.0/lib/ocaml/libunix.a(initgroups.o): in function `unix_initgroups':
initgroups.c:(.text.unix_initgroups+0x1f): warning: Using 'initgroups' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
[...]
$ file _build/default/fserv.exe 
_build/default/fserv.exe: ELF 64-bit LSB executable, x86-64, version 1 (GNU/Linux), statically linked, BuildID[sha1]=9ee3ae1c24fbc291d1f580bc7aaecba2777ee6c2, for GNU/Linux 3.2.0, with debug_info, not stripped
$ ldd _build/default/fserv.exe
        not a dynamic executable

The executable was generated… and the result seems OK, but we shouldn’t skip all these ld warnings. Basically, what ld is telling us is that you shouldn’t statically link glibc (it internally uses dynlinking, to libraries that also need glibc functions, and will therefore still need to dynlink a second version from the system ).

Indeed here, we have been statically linking a dynamic linking engine, among other things. Don’t do it.

Linux solution: linking with musl instead of glibc

The easiest workaround at this point, on Linux, is to compile with musl, which is basically a glibc replacement that can be statically linked. There are some OCaml and gcc variants to automatically use musl (comments welcome if you have been successful with them!), but I have found the simplest option is to use a tiny Alpine Linux image through a Docker container. Here we’ll use OCamlPro’s minimal Docker images but anything based on musl should do.

$ docker run --rm -it ocamlpro/ocaml:4.12
[...]
~/fserv $ sudo apk add openssl-libs-static
(1/1) Installing openssl-libs-static (1.1.1l-r0)
OK: 161 MiB in 52 packages
~/fserv $ opam switch create . --deps ocaml-system
[...]
~/fserv $ eval $(opam env)
~/fserv $ dune build fserv.exe
~/fserv $ file _build/default/fserv.exe
_build/default/fserv.exe: ELF 64-bit LSB pie executable, x86-64, version 1 (SYSV), dynamically linked, with debug_info, not stripped
~/fserv $ ldd _build/default/fserv.exe
        /lib/ld-musl-x86_64.so.1 (0x7ff41353f000)

Almost there! We see that we had to install extra packages with apk add: the static libraries might not be already installed and in this case are in a separate package (you would get bin/ld: cannot find -lssl). The last remaining dynamic loader in the output of ldd is because static PIE executable were not supported until recently. To get rid of it, we just need to add -cclib -no-pie (note: a previous revision of this blogpost mentionned -static-pie instead, which may work with recent compilers, but didn’t seem to give reliable results):

(executable
  (public_name fserv)
  (flags (:standard -cclib -static -cclib -no-pie))
  (libraries dream))

And we are good!

~/fserv $ file _build/default/fserv.exe
_build/default/fserv.exe: ELF 64-bit LSB executable, x86-64, version 1 (SYSV), statically linked, with debug_info, not stripped
~/fserv $ ldd _build/default/fserv.exe
/lib/ld-musl-x86_64.so.1: _build/default/fserv.exe: Not a valid dynamic program

Trick: short script to compile through a Docker container

Passing the context to a Docker container and getting the artefacts back can be bothersome and often causes file ownership issues, so I use the following snippet to pipe them to/from it using tar:

git ls-files -z | xargs -0 tar c | \
docker run --rm -i ocamlpro/ocaml:4.12 \
  sh -uexc \
    '{ tar x &&
       opam switch create . ocaml-system --deps-only --locked &&
       opam exec -- dune build --profile=release @install;
     } >&2 && tar c -hC _build/install/default/bin .' | \
tar vx

The other cases: turning to manual linking

Sometimes you can’t use the above: the automatic linking options may need to be tweaked for static libraries, your app may still need dynlinking support at some point, or you may not have the musl option. On macOS, for example, the libc doesn’t have a static version at all (and the -static option of ld is explicitely “only used building the kernel”). Let’s get our hands dirty and see how to use a mixed static/dynamic linking scheme. First, we examine how OCaml does the linking usually:

The linking options are passed automatically by OCaml, using information that is embedded in the cm(x)a files, for example:

$ ocamlobjinfo $(opam var lwt:lib)/unix/lwt_unix.cma |head
File ~/.opam/4.11.0/lib/lwt/unix/lwt_unix.cma
Force custom: no
Extra C object files: -llwt_unix_stubs -lev -lpthread
Extra C options:
Extra dynamically-loaded libraries: -llwt_unix_stubs
Unit name: Lwt_features
Interfaces imported:
        c21c5d26416461b543321872a551ea0d        Stdlib
        1372e035e54f502dcc3646993900232f        Lwt_features
        3a3ca1838627f7762f49679ce0278ad1        CamlinternalFormatBasics

Now the linking flags, here -llwt_unix_stubs -lev -lpthread let the C compiler choose the best way to link; in the case of stubs, they will be static (using the .a files — unless you make special effort to use dynamic ones), but -lev will let the system linker select the shared library, because it is generally preferred. Gathering these flags by hand would be tedious: my preferred trick is to just add the -verbose flag to OCaml (for the lazy, you can just set — temporarily — OCAMLPARAM=_,verbose=1):

(executable
  (public_name fserv)
  (flags (:standard -verbose))
  (libraries dream))

$ dune build
      ocamlc .fserv.eobjs/byte/dune__exe__Fserv.{cmi,cmo,cmt}
    ocamlopt .fserv.eobjs/native/dune__exe__Fserv.{cmx,o}
+ as  -o '.fserv.eobjs/native/dune__exe__Fserv.o' '/tmp/build8eb7e5.dune/camlasm91a0b9.s'
    ocamlopt fserv.exe
+ as  -o '/tmp/build8eb7e5.dune/camlstartupc9267f.o' '/tmp/build8eb7e5.dune/camlstartup1d9915.s'
+ gcc -O2 -fno-strict-aliasing -fwrapv -Wall -Wdeclaration-after-statement -fno-common -fexcess-precision=standard -fno-tree-vrp -ffunction-sections -D_FILE_OFFSET_BITS=64 -D_REENTRANT -DCAML_NAME_SPACE  -Wl,-E -o 'fserv.exe'  '-L~/.opam/4.11.0/lib/bigstringaf' '-L~/.opam/4.11.0/lib/ocaml' '-L~/.opam/4.11.0/lib/ocaml' '-L~/.opam/4.11.0/lib/ocaml' '-L~/.opam/4.11.0/lib/lwt/unix' '-L~/.opam/4.11.0/lib/cstruct' '-L~/.opam/4.11.0/lib/mirage-crypto' '-L~/.opam/4.11.0/lib/mirage-crypto-rng/unix' '-L~/.opam/4.11.0/lib/mtime/os' '-L~/.opam/4.11.0/lib/digestif/c' '-L~/.opam/4.11.0/lib/bigarray-overlap/stubs' '-L~/.opam/4.11.0/lib/ocaml' '-L~/.opam/4.11.0/lib/ssl' '-L~/.opam/4.11.0/lib/ocaml'  '/tmp/build8eb7e5.dune/camlstartupc9267f.o' '~/.opam/4.11.0/lib/ocaml/std_exit.o' '.fserv.eobjs/native/dune__exe__Fserv.o' '~/.opam/4.11.0/lib/dream/dream.a' '~/.opam/4.11.0/lib/dream/sql/dream__sql.a' '~/.opam/4.11.0/lib/dream/http/dream__http.a' '~/.opam/4.11.0/lib/dream/websocketaf/websocketaf.a' '~/.opam/4.11.0/lib/dream/httpaf-lwt-unix/httpaf_lwt_unix.a' '~/.opam/4.11.0/lib/dream/httpaf-lwt/httpaf_lwt.a' '~/.opam/4.11.0/lib/dream/h2-lwt-unix/h2_lwt_unix.a' '~/.opam/4.11.0/lib/dream/h2-lwt/h2_lwt.a' '~/.opam/4.11.0/lib/dream/h2/h2.a' '~/.opam/4.11.0/lib/psq/psq.a' '~/.opam/4.11.0/lib/dream/httpaf/httpaf.a' '~/.opam/4.11.0/lib/dream/hpack/hpack.a' '~/.opam/4.11.0/lib/dream/gluten-lwt-unix/gluten_lwt_unix.a' '~/.opam/4.11.0/lib/lwt_ssl/lwt_ssl.a' '~/.opam/4.11.0/lib/ssl/ssl.a' '~/.opam/4.11.0/lib/dream/gluten-lwt/gluten_lwt.a' '~/.opam/4.11.0/lib/faraday-lwt-unix/faraday_lwt_unix.a' '~/.opam/4.11.0/lib/faraday-lwt/faraday_lwt.a' '~/.opam/4.11.0/lib/dream/gluten/gluten.a' '~/.opam/4.11.0/lib/faraday/faraday.a' '~/.opam/4.11.0/lib/dream/localhost/dream__localhost.a' '~/.opam/4.11.0/lib/dream/graphql/dream__graphql.a' '~/.opam/4.11.0/lib/ocaml/str.a' '~/.opam/4.11.0/lib/graphql-lwt/graphql_lwt.a' '~/.opam/4.11.0/lib/graphql/graphql.a' '~/.opam/4.11.0/lib/graphql_parser/graphql_parser.a' '~/.opam/4.11.0/lib/re/re.a' '~/.opam/4.11.0/lib/dream/middleware/dream__middleware.a' '~/.opam/4.11.0/lib/yojson/yojson.a' '~/.opam/4.11.0/lib/biniou/biniou.a' '~/.opam/4.11.0/lib/easy-format/easy_format.a' '~/.opam/4.11.0/lib/magic-mime/magic_mime_library.a' '~/.opam/4.11.0/lib/fmt/fmt_tty.a' '~/.opam/4.11.0/lib/multipart_form/lwt/multipart_form_lwt.a' '~/.opam/4.11.0/lib/dream/pure/dream__pure.a' '~/.opam/4.11.0/lib/hmap/hmap.a' '~/.opam/4.11.0/lib/multipart_form/multipart_form.a' '~/.opam/4.11.0/lib/rresult/rresult.a' '~/.opam/4.11.0/lib/pecu/pecu.a' '~/.opam/4.11.0/lib/prettym/prettym.a' '~/.opam/4.11.0/lib/bigarray-overlap/overlap.a' '~/.opam/4.11.0/lib/bigarray-overlap/stubs/overlap_stubs.a' '~/.opam/4.11.0/lib/base64/rfc2045/base64_rfc2045.a' '~/.opam/4.11.0/lib/unstrctrd/parser/unstrctrd_parser.a' '~/.opam/4.11.0/lib/unstrctrd/unstrctrd.a' '~/.opam/4.11.0/lib/uutf/uutf.a' '~/.opam/4.11.0/lib/ke/ke.a' '~/.opam/4.11.0/lib/fmt/fmt.a' '~/.opam/4.11.0/lib/base64/base64.a' '~/.opam/4.11.0/lib/digestif/c/digestif_c.a' '~/.opam/4.11.0/lib/stdlib-shims/stdlib_shims.a' '~/.opam/4.11.0/lib/dream/graphiql/dream__graphiql.a' '~/.opam/4.11.0/lib/dream/cipher/dream__cipher.a' '~/.opam/4.11.0/lib/mirage-crypto-rng/lwt/mirage_crypto_rng_lwt.a' '~/.opam/4.11.0/lib/mtime/os/mtime_clock.a' '~/.opam/4.11.0/lib/mtime/mtime.a' '~/.opam/4.11.0/lib/duration/duration.a' '~/.opam/4.11.0/lib/mirage-crypto-rng/unix/mirage_crypto_rng_unix.a' '~/.opam/4.11.0/lib/mirage-crypto-rng/mirage_crypto_rng.a' '~/.opam/4.11.0/lib/mirage-crypto/mirage_crypto.a' '~/.opam/4.11.0/lib/eqaf/cstruct/eqaf_cstruct.a' '~/.opam/4.11.0/lib/eqaf/bigstring/eqaf_bigstring.a' '~/.opam/4.11.0/lib/eqaf/eqaf.a' '~/.opam/4.11.0/lib/cstruct/cstruct.a' '~/.opam/4.11.0/lib/caqti-lwt/caqti_lwt.a' '~/.opam/4.11.0/lib/lwt/unix/lwt_unix.a' '~/.opam/4.11.0/lib/ocaml/threads/threads.a' '~/.opam/4.11.0/lib/ocplib-endian/bigstring/ocplib_endian_bigstring.a' '~/.opam/4.11.0/lib/ocplib-endian/ocplib_endian.a' '~/.opam/4.11.0/lib/mmap/mmap.a' '~/.opam/4.11.0/lib/ocaml/bigarray.a' '~/.opam/4.11.0/lib/ocaml/unix.a' '~/.opam/4.11.0/lib/logs/logs_lwt.a' '~/.opam/4.11.0/lib/lwt/lwt.a' '~/.opam/4.11.0/lib/caqti/caqti.a' '~/.opam/4.11.0/lib/uri/uri.a' '~/.opam/4.11.0/lib/angstrom/angstrom.a' '~/.opam/4.11.0/lib/bigstringaf/bigstringaf.a' '~/.opam/4.11.0/lib/bigarray-compat/bigarray_compat.a' '~/.opam/4.11.0/lib/stringext/stringext.a' '~/.opam/4.11.0/lib/ptime/ptime.a' '~/.opam/4.11.0/lib/result/result.a' '~/.opam/4.11.0/lib/logs/logs.a' '~/.opam/4.11.0/lib/ocaml/stdlib.a' '-lssl_stubs' '-lssl' '-lcrypto' '-lcamlstr' '-loverlap_stubs_stubs' '-ldigestif_c_stubs' '-lmtime_clock_stubs' '-lrt' '-lmirage_crypto_rng_unix_stubs' '-lmirage_crypto_stubs' '-lcstruct_stubs' '-llwt_unix_stubs' '-lev' '-lpthread' '-lthreadsnat' '-lpthread' '-lunix' '-lbigstringaf_stubs' '~/.opam/4.11.0/lib/ocaml/libasmrun.a' -lm -ldl

There is a lot of noise, but the interesting part is at the end, the -l* options before the standard ocaml/libasmrun -lm -ldl:

  '-lssl_stubs' '-lssl' '-lcrypto' '-lcamlstr' '-loverlap_stubs_stubs' '-ldigestif_c_stubs' '-lmtime_clock_stubs' '-lrt' '-lmirage_crypto_rng_unix_stubs' '-lmirage_crypto_stubs' '-lcstruct_stubs' '-llwt_unix_stubs' '-lev' '-lpthread' '-lthreadsnat' '-lpthread' '-lunix' '-lbigstringaf_stubs'

Manually linking with glibc (Linux)

To link these statically, but the glibc dynamically:

• we disable the automatic generation of linking flags by OCaml with -noautolink
• we pass directives to the linker through OCaml and the C compiler, using -cclib -Wl,xxx. -Bstatic makes static linking the preferred option
• we escape the linking flags we extracted above through -cclib

(executable
  (public_name fserv)
  (flags (:standard
          -noautolink
          -cclib -Wl,-Bstatic
          -cclib -lssl_stubs                    -cclib -lssl
          -cclib -lcrypto                       -cclib -lcamlstr
          -cclib -loverlap_stubs_stubs          -cclib -ldigestif_c_stubs
          -cclib -lmtime_clock_stubs            -cclib -lrt
          -cclib -lmirage_crypto_rng_unix_stubs -cclib -lmirage_crypto_stubs
          -cclib -lcstruct_stubs                -cclib -llwt_unix_stubs
          -cclib -lev                           -cclib -lthreadsnat
          -cclib -lunix                         -cclib -lbigstringaf_stubs
          -cclib -Wl,-Bdynamic
          -cclib -lpthread))
  (libraries dream))

Note that -lpthread and -lm are tightly bound to the libc and can’t be static in this case, so we moved -lpthread to the end, outside of the static section. The part between the -Bstatic and the -Bdynamic is what will be statically linked, leaving the defaults and the libc dynamic. Result:

$ dune build fserv.exe && ldd _build/default/fserv.exe
      ocamlc .fserv.eobjs/byte/dune__exe__Fserv.{cmi,cmo,cmt}
    ocamlopt .fserv.eobjs/native/dune__exe__Fserv.{cmx,o}
    ocamlopt fserv.exe
$ file _build/default/fserv.exe
_build/default/fserv.exe: ELF 64-bit LSB pie executable, x86-64, version 1 (SYSV), dynamically linked, interpreter /lib64/ld-linux-x86-64.so.2, BuildID[sha1]=31c93085284da5d74002218b1d6b61c0efbdefe4, for GNU/Linux 3.2.0, with debug_info, not stripped
$ ldd _build/default/fserv.exe
        linux-vdso.so.1 (0x00007ffe207c5000)
        libpthread.so.0 => /lib/x86_64-linux-gnu/libpthread.so.0 (0x00007f49d5e56000)
        libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007f49d5d12000)
        libdl.so.2 => /lib/x86_64-linux-gnu/libdl.so.2 (0x00007f49d5d0c000)
        libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007f49d5b47000)
        /lib64/ld-linux-x86-64.so.2 (0x00007f49d69bf000)

The remaining are the base of the dynamic linking / shared object systems, but we got away with libssl, libcrypto and libev, which were the ones possibly absent from target systems. The resulting executable should work on any glibc-based Linux distribution that is recent enough; on older ones you will likely get missing GLIBC symbols.

If you need to distribute that way, it’s a good idea to compile on an old release (like Debian ‘oldstable’ or ‘oldoldstable’) for maximum portability.

Manually linking on macOS

Unfortunately, the linker on macOS doesn’t seem to have options to select the static versions of the libraries; the only solution is to get our hands even dirtier, and link directly to the .a files, instead of using -l arguments.

Most of the flags just link with stubs, we can keep them as is: -lssl_stubs -lcamlstr -loverlap_stubs_stubs -ldigestif_c_stubs -lmtime_clock_stubs -lmirage_crypto_rng_unix_stubs -lmirage_crypto_stubs -lcstruct_stubs -llwt_unix_stubs -lthreadsnat -lunix -lbigstringaf_stubs

That leaves us with: -lssl -lcrypto -lev -lpthread

• lpthread is built-in, we can ignore it
• for the others, we need to lookup the .a file: I use e.g.

  $ echo $(pkg-config libssl --variable libdir)/libssl.a
  ~/brew/Cellar/openssl@1.1/1.1.1k/lib/libcrypto.a
  

Of course you don’t want to hardcode these paths, but let’s test for now:

(executable
  (public_name fserv)
  (flags (:standard
          -noautolink
          -cclib -lssl_stubs           -cclib -lcamlstr
          -cclib -loverlap_stubs_stubs -cclib -ldigestif_c_stubs
          -cclib -lmtime_clock_stubs   -cclib -lmirage_crypto_rng_unix_stubs
          -cclib -lmirage_crypto_stubs -cclib -lcstruct_stubs
          -cclib -llwt_unix_stubs      -cclib -lthreadsnat
          -cclib -lunix                -cclib -lbigstringaf_stubs
          -cclib ~/brew/Cellar/openssl@1.1/1.1.1k/lib/libssl.a
          -cclib ~/brew/Cellar/openssl@1.1/1.1.1k/lib/libcrypto.a
          -cclib ~/brew/Cellar/libev/4.33/lib/libev.a))
  (libraries dream))

$ dune build fserv.exe
      ocamlc .fserv.eobjs/byte/dune__exe__Fserv.{cmi,cmo,cmt}
    ocamlopt .fserv.eobjs/native/dune__exe__Fserv.{cmx,o}
    ocamlopt fserv.exe
$ file _build/default/fserv.exe
_build/default/fserv.exe: Mach-O 64-bit executable x86_64
$ otool -L _build/default/fserv.exe
_build/default/fserv.exe:
        /usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1292.60.1)

This is as good as it will get!

Cleaning up the build system

We have until now been adding the linking flags manually in the dune file; you probably don’t want to do that and be restricted to static builds only! Not counting the non-portable link options we have been using…

The quick&dirty way

Don’t use this in your build system! But for quick testing you can conveniently pass flags to the OCaml compilers using the OCAMLPARAM variable. Combined with the tar/docker snippet above, we get a very simple static-binary generating command:

git ls-files -z | xargs -0 tar c | \
docker run --rm -i ocamlpro/ocaml:4.12 \
  sh -uexc '{
    tar x &&
    sudo apk add openssl-libs-static &&
    opam switch create . ocaml-system --deps-only --locked &&
    OCAMLPARAM=_,cclib=-static,cclib=-no-pie opam exec -- dune build --profile=release @install;
  } >&2 && tar c -hC _build/install/default/bin .' | \
tar vx

Note that, for releases, you may also want to strip the generated binaries.

Making it an option of the build system (with dune)

For something you will want to commit, I recommend to generate the flags in a separate file linking-flags-fserv.sexp:

(executable
  (public_name fserv)
  (flags (:standard (;include linking-flags-fserv.sexp)))
  (libraries dream))

The linking flags will depend on the chosen linking mode and on the OS. For the OS, it’s easiest to generate them through a script ; for the linking mode, I use an environment variable to optionally turn static linking on.

(rule
  (with-stdout-to linking-flags-fserv.sexp
    (run ./gen-linking-flags.sh %{env:LINKING_MODE=dynamic} %{ocaml-config:system})))

This will use the following gen-linking-flags.sh script to generate the file, passing it the value of $LINKING_MODE and defaulting to dynamic. Doing it this way also ensures that dune will properly recompile when the value of the environment variable changes.

#!/bin/sh
set -ue

LINKING_MODE="$1"
OS="$2"
FLAGS=
CCLIB=

case "$LINKING_MODE" in
    dynamic)
        ;; # No extra flags needed
    static)
        case "$OS" in
            linux) # Assuming Alpine here
                CCLIB="-static -no-pie";;
            macosx)
                FLAGS="-noautolink"
                CCLIB="-lssl_stubs -lcamlstr -loverlap_stubs_stubs
                       -ldigestif_c_stubs -lmtime_clock_stubs
                       -lmirage_crypto_rng_unix_stubs -lmirage_crypto_stubs
                       -lcstruct_stubs -llwt_unix_stubs -lthreadsnat -lunix
                       -lbigstringaf_stubs"
                LIBS="libssl libcrypto libev"
                for lib in $LIBS; do
                    CCLIB="$CCLIB $(pkg-config $lib --variable libdir)/$lib.a"
                done;;
            *)
                echo "No known static compilation flags for '$OS'" >&2
                exit 1
        esac;;
    *)
        echo "Invalid linking mode '$LINKING_MODE'" >&2
        exit 2
esac

echo '('
for f in $FLAGS; do echo "  $f"; done
for f in $CCLIB; do echo "  -cclib $f"; done
echo ')'

Then you’ll only have to run LINKING_MODE=static dune build fserv.exe to generate the static executable (wrapped in the Docker script above, in the case of Alpine), and can include that in your CI as well.

For real-world examples, you can check learn-ocaml or opam.

Related topics

• reproducible builds should be a goal when you intend to distribute pre-compiled binaries.
• opam-bundle is a different, heavy-weight approach to distributing opam software to non-OCaml developers, that retains the “compile all from source” policy but provides one big package that bootstraps OCaml, opam and all the dependencies with a single command.

Regular CI systems are optimised for workloads that do not require stable performance over time. This makes them unsuitable for running performance benchmarks.

current-bench provides a predictable environment for performance benchmarks and a UI for analysing results over time. Similar to a CI system, it runs on pull requests and branches which allows performance to be analysed and compared. It can currently be enabled as an app on GitHub repositories with zero configuration. Several public repo…

Regular CI systems are optimised for workloads that do not require stable performance over time. This makes them unsuitable for running performance benchmarks.

current-bench provides a predictable environment for performance benchmarks and a UI for analysing results over time. Similar to a CI system, it runs on pull requests and branches which allows performance to be analysed and compared. It can currently be enabled as an app on GitHub repositories with zero configuration. Several public repositories are runningcurrent-bench, including Irmin and Dune. We plan to enable it on more projects in the future.

In this article, we give a technical overview of current-bench, showing how results are collected and analysed, requirements for using it and how we built the infrastructure for stable benchmarks. We also describe future work that would allow more OCaml projects to run current-bench.

Introduction

For performance critical software, we must run benchmarks to ensure that there's no regression. Running benchmarks before the user submits their pull request is tedious, and since every user might have a different machine, you can't be sure if the benchmarks performed actually improved or regressed performance.

Our current-bench aims to solve this problem by providing a stable benchmarking platform that runs every time the user submits a pull request and compares the result to the benchmarks on the main branch. As current-bench is zero-configuration, users can enroll their repository to run benchmarks with ease. This current-bench has helped projects ensure that regression doesn't happen, so you can merge code with more confidence.

Architecture

Benchmarking Pipeline

As shown in Figure 1 (above), the benchmarking infrastructure uses ocurrent¹, an embedded Domain Specific Language to write a pipeline. The ocurrent command computes the build incrementally and helps with static analysis. Whenever a pull request is opened on a repository monitored by current-bench, a POST request is sent to the server running the pipeline. The pipeline fetches the head commit on the pull request and uses Docker to compile the code, and then it runs the make bench command inside the generated Docker image.

The pipeline runs on a single node, and the process is pinned to a single core to ensure there's no contention of resources when running the benchmarks. Once finished, the raw JSON result is stored in a Postgres database, which the frontend can query using a GraphQL API, as shown in Figure 2 below.

The frontend supports historical navigation and provides comparison with the default branch. It allows users to select a pull request of which they want to see the graphs. The graphs display the individual result of the head commit and the comparison with the commits on the default branch. The frontend permits users to select the historical interval when they want to compare benchmarks, and it also shows the standard deviation. Once the benchmarks have run successfully, the pipeline sets the pull request status to the frontend URL. Then the user can look at the graphs.

Hardware Optimisation

Our current-bench uses the hardware optimisations developed for OCaml multicore compiler benchmarks (presented at ICFP OCaml Workshop 2019) with a few modifications to allow the benchmarks to run inside Docker containers. To get stable performance, we configured the kernel to isolate some of the CPU cores. Linux then avoids scheduling other user processes automatically. We also disabled IRQ handling and power saving.

The container that runs the benchmark is pinned to one of the isolated cores. Since I/O operations can make the benchmarks less stable, we use an in-memory tmpfs partition in /dev/shm for all storage. For NUMA enabled systems, we configure this partition to be allocated on the NUMA node of the isolated core. The pipeline disables ASLR inside the container automatically, which is normally blocked by the default Docker seccomp profile, so we have modified the profile to allow the personality(2) syscall.

Enrolling a repository

To enroll a repository, you need to ensure the following:

• Enable the ocaml-benchmarks GitHub app for your repository.
• The repository needs a bench Makefile target. This is triggered from the current-bench pipeline.
• The output of the make bench target is JSON, which can be parsed by the pipeline and displayed by the frontend.

Future work

Anyone who wants to roll out a continuous, zero-configured benchmarking infrastructure can set up the current-bench infrastructure. In the future, we want to scale current-bench by isolating cores on multiple machines and adding a scheduler to ensure that benchmarks use only one core at a time per machine. We plan to add support for different benchmarking libraries that repositories can use—for example, we currently support repositories using bechamel. We also aim to make the adoption of current-bench easier by adding a conversion library that can convert any benchmark output into output parseable by current-bench. We intend to add support for quick and slow benchmarks, which would allow users to have faster feedback loops on pull requests while ensuring they can still run more extensive, time consuming benchmarks to see the performance.

Thank you for reading! You can check out the implementation for current-bench here!

This year marks the 25th anniversary of the OCaml Language! It's an exciting time for OCaml programmers and enthusiasts. A fun and informative way to celebrate OCaml's birthday is to attend the 26th Annual International Conference on Functional Programming (ICFP), held online this year due to ongoing Covid restrictions. While this is disappointing news for so many, it's beneficial to those of you outside France because now you can hear professionals talk about cutting edge technology from the co…

This year marks the 25th anniversary of the OCaml Language! It's an exciting time for OCaml programmers and enthusiasts. A fun and informative way to celebrate OCaml's birthday is to attend the 26th Annual International Conference on Functional Programming (ICFP), held online this year due to ongoing Covid restrictions. While this is disappointing news for so many, it's beneficial to those of you outside France because now you can hear professionals talk about cutting edge technology from the comfort of your own home.

Tarides engineers, as well as our colleagues at OCaml Labs Consultancy and Segfault Systems, have some exciting presentations at this year's ICFP! Listen to talks on running OCaml on multiple cores, generating fuzzing suites, benchmarking, and the experimental OCaml effects.

You can search the complete ICFP Timetable for other topics of interest and read below about our engineers' projects and presentations. Times are listed both in London (GMT +1) and Paris (GMT +2) for ease of planning. The following talks are scheduled for Friday, 27 August 2021.

Grab a cup of coffee for our first morning talk at 9am London / 10am Paris and learn about Adapting the OCaml Ecosystem for Multicore OCaml. With the soon-to-be released OCaml 5.0, there will be support for Shared-Memory Parallelism. There’s increasing interest in the community to port existing libraries to Multicore, so this talk will cover the arrival of Multicore and what that means to the OCaml ecosystem. Our engineers will highlight existing tools and provide methods for a smooth transition, so viewers can benefit from Multicore parallelism. They'll also share some insights from their experience porting existing libraries to Multicore OCaml.

Read more about this topic on todays' post at Segfault Systems, written by one of tomorrow's presenters, Sudha Parimala of Segfault Systems. Joining Sudha for the presentation are Enguerrand Decorne (Tarides), Sadiq Jaffer (Opsian and OCaml Labs Consultancy), Tom Kelly (OCaml Labs Consultancy), and KC Sivaramakrishnan of IIT Madras.

Next up is Leveraging Formal Specifications to Generate Fuzzing Suites at 11:10 London / 12:10 Paris, presented by Tarides's own Nicolas Osborne and Clément Pascutto. They'll discuss how developers typically first have to capture the semantics they want when checking a library and then write the code implementing these tests and find relevant test cases that expose possible misbehaviours. Through their work, they'll present a tool that automatically takes care of those last two steps by automatically generating fuzz testing suites from OCaml interfaces annotated with formal behavioural specifications. They'll also show some ongoing experiments on fuzzing capabilities and limitations applied to real-world libraries.

Next up is our talk on Continuous Benchmarking for OCaml Projects at 12:30 London / 13:30 Paris. Regular CI systems are optimised for workloads that do not require stable performance over time, which makes them unsuitable for running performance benchmarks. Tarides engineers Gargi Sharma, Rizo Isrof, and Magnus Skjegstad will discuss how current-bench provides a predictable environment for performance benchmarks and a UI for analysing results over time. Similar to a CI system it runs on pull requests and branches allowing performance to be analysed and compared, and it can currently be enabled on as an app on GitHub repositories with zero configuration. Several public repositories already run current-bench, including Irmin and Dune, and they plan to enable it on more projects in the future. Read Gargi's recent blog post for more information on benchmarking.

In this presentation, they will give a technical overview of current-bench, showing how results are collected and analysed, requirements for using it, and how they built the infrastructure for stable benchmarks. They'll also cover some future work that will allow more OCaml projects to run current-bench.

Immediately after the Benchmarking talk, catch A Multiverse of Glorious Documentation scheduled at 12:50 London / 13:50 Paris. Lucas Pluvinage of Tarides and Jonathan Ludlam of OCaml Labs Consultancy will discuss the process of generating documentation for every version of every package that can be built from the Opam repository and present it as a single coherent website that's continuously updated as new packages are released and old packages are updated. They will address the challenges of caching, handling different compiler versions, and incompatible libraries. The process has been implemented as an OCurrent pipeline named ocaml-docs-ci and is already available on Github. It has been used to produce the documentation of more than 10,000 package versions, generating 2.5M HTML pages. That's 38GB of artifacts!

After a relaxing lunch, come back for Experiences with Effects at 15:30 London / 16:30 Paris. Join OCaml Labs and Tarides engineers Thomas Leonard, Craig Ferguson, Patrick Ferris, Sadiq Jaffer, Tom Kelly, KC Sivaramakrishnan, and Anil Madhavapeddy as they talk about an exciting, experimental branch of Multicore OCaml that adds support for effect handlers. In this presentation, they'll discuss their experiences with effects, both from converting existing code and from writing new code. They discovered that converting the Angstrom parser from a callback style to effects greatly simplified the code while also improving performance and reducing allocations. Their experimental Eio library uses effects that allows writing concurrent code in direct style, without the need for monads (as found in Lwt or Async).

Enjoy a full day of OCaml innovation and get to know some of our talented engineers better by joining Tarides, OCaml Labs, and Segfault Systems at ICFP on Friday, 27 August 2021. See you there!

We are happy to announce the release of opam 2.1.0.

Many new features made it in (see the pre-release changelogs or release notes for the details), but here are a few highlights.

What’s new in opam 2.1?

• Integration of system dependencies (formerly the opam-depext plugin), increasing their reliability as it integrates the solving step
• Creation of lock files for reproducible installations (formerly the opam-lock plugin)
• Switch invariants, replacing the “base packages”…

We are happy to announce the release of opam 2.1.0.

Many new features made it in (see the pre-release changelogs or release notes for the details), but here are a few highlights.

What’s new in opam 2.1?

• Integration of system dependencies (formerly the opam-depext plugin), increasing their reliability as it integrates the solving step
• Creation of lock files for reproducible installations (formerly the opam-lock plugin)
• Switch invariants, replacing the “base packages” in opam 2.0 and allowing for easier compiler upgrades
• Improved options configuration (see the new option and expanded var sub-commands)
• CLI versioning, allowing cleaner deprecations for opam now and also improvements to semantics in future without breaking backwards-compatibility
• opam root readability by newer and older versions, even if the format changed
• Performance improvements to opam-update, conflict messages, and many other areas

Seamless integration of System dependencies handling (a.k.a. “depexts”)

opam has long included the ability to install system dependencies automatically via the depext plugin. This plugin has been promoted to a native feature of opam 2.1.0 onwards, giving the following benefits:

• You no longer have to remember to run opam depext, opam always checks depexts (there are options to disable this or automate it for CI use). Installation of an opam package in a CI system is now as easy as opam install ., without having to do the dance of opam pin add -n/depext/install. Just one command now for the common case!
• The solver is only called once, which both saves time and also stabilises the behaviour of opam in cases where the solver result is not stable. It was possible to get one package solution for the opam depext stage and a different solution for the opam install stage, resulting in some depexts missing.
• opam now has full knowledge of depexts, which means that packages can be automatically selected based on whether a system package is already installed. For example, if you have neither MariaDB nor MySQL dev libraries installed, opam install mysql will offer to install conf-mysql and mysql, but if you have the MariaDB dev libraries installed, opam will offer to install conf-mariadb and mysql.

Hint: You can set OPAMCONFIRMLEVEL=unsafe-yes or --confirm-level=unsafe-yes to launch non interactive system package commands.

opam lock files and reproducibility

When opam was first released, it had the mission of gathering together scattered OCaml source code to build a community repository. As time marches on, the size of the opam repository has grown tremendously, to over 3000 unique packages with over 19500 unique versions. opam looks at all these packages and is designed to solve for the best constraints for a given package, so that your project can keep up with releases of your dependencies.

While this works well for libraries, we need a different strategy for projects that need to test and ship using a fixed set of dependencies. To satisfy this use-case, opam 2.0.0 shipped with support for using project.opam.locked files. These are normal opam files but with exact versions of dependencies. The lock file can be used as simply as opam install . --locked to have a reproducible package installation.

With opam 2.1.0, the creation of lock files is also now integrated into the client:

• opam lock will create a .locked file for your current switch and project, that you can check into the repository.
• opam switch create . --locked can be used by users to reproduce your dependencies in a fresh switch.

This lets a project simultaneously keep up with the latest dependencies (without lock files) while providing a stricter set for projects that need it (with lock files).

Hint: You can export the full configuration of a switch with opam switch export new options, --full to have all packages metadata included, and --freeze to freeze all VCS to their current commit.

Switch invariants

In opam 2.0, when a switch is created the packages selected are put into the “base” of the switch. These packages are not normally considered for upgrade, in order to ease pressure on opam’s solver. This was a much bigger concern early on in opam 2.0’s development, but is less of a problem with the default mccs solver.

However, it’s a problem for system compilers. opam would detect that your system compiler version had changed, but be unable to upgrade the ocaml-system package unless you went through a slightly convoluted process with --unlock-base.

In opam 2.1, base packages have been replaced by switch invariants. The switch invariant is a package formula which must be satisfied on every upgrade and install. All existing switches’ base packages could just be expressed as package1 & package2 & package3 etc. but opam 2.1 recognises many existing patterns and simplifies them, so in most cases the invariant will be "ocaml-base-compiler" {= "4.11.1"}, etc. This means that opam switch create my_switch ocaml-system now creates a switch invariant of "ocaml-system" rather than a specific version of the ocaml-system package. If your system OCaml package is updated, opam upgrade will seamlessly switch to the new package.

This also allows you to have switches which automatically install new point releases of OCaml. For example:

opam switch create ocaml-4.11 --formula='"ocaml-base-compiler" {>= "4.11.0" & < "4.12.0~"}' --repos=old=git+https://github.com/ocaml/opam-repository#a11299d81591
opam install utop

Creates a switch with OCaml 4.11.0 (the --repos= was just to select a version of opam-repository from before 4.11.1 was released). Now issue:

opam repo set-url old git+https://github.com/ocaml/opam-repository
opam upgrade

and opam 2.1 will automatically offer to upgrade OCaml 4.11.1 along with a rebuild of the switch. There's not yet a clean CLI for specifying the formula, but we intend to iterate further on this with future opam releases so that there is an easier way of saying “install OCaml 4.11.x”.

Hint: You can set up a default invariant that will apply for all new switches, via a specific opamrc. The default one is ocaml >= 4.05.0

Configuring opam from the command-line

Configuring opam is not a simple task: you need to use an opamrc at init stage, or hack global/switch config file, or use opam config var for additional variables. To ease that step, and permit a more consistent opam config tweaking, a new command was added : opam option.

For example:

• opam option download-jobs gives the global download-jobs value (as it exists only in global configuration)
• opam option jobs=6 --global will set the number of parallel build jobs opam is allowed to run (along with the associated jobs variable)
• opam option depext-run-commands=false disables the use of sudo for handling system dependencies; it will be replaced by a prompt to run the installation commands
• opam option depext-bypass=m4 --global bypass m4 system package check globally, while opam option depext-bypass=m4 --switch myswitch will only bypass it in the selected switch

The command opam var is extended with the same format, acting on switch and global variables.

Hint: to revert your changes use opam option <field>=, it will take its default value.

CLI Versioning

A new --cli switch was added to the first beta release, but it's only now that it's being widely used. opam is a complex enough system that sometimes bug fixes need to change the semantics of some commands. For example:

• opam show --file needed to change behaviour
• The addition of new controls for setting global variables means that the opam config was becoming cluttered and some things want to move to opam var
• opam switch install 4.11.1 still works in opam 2.0, but it's really an OPAM 1.2.2 syntax.

Changing the CLI is exceptionally painful since it can break scripts and tools which themselves need to drive opam. CLI versioning is our attempt to solve this. The feature is inspired by the (lang dune ...) stanza in dune-project files which has allowed the Dune project to rename variables and alter semantics without requiring every single package using Dune to upgrade their dune files on each release.

Now you can specify which version of opam you expected the command to be run against. In day-to-day use of opam at the terminal, you wouldn't specify it, and you'll get the latest version of the CLI. For example: opam var --global is the same as opam var --cli=2.1 --global. However, if you issue opam var --cli=2.0 --global, you will told that --global was added in 2.1 and so is not available to you. You can see similar things with the renaming of opam upgrade --unlock-base to opam upgrade --update-invariant.

The intention is that --cli should be used in scripts, user guides (e.g. blog posts), and in software which calls opam. The only decision you have to take is the oldest version of opam which you need to support. If your script is using a new opam 2.1 feature (for example opam switch create --formula=) then you simply don't support opam 2.0. If you need to support opam 2.0, then you can't use --formula and should use --packages instead. opam 2.0 does not have the --cli option, so for opam 2.0 instead of --cli=2.0 you should set the environment variable OPAMCLI to 2.0. As with all opam command line switches, OPAMCLI is simply the equivalent of --cli which opam 2.1 will pick-up but opam 2.0 will quietly ignore (and, as with other options, the command line takes precedence over the environment).

Note that opam 2.1 sets OPAMCLI=2.0 when building packages, so on the rare instances where you need to use the opam command in a package build: command (or in your build system), you must specify --cli=2.1 if you're using new features.

Since 2.1.0~rc2, CLI versioning applies to opam environment variables. The previous behavior was to ignore unknown or wrongly set environment variable, while now you will have a warning to let you know that the environment variable won't be handled by this version of opam.

To ensure not breaking compatibility of some widely used deprecated options, a default CLI is introduced: when no CLI is specified, those deprecated options are accepted. It concerns opam exec and opam var subcommands.

There's even more detail on this feature in our wiki. We're hoping that this feature will make it much easier in future releases for opam to make required changes and improvements to the CLI without breaking existing set-ups and tools.

Note: For opam libraries users, since 2.1 environment variable are no more loaded by the libraries, only by opam client. You need to load them explicitly.

opam root portability

opam root format changes during opam life-cycle, new field are added or removed, new files are added ; an older opam version sometimes can no longer read an upgraded or newly created opam root. opam root format has been updated to allow new versions of opam to indicate that the root may still be read by older versions of the opam libraries. A plugin compiled against the 2.0.9 opam libraries will therefore be able to read information about an opam 2.1 root (plugins and tools compiled against 2.0.8 are unable to load opam 2.1.0 roots). It is a read-only best effort access, any attempt to modify the opam root fails.

Hint: for opam libraries users, you can safely load states with OpamStateConfig load functions.

Tremendous thanks to all involved people, who've developed, tested & retested, helped with issue reports, comments, feedback...

Try it!

In case you plan a possible rollback, you may want to first backup your ~/.opam directory.

The upgrade instructions are unchanged:

1. Either from binaries: run bash -c "sh <(curl -fsSL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh) --version 2.1.0" or download manually from the Github "Releases" page to your PATH.
2. Or from source, manually: see the instructions in the README.

You should then run:

opam init --reinit -ni

About OCamlPro:
OCamlPro is a R&D lab founded in 2011, with the mission to help industrial users benefit from state-of-the art programming languages like OCaml and Rust. We design, create and implement custom ad-hoc software for our clients. We also have a long experience in developing and maintaining open-source tooling for OCaml, such as Opam, TryOCaml, ocp-indent, ocp-index and ocp-browser, and we contribute to the core-development of OCaml, notably with our work on the Flambda optimizer branch. Another area of expertise is that of Formal Methods, with tools such as our SMT Solver Alt-Ergo (check our Alt-Ergo Users' Club). We also provide vocational trainings in OCaml and Rust, and we can build courses on formal methods on-demand. Do not hesitate to reach out by email: contact@ocamlpro.com.

Feedback on this post is welcomed on Discuss!

We are pleased to announce the minor release of opam 2.0.9.

This new version contains some back-ported fixes.

New features

• Back-ported ability to load upgraded roots read-only; allows applications compiled with opam-state 2.0.9 to load a root which has been upgraded to opam 2.1 [#4636]
• macOS sandbox now supports OPAM_USER_PATH_RO for adding a custom read-only directory to the sandbox [#4589, #4609]
• OPAMROOT and OPAMSWITCH now reflect t…

Feedback on this post is welcomed on Discuss!

We are pleased to announce the minor release of opam 2.0.9.

This new version contains some back-ported fixes.

New features

• Back-ported ability to load upgraded roots read-only; allows applications compiled with opam-state 2.0.9 to load a root which has been upgraded to opam 2.1 [#4636]
• macOS sandbox now supports OPAM_USER_PATH_RO for adding a custom read-only directory to the sandbox [#4589, #4609]
• OPAMROOT and OPAMSWITCH now reflect the --root and --switch parameters in the package build [#4668]
• When built with opam-file-format 2.1.3+, opam-format 2.0.x displays better errors for newer opam files [#4394]

Bug fixes

• Linux sandbox now mounts host $TMPDIR read-only, then sets the sandbox $TMPDIR to a new separate tmpfs. Hardcoded /tmp access no longer works if TMPDIR points to another directory [#4589]
• Stop clobbering DUNE_CACHE in the sandbox script [#4535, fixing ocaml/dune#4166]
• Ctrl-C now correctly terminates builds with bubblewrap; sandbox now requires bubblewrap 0.1.8 or later [#4400]
• Linux sandbox script no longer makes PWD read-write on remove actions [#4589]
• Lint W59 and E60 no longer trigger for packages flagged conf [#4549]
• Reduce the length of temporary file names for pin caching to ease pressure on Windows [#4590]
• Security: correct quoting of arguments when removing switches [#4707]
• Stop advertising the removed option --compiler when creating local switches [#4718]
• Pinning no longer fails if the archive’s opam file is malformed [#4580]
• Fish: stop using deprecated ^ syntax to fix support for Fish 3.3.0+ [#4736]

Installation instructions (unchanged):

1. From binaries: run

bash -c "sh <(curl -fsSL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh) --version 2.0.9"

or download manually from the Github "Releases" page to your PATH. In this case, don't forget to run opam init --reinit -ni to enable sandboxing if you had version 2.0.0~rc manually installed or to update you sandbox script.

2. From source, using opam:

 opam update; opam install opam-devel 

(then copy the opam binary to your PATH as explained, and don't forget to run opam init --reinit -ni to enable sandboxing if you had version 2.0.0~rc manually installed or to update your sandbox script)

From source, manually: see the instructions in the README.

We hope you enjoy this new minor version, and remain open to bug reports and suggestions.

About OCamlPro:
OCamlPro is a R&D lab founded in 2011, with the mission to help industrial users benefit from state-of-the art programming languages like OCaml and Rust. We design, create and implement custom ad-hoc software for our clients. We also have a long experience in developing and maintaining open-source tooling for OCaml, such as Opam, TryOCaml, ocp-indent, ocp-index and ocp-browser, and we contribute to the core-development of OCaml, notably with our work on the Flambda optimizer branch. Another area of expertise is that of Formal Methods, with tools such as our SMT Solver Alt-Ergo (check our Alt-Ergo Users' Club). We also provide vocational trainings in OCaml and Rust, and we can build courses on formal methods on-demand. Do not hesitate to reach out by email: contact@ocamlpro.com.

Feedback on this post is welcomed on Discuss!

We are happy to announce the release of opam 2.1.0.

Many new features made it in (see the pre-release changelogs or release notes for the details), but here are a few highlights.

What's new in opam 2.1?

• Integration of system dependencies (formerly the opam-depext plugin), increasing their reliability as it integrates the solving step
• Creation of lock files for reproducible installations (formerly the opam-lock plugin)
• Switch invariants, replacing …

Feedback on this post is welcomed on Discuss!

We are happy to announce the release of opam 2.1.0.

Many new features made it in (see the pre-release changelogs or release notes for the details), but here are a few highlights.

What's new in opam 2.1?

• Integration of system dependencies (formerly the opam-depext plugin), increasing their reliability as it integrates the solving step
• Creation of lock files for reproducible installations (formerly the opam-lock plugin)
• Switch invariants, replacing the "base packages" in opam 2.0 and allowing for easier compiler upgrades
• Improved options configuration (see the new option and expanded var sub-commands)
• CLI versioning, allowing cleaner deprecations for opam now and also improvements to semantics in future without breaking backwards-compatibility
• opam root readability by newer and older versions, even if the format changed
• Performance improvements to opam-update, conflict messages, and many other areas

Seamless integration of System dependencies handling (a.k.a. "depexts")

opam has long included the ability to install system dependencies automatically via the depext plugin. This plugin has been promoted to a native feature of opam 2.1.0 onwards, giving the following benefits:

• You no longer have to remember to run opam depext, opam always checks depexts (there are options to disable this or automate it for CI use). Installation of an opam package in a CI system is now as easy as opam install ., without having to do the dance of opam pin add -n/depext/install. Just one command now for the common case!
• The solver is only called once, which both saves time and also stabilises the behaviour of opam in cases where the solver result is not stable. It was possible to get one package solution for the opam depext stage and a different solution for the opam install stage, resulting in some depexts missing.
• opam now has full knowledge of depexts, which means that packages can be automatically selected based on whether a system package is already installed. For example, if you have neither MariaDB nor MySQL dev libraries installed, opam install mysql will offer to install conf-mysql and mysql, but if you have the MariaDB dev libraries installed, opam will offer to install conf-mariadb and mysql.

Hint: You can set OPAMCONFIRMLEVEL=unsafe-yes or --confirm-level=unsafe-yes to launch non interactive system package commands.

opam lock files and reproducibility

When opam was first released, it had the mission of gathering together scattered OCaml source code to build a community repository. As time marches on, the size of the opam repository has grown tremendously, to over 3000 unique packages with over 19500 unique versions. opam looks at all these packages and is designed to solve for the best constraints for a given package, so that your project can keep up with releases of your dependencies.

While this works well for libraries, we need a different strategy for projects that need to test and ship using a fixed set of dependencies. To satisfy this use-case, opam 2.0.0 shipped with support for using project.opam.locked files. These are normal opam files but with exact versions of dependencies. The lock file can be used as simply as opam install . --locked to have a reproducible package installation.

With opam 2.1.0, the creation of lock files is also now integrated into the client:

• opam lock will create a .locked file for your current switch and project, that you can check into the repository.
• opam switch create . --locked can be used by users to reproduce your dependencies in a fresh switch.

This lets a project simultaneously keep up with the latest dependencies (without lock files) while providing a stricter set for projects that need it (with lock files).

Hint: You can export the full configuration of a switch with opam switch export new options, --full to have all packages metadata included, and --freeze to freeze all VCS to their current commit.

Switch invariants

In opam 2.0, when a switch is created the packages selected are put into the “base” of the switch. These packages are not normally considered for upgrade, in order to ease pressure on opam's solver. This was a much bigger concern early on in opam 2.0's development, but is less of a problem with the default mccs solver.

However, it's a problem for system compilers. opam would detect that your system compiler version had changed, but be unable to upgrade the ocaml-system package unless you went through a slightly convoluted process with --unlock-base.

In opam 2.1, base packages have been replaced by switch invariants. The switch invariant is a package formula which must be satisfied on every upgrade and install. All existing switches' base packages could just be expressed as package1 & package2 & package3 etc. but opam 2.1 recognises many existing patterns and simplifies them, so in most cases the invariant will be "ocaml-base-compiler" {= "4.11.1"}, etc. This means that opam switch create my_switch ocaml-system now creates a switch invariant of "ocaml-system" rather than a specific version of the ocaml-system package. If your system OCaml package is updated, opam upgrade will seamlessly switch to the new package.

This also allows you to have switches which automatically install new point releases of OCaml. For example:

opam switch create ocaml-4.11 --formula='"ocaml-base-compiler" {>= "4.11.0" & < "4.12.0~"}' --repos=old=git+https://github.com/ocaml/opam-repository#a11299d81591
opam install utop

Creates a switch with OCaml 4.11.0 (the --repos= was just to select a version of opam-repository from before 4.11.1 was released). Now issue:

opam repo set-url old git+https://github.com/ocaml/opam-repository
opam upgrade

and opam 2.1 will automatically offer to upgrade OCaml 4.11.1 along with a rebuild of the switch. There's not yet a clean CLI for specifying the formula, but we intend to iterate further on this with future opam releases so that there is an easier way of saying “install OCaml 4.11.x”.

Hint: You can set up a default invariant that will apply for all new switches, via a specific opamrc. The default one is ocaml >= 4.05.0

Configuring opam from the command-line

Configuring opam is not a simple task: you need to use an opamrc at init stage, or hack global/switch config file, or use opam config var for additional variables. To ease that step, and permit a more consistent opam config tweaking, a new command was added : opam option.

For example:

• opam option download-jobs gives the global download-jobs value (as it exists only in global configuration)
• opam option jobs=6 --global will set the number of parallel build jobs opam is allowed to run (along with the associated jobs variable)
• opam option depext-run-commands=false disables the use of sudo for handling system dependencies; it will be replaced by a prompt to run the installation commands
• opam option depext-bypass=m4 --global bypass m4 system package check globally, while opam option depext-bypass=m4 --switch myswitch will only bypass it in the selected switch

The command opam var is extended with the same format, acting on switch and global variables.

Hint: to revert your changes use opam option <field>=, it will take its default value.

CLI Versioning

A new --cli switch was added to the first beta release, but it's only now that it's being widely used. opam is a complex enough system that sometimes bug fixes need to change the semantics of some commands. For example:

• opam show --file needed to change behaviour
• The addition of new controls for setting global variables means that the opam config was becoming cluttered and some things want to move to opam var
• opam switch install 4.11.1 still works in opam 2.0, but it's really an OPAM 1.2.2 syntax.

Changing the CLI is exceptionally painful since it can break scripts and tools which themselves need to drive opam. CLI versioning is our attempt to solve this. The feature is inspired by the (lang dune ...) stanza in dune-project files which has allowed the Dune project to rename variables and alter semantics without requiring every single package using Dune to upgrade their dune files on each release.

Now you can specify which version of opam you expected the command to be run against. In day-to-day use of opam at the terminal, you wouldn't specify it, and you'll get the latest version of the CLI. For example: opam var --global is the same as opam var --cli=2.1 --global. However, if you issue opam var --cli=2.0 --global, you will told that --global was added in 2.1 and so is not available to you. You can see similar things with the renaming of opam upgrade --unlock-base to opam upgrade --update-invariant.

The intention is that --cli should be used in scripts, user guides (e.g. blog posts), and in software which calls opam. The only decision you have to take is the oldest version of opam which you need to support. If your script is using a new opam 2.1 feature (for example opam switch create --formula=) then you simply don't support opam 2.0. If you need to support opam 2.0, then you can't use --formula and should use --packages instead. opam 2.0 does not have the --cli option, so for opam 2.0 instead of --cli=2.0 you should set the environment variable OPAMCLI to 2.0. As with all opam command line switches, OPAMCLI is simply the equivalent of --cli which opam 2.1 will pick-up but opam 2.0 will quietly ignore (and, as with other options, the command line takes precedence over the environment).

Note that opam 2.1 sets OPAMCLI=2.0 when building packages, so on the rare instances where you need to use the opam command in a package build: command (or in your build system), you must specify --cli=2.1 if you're using new features.

Since 2.1.0~rc2, CLI versioning applies to opam environment variables. The previous behavior was to ignore unknown or wrongly set environment variable, while now you will have a warning to let you know that the environment variable won't be handled by this version of opam.

To ensure not breaking compatibility of some widely used deprecated options, a default CLI is introduced: when no CLI is specified, those deprecated options are accepted. It concerns opam exec and opam var subcommands.

There's even more detail on this feature in our wiki. We're hoping that this feature will make it much easier in future releases for opam to make required changes and improvements to the CLI without breaking existing set-ups and tools.

Note: For opam libraries users, since 2.1 environment variable are no more loaded by the libraries, only by opam client. You need to load them explicitly.

opam root portability

opam root format changes during opam life-cycle, new field are added or removed, new files are added ; an older opam version sometimes can no longer read an upgraded or newly created opam root. opam root format has been updated to allow new versions of opam to indicate that the root may still be read by older versions of the opam libraries. A plugin compiled against the 2.0.9 opam libraries will therefore be able to read information about an opam 2.1 root (plugins and tools compiled against 2.0.8 are unable to load opam 2.1.0 roots). It is a read-only best effort access, any attempt to modify the opam root fails.

Hint: for opam libraries users, you can safely load states with OpamStateConfig load functions.

Tremendous thanks to all involved people, who've developed, tested & retested, helped with issue reports, comments, feedback...

Try it!

In case you plan a possible rollback, you may want to first backup your ~/.opam directory.

The upgrade instructions are unchanged:

1. Either from binaries: run

   bash -c "sh <(curl -fsSL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh) --version 2.1.0"

   or download manually from the Github "Releases" page to your PATH.

2. Or from source, manually: see the instructions in the README.

You should then run:

opam init --reinit -ni

Feedback on this post is welcomed on Discuss!

We are pleased to announce the minor release of opam 2.0.9.

This new version contains some back-ported fixes.

New features

• Back-ported ability to load upgraded roots read-only; allows applications compiled with opam-state 2.0.9 to load a root which has been upgraded to opam 2.1 [#4636]
• macOS sandbox now supports OPAM_USER_PATH_RO for adding a custom read-only directory to the sandbox [#4589, #4609]
• OPAMROOT and OPAMSWITCH now reflect the --root and --…

Feedback on this post is welcomed on Discuss!

We are pleased to announce the minor release of opam 2.0.9.

This new version contains some back-ported fixes.

New features

• Back-ported ability to load upgraded roots read-only; allows applications compiled with opam-state 2.0.9 to load a root which has been upgraded to opam 2.1 [#4636]
• macOS sandbox now supports OPAM_USER_PATH_RO for adding a custom read-only directory to the sandbox [#4589, #4609]
• OPAMROOT and OPAMSWITCH now reflect the --root and --switch parameters in the package build [#4668]
• When built with opam-file-format 2.1.3+, opam-format 2.0.x displays better errors for newer opam files [#4394]

Bug fixes

• Linux sandbox now mounts host $TMPDIR read-only, then sets the sandbox $TMPDIR to a new separate tmpfs. Hardcoded /tmp access no longer works if TMPDIR points to another directory [#4589]
• Stop clobbering DUNE_CACHE in the sandbox script [#4535, fixing ocaml/dune#4166]
• Ctrl-C now correctly terminates builds with bubblewrap; sandbox now requires bubblewrap 0.1.8 or later [#4400]
• Linux sandbox script no longer makes PWD read-write on remove actions [#4589]
• Lint W59 and E60 no longer trigger for packages flagged conf [#4549]
• Reduce the length of temporary file names for pin caching to ease pressure on Windows [#4590]
• Security: correct quoting of arguments when removing switches [#4707]
• Stop advertising the removed option --compiler when creating local switches [#4718]
• Pinning no longer fails if the archive's opam file is malformed [#4580]
• Fish: stop using deprecated ^ syntax to fix support for Fish 3.3.0+ [#4736]

1. From binaries: run

   bash -c "sh <(curl -fsSL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh) --version 2.0.9"

   or download manually from the Github "Releases" page to your PATH. In this case, don't forget to run opam init --reinit -ni to enable sandboxing if you had version 2.0.0~rc manually installed or to update you sandbox script.

2. From source, using opam:

   opam update; opam install opam-devel

   (then copy the opam binary to your PATH as explained, and don't forget to run opam init --reinit -ni to enable sandboxing if you had version 2.0.0~rc manually installed or to update your sandbox script)

3. From source, manually: see the instructions in the README.

We hope you enjoy this new minor version, and remain open to bug reports and suggestions.

Tarides takes great pride in a diverse workforce and strives to continue bringing talented people to its team from around the globe. This is why Sonja Heinze, a Tarides software engineer, and the Head of HR, Héloïse Lutton, will attend WomenHack, an online event dedicated to recruiting more women into the tech world. They're participating not only to present Tarides to the Women In Tech community, but to also network and possibly find new talented programmers to join our growing team.

The Wome…

Tarides takes great pride in a diverse workforce and strives to continue bringing talented people to its team from around the globe. This is why Sonja Heinze, a Tarides software engineer, and the Head of HR, Héloïse Lutton, will attend WomenHack, an online event dedicated to recruiting more women into the tech world. They're participating not only to present Tarides to the Women In Tech community, but to also network and possibly find new talented programmers to join our growing team.

The WomenHack event has a unique setup similar to 'speed dating,' but for prospective jobs. Each candidate is paired with a company, and they have 5 minutes to chat before moving on to the next company. This "rapid interview" is both fun and efficient for all involved, and it ensures each company will meet several talented candidates from diverse backgrounds, which increases their chance of finding that perfect fit for an open position!

From their website:

WomenHack is a community that empowers women in tech through events, jobs, and reviews. We aim to create a more inclusive and diverse workplace for all. Our diversity recruiting events target some of the most talented women in tech which include software developers, designers, and product talent. 

Join us tomorrow, July 21st, at WomenHack! You can get your ticket here.

In some discussions among OCaml developers around the empty type (PR#9459), some people mused about the possibility of annotating functions with an attribute telling the compiler that the function should be trivial, and always return a value strictly equivalent to its argument.
Curious about the feasibility of implementing this feature, we advertised an internship with our compiler team aimed at exploring this subject.
We welcomed Léo Boitel during three months to work on this topic, with Vincen…

In some discussions among OCaml developers around the empty type (PR#9459), some people mused about the possibility of annotating functions with an attribute telling the compiler that the function should be trivial, and always return a value strictly equivalent to its argument.
Curious about the feasibility of implementing this feature, we advertised an internship with our compiler team aimed at exploring this subject.
We welcomed Léo Boitel during three months to work on this topic, with Vincent Laviron as mentor, and we’re proud to let him show off what he has achieved in this post.

The problem at hand

OCaml’s strong typing system is one of its main perks: it allows to write safe code thanks to the abstraction it provides. Most of the basic design mistakes will directly result into a typing error and the user cannot mess up the memory as it is automatically handled by the compiler and runtime.

However, these perks keep a power-user from implementing some optimizations, in particular those linked to memory representation as they cannot be accessed directly.

A good example would be this piece of code:

type return = Ok of int | Failure
let id = function
| Some x -> Ok x
| None -> Failure

In terms of memory representation, this function is indeed the identity function. Some x and Ok x share the same representation (and so do None and Failure). However, this identity is invisible to the user. Even if the user knows the representation is the same, they would need to use this function to avoid a typing error.

Another good example would be this one:

type record = { a:int; b:int }
let id (x,y) = { a = x; b = y }

Even if those functions are the identity, they come with a cost: not only do they cost a function call, they reallocate the result instead of just returning their argument directly. Detecting those functions would allow us to produce interesting optimizations.

Hurdles

If we want to detect identities, we quickly hit the problem of recursive functions: how does one recognize identity in those cases? Can a function be an identity if it doesn’t always terminate, or if it never does?

Once we have a good definition of what exactly an identity function is, we still need to prove that an existing function fits the definition. Indeed, we want to ensure the user that this optimization will not change the observable behavior of the program.

We also want to avoid breaking type safety. As an example, the following function:

let rec fake_id = function
| [] -> 0
| t::q -> fake_id (t::q)

A naive induction proof would allow us to replace this function with the identity, as [] and 0 share the same memory representation. However, this is unsafe as applying this to a non-empty list would return a list even if this function has an int type (we’ll talk more about it later).

To tackle those challenges, we started the internship with a theoretical study that lasted for three fourths of the allocated time and lastly implemented a practical solution in the Flambda representation of the compiler.

Theoretical results

We worked on extensions of lambda-calculus (implemented in OCaml) in order to gradually test our ideas in a simpler framework than the full Flambda.

Pairs

We started with a lambda-calculus to which we only added the concept of pairs. To prove identities, every function has to be annotated as identity or not. We then prove these annotations by β-reducing the function bodies. After each recursive reduction, we apply a rule that states that a pair made of the first and second projection of a variable is equal to that variable. We do not reduce applications, but we replace them by the argument if the concerned function is annotated as identity.

Using this method, we maintain a reasonable complexity compared to a full β-reduction which would be unrealistic on a big program.

We then add higher-order capabilities by allowing annotations of the form Annotation → Annotation. Functions as List.map can that way be abstracted as Id → Id. Even though this solution doesn’t cover every case, most real-world usage are recognized by these patterns.

Tuple reconstruction

We then move from just pairs to tuples of arbitrary size. This adds a new problem: if we make a pair out of the first two fields of a variable, this is no longer necessarily that variable, as it may have more than two fields.

We then have two solutions: we can first annotate every projection with the size of the involved tuple to know if we are indeed reconstructing the entire variable. As an example, if we make a pair from the fields of a triplet, we know there is no way to simplify this reconstruction.

Another solution, more ambitious, is to adopt a less restrictive definition of equality and to allow the replacement of (x,y) by (x,y,z). Indeed, if the variable was typed as a pair, we are guaranteed that the third field will never be accessed. The behavior of the program will therefore never be affected by this extension.

Though this allows to avoid a lot of allocations, it may also increase memory usage in some cases: if the triplet ceases to be used, it won’t be deallocated by the Garbage Collector (GC) and the field z will be kept in memory as long as (x,y) is still accessible.

This approach remains interesting to us, as long as it is manually enabled by the user for some specific blocks.

Recursion

We now add recursive definitions to our language, through the use of a fixpoint operator.

To prove that a recursive function is the identity, we have to use induction. The main difficulty is to prove that the function indeed terminates to ensure the validity of the induction.

We can separate this into three different levels of safety. The first option is to not prove termination at all, and let the user state which function they know will return. We can then assume the function is the identity and replace its body on that hypothesis. This approach is enough for most practical cases, but its main problem lies in the fact that it allows to write unsafe code (as we’ve already seen).

Our second option is to limit our induction hypothesis to recursive applications on “smaller” elements than the argument. An element is defined as smaller if it is a projection of the argument or a projection of a smaller element. This is not enough to prove that the function will terminate (the argument might be cyclic, for example) but is enough to ensure type safety. The reason is that any possibly returned value is constructed (as it cannot directly come from a recursive call) and have therefore a defined type. Typing would fail if the function was to return a value that cannot be identified to its argument.

Finally, we may want to establish a perfect equivalence between the function and the identity function before simplifying it. In that case, we propose to create a special annotation for functions that are the identity when applied to a non-cyclical object. We can prove they have this property with the already described induction. The difficulty now lies into applying the simplification only to valid applications: if an object is immutable, wasn’t recursively defined and is made of components that also have that property, we can declare that object inductive and simplify applications on it. The inductive state of variables can be propagated during our recursive pass of optimization.

Block reconstruction

The representation of blocks in Flambda provides interesting challenges in terms of equality detection, which is often crucial to prove an identity. It is very hard to detect an identical block reconstruction.

Blocks in Flambda

Variants

The blocks in Flambda come from the existence of variants in OCaml: one type may have several different constructors, as we can see in

type choice = A of int | B of int

When OCaml is compiled to Flambda, the information used by the constructor is lost and replaced by a tag. The tag is a number contained in the header of the object’s memory representation between 0 and 255 that represents which constructor was used. As an example, an element of type choice would have tag 0 for the A constructor, and 1 for B.

That tag will be kept at runtime, which will allow for example to implement pattern matching as a simple switch in Flambda, that executes simple comparisons on the tag to know which branch to execute next.

This system complicates our task as Flambda’s typing doesn’t inform us which type the constructor is supposed to have, and therefore keeps us from easily knowing if two variants are indeed equal.

Tag generalization

To complicate things, tags are actually used for any block, meaning tuples, modules or functions (as a matter of fact, almost anything but constant constructors and integers). If the object doesn’t have variants, it will usually have tag 0. This tag is never read (as there are no variants to differentiate) but keeps us from simply comparing two tuples, because Flambda will simply see two blocks of unknown tag.

Inlining

Finally, this system is optimized by inlining tuples: if a variant has a shape Pair of int * int, it will be often be flattened into a tuple (tag Pair, int, int).

This also means that variants can have an arbitrary size, which is also unknown in Flambda.

Existing approach

A partial solution to the problem already existed in a Pull Request (PR) you can read here.

The chosen approach in this PR is the natural one: we use the switch to gain information on the tag of a block, depending on the branch taken. The PR also allows to know the mutability and size of the block in each branch, starting from OCaml (where this information is known as it is explicit in the pattern matching) and propagating the knowledge to Flambda.

This allows to register every block on which a switch is done with their tag, size and mutability. We can then detect if one of them is reconstructed with the use of a Pmakeblock primitive.

Unfortunately, this path has its limits as there are numerous cases where the tag and size could be known without performing a switch on the value. As an example, this doesn’t allow the simplification of tuple reconstruction.

New solution

Our new solution will have to propagate more information from OCaml into Flambda. This propagation is based on two PRs that already existed for Flambda 2, which annotated in the lambda representation each projection (Pfield) with typing informations. We add block mutability and tag and finally size.

Our first contribution was to translate these PRs to Flambda 1, and to propagate from lambda to Flambda correctly.

We then had access to every necessary information to detect and prove block reconstruction: not only we have a list of blocks that were pattern-matched, we can make a list of partially immutable blocks, meaning blocks for which we know that some fields are immutable.

Here’s how we use it:

Block discovery

As soon as we find a projection, we verify whether it is done on an immutable block of known size. If so, we add that block to the list of partial blocks. We verify that the information we have on the tag and size are compatible with the already known projections. If all of the fields of the block are known, the block is added to the list of simplifiable blocks.

Of course, we also keep track of known blocks though switches.

Simplification

This part is similar to the original PR: when an immutable block is met, we check whether this block is known as simplifiable. In that case we avoid a reallocation.

Compared to the original approach, we also reduced the asymptotic complexity (from quadratic to linear) by registering the association of every projection variable to its index and original block. We also modified some implementation details that could have triggered a bug when associated with our PR.

Example

Let’s consider this function:

type typ1 = A of int | B of int * int
type typ2 = C of int | D of {x:int; y:int}
let id = function
  | A n -> C n
  | B (x,y) -> D {x; y}

The current compiler would produce the resulting Flambda output:

End of middle end:
let_symbol
  (camlTest__id_21
    (Set_of_closures (
      (set_of_closures id=Test.8
        (id/5 = fun param/7 ->
          (switch*(0,2) param/7
           case tag 0:
            (let
              (Pmakeblock_arg/11 (field 0<{../../test.ml:4,4-7}> param/7)
               Pmakeblock/12
                 (makeblock 0 (int)<{../../test.ml:4,11-14}>
                   Pmakeblock_arg/11))
              Pmakeblock/12)
           case tag 1:
            (let
              (Pmakeblock_arg/15 (field 1<{../../test.ml:5,4-11}> param/7)
               Pmakeblock_arg/16 (field 0<{../../test.ml:5,4-11}> param/7)
               Pmakeblock/17
                 (makeblock 1 (int,int)<{../../test.ml:5,17-23}>
                   Pmakeblock_arg/16 Pmakeblock_arg/15))
              Pmakeblock/17)))
         free_vars={ } specialised_args={}) direct_call_surrogates={ }
        set_of_closures_origin=Test.1])))
  (camlTest__id_5_closure (Project_closure (camlTest__id_21, id/5)))
  (camlTest (Block (tag 0,  camlTest__id_5_closure)))
End camlTest

Our optimization allows to detect that this function reconstructs a similar block and therefore can simplify it:

End of middle end:
let_symbol
  (camlTest__id_21
    (Set_of_closures (
      (set_of_closures id=Test.7
        (id/5 = fun param/7 ->
          (switch*(0,2) param/7
           case tag 0 (1): param/7
           case tag 1 (2): param/7))
         free_vars={ } specialised_args={}) direct_call_surrogates={ }
        set_of_closures_origin=Test.1])))
  (camlTest__id_5_closure (Project_closure (camlTest__id_21, id/5)))
  (camlTest (Block (tag 0,  camlTest__id_5_closure)))
End camlTest

Possible improvements

Equality relaxation

We can use observational equality studied in the theoretical part for block equality in order to avoid more allocations. The implementation is simple:

When a block is created, to know if it will be allocated, the normal course of action is to check if all of its fields are the known projections of another block, with the same index, and if the block sizes are the same. We can just remove that last check.

Implementing this was a bit more tricky because of several practical details. First, we want that optimization to be only triggered on user-annotated blocks, we had to propagate that annotation to Flambda.

Additionally, if we only implement that optimization, numerous optimization cases will be ignored because unused variables are simplified before our optimization pass. As an example, if a function looks like

let loose_id (a,b,c) = (a,b)

The c variable will be simplified away before reaching Flambda, and there will be no way to prove that (a,b,c) is immutable as its third field could not be. This problem is being solved on Flambda2 thanks to a PR that propagates mutability information for every block, but we didn’t have the time necessary to migrate it on Flambda 1.

Detecting recursive identities

Now that we can detect block reconstruction, we’re left with solving the problem of recursive functions.

Unsafe approach

We began the implementation of a pass that contains no termination proof. The idea is to add the proof later, or to authorize non-terminating functions to be simplified as long as they type correctly (see previously in the theory part).

For now, we trust the user to verify these properties manually.

Hence, we modified the function simplification procedure: when a function with a single argument is modified, we first assume that this function is the identity before simplifying its body. We then check whether the result is equivalent to an identity by recursively going through it, so as to cover as many cases as possible (for example in conditional branchings). If it is the case, the function will be replaced by the identity ; otherwise, we go back to a normal simplification, without the induction hypothesis.

Constant propagation

We took some time to improve our code that checks whether the body of a function is an identity or not, so as to handle constant values. It propagates identity information we have on an argument during conditional branching.

This way, on a function like

type truc = A | B | C
let id = function
  | A -> A
  | B -> B
  | C -> C

or even

let id x = if x=0 then 0 else x

We can successfully detect identity.

Examples

Recursive functions

We can now detect recursive identities:

let rec listid = function
  | t::q -> t::(listid q)
  | [] -> []

Used to compile to:

End of middle end:
let_rec_symbol
  (camlTest__listid_5_closure
    (Project_closure (camlTest__set_of_closures_20, listid/5)))
  (camlTest__set_of_closures_20
    (Set_of_closures (
      (set_of_closures id=Test.11
        (listid/5 = fun param/7 ->
          (if param/7 then begin
            (let
              (apply_arg/13 (field 1<{../../test.ml:9,4-8}> param/7)
               apply_funct/14 camlTest__listid_5_closure
               Pmakeblock_arg/15
                 *(apply*[listid/5]<{../../test.ml:9,15-25}> apply_funct/14
                    apply_arg/13)
               Pmakeblock_arg/16 (field 0<{../../test.ml:9,4-8}> param/7)
               Pmakeblock/17
                 (makeblock 0<{../../test.ml:9,12-25}> Pmakeblock_arg/16
                   Pmakeblock_arg/15))
              Pmakeblock/17)
            end else begin
            (let (const_ptr_zero/27 Const(0a)) const_ptr_zero/27) end))
         free_vars={ } specialised_args={}) direct_call_surrogates={ }
        set_of_closures_origin=Test.1])))
let_symbol (camlTest (Block (tag 0,  camlTest__listid_5_closure)))
End camlTest

But is now detected as being the identity:

End of middle end:
let_symbol
  (camlTest__set_of_closures_20
    (Set_of_closures (
      (set_of_closures id=Test.13 (listid/5 = fun param/7 -> param/7)
        free_vars={ } specialised_args={}) direct_call_surrogates={ }
        set_of_closures_origin=Test.1])))
  (camlTest__listid_5_closure
    (Project_closure (camlTest__set_of_closures_20, listid/5)))
  (camlTest (Block (tag 0,  camlTest__listid_5_closure)))
End camlTest

Unsafe example

However, we can use the unsafety of the feature to go around the typing system and access a memory address as if it was an integer:

type bugg = A of int*int | B of int
let rec bug = function
  | A (a,b) -> (a,b)
  | B x -> bug (B x)
  
let (a,b) = (bug (B 42))
let _ = print_int b

This function will be simplified to the identity even though the bugg type is not compatible with tuples; trying to project on the second field of variant b will access an undefined part of memory:

$ ./unsafe.out
47423997875612

Possible improvements – short term

Function annotation

A theoretically simple thing to add would be to let the choice of applying unsafe optimizations to the user. We lacked the time to do the work of propagating the information to Flambda, but it would not be hard to implement.

Order on arguments

For a safer optimization, we could use the idea developed in the theoretical part to make the optimization correct on non-cyclical objects and more importantly give us typing guarantees to avoid the problem we just saw.

To get this guarantee, we would have to change the simplification pass by adding an optional pair of function-argument to the environment. When this option exists, the pair indicates that we are in the body in the process of simplification and that applications on smaller elements can be simplified as identity. Of course, the pass would need to be modified to remember which elements are not smaller than the previous argument.

Possible improvements – long term

Exclusion of cyclical objects

As described in the theoretical part, we could recursively deduce which objects are cyclical and attempt to remove them from our optimization. The problem is then that instead of having to replace functions by the identity, we need to add a special annotation that represents IdRec.

This amounts to a lot of added implementation complexity when compiling over several files, as we need access to the interface of already compiled files to know when the optimization can be used.

A possibility would be to use .cmx files to store this information when the file is compiled, but that kind of work would have taken too long to be achieved during the internship. Moreover, the practicality of that choice is far from obvious: it would complexify the optimization pass for a small improvement with respect to a version that would be correct on non-cyclical objects and activated through annotations.

About OCamlPro:
OCamlPro is a company founded in 2011, with the mission to help industrial users benefit from state-of-the art programming languages like OCaml and Rust. We design, create and implement custom ad-hoc software for our clients. We also have a long experience in developing and maintaining open-source tooling for OCaml, such as Opam, TryOCaml, ocp-indent, ocp-index, and ocp-browser, and we contribute to the core-development of OCaml, notably with our work on the Flambda optimizer branch. Another area of expertise is that of Formal Methods, with tools such as our SMT Solver Alt-Ergo (check our Alt-Ergo Users’ Club). We also provide vocational trainings in OCaml and Rust, and we can build courses on formal methods on-demand. Do not hesitate to reach out by email: contact@ocamlpro.com.

Introduction

MirageOS development focus has been a lot on tooling and the developer experience, but to accomplish our goal to "get MirageOS into production", we need to lower the barrier. This means for us to release binary unikernels. As described earlier, we received a grant for "Deploying MirageOS" from NGI Pointer to work on the required infrastructure. This is joint work with Reynir.

We provide at builds.robur.coop binary unikernel images (and supplementary software). Do…

Introduction

MirageOS development focus has been a lot on tooling and the developer experience, but to accomplish our goal to "get MirageOS into production", we need to lower the barrier. This means for us to release binary unikernels. As described earlier, we received a grant for "Deploying MirageOS" from NGI Pointer to work on the required infrastructure. This is joint work with Reynir.

We provide at builds.robur.coop binary unikernel images (and supplementary software). Doing binary releases of MirageOS unikernels is challenging in two aspects: firstly to be useful for everyone, a binary unikernel should not contain any configuration (such as private keys, certificates, etc.). Secondly, the binaries should be reproducible. This is crucial for security; everyone can reproduce the exact same binary and verify that our build service did only use the sources. No malware or backdoors included.

This post describes how you can deploy MirageOS unikernels without compiling it from source, then dives into the two issues outlined above - configuration and reproducibility - and finally describes how to setup your own reproducible build infrastructure for MirageOS, and how to bootstrap it.

Deploying MirageOS unikernels from binary

To execute a MirageOS unikernel, apart from a hypervisor (Xen/KVM/Muen), a tender (responsible for allocating host system resources and passing these to the unikernel) is needed. Using virtio, this is conventionally done with qemu on Linux, but its code size (and attack surface) is huge. For MirageOS, we develop Solo5, a minimal tender. It supports hvt - hardware virtualization (Linux KVM, FreeBSD BHyve, OpenBSD VMM), spt - sandboxed process (a tight seccomp ruleset (only a handful of system calls allowed, no hardware virtualization needed), Linux only). Apart from that, muen (a hypervisor developed in Ada), virtio (for some cloud deployments), and xen (PVHv2 or Qubes 4.0) - read more. We deploy our unikernels as hvt with FreeBSD BHyve as hypervisor.

On builds.robur.coop, next to the unikernel images, solo5-hvt packages (FreeBSD 12.2, Ubuntu 20.04) are provided - download the binary and install it. A NixOS package is already available - please note that soon packaging will be much easier (and we will work on packages merged into distributions).

When the tender is installed, download a unikernel image (e.g. the traceroute described in an earlier post), and execute it:

$ solo5-hvt --net:service=tap0 -- traceroute.hvt --ipv4=10.0.42.2/24 --ipv4-gateway=10.0.42.1

If you plan to orchestrate MirageOS unikernels, you may be interested in albatross - we provide binary packages as well for this (albatross FreeBSD and albatross Ubuntu 20.04). An upcoming post will go into further details of how to setup albatross.

MirageOS configuration

A MirageOS unikernel has a specific purpose - composed of OCaml libraries - selected at compile time, which allows to only embed the required pieces. This reduces the attack surface drastically. At the same time, to be widely useful to multiple organisations, no configuration data must be embedded into the unikernel.

Early MirageOS unikernels such as mirage-www embed content (blog posts, ..) and TLS certificates and private keys in the binary (using crunch). The Qubes firewall (read the blog post by Thomas for more information) used to include the firewall rules until v0.6 in the binary, since v0.7 the rules are read dynamically from QubesDB. This is big usability improvement.

We have several possibilities to provide configuration information in MirageOS, on the one hand via boot parameters (can be pre-filled at development time, and further refined at configuration time, but those passed at boot time take precedence). Boot parameters have a length limitation.

Another option is to use a block device - where the TLS reverse proxy stores the configuration, modifiable via a TCP control socket (authentication using a shared hmac secret).

Several other unikernels, such as this website and our CalDAV server, store the content in a remote git repository. The git URI and credentials (private key seed, host key fingerprint) are passed via boot parameter.

Finally, another option that we take advantage of is to introduce a post-link step that rewrites the binary to embed configuration. The tool caravan developed by Romain that does this rewrite is used by our openvpn router (binary).

In the future, some configuration information - such as monitoring system, syslog sink, IP addresses - may be done via DHCP on one of the private network interfaces - this would mean that the DHCP server has some global configuration option, and the unikernels no longer require that many boot parameters. Another option we want to investigate is where the tender shares a file as read-only memory-mapped region from the host system to the guest system - but this is tricky considering all targets above (especially virtio and muen).

Behind the scenes: reproducible builds

To provide a high level of assurance and trust, if you distribute binaries in 2021, you should have a recipe how they can be reproduced in a bit-by-bit identical way. This way, different organisations can run builders and rebuilders, and a user can decide to only use a binary if it has been reproduced by multiple organisations in different jurisdictions using different physical machines - to avoid malware being embedded in the binary.

For a reproduction to be successful, you need to collect the checksums of all sources that contributed to the built, together with other things (host system packages, environment variables, etc.). Of course, you can record the entire OS and sources as a tarball (or file system snapshot) and distribute that - but this may be suboptimal in terms of bandwidth requirements.

With opam, we already have precise tracking which opam packages are used, and since opam 2.1 the opam switch export includes extra-files (patches) and records the VCS version. Based on this functionality, orb, an alternative command line application using the opam-client library, can be used to collect (a) the switch export, (b) host system packages, and (c) the environment variables. Only required environment variables are kept, all others are unset while conducting a build. The only required environment variables are PATH (sanitized with an allow list, /bin, /sbin, with /usr, /usr/local, and /opt prefixes), and HOME. To enable Debian's apt to install packages, DEBIAN_FRONTEND is set to noninteractive. The SWITCH_PATH is recorded to allow orb to use the same path during a rebuild. The SOURCE_DATE_EPOCH is set to enable tools that record a timestamp to use a static one. The OS* variables are only used for recording the host OS and version.

The goal of reproducible builds can certainly be achieved in several ways, including to store all sources and used executables in a huge tarball (or docker container), which is preserved for rebuilders. The question of minimal trusted computing base and how such a container could be rebuild from sources in reproducible way are open.

The opam-repository is a community repository, where packages are released to on a daily basis by a lot of OCaml developers. Package dependencies usually only use lower bounds of other packages, and the continuous integration system of the opam repository takes care that upon API changes all reverse dependencies include the right upper bounds. Using the head commit of opam-repository usually leads to a working package universe.

For our MirageOS unikernels, we don't want to stay behind with ancient versions of libraries. That's why our automated building is done on a daily basis with the head commit of opam-repository. Since our unikernels are not part of the main opam repository (they include the configuration information which target to use, e.g. hvt), and we occasionally development versions of opam packages, we use the unikernel-repo as overlay.

If no dependent package got a new release, the resulting binary has the same checksum. If any dependency was released with a newer release, this is picked up, and eventually the checksum changes.

Each unikernel (and non-unikernel) job (e.g. dns-primary outputs some artifacts:

• the binary image (in bin/, unikernel image, OS package)
• the build-environment containing the environment variables used for this build
• the system-packages containing all packages installed on the host system
• the opam-switch that contains all opam packages, including git commit or tarball with checksum, and potentially extra patches, used for this build
• a job script and console output

To reproduce such a built, you need to get the same operating system (OS, OS_FAMILY, OS_DISTRIBUTION, OS_VERSION in build-environment), the same set of system packages, and then you can orb rebuild which sets the environment variables and installs the opam packages from the opam-switch.

You can browse the different builds, and if there are checksum changes, you can browse to a diff between the opam switches to reason whether the checksum change was intentional (e.g. here the checksum of the unikernel changed when the x509 library was updated).

The opam reproducible build infrastructure is driven by:

• orb conducting reproducible builds (packages FreeBSD, Ubuntu 20.04)
• builder scheduling builds in contained environments (packages FreeBSD, Ubuntu 20.04)
• builder-web storing builds in a database and providing a HTTP interface (packages FreeBSD)

These tools are themselves reproducible, and built on a daily basis. The infrastructure executing the build jobs installs the most recent packages of orb and builder before conducting a build. This means that our build infrastructure is reproducible as well, and uses the latest code when it is released.

Conclusion

Thanks to NGI funding we now have reproducible MirageOS binary builds available at builds.robur.coop. The underlying infrastructure is reproducible, available for multiple platforms (Ubuntu using docker, FreeBSD using jails), and can be easily bootstrapped from source (once you have OCaml and opam working, getting builder and orb should be easy). All components are open source software, mostly with permissive licenses.

We also have an index over sha-256 checksum of binaries - in the case you find a running unikernel image where you forgot which exact packages were used, you can do a reverse lookup.

We are aware that the web interface can be improved (PRs welcome). We will also work on the rebuilder setup and run some rebuilds.

Please reach out to us (at team AT robur DOT coop) if you have feedback and suggestions.

Tarides is excited to announce that our CEO, Dr. Thomas Gazagnaire, and Prof. Anil Madhavapeddy, from the University of Cambridge, will present their innovative platform OSMOSE at the Open Source Innovation Sprint (OSIS) conference on 1 July 2021. This event is organized by Systematic.

OSMOSE is a software platform made to manage digital infrastructure at scale, securely and efficiently. It uses the groundbreaking creation of unikernels to radically simplify the way applications are built and de…

Tarides is excited to announce that our CEO, Dr. Thomas Gazagnaire, and Prof. Anil Madhavapeddy, from the University of Cambridge, will present their innovative platform OSMOSE at the Open Source Innovation Sprint (OSIS) conference on 1 July 2021. This event is organized by Systematic.

OSMOSE is a software platform made to manage digital infrastructure at scale, securely and efficiently. It uses the groundbreaking creation of unikernels to radically simplify the way applications are built and deployed for the cloud.

Since digital transformation has become more and more dependent on cloud computing, it has increasing problems with high response latency, security risks, and resource inefficiencies—all which make these services ultimately unreliable. The demand for interconnected devices is ever increasing, but the security of these devices remain unchecked, making them susceptible to security vulnerabilities. This leaves consumers and businesses open to exploitation, as demonstrated in reports of tech devices violating users’ privacy, like sending audio recordings without their knowledge or consent.

Tarides addresses these issues with OSMOSE, a platform which combines hardware and software elements to invert the current cloud-centric model. OSMOSE securely connects with physical spaces to provide extremely low latency and high-bandwidth, local-area computation capabilities, which can turn a fleet of IoT devices into a local data-centre.

This innovative platform enables computer resources to be tracked efficiently and temporarily rented to users. This turns any IoT deployment into a local, private cloud, allowing a better utilization of local resources and improved security.

Major components of OSMOSE already have commercial applications. It’s been used to make existing cloud deployments more secure and efficient by companies such as Amazon, Citrix, and Docker.

Tarides applies a high-touch, mixed business strategy—using consultancy services to field test open source components under development. Tarides applies their research to real-world systems to build unikernels, a secure-by-design and resource-efficient application specialised to their run-time environments. If interested in using OSMOSE as a solution for your business, please reach out to Tarides for more information.

Register for OSIS to attend the OSMOSE presentation on 1 July 2021.

Feedback on this post is welcomed on Discuss!

The opam team has great pleasure in announcing opam 2.1.0~rc2!

The focus since beta4 has been preparing for a world with more than one released version of opam (i.e. 2.0.x and 2.1.x). The release candidate extends CLI versioning further and, under the hood, includes a big change to the opam root format which allows new versions of opam to indicate that the root may still be read by older versions of the opam libraries. A plugin compiled against the…

Feedback on this post is welcomed on Discuss!

The opam team has great pleasure in announcing opam 2.1.0~rc2!

The focus since beta4 has been preparing for a world with more than one released version of opam (i.e. 2.0.x and 2.1.x). The release candidate extends CLI versioning further and, under the hood, includes a big change to the opam root format which allows new versions of opam to indicate that the root may still be read by older versions of the opam libraries. A plugin compiled against the 2.0.9 opam libraries will therefore be able to read information about an opam 2.1 root (plugins and tools compiled against 2.0.8 are unable to load opam 2.1.0 roots).

Please do take this release candidate for a spin! It is available in the Docker images at ocaml/opam on Docker Hub as the opam-2.1 command (or you can sudo ln -f /usr/bin/opam-2.1 /usr/bin/opam in your Dockerfile to switch to it permanently). The release candidate can also be tested via our installation script (see the wiki for more information).

Thank you to anyone who noticed the unannounced first release candidate and tried it out. Between tagging and what would have been announcing it, we discovered an issue with upgrading local switches from earlier alpha/beta releases, and so fixed that for this second release candidate.

Assuming no showstoppers, we plan to release opam 2.1.0 next week. The improvements made in 2.1.0 will allow for a much faster release cycle, and we look forward to posting about the 2.2.0 plans soon!

Try it!

In case you plan a possible rollback, you may want to first backup your ~/.opam directory.

The upgrade instructions are unchanged:

1. Either from binaries: run

   bash -c "sh <(curl -fsSL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh) --version 2.1.0~rc2"

   or download manually from the Github "Releases" page to your PATH.

2. Or from source, manually: see the instructions in the README.

You should then run:

opam init --reinit -ni

We hope there won't be any, but please report any issues to the bug-tracker. Thanks for trying it out, and hoping you enjoy!