# Should We Balance? Towards Formal Verification of the Linux Kernel Scheduler

Julia Lawall, Keisuke Nishimura, Jean-Pierre Lozi

► To cite this version:

Julia Lawall, Keisuke Nishimura, Jean-Pierre Lozi. Should We Balance? Towards Formal Verification of the Linux Kernel Scheduler. SAS 2024 - 31st Static Analysis Symposium, Oct 2024, Pasadena (California), United States. hal-04708445

HAL Id: hal-04708445

https://inria.hal.science/hal-04708445v1

Submitted on 24 Sep 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Should We Balance? Towards Formal Verification of the Linux Kernel Scheduler

Julia Lawall[0000-0002-1684-1264], Keisuke Nishimura[0009-0009-1120-7262], and
Jean-Pierre Lozi[0009-0002-2876-8292]

Inria Paris, Paris, France
firstname.lastname@inria.fr

**Abstract.** The frequent tweaking of heuristics in the Linux kernel task scheduler suggests a need for formal verification, to ensure that important properties are maintained. Nevertheless, writing and verifying specifications for Linux kernel code have been considered to be impractical, leading other operating system verification efforts to propose co-design of new code and associated specifications instead. Furthermore, the Linux kernel evolves frequently, making any verification effort quickly out of date. Still, verification tools for C code are becoming more and more robust. In this paper, we explore whether it is now possible to apply formal verification directly to Linux kernel code, and to maintain the resulting specifications as the Linux kernel evolves. Our experiment focuses on the function `should_we_balance`, which is the gatekeeper to the Linux kernel scheduler's load balancer, and on the verification tool Frama-C.

**Keywords:** Linux kernel · Deductive verification · Frama-C.

<figure><img src="image_2.png" /></figure>

<figure><img src="image_3.png" /></figure>

<figure><img src="image_4.png" /></figure>

## 1 Introduction

An operating system is a collection of *mechanisms* and *policies* [29]. Mechanisms encode the technical details of access to machine resources, while policies determine the strategies for performing that access. In a general-purpose operating system, such as the Linux kernel, the operating system has no information about future application behavior. Accordingly, the policies typically amount to large, intertwined collections of heuristics. These policies critically determine application performance, so could expect that they should be stable. But, in practice, they are regularly tweaked, as weaknesses are identified and new needs emerge. There is thus a need for some form of verification that the heuristics respect some desired properties, and that the properties are maintained as the code evolves.

The Linux kernel has a long history of openness to verification techniques. Tools such as Coverity [6], Smatch [9], and Coccinelle [27] are regularly run on the Linux kernel to find patterns of code that indicate possible bugs. Coding
styles have been adopted that automate memory management in some common
cases, for example, automatically releasing device resources when the device is
removed [11] or tying resource lifetimes to variable scopes [13]. Recently, Rust
code has been admitted into the Linux kernel [12], recognizing the benefits of
its safety guarantees. These tools, however, check fixed properties, or properties
that they have been configured to check, that are intended to be relevant across
the code base, such as correct use of locks, avoidance of Null pointer dereferences,
etc. [34]. They do not address semantic bugs [24, 30, 33], i.e., violations of the
intended behavior of specific code fragments.

Deductive program verification proves by logical inference that, given a pre
condition describing possible input states, the program execution produces a
state that is described by a given post condition. Given pre and post conditions
that describe the intended behavior, deductive verification makes it possible
to ensure that the code is free of semantic bugs. In recent years, there have
been impressive efforts towards applying such verification to operating systems
code. seL4 [25] is a fully verified microkernel, that was verified by expressing
the kernel functionality in Haskell, verifying the code using Isabelle, and then
translating the resulting code to C. CertiKOS [22] is based on designing an
operating system according to a series of abstraction layers, each verified using
Coq [5]. Ipanema [28] relies on a domain-specific language to facilitate verification
using Why3 [7]. Unlike seL4 and CertiKOS that offer fully verified operating
systems, Ipanema focuses only on the scheduler, but provides a compiler for
translating code written in its domain-specific language to C code that can be
linked with the Linux kernel. This approach presents an incremental path to
achieving full operating system verification.

All of the deductive verification research efforts, while effective, focus on
only one instance of the operating system code. For example, while seL4 has been
released in multiple versions,<fnref n="1" /> the research around it has targeted proving specific
properties [21] or verifying new parts of the ecosystem [35]. There is no general
consideration of how to verify successive versions, as is essential for a regularly
evolving operating system such as the Linux kernel. Indeed, constructing pre and
post conditions that are consistent with a program's behavior is challenging, and
verifying that they are consistent with the code is challenging as well. The fact
that Linux kernel code changes frequently implies that once this effort has been
completed, it may immediately become out of date.

Today, there are mature or emerging verification tools, such as Frama-C [16],
VeriFast [23], and CN [36], that are aware of the semantics of C code, and that
can automatically generate verification conditions based on the code and user-
provided pre and post conditions and loop invariants. These tools furthermore
help the user discharge the generated verification conditions automatically by
providing an interface to one or more SMT solvers, such as Z3 [32], CVC4 [2],
CVC5 [1], and Alt-Ergo [10]. Given this degree of automation, we conjecture
that it may be possible to create specifications for an initial variant, and then

<footnote n="1">¹ https://docs sel4 systems releases sel4 12.1.0</footnote>
reuse them for subsequent variants, perhaps with minor variations, allowing the SMT solver to automatically search for proofs according to the new code.

In this paper, we carry out a preliminary investigation of this conjecture for a single function of the Linux kernel task scheduler, `should_we_balance()`. This function is a core part of the Linux kernel load balancer, determining whether a core is allowed to steal load from other cores, based on the current state of the machine. At the start of the project, there had been 10 versions of this function since its introduction in the Linux kernel in 2013. We start with the oldest version, and manually write and verify pre and post conditions for the function itself and its dependencies. While an operating system kernel is intrinsically a highly concurrent system, involving activities on multiple CPUs and interrupts from multiple devices, our initial pre and post conditions ignore the effect of concurrency, to focus on the expressed algorithm; we leave reasoning about concurrency to further studies. Given our pre and post conditions, we then use Frama-C to verify the successive versions, studying any impact on the specifications triggered by the changes in the code. In the course of our study, we found a previously unidentified bug in recent versions of `should_we_balance()`. Our fix for this bug has been part of the Linux kernel since v6.8, released in 2024, and is verified in our study. Overall, we find that minor changes in the code lead to no or minor changes in the specifications, but algorithmic changes, particularly within loops, require a major new verification effort. The latter cases, however, all reveal opportunities for improvement, either to fix bugs or to generalize an optimization, suggesting that the verification effort is worthwhile.

The rest of this paper is structured as follows. Section 2 provides some context on `should_we_balance()` and briefly presents Frama-C. Section 3 traces through the history of `should_we_balance()` and highlights the verification challenges found at each step. Section 4 discusses the results and our experience. Finally, Section 5 presents some related work and Section 6 concludes.

# 2 Background

We give an overview of `should_we_balance()` and briefly present Frama-C [16].

## 2.1 The code

In an operating system task scheduler, load balancing is the process of migrating one or more tasks from one CPU to another, in order to balance the amount of load on each CPU. In the Linux kernel, load balancing can be triggered periodically, i.e., on each tick, and when a CPU becomes idle. Load balancing is implemented by the function `load_balance`.<fnref n="2" /> This function takes as input information about the environment of the call, including the CPU from which the function is invoked (we refer to this as the *requesting CPU*) and a *scheduling do-main* representing a collection of CPUs across which load balancing is requested.

