Re: [seL4] vmm documentation

Here is another question, again on ARM. Let's say I want to configure the VCPU to trap on certain instructions or register accesses. It is my understanding I can do this by setting either HCR or HSTR to trap the way I want it to. I've played with setting HCR how I want it, and it looks like I can handle the trap in the vm_event function of vm.c, under the seL4_Fault_VCPUFault case. What I'm unsure of is how to handle the trap. I need to emulate the trapped instruction, right? Is there a particularly good place to do that or is it already implemented? If I switch to using HSTR to trap, where should that be handled? Also in the seL4_Fault_VCPUFault case? On Wed, Jun 14, 2017 at 1:17 PM, Mike Clark wrote:

Thanks Anna. That is great. Is there a quick and easy way to get up and running with hypercalls on ARM?

On Mon, Jun 12, 2017 at 8:17 PM, wrote:

...

Hi Mike,

We have some pages on the developer wiki. For x86 there is a pretty comprehensive tutorial on adding a hypercall and more:

https://wiki.sel4.systems/CAmkESVM

We're starting to develop docs on the ARM vm here: https://wiki.sel4.systems/CAmkES-ARM-VM but as you can see it's pretty bare. Note that I don't think the x86 VM instrcutions apply to the ARM VM, as they are structured differently.

Anna.

________________________________________ From: Devel on behalf of Mike Clark Sent: Friday, 9 June 2017 10:56 PM To: Danis, Adrian (Data61, Kensington NSW) Cc: devel@sel4.systems Subject: Re: [seL4] vmm documentation

Okay, so I'll start with something more concrete that should help me understand a few things. Let's say I wanted to implement a hypercall and for the purposes of this discussion, let's assume ARM.

A user process on the Linux VM can issue a hypercall with the HVC instruction, right? Where would I need to add code to the VMM to handle this hypercall?

Also, it is my understanding that certain instructions will cause a trap into the VMM. Where is that handled?

Thanks!

On Thu, Jun 8, 2017 at 8:10 PM, wrote:

...

Hi Mike,

Unfortunately we haven't yet written any documentation on the VMM internals or how it works. You are actually the first person to express interest in this. Will try to make it a higher priority to write at least a brief overview of the structure. For now my advice is to be familiar with CAmkES, have a built version of the VMM so that you can code search for generated code and then start exploring from either https://github.com/seL4/camkes-vm/blob/master/components/Init/src/main.c#L52... or https://github.com/SEL4PROJ/camkes-arm-vm/blob/master/components/VM/src/main... depending on whether you are asking about the arm or x86 VMM.

Adrian

On Fri 09-Jun-2017 2:26 AM, Mike Clark wrote:

Is there any documentation on how the VMM works? If I wanted to start hacking on the VMM and extend its capability, where should I start looking to learn how it works, etc?

That might be a pretty broad topic, because there are lots of ways the VMM can be extended, I'm sure. Broad is fine, until I get things more figured out.

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel