These posts broadly discusses induction as a formal verification technique, which here really means formal program verification. I will use concrete, runnable examples whenever possible. Some of them can run directly in a browser, while others require to run small easy-to-retrieve tools locally. Such is the case for pretty much all examples dealing dir…
These posts broadly discusses induction as a formal verification technique, which here really means formal program verification. I will use concrete, runnable examples whenever possible. Some of them can run directly in a browser, while others require to run small easy-to-retrieve tools locally. Such is the case for pretty much all examples dealing directly with induction.
The next chapters discuss the following notions:
formal logics and formal frameworks;
SMT-solving: modern, low-level verification building blocks;
declarative transition systems;
transition system unrolling;
BMC and induction proofs over transition systems;
candidate strengthening.
The approach presented here is far from being the only one when it comes to program verification. It happens to be relatively simple to understand, and I believe that familiarity with the notions discussed here makes understanding other approaches significantly easier.
This book thus hopes to serve both as a relatively deep dive into the specific technique of SMT-based induction, as well as an example of the technical challenges inherent to both developing and using automated proof engines.
Some chapters contain a few pieces of Rust code. Usually to provide a runnable version of a system under discussion, or to serve as example of actual code that we want to encode and verify. Some notions of Rust could definitely help in places, but this is not mandatory (probably).
In April, we announced that the DAPSI initiative accepted
the proposal for our Secure-by-Design Communication Protocols (SCoP) project. Today, we are thrilled to announce that SCoP has passed the initiative’s Phase 1,
and we are now on our way to Phase 2!
SCoP is an open, secure, and resource-efficient infrastructure to engineer a modern basis for open messaging (for existing and emerging protocols)
using type-safe languages and unikernels—to ensure your private information remains secure. A…
In April, we announced that the DAPSI initiative accepted
the proposal for our Secure-by-Design Communication Protocols (SCoP) project. Today, we are thrilled to announce that SCoP has passed the initiative’s Phase 1,
and we are now on our way to Phase 2!
SCoP is an open, secure, and resource-efficient infrastructure to engineer a modern basis for open messaging (for existing and emerging protocols)
using type-safe languages and unikernels—to ensure your private information remains secure. After all, you wouldn’t like your postal carrier reading
your snail mail, so why should emails be any different?
Challenges
To operate an email service requires many technical skills and reliable infrastructure. As a result, only a few large companies can handle emails with
the proper security levels. Unfortunately, the core business model of these companies is to mine your personal data.
The number of emails exchanged every day is expected to reach 333 billion in 2022. That’s a considerable amount of data, much of it private or sensitive,
sent across Cyberspace through portals with questionable security. The ‘memory unsafe’ languages used in most communication services leave far too much room
for mistakes that have serious ramifications, like security flaws that turn into security breaches, leaving your personal or business information vulnerable to
malicious hackers.
Due to this global challenge, we set out to build a simple, secure, easily deployable solution to preserve users' privacy, and we’re making great strides toward
accomplishing that goal. We base our systems on scientific foundations to last for decades and drive positive change for the world. Our robust understanding of
both theory and practice enables us to solve these security problems, so we explore ideas where research and engineering meet at the intersection of the domains
of operating systems, distributed systems, and programming languages.
Every component of SCoP is carefully designed as independent libraries, using modern development techniques to avoid the common reported threats and flaws.
For instance, the implementation of protocol parsers and serializers are written in a type-safe language and tested using fuzzing. Combining these techniques
will increase users' trust to migrate their personal data to these new, more secure services.
Architecture
The architecture of the SCoP communication service is composed of an Email Service based on a secure extension of the SMTP protocol, and a decentralised
real-time communication system based on Matrix.
The SMTP and Matrix protocols implemented in SCoP follow the separation of
concerns design principle, meaning that the SMTP Sender and SMTP Receiver are designed as two distinct units. They’re implemented as isolated micro-services
which run as unikernels. The SMTP Sender, Receiver, and Matrix are all configurable, and each configuration comes with a security risk analysis report to
understand possible privacy risks
Progress
Not only are we on our way to Phase 2 in the DAPSI Initiative, but we’re also proud to report that we’re on track with our
planned milestones!
Our first milestone was to generate a corpus of emails to test our parser implementation against existing projects in order to detect differences
between the descriptions specified in the RFCs. We now have 1 million emails that have been parsed/encoded without any issues! Our email corpus keeps
isomorphism between the encoder and decoder, and you can find it in this GitHub Repo, as we encourage implementors of other languages to use it to improve
their trust in their own implementation.
We set out to implement an SMTP extension mechanism and support for SPF as well as implement DMARC, a security framework, on top of DKIM and SPF for our
second milestone, and we are right on target. To date, we’ve completed four components:
MrMIME can generate the email, then SMTP sends the email (signed by a DKIM private key). We can correctly sign an email, generate a signature, and the DKIM field containing the signature. When the email is received, we check the DKIM signature and the SPF metadata.
For our third milestone, we set out to implement DNSSEC, a set of security extensions over DNS. This security layer verifies the identity of an email sender
through DKIM/SPF/DMARC, but it also needs security extensions in the DNS protocol. We completed our initial investigation of a DNSSEC implementation prototype,
and we discovered several issues, like some of the elliptic curve cryptography was missing. Those necessary cryptographic primitives are now available, so we
should complete this milestone by the end of the month.
Finally, our fourth milestone was to implement the Matrix protocol (client and server). We completed the protocol’s client library, which sends a notification
from OCaml CI. Plus, we have a PoC, and Matrix’s server-side, which received the notification, is also complete.
Although we still have much work ahead of us, we’re quite pleased with the progress thus far, and so is the DAPSI Initiative! Follow our progress by subscribing
to this blog and our Twitter feed (@tarides_) for the latest updates.
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.
The last upgrade of the Tezos protocol, Granada, activated on August 6th, 2021.
We are now glad to announce a new protocol proposal, Hangzhou, the result of a
collaborative work from various teams.
It can be tricky to evaluate the effect of invidual commits or pull requests on
the speed of the OCaml compiler. In this blog post, I (Florian Angeletti) report my
experience on measuring such impact with some degree of statistical significance.
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…
It can be tricky to evaluate the effect of invidual commits or pull requests on
the speed of the OCaml compiler. In this blog post, I (Florian Angeletti) report my
experience on measuring such impact with some degree of statistical significance.
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
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.
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
Relative change in average typechecking time by files
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
Relative change in average non-typechecking time by files
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)
Relative change in average total time by files
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:
Typechecking average
Other average
Total average
1.06641
1.01756
1.03307
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
Typechecking geometric average
Other geometric average
Total geometric average
1.05963
1.01513
1.03215
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)
Typechecking median
Other median
Total media
1.03834
1.00852
1.02507
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
Quantiles of the relative change of average typechecking time by files
%
mean quantiles
1%
0.875097
10%
1
25%
1.001
50%
1.03834
75%
1.08826
90%
1.162
99%
1.51411
99.9%
2.76834
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
Quantiles of the relative change in average total time by files
%
total quantiles
1%
0.945555
10%
1
25%
1.00707
50%
1.02507
75%
1.05
90%
1.07895
99%
1.17846
99.9%
1.4379
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
Quantiles of the relative change in average non-typechecking time by files
%
other quantiles
1%
0.855129
10%
0.956174
25%
0.995239
50%
1.00852
75%
1.03743
90%
1.08618
99%
1.25541
99.9%
1.67784
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:
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:
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),
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:
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
(/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
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
Relative change in minimal typechecking time by files
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
Relative change in minimal total time by files
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
Typechecking
Other
Total
Average
1.06907
1.01031
1.02901
Geometric average
1.05998
1.00672
1.0276
Median
1
1
1
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,
Quantiles of the relative change in minimal typechecking time by files
%
min quantiles
1%
1
10%
1
25%
1
50%
1
75%
1.07692
90%
1.2
99%
2
99.9%
2
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,
Quantiles of the relative change in minimal non-typechecking time by files
%
min_other quantiles
1%
0.8
10%
0.947368
25%
1
50%
1
75%
1
90%
1.11111
99%
1.33333
99.9%
1.6
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,
%
min_total quantiles
1%
0.92
10%
1
25%
1
50%
1
75%
1.04545
90%
1.1
99%
1.22727
99.9%
1.4
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:
Relative time spent in typechecking 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
Arithmetic average
Median
38.8827%
39.7336%
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)
Quantiles of the relative time spent in typechecking by files
%
profile quantiles
1%
0.111556
10%
0.16431
25%
0.283249
50%
0.397336
75%
0.487892
90%
0.573355
99%
0.749689
99.9%
0.913336
and on the histogram of the relative time spent in typechecking
Histogram of the relative time spent in typechecking by files
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,
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
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.,
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,
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,
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,
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),
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.,
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,
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,
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,
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
(defmacrofoo(xxs)...)
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,
(msg"we have $0 registers"(lengthr1r2r3r4r5r6r7r8))
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,
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 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.,
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(targetarm)))
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,
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.,
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,
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
}
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.
(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:
$ 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.
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):
~/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):
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:
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.
$ 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:
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.
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.
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.
We recently restructured our standard libraries at Jane Street in a
way that eliminates the difference between Core_kernel and Core
and we’re happy with the result. The new layout should reach the open
source world before the end of the year.
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 ocurrent1, 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:
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-benchhere!
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](https://icfp21.sigplan.org/program/program-icfp-2021/?past=Show
upcoming events only&date=Fri 27 Aug 2021) 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.
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!
It’s the end of another dev internship season, and this one marked
something of a transition, since halfway through the season, NY-based
interns were invited back to the recently reinvigorated office. Which
means that many more of us got the chance to meet and hang out with
the interns in person than we did last year. And hopefully the
interns were able to get a better sense of Jane Street and how it
operates.
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 usingproject.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:
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 packagebuild: 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:
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.
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.
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]
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]
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.
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 usingproject.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:
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 packagebuild:
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.
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 --…
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]
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.
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.
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.
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.
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.
For a recent project we wrote a compiler that translates a
domain-specific language (DSL) to some runnable form, and we did
that in OCaml. The DSL is now part of an Electron-based integrated
development environment (IDE) that will soon be available
from Remix Labs. Electron runs
on a couple of operating systems, but the DSL compiler orginally did
not. How do we accomplish it to run the DSL compiler on as many
different opera…
For a recent project we wrote a compiler that translates a
domain-specific language (DSL) to some runnable form, and we did
that in OCaml. The DSL is now part of an Electron-based integrated
development environment (IDE) that will soon be available
from Remix Labs. Electron runs
on a couple of operating systems, but the DSL compiler orginally did
not. How do we accomplish it to run the DSL compiler on as many
different operating systems? This was the question we faced when
starting the development of WasiCaml, a translator from OCaml
bytecode to WebAssembly.
Of course, Electron is just an example of a cross-platform
environment. You can develop apps for Mac, Windows, and Linux, and
it is Javascript-based. We picked Electron for porting the user
interface of the IDE to the desktop - originally the IDE was written
for the web, and the DSL compiler was running on a server backing
the web app. Initially, the Electron version of the IDE started just
a native binary of the DSL compiler as a server process that ran in
the background, just like we did it for the web, but this means that
you run into the cross-build problem again that you actually want to
avoid by running something in Electron: we would have needed to set
up several build pipelines, one for each OS, in order to build the
DSL compiler for the targets we wanted to support.
There are already tools to translate OCaml to Javascript (namely
Bucklescript and js_of_ocaml), and we could have used these to fiddle
the DSL compiler into the Javascript code base. However, this does
not feel right: we would have had to reorganize the OCaml code base
because you can't link in C libraries, and driving the DSL compiler
would have been quite adventurous (it talks via a bidirectional
pipeline to its clients). At that time we were already exploring
WebAssembly for other parts of the system, and the idea came up
to also use WebAssembly for running the DSL compiler. The
WasiCaml
project was born (and the translation to Javascript only plan B
should this turn out to be more difficult than expected).
A quick intro to WebAssembly
As the name suggests, WebAssembly provides a fairly low-level virtual
machine for running the code. The instructions are comparable to the
ones you find in a CPU, e.g. load, store, arithmetic. The code is
structured into functions which take a fixed number of parameters
and return a single result. The functions can have local variables
that can be read and written by the code. The parameters and variables
can have one of four numeric types (i32, i64, f32, and f64).
For example, this is a WebAssembly module with just one function that
increments a 32 bit number at a memory location by one, and returns
the value:
Here, the code is given in the textual format known as WAT. For running
it, you first need to convert it to the binary format (WASM), e.g.
with a tool like wat2wasm.
Also note that there is an operands stack: local.get pushes
the result on this stack, and i32.load loads the number
from the address found on the stack, and also pushes the result on the
stack. This stack is mainly meant to express the code in a very compact
way. The engine running code normally translates the stack operations
into a more efficient form before starting up.
A WebAssembly VM is equipped with linear memory, i.e. the memory
addresses go from 0 to a maximum address, without fragmentation, and
without address ranges supporting special semantics like mapped files. The
memory is only used for data - the running code is inaccessible
(i.e. the VM has a Harvard architecture), and this also includes the
call stack and other parts of the VM (e.g. you cannot iterate over
the local variables of the functions). In order to also support
indirect jumps, there is a way to reference functions by numeric
IDs.
Typically, WebAssembly VMs translate the code to the native
instruction set of the host running of code before running the code
(often as JIT compilers, but there are now also engines doing the
translation statically ahead of time, and producing native binaries),
and these engines almost reach native speed. All current browsers support
WebAssembly now, and it is also present in other Javascript-based
environments (like node, or the Electron platform). Although it
started as a web technology, WebAssembly is not limited to the web.
For example, wasmtime
allows you to embed a WebAssembly engine into almost any environment
- e.g. you could embed the engine into an application server written
in Go. In this case, there is no Javascript involved at all.
WASI
While the WebAssembly standard defines how to express the code and
how to run it, there is still the question how to use it with
popular languages like C, and
Rust. The WASI standard is an ABI
that answers a lot of the questions. As an ABI it defines calling
conventions, but it is not limited to that. In particular, there is
a version of libc that defines a Unix-like set of base functionality
the language-specific runtime can use. Also, WASI defines a set of host
functions that play a role comparable to system calls in the WebAssembly
world, and that allow access to files, the process environment, and
the current time. With the help of WASI you can compile many C
or Rust libraries to WebAssembly, and the porting effort is low.
WASI is multi-lingual environment, and you can in particular link
code written in different languages into the same executable. This is
possible because the language-specific runtimes have a common foundation
(libc), and e.g. memory allocated from one language also counts as
"taken" within the other language.
WASI is still in an early stage. While developing with it I discovered
a couple of bugs, but the functionality is already impressive and
usable for many purposes.
WasiCaml
So now, what is WasiCaml, and how can I use it?
Let's assume you have a bytecode executable created by something like
ocamlc -o myexecutable mycode.ml
Now, you can further translate the bytecode executable to WebAssembly:
wasicaml -o mywasm.wasm myexecutable
If you want to run this executable, you need a specially configured
WebAssembly engine which can be found in ~/.wasicaml/js after installation:
Of course, the C library must also be WASI-compatible.
Note that WasiCaml-produced code can so far not be run with
wasmtime or wasmer, in particular because there is no machinery
for exception handling in these engines. Browsers are fully
supported, though.
The WasiCaml project
WebAssembly is still a very new technology and information about it
is rare. For example, it took a while until I understood that LLVM
includes a full-featured assembler for WebAssembly, i.e. you can feed
it a code.s file, and you get a code.o
file back with partially linked WebAssembly code. This is documented
nowhere, and I could only figure out some parts of the assembler syntax
by reading the source code of LLVM.
What I already knew from an earlier WebAssembly project is that
there is no exception handling (EH) mechanism yet in the standard
(although this will likely change soon). This turned out as a
special problem for WasiCaml, because the OCaml runtime uses long
jumps in external C code to trigger OCaml exceptions. I remembered
the way the Emscripten
toolchain (which is another wrapper around LLVM) gets around this
difficulty. If the host language is Javascript, embedded
WebAssembly code is compiled to run in the same VM that is also used
to execute Javascript itself, and this means that Javascript exceptions
also work perfectly for WebAssembly! Of course, this trick is
really limited to Javascript hosts, but at least I could remove
the blocker for one of the possible execution environments.
The very first task was then to get the OCaml bytecode interpreter
working in a WASI (plus EH) environment.
Milestone: running the bytecode interpreter in the WASI environment
Essentially, this means that I wanted to (1) clone the OCaml source
code, (2) configure it, and (3) make the
bytecode interpreter (and the whole OCaml bytecode toolchain). The
C compiler comes from the
WASI SDK,
and it compiles directly to WebAssembly. Now, if you just set the
CC variable to this C compiler, configure
will consider the target as a cross-compile target. Such targets
are still very tricky, and - because we actually can run
the code somehow - I thought it is better to avoid cross-compilation
altogether, and to add some tooling so that binaries are
directly runnable.
Instead of pointing CC directly to the C compiler of
the WASI SDK, there is now a wrapper script wasi_cc.
The main purpose of this script is to reshape the WebAssembly
executables so that they are directly runnable on the host
system. This is accomplished by prepending a starter to the
WebAssembly code. The starter runs node with
the right driver script, and extracts the WebAssembly code from the
executable file. For example, if you do
wasi_cc -o ex code.c
the resulting file ex can be directly run with
./ex.
With this trick, configure now "thinks" that the
target is a native target of the operating
system. configure could also run the tests on the
existence of the various libc library functions the OCaml runtime
needs, and figured out a lot of that stuff correctly. Nevertheless,
not everything was working, and I had to fork the OCaml sources in
order to disable functions that are not available
(see gerd/wasi-4.12.0
for the changes).
In this branch of OCaml I also changed the main function of the
bytecode interpreter so that it catches exceptions from Javascript
(actually, this function was split into two, and the outer function
catches the exception thrown by the inner function).
A final difficulty was that function pointers in WebAssembly are typed
- which is a logical consequence of the fact that functions are typed.
OCaml generates a file prims.c that initializes the list
of FFI functions, and initially LLVM did not like this file, because
it could not infer the types of the function pointers. The solution
was not to generate WebAssembly for this single file but
to leave it as LLVM IR ("bitcode"). In this format function pointers
can remain untyped, and the LLVM linker is smart enough to fix up
the problem at link time, and to convert LLVM IR to WebAssembly when
the types of the FFI functions are known.
With this trick, everything worked fine! The speed of the bytecode
interpreter did not slow much down in WebAssembly, which was very
encouraging.
Milestone: the direct translator
After the bytecode interpreter was running, the second step was to
directly generate WebAssembly code from OCaml. Actually, there were
two choices: either to pick up one of the internal formats of OCaml
(e.g. "Lambda" or "C--") and to change the OCaml compiler directly,
or to take the bytecode as the starting point. I preferred the
latter because WasiCaml is then an add-on processor that can be
easily added to existing OCaml projects, and because some
difficulties could be avoided (e.g. incremental compilation, and
many many fixups through the whole toolchain). Also, I hoped that
the resulting speed would still be "good enough" (at least for the
purposes of the DSL compiler we wanted to run with WebAssembly).
Also, bytecode made it also a lot easier for me to get started.
There were really a lot of unanswered questions: what does the
function call mechanism look like? How do we get around the problem
that OCaml code typically requires tail calls to be working but
there aren't tail calls in WebAssembly (yet)? What does the code
look to allocate a block of memory? How do we emulate exceptions?
Picking bytecode meant that I could focus on these questions, while
the bytecode instructions could initially be translated in a naive
way, e.g. by translating each bytecode instruction separately to a
fixed block of WebAssembly instructions (like instantiating a
template). (Note that the current WasiCaml compiler is already
a lot better than that.)
Picking bytecode also meant that WasiCaml inherits the bytecode
stack. This is actually not a bad thing - because of OCaml's memory
management the stack must reside in addressable memory, and the
bytecode stack could serve as what the WebAssembly community calls
a shadow stack. (Even for the C language there is a
shadow stack - and the alternative would have been to also use the
shadow stack of the C language.) So we got the shadow stack for
OCaml code practically for free.
The stack is important because the garbage collector must be
able to run over all locations where OCaml values are stored.
As already mentioned, the locations WebAssembly natively supports
cannot be traversed over (like local and global variables), and
hence it is crucial to put OCaml values into memory whenever there
is the chance of a garbage collector run.
Note that the native OCaml compiler is not much different in this
respect - only that the native stack of the operating system can be
used for storing values because it resides in memory. The details
are different, though. When a value is moved temporarily to the
stack, this is usually called "register spilling", and this is done
because (1) there is only a limited amount of registers, but another
register is needed, or (2) you don't know which register remains
untouched when you call a function, or (3) you call some code that
may run the garbage collector. Now, in WebAssembly, reason (1) is
never the case because there can be any number of local variables
(which take over the role of registers), and the details of (3) are
very different, because in a native environment the registers are
global stores, permitting some time-saving tricks that are
unavailable in WebAssembly.
So, for developing the WasiCaml code emitter, this meant that it
had to follow constraints so that OCaml values end up on the stack
in the right moment. Actually, these constraints mainly shaped the
layout of the WasiCaml code.
32 bit comes back!
Once WasiCaml was working, we got back to the DSL compiler we
originally wanted to make cross-platform. And we actually got it
running! There was one remaining problem, though: WebAseembly is a
32 bit environment. As you may know, OCaml suffers from some
limitations in this case. Most annoyingly, strings can only be 16 MB
in size at most.
Fortunately, this problem occurred only here and there, mostly
in the code emitter. Here, we could switch to
ropes
as alternate representation - and, lucky as we were, it turned
out that this change did not eat much performance.
The DSL compiler is quite big, and the WebAssembly version takes
around 3 seconds to start up. This is longer than usual, but for
our application we could hide the startup time, and are now quite
happy with the product.
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…
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:
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:
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.
Hiring a Developer Educator — Jane Street, Oct 21, 2021
).