<footnote n="2">² The load balancer is implemented in kernel/sched/fair.c.
`load_balance()` was renamed `sched_balance_rq()` in Linux 6.10.</footnote>
1 static int should_we_balance(struct lb_env *env)
2 {
3     struct sched_group *sg = env->sd->groups;
4     struct cpumask *sg_cpus, *sg_mask;
5     int cpu, balance_cpu = -1;
6
7     if (env->idle == CPU_NEWLY_IDLE)
8         return 1;
9     sg_cpus = sched_group_cpus(sg);
10    sg_mask = sched_group_mask(sg);
11    forEach_cpu_and.cpu = sg_cpus, env->cpus) {
12        if (!cpumask_test_cpu.cpu, sg_mask) || !idle_cpu.cpu))
13            continue;
14        balance_cpu = cpu;
15        break;
16    }
17    if (balance_cpu == -1)
18        balance_cpu = group_balance_cpu(sg);
19    return balance_cpu != env->dst_cpu;
20 }

<caption>Fig. 1. Original definition of should_we_balance()</caption>

One of the first steps of load_balance is to call should_we_balance(), which analyzes the properties of the provided environment to determine whether the requesting CPU should perform load balancing. To prevent tasks from bouncing around the machine, it is desirable to allow only one CPU that is not newly idle to perform load balancing over a given scheduling group at a particular time. The function should_we_balance() enforces this constraint.

The function should_we_balance() was introduced in commit 23f0d2093c78, created on August 6, 2013, comprising various code fragments extracted from the existing scheduler function update_sd_lb_stats. should_we_balance first appeared in a Linux kernel mainline release in Linux v3.12. Figure 1 shows the original definition. The input of should_we_balance(), env, packages the environment information provided to load_balance. The result is true (or 1), if the requesting CPU should be allowed to load balance, and false otherwise.

A newly idle CPU is always allowed to load balance (lines 7-8). Otherwise, load balancing is limited to the CPUs in the intersection of three masks: sg_cpus, env->cpus, sg_mask, which collectively describe the set of CPUs associated with the scheduling domain. Assuming no concurrent effects, all CPUs in the domain should obtain the same value for the intersection of these masks, allowing them all to elect the same CPU to perform load balancing. In the code, the iteration<fnref n="3" /> on line 11 selects only CPUs that are in the intersection of sg_cpus and env->cpus, while cpumask_test_cpu() on line 12 checks whether each selected CPU also satisfies sg_mask. On reaching a CPU for which load balancing is allowed and that is also idle, the loop initializes balance_cpu to this CPU and then exits the loop (lines 14-15). If the latter conditions are never satisfied, then the loop terminates with balance_cpu as -1. In the latter case, balance_cpu is initialized to the first CPU in the scheduling domain, as identi-

<footnote n="3">³ for Each_cpu_and is a macro of the Linux kernel. It expands to a for loop header.</footnote>
fied by `group_balance_cpu()` (line 18). Finally, the return value is true if and only if the requesting CPU is different from the one stored in `balance_cpu`.

Note that there is a bug in the initial version of `should_we_balance()`; if the requesting CPU is not newly idle, the function returns true for all CPUs except the elected one (line 19). This bug was fixed in commit b0cff9d88ce2, on September 10, 2013, which was part of the first Linux kernel release containing `should_we_balance()`, Linux v3.12.

## 2.2 The verifier

Frama-C [16] is a toolset for reasoning about C code. Among the available plugins, we use the plugin WP that performs weakest pre condition reasoning about the semantics of the C code, by generating verification conditions using provided pre conditions, post conditions, and loop invariants. Frama-C manages the use of off-the-shelf SMT solvers to prove the verification conditions, and allows manual construction of proofs using the Coq Proof Assistant [5].

Frama-C specifications are written using the ANSI/ISO C Specification Language (ACSL) [3]. The user must both specify properties about memory layout (pointers whose data can be read (`\valid_read()`), pointers whose data can be written (`\valid()`), and pointers whose data does not overlap (`\separated()`)), and specify properties about function behavior (requires for pre conditions and ensures for post conditions). Pre and post conditions can be grouped into named behaviors; in this case the keywords assumes and ensures provide pre and post conditions, respectively. Behaviors can be declared and checked to be disjoint and complete. `\result` represents the return value of a function. assigns declares an overapproximation of the memory regions that a function may have modified; other memory regions are considered to be unaffected. `\forall` and `\exists`s are the universal and existential quantifiers, respectively. Further information can be found in the ACSL documentation [3].

# 3 Case Study

As a case study, we consider the function `should_we_balance()`, in the 10 variants that have been developed since its introduction in August 2013 (Table 1). We conclude with a last variant reflecting our change to the Linux kernel that fixes a semantic bug identified during the verification process. All experiments are carried out on a 2-socket Intel Xeon Gold 6130, using Frama-C 28.1 configured to use the SMT solvers Alt-Ergo (version 2.5.3), CVC4 (version 1.8), CVC5 (version 1.1.2), and Z3 (version 4.13.0), with a timeout of 600 seconds.

Throughout this section, postconditions refer to the system state after the call to `should_we_balance()`. To use these specifications to prove properties of code that calls `should_we_balance()`, it may be more practical that the hypotheses of implications in the postconditions refer to the state before calling the function. Fortunately, most of the memory referenced by `should_we_balance()` is not
<table><caption>**Table 1.** The considered commits. Commits with Release – are subsumed by a more recent commit and thus do not appear, as is, in any Linux kernel release.</caption><thead><tr><th>#</th><th>Commit id</th><th>Date</th><th>Release</th><th>Impact</th></tr></thead><tbody><tr><td>0</td><td>23f0d2093c78</td><td>08.2013</td><td>–</td><td>create the function</td></tr><tr><td>1</td><td>b0cff9d88ce2</td><td>09.2013</td><td>v3.12</td><td>replace != by ==</td></tr><tr><td>2</td><td>af218122b103</td><td>05.2017</td><td>–</td><td>eliminate a redundant function call</td></tr><tr><td>3</td><td>e5c14b1fb892</td><td>05.2017</td><td>v4.13</td><td>rename a function</td></tr><tr><td>4</td><td>024c9d2faebd</td><td>10.2017</td><td>v4.14</td><td>check validity of the stealing CPU</td></tr><tr><td>5</td><td>97fb7a0a8944</td><td>03.2018</td><td>v4.17</td><td>improve comments</td></tr><tr><td>6</td><td>64297f2b03cc</td><td>04.2020</td><td>v5.8</td><td>return early on finding an idle core</td></tr><tr><td>7</td><td>792b9f65a568</td><td>06.2022</td><td>v6.0</td><td>bail out if tasks detected on a newly idle CPU</td></tr><tr><td>8</td><td>b1bfeab9b002</td><td>07.2023</td><td>–</td><td>prefer fully idle cores</td></tr><tr><td>9</td><td>f8858d96061f</td><td>09.2023</td><td>v6.6</td><td>remove non-idle core hyperthreads from the CPU mask</td></tr><tr><td>10</td><td>6d7e4782bcf5</td><td>10.2023</td><td>v6.8</td><td>change a condition of the selection algorithm</td></tr></tbody></table>

affected by the call. In our artifact,<fnref n="4" /> we prove both the post conditions shown in the paper and the post conditions that refer to the state before the call site.

## 3.1 Creation of `should_we_balance()` at commit 23f0d2093c78

Our verification effort starts by creating the pre conditions, post conditions, and loop invariants of the initial definition of `should_we_balance()`. For the functions called by `should_we_balance()`, we model them by their prototypes and associated pre and post conditions. As such prototypes rarely change over time, for simplicity, we use the same definitions for all `should_we_balance()` versions. The complete formalization in terms of these prototypes is available in our artifact. The actual definitions of these modeled functions in their different versions are available in the Linux kernel source tree.<fnref n="5" /> Various declarations are required to show that the variables and data structures manipulated by `should_we_balance()` are within the appropriate bounds and the accesses performed on them are valid. Frama-C also requests that we indicate the set of side effects of `should_we_balance()`; there are none. We omit these declarations and focus on the pre and post conditions and loop invariants, which define the possible behaviors of `should_we_balance()`.

