History log of /seL4-l4v-10.1.1/l4v/spec/design/skel/X64/ArchRetype_H.thy
Revision Date Author Comments
# 53fde5e5 29-Jul-2018 Gerwin Klein <gerwin.klein@data61.csiro.au>

lib/design: enable more Haskell-like list comprehension syntax

Accept "[f x | x \leftarrow t]" in addition to "[f x . x \leftarrow t]",
because the former is what naturally comes out of the Haskell translator, and
the regexps that would be necessary in the Haskell translator for this are
distasteful.

JIRA-VER 927


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


# 53299592 14-Mar-2017 Joel Beeren <joel.beeren@nicta.com.au>

x64: got haskell translator running on existing haskell kernel


# 73b73156 05-May-2016 Joel Beeren <joel.beeren@nicta.com.au>

x64: add arch_split'd x64 spec with IOMMU stuff