Flambda2 Ep. 5: Strict Boolean Ifs

---

Welcome to a new episode of The Flambda2 Snippets!

The F2S blog posts aim at gradually introducing the world to the inner-workings of a complex piece of software engineering: The Flambda2 Optimising Compiler for OCaml, a technical marvel born from a 10 year-long effort in Research & Development and Compilation; with many more years of expertise in all aspects of Computer Science and Formal Methods.

Today, we are doing something a little different than usual. Indeed, all previous F2S deal with an aspect of the functioning of the compiler. Either how some optimizations are led, to front facing features like Loopify which allow our users to benefit from efficient tail-recursive calls.

The point of today's topic is not inherently technical, but is rather about how people handle technicalities together. We are going to cover a broader subject around how IRs, and their semantics evolve. We are going to see how their lifecycles are driven by social interactions and many other considerations.

We will illustrate today's topic by breaking down the context of this PR. We will eventually dive into the social questions that such lifecycles pose but first we'll introduce the technical context of language semantics and then elaborate on the specific technicalities of this PR.

We suggest to our readers to skip over the sections that they are less interested in and to use the Table of Contents to navigate the article.

The semantics of Intermediate Representations

So what do we mean by "semantics" in this context ?

Semantics is what gives a program its meaning.

The simplest kind of semantics we can think of would be a way to describe the mathematical function that, for a given correct program, links its parameters to its results.

Obviously, one can see how this description alone is not enough. There are just so many more things one may want to say about a program's behaviour.

• What happens when the program is incorrect?
• What about side effects: printing, system or user interactions?
• Does a program terminate, and does it do something when it does not terminate?
• Non-determinism, is there a single possible result of a given program?
• Partial programs: what can we say about a single function without main?
• Execution time, resource consumption: when does it terminate in practice? Will it blow the memory?
• Precise memory layout: where are the bits in memory during execution?
• and so on...

One may or may not want to specify one or several of these to different levels of rigor depending on the context.

Let's take Fibonacci as an example.

int fibonacci(int n) {
    if (n == 0)
        return 0;
    if (n == 1)
        return 1;
    return fibonacci(n - 1) + fibonacci(n - 2);
}

The most basic property of this function is that it should compute Fibonacci numbers.

Choosing to implement it in C, which has its own specification, already implies a lot of semantic properties. For example, using type int limits the range of representable values. On one hand, this guarantees that the function will return valid values for some sufficiently small parameters. On the other hand, this also guarantees that the function result will not be the expected mathematical result for larger arguments.

That's all the information that you need when the function call is correct in a non-buggy program.

You may have noticed that our function does not reject negative numbers. However, the Fibonacci sequence is not defined for negative indices. On paper, this is the correct way to implement this function, however the C compiler still has to decide what to do when the number is negative. You could consider this a second level of semantics because the compiler will have more precise semantics than our mathematical model, and that is fine as long as they are consistent with one another.

This specific function can consume resources. The most obvious would be stack memory. Computers have finite stack memory and recursive calls tend to consume stack space. This means that this function could exhaust the stack in some specific contexts, for instance if it was called under a sufficiently deep stack. If we look at this function independently from that context, however, the behaviour is non-deterministic. So even if we call the function with a valid value, it is possible that the function will not produce the correct result even though the function looks completely deterministic.

The naïve implementation we provided, has exponential complexity. It is possible to write a function that computes the same results more efficiently, with linear complexity. Our simple initial semantics allows the compiler to choose a more efficient implementation than the one we provided, or even a worse one.

When does it matter to establish the details of the semantics?

The previous section explained why it's important for the programmers and languages developers to agree on the semantics. It's also important for compiler developers to agree on the semantics of the different parts of the compiler.

Like many a French researcher in Formal Verification, we will resort to space crash analogies to illustrate our point.

See, in 1999, the Mars Climate Orbiter Space probe crashed on the surface of the red planet. After a detailed analysis of the events that led to it, NASA discovered an unfortunate misunderstanding between its teams and their contractor's engineers. Indeed, some software was expected to compute some thrust in SI units but instead returned it in Imperial units which is wrong by a factor of 4.45... While at a lesser scale, compiler development involves teams of people working independently, which makes the specification of the different parts of the compiler necessary.

