| #
8173a37c |
|
13-Aug-2018 |
Mitchell Buckley <mitchell.buckley@data61.csiro.au> |
Updated specs and proofs for SELFOUR-1491: control IRQ triggering on ARM.
|
| #
9d315cda |
|
12-Dec-2017 |
Maksym Bortin <Maksym.Bortin@data61.csiro.au> |
ainvs+refine: update proofs for SetTLSBase (VER-807)
|
| #
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.
|
| #
2d0baab4 |
|
13-Mar-2018 |
Corey Lewis <corey.lewis@data61.csiro.au> |
Proof update for crunch changes
|
| #
830f407d |
|
05-Mar-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
arm-hyp ainvs: proof update for user_context refactor
|
| #
f0795805 |
|
15-Feb-2018 |
Michael Sproul <michael.sproul@data61.csiro.au> |
SELFOUR-1016: fix confused deputy problem when setting priorities
|
| #
a5a5edc8 |
|
28-Nov-2017 |
Joel Beeren <joel.beeren@data61.csiro.au> |
VER-849: abstractly declare a threads registers have changed
This removes an ifdef present in invokeTCB_(Copy|Write)Registers, and
adds the function Arch_postModifyRegisters which does nothing on any
arch except x86-64.
|
| #
2c0820c1 |
|
05-Oct-2017 |
Thomas Sewell <Thomas.Sewell@data61.csiro.au> |
Improve arch-split for BCorres2_AI changes.
|
| #
1f4b9e68 |
|
03-May-2017 |
Joel Beeren <joel.beeren@nicta.com.au> |
arm-hyp: rename archTCBSanitise, arch_tcb_sanitise_condition, Arch_hasVCPU to be more appropriate
|
| #
083e65a4 |
|
26-Apr-2017 |
Joel Beeren <joel.beeren@nicta.com.au> |
arm-hyp ainvs: fix ainvs after sanitise_register refactor
|
| #
65926a84 |
|
15-Mar-2017 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
arm-hyp/ainvs: proof repair for vgic_maintenance
Includes stronger assumptions for handle_reserved_interrupt and friends,
which should be backported later (see JIRA VER-719 and VER-720)
|
| #
9123c363 |
|
05-Feb-2017 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
arm-hyp: changes after rebase (on top of d08ee04e2f8)
|
| #
c80cffc4 |
|
27-Feb-2017 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
arm-hyp invariants: more fixes for crunches and sorries
* passes quick_and_dirty test but needs a bit more work
|
| #
d25e2c8d |
|
19-Dec-2016 |
Alejandro Gomez-Londono <alejandro.gomez@nicta.com.au> |
arm-hyp invariants: fixing crunches and invs proofs
|
| #
5cabf382 |
|
18-Dec-2016 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
arm-hyp invariants: fix arch_splitting/locales
* tcb_arch_ref: definition and invariants (to access obj_refs in tcb_arch in generic contexts)
* fixes related hyp_refs
|
| #
c1c30691 |
|
12-Dec-2016 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
arm-hyp invariants: incremental progress (sorrying, fixing crunches/alignments, etc.)
* sorry perform_vcpu_invocation invariant statements
* fix pg_entry_align and related statements
* some crunches in ArchFinalise_AI
|
| #
61dffdb6 |
|
26-Feb-2017 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
arm-hyp invariants: changes from rebase for ARM_HYP invariants
|
| #
298d4ea6 |
|
04-Jul-2016 |
Rafal Kolanski <rafal.kolanski@nicta.com.au> |
arm-hyp haskell: changes from meeting
|