#
6b9d9d24 |
|
09-Jun-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
|
#
97c24b95 |
|
11-Jun-2018 |
Corey Lewis <corey.lewis@data61.csiro.au> |
ainvs: Add itcb_arch to the itcb projection This allows us to more easily show that arch specific tcb fields are preserved by many functions of the spec. For ARM_HYP we add a projection for the tcb_vcpu field.
|
#
25125763 |
|
11-Apr-2018 |
Joel Beeren <joel.beeren@data61.csiro.au> |
arm-hyp: ioportcontrol: fixes after adding IOPortControlCaps to x64
|
#
2d0baab4 |
|
13-Mar-2018 |
Corey Lewis <corey.lewis@data61.csiro.au> |
Proof update for crunch changes
|
#
652cbb96 |
|
14-Mar-2018 |
Thomas Sewell <Thomas.Sewell@data61.csiro.au> |
Initial proof updates for combinator changes.
|
#
4601f2a1 |
|
06-Feb-2018 |
Joel Beeren <joel.beeren@data61.csiro.au> |
Genericise deletion actions that occur after empty_slot This patch adds a generic "post_cap_deletion" step that is called by finalise_slot. Previous to this, the only caps which had actions required at this stage were IRQHandlerCaps -- it was required that the IRQ bitmap be updated after the cap itself was removed (as the invariants state that for any existing IRQHandlerCap, the corresponding bit in the IRQ bitmap must be set). By genericising this, we add the capacity for new, arch-specific post cap deletion actions to occur in the future.
|
#
6d8e9170 |
|
19-Jul-2017 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
Remove valid_arch_objs now that we have valid_vspace_objs to express validiy of vspace objects, we do not need valid_arch_objs: we have valid_objs to state the validity of non-vspace arch objects.
|
#
2f70a304 |
|
09-Aug-2017 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
ainvs: integrate all architectures
|
#
88e2c549 |
|
04-Feb-2017 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
arm-hyp invariants: ArchCNodeInv_AI done
|
#
317b2b3f |
|
02-Feb-2017 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
arm-hyp invariants: new liveness definition * the definition of liveness is extended for tcb/vcpu reference * proved liveness related properties for dissociate_vcpu_tcb, prepare_thread_delete, etc.
|
#
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
|
#
7e79b1b7 |
|
17-Jan-2017 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
changes after rebasing (for isabelle2016-1 and the new wp)
|
#
eb0ec4dc |
|
27-Feb-2017 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
arch_splitting, fixing sorries, some more invariants
|
#
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
|
#
1d4b6e93 |
|
26-Aug-2016 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
arm-hyp invariants: updates for vcpu, alignments, valid_vspace_obj, wellformed_arch_obj, etc.
|
#
0d4e4bd2 |
|
23-Nov-2016 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
arm-hyp invariants: copy arch-splitted invariant files from ARM earlier updates in ArchInvariants are kept
|
#
f0da7d17 |
|
06-Dec-2016 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
arm-hyp invariants: add ARM_HYP directory, updating ArchInvariants_AI and Invariants_AI
|