| #
4a3d7a95 |
|
13-Jun-2018 |
Rafal Kolanski <rafal.kolanski@nicta.com.au> |
arm-hyp: update proofs for SELFOUR-584: running multiple VMs on ARM
As requested by verification, hypervisor registers are now an
enumeration-indexed array rather than individual fields. This cleans up
some of the proof. Additionally, we sweep some non-complexity under the
machine op rug: vcpu_hw_write/read_reg_ccorres is as deep as we go,
rather than specifying every operation and proving that
vcpu_hw_write seL4_VCPUReg_REG calls set_REG for every REG
I took this opportunity to clean up some arm-hyp definitions and proofs,
so some whitespace cleanup got tangled in.
|
| #
9f3924d1 |
|
28-Jun-2017 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
design spec: adjust skeleton files for unified haskell files
|
| #
da1aaa50 |
|
26-Apr-2017 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
arm-hyp design: update skeleton to include new Haskell functions
|
| #
5181434b |
|
21-Feb-2017 |
Rafal Kolanski <rafal.kolanski@nicta.com.au> |
arm-hyp design: VCPUFault and VGICMaintenance
|
| #
c32e6552 |
|
27-Jul-2016 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
arm-hyp execspec: add irqVGICMaintenane and initInterruptController
with caseconvs, generated files
|
| #
00f1393c |
|
27-Jul-2016 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
arm-hyp execspec: add caseconvs, fixes in haskell + VCPU_H
|
| #
0ee19108 |
|
19-Jul-2016 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
arm-hyp execspec: VCPU skeleton file, new constructs (arch_tcb, arch_fault, Hypervisor) for ARM_HYP
|