While everybody agrees that a specification is required, what to put in it is a different story. A strict specification helps everybody agree on what exactly is happening in the code, but narrows the potential future evolutions. Also compiling and running a program involves many moving pieces, and writing down precisely what is happening (taking into account how a CPU works for real) might be as obscure as reading the code of the compiler itself.

So, back to the OCaml compiler. As its developers, we want to transform programs while preserving semantics. When writing these transformations, knowing what is and isn't part of the semantics is important.

Here are a few examples that might appear counter-intuitive at first but that show that there is a large set of properties that might or might not be relevant.

1. Resource consumption can be part of the expected specification

Let's take the example of tail-call optimisation. The Wasm Committee has specified that TCO would not be permitted in Wasm because they want to enforce consistency between the different implementations. A program with too many recursive calls should StackOverflow on every platform indiscriminately.

2. Memory layout can be part of the expected specification

When memory layout is not part of the specification, you have more ways to optimise a given program. However when debugging, having a reliable and fixed memory layout is necessary. This means that supporting debugging creates more complexity in the compiler code.

3. Complexity can be part of the expected specification

In cryptography, some programs aim to be protected against side-channel attacks. One of these side-channels is execution time. This means that these programs rely on the consistent execution time for all the individual instructions.

Let's look at an example through this discussion on the LLVM mailing list. This mail describes a problem encountered by engineers writing cryptographic primitives. There were functions that they would have preferred to write in C for the sake of simplicity rather than assembly. However the LLVM sometimes optimises a specific code pattern. This optimisation shortcutted some computations depending on the values. Simply put, this broke the constant-time properties that these engineers needed by producing opportunities for side-channel attacks. That optimisation is generally a good choice for the majority of users, so removing it was out of the question. For the curious ones out there: this is code exposed to side-channel attacks. This example shows an instance of incompatible compiler specification and user requirements.

IR Evolution

An example of an arduous lifecycle that we wanted to cover was that of the fine details of Undef and Poison in LLVM.

This is probably one of the most complex instances of IR evolutions out there. LLVM is a huge codebase, developed by thousands of engineers, and almost everybody carries in their pocket some code compiled with it. The nature of the proposed evolution was complex in itself, among all those that had been suggested up to that point.

For reference, see this presentation: Undef and Poison: Present and Future. It is one of the most complex IR changes ever undertaken, carried out over a long period of time. In hindsight, it clearly illustrates the very complex nature of designing an IR change in an already very large and widely used codebase. Despite a large group of developers, converging on a satisfactory solution was laborious.

Making decisions about IR evolution can drastically change things for a significant portion of users. At that point, the discussion shifts towards formalising or specifying certain behaviours to get these suggestions adopted, and the subject becomes more social in nature.

In practice, developers have a mental representation of the semantics of intermediate languages. Obviously, each mental image differs from person to person, and they can even be incompatible with one another. However, they remain compatible with the implementation, and these incompatibilities are not observable until some edge case reveals them (a satellite crash, for example).

A mental image necessarily starts out naively, since it's generally based on what has been written about the semantics—but a complete semantics is usually too complex to be written down entirely. In a software project, if you don't write a proper semantics, the existing code becomes the only semantics, and that causes problems.

Faced with all these potential issues, there are two paths that compiler developers can take to evolve an IR while limiting the damage:

1. Replicate and modify: Duplicate the piece of semantics, changing it slightly in problematic cases. This preserves the old behaviour but is complex because it requires correctly tracking all the places to change, as well as updating the mental models of developers who were using it before.

2. Modify in place: Change the existing construct directly. This is more drastic and risky, but it doesn't add complexity to the language and is easier to track.

Technical Context: The Semantics of If

In the Lambda IR of the OCaml compiler, the if conditional was not required to be a boolean. It was similar to that of C. Its semantics was that, if the value of the conditional was 0 the false branch was to be taken, and in any other case, the true branch was taken instead. This made it rather straightforward to compile efficiently as it matches the usual semantics of C.

Here are a few examples of what that would look like in different representations:

(* in OCaml *)
if cond then case1 else case2

(* in Lambda IR *)
(if cond case1 case2)

/* in asm */
    cmpq    $1, %rax
    je  .LBL_ELSE
    /* Not equal: case1 */
    movq    %rbx, %rax
    ret
.LBL_ELSE:
    /* Equal: case2 */
    movq    %rdi, %rax
    ret

Since the source language uses boolean values for conditions, at some point the compiler IRs will have to switch from one semantics to the other.

We will call Strict Boolean If the version of the semantics that can be found in the source language, where conditions can only be either true or false, and not any other value. We will call Generalized If the version of the semantics where only the single value 0 is considered false, and any other value is considered true.

In older versions of OCaml, the translation was done very early. In particular, as mentioned earlier, the Lambda IR used to follow the Generalized If semantics. This allowed the bytecode compiler to benefit from a few optimisations including the following one:

(* in OCaml *)
let is_non_empty list =
  match list with
  | [] -> false
  | _ :: _ -> true

(* in Lambda IR with OCaml 4.12 *)
is_non_empty = (function list (if list 1 0))

The empty list is represented using value 0. Non-empty lists are allocated memory blocks, and are therefore represented using a (non zero) pointer. Here the compiler uses this fact to translate a match ... with into a single if construct.

---

Strict Boolean Ifs in Flambda2

Flambda2 has always used Strict Boolean If, so the earlier versions had to convert Lambda's Generalized If constructions conservatively using an additional equality test. This interfered a bit with optimisations so we pushed instead to change the semantics of Lambda to a Strict Boolean If and perform that transformation to Generalized If later in the backend.

We chose Strict Boolean If for Flambda2's if semantic for the sake of simplicity. One way to look at it would be to say: the singleton set {1} is much simpler than the set of OCaml values excluding the integer 0. These sets arise when considering the true branch of an if. Indeed, in Strict Boolean If, we know that the condition is true , which is the integer 1 in OCaml, whereas in Generalized If it's any value except the integer 0.

This simplicity manifests itself at different levels: when processing an if (codebase level), when reasoning (architectural considerations), and when communicating (social level).

---

Here's an example of a basic optimisation:

(* example 1 *)
let cond x =
  if x then true else false

This code is equivalent to let cond x = x.

We would like to perform this optimisation in Flambda2. Although people do not usually write this kind of code, this pattern can occur after the branches of the if have been simplified.

For more on how Flambda2 handles simultaneous optimisations, see our earlier article on Speculative Inlining.

However if we try to perform the optimisation in a language with the Integer If semantics it's much more complicated: the IR term for the cond function is exactly the same as the IR for the is_non_empty one, but this optimisation is illegal for the is_non_empty one. This is a problem.

Here's an example of an existing function (Option.is_none from the standard library) which actually benefits from switching to Strict Boolean If.

(* Code from the standard library *)
let is_none option =
  match option with
  | None -> true
  | Some _ -> false

Here's the Lambda code for this function shown in Scheme syntax, compiled with Generalized If semantics:

(define (is_none option)
  (if
    option
    0 1))

You will notice that the if cannot be removed and the code will branch at runtime.

The same function again but compiled with Strict Boolean If semantics:

(define (is_none option)
  (if
    (is_int option)
    0 1))

This might look less efficient with an additional primitive (is_int) however the Strict Boolean If semantics allows us to apply the previously mentioned optimisation and replace the if statement with its condition, thus this code will not branch at runtime.

; If we applied this optimisation to Lambda
(define (is_none option)
  (is_int option))

Now that we have covered the reasoning and inception of the support for Strict Boolean If inside Lambda, we'll talk a little bit about what we had to do in order to make it a reality inside the upstream OCaml compiler.

Contributing to the Compiler

Almost the full story of this change can be seen by following this PR, it includes both the technical aspects (code changes) and most of the social interactions through the comments and linked issues.

Technical Aspect: what changed

If we look at what the PR changed, we can easily see that it is relatively small.

Some of the main changes:

• introducing an equality check when testing whether a value is 0 or not;
• some conditionals were added to differentiate between native and bytecode paths;
• a lot of inlined comments;