**Pre and post conditions.** The function `should_we_balance()` involves two main cases, either `env->idle` is `CPU_NEWLY_IDLE`, in which case the function returns 1 immediately, or it is not, resulting in the execution of the rest of the function. The first pair of pre and post conditions is thus defined by the behavior `newly_idle` (Fig. 2, lines 1-3), specifying these properties. The preconditions of all other behaviors furthermore ensure that the first test fails, with the property `env->idle != CPU_NEWLY_IDLE` (lines 6 and 14).

<footnote n="4">⁴ https://zenodo.org/records/13132904 (10.5281/zenodo.13132903)</footnote>

<footnote n="5">⁵ https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git/</footnote>
1 behavior newly_idle:
2 assumes env->idle == CPU_NEWLY_IDLE;
3 ensures \result;
4
5 behavior not_newly_idle_with_idle:
6 assumes env->idle != CPU_NEWLY_IDLE;
7 assumes ∃integer i; relevant(i, env) && idle_cpu(i);
8 ensures ∀integer i;
9 relevant(i, env) ==> idle_cpu(i) ==>
10 (Vinteger j; 0 <= j < i ==> relevant(j, env) ==> !idle_cpu(j)) ==>
11 (\result <=> env->dst_cpu != i);
12
13 behavior not_newly_idleWithout_idle:
14 assumes env->idle != CPU_NEWLY_IDLE;
15 assumes ∀integer i; relevant(i, env) ==> !idle_cpu(i);
16 ensures \result <=> group_balance_cpu env->sd->groups != env->dst_cpu;

<caption>Fig. 2. Initial pre and post conditions for `should_we_balance()`</caption>

The rest of the function then loops over the relevant CPUs until reaching one that is idle, which is recorded in `balance_cpu`, or, if no idle CPU is detected, chooses a CPU using `group_balance_cpu()`. This leads to two further behaviors, `not_newly_idle_with_idle` where there exists an idle CPU (lines 5-11) and `not_newly_idleWithout_idle` where no CPU is idle (lines 13-16). Both behaviors rely on a predicate<fnref n="6" /> `relevant()` that checks whether the first argument, representing a CPU, is in bounds and whether the CPU is selected in the various masks accessible from the environment `env`, namely `sgCPUS`, `env->cpus`, and `sg_mask`. The behavior `not_newly_idle_with_idle` ensures that if there is at least one CPU that is both relevant and idle, then the result of the function is `true` if and only if the requesting CPU, `env->dst_cpu`, is the CPU with the lowest index satisfying these properties. The behavior `not_newly_idleWithout_idle`, in contrast, ensures that if no CPU is both relevant and idle, then the result is `true` if and only if the destination CPU is different from the one returned by `group_balance_cpu()`.

Loop invariants. As `should_we_balance()` contains a loop, we must also define the associated loop invariants, declare the side effects performed by the loop, and provide a loop variant ensuring termination. The first loop invariant (line 1, below) and the loop variant (line 4) reflect the relationship between the loop index `cpu` and the loop bound `small_cputmask_bits` in each iteration. The second loop invariant (line 2) reflects the fact Fig. 1 shows that the only way around the loop for a relevant CPU is under a test that the CPU is not idle (lines 12-13, Fig. 1), implying that every relevant CPU with an index less than the current one is not idle. This loop invariant is needed to prove the properties of idle CPUs found in the function post conditions (Fig. 2). The only side effect is to the loop index, `cpu` (line 3). `balance_cpu` is assigned within the loop body, but it is not

<footnote n="6">⁶ This predicate is actually defined as a macro, to expose the constituent properties to the SMT solvers used by Frama-C without relying on the solver to unfold predicates.</footnote>
considered to be modified within the loop, because all execution paths from the assignment lead to a break; and thus directly out of the loop (see Section 3.7).

1 loop invariant 0 <= cpu <= smallogenic_cpmask_bits;
2 loop invariant $\forall$integer j; 0 <= j < cpu == > relevant(j, env) == > !idle_cpu(j);
3 loop assigns cpu;
4 loop variant small_cpmask_bits - cpu;

## 3.2 Change #1: Commit b0cff9d88ce2

Commit b0cff9d88ce2 changes the final != (line 19, Fig. 1) to == to fix the bug that the original version of `should_we_balance()` returns true for all cores that are different from the one returned by `group_balance_cpu`, potentially allowing many non-idle cores to try to steal load at the same time. In the specification, only the behavior `not_newly_idleWithout_idle` changes, as follows:

```
behavior not_newly_idleWithout_idle:
    assumes env->idle != CPU_NEWLY_IDLE;
    assumes $\forall$integer i; relevant(i, env) == > !idle_cpu(i);
- ensures \result <==> group_balance_cpu env->sd->groups != env->dst_cpu;
+ ensures \result <==> group_balance_cpu env->sd->groups == env->dst_cpu;
```

## 3.3 Change #2: Commit af218122b103

The log message of commit af218122b103 reports that the change is based on the observation that `sg_cpus` & `sg_mask == sg_mask`, where `sg_cpus` is initialized by calling `sched_group_cpus` (Fig. 1, line 9) and `sg_mask` is initialized by calling `sched_group_mask` (Fig. 1, line 10). The changes to `should_we_balance()`, shown in Fig. 3, remove the declaration and initialization of `sg_cpus` (lines 4-5, 11), simplify the loop to test `sg_mask` and `env->cpus` directly (lines 14 and 16), and correspondingly eliminate the `cpumask_test_cpu` test (lines 15 and 17).

```
1 static int should_we_balance(struct lb_env *env)
2 {
3     struct sched_group *sg = env->sd->groups;
4     struct cpumask *sg_cpus, *sg_mask;
5     struct cpumask *sg_mask;
6     int cpu, balance_cpu = -1;
7
8     [...]
9     if (env->idle == CPU_NEWLY_IDLE)
10    return 1;
11   sg_cpus = sched_group_cpus(sg);
12   sg_mask = sched_group_mask(sg);
13   /* Try to find first idle cpu */
14   forEach_cpu_and(cpu, sg_cpus, env->cpus) {
15     if (!cpumask_test_cpu(cpu, sg_mask) || !idle_cpu(cpu))
16     forEach_cpu_and(cpu, sg_mask, env->cpus) {
17       if (!idle_cpu(cpu))
18         continue;
19     balance_cpu = cpu;
```

<caption>Fig. 3. Commit af218122b103: eliminating a call to `sched_group_cpus`</caption>
To update the specifications, we correspondingly eliminate references to the predicate `sched_group_cpus()`. `sched_group_cpus()` is part of the conditions for entering the loop body in `should_we_balance()`, and thus it is referenced in any part of the specification that describes the loop behavior. Nevertheless, as noted in Section 3.1, for conciseness, we have factorized the loop-body entry conditions into a macro, relevant. Thus, the only change needed is to remove the redundant reference to `sched_group_cpus env->sd->groups ->bits[i]` in the definition of this macro, as shown below:

```c
#define relevant(i, env) \
    (0 <= i < small_cpunumask_bits && \
     sched_group_cpus (env->sd->groups)->bits[i] && \
      env->cpus->bits[i] && sched_group_mask (env->sd->groups)->bits[i])
```

In general, the amount of specification change entailed for such a code change depends on the design of the specifications; if we did not have the relevant macro, many parts of the specification would be affected, which would require the Linux kernel developer to understand these specifications in detail. We also explored the possibility of defining an axiom describing the relationship between the two functions, allowing the existing specifications to remain unchanged. Unfortunately, we found that this approach could cause the SMT solvers to fail in unexpected ways on the more complex variants of `should_we_balance()` found in more recent versions of the Linux kernel (e.g., Sections 3.10 and 3.11).

## 3.4 Change #3: Commit e5c14b1fb892

This commit simply renames `sched_group_mask()` to `group_balance_mask()`. We make the corresponding change in the specifications, affecting only the definition of the macro `relevant`:

```c
#define relevant(i, env) \
    (0 <= i < small_cpunumask_bits && env->cpus->bits[i] && \
     sched_group_mask (env->sd->groups)->bits[i])
+ group_balance_mask (env->sd->groups)->bits[i])
```

