portugalfuturista/seL4
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

x64: Allow full 48bits of virtual address space to be used

Browse source 
Prior to this commit virtual addresses in the bitfield were considered
to be 48-bits, with sign extension to 64-bits. This meant that we were
actually sign extended bit number 47. Whilst this gives correct cannonical
addresses it prevents a portion of the address space from being used.

This commit changes the bitfield to use 49-bit virtual addresses, so that
after the bit 48 is used for sign extension there is still 48-bits of
usable address.
This commit is contained in:
Adrian Danis 2017-01-25 10:42:59 +11:00
parent f3d62531b5
commit f6d367e8df
2 changed files with 41 additions and 41 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

46
include/arch/x86/arch/64/mode/object/structures.bf
View file

@ -13,7 +13,7 @@
#include <config.h>
---- Default base size: uint64_t
base 64(48,1)
base 64(49,1)
-- Including the common structures.bf is neccessary because
-- we need the structures to be visible here when building
@ -31,49 +31,49 @@ block frame_cap {
field capType 5
field capFSize 2
field capFMapType 2
field_high capFMappedAddress 48
field_high capFMappedAddress 49
field capFVMRights 2
field capFIsDevice 1
padding 4
padding 3
}
-- Second-level page table
block page_table_cap {
padding 4
padding 3
field capPTMappedASID 12
field_high capPTBasePtr 48
field_high capPTBasePtr 49
field capType 5
padding 10
padding 9
field capPTIsMapped 1
field_high capPTMappedAddress 27
field_high capPTMappedAddress 28
padding 21
}
-- First-level page table (page directory)
block page_directory_cap {
padding 4
padding 3
field capPDMappedASID 12
field_high capPDBasePtr 48
field_high capPDBasePtr 49
field capType 5
padding 10
padding 9
field capPDIsMapped 1
field_high capPDMappedAddress 18
field_high capPDMappedAddress 19
padding 30
}
block pdpt_cap {
padding 4
padding 3
field capPDPTMappedASID 12
field_high capPDPTBasePtr 48
field_high capPDPTBasePtr 49
field capType 5
field capPDPTIsMapped 1
field_high capPDPTMappedAddress 9
padding 49
field_high capPDPTMappedAddress 10
padding 48
}
block pml4_cap(capPML4MappedASID, capPML4BasePtr, capType, capPML4IsMapped) {
@ -144,10 +144,10 @@ block io_page_table_cap (capType, capIOPTIsMapped, capIOPTLevel, capIOPTMappedAd
field_high capIOPTBasePtr 48
field capType 5
padding 6
padding 5
field capIOPTIsMapped 1
field capIOPTLevel 4
field_high capIOPTMappedAddress 48
field_high capIOPTMappedAddress 49
}
block vcpu_cap {
@ -163,8 +163,8 @@ block ept_pt_cap (capType, capPTMappedAddress, capPTIsMapped, capPTMappedASID, c
field capType 5
field capPTIsMapped 1
padding 10
field_high capPTMappedAddress 27
padding 9
field_high capPTMappedAddress 28
field capPTMappedASID 16
padding 5
}
@ -175,8 +175,8 @@ block ept_pd_cap (capType, capPDMappedAddress, capPDIsMapped, capPDMappedASID, c
field capType 5
field capPDIsMapped 1
padding 10
field_high capPDMappedAddress 19
padding 9
field_high capPDMappedAddress 20
field capPDMappedASID 16
padding 13
}
@ -187,8 +187,8 @@ block ept_pdpt_cap (capType, capPDPTMappedAddress, capPDPTIsMapped, capPDPTMappe
field capType 5
field capPDPTIsMapped 1
padding 10
field_high capPDPTMappedAddress 17
padding 9
field_high capPDPTMappedAddress 18
field capPDPTMappedASID 16
padding 15
}

36
include/object/structures_64.bf
View file

@ -24,8 +24,8 @@ block untyped_cap {
field capBlockSize 6
field capType 5
padding 11
field_high capPtr 48
padding 10
field_high capPtr 49
}
block endpoint_cap(capEPBadge, capType, capCanGrant, capCanSend, capCanReceive,
@ -46,8 +46,8 @@ block notification_cap {
field capType 5
field capNtfnCanReceive 1
field capNtfnCanSend 1
padding 9
field_high capNtfnPtr 48
padding 8
field_high capNtfnPtr 49
}
block reply_cap(capReplyMaster, capTCBPtr, capType) {
@ -82,8 +82,8 @@ block thread_cap {
padding 64
field capType 5
padding 11
field_high capTCBPtr 48
padding 10
field_high capTCBPtr 49
}
block irq_control_cap {
@ -122,31 +122,31 @@ block domain_cap {
block endpoint {
field epQueue_head 64
padding 16
field_high epQueue_tail 46
padding 15
field_high epQueue_tail 47
field state 2
}
-- Async endpoint: size = 32 bytes
block notification {
padding 16
field_high ntfnBoundTCB 48
padding 15
field_high ntfnBoundTCB 49
field ntfnMsgIdentifier 64
padding 16
field_high ntfnQueue_head 48
padding 15
field_high ntfnQueue_head 49
field_high ntfnQueue_tail 48
padding 13
field_high ntfnQueue_tail 49
padding 12
field bound 1
field state 2
}
-- Mapping database (MDB) node: size = 16 bytes
block mdb_node {
padding 16
field_high mdbNext 46
padding 15
field_high mdbNext 47
field mdbRevocable 1
field mdbFirstBadged 1
@ -299,7 +299,7 @@ block thread_state(blockingIPCBadge, blockingIPCCanGrant, blockingIPCIsCall,
field blockingIPCDiminishCaps 1
field tcbQueued 1
padding 16
field_high blockingObject 44
padding 15
field_high blockingObject 45
field tsType 4
}