Frightening small children and disconcerting grown-ups: Concurrency in the Linux kernel— Companion Material

Submission with appendix

We provide a complete version of our article with appendices.

Tests and models

Our complete test base consists of 8238 tests. The test base has been constructed both by accumulating significant tests and by systematic generation from cycles of non-SC executions. Tests are in two languages:

• The LISA pseudo-assembly language allows rapid model prototyping without bothering with syntactical details and facilitates systematic test generations. Example test.
• Tests in C are easier to extract from actual kernel code and are also easier for programmers to understand and discuss. Example test.

Using the following files, and the memory model simulator herd7, run a test by:

% herd7 -macros kernel.def -bell kernel.bell -model kernel.cat [filename]+

• Macro file kernel.def.
• Bell file  kernel.bell.
• Model: kernel.cat (and the experimental lock.cat, which handles spin-locks).

Once the files above have been copied to the local directory, your can also use the configuration file kernel.cfg:

% herd7 -conf kernel.cfg [filename]+

We run our tests on machine using a dedicated python script and the klitmus tool. We have run a subset of 2576 tests of the complete test base. Limitations are as follows:

• We run tests that span over six threads or less. Some of our machines (ARMv8, ARMv7) have four cores, we do not run tests that span over five threads or more on those.
• We do not run tests that might deadlock.
• Our simulator is less strict than C compilers as regards the typing requirements of some RCU constructs such as rcu_assign_pointer.

Tested systems are “Power8”, a CHRP IBM pSeries machine with 8 POWER8E CPUs at 3.4GHz (Linux v4.4.40), “ARMv8”, a Amlogic ARMv8 board with 4 Cortex-A53 cores at 1.5GHz (Linux v3.14.29), “ARMv7”, a Raspberry Pi ARMv7 board with 4 Cortex-A7 cores at 900Mhz (Linux v4.9.20), and “X86”, a HP desktop computer with 2 (6-core) Intel Xeon E5-2620 v3 CPUs at 2.40GHz (Linux v3.16.04).

Examples from the paper

We here provide an actualized version of the result table of the paper

Detailed hardware results

Our main experimental result is here: our model is experimentally sound as demonstrated by the empty table “Forbidden by model and observed” below.

• Comparison with hardware
  • Forbidden by model and observed
  • Allowed by model and unobserved
• Specific behaviours
  • ARMv7
  • ARMv8
  • Power8
  • X86

Comparison with the C11 model

In this section we compare the Linux model with the C11 model. The C11 CAT model is the default C11 model of herd7. This model is the second C11 model (partial order SC model) from “Overhauling SC atomics in C11 and OpenCL” (POPL’2016) by Mark Batty, Alastair F. Donaldson, and John Wickerson. The herd7 implementation of this model is adapted from the authors own CAT files.

Our main experimental result demonstrates that C11 SC fence atomic_thread_fence(memory_order_seq_cst) does not suffice to rule out all non-sequentially consistent executions — see the table here. By contrast and given our Linux model, smp_mb() suffices to guarantee sequential consistency. One should notice that all modern architectures provide such a strong fence that Linux implementations would map smp_mb() onto.

• Fences
  • Equivalence of constructs
  • C11 shows more behaviours
  • C11 shows less behaviours
• Fences, write release and read acquire
  • C11 shows more behaviours
  • C11 shows less behaviours

New this round

Comparison with old model

More behaviours

Less behaviours

This document was translated from L^AT_EX by H^EV^EA.