[CuriousSkeptic]

Probably not at all related to the OP. But I found the thought entertaining, so offering it as such.

One way to address you concern would be to guarantee that task always terminate in a bounded amount of instructions.

One way to solve that would be offer a limited buffer in which the program instructions for the task might be expressed, and a language to express them in that is strongly normalizing (think something like Morte)

[elihu]

The Linux kernel makes a somewhat similar distinction between code that's executing in an atomic context and code that isn't. Atomic code can get stuck in an infinite loop or whatever, but what it isn't allowed to do is to go to sleep (i.e. put itself into a sleeping state and invoke the scheduler).

Atomic tasks are generally expected to do a finite amount of work that can be finished in a short time without waiting for anything else (except maybe a spinlock, which should be held by some other similarly-atomic task that will finish in a short time).

[yencabulator]

The seL4 microkernel, written in C, has formal proofs of the maximum clock cycles for all of its syscalls. That's one way they manage to not need in-kernel preemption.