Extending the Linux Kernel with Built-In Kernel Headers

Yes but JAR files are basically equivalent to source code parsed and serialised as bytecode with only the most rudimentary optimisations applied. I don't really see a difference between that and carrying gzipped headers with the kernel. Yes, the .class format is cleaner, but it's still very close to what the programmer wrote. Another plus to carrying the header with the kernel is that you can carry the preprocessed header to make sure the user doesn't set the wrong defines, and you can add compiler checks to check that the user isn't using a too old or too new compiler with incompatible ABI.

From what I know about it, gobject-introspection has some nice properties, but one killer drawback: it's incompatible with cross compilation. This is apparently because it requires running binaries compiled for the target system as part of the build process. You actually can cross compile if you have an emulator for that system handy [1], but that's horrible.

Apparently the reason it requires running the compiled binaries is that GObject types are only registered at runtime, within so-called "_get_type" functions. For more typical systems, everything needed can be determined at compile time. Too bad there's no portable way to ask a C compiler to dump what it knows about a source file, but if you just want things like struct sizes and field offsets, you can compile a C file that embeds them as global variables, and then extract the variable values. For more advanced introspection there are many less-portable options including Clang's API, GCC-XML, parsing debug info, or writing your own compiler (easier for C; it seems that parts of gobject-introspection work like this).

Anyway, another interesting comparison is DTrace's CTF (Compact Type Format) [2], a simple binary format that describes the kernel's C struct layouts, function signatures, etc. This information is simply converted from compiler-generated debug info [3], but it's stripped down enough that it can be embedded into every kernel without too much size overhead. When the DTrace compiler is invoked to compile a user hook, it parses the CTF data and exposes the types and functions to the user's code (which is written in a custom C-like language).

Ironically, BPF has BTF, which is a very similar-looking format that encodes very similar kinds of data – but is used for a completely different purpose. Specifically, it's only used to encode types and functions defined by BPF programs, to allow the kernel to pretty-print things. But in theory BTF could be repurposed to work like CTF: you would need to generate BTF information for the kernel itself, and then Clang could be extended to support "including" BTF files in place of C headers. However, this option was apparently discussed and rejected [4]. I haven't read the original threads to find out why, but I suspect it might involve:

- Lack of existing tooling to do the above;

- Lower expressivity compared to C headers, e.g. the inability to encode macros (although this could be fixed);

- Desire to use the information for building not just BPF hooks but also full-fledged kernel modules.

[1] https://maxice8.github.io/8-cross-the-gir/

[2] https://github.com/oracle/libdtrace-ctf/blob/master/include/...

[3] https://www.freebsd.org/cgi/man.cgi?query=ctfconvert&sektion...

[4] https://lwn.net/Articles/783832/

There is a very long thread on LKML discussing this. But I'm pretty sure the primary reason is that procfs has been slowly accumulating more and more random knobs, while sysfs actually has a structure that can be used reasonably by userspace.

BPF is compiled in user-space and the bytecode is provided to the kernel -- the compiler definitely isn't shipped as part of the kernel.

Forbidding loops in a language does make all code written in that language provably terminating. But there’s not much else it lets you prove for all code, at least not if you want to get results before the heat death of the universe. For example, you can’t determine what inputs to a program will yield a given output: even classic BPF is probably expressive enough to implement a cryptographic hash, and eBPF definitely is. You can’t enumerate all possible paths through the program: the number of paths is exponential in the size of the program.

On the other hand, forbidding loops does make some properties easier to prove for restricted classes of programs. For instance, Linux’s BPF verifier tracks, for each instruction, the minimum and maximum value of each register at that point in the program. It uses that to determine whether array accesses in the program are bounds checked, and complain if not: that way, it doesn’t have to insert its own bounds check, which might be redundant. Doing the same in the presence of loops would require a more expensive algorithm, so forbidding them is a benefit. Yet... Linux’s verifier is sound: it will forbid all programs that could possibly index out of bounds, at least barring bugs. But it is not fully precise: it does not pass all programs that have the property of never indexing out of bounds for any input. For example, you could have a program that takes a 256-bit input and indexes out of bounds only if its SHA-256 hash is a specific value. That program is safe iff there happen to be no 256-bit strings that hash to that value, something that you could theoretically verify – but only by going through all 2^256 possible strings and hashing each of them. Linux does not.

Nor would it be reasonable to, why does that hypothetical matter? Because the ability to prove arbitrary properties about all programs, at the cost of arbitrarily long analysis time, is sort of the main mathematical benefit to non-Turing-completeness. But from a practical standpoint that’s useless. And if you don’t need that – if you only care about the ability to prove things about restricted classes of programs – well, you can achieve that even with loops. After all, that’s what a type system does, and there are plenty of Turing-complete languages with type systems. As I said, disallowing loops makes the job easier in some cases. But that’s more of a matter of degree, not the kind of hard theoretical barrier that “non-Turing-complete = analyzable” makes it sound like. That makes it a less convincing rationale for disallowing them.