# Understanding Linux Kernel Code through Formal Verification: A Case Study of the Task-Scheduler Function select_idle_core

Julia Lawall, Keisuke Nishimura, Jean-Pierre Lozi

► To cite this version:

Julia Lawall, Keisuke Nishimura, Jean-Pierre Lozi. Understanding Linux Kernel Code through Formal Verification: A Case Study of the Task-Scheduler Function select_idle_core. OLIVIERFEST '25 - Workshop Dedicated to Olivier Danvy on the Occasion of His 64th Birthday, Oct 2025, Singapore, Singapore. pp.94 - 105, 10.1145/3759427.3760371. hal-05337063

HAL Id: hal-05337063

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

Submitted on 29 Oct 2025

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
# Understanding Linux Kernel Code through Formal Verification

## A Case Study of the Task-Scheduler Function select_idle_core

### Julia Lawall

Inria
Paris, France
julia.lawall@inria.fr

### Keisuke Nishimura

Inria
Paris, France
keisuke.nishimura@inria.fr

### Jean-Pierre Lozi

Inria
Paris, France
jean-pierre.lozi@inria.fr

## Abstract

On the one hand, the Linux kernel task scheduler is critical to all application performance. On the other hand, it is widely agreed that its code complexity is spiraling out of control, and only a tiny handful of kernel developers understand it. We are exploring the opportunities and challenges in applying formal verification to Linux kernel task-scheduler code. Building on a previous work focusing on the evolution of the function *should_we_balance*, we here consider a version of the key task-placement function *select_idle_core* and the evolution of the iterators on which it relies.

**CCS Concepts: Software and its engineering → Formal software verification; Software evolution.**

**Keywords:** Linux kernel, scheduling, verification, Frama-C

**ACM Reference Format:**

Julia Lawall, Keisuke Nishimura, and Jean-Pierre Lozi. 2025. Understanding Linux Kernel Code through Formal Verification: A Case Study of the Task-Scheduler Function *select_idle_core*. In *Proceedings of the Workshop Dedicated to Olivier Danvy on the Occasion of His 64th Birthday (OLIVIERFEST '25), October 12–18, 2025, Singapore, Singapore*. ACM, New York, NY, USA, 12 pages. https://doi.org/10.1145/3759427.3760371

## 1 Introduction

The Linux kernel task scheduler is responsible for placing tasks on CPUs and for selecting which task placed on a given CPU should be allowed to run. As such, it has a substantial impact on application performance. Recent research and discussions in the Linux kernel developer community have put forth the point of view that the scheduler, at over 34,000 lines of code, is becoming too complex to understand while at the same time not adequately meeting the needs of all kinds of workloads. Proposals have emerged for frameworks allowing the implementation and use of more specific scheduling

policies [6, 7, 14]. Nevertheless, even the most developed of these do not yet provide out of the box all of the algorithms and functionalities found in the mainline Linux kernel scheduler [8]. It thus may be valuable to fully understand what the current Linux kernel task scheduler offers before we abandon it for something else.

This paper represents a small step in the direction of understanding the Linux kernel task scheduler. Inspired by the recent work of Olivier Danvy on using mechanized theorem proving to teach programming concepts [10], we turn to formal verification as a means of organizing our understanding of the code. Verification of source code requires writing specifications that describe the expected inputs (preconditions) and corresponding outputs (postconditions). The approach that we follow, based on the C-code program-analysis framework Frama-C [9] with the weakest precondition (WP) plugin, also requires writing loop invariants, and allows writing assertions to facilitate the verification process. Writing such specifications and verifying that they accurately describe the behavior of the source code tends to reveal all of the subtleties of the code and its interactions.

Here, we apply this code-understanding approach to the problem of reasoning about complex iterators, as are used by the scheduler function *select_idle_core*. This function is used as part of the algorithm for placing a waking task on a CPU. We take an older version of this function, from 2016, because it is compatible with multiple successive iterator definitions, making it possible to explore the impact of the design choices of these iterators both from a proof and from a programming perspective. While not a main aim of this work, the reflection on the code entailed by this experiment highlighted a possibly undesirable feature that remains in the task scheduler of the latest Linux kernel version (v6.15, released in May 2025) as well as a probable refactoring gone wrong that survived from 2009 until the affected code was deleted in 2022.

The rest of this paper is organized as follows. Section 2 introduces some terminology needed to understand both *select_idle_core* and Frama-C. Section 3 presents the source code under consideration. Section 4 presents the developed specifications. Section 5 presents some lessons learned from the verification experiment. Section 6 presents related

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

This work is licensed under a Creative Commons Attribution 4.0 International License.

OLIVIERFEST '25, Singapore, Singapore

© 2025 Copyright held by the owner/author(s).

ACM ISBN 979-8-4007-2150-2/25/10

https://doi.org/10.1145/3759427.3760371
work. Section 7 concludes. All of the source code used in this work is available in our artifact, described in the appendix.

# 2 Terminology

We begin by establishing some terminology about task scheduling, verification using Frama-C, and for loops.

## 2.1 Scheduler Terminology

The function `select_idle_core` that we are concerned with is part of the implementation of the function `select_idleSibling` that is used by the Linux kernel task scheduler for non-real-time tasks to select a CPU on which a task should run. Accordingly, we introduce some Linux kernel terminology related to this task placement problem.

The Linux kernel task scheduler uses `CPU` to refer to an individual unit of computation. Multiple CPUs can be implemented on a single physical core; this kind of concurrency is referred to as simultaneous multithreading (SMT). Running multiple tasks concurrently on a single core is thus possible, but performance may be better if a task runs on a core alone. A `CPU` is considered to be idle if there is no task running on it. A core is considered to be idle if there is no task running on any of its CPUs.

The Linux kernel task scheduler takes into account core idleness in placing tasks. CPUs are organized into a scheduling hierarchy, each level of which partitions the set of CPUs. Each element of such a partition is a *scheduling domain*. Our target function `select_idle_core` is only concerned with the scheduling domains consisting of the set of tasks that share a Last Level Cache (LLC).

A set of CPUs, e.g., those in a given scheduling domain or those desired for a particular task, is represented in the Linux kernel as a mask, in which 0 means that the CPU is not in the set and 1 means that the CPU is in the set. In the Linux kernel, these masks are packed into an array of long integers. For simplicity, we reimplement masks and all of the low-level mask operations on boolean arrays (see the files `loops.c` and `globals.c` in the artifact for details).

The Linux kernel scheduler runs independently on each `CPU`, and is thus highly concurrent. Most of the algorithms in the scheduler, however, are speculative, and ignore the possibility of concurrency. Our goal here is to study the execution of `select_idle_core` in isolation, and thus our proof efforts do not take concurrency into account.

## 2.2 Verification Terminology

Verification of source code entails writing pre- and postconditions describing the inputs and outputs of the code, and then proving that they are respected by the implementation. Frama-C allows such specifications to be organized as a collection of *behaviors*, which provide information about the inputs and outputs under specific conditions. Frama-C also requires that loops be annotated with loop invariants,

including showing loop side effects and termination. Loop invariants thus typically include information about the range of the loop index, information accumulated from previous iterations, a list of any modified memory locations, and a *loop variant* expression evaluating to an integer that becomes increasingly close to 0 on each iteration. Finally, Frama-C allows providing information about memory regions, whether they can be read or written and whether they may overlap with other memory regions. The latter issue is not the focus of this paper, but such declarations are needed in practice and are included in the artifact.

In expressing the invariants it is often useful to quantify over a set of bits, or the set of bits that are set (1) in a mask. For conciseness, we define the macros shown in Figure 1. `allbits(i,p)` (lines 1-2) introduces a new universally quantified integer variable `i` that may be referenced by property `p`. If the variable `i` is found to be in the range `[0, nr_cpu_ids-1]` (`nr_cpu_ids` is a global variable with unspecified value indicating the number of CPUs on the machine), then the property `p` should hold. `existsbits(i,p)` (lines 5-6) is analogous, but `i` is existentially quantified. `allmaskbits(i,mask,p)` and `existsmaskbits(i,mask,p)` (lines 3-4 and 7-8) are similar, but add the further constraint that the offset `i` should be set in the mask. These macros encapsulate simple specifications, but are useful to reduce clutter.

1 #define allbits(i,p) 
2 (\forall integer i; 0 <= i < nr_cpu_ids == > (p))
3 #define allmaskbits(i,mask,p) 
4 allbits(i, cpumask_bits[i] == > (p))
5 #define existsbits(i,p) 
6 (\exists integer i; 0 <= i < nr_cpu_ids && (p))
7 #define existsmaskbits(i,mask,p) 
8 existsbits(i, cpumask_bits Mask)[i] && (p))