## 3.5 Change #4: Commit 024c9d2faebd

This commit addresses a usage condition that was previously overlooked: load balancing may be triggered by an interrupt at the same time as a CPU is being disabled. Accordingly, a new test is added at the beginning of the function that returns 0 (i.e., `false`) if the CPU requesting to load balance is no longer valid:

```c
if (!cpumask_test_cpu (env->dst_cpu, env->cpus)) return 0;
```

This new test and corresponding return value lead to a new behavior:

```
behavior race_condition:
    assumes !env->cpus->bits[env->dst_cpu];
    ensures \result == false;
```

The new test and return value furthermore imply that the rest of the function, represented by all of the existing behaviors, is not executed if the condition is satisfied. We thus add the following to each of the existing behaviors:

```
assumes env->cpus->bits[env->dst_cpu];
```
## 3.6 Change #5: Commit 97fb7a0a8944

This commit only adjusts the text of some comments in the code. There is no impact on the specifications or the proof.

## 3.7 Change #6: Commit 64297f2b03cc

This commit changes the path that exits the loop and the code after the loop:

1. `for Each_cpu_and(cpu, group_balance_mask sg), env->cpus) {
2.   if (!idle_cpu(cpu))
3.     continue;
4.   balance_cpu = cpu;
5.   break;
6. } + return cpu == env->dst_cpu;
8.   if (balance_cpu == -1)
9.     balance_cpu = group_balance_cpu(sg);
10.   return balance_cpu == env->dst_cpu;
11. } + return group_balance_cpu(sg) == env->dst_cpu;

The variable `balance_cpu` is now unneeded, and its declaration is also removed.

Following these changes, if an idle CPU is found (i.e., the first idle CPU), the loop exits the function immediately, indicating whether the idle CPU is the requesting one (line 6). The code after the loop is now thus only reached if there is no idle CPU. In this case, the result is determined by `group_balance_cpu()` and the result of this comparison can be returned directly (line 11).

The changes only reorganize the computation but have no impact on the return value, and thus no changes are needed to the specification. As noted in Section 3.1, a `break;` path in a loop is considered to be outside the loop body. The use of `balance_cpu` was thus not part of the loop invariant, and there are thus no changes to the loop specifications.

## 3.8 Change #7: Commit 792b9f65a568

As for commit 024c9d2faebd, described in Section 3.5, this commit is motivated by the detection of a specific, unexpected, condition of the calling context. Here it is observed that a CPU that was labeled as `CPU_NEWLY_IDLE` may no longer be idle, due to task wakeups performed by other CPUs on the machine. The changes to the `CPU_NEWLY_IDLE` test are as follows:

```c
- if (env->idle == CPU_NEWLY_IDLE)
+ if (env->idle == CPU_NEWLY_IDLE) {
+   if (env->dst_rq->nr_running > 0 || env->dst_rq->ttwu_pending)
+     return 0;
+   return 1;
+ }
```

The corresponding changes to the existing `newly_idle` behavior are:

```
behavior newly_idle:
    assumes env->idle == CPU_NEWLY_IDLE;
    assumes env->cpus->bits[env->dst_cpu];
- ensures \result;
+ ensures \result <==>
+   !(env->dst_rq->nr_running > 0 ||
    env->dst_rq->ttwu_pending);
```
1 for Each_cpu_and (cpu, group_balance_mask (sg), env - >cpus) {
2 if (! idle_cpu (cpu))
3 continue;
4 + if (! (env - >sd - >flags & SD_SHARE_CPCAPACITY) && !is_core_idle (cpu)) {
5 + if (idle_smt == -1)
6 idle_smt = cpu;
7 + continue;
8 + }
9 return cpu == env - >dst_cpu;
10 }
11 + if (idle_smt == env - >dst_cpu)
12 + return true;
13 return group_balance_cpu (sg) == env - >dst_cpu;

<caption>Fig. 4. Extract of commit b1bfeab9b002: prefer fully idle cores</caption>

Here, the new *if* condition is embedded into the post condition of an existing behavior, rather than adding a new behavior, as in Section 3.5. Thus, there is no need to change the pre conditions of the other behaviors.

3.9 Change #8: Commit b1bfeab9b002

Writing loop invariants is commonly perceived as difficult and as an extra bur-
den on the developer. The previous seven updates to should_we_balance() do
not affect the contents of the loop, and thus no change is required to the loop
invariants. In the original implementation, the loop cycles through the relevant
CPUs and returns the first one that is detected to be idle. Commit b1bfeab9b002
changes that behavior, to take hyperthreads into account. Hyperthreads imple-
ment multithreading at the hardware level, allowing one physical core to perform
two or more threads of computation, depending on the hardware architecture.
Hyperthreads are designed to exploit the ability to execute multiple parts of
the processor pipeline at once and to fill any time left idle by processor stalls,
e.g., induced by cache misses. Nevertheless, hyperthreading does not achieve
perfect scalability, and thus it is desirable to place a task on a CPU such that
all hyperthreads are idle, if one is available. This commit rewrites the loop to
search for a CPU whose associated physical core is completely idle (detected by
is_idle_core()), while still keeping track of the first CPU (idle_smt) that is
idle but that has non-idle sibling hyperthreads, as a fallback.

To account for hyperthreads, the portion of should_we_balance() from the
loop to the end of the function is modified as shown in Fig. 4. A declaration of
idle_smt is also added at the top of the function, with initial value -1. Now, the
loop only returns from the function if it finds a fully idle physical core (Fig. 4,
line 9). New code is added after the loop for the case where there is no fully
idle physical core, but an idle CPU was identified on some iteration (lines 11-
12). These new strategies only apply if the scheduling domain does not have the
SD_SHARE_CPCAPACITY flag set (line 4). On our test machine, this flag is only
set for the scheduling domains representing a single physical core.
Pre and post conditions. This commit defines a new algorithm, which has a major impact on the specifications, specifically in the case where there is at least one relevant idle CPU, i.e., the behavior not_newly_idle_with_idle. First, if the test env->sd->flags & SD_SHARE_CUCAPACITY; (Fig. 4, line 4) succeeds, then the behavior of should_idle_balance is entirely unchanged:

1 behavior not_newly_idle_with_idle:
2 assumes env->idle != CPU_NEWLY_IDLE;
3 assumes env->cpus->bits[env->dst_cpu];
4 + assumes env->sd->flags & SD_SHARE_CUCAPACITY;
5 assumes ∃integer i; relevant(i, env) && idle_cpu(i);
6 ensures ∀integer i;
7 relevant(i, env) ==> idle_cpu(i) ==>
8 (∀integer j; 0 <= j < i ==> relevant(j, env) ==> !idle_cpu(j)) ==>
9 (\result <=> env->dst_cpu == i);

If env->sd->flags & SD_SHARE_CUCAPACITY; fails, we have to distinguish the case where there is an idle core from the case where there is no idle core, but only an idle CPU having at least one non-idle hyperthread. We create variants of the behavior not_newly_idle_with_idle for these two cases. The new behavior not_newly_idle_with_idle_core checks for the case where there exists an idle core. This involves simply replacing idle_cpu by idle_core throughout the behavior, implying that load balancing is allowed for the first fully idle core:

-behavior not_newly_idle_with_idle:
+behavior not_newly_idle_with_idle_core:
  assumes env->idle != CPU_NEWLY_IDLE;
  assumes env->cpus->bits[env->dst_cpu];
- assumes ∃integer i; relevant(i, env) && idle_cpu(i);
+ assumes ! (env->sd->flags & SD_SHARE_CUCAPACITY);
+ assumes ∃integer i; relevant(i, env) && idle_core(i);
ensures ∀integer i;
- relevant(i, env) ==> idle_cpu(i) ==>
- (∀integer j; 0 <= j < i ==> relevant(j, env) ==> !idle_cpu(j)) ==>
+ relevant(i, env) ==> idle_core(i) ==>
+ (∀integer j; 0 <= j < i ==> relevant(j, env) ==> !idle_core(j)) ==>
  (\result <=> env->dst_cpu == i);

The remaining case, in which there is an idle CPU but no idle core, should intuitively fall back on the original behavior of allowing the first idle CPU to perform load balancing, which would lead to the following behavior:

-behavior not_newly_idle_with_idle:
+behavior not_newly_idle_with_idle_cpu:
  assumes env->idle != CPU_NEWLY_IDLE;
  assumes env->cpus->bits[env->dst_cpu];
+ assumes ! (env->sd->flags & SD_SHARE_CUCAPACITY);
+ assumes ∀integer i; relevant(i, env) ==> !idle_core(i);
  assumes ∃integer i; relevant(i, env) && idle_cpu(i);
ensures ∀integer i;
  relevant(i, env) ==> idle_cpu(i) ==>
  (∀integer j; 0 <= j < i ==> relevant(j, env) ==> !idle_cpu(j)) ==>
  (\result <=> env->dst_cpu == i);

The above behavior, however, cannot be proved, due to a bug in the code. If there is no idle core and the chosen idle CPU, idle_smt, is different from the requesting CPU (Fig. 4, lines 11-12), then the return value is computed by checking group_balance_cpu(sg) (line 13). This allows should_we_balance() to return true for two non newly idle cores at once, making the <==> in the last line of the above behavior unprovable. A behavior that can be proved is:
```
-behavior not_newly_idle_with_idle:
+behavior not_newly_idle_with_idle_cpu:
  assumes env->idle != CPU_NEWLY_IDLE;
  assumes env->cpus->bits[env->dst_cpu];
