History log of /seL4-l4v-10.1.1/l4v/spec/haskell/src/SEL4/Object/Interrupt/ARM.lhs
Revision Date Author Comments
# 8173a37c 13-Aug-2018 Mitchell Buckley <mitchell.buckley@data61.csiro.au>

Updated specs and proofs for SELFOUR-1491: control IRQ triggering on ARM.


# dac7a00e 26-Aug-2018 Ilya Yanok <ilya.yanok@gmail.com>

haskell: explicitly import Prelude hiding Word

everywhere where it can clash with Word type defined by SEL4.


# 807a9792 15-Jul-2018 Gerwin Klein <gerwin.klein@data61.csiro.au>

arm-hyp haskell: use consistent ARMHYP_SMMU tag


# d8d1ee01 28-Jun-2017 Miki Tanaka <miki.tanaka@nicta.com.au>

haskell: unify arm and arm-hyp haskell files

- both ARM and ARM_HYP haskell specs are now generated from the same set of files using cpp
- callbacks and platform files are merged into one directory (ARM)
- remove check-arm-hyp.py now that there are no ARM_HYP.lhs files


# 7b75ed2b 06-Feb-2017 Rafal Kolanski <rafal.kolanski@nicta.com.au>

haskell: make ARM resemble the output of ARM_HYP preprocessing

The first step of merging the ARM hypervisor extensions into existing
ARM is to make the current ARM look like the preprocessed output of
ARM_HYP, which currently supports both platforms.

NOTE: this requires updates to ARM Refine and CRefine due to shuffling
around some constants (pteBits et al.). That is on its way.


# 6dad6a1c 19-Jul-2016 Miki Tanaka <miki.tanaka@nicta.com.au>

ExecSpec: arch-specific faults + VMFault -> ArchFault + ReservedIRQ

* skeletons, adding new constructs (arch_tcb, arch_fault)

* adjusting skeletons for ReserveIRQ + small change in haskell (ARM)

Changes in: spec/haskell/src/SEL4/Object/Interrupt/ARM.lhs:37:21
Due to "Defined but not used: ‘irq’"

* arch-splitting faults in skeletons (ARM)

* fix arch_tcb and asUser namespace issues in skeletons (ARM)

* checking in current generated files

tags: [VER-623][SELFOUR-413]


# c92baf74 15-Jul-2016 Rafal Kolanski <rafal.kolanski@nicta.com.au>

Haskell: arch-specific faults + split VMFault -> ArchFault + ReservedIRQ

Hypervisor extensions add extra fault types which are entirely
arch-specific. While the concept of a VM fault exists on all platforms,
these faults are also arch-specific.

This change adds an ArchFault datatype and constructor to the generic
Faults and Failures, and moves VMFault into ArchFault for the ARM
platform.

NOTE: fault indices have changed (generic goes before arch) as per
the changes needed for SELFOUR-413, which is the seL4 C equivalent of
this commit.

* add arch faults and failures to SEL4.cabal

* introduce and handle IRQReserved

On ARM this does nothing, but on other platforms reserved IRQs are
actually used.

* split TCB into ArchTCB (userContext)

* changing ArchFault to make haskell-translator to work

tags: [VER-623][SELFOUR-413]


# ebc7cbe5 23-May-2016 Japheth Lim <Japheth.Lim@nicta.com.au>

haskell: move Haskell kernel into spec/