<caption>Figure 1. Macros for use in defining loop invariants</caption>

## 2.3 Loop Terminology

The definition of `select_idle_core` interacts closely with the definitions of the iterators over CPU masks. These iterators are implemented as `for` loops. We refer to the components of a `for` loop header for `(initialization; test; update)` as the initialization, test, and update, respectively.

# 3 Implementation

## 3.1 Core Selection Algorithm

The `select_idle_core` implementation from Linux kernel commit 10e2f1acd010 (May 2016) is shown in Figure 2. This function takes three arguments: 1) a representation of the task `p`, which is the task for which the function should try to find an idle core, 2) a representation of a scheduling domain indicating the set of CPUs that are under consideration for placing `p`, and 3) a target `CPU`, which is the first choice if
that CPU satisfies all of the placement constraints. The target CPU is either the CPU where task p was running previously, or the CPU of the waker task, if heuristics have suggested that placing p near the waker will improve performance. The definition of `select_idle_core` then amounts to a collection of interleaved heuristics.

```c
1 static int select_idle_core(struct task_struct *p,
2                          struct sched_domain *sd, int target) {
3     struct cpumask *cpus =
4         this_cpu_cpmask_var_ptr(select_idle_mask);
5     int core, cpu;
6     if (!test_idle Cores(target, false)) // heuristic 1
7         return -1;
8     cpumask_and(cpus, sched_domain_span sd);
9     tsk_cpus_allowed(p);
10    for Each_cpuWrap (core, cpus, target) { // heuristic 2
11        bool idle = true;
12        for Each_cpu (cpu, cpu_smt_mask (core)) { // heuristic 3
13            cpumask_clear_cpu (cpu, cpus); // heuristic 4
14            if (!idle_cpu (cpu))
15                idle = false;
16        }
17        if (idle) return core;
18    }
19    set_idle Cores(target, 0);
20    return -1;
21}
```

<caption>Figure 2. `select_idle_core` implementation from Linux kernel commit 10e2f1acd010</caption>

The first heuristic (lines 6, 7, and 19) is that if all cores in the same scheduling domain as `target` are known to not be idle, as recorded by a flag set on a previous call to `select_idle_core`, then there is no need to analyze any of them. Indeed, running `select_idle_core` entails remote memory accesses to the data structures of other CPUs, which have a non-negligible cost, so aborting a search that is certain to fail has a performance benefit. Lines 6 and 7 detect that there are no idle cores, and line 19 records that no idle core has been detected, to be used on the next invocation. The associated flag is reset by other scheduler code when any CPU in the same scheduling domain becomes idle.

The second heuristic is that the search for an idle core should proceed sequentially through the available CPUs, starting at the target. In practice, many CPUs may be running `select_idle_core` for different tasks p concurrently, and starting the search for each at a different target increases the chance that the different tasks will be placed on different CPUs. Furthermore, only CPUs that are in the desired domain and that are acceptable to the task p should be considered. The set of these CPUs is represented by the mask cpus, computed on line 8 by intersecting `sched_domain_span sd`, representing the CPUs in the scheduling domain, and `tsk_cpus_allowed(p)`, representing the CPUs allowed by the task. The iterator on line 10 (`for Each_cpuWrap`) starts with `target` and checks whether any successive acceptable CPU is on an idle core until reaching the maximum number of CPUs, at which point it wraps around to CPU 0,

checking each remaining successive CPU until reaching the target. Only CPUs in the mask `cpus` are considered.

The third heuristic is that the search as to whether a CPU is part of an idle core needs to check all of the CPUs on the core, represented by `cpu_smt_mask(core)`, to see if any is not idle. If such a nonidle CPU exists, then the core is not idle; otherwise it is idle. As there is no advantage to starting with one CPU or another, the search is done using `for Each_cpu` (line 12), which starts at CPU 0.

The final heuristic is to observe that once all the CPUs of a core have been tested once for idleness, there is no need to test them again, as the associated core has already been determined not to be idle. The call to `cpumask_clear_cpu` (line 13) removes these CPUs from the mask `cpus` used by the outer loop, implying that despite the pair of nested loops, each CPU is only tested for idleness once.

## 3.2 Iterator Implementation

The function `select_idle_core` involves two Linux-kernel specific iterators, defined as macros: `for Each_cpu` and `for Each_cpuWrap`. The implementations of both of these iterators have changed over time. We consider the implementations from their introduction, in 2008 and 2016, respectively, through the present day (Linux v6.15). Note that the code shown in Figure 2 was not actually used with all of these definitions, because the definition of `select_idle_core` has changed as well. As our focus is on the impact of the changes in the definitions of the iterators, we consider only the changes to Figure 2 that are necessary to use the different iterator definitions, and ignore other changes in the `select_idle_core` implementation.

Evolution of `for Each_cpu`. The macro `for Each_cpu`, as defined in Figure 3 (lines 34-37), was introduced in 2008 in the commit 2d3854a37e8b in the file `include/linux/`-`cpumask.h`. The arguments are an index variable and a mask. It expands to a `for` loop header. The header first initializes the index variable to -1. Then, each test, somewhat unusually, first uses `cpumask_next` (line 36) to find the offset of the next 1 value in the mask and then checks that that offset is smaller than the number of elements in the mask (line 37). The loop header has no update component. `cpumask_next` is essentially a wrapper for `find_next_bit`. For conciseness, we omit the specification of `cpumask_next`<fnref n="1" /> and provide only the specification of `find_next_bit`, in terms of our array-based implementation of `cpumask`.

Commit 33e67710beda, from Sep. 19, 2022, then redefined `for Each_cpu` as shown in Figure 4. The new definition simply invokes another macro, `for Each_set_bit`, which again creates a `for` loop header. This loop header uses `find_next_bit` to initialize the index variable to the offset of the first CPU included in the mask, and `find_next_bit` again to

<footnote n="1">¹Details can be found in the artifact.</footnote>
1 /*@ 2 requires size <= NR_CPU$; 3 requires 0 <= offset <= nr\_cpumask\_bits <= NR_CPU$; 4 requires \valid\_read addr + (0 .. size\_1); 5 assigns \nothing; 6 7 behavior above: 8 assumes \exists integer j; offset <= j < size && addr[j]; 9 ensures offset <= \result < size; 10 ensures addr[\result]; 11 ensures \forall integer j; 12 offset <= j < \result == > !addr[j]; 13 14 behavior nowhere: 15 assumes \forallall integer j; 16 offset <= j < size == > !addr[j]; 17 ensures \result == size; 18 19 complete behaviors; 20 disjoint behaviors; 21 */ 22 static int 23 find\_next\_bit ( const bool *addr, unsigned long size, 24 unsigned long offset); 25 26 static inline unsigned int 27 cpumask\_next (int n, const struct cpumask *srcp) { 28 /* -1 is a legal arg here. */ 29 if (n != -1) cpumask\_check(n); 30 return find\_next\_bit (cpumask\_bits (srcp), 31 nr\_cpumask\_bits, n+1); 32 } 33 34 #define for\_each\_cpu (cpu, mask) \ 35 for ((cpu) = -1; 36 (cpu) = cpumask\_next((cpu), (mask)), 37 (cpu) < nr\_cpu\_ids; )