+ assumes !(env->sd->flags & SD_SHARE_CUCAPACITY);
+ assumes Vinteger i; relevant(i, env) ==> !idle_core(i);
  assumes Einteger i; relevant(i, env) && idle_cpu(i);
  ensures Vinteger i;
    relevant(i, env) ==> idle_cpu(i) ==>
    (Vinteger j; 0 <= j < i ==> relevant(j, env) ==> !idle_cpu(j)) ==>
    (\result <=> env->dst_cpu == i);
+ (\result ==>
+ (env->dst_cpu==i || env->dst_cpu==group_balance_cpu env->sd->groups)));
+ ensures Vinteger i;
+ relevant(i, env) ==> idle_cpu(i) ==>
+ (Vinteger j; 0 <= j < i ==> relevant(j, env) ==> !idle_cpu(j)) ==>
+ (env->dst_cpu == i ==>
\result);
```

When trying to verify the code discussed in the next section (Change #9), which has the same problem, the second author identified the problem and submitted a patch to fix it. This patch has since been integrated into the Linux kernel as commit 6d7e4782bcf5, which is discussed further in Section 3.11.

**Loop invariants.** The change affects the body of the loop and has an impact on the loop invariants. In previous versions, the loop iterated over the non-idle CPUs, as expressed by the following invariant:

```
loop invariant Vinteger j; 0 <= j < cpu ==> relevant(j, env) ==> !idle_cpu(j);
```

The behavior of the new loop depends on whether a value (other than -1) for `idle_smt` has been chosen. As long as `idle_smt` is -1 (which is always the case if the test `env->sd->flags & SD_SHARE_CUCAPACITY` holds (invariant `i1`, below)), every previous relevant CPU is non-idle, and the above invariant continues to hold (invariant `i2`). Once an idle CPU is detected that is not an idle core, it is stored in `idle_smt`. The loop invariant must record that `idle_smt` is relevant and idle (invariant `i3`), and the first CPU with this property (invariant `i4`). Subsequent iterations can be the result of either the `continue` on line 3 or the one on line 7 (Fig. 4), and thus for these CPUs, it is only known that the initial cores are not idle (invariant `i5`). Thus, we replace the above loop invariant with:

```
loop invariant i1:
  env->sd->flags & SD_SHARE_CUCAPACITY ==> idle_smt == -1;
loop invariant i2: idle_smt == -1 ==>
  Vinteger j; 0 <= j < cpu ==> relevant(j, env) ==> !idle_cpu(j);
loop invariant i3: idle_smt != -1 ==>
  relevant(idle_smt, env) && idle_cpu(idle_smt);
loop invariant i4: idle_smt != -1 ==>
  Vinteger j; 0 <= j < idle_smt ==> relevant(j, env) ==> !idle_cpu(j);
loop invariant i5: idle_smt != -1 ==>
  Vinteger j; idle_smt <= j < cpu ==> relevant(j, env) ==> !idle_core(j);
```

## 3.10 Change #9: Commit f8858d96061f

As used in the previous change, a call to `is_core_idle.cpu)` checks all of the hyperthreads of `cpu` for idleness, which may involve multiple remote memory accesses. The test is furthermore redundant if such a test has failed on a previously
1 + struct cpumask *swb_cpus =
2 + this_cpu cpumask_var_ptr(should_we_balance_tmpmask);
3 ...;
4 - for Each_cpu and (cpu, group_balance_mask (sg), env->cpus) {
5 + cpumask_copy (swb_cpus, group_balance_mask (sg));
6 + for each_cpu and (cpu, swb_cpus, env->cpus) {
7     if (!idle_cpu (cpu))
8       continue;
9     if (! (env->sd->flags & SD_SHARE_CPCAPACITY) && !is_core_idle (cpu)) {
10         if (idle_smt == -1)
11         idle_smt = cpu;
12 + #ifdef CONFIG_SCHED_SMT
13 + cpumask_andnot (swb_cpus, swb_cpus, cpu_smt_mask (cpu));
14 + #endif
15     continue;
16 }  
17   return cpu == env->dst_cpu;
18 }

<caption>Fig. 5. Commit f8858d96061f: Remove non-idle core hyperthreads from the CPU mask</caption>

considered hyperthread of cpu. The complexity of these tests is thus quadratic
in the number of hyperthreads. Motivated by experiments on a POWER10 ar-
chitecture, with 4 hyperthreads per core, once an idle CPU is detected that has
some non-idle hyperthreads, this commit (Fig. 5) uses cpumask_andnot (com-
puting A = B ∧ ¬C, for masks A, B and C, line 13) to remove all hyperthreads
of cpu from the mask copied from group_balance_mask() (line 5).

This commit introduces a new data structure, `should_we_balance_tmpmask` (lines 1-2), and calls to `cpumask_copy()` (line 5) and `cpumask_andnot()` (line 13). The data structure amounts to an array containing a buffer for each CPU that can be used to hold a temporary copy of a cpumask. A copy is needed because the mask obtained from `group_balance_mask(sg)` cannot be modified. The new functions, to copy and update the mask, respectively, need pre and post conditions. Both functions write into their first argument, and thus their pre conditions must declare the aliases that may exist between this argument and the other memory locations accessed by the function. The default memory model of Frama-C considers that aliases are only possible between pointers of the same type. Thus, in practice, we need only consider the possible aliases among the function arguments, which are all pointers to cpumasks. As copying a mask on top of itself makes little sense, we simply declare that the arguments to `cpumask_copy()` are separated. On the other hand, for `cpumask_andnot()`, in the call in `should_we_balance()` the first two arguments are equal, and in the more general case any of the arguments could be aliases. We thus add pre conditions declaring that either the first argument is identical to the second (respectively, third) argument, or they are separated. For both functions, it is furthermore necessary to state that the first argument is writeable and modified, and that the remaining arguments are readable.

Beyond the need for pre and post conditions for the new functions, we must
also take into account the fact that cpumask_andnot is called within a loop, and
indeed affects the contents of one of the masks that affects the possible values
of the loop index. Accordingly, we must also update the loop invariants. The main challenge is to express the evolving relationship between the local mask `swb_cpus` and the mask used in previous versions, `group_balance_mask(sg)`. The changes trigger the need for three new invariants, in addition to the ones presented at the end of Section 3.9:

loop invariant a1:
    Vinteger j; 0 <= j < small_cpmask_bits ==>
    swb_cpus->bits[j] ==> group_balance_mask(sg)->bits[j];
loop invariant a2: idle_smt == -1 ==>
    Vinteger j; 0 <= j < small_cpmask_bits ==>
    group_balance_mask(sg)->bits[j] ==> swb_cpus->bits[j];
loop invariant a3: idle_smt != -1 ==>
    Vinteger j; 0 <= j < small_cpmask_bits ==>
    group_balance_mask(sg)->bits[j] ==> swb_cpus->bits[j] || !idle_core(j);

By the semantics of `cpumask_andnot()`, the set of CPUs represented by `swb_cpus` is always a subset of the set of CPUs represented by `group_balance_mask(sg)` (invariant a1). If `idle_smt` has not yet been set, then `cpumask_andnot()` has also not yet been called, and thus `swb_cpus` and `group_balance_mask(sg)` represent the same set of CPUs (invariant a2). Finally, if `idle_smt` has been set to the index of some CPU, then `cpumask_andnot()` has been called at least once, and `swb_cpus` may represent a reduced set of CPUs. As CPUs are removed from `swb_cpus` because they are hyperthreads (i.e., elements of `cpu_smt_mask()`) of a previously seen CPU that is part of a core that is not idle and the set of hyperthreads forms an equivalence class, all of the hyperthreads, whether idle or not, cause the predicate `idle_core` to fail. Thus, any CPU in `group_balance_mask(sg)` is either still an element of `swb_cpus` or it has been detected as being part of a core that is not idle, leading to invariant a3.

There is no change to the pre and post conditions of `should_we_balance`, reflecting the fact that this change is only an optimization.

## 3.11 Change #10: Commit 6d7e4782bcf5

As noted in Section 3.9, the two previous versions of `should_we_balance` can return true for multiple non newly idle cores, contrary to the intent of `should-we_balance`. The inability to prove `\result ==> env->dst_cpu == i, i.e.,` that if the result is true then the requesting CPU is the same as the chosen one, led the second author to submit the following change to the Linux kernel:

```c
- if (idle_smt == env->dst_cpu) return true;
+ if (idle_smt != -1) return idle_smt == env->dst_cpu;
```

With this change, it is possible to prove not only the relaxed post condition presented in Section 3.9 for behavior `not_newly_idle_with_idle_cpu`:

ensures Vinteger i;
relevant(i, env) ==>
idle_cpu(i) ==>
(Vinteger j; 0 <= j < i ==>
relevant(j, env) ==>
!idle_cpu(j)) ==>
\result ==>
 env->dst_cpu == i || env->dst_cpu == group_balance_cpu env->sd->groups));

but also the expected more strict post condition found in the earlier versions, showing that the bug has been fixed.
ensures `Integer i;
relevant(i, env) ==> idle_cpu(i) ==>
(∀integer j; 0 <= j < i ==> relevant(j, env) ==> !idle_cpu(j)) ==>
(\result <== env->dst_cpu == i);

