#
d930ef2c |
|
30-Oct-2018 |
Santiago Bautista <santiago.bautista@data61.csiro.au> |
arm-hyp ainvs: prove that the vcpu of the idle thread is always None * Context : We would like to prove that, for ARM_HYP architecture, the current vcpu is always the vcpu associated to the current thread. See issue https://jira.csiro.au/browse/VER-770 and PR 291 http://bitbucket.keg.ertos.in.nicta.com.au/projects/SEL4/repos/l4v/pull-requests/291 * Intermediate step : the vcpu of the idle thread is always None In this commit we update the proofs of abstract invariants for the arm_hyp architecture, so that the new version of `valid_idle`, stating that the vcpu of the idle thread is always None, holds.
|
#
c4dc578b |
|
17-Sep-2018 |
Edward Pierzchalski <ed.pierzchalski@data61.csiro.au> |
Fix up proofs after word lemma moves
|
#
d7574020 |
|
20-Sep-2018 |
Edward Pierzchalski <ed.pierzchalski@data61.csiro.au> |
Remove pure word lemmas from proof/* Removes redundant lemmas after moving them up to Word_Lib.
|
#
590b83ce |
|
23-Jun-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
Isabelle2018 arm: AInvs
|
#
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>")
|
#
b5cdf470 |
|
13-Jun-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
globally use session-qualified imports; add Lib session Session-qualified imports will be required for Isabelle2018 and help clarify the structure of sessions in the build tree. This commit mainly adds a new set of sessions for lib/, including a Lib session that includes most theories in lib/ and a few separate sessions for parts that have dependencies beyond CParser or are separate AFP sessions. The group "lib" collects all lib/ sessions. As a consequence, other theories should use lib/ theories by session name, not by path, which in turns means spec and proof sessions should also refer to each other by session name, not path, to avoid duplicate theory errors in theory merges later.
|
#
d77d31a7 |
|
03-Jun-2018 |
Corey Lewis <corey.lewis@data61.csiro.au> |
lib: Refactor crunch so that it can be used for both the nondet monad and the trace monad
|
#
25125763 |
|
11-Apr-2018 |
Joel Beeren <joel.beeren@data61.csiro.au> |
arm-hyp: ioportcontrol: fixes after adding IOPortControlCaps to x64
|
#
830f407d |
|
05-Mar-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
arm-hyp ainvs: proof update for user_context refactor
|
#
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.
|
#
6eb2cb74 |
|
13-Dec-2017 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
arm-hyp: simple_ko setter/getter
|
#
4f68967b |
|
28-Aug-2017 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
Isabelle2017: update AInvs for RC0 * word_eqI is no longer rule_format. * Updated Isabelle/ML Thm.join_proofs to Thm.consolidate. * Updated suffix_refl to suffix_order.order.refl. * Removed some lines of proofs, thanks to improved simplifier.
|
#
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
|
#
392d055e |
|
15-May-2017 |
Joel Beeren <joel.beeren@nicta.com.au> |
SELFOUR-748: rename tlb invalidation functions
|
#
3dd69560 |
|
16-May-2017 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
arm-hyp AInvs: reintroduce valid_global_objs and valid_global_vspace_mappings
|
#
7470dcb6 |
|
08-May-2017 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
arm-hyp invariants: make valid_arch_obj depend on valid_vspace_obj
|
#
cab9f288 |
|
05-Apr-2017 |
Alejandro Gomez-Londono <alejandro.gomez@nicta.com.au> |
arm-hyp ainvs: (Fix) Correctly defining setCurrentPD
|
#
dbbc0d41 |
|
25-Feb-2017 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
arm-hyp: AInvs sorry-free
|
#
4407fc31 |
|
25-Feb-2017 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
arm-hyp invariants: fix pde_shifting in ArchAcc_AI
|
#
9123c363 |
|
05-Feb-2017 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
arm-hyp: changes after rebase (on top of d08ee04e2f8)
|
#
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.
|
#
7e79b1b7 |
|
17-Jan-2017 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
changes after rebasing (for isabelle2016-1 and the new wp)
|
#
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.
|
#
26970ce8 |
|
24-Aug-2016 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
arm-hyp invariants: symrefs for hypervisor introducing hyp_sym_refs (vcpu/tcb symref) related definitions + proof updates
|
#
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
|