<caption>**Figure 3.** The original `for Each cpu` implementation from Linux kernel commit 2d3854a37e8b, Nov. 5, 2008</caption>

subsequently update it. `find_next_bit` has the same specification as shown in Figure 3. Commit 33e67710beda was then immediately followed by commit fdae96a3fc7f, on the same day, that merged the two calls to `find_next_bit` to a single one before the loop test, as shown in Figure 5.

1 #define for Each_set\_bit (bit, addr, size) \
2 for ((bit) = find\_next\_bit((addr), (size), 0); \
3 (bit) < (size); \
4 (bit) = find\_next\_bit((addr), (size), (bit) + 1))
5
6 #define for Each_cpu (cpu, mask) \
7 for\_each\_set\_bit (cpu, cpumask\_bits (mask), nr\_cpumask\_bits)

<caption>**Figure 4.** Updated `for Each_cpu` implementation from Linux kernel commit 33e67710beda, Sep. 19, 2022</caption>

1 #define for Each_set\_bit (bit, addr, size) \
2 for ((bit) = 0; \
3 (bit) = find\_next\_bit((addr), (size), (bit)), (bit) < (size); \
4 (bit)++)

<caption>**Figure 5.** Updated `for Each_cpu` implementation from Linux kernel commit fdae96a3fc7f, Sep. 19, 2022</caption>

**Evolution of for Each_cpuWrap.** `for Each_cpu_`-wrap (Figure 6) was first introduced in commit 10e2f1acd010, in `kernel/sched/fair.c`,<fnref n="2" /> on May 9, 2016. The arguments are, as for `for Each_cpu`, the index variable and the mask, followed by the offset of the starting CPU and a flag variable that records whether the index variable has reached the end of the mask and should move back to CPU 0. The definition of `for Each_cpuWrap` is analogous to the original definition of `for Each_cpu`, in that the index variable starts out below the start point and updates are done in the test expression of the generated loop header; the update section is empty.

1 int cpumask\_next\_wrap (int n, const struct cpumask *mask, 2 int start, bool wrap) { 3 int next; 4 again: 5 next = cpumask\_next(n, mask); 6 if (wrap && n < start && next >= start) { 7 return nr\_cpumask\_bits; 8 } else if (next >= nr\_cpumask\_bits) { 9 wrap = true; 10 n = -1; 11 goto again; 12 } 13 return next; 14 } 15
16 #define for\_each\_cpu\_wrap (cpu, mask, start, wrap) \
17 for ((wrap) = 0, (cpu) = (start) -1; 18 (cpu) = cpumask\_next\_wrap((cpu), (mask), (start), 19 &(wrap)), 20 (cpu) < nr\_cpumask\_bits; )

<caption>**Figure 6.** The original `for Each_cpuWrap` implementation from Linux kernel commit 10e2f1acd010, May 9, 2016</caption>

The macro `for Each_cpuWrap` relies on the `cpumask_next-wrap` function (lines 1-14 of Figure 6) to find the next CPU, analogous to the use of `find_next_bit` in Figure 4. This function introduces some complexity for Frama-C. In its definition, the statement `goto again;` amounts to a loop, but there is no place to put a loop invariant. Fortunately, `goto again;` is only useful for the wrap around, which is only executed once. To eliminate the loop, we manually unroll it, by inlining the code following again at the point of the `goto again;`. To ensure that the introduced second `goto` is dead code, we replace it by `assert false;`. The rewritten definition is available in the artifact. `cpumask_next-wrap` relies on `cpumask_next`, defined in Figure 3 (lines 26-32).

A new definition of `for Each_cpuWrap`, shown in Figure 7, was introduced in commit c743f0a5c50f, now in `include/./linux/cpumask.h`, in Apr. 14, 2017. The arguments are now only the loop index, the mask, and the offset of the starting CPU. The definition is analogous to the second definition of `for Each_cpu` shown in Figure 4 (which came several years later), in that the calls to the function `cpumask_next-wrap` to find the next CPU are now in the initialization and the update section of the `for` loop header. The wrap flag is

<footnote n="2">²Placing a macro definition in a .c file suggests that the macro may be seen as dedicated to that file, and not of general interest.</footnote>
no longer exposed to the function using the iterator, e.g., `select_idle_core`; instead, it merely indicates whether the call comes from the initialization section of the for loop, where the start value is a CPU to consider, or the update section, where the start value indicates the end of the iteration.

1 #define for Each_cpuWrap (cpu, mask, start) \
2 for ((cpu) = cpumask_nextWrap((start)-1, (mask), \
3 (start), false); \
4 (cpu) < nr_cpmask_bits; \
5 (cpu) = cpumask_nextWrap((cpu), (mask), \
6 (start), true))

<caption>**Figure 7.** Updated `for Each_cpuWrap` implementation from Linux kernel commit c743f0a5c50f, Apr. 14, 2017</caption>

A third definition of `for Each_cpuWrap`, as shown in Figure 8, was introduced in commit 4fe49b3b97c2, on Sep. 19, 2022. The arguments are again the loop index, the mask, and the offset of the starting CPU. Just as the implementation of `for Each_cpu` introduced on the same date uses the macro `for Each_set_bit`, this implementation of `for Each_cpuWrap` uses `for Each_set_bitWrap`. This macro completely abandons the wrap flags, and reflects the difference in behavior between the initialization and the update by calling different functions; `find_next_bitWrap` for the initialization and `__for EachWrap` for the update. The definitions of these two functions look quite different, with different parameter names, different function calls, and different if nesting depths. In practice, however, `find_next_bitWrap` is a specialization of `__for EachWrap` to the fact that the starting offset is initially a valid result, rather than the stopping point. `find_first_bit` searches for the first set bit in a mask; the definition is omitted for conciseness.

**Summary.** We see that `for Each_cpu` and `for Each_cpuWrap` have evolved in a similar way, although not at exactly the same time. Both start with an unusual implementation, where the loop index contains an invalid CPU (-1) after the initialization and the old CPU value after the update, and is only given the correct CPU value in the loop test expression. Both are later rewritten in a more standard way where the initialization and update set the loop index to the next CPU to consider. The evolution of `for Each_cpuWrap` further addresses the question of how to know when the end of the mask has been detected and it is time to wrap. This is initially done by requiring the client to maintain the state, received as the parameter wrap, and then by shifting this information to an internal flag, and finally by choosing between two different functions, optimized for the different cases.

1 static inline unsigned long \
2 find_next_bitWrap(const unsigned long *addr, \
3 unsigned long size, unsigned long offset) { \
4 unsigned long bit = find_next_bit(addr, size, offset); \
5 if (bit < size) return bit; \
6 bit = find_first_bit(addr, offset); \
7 return bit < offset ? bit : size; \
8 } \
9 \
10 static inline unsigned long \
11 __for EachWrap(const unsigned long * bitmap, \
12 unsigned long size, unsigned long start, \
13 unsigned long n) { \
14 unsigned long bit; \
15 /* If not wrapped around */ \
16 if (n > start) { \
17 bit = find_next_bit bitmap, size, n); \
18 if (bit < size) \
19 return bit; \
20 n = 0; \
21 } \
22 bit = find_next_bit bitmap, start, n); \
23 return bit < start ? bit : size; \
24 } \
25 \
26 #define for Each_set_bitWrap(bit, addr, size, start) \
27 for ((bit) = find_next_bitWrap((addr), (size), (start)); \
28 (bit) < (size); \
29 (bit) = __for EachWrap((addr), (size), (start), \
30 (bit) + 1)); \
31 \
32 #define for Each_cpuWrap cpu, mask, start) \
33 for Each_set_bitWrap cpu, cpumask_bits mask, \
34 nr_cpmask_bits, start)