We don't touch the language itself, nor any of its intermediate representations.

This reveals a counter-intuitive reality: changing the semantics of a given IR requires updating the producers and consumers, but not the IR itself, that is, its type definition.

Here's the complete lists of the technical changes included in this PR:

1. Disabling optimisations that were only valid when using Generalized If semantic;
2. Adapting an existing optimisation to take into account the new pattern for compiling conditions;
3. Enabling the optimisation that we mentioned earlier and which became possible with Strict Boolean If.
4. A lot of Comments;

The lesson here is: changing semantic is merely done by telling other devs about it... As well as to other parts of the compiler.

Social aspect: other devs

"The social aspect" we are talking about here is in fact an umbrella term for a few different things.

It can describe different channels on which the OCaml Core Team members discuss these matters. The channels are usually either in person (within the same team, or at conferences and meetings), or through a private mailing list, but nowadays they are mostly held on the official repository through pull-request discussions, issue threads and so on. Concerning this work, most information is available online although some private discussions also occurred.

There is also a "social aspect" to the actual contribution. In addition to the changing of code, we wrote comments, documentation and a changelog entry - things that are necessary in proper open-source projects.

Additionally, since we do not have a formal specification for the Lambda IR, comments are particularly important here because they help people familiarize themselves with a given change, and therefore help in convincing them that they can easily wrap their head around it.

Concrete Consequences

This change in the IR allowed for cleaning the semantics, generating better code, and helped towards upstream the FL2 project.

Of all these things, the first noticeable effect has been the improved optimisation. Even though it is difficult to quantify the impact, when this optimisation triggers, it's always a strict improvement for the users. Now, from a compiler dev's point of view, this change didn't increase the complexity of the codebase and also made the reason why the compiler works actually simpler. A win-win situation overall.

Unfortunately, it is not all sunshine and rainbows.

We had to change the code that relied on the Generalized Ifs semantics. We did not actually expect any outside code to depend on the part we changed within the compiler, because the public API of a compiler is the source language... Which didn't change. Yet it so happened that another open-source project used the compiler internals and did rely on the Generalized If semantic.

This occurred to us in the form of a bug report. In the end, since the now faulty code of that project happened to replicate code we had just modified in the compiler, the fix itself came down to replicating this change. We wanted to mention this situation to illustrate the socially-oriented nature of these endeavours.

Conclusion

We used the case of changing the semantics of If within the OCaml compiler to illustrate the social nature of IR evolution. By changing the behaviour of a single construct, people outside the core working group can see their programs break unexpectedly.

As we mentioned earlier, having a formal specification helps avoid ambiguities. In the case of Lambda, this work sparked conversations about creating a formal semantics—a step in the right direction.

It's worth noting that some projects have taken formal semantics seriously from the very beginning. WebAssembly, for instance, was designed with a formal specification from day one, which has helped avoid many of these issues.

Finally, we'd like to leave you with this relevant xkcd comic as a reminder that every change, no matter how well-intentioned, will inevitably break someone's workflow. The art lies in making changes that benefit the majority while minimising disruption—and communicating clearly throughout the process.

---

Au sujet d'OCamlPro :

OCamlPro développe des applications à haute valeur ajoutée depuis plus de 10 ans, en utilisant les langages les plus avancés, tels que OCaml, Rust, et WebAssembly (Wasm) visant aussi bien rapidité de développement que robustesse, et en ciblant les domaines les plus exigeants (méthodes formelles, cybersécurité, systèmes distribués/blockchain, conception de DSLs). Fort de plus de 20 ingénieurs R&D, avec une expertise unique sur les langages de programmation, aussi bien théorique (plus de 80% de nos ingénieurs ont une thèse en informatique) que pratique (participation active au développement de plusieurs compilateurs open-source, prototypage de la blockchain Tezos, etc.), diversifiée (OCaml, Rust, Cobol, Python, Scilab, C/C++, etc.) et appliquée à de multiples domaines. Nous dispensons également des [formations sur mesure certifiées Qualiopi sur OCaml, Rust, et les méthodes formelles] (https://training.ocamlpro.com/) Pour nous contacter : contact@ocamlpro.com.