Can camkes be used with ARM AARCH64?
I am attempting to build a linux virtual machine on top of the zynqmp ultrascape+ / sel4 kernel, and using the tk1 vmm project as my reference point.
When the build system attempts to generate camkes-gen.mk, it fails - displaying an error indicating that aarch64 is not a valid architecture specification for camkes. I see that valid arm options are aarch32 or arm_hyp.
Is arm_hyp what I am looking for here?
What would I need to do in order to strip the camkes dependencies out of the tk1 vmm project?
Thanks,
Mike D Computer Security Engineer - Intelligent Automation, Inc. (301)294-5263
________________________________ This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.
"Michael" == Michael DeFrancis mdefrancis@i-a-i.com writes:
Michael> I am attempting to build a linux virtual machine on top of Michael> the zynqmp ultrascape+ / sel4 kernel, and using the tk1 vmm Michael> project as my reference point.
The TK1 VMM runs in 32-bit mode. We haven't written a hypervisor yet for aarch64.
arm_hyp is essentially armv7-a with VE; aarch32 is armv6 or later. Both are 32-bit.
Patches are welcome (with Contributer licence agreement); we would really like to see a 64-bit virtual machine monitor.
Peter C -- Dr Peter Chubb Tel: +61 2 9490 5852 http://ts.data61.csiro.au/ Trustworthy Systems Group Data61 (formerly NICTA)
Right.
I need to create an aarch64 (armv8-a) sel4 hypervisor and vmm in order to support our customers in the USA. I will contribute all back to community afterwards.
I need help getting started. Can you help?
Mike
____ Ramble.. I need the hypervisor pieces and the vmm pieces to run at aarch64 to do this. I am willing to do the heavy lifting myself and of course contribute back all of my changes - with whatever license agreement is necessary - but I think I need some help getting started. Could you or someone from your team point me in the right direction?
Getting an aarch64 hypervisor / linux demo running on top of sel4 will definitely help us to sell sel4 (no pun intended?) to US customers interested in using sel4 for safety critical systems.
I would prefer to stick with using camkes but I may have to strip all of the camkes stuff out if it expedites things on my end in order to meet our schedule. I have reference code from the xen hypervisor (www.xen.world), that I can use as a baseline.
-----Original Message----- From: Peter.Chubb@data61.csiro.au [mailto:Peter.Chubb@data61.csiro.au] Sent: Tuesday, December 5, 2017 4:38 PM To: Michael DeFrancis mdefrancis@i-a-i.com Cc: devel@sel4.systems Subject: Re: [seL4] AARCH64 with CAMKES (Questions)
"Michael" == Michael DeFrancis mdefrancis@i-a-i.com writes:
Michael> I am attempting to build a linux virtual machine on top of the Michael> zynqmp ultrascape+ / sel4 kernel, and using the tk1 vmm project Michael> as my reference point.
The TK1 VMM runs in 32-bit mode. We haven't written a hypervisor yet for aarch64.
arm_hyp is essentially armv7-a with VE; aarch32 is armv6 or later. Both are 32-bit.
Patches are welcome (with Contributer licence agreement); we would really like to see a 64-bit virtual machine monitor.
Peter C -- Dr Peter Chubb Tel: +61 2 9490 5852 http://ts.data61.csiro.au/ Trustworthy Systems Group Data61 (formerly NICTA)
________________________________ This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.
Hi, Mike,
I am adding the ARMv8 hypervisor support for seL4 and related user-mode libraries (Tegra TX1 board). Let's discuss how could collaborate on this off-line.
Regards, Yanyan
________________________________________ From: Devel devel-bounces@sel4.systems on behalf of Michael DeFrancis mdefrancis@i-a-i.com Sent: Wednesday, December 6, 2017 8:54 AM To: Chubb, Peter (Data61, Kensington NSW) Cc: devel@sel4.systems Subject: Re: [seL4] AARCH64 with CAMKES (Questions)
Right.
I need to create an aarch64 (armv8-a) sel4 hypervisor and vmm in order to support our customers in the USA. I will contribute all back to community afterwards.
I need help getting started. Can you help?
Mike
____ Ramble.. I need the hypervisor pieces and the vmm pieces to run at aarch64 to do this. I am willing to do the heavy lifting myself and of course contribute back all of my changes - with whatever license agreement is necessary - but I think I need some help getting started. Could you or someone from your team point me in the right direction?
Getting an aarch64 hypervisor / linux demo running on top of sel4 will definitely help us to sell sel4 (no pun intended?) to US customers interested in using sel4 for safety critical systems.
I would prefer to stick with using camkes but I may have to strip all of the camkes stuff out if it expedites things on my end in order to meet our schedule. I have reference code from the xen hypervisor (www.xen.world), that I can use as a baseline.
-----Original Message----- From: Peter.Chubb@data61.csiro.au [mailto:Peter.Chubb@data61.csiro.au] Sent: Tuesday, December 5, 2017 4:38 PM To: Michael DeFrancis mdefrancis@i-a-i.com Cc: devel@sel4.systems Subject: Re: [seL4] AARCH64 with CAMKES (Questions)
"Michael" == Michael DeFrancis mdefrancis@i-a-i.com writes:
Michael> I am attempting to build a linux virtual machine on top of the Michael> zynqmp ultrascape+ / sel4 kernel, and using the tk1 vmm project Michael> as my reference point.
The TK1 VMM runs in 32-bit mode. We haven't written a hypervisor yet for aarch64.
arm_hyp is essentially armv7-a with VE; aarch32 is armv6 or later. Both are 32-bit.
Patches are welcome (with Contributer licence agreement); we would really like to see a 64-bit virtual machine monitor.
Peter C -- Dr Peter Chubb Tel: +61 2 9490 5852 http://ts.data61.csiro.au/ Trustworthy Systems Group Data61 (formerly NICTA)
________________________________ This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.
_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
-
Michael DeFrancis -
Peter.Chubb＠data61.csiro.au -
Yanyan.Shen＠data61.csiro.au