<caption>**Figure 8.** `for Each_cpuWrap` implementation from Linux kernel commit 4fe49b3b97c2, Sep. 19, 2022</caption>

# 4 Specifications

In this section we develop and prove the specifications for `select_idle_core` considering the different iterator implementations presented in Section 3.2.

## 4.1 Starting Point

As argued in Section 3.1, the implementation of `select_idle_core` is composed of a collection of heuristics. To explain the associated specifications, we start with a simple implementation of `select_idle_core` and introduce these heuristics incrementally.

**Base Implementation.** Our starting implementation is shown in Figure 9. This implementation does not include the global flag recording whether any idle cores are available (lines 6, 7, and 19 in Figure 2) and does not include the optimization of clearing offsets in the mask that are known not to represent idle cores (line 13 in Figure 2). Furthermore, no iterators are used; each loop is represented as a straightforward for loop over all of the possible CPUs, starting with CPU 0.

The first challenge is to construct the loop invariants. It is easy to see that both loop index variables range from 0 to `nr_cpu_ids` (lines 8 and 11 in Figure 10), that both loop index variables are modified (lines 8 and 11), as well as the local variable `idle` in the inner loop (line 14), and that a loop
```c
1 static int select_idle_core(struct task_struct *p,
2                          struct sched_domain *sd) {
3     struct cpumask *cpus =
4         this_cpu_cpmask_var_ptr(select_idle_mask);
5     int core, cpu;
6     cpmask_and(cpus, sched_domain_span(sd),
7                 tsk_cpus_allowed(p));
8     for (core = 0; core < nr_cpu_ids; core++) {
9         if (cpumask_bits(cpus)[core]) {
10         bool idle = true;
11         for (cpu = 0; cpu < nr_cpu_ids; cpu++) {
12             if (cpumask_bits(cpu_smt_mask(core))[cpu]) {
13                 if (!idle_cpu.cpu))
14                 idle = false;
15             }
16         }
17         if (idle) return core;
18     }
19 }
20 return -1;
21}
```

<caption>**Figure 9.** Simplified `select_idle_core` implementation using for loops (file step0.c in the artifact)</caption>

variant expression that approaches 0 to show termination is the difference between `nr_cpu_ids` and the loop index in each case. These observations thus lead directly to loop invariants. Each loop furthermore checks some property on each iteration and continues until the property is satisfied. The loop invariants thus need to express the relationship between the range of visited CPUs and this property of interest.

To identify the property, we consider the goal of the loops. Overall, the goal of the nested loops of `select_idle_core` is to iterate over all of the CPUs, via the outer loop, until reaching the first one that is part of an idle core (line 17), i.e., where all hyperthread siblings of the CPU are idle, which is detected via the inner loop (lines 11-16). The invariant of the outer loop thus states that all cores prior to the one indicated by the loop index core are not idle: `allmaskbits(i, cpus, i < core == > !idle_core(i))`. Unlike the outer loop, which aborts as soon as the desired condition is satisfied, the inner loop records its state in the variable `idle`. `idle` is initially true, but is set to false if a hyperthread is found not to be idle. This leads to two loop invariants, one if the value of `idle` is true and one if the value of `idle` is false. In the former case, expressed using `allmaskbits`, all previously considered CPUs have been found to be idle. In the latter case, expressed using `existsmaskbits`, some previously considered CPU has been found not to be idle.

The complete loop invariants are shown in Figure 10, on lines 28-33 for the outer loop and on lines 37-46 for the inner loop. Based on the loop invariants, we can determine the conditions that lead to each of the return statements, to identify the function behaviors. Either an idle core is found (line 53) or none is found (line 56). Accordingly, we define two Frama-C behaviors: found (line 7) and notfound (line 15). Like the invariants, these must refer to the set of CPUs

under consideration. The outer loop refers to the set of allowed cores using the mask cpus, but that is a local variable that is not visible to the function pre- and postconditions. Accordingly, we define another macro `domainok(i, sd, p)` to check whether a CPU *i* is compatible with the masks associated with both the arguments `sd` and `p`. With this, the found behavior (lines 7-13) states that if there exists a CPU that is compatible with the masks and is part of an idle core, then the result is part of an idle core and no lower-numbered CPU satisfies all of these properties. And the notfound behavior (lines 15-17) states that if all CPUs compatible with the masks are not part of an idle core, then the result is -1. For completeness we omit the preconditions of `select_idle_core`, which express various input data validity properties. The complete specifications are found in the artifact.

**Introducing Iterators.** To begin to introduce the use of iterators, we next replace the `for` loops and associated mask tests by uses of `forEach_cpu` (Figure 11). For example, the outer loop and subsequent test become simply `forEach_cpu(core, cpus)`. But this change is not entirely simple from a verification point of view, because of the “off by one” nature of the initial version of the iterators. Frama-C expects loop invariants to describe the state after the initialization and after the update of the loop, but the iterators only set the loop index to the new value in the test expression. Thus, after the initialization the loop index value is -1 and after the update the loop index value is the value from the previous iteration. On the other hand, by the time the loop body is reached, the loop index has the value appropriate for the current iteration. Invariants describing the current iteration thus refer to the index value from the previous iteration, while invariants describing previous iterations thus refer to the index values for those iterations. Concretely, the first invariant on the outer loop (line 17) changes from `0 <= core <= nr_cpu_ids` to `-1 <= core < nr_cpu_ids`, i.e., core no longer reaches the upper bound of the loop. The second invariant (line 18) changes from `allmaskbits(i, cpus, i < core == > !idle_core(i))` to `allmaskbits(i, cpus, i <= core == > !idle_core(i), i.e.,` reasoning about all of the CPUs prior to the one handled by the current iteration now includes the current value of `core`. A similar change is needed on the invariants of the inner loop. There is no change to the pre- and postconditions, which are thus omitted in Figure 11.

**Introducing the Wrapping Iterator.** The above implementations search though the CPUs consecutively from CPU 0 in each loop. In Section 3.1, we argued that to avoid conflict with task placements on other cores, it is better to start the outer loop at some chosen target CPU, rather than always at CPU 0. For this, `select_idle_core` uses the wrapping iterator `forEach_cpu-wrap` that counts up from target and then wraps around to CPU 0. The initial version of this iterator takes two extra arguments, the target and the
```c
1 #define domainok(i,sd,p) \
2 (cpumask_bits(sched_domain_span sd))[i] && \
3 cpumask_bits(tsk_cpu_allowed(p))[i])
4
5 /*@ \
6 ... // omitted input validity checks
7 behavior found:
8 assumes existsbits(i, domainok(i,sd,p) && idle_core(i));
9 ensures 0 <= \result < nr_cpu_ids;
10 ensures domainok(\result,sd,p);
11 ensures idle_core(\result);
12 ensures allbits(i, i < \result == > domainok(i,sd,p) == >
13                 !idle_core(i));
14
15 behavior notfound:
16 assumes allbits(i, domainok(i,sd,p) == > !idle_core(i));
17 ensures \result == -1;
18
19 complete behaviors;
20 disjoint behaviors;
21 */
22 static int select_idle_core(struct task_struct *p,
23                          struct sched_domain *sd) {
24     struct cpumask *cpus =
25         this_cpu CPUMASK_VAR_ptr(select_idle_mask);
26     int core, cpu;
27     cpumask_and(cpus, sched_domain_span sd, tsk_cpu_allowed(p));
28     /*@ 
29     loop invariant 0 <= core <= nr_cpu_ids;
30     loop invariant allmaskbits(i, cpus,
31                                 i < core == > !idle_core(i));
32     loop assigns core, cpu;
33     loop variant nr_cpu_ids - core; */
34 for (core = 0; core < nr_cpu_ids; core++) {
35     if (cpumask_bits(cpus)[core]) {
36         bool idle = true;
37         /*@ 
38         loop invariant 0 <= cpu <= nr_cpu_ids;
39         loop invariant idle == >
40             allmaskbits(i, cpu_smt_mask(core),
41                             i < cpu == > idle_cpu(i));
42         loop invariant !idle == >
43             existsmaskbits(i, cpu_smt_mask(core),
44                             i < cpu && !idle_cpu(i));
45     loop assigns cpu, idle;
46     loop variant nr_cpu_ids - cpu; */
47 for (cpu = 0; cpu < nr_cpu_ids; cpu++) {
48         if (cpumask_bits cpu_smt_mask(core))[cpu]) {
49             if (!idle_cpu.cpu)
50                 idle = false;
51         }
52     }
53     if (idle) return core;
54 }
55 }
56 return -1;
57 }
```

