diminished takes two caps and asserts that one is equal to the other
except that one may have fewer rights. We remove this definition and all
references to it, replacing diminished with equality.
Fixes a case where a thread can go from Running->Inactive->Restart and
use a restart PC that is out of date. An out of date restart PC occurs
when a thread was transitioned to running after being in a blocked
state, but was never scheduled and so did not execute the traps code
that updates the restart PC.
This also renames relevant register names for consistency across
architectures (FaultIP and NextIP).
Mainly repercusion of changes occuring for Access:
- Fix subjectReads and subjectAffects with new authorities
- SILC label is forbidden to contain any transferable cap
- Lots of lemma that required is_subject on their parameter now only
require aag_can_read when possible
- Major cleanup of the integrity ==> subjectAffects proofs for kheap,
CDT and user memory.
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.
The things that usually go wrong:
- wp fall through: add +, e.g.
apply (wp select_wp) -> apply (wp select_wp)+
- precondition: you can remove most hoare_pre, but wpc still needs it, and
sometimes the wp instance relies on being able to fit a rule to the
current non-schematic precondition. In that case, use "including no_pre"
to switch off the automatic hoare_pre application.
- very rarely there is a schematic postcondition that interferes with the
new trivial cleanup rules, because the rest of the script assumes some
specific state afterwards (shouldn't happen in a reasonable proof, but
not all proofs are reasonable..). In that case, (wp_once ...)+ should
emulate the old behaviour precisely.
* tcb_context rephrasing to (tcb_context o tcb_arch) and respectively
for set operations
* unfolding of reserved_irq for trivially solving most lemmas
* Changes to the inductive definition of integrity_obj to account for
tcb_arch and tcb_context new location
* Changes to the tcb examples in ExampleSystem to include tcb_arch
* Rephrasing of domain_sep_inv to accommodate the ReservedIRQ case
* Mostly rephrasing of tcb_context to (some form of) (tcb_context o tcb_arch)
* Trivial unfolding of handle_reserved_irq for hoare rules
* Examples in Example_Valid_State.thy were updated
* Nothing remarkable, mostly rephrasing of tcb_context and ReservedIRQ
handling
* Fun fact, some proofs are now shorter
tags: [VER-623][SELFOUR-413]
To finish the proof of refinement to C, the specification for checkPrio
needed strengthening: the checkPrio spec now takes a machine word
argument. In the spec, priorities are still stored as 8-bit quantities,
however. Once the spec was strenthened, it was possible to remove some
redundant checks and mask operations from the C code.
A thread's maximum controlled priority (MCP) determines the maximum
thread priority or MCP it can assign to another thread (or itself).
Ryan Barry
Gerwin Klein
Mitchell Buckley
Gerwin Klein
Victor Phan
Corey Lewis
Michael McInerney
Japheth Lim
Thibaut Perami
Edward Pierzchalski
Mitchell Buckley
Thomas Sewell
Joel Beeren
Miki Tanaka
Alejandro Gomez-Londono
Gerwin Klein
Matthew Brecknell
Xin,Gao
Joel Beeren
Thomas Sewell
Daniel Matichuk
Matthew Brecknell
Sophie Taylor