History log of /seL4-l4v-10.1.1/l4v/spec/design/skel/Retype_H.thy
Revision Date Author Comments
# f728dd25 18-Mar-2018 Joel Beeren <joel.beeren@data61.csiro.au>

x64: Add IOPortControlCaps to control IO port allocation

The previous implementation of IOPortCaps has problems with revocability
and determining parency etc. This commit adds IOPortControlCaps which
behave identically to IRQControlCaps -- invoking the IOPortControlCap
allows one to create IOPortCaps with the supplied range.

There now exist invariants to show that there is only one
IOPortControlCap and that all IOPortCaps in the system do not overlap.
Furthermore there is a global record of which IO ports have been
allocated to prevent reissuing the same ports.


# 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.


# 7602a6c3 31-Jul-2017 Joel Beeren <joel.beeren@nicta.com.au>

design: integrate all architectures


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

Removes all trailing whitespaces


# b853647a 07-Feb-2017 Miki Tanaka <miki.tanaka@nicta.com.au>

execspec: fix skeleton for prepareThreadDelete, generated files


# 2553371a 06-Nov-2016 Joel Beeren <joel.beeren@nicta.com.au>

SELFOUR-64: Remove general Recycle operation

This removes the RecycleCap CNodeInvocation, whilst
retaining recycle behaviour for Endpoints -- now renamed
CNodeCancelBadgedSends.


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

arch_split: fix proofs after removing shadow and unqualify commands and adding fix for crunch. Checks up to DPolicy.


# 1d20b393 26-Apr-2016 Daniel Matichuk <daniel.matichuk@nicta.com.au>

arch_split: replaced sublocale with global_naming


# 72337faa 31-Mar-2016 Daniel Matichuk <daniel.matichuk@nicta.com.au>

arch_split: added namespacing to ExecSpec


# 12fa8686 16-May-2015 Gerwin Klein <gerwin.klein@nicta.com.au>

fewer warnings


# 2a03e81d 14-Jul-2014 Gerwin Klein <gerwin.klein@nicta.com.au>

Import release snapshot.