History log of /seL4-l4v-10.1.1/l4v/proof/invariant-abstract/ARM/ArchIpcCancel_AI.thy
Revision Date Author Comments
# 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.


# b37bc044 20-Nov-2017 Miki Tanaka <miki.tanaka@nicta.com.au>

arm ainvs: wp rules for simple_ko setter/getter


# 796887d9 11-Jul-2017 Alejandro Gomez-Londono <alejandro.gomez@nicta.com.au>

Removes all trailing whitespaces


# b9313f6d 14-Jun-2016 Matthew Brecknell <Matthew.Brecknell@nicta.com.au>

arch_split: invariants: tidied


# eb40bef2 02-Jun-2016 Alejandro Gomez-Londono <alejandro.gomez@nicta.com.au>

arch_split: IpcCancel_AI [VER-567]


# 9f626225 10-May-2016 Daniel Matichuk <daniel.matichuk@nicta.com.au>

arch_split: skeleton arch files for AInvs