>But for as long as the kernel defines a cpumask_first() function, I will always worry that some other Linux feature might employ it to force unrelated, latency-spiking workloads upon that core.
Very Linux. It's complex, very complex, and full of footguns like this.
The real answer is to use seL4[0]. Among its extensive formal proofs, it has proof of WCET (Worst Case Execution Time), therefore unlike Linux and other hopelessly non-deterministic unorthogonal toy OSs, seL4 can actually guarantee latency bounds.
Very Linux. It's complex, very complex, and full of footguns like this.
The real answer is to use seL4[0]. Among its extensive formal proofs, it has proof of WCET (Worst Case Execution Time), therefore unlike Linux and other hopelessly non-deterministic unorthogonal toy OSs, seL4 can actually guarantee latency bounds.
0. https://sel4.systems/About/seL4-whitepaper.pdf