<caption>**Figure 10.** Simplified `select_idle_core` implementation using `for` loops, augmented with specifications (`step0.c` in the artifact)</caption>

flag wrap. `target` is a new argument to `select_idle_core`, while `wrap` is a new local variable that is only used to maintain the flag value across iterations. The inner loop continues to use `for Each cpu` and does not change in any way.

We must then adjust the loop invariants for the outer loop. As for the definition of `for Each cpu`, we have the property that the loop invariant is checked when the loop index still has the value of the previous iteration. We now have the further complexity that the loop index can be in two regions, initially from the target to the end of the list of CPUs and

```c
1 static int
2 select_idle_core(struct task_struct *p, struct sched_domain *sd) {
3     struct cpumask *cpus =
4         this_cpu CPUMASK_VAR_ptr(select_idle_mask);
5     int core, cpu;
6     cpumask_and(cpus, sched_domain_span sd, tsk_cpu_allowed(p));
7     /*@ 
8     loop invariant -1 <= core < nr_cpu_ids;
9     loop invariant allmaskbits(i, cpus,
10                                 i <= core == > !idle_core(i));
11     loop assigns core, cpu;
12     loop variant nr_cpu_ids - core;
13   */
14 for Each_cpu(core, cpus) {
15     bool idle = true;
16     /*@ 
17     loop invariant -1 <= cpu < nr_cpu_ids;
18     loop invariant idle == >
19         allmaskbits(i, cpu_smt_mask(core),
20                         i <= cpu == > idle_cpu(i));
21     loop invariant !idle == >
22         existsmaskbits(i, cpu_smt_mask(core),
23                         i <= cpu && !idle_cpu(i));
24     loop assigns cpu, idle;
25     loop variant nr_cpu_ids - cpu;
26   */
27 for Each_cpu.cpu, cpu_smt_mask(core) {
28     if (!idle_cpu.cpu)
29         idle = false;
30 }
31     if (idle)
32         return core;
33 }
34 return -1;
35 }
```

<caption>**Figure 11.** Simplified `select_idle_core` implementation using `for Each cpu` (file step1.c in the artifact)</caption>

then from 0 to just before the target. As before, there are three kinds of invariants: 1) the range of the loop index, 2) the properties of CPUs accumulated over the sequence of loop iterations, and 3) the loop variant expression justifying termination. Here, each of these is determined in one way if `wrap` is `false`, meaning that the loop index is in the region starting with the target, and another way if `wrap` is `true`, meaning that the region starting with the target has been completely considered and the loop index is now in the region prior to the target. The resulting loop invariants are shown in Figure 12 (lines 8-19).

We first consider the initial case, where the loop index is at or above the target, i.e., `wrap` is `false`. While the range of core was previously -1 <= core < nr_cpu_ids, its lower limit is now offset by target, resulting in target - 1 <= core < nr_cpu_ids (line 8 of Figure 12). While all of the CPUs from 0 up through core were previously known not to be on idle cores, now that is only the case of CPUs in the range target <= i <= core (line 10 of Figure 12). Finally, when the loop index is at or above the target, we must construct a variant expression that is larger than the variant expression used when the loop index is below the target. For this, we add in target to the difference between the number of CPUs and the current value of core (line 19 of Figure 12).
```c
1 static int select_idle_core(struct task_struct *p,
2                          struct sched_domain *sd, int target) {
3     struct cpumask *cpus =
4         this_cpu_cpmask_var_ptr(select_idle_mask);
5     int core, cpu, wrap;
6     cpumask_and(cpus, sched_domain_span sd, tsk_cpus_allowed(p));
7     /*@
8     loop invariant !wrap ==>> target - 1 <= core < nr_cpu_ids;
9     loop invariant wrap ==>> 0 <= core < target;
10    loop invariant !wrap ==>>
11         allmaskbits(i, cpus, target <= i <= core ==>> !idle_core(i));
12    loop invariant wrap ==>>
13         allmaskbits(i, cpus,
14                 target <= i < nr_cpu_ids ==>> !idle_core(i));
15    loop invariant wrap ==>>
16         allmaskbits(i, cpus, 0 <= i <= core ==>> !idle_core(i));
17    loop assigns core, cpu, wrap;
18    loop variant wrap ?
19         target - core : target + nr_cpu_ids - core;
20 */
21 for Each_cpuWrap(core, cpus, target, wrap) {
22     bool idle = true;
23     /*@
24     loop invariant -1 <= cpu < nr_cpu_ids;
25     loop invariant idle ==>>
26         allmaskbits(i, cpu_smt_mask(core),
27                 i <= cpu ==>> idle_cpu(i));
28     loop invariant !idle ==>>
29         existsmaskbits(i, cpu_smt_mask(core),
30                 i <= cpu && !idle_cpu(i));
31     loop assigns cpu, idle;
32     loop variant nr_cpu_ids - cpu;
33     */
34 for Each_cpu(cu, cpu_smt_mask(core))
35     if (!idle_cpu(cu))
36         idle = false;
37     if (idle)
38         return core;
39 }
40 return -1;
41 }
```

<caption>**Figure 12.** Simplified `select_idle_core` implementation using `for Each_cpuWrap` (file step2.c in the artifact)</caption>

Next, we consider the case where the loop index is below the target, i.e., wrap is true. Now the range of the loop index is $0 \le \text{core} < \text{target}$ (line 9 of Figure 12). The -1 case does not occur, having been replaced by the last value above the target. With respect to the accumulated information, when the loop index is below the target, we know that all of the CPUs compatible with the mask above and including the target are part of cores that are not idle, and we know the same of the CPUs below the loop index (lines 12-16 of Figure 12). Finally, the loop variant should be a value approaching 0, so we use `target - core` (line 19 of Figure 12).

The changes in the invariants of the outer loop imply similar changes on the postconditions. The resulting specifications are found in the artifact.

**Clearing Mask Entries For Visited CPUs.** The implementation presented so far is inefficient, in that for each CPU it performs remote-core accesses to all of the CPUs sharing the same core to determine whether the core is idle. Instead, once a CPU has been tested for idleness, it is never

necessary to test it again.<fnref n="3" /> Accordingly, the original definition of `select_idle_core` removes (line 13 in Figure 2) each CPU visited by the inner loop from the mask cpus iterated over by the outer loop, causing cpus to represent increasingly smaller subsets of the initial intersection of the `sched_domain_span sd` and `tsk_cpus_allowed(p)` masks. As the function's pre- and postcondition, on the other hand, are still expressed in terms of those latter masks, the loop invariants then have to describe how their relation with cpus is maintained.

