Re: termination, can't you use Ethereum gas style termination? I always found termination verification strange, because "gas" is usually more practical alternative.
The ZFS file system supports running Lua programs in Kernel mode. It supports setting a limit on the number of instructions run and the amount of memory used:
So it’s been done before. I think traditional BPF programs were really short and ran in performance critical contexts. Disallowing backwards branches and limiting size was preferred to slowing down these code paths with instruction counting.
