yyshen

@nomadeel I wonder if you have a tarball with all the required patches to run an x64 VM? If so, could you send me a copy? That might save me...

> Sure, go for it. To test it, checkout the camkes-vm-examples manifest and then you'll need this other branch [seL4/seL4_projects_libs#16](https://github.com/seL4/seL4_projects_libs/pull/16). Then run `../init-build.sh -DPLATFORM=x86_64 -DCAMKES_VM_APP=minimal`. This should build an x64...

> > @nomadeel Do you have a working tarball for all the required changes. Could you drop me one so I can just build and run? Thanks > > This...

> Sure, go for it. To test it, checkout the camkes-vm-examples manifest and then you'll need this other branch [seL4/seL4_projects_libs#16](https://github.com/seL4/seL4_projects_libs/pull/16). Then run `../init-build.sh -DPLATFORM=x86_64 -DCAMKES_VM_APP=minimal`. This should build an x64...

> You'll have remove the `FORCE` keywords at the end of the `KernelSel4Arch` variable in this file here: https://github.com/seL4/camkes-vm-examples/blob/master/apps/x86/minimal/app_settings.cmake @nomadeel Thanks. Changing it to x86_64 worked. A follow-up question: what...

> What is the difference between a page directory and a page table in the terminology you are using? If the final mapping is a page mapping, via seL4_ARM_Page_Map(), it...

@oscarwcl good catch!

@kent-mcleod @lsf37 What I have in mind to fix this is to use "address translation" instruction to check the write permission of the address before performing an invalidation, unless the...

> The ultimate right (including masks etc) is only in the page table entries, so I guess we do have to walk the table, yes. Is the plan to put...

> > It depends if an error would be returned to the caller. If we could simply ignore invalidate without write permission, putting the check in invalidateByVA is OK. But...