Figure 13 shows the updated implementation and loop invariants. Only the new loop invariants are shown; the others are unchanged. The new invariants use the macro `domainok(i,sd,p)` to check whether a bit `i` is set in the intersection of the two original masks, and the expression `cpumask_bits(cpus)[i]` to check whether the same bit is set in the local copy cpus. `cpumask_clear_cpu` simply clears a bit of a mask, regardless of its previous value. Thus, if a bit is still set in cpus then `domainok(i,sd,p)` also still holds (lines 8 and 17). On the other hand, if `domainok(i,sd,p)` holds, then there is no guarantee that the bit is still set in cpus. At the point of the outer loop (invariant on line 10), either the bit is still set or the CPU has already been traversed by the inner loop and it has been determined that the CPU is not part of an idle core (if it was part of an idle core, the function would have exited, and that execution path is not covered by the loop invariant). As the right-hand sides of the implications in the behaviors are known to be true, there is no need to check again such values of `i`. For the inner loop (invariant on line 19), the invariant is similar, but the analysis of the current core is in progress, so we also take into account (third disjunct) that any CPU up to the current one that is on the same core as the current value of core has also been cleared.

While most of the loop invariants record properties of the CPUs seen so far, the loop invariants related to `cpumask_clear_cpu` consider all CPUs, because they record information from previous executions of the inner loop, which considers all CPUs. Finally, the use of `cpumask_clear_cpu` only affects the loops. The pre- and postconditions of `select_idle_core` are unchanged.

**Recording of the Availability of Idle Cores.** The complete definition of `select_idle_core` is optimized with a global flag that indicates when no idle cores are available on the scheduling domain of `target`; if this flag is true, the iteration over the CPUs can be skipped. The function thus starts by checking this flag (lines 30 and 31 in Figure 14) and concludes in the case where no idle cores are found by setting the flag to `false` (line 40 in Figure 14). This feature

<footnote n="3">³Concurrent actions on other CPUs could indeed change the result, but `select_idle_core` is implemented as though that possibility does not exist.</footnote>
```c
1 static int select_idle_core(struct task_struct *p,
2                          struct sched_domain *sd, int target) {
3     struct cpumask *cpus =
4         this_cpu_cpmask_var_ptr(select_idle_mask);
5     int core, cpu, wrap;
6     cpumask_and(cpus, sched_domain_span sd, tsk_cpus_allowed(p));
7     /*@ ... */
8     loop invariant allbits(i,
9         cpumask_bits(cpus)[i] ===> domainok(i,sd,p));
10    loop invariant allbits(i,
11        domainok(i,sd,p) ===> (
12        cpumask_bits(cpus)[i] || !idle_core(i));
13    ... */
14    forEach_cpu-wrap(core, cpus, target, wrap) {
15        bool idle = true;
16        /*@ ... */
17        loop invariant allbits(i,
18            cpumask_bits(cpus)[i] ===> domainok(i,sd,p));
19        loop invariant allbits(i,
20            domainok(i,sd,p) ===> (
21            cpumask_bits(cpus)[i] || !idle_core(i) ||
22            (i <= cpu && (cpumask_bits(cpu_smt_mask(core))[i])));
23        ... */
24        forEach_cpu.cpu, cpu_smt_mask(core)) {
25            cpumask_clear_cpu.cpu, cpus);
26            if (!idle_cpu.cpu)
27                idle = false;
28        }
29        if (idle)
30            return core;
31    }
32    return -1;
33}
```

<caption>Figure 13. Simplified `select_idle_core` implementation incorporating `cpumask_clear_cpu` (file step2a.c in the artifact)</caption>

also adds a new behavior (lines 2-5) and augments the existing ones (lines 8, 14, 17, and 20) to reflect the new tested condition. It has no impact on the loop invariants.

A reasonable postcondition could be that the `idle Cores` flag is only set to false when there are no idle cores in the current scheduling domain:

ensures !idle Cores[ target] <=> allbits(i, sched_domain_span sd), !idle core(i)

But this postcondition does not hold; failure of `select_idle_core` only implies that there are no CPUs on idle cores among the CPUs considered by the outer loop, i.e., the ones in the intersection of the `sched_domain_span` (`sd`) and `tsk_cpus_allowed(p)` masks. If `p` is only allowed to be placed on a few CPUs, many idle cores may be overlooked. This longstanding issue has been acknowledged by the Linux kernel scheduler maintainers.<fnref n="4" /> It remains to see whether it can have an impact in practice.

## 4.2 Iterator Evolution

Section 4.1 has developed the specifications for `select_idle_core` relying on the original definitions of `forEach_cpu-wrap` and `forEach_cpu`. We now consider the impact of the evolution of these iterators on the loop invariants.

```c
1 /*@ ... */
2 behavior none_available:
3     assumes idle Cores[ target] == 0;
4     ensures \result == -1;
5     ensures idle Cores[ target] == 0;
6
7 behavior found:
8     assumes idle Cores[ target] == 1;
9     assumes existsbits(i, domainok(i,sd,p) && idle Cores(i));
10    ensures idle Cores(\result);
11    ensures 0 <= \result < nr_cpu_ids;
12    ensures domainok(\result,sd,p);
13    ...
14    ensures idle Cores[ target] == 1;
15
16 behavior notfound:
17     assumes idle Cores[ target] == 1;
18     assumes allbits(i, domainok(i,sd,p) ===> !idle Cores(i));
19     ensures \result == -1;
20     ensures idle Cores[ target] == 0;
21
22 complete behaviors;
23 disjoint behaviors;
24 */
25 static int select_idle_core(struct task_struct *p,
26                          struct sched_domain *sd, int target) {
27     struct cpumask *cpus =
28         this_cpu_cpmask_var_ptr(select_idle_mask);
29     int core, cpu, wrap;
30     if (!test_idle Cores(target, false))
31         return -1;
32     cpumask_and(cpus, sched_domain_span sd, tsk_cpus_allowed(p));
33     /*@ ... */
34     forEach_cpu-wrap(core, cpus, target, wrap) {
35         bool idle = true;
36         /*@ ... */
37     forEach_cpu.cpu, cpu_smt_mask(core)) { ... }
38     if (idle) return core;
39 }
40     set_idle Cores(target, 0);
41     return -1;
42}
```

<caption>Figure 14. `select_idle_core` implementation with the idle-core optimization (file step3a.c in the artifact)</caption>

These changes have no impact on the `select_idle_core` pre- and postconditions.

**Using the for Loop Initialization and Update Fields.**
The initial definitions of `forEach_cpu-wrap` and `forEach_cpu` start the loop index at -1 or the loop index value of a previous iteration and update the loop index in the test expression, which complicates the loop invariants. First `forEach_cpu-wrap` and then `forEach_cpu` have been updated to use the initialization and update fields in a more traditional way, such that the loop index value at the top of the loop is the same as the loop index value that is used on the current iteration.

With the new definition of `forEach_cpu-wrap`, the range of the loop index becomes 0 <= core <= nr_cpu_ids and the wrap variable disappears from `select_idle_core` and thus from the loop invariants. The loop invariants that were previously conditional on the value of `wrap` are now conditional on whether the loop index, core, is above or below the target. As the loop index can now reach the end of the range, `nr_cpu_ids`, signifying that no idle core is available,

<footnote n="4">⁴(https://lore.kernel.org/lkml/alpine.DEB.2.22.394.2506152216150.3463@hadrien/)</footnote>
it is necessary to declare that the loop index is a relevant CPU (i.e., satisfying domainok) except when it has the value nr_cpu_ids. The possibility that core is nr_cpu_ids also has to be taken into account in the loop variant, where the result is 0. Finally, invariants describing the accumulated properties of previously visited CPUs now range up to a value < core rather than <= core, reflecting the fact that core now represents the CPU to be considered on the current iteration, rather than the previous one. The changes in the invariants needed after the update to forEach_cpu are similar, but without the complexity of wrapping. After both steps it was necessary to introduce some asserts to help the solvers prove that the invariants still hold. These have no impact on the validity of the proof, but may make some information more easily accessible to the solvers.

The iterator `forEach_cpu` has a third variant, with the redefinition of `forEach_set_bit`, as shown in Figure 5. This definition again takes the strategy of moving (part of) the update of the loop index variable into the test expression. Here, however, the index variable remains within the range of valid CPUs plus `nrCPUMASK_bits`, representing the error value, but it is no longer always in the mask at the top of the loop. The value of the loop index at the top of a given iteration is just one greater than it was in the previous iteration, and it is only on entering the loop body that the index variable is in the mask.

The complete specifications are found in the artifact.

### Replacing the *wrap* Flag by *Specialized Function Calls*.

A second change to `forEach_cpuWrap` replaces the call to a single function, with different flags indicating initialization and update, by a call to a distinct function for each case. This change has no impact on the value of the index variable and thus is not visible to developers. However, it introduced an unexpected complexity in the proof effort. As the two functions are both optimized for their usage context, initialization vs. update, they are structured in different ways, and thus the natural decomposition into behaviors based on the function's `if` tests produces pre- and postconditions that decompose the search space in different ways. The annotations on loops, specifically the loop variant, require a uniform specification. After many mysterious proof failures, we added postconditions to the function used in the update to make clear how the loop index can evolve, thus enabling Frama-C to prove that the value of the loop variant expression decreases on each iteration. No changes to the loop invariants were needed, but one more assert also had to be added. The complete specifications are found in the artifact, with the updated postconditions found in the file `loops.c`.

## 5 Discussion

The proof effort reported in this paper was carried out over a period of roughly one month. A previous effort based on

the original definitions of `forEach_cpu` and `forEach_cpuWrap` (Section 4.1), by the first and third authors individually, got stuck at the point of introducing the call to `cpumask_clear_cpu`. This code introduces a second side effect on masks within nested loops, which greatly increases the proving time, and complicates the loop invariants. The effort leading to this paper succeeded by rewriting the code using increasingly complex forms of loops, following the presentation in Section 4.1. This incremental approach made it possible to get the basic preconditions, postconditions, and loop invariants in place before adjusting them to account for the unusual structure of the for loops in the initial definitions of `forEach_cpu` and `forEach_cpuWrap`.

A goal of our work is to study the impact of changes in the definitions of the iterators on the proof effort. The first change to `forEach_cpu` and `forEach_cpuWrap`, by moving the initialization of the loop index from the for loop test expression to the for loop initialization and update, causes the value of the loop index seen in the loop invariant to correspond to the value of the loop index seen in the loop body. This change simplified the development of correct specifications. There is also evidence that the original implementations, starting the search at a position prior to the smallest value that can be selected, could be confusing for developers. The function `cpumask_next` contains the surprising comment `/* -1 is a legal arg here. */`, at the point of checking the validity of the search starting point. Outside of the scheduler, the following refactoring change was made at two places in the file `arch/ia64/kernel/mca.c`, providing support for the Itanium architecture, in commit `5dd3c9949a3e` in March 2009:

1. `for (++cpuid; cpuid < NR_CPUS && !cpu_online(cpuid);`
2. `cpuid++);`
3. `cpuid = cpumask_next(cpuid+1, cpu_online_mask);`

While the original search started at the CPU just after `cpuid`, the updated search skips that CPU and starts at the one after that. The code remained unchanged until October 2022 (commit cf8e8658100d) removing support for the Itanium architecture, which was then obsolete. The Linux kernel still contains calls to `cpumask_next`. While none of them adds 1 to the CPU argument, careful auditing of each use would be required to determine whether it is expected that the smallest possible result is one past the provided CPU.

The second change to `forEach_cpuWrap` replaced a single function with a flag by separate specialized functions, each with a different structure. This complicated the proof effort, but had no discernible effect on the code using the iterator. We noted, however, in Section 3.2, that the implementations of the two functions are quite dissimilar, which may hinder understanding of the iterator and even lead to bugs in the future.

We conclude with some performance measurements, in Table 1. Our test machine is an Intel Xeon Gold 5320 with two sockets, each of which contains 26 cores, each containing 2
<table><caption>**Table 1.** Performance summary</caption><thead><tr><th></th><th>Total time</th><th>Longest VC</th></tr></thead><tbody><tr><td colspan="3">Original Definitions (simplified implementations), Section 4.1</td></tr><tr><td>for loop (Figure 10)</td><td>28s</td><td>676ms</td></tr><tr><td>for each_cpu only (Figure 11)</td><td>33s</td><td>1.7s</td></tr><tr><td>both iterators (Figure 12)</td><td>46s</td><td>6s</td></tr><tr><td>adding cpumask_clear_cpu (Figure 13)</td><td>5m25s</td><td>1m52s</td></tr><tr><td>adding global idle-core flag (Figure 14)</td><td>5m52s</td><td>2m3s</td></tr><tr><td colspan="3">Later Definitions (full implementations), Section 4.2</td></tr><tr><td>1st change to for each_cpuWrap (Figure 7)</td><td>4m43s</td><td>2m22s</td></tr><tr><td>1st Change to for each_cpu (Figure 4)</td><td>13m23s</td><td>7m45s</td></tr><tr><td>2nd change to for each_cpuWrap (Figure 8)</td><td>5m36s</td><td>1m32s</td></tr><tr><td>2nd Change to for each_cpu (Figure 5)</td><td>15m56s</td><td>13m40</td></tr><tr><td></td><td>15m56s</td><td></td></tr></tbody></table>

CPUs. The machine has 384 GiB memory. Each experiment is run once. We use Frama-C 29.0, with solvers Alt-Ergo 2.5.4 [5], CVC4 v1.8 [3], and CVC5 v1.1.2 [2], and with the default parallelism settings. The table contains information about the elapsed runtime, obtained using the Linux utility `/bin/time`, and the largest proof time of a single individual verification condition (VC), as reported by Frama-C. The top half of the table reports on the steps in the development of the original implementation of `select_idle_core`, as presented in Section 4.1. The times increase as the code becomes more complicated. There is a big increase when the call to `cpumask_clear_cpu` is added, triggering the modification of a data structure within a loop. A similar performance jump was observed in the case of an analysis of the Linux kernel load-balancer function `should_we_balance` [16]. The bottom half of the table considers the successive definitions of the iterators, as presented in Section 4.2. Here asserts have to be added to the `select_idle_core` code. These asserts make relevant information apparent to the underlying solvers and somewhat reduce the execution times. Nevertheless, as the asserts represent a further burden for the specification developer, we will try to see whether it is possible remove the need for these asserts in future work.

## 6 Related Work

There have been various efforts on developing a fully proved operating system, including SeL4 [15], using Isabelle [20], and CertiKOS [12], using Coq [4]. Ipanema proposes a domain-specific language for reimplementing task schedulers of Linux and FreeBSD and proving their correctness [17]. These projects have emphasized how to design operating-system code to facilitate its proof, while we are targeting proving the correctness of existing operating-system code.

Starting with Engler et al.'s Metal [11], numerous tools [1, 13, 18, 19, 21–23] have proposed to scan the code of existing operating systems, such as Linux, to find bugs. Many bugs have been found, typically related to incorrect sequences of operations, such as use after free, missing unlocks, etc. These works do not construct, exhibit, or verify a comprehensive specification of the studied code.

Lawall et al. have studied the problem of proving the correctness of the Linux kernel load balancer function `should-we_balance` as it has varied over time, assessing the amount of proof work required to maintain the specifications as the code changes [16]. The current paper represents another such case study. Here, we leave the client function fixed and explore the impact of different iterator implementations on the specifications and proofs.

## 7 Conclusion

This paper has studied the verification of the function `select_idle_core` that was an important part of the Linux kernel scheduler's task placement approach in 2016. We have used this function as a vehicle to study the impact of the evolution of the generic CPU mask iterators `for-each_cpu` and `for-each_cpu-wrap` on the verification of functions that use the iterators. Since 2016, there has been substantial reorganization of the task placement code, while still keeping essentially the same underlying algorithm. It could be interesting to verify the complete implementation in its more complex up to date version. Nevertheless, the results of the verification process have led to some observations that are still relevant today.

The proof effort as a whole, while done more rapidly than reported for a previous similar experiment [16], remains challenging, particularly as changes in the code lead to individual verification conditions that require multiple minutes to solve. In the future, we will investigate whether specification encoding strategies adapted to Linux kernel code can simplify the construction and verification of specifications. This is particularly essential due to the rate of change of Linux kernel code; the proof of any snapshot is typically quickly out of date, making specification maintenance an important problem.

## Acknowledgements

We thank the anonymous reviewers for their feedback on the paper and the Frama-C community for their advice throughout this project. This work was supported in part by the ANR EMASS grant. Experiments presented in this paper were carried out using the Grid'5000 testbed, supported by a scientific interest group hosted by Inria and including CNRS, RENATER and several Universities as well as other organizations (see https://www.grid5000.fr).
## A Overview of the artifact

The source code and specifications discussed in this paper are available at DOI 10.5281/zenodo.16842821. The code consists of five directories, corresponding to the different versions of the iterator implementations over time. The hash code at the end of the directory name is the corresponding Linux kernel commit id:

* `select_idle_core_v0_10e2f1acd010`

* `select_idle_core_v1_c743f0a5c50f`

* `select_idle_core_v2_33e67710beda`

* `select_idle_core_v3_4fe49b3b97c2`

* `select_idle_core_v4_fdae96a3fc7f`

Each directory contains the following files:

* `Makefile`

* `globals.c`, `loops.c`: Auxiliary definitions needed by `select_idle_core`.

* `step0.c`, `step1.c`, `step2.c`, `step3.c`: Variants of `select_idle_core` corresponding to Figures 9-14, without using `cpumask_clear_cpu` in the inner loop.

* `step0a.c`, `step1a.c`, `step2a.c`, `step3a.c`: Variants of `select_idle_core` corresponding to Figures 9-14, using `cpumask_clear_cpu` in the inner loop.

In each directory, the experiments can be run using `make all` and can be run with Frama-C smoke tests, checking for trivial proofs from false, using `make alls`.

## References

[1] Jia-Ju Bai, Yu-Ping Wang, Julia Lawall, and Shi-Min Hu. 2018. DSAC: Effective static analysis of sleep-in-atomic-context bugs in kernel modules. In USENIX ATC, Haryadi S. Gunawi and Benjamin C. Reed (Eds.). USENIX Association, 587–600.

[2] Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. 2022. cvc5: A versatile and industrial-strength SMT solver. In TACAS (LNCS, Vol. 13243). Springer, 415–442. doi:10.1007/978-3-030-99524-9_24

[3] Clark W. Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, and Cesare Tinelli. 2011. CVC4. In CAV (LNCS, Vol. 6806). Springer, 171–177. doi:10.1007/978-3-642-22110-1_14

[4] Yves Bertot and Pierre Castéran. 2004. Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions. Springer. doi:10.1007/978-3-662-07964-5

[5] Sylvain Conchon, Albin Coquereau, Mohamed Iguernlala, and Alain Mebsout. 2018. Alt-Ergo 2.2. In SMT Workshop: International Workshop on Satisfiability Modulo Theories. Oxford, United Kingdom. https://inria.hal.science/hal-01960203

[6] Jonathan Corbet. 2024. Another push for sched_ext. Linux Weekly News (9 May 2024). https://lwn.net/Articles/972710/

[7] Jonathan Corbet. 2025. Reports from OSPM 2025, day one: Scheduler governors, Steven Rostedt. Linux Weekly News (19 May 2025). https://lwn.net/Articles/1020596/

[8] Jonathan Corbet. 2025. Reports from OSPM 2025, day two: Sched_ext: Current status, future plans, and what's missing, Andrea Righi and

Joel Fernandes. Linux Weekly News (23 May 2025). https://lwn.net/Articles/1021332/

[9] Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. 2012. Frama-C - A software analysis perspective. In Software Engineering and Formal Methods (SEFM) (LNCS, Vol. 7504). Springer, 233–247. doi:10.1007/978-3-642-33826-7_16

[10] Olivier Danvy. 2022. Fold-unfold lemmas for reasoning about recursive programs using the Coq proof assistant. Journal of Functional Programming 32 (2022), e13. doi:10.1017/S0956796822000107

[11] Dawson R. Engler, Benjamin Chelf, Andy Chou, and Seth Hallem. 2000. Checking system rules using system-specific, programmer-written compiler extensions. In OSDI, Michael B. Jones and M. Frans Kaashoek (Eds.). USENIX Association, 1–16.

[12] Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. 2016. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In OSDI. 653–669.

[13] Haryadi S. Gunawi, Cindy Rubio-González, Andrea C. Arpaci-Dusseau, Remzi H. Arpaci-Dusseau, and Ben Liblit. 2008. EIO: Error handling is occasionally correct. In FAST, Mary Baker and Erik Riedel (Eds.). USENIX, 207–222.

[14] Jack Tigar Humphries, Neel Natu, Ashwin Chaugule, Ofir Weisse, Barret Rhoden, Josh Don, Luigi Rizzo, Oleg Rombakh, Paul Turner, and Christos Kozyrakis. 2021. ghOSt: Fast & flexible user-space delegation of Linux scheduling. In SOSP, Robbert van Renesse and Nickolai Zeldovich (Eds.). ACM, 588–604. doi:10.1145/3477132.3483542

[15] Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David A. Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. 2009. seL4: formal verification of an OS kernel. In SOSP. 207–220. doi:10.1145/1629575.1629596

[16] Julia Lawall, Keisuke Nishimura, and Jean-Pierre Lozi. 2024. Should we balance? Towards formal verification of the Linux kernel scheduler. In Static Analysis - 31st International Symposium, SAS 2024 (Lecture Notes in Computer Science, Vol. 14995), Roberto Giacobazzi and Alessandra Gorla (Eds.). Springer, 194–215. doi:10.1007/978-3-031-74776-2_8

[17] Baptiste Lepers, Redha Gouicem, Damien Carver, Jean-Pierre Lozi, Nicolas Palix, Maria-Virginia Aponte, Willy Zwaenepoel, Julien Sopena, Julia Lawall, and Gilles Muller. 2020. Provable multicore schedulers with Ipanema: application to work conservation. In EuroSys. 3:1–3:16. doi:10.1145/3342195.3387544

[18] Shan Lu, Soyeon Park, Chongfeng Hu, Xiao Ma, Weihang Jiang, Zhenmin Li, Raluca A. Popa, and Yuanyuan Zhou. 2007. MUVI: automatically inferring multi-variable access correlations and detecting related semantic and concurrency bugs. In SOSP, Thomas C. Bressoud and M. Frans Kaashoek (Eds.). ACM, 103–116. doi:10.1145/1294261.1294272

[19] Nicolas Palix, Gaël Thomas, Suman Saha, Christophe Calvès, Gilles Muller, and Julia Lawall. 2014. Faults in Linux 2.6. ACM Trans. Comput. Syst. 32, 2 (2014), 4:1–4:40. doi:10.1145/2619090

[20] Lawrence C Paulson. 1994. Isabelle: A generic theorem prover. Vol. 828. Springer.

[21] Suman Saha, Jean-Pierre Lozi, Gaël Thomas, Julia L. Lawall, and Gilles Muller. 2013. Hector: Detecting resource-release omission faults in error-handling code for systems software. In DSN. IEEE Computer Society, 1–12. doi:10.1109/DSN.2013.6575307

[22] Keita Suzuki, Kenta Ishiguro, and Kenji Kono. 2024. Balancing analysis time and bug detection: Daily development-friendly bug detection in Linux. In USENIX ATC, Saurabh Bagchi and Yiying Zhang (Eds.). USENIX Association, 493–508.

[23] Wenwen Wang. 2021. MLEE: Effective detection of memory leaks on early-exit paths in OS kernels. In USENIX ATC. USENIX Association, 31–45.