Safe kernel extension is an extremely successful feature in OS kernels with a plethora of interesting applications. It provides significant performance benefits by avoiding context switching and data copying, without compromising the kernel's integrity due to its verifiable safety. The most mature existing approach, namely BPF, verifies extension safety using sound abstract interpretation techniques with best effort precision. Such design not only increases the kernel maintenance burden due to its complexity, but also restricts extension expressiveness due to its approximations. The core of the problem, we argue, is the BPF verifier's dual mandate of precision and soundness in its safety analysis.

Cooperative scheduling avoids the many shared-state pitfalls of preemption, but risks fairness---in the limit resulting in denial of service and resource exhaustion. This paper argues that a careful hybrid between cooperation and preemption is both feasible and advantageous: by allowing only carefully controlled and developer-configurable preemption in an otherwise cooperative environment, the scheduler can maintain key invariants while restoring fairness. The paper presents a series of case-study workloads that motivate the need for preemption in real-world cooperative environments, sketches a hybrid design that introduces controlled preemption while maintaining cooperation benefits, and discusses the benefits by applying this hybrid design on the case-study workloads. A hybrid scheduling implementation, Cx, is in progress.