4 ms·

I've been wondering recently to what extent formal verification could be used to simplify CPU hardware and ISAs. For example, MMUs are unnecessary if the OS ver

I've been wondering recently to what extent formal verification could be used to simplify CPU hardware and ISAs. For example, MMUs are unnecessary if the OS verifies that all programs only access memory that's been allocated to it. This paper[0] seems to imply that the savings would be non-negligible. Also interrupts and context switching could be avoided if programs are cooperatively scheduled and verified that they always yield after an appropriate amount of time. Those two examples are the only ones I could come up with, but I suspect that's because I don't know very much about hardware design. Are people working on this or am I just off-base here? [0]: https://arxiv.org/abs/2009.06789 https://arxiv.org/abs/2009.06789

zozbot234 5y ago
> For example, MMUs are unnecessary if the OS verifies that all programs only access memory that's been allocated to it. You'd need some sort of proof-carrying code to allow verification of these properties in binaries. Also, features like MMU's and interrupts are needed anyway to implement virtual memory, or user tasks with adjustable priorities.
- fuklief 5y ago
  Would virtual memory still be necessary on a capability machine architecture [0] ? My understanding is that would not be the case since all programs can only access memory that's been allocated to it. By definition, capabilities cannot be created out of thin air like pointers can be ? [0]: https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/ https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/
  - warkdarrior 5y ago
    You probably still want to use virtual memory to simplify the programming model (flat address space) and to be able to overallocate memory across many processes. Without virtual memory you are pushing these functionalities to app developers.
gmueckl 5y ago
Cooperative scheduling would require provable upper limits on the number of instructions run by process between calls to a yield function. When the process is a compute task with an input of variable size, this would result in the need to count iterations and branch in inner loops that you want to be fast. I am not sold on the idea that such an overhead is lower in that case than interrupt driven preemptive scheduling. Also, task prioritization can be a problem: the rate at which an interrupt-less cooperatively scheduled system must reschedule depends on the response time for the task with the shortest maximum response time. You must guarantee that the scheduler can switch to it in time to meet its deadline. This can increase the scheduling frequency for everything, requiring all components of the system to call the scheduler more often. So you'd have pretty tight coupling between everything.
- awelkie 5y ago
  Both great points. Regarding your second paragraph, note that this isn't so bad for multi-core processors. For randomly scheduled processes, the (expected) maximum response time is the maximum time between yield points divided by the number of cores. And the OS could maybe do something smarter by making sure that at least one core has a time-to-yield which is very small. This would mean that you can still have very large time-between-yields for some processes without affecting the maximum response time. And my hope was that simplifying the hardware would allow us to fit more cores on the same chip. So your first point means that the per-core performance is worse but maybe for some workloads the processor performance as a whole is better. But yeah not sure if that's realistic.
- jhgb 5y ago
  > Cooperative scheduling would require provable upper limits on the number of instructions run by process between calls to a yield function. When the process is a compute task with an input of variable size, this would result in the need to count iterations and branch in inner loops that you want to be fast. I am not sold on the idea that such an overhead is lower in that case than interrupt driven preemptive scheduling. Surely something like branch-on-random could be made to work with such code. It's effectively an interrupt point with the added benefit that you can place it exactly where you want it to.
- 5y ago
tachyonbeam 5y ago
Memory protection isn't just used to protect processes against one another, you can also use it to implement write barriers for a garbage collector, or to map files to memory, for example. I think you'd be hard pressed, with any kind of compiler, to prove that an object you're writing to isn't part of an old GC generation, seems like an intractable problem, unless you're in a pure functional programming language.
- ingenieroariel 5y ago
  sel4 has a Haskell version that they write before the C (granted, not sure how a ghc generated binary would be verified) but would the problem be tractable in that case?
