#
1adb7e9b |
|
22-Jun-2020 |
Yanyan Shen <yshen@cog.systems> |
vtd: Add seL4_PageBits when testing address bits The total bits should include the page bit and index bits. The commit is based on PR #185 by laokz. Co-authored-by: laokz <laokz@foxmail.com> Signed-off-by: Yanyan Shen <yshen@cog.systems>
|
#
79da0792 |
|
01-Mar-2020 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
Convert license tags to SPDX identifiers This commit also converts our own copyright headers to directly use SPDX, but leaves all other copyright header intact, only adding the SPDX ident. As far as possible this commit also merges multiple Data61 copyright statements/headers into one for consistency.
|
#
8586b7f2 |
|
07-May-2019 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
boot: refactor allocation of rootserver objects Prior to this change, the boot process would dynamically allocate memory for root server objects based on the order of initialisation. Allocation was a best-fit algorithm. This change preallocates all memory for root server objects to an aligned untyped just after the user image. By allocating the objects in order of size, allocation is greatly simplified and the ability to reproduce the allocation offline based on the kernel and user image sizes is increased.
|
#
cd53e363 |
|
29-Apr-2019 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
trivial: remove unneccessary void cast
|
#
d0930f67 |
|
18-Mar-2019 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
style: consistently attach return type Add attach-return-type to astyle
|
#
761006e0 |
|
18-Mar-2019 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
style: consistently align pointer with name Run astyle with align-pointer=name
|
#
3d10ef0c |
|
18-Mar-2019 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
style: correct parenthesis padding Use astyle's unpad-paren to unpad all parentheses that are not included by pad-header, pad-oper, and pad-comma.
|
#
9d218f8c |
|
08-Aug-2018 |
Kent McLeod <Kent.Mcleod@data61.csiro.au> |
intel-vtd: Improve DMA fault error helpfulness The error will now split the source up into bus,dev,func components.
|
#
a9e1f517 |
|
21-Aug-2017 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
SELFOUR-1062: Hide all IOMMU related code behind #ifdef guards The IOMMU implementation is not going to be verified at the moment, and so the code for it needs to be hidden from verification, which we do by #ifdef'ing it out if the IOMMU is not enabled. As a result the IOMMU configuration depends on a non verification target
|
#
57fa0e0f |
|
07-Aug-2017 |
Hesham Almatary <hesham.almatary@data61.csiro.au> |
Share linker.h between architectures
|
#
de74bbb0 |
|
13-Jun-2017 |
Jonas Claeson <jonas.cl@protonmail.com> |
Removed unused static function supports_passthrough The last call to supports_passthrough was removed in commit 8e15c42921e42be2b80b2645f750fce7238fe231
|
#
bc380859 |
|
21-May-2017 |
Bamboo <bamboo@keg.ertos.in.nicta.com.au> |
[STYLE_FIX]
|
#
bac7826a |
|
21-May-2017 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
Avoid using bitfield generated *_ptr_new functions These functions can cause slow down during verification C parsing and do not currently have any proofs about them. More importantly there is no performance impact from just calling the regular *_new functions instead
|
#
96415656 |
|
03-Oct-2016 |
Bamboo <bamboo@keg.ertos.in.nicta.com.au> |
[STYLE_FIX]
|
#
2320d909 |
|
29-Sep-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
x86: Fixup IOMMU implementation Adds a mapping type to frame caps that tracks what kind of hierarchy the cap is mapped into; an MMU, IOMMU and in the future an EPT structure. Additionally the IOMMU code is updated to have correct functionality and be verification friendly.
|
#
bbc98573 |
|
28-Aug-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
SELFOUR-556: Rationalize BITS vs INDEX_BITS s/VTD_PT_BITS/VTD_PT_INDEX_BITS Current convention is to say that X_BITS is the log base 2 size of an object, not the log base 2 number of indices
|
#
f34f354a |
|
16-Aug-2016 |
Anna Lyons <Anna.Lyons@data61.csiro.au> |
SELFOUR-617: one source of memory object sizes Adds the following constants to libsel4 and uses them in the kernel. seL4_SectionSize (arm) seL4_SuperSectionSize (arm) seL4_HugePageSize (x86 - pae) seL4_LargePageSize (arm) seL4_DataFault seL4_InstructionFault
|
#
9a3a4504 |
|
15-Jun-2016 |
Adrian Danis <Adrian.Danis@data61.csiro.au> |
x86: Use IO page table size defined in libsel4
|
#
d20ca20a |
|
13-Jan-2016 |
Adrian Danis <Adrian.Danis@nicta.com.au> |
x86: Rename ia32->x86 This is a stylistic commit to make names of variables/constants and functions in the kernel more consistent. That is, things that are not IA32 specific, but are generic x86, get renamed to having an x86 name
|
#
8e15c429 |
|
03-Nov-2015 |
Adrian Danis <Adrian.Danis@nicta.com.au> |
x86: Port some of the IOMMU changes on the experimental branch This changes the IOMMU from using passthrough devices and instead directly mapping in the reserved regions that are needed for each device.
|
#
646638ef |
|
09-Nov-2015 |
Adrian Danis <Adrian.Danis@nicta.com.au> |
x86: Do not conditionally compile IOMMU code, use build/run time checks Guarding code with #ifdef's makes even cursor testing of 'does this code compile' difficult due to code being hidden by the pre-processor. Using config_set in regular C if statements is performant as the compiler can trivially detect dead code at compile time, and at -O1 and above will not even link in symbols referenced by dead code in these blocks, so this will not bloat image size
|
#
171824f7 |
|
07-Dec-2015 |
Adrian Danis <Adrian.Danis@nicta.com.au> |
Change additional int->word_t due to interraction with the C parser to ease verification
|
#
617df4a7 |
|
03-Nov-2015 |
Adrian Danis <Adrian.Danis@nicta.com.au> |
Rationalize standard types This commit aims to rationalize how we represent different types for compatiblity between ARM and x86, as well as between 32 and 64 bit code. The choices being made here is to declare that a uint32_t has a type of 'int', this allows uint32_t to be declared consistently across 32 and 64 bit (at least in GCC). The word_t type is declared using a 'long' (not a uint32_t or uint64_t) to allow for a word_t to be backed by the same type on both 32 and 64 bit All other types that want to be declared as the size of a native word get declared in terms of a word_t
|
#
52dbcd6a |
|
01-Oct-2015 |
Anna Lyons <Anna.Lyons@nicta.com.au> |
and one last format string
|
#
72826dba |
|
01-Oct-2015 |
Anna Lyons <Anna.Lyons@nicta.com.au> |
Fix IOMMU part of x86 build
|
#
91b7da86 |
|
17-Jul-2014 |
TrusthworthySystems <gatekeeper@sel4.systems> |
Release snapshot
|