# 4 Discussion

In this section, we provide an overview of our results, some reflections on our experience, and some directions for future work.

## 4.1 Overview of the results

Our intent was to examine the resilience of verification to the kinds of changes that occur in Linux kernel source code. We hoped to find that specifications would need to be rewritten only on major algorithmic changes, while minor changes, such as refactorings would require at most small tweaks. Table 2 characterizes the changes in our considered commits and the corresponding

<table><caption>Table 2. Description of the considered commits</caption><thead><tr><th>#</th><th>Commit id</th><th>Change type</th><th>Proof impact</th></tr></thead><tbody><tr><td>0</td><td>23f0d2093c78</td><td>new algorithm</td><td>new specification</td></tr><tr><td>1</td><td>b0cff9d88ce2</td><td>bug fix</td><td>invariant update</td></tr><tr><td>2</td><td>af218122b103</td><td>refactoring</td><td>invariant update</td></tr><tr><td>3</td><td>e5c14b1fb892</td><td>refactoring</td><td>invariant update</td></tr><tr><td>4</td><td>024c9d2faebd</td><td>refinement</td><td>new behavior</td></tr><tr><td>5</td><td>97fb7a0a8944</td><td>refactoring</td><td>none</td></tr><tr><td>6</td><td>64297f2b03cc</td><td>refactoring</td><td>none</td></tr><tr><td>7</td><td>792b9f65a568</td><td>refinement</td><td>new behavior</td></tr><tr><td>8</td><td>b1bfeab9b002</td><td>new algorithm</td><td>many changes</td></tr><tr><td>9</td><td>f8858d96061f</td><td>new algorithm</td><td>many changes</td></tr><tr><td>10</td><td>6d7e4782bcf5</td><td>bug fix</td><td>invariant update</td></tr></tbody></table>

proof update effort. The most challenging cases are the three where the function is introduced or the algorithm changes (Changes #0, #8, and #9), which require new pre and post conditions and new loop invariants. Furthermore, all three of the commits that made major algorithmic changes either introduced a bug or missed an optimization opportunity (see Section 4.3), suggesting that the time invested in verification could be worthwhile.

From Change #0 to #8, the number of verification conditions is relatively stable at around 255, and the complete proof of each version takes around one minute. The introduction of the temporary buffer and the calls to `cpumask_` and `not()` in Change #9 increases the number of verification conditions to over 300, and dramatically increases the total verification time to 9 minutes or more. In practice, while developing the specifications, we frequently use the “smoke tests” provided by Frama-C. These tests amount to trying to prove false in each basic block, to identify dead code or logical contradictions. Smoke tests add around 100 verification conditions and around 2 minutes to the total time of each of our experiments.

To maximize the chance of success, we have used four SMT solvers, Alt-Ergo, CVC4, CVC5, and Z3, as well as Frama-C's internal simplifier Qed. When multiple solvers are available, Frama-C can try them in parallel. The first to complete is the one reported as successful. Typically, Qed is credited with proving 60% of the verification conditions, Alt-Ergo is credited with 33-37%, and CVC4
and CVC5 are credited with a few percent each. Within 1000 seconds, Alt-Ergo was able to prove all verification conditions for all variants. CVC5 could prove all up through Change #8, but misses some afterwards. CVC4 and Z3 miss some for all variants.

## 4.2 Verification bottlenecks

None of the authors of this paper had any previous experience with Frama-C. The first author, however, had extensive previous experience with Why-3, which also relies on SMT solvers. Frama-C itself relies on Why3 for its interaction with SMT solvers, giving a similar experience “under the hood”.

A recurring challenge was the need to define properties of memory regions, i.e., whether read or write is valid, whether there are aliases, and whether modifications are possible. As noted in Section 3.10, modifications and aliases must be declared for `cpumask_andnot`. Our first intuition was that there should be a separate behavior for each possible pattern of aliases among the arguments and that the `assigns` annotations should take these aliases into account explicitly. This caused us to create a behavior for each pattern of aliases among the arguments of `cpumask_andnot`, each with its own specific `assigns` declaration. At the time, we were using Frama-C 27.1 in which such behavior-specific `assigns` annotations caused timeouts. Even with this situation resolved in Frama-C 28.1, the verification of `should_we_balance()` did not complete in practice, perhaps due to an overload of unnecessary specifications. In the end, we found that it was not necessary to have a behavior per pattern of aliases; the specifications described in Section 3.10, where the only mention of the aliases is in the `separated` declarations, were sufficient to cover all of the cases.

Again to reduce the need to define properties of memory regions, we initially started with the following simplified definitions of the `cpumask` data structure and of the set of temporary buffers used in Changes #9 and #10:

```c
struct cpumask { bool bits[FINT_MAX]; };
struct cpumask should_we_balance_tmpmask[FINT_MAX];
```

We furthermore defined a collection of global variables of type `cpumask`, as well as the types of other structures used by `should_we_balance`. As global variables are intrinsically separated, this strategy reduced the need to think about aliases. Furthermore, as the masks are stored directly in their containing structures, only one validity declaration was needed for each structure.

These solutions, however, were not very satisfying, because the correctness of `should_we_balance` should not depend on the values of constants such as the mask size, and because the use of global variables for quantities such as `group_balance_mask sg` hides the fact that this call should give a different mask for different values of `sg`. We thus replaced the `cpumask` type by:

```c
struct cpumask { bool *bits; };
struct cpumask *should_we_balance_tmpmask;
```

and replaced the global variables by preconditions requiring the existence and validity of the various referenced structures. These changes doubled the number
of validity declarations, as the pointer to the `cpumask` and the mask itself are now separate entities. They also required declaring that the buffer cpumasks referenced by `should_we_balance_tmpmask`, which are modified by `cpumask_copy` and `cpumask_andnot`, are separated from the other cpumasks, which are only readable. In the end, a few macros were sufficient to hide most of this complexity. Still, starting from Change #9, where `cpumask_andnot` is introduced within a loop, it is necessary to add an assert, `relevant.cpu, env)` in the return path where an idle core is detected (line 18, Figure 5), suggesting that the increase in information due to representing a mask as a pointer makes it harder for the SMT solver to prove some basic information.

Frama-C allows the user to define proof scripts through the GUI to, e.g., specify when to unfold predicates before submitting formulas to the SMT solvers. These scripts can then be saved and reloaded on a future proof attempt. With the goal of providing a single file with the complete proof annotations, we do not use this feature, and instead rely on the Frama-C simplifier Qed and the SMT solvers to perform all of the proof operations. The difficulties cited above in getting the proofs of Changes #9 and #10 to go through, however, suggest that more manual guidance via proof scripts may be needed for more complex proof efforts. Correnson et al. [14] propose an approach to inferring scripts from some initial proof steps that may facilitate this effort.

## 4.3 A missed opportunity for optimization?

Change #9 (Section 3.10) removes the hyperthreads of a CPU from the set of relevant CPUs when an idle CPU is found to have at least one non-idle hyperthread. Reflecting on the invariants while verifying this code revealed that there is another opportunity for this optimization. When a CPU is itself not idle then its core is also not idle, and there is no need to check the hyperthreads if an idle CPU has already been identified (`idle_smt` is not -1). The code change is below. No change is needed in the specifications.

```c
forEach_cpu_and(cpu, swb_cpus, env->cpus) {
    if (!idle_cpu(cpu))
        if (!idle_cpu(cpu)) {
            #ifdef CONFIG_SCHED_SMT
            if (idle_smt != -1)
                cpumask_andnot(swb_cpus, swb_cpus, cpu_smt_mask(cpu));
            #endif
            continue;
        }
}
```

## 4.4 The intention of `should_we_balance()`

There is, in general, some latitude in designing specifications. If we can prove $P \implies Q$, for pre and post conditions $P$ and $Q$, we can also prove $P' \implies Q'$, for some more specific pre condition $P'$, i.e., where $P' \implies P$, and some more general post condition $Q'$, i.e., where $Q \implies Q'$. In our experiments, the chosen pre and post conditions follow the code structure and thus can be viewed as
providing a concise presentation of what the code does, rather than showing
that the code successfully achieves some externally defined property.

A more high-level understanding of `should_we_balance()` is that for a set of non newly idle requesting CPUs, at most one should be allowed to balance at a given in time; being the idle CPU with the lowest index, as stated in our post conditions, is unimportant. While pre and post conditions focus on a single run, proving this property requires comparing runs for different CPUs, i.e., the one that returns **true** and the others that must return **false**. As our focus is on how code changes affect pre and post conditions and the ability to verify them, we have not yet explored proving this more general property. However, we expect that it should be provable (when it is true) from the pre and post conditions that we have defined, rather than requiring to again descend to the source code.

# 5 Related Work

*Verification tools.* VeriFast [23] is a deductive verifier for C and Java programs. The main differences from Frama-C are that it uses symbolic execution to explore all possible paths and that it supports the use of separation logic in specifications. Unfortunately, our first attempt to apply VeriFast was unsuccessful due to parsing errors. We have recently reported these issues and they were quickly solved.<fnref n="7" /> We will try our experiment using VeriFast in future work.

CN [36] verifies C code, based on translation of the code using the C semantic model Cerberus [31]. Specifications for CN are constrained to be decidable, and thus the SMT solver used, Z3, can produce counterexamples that are helpful in debugging specifications. Nevertheless, CN is not yet mature. For example, it does not yet support specification formulas that contain multiple quantifiers. Thus, we have not yet been able to try our experiment with CN.

Regression verification [18, 20] and SymDiff [26] prove that no regressions occur after a program has been updated by verifying the equivalence between the original program and its updated version. In these approaches, two programs are considered equivalent only if, for any given input, the results of both programs are identical. However, this notion of program equivalence does not align with our setting, where the behaviors of a target program can change across versions.

*Linux kernel verification.* Bristot de Oliveira et al. [8] target formal verification of the Linux kernel via dynamic analysis. They enable injecting an automaton that expresses required state transitions into the kernel source code. Their approach should apply to multiple variants of the kernel. However, like any form of dynamic analysis, their approach relies on the adequate choice of test cases. Furthermore, they focus on generic properties, reducing the chance of finding semantic bugs.

Efremov et al. [17] use a verification toolchain building on Frama-C to verify a collection of Linux kernel string and memory manipulation functions. The correctness of these functions typically must consider the possibility of aliases,

<footnote n="7">⁷ https://github.com/verifast/verifast/issues/{500,507}</footnote>
including overlapping memory regions, as well as the granularity of pointer arith-
metic and the possibility of arithmetic overflows. We focus on algorithmic issues
and rely on pre conditions that assume that such pointer and arithmetic issues
cannot arise. Our main focus is on the impact of code changes over multiple
versions. Nevertheless, the specifications developed by Efremov et al. could be
useful in a generalization of our work to functions that rely on such string and
memory manipulation functions.

Abstract interpretation [15] also enables program verification. Giet et al. [19] introduce a novel abstract domain to capture detailed properties of data structures, which they apply within MemCAD [37] to prove the functional correctness of the Linux kernel list data structure. Their approach primarily targets specific correctness of data structures rather than the global properties of functions. Recently, Bernier et al. [4] have shown that combining Frama-C with MemCAD helps state and prove the kinds of memory validity and separation properties that we found challenging to declare correctly (see Section 4.2). Such an approach can help the user focus on the proofs of algorithmic properties.

# 6 Conclusion

While formal verification has the potential to precisely capture the semantics of
source code and thus to facilitate the identification of semantic bugs, it requires
a substantial manual effort to write the necessary specifications. In this paper,
we have set out to study whether it may be possible to reuse specifications as
the source code changes. While this initial case study has focused on a single
small function from the Linux kernel, we argue that we have obtained promising
results. When the core algorithm does not change, the proof goes through with
only minor tweaks, many of which we were able to perform in a matter of minutes.
When the core algorithm does change, substantially more effort is required,
with several months of work required for the changes in the most recent Linux
versions. Nevertheless, we also found a bug and a potential missed optimization
opportunity in these cases. Furthermore, some of the encountered difficulties
may have resulted from insufficient familiarity with Frama-C, in particular the
kinds of declarations needed around pointers; the practical aspects that we have
learned here can facilitate future efforts.

In the future, we plan to perform a systematic study of the costs and benefits
of verification for the Linux kernel, over time as the code evolves. We will explore
opportunities to develop tools to automate the process and to facilitate the reuse
of verification efforts. Indeed, the third author has experimented with one version
of the Linux kernel scheduler function `select_idle_core()`, which shares some
functionalities with `should_we_balance()`, and has been able to reuse some of
the specifications developed here, giving hope that such reuse could be more
general, particularly within a single Linux kernel subsystem.

***Acknowledgements.*** We would like to thank the Frama-C team for their quick and thorough feedback throughout this work. We would like to thank Olivier Danvy and Xavier Rival for their feedback on preliminary drafts of this paper.
## References

1. H. Barbosa, C. W. Barrett, M. Brain, G. Kremer, H. Lachnitt, M. Mann, A. Mohamed, M. Mohamed, A. Niemetz, A. Nötzli, A. Ozdemir, M. Preiner, A. Reynolds, Y. Sheng, C. Tinelli, and Y. Zohar. cvc5: A versatile and industrial-strength SMT solver. In *TACAS*, volume 13243 of LNCS, pages 415–442. Springer, 2022.

2. C. W. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanovic, T. King, A. Reynolds, and C. Tinelli. CVC4. In *CAV*, volume 6806 of LNCS, pages 171–177. Springer, 2011.

3. P. Baudin, J.-C. Filliâtre, C. Marché, B. Monate, Y. Moy, and V. Prevosto. ACSL: *ANSI/ISO C Specification Language*.

4. T. Bernier, Y. Ziani, N. Kosmatov, and F. Louergue. Combining deductive verification with shape analysis. In D. Beyer and A. Cavalcanti, editors, *FASE*, volume 14573 of LNCS, pages 280–289. Springer, 2024.

5. Y. Bertot and P. Castéran. *Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions*. Texts in Theoretical Computer Science. An EATCS Series (TTCS). Springer, 2004.

6. A. Bessey, K. Block, B. Chelf, A. Chou, B. Fulton, S. Hallem, C. Gros, A. Kamsky, S. McPeak, and D. R. Engler. A few billion lines of code later: using static analysis to find bugs in the real world. *Commun. ACM*, 53(2):66–75, 2010.

7. F. Bobot, J.-C. Filliâtre, C. Marché, and A. Paskevich. Why3: Shepherd your herd of provers. In *Boogie 2011: First International Workshop on Intermediate Verification Languages*, pages 53–64, Wrocław, Poland, August 2011. https://hal.inria.fr/hal-00790310.

8. D. Bristot de Oliveira, T. Cucinotta, and R. S. de Oliveira. Efficient formal verification for the Linux kernel. In *Software Engineering and Formal Methods (SEFM)*, volume 11724 of LNCS, pages 315–332. Springer, 2019.

9. N. Brown. Smatch: pluggable static analysis for C. *Linux Weekly News*, June 2016.

10. S. Conchon, A. Coquereau, M. Iguernlala, and A. Mebsout. Alt-Ergo 2.2. In *SMT Workshop: International Workshop on Satisfiability Modulo Theories*, Oxford, United Kingdom, July 2018.

11. J. Corbet. The managed resource API. *Linux Weekly News*, Feb. 2007.

12. J. Corbet. Committing to Rust for kernel code. *Linux Weekly News*, Nov. 2023.

13. J. Corbet. Scope-based resource management for the kernel. *Linux Weekly News*, June 2023.

14. L. Correnson, A. Blanchard, A. Djoudi, and N. Kosmatov. Automate where automation fails: Proof strategies for Frama-C/WP. In *TACAS*, volume 14570 of LNCS, pages 331–339. Springer, 2024.

15. P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In *POPL*, pages 238–252, 1977.

16. P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yakobowski. Frama-C – A software analysis perspective. In *Software Engineering and Formal Methods (SEFM)*, volume 7504 of LNCS, pages 233–247. Springer, 2012.

17. D. Efremov, M. U. Mandrykin, and A. V. Khoroshilov. Deductive verification of unmodified Linux kernel library functions. In *Leveraging Applications of Formal Methods, Verification and Validation. Verification (ISOLA)*, volume 11245 of LNCS, pages 216–234. Springer, 2018.

18. D. Felsing, S. Grebing, V. Klebanov, P. Rümmer, and M. Ulbrich. Automating regression verification. In *Automated Software Engineering (ASE)*, pages 349–360, 2014.
19. J. Giet, F. Ridoux, and X. Rival. A product of shape and sequence abstractions. In *SAS*, volume 14284 of *LNCS*, pages 310–342. Springer, 2023.

20. B. Godlin and O. Strichman. Regression verification. In *Design Automation Conference (DAC)*, pages 466–471, 2009.

21. D. Greenaway, J. Lim, J. Andronick, and G. Klein. Don't sweat the small stuff: formal verification of C code without the pain. In *PLDI*, pages 429–439, 2014.

22. R. Gu, Z. Shao, H. Chen, X. N. Wu, J. Kim, V. Sjöberg, and D. Costanzo. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In *OSDI*, pages 653–669, 2016.

23. B. Jacobs, J. Smans, P. Philippaerts, F. Vogels, W. Penninckx, and F. Piessens. Verifast: A powerful, sound, predictable, fast verifier for C and Java. In *NASA Formal Methods - Third International Symposium (NFM)*, volume 6617 of *LNCS*, pages 41–55. Springer, 2011.

24. S. Kim, M. Xu, S. Kashyap, J. Yoon, W. Xu, and T. Kim. Finding semantic bugs in file systems with an extensible fuzzing framework. In *SOSP*, pages 207–220, 2019.

25. G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. A. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood. seL4: formal verification of an OS kernel. In *SOSP*, pages 207–220, 2009.

26. S. K. Lahiri, C. Hawblitzel, M. Kawaguchi, and H. Rebêlo. SYMDIFF: A language-agnostic semantic diff tool for imperative programs. In *CAV*, volume 7358 of *LNCS*, pages 712–717. Springer, 2012.

27. J. Lawall and G. Muller. Coccinelle: 10 years of automated evolution in the Linux kernel. In *USENIX Annual Technical Conference*, pages 601–614, 2018.

28. B. Lepers, R. Gouicem, D. Carver, J. Lozi, N. Palix, M. Aponte, W. Zwaenepoel, J. Sopena, J. Lawall, and G. Muller. Provable multicore schedulers with Ipanema: application to work conservation. In *EuroSys*, pages 3:1–3:16, 2020.

29. R. Levin, E. S. Cohen, W. M. Corwin, F. J. Pollack, and W. A. Wulf. Policy/mechanism separation in HYDRA. In *SOSP*, pages 132–140, 1975.

30. S. Lu, Z. Li, F. Qin, L. Tan, P. Zhou, and Y. Zhou. Bugbench: Benchmarks for evaluating bug detection tools. In *Workshop on the evaluation of software defect detection tools (BUGS)*, volume 5, 2005.

31. K. Memarian, J. Matthiesen, J. Lingard, K. Nienhuis, D. Chisnall, R. N. M. Watson, and P. Sewell. Into the depths of C: elaborating the de facto standards. In *PLDI*, pages 1–15, 2016.

32. L. Mendonça de Moura and N. S. Bjørner. Z3: an efficient SMT solver. In *TACAS*, volume 4963 of *LNCS*, pages 337–340. Springer, 2008.

33. M. L. Miller and I. P. Goldstein. SPADE: A grammar based editor for planning and debugging programs, 1976. MIT AI Memo no. 386.

34. N. Palix, G. Thomas, S. Saha, C. Calvès, G. Muller, and J. Lawall. Faults in Linux 2.6. *ACM Trans. Comput. Syst.*, 32(2):4:1–4:40, 2014.

35. M. Paturel, I. Subasinghe, and G. Heiser. First steps in verifying the seL4 core platform. In *Asia-Pacific Workshop on Systems (APSys)*, pages 9–15, 2023.

36. C. Pulte, D. C. Makwana, T. Sewell, K. Memarian, P. Sewell, and N. Krishnaswami. CN: verifying systems C code with separation-logic refinement types. *Proc. ACM Program. Lang.*, 7(POPL):1–32, 2023.

37. P. Sotin and X. Rival. Hierarchical shape abstraction of dynamic structures in static blocks. In *Programming Languages and Systems - 10th Asian Symposium (APLAS)*, volume 7705 of *LNCS*, pages 131–147. Springer, 2012.