Linked by Thom Holwerda on Wed 12th Sep 2018 19:29 UTC
OSNews, Generic OSes

This work describes the porting of Hyperkernel, an x86 kernel, to the ARMv8-A architecture. Hyperkernel was created to demonstrate various OS design decisions that are amenable to push-button verification. Hyperkernel simplifies reasoning about virtual memory by separating the kernel and user address spaces. In addition, Hyperkernel adopts an exokernel design to minimize code complexity, and thus its required proof burden. Both of Hyperkernel's design choices are accomplished through the use of x86 virtualization support. After developing an x86 prototype, advantageous design differences between x86 and ARM motivated us to port Hyperkernel to the ARMv8-A architecture. We explored these differences and benchmarked aspects of the new interface Hyperkernel provides on ARM to demonstrate that the ARM version of Hyperkernel should be explored further in the future. We also outline the ARMv8-A architecture and the various design challenges overcome to fit Hyperkernel within the ARM programming model.

E-mail Print r 2   1 Comment(s)
Thread beginning with comment 662275
To read all comments associated with this story, please click here.
Comment by ssokolow
by ssokolow on Wed 12th Sep 2018 20:58 UTC
ssokolow
Member since:
2010-01-21

Aside from the missing spaces, that quote has some "fi" ligatures that get mojibake'd by the interaction between OSNews's feed generation and my Thunderbird.

"x86kernel,totheARMv8-Aarchitecture."
"designdifferencesbetweenx86andARMmotivatedus"
"theARMv8-Aarchitectureandthevariousdesignchallenges"
"verification"
"simplifies"
"overcome to fit"

Edited 2018-09-12 21:01 UTC

Reply Score: 2