zamalek 5y ago
> For example, MMUs are unnecessary if the OS verifies that all programs only access memory that's been allocated to it. That's what Microsoft was attempting with Singularity. Because binaries were IL, they could be reasonably verified for isolation guarantees during JIT compilation.
nynx 5y ago
I tried this with nebulet (https://github.com/nebulet/nebulet https://github.com/nebulet/nebulet). Unfortunately the MMU cannot be turned off on modern x86_64 processors.
opnitro 5y ago
Check out theseus! It's exploring some of these ideas. https://github.com/theseus-os/Theseus https://github.com/theseus-os/Theseus
mcguire 5y ago
I can't recall any names at the moment, but you might check out some of the Unikernel research. I seem to recall results of combining a unikernel and a safe language to be exactly what you describe.

zozbot234 5y ago

> For example, MMUs are unnecessary if the OS verifies that all programs only access memory that's been allocated to it. You'd need some sort of proof-carrying code to allow verification of these properties in binaries. Also, features like MMU's and interrupts are needed anyway to implement virtual memory, or user tasks with adjustable priorities.

fuklief 5y ago
Would virtual memory still be necessary on a capability machine architecture [0] ? My understanding is that would not be the case since all programs can only access memory that's been allocated to it. By definition, capabilities cannot be created out of thin air like pointers can be ? [0]: https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/ https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/
- warkdarrior 5y ago
  You probably still want to use virtual memory to simplify the programming model (flat address space) and to be able to overallocate memory across many processes. Without virtual memory you are pushing these functionalities to app developers.

gmueckl 5y ago

Cooperative scheduling would require provable upper limits on the number of instructions run by process between calls to a yield function. When the process is a compute task with an input of variable size, this would result in the need to count iterations and branch in inner loops that you want to be fast. I am not sold on the idea that such an overhead is lower in that case than interrupt driven preemptive scheduling. Also, task prioritization can be a problem: the rate at which an interrupt-less cooperatively scheduled system must reschedule depends on the response time for the task with the shortest maximum response time. You must guarantee that the scheduler can switch to it in time to meet its deadline. This can increase the scheduling frequency for everything, requiring all components of the system to call the scheduler more often. So you'd have pretty tight coupling between everything.

awelkie 5y ago
Both great points. Regarding your second paragraph, note that this isn't so bad for multi-core processors. For randomly scheduled processes, the (expected) maximum response time is the maximum time between yield points divided by the number of cores. And the OS could maybe do something smarter by making sure that at least one core has a time-to-yield which is very small. This would mean that you can still have very large time-between-yields for some processes without affecting the maximum response time. And my hope was that simplifying the hardware would allow us to fit more cores on the same chip. So your first point means that the per-core performance is worse but maybe for some workloads the processor performance as a whole is better. But yeah not sure if that's realistic.
jhgb 5y ago
> Cooperative scheduling would require provable upper limits on the number of instructions run by process between calls to a yield function. When the process is a compute task with an input of variable size, this would result in the need to count iterations and branch in inner loops that you want to be fast. I am not sold on the idea that such an overhead is lower in that case than interrupt driven preemptive scheduling. Surely something like branch-on-random could be made to work with such code. It's effectively an interrupt point with the added benefit that you can place it exactly where you want it to.
5y ago

tachyonbeam 5y ago

Memory protection isn't just used to protect processes against one another, you can also use it to implement write barriers for a garbage collector, or to map files to memory, for example. I think you'd be hard pressed, with any kind of compiler, to prove that an object you're writing to isn't part of an old GC generation, seems like an intractable problem, unless you're in a pure functional programming language.

ingenieroariel 5y ago
sel4 has a Haskell version that they write before the C (granted, not sure how a ghc generated binary would be verified) but would the problem be tractable in that case?

zamalek 5y ago

> For example, MMUs are unnecessary if the OS verifies that all programs only access memory that's been allocated to it. That's what Microsoft was attempting with Singularity. Because binaries were IL, they could be reasonably verified for isolation guarantees during JIT compilation.

nynx 5y ago

I tried this with nebulet (https://github.com/nebulet/nebulet https://github.com/nebulet/nebulet). Unfortunately the MMU cannot be turned off on modern x86_64 processors.

opnitro 5y ago

Check out theseus! It's exploring some of these ideas. https://github.com/theseus-os/Theseus https://github.com/theseus-os/Theseus

mcguire 5y ago

I can't recall any names at the moment, but you might check out some of the Unikernel research. I seem to recall results of combining a unikernel and a safe language to be exactly what you describe.