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

libsel4: deprecate old seL4_UserTop constant

Browse source 
This value was inconsistent across platforms, and one
should use seL4_UserVSpaceTop instead.

Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
This commit is contained in:
Julia Vassiliki 2026-06-30 15:25:10 +10:00 committed by Julia
parent dbc3da9d97
commit c8526a426f
25 changed files with 26 additions and 25 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
CHANGES.md
View file

@ -34,6 +34,7 @@ description indicates whether it is SOURCE-COMPATIBLE, BINARY-COMPATIBLE, or BRE
the highest available address available to user level. The existing constant
`seL4_UserTop` is a mix of inclusive and exclusive across existing platforms, however,
changing this to be consistent would break userspace and require proof updates.
The existing `seL4_UserTop` define is deprecated.
### Platforms

4
libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/constants.h
View file

@ -243,7 +243,7 @@ SEL4_SIZE_SANITY(seL4_VSpaceEntryBits, seL4_VSpaceIndexBits, seL4_VSpaceBits);
* Anything address above the range above triggers an
* address size fault.
*/
/* Last address in the virtual address space that is accessible to user level */
/* (Deprecated) Last address in the virtual address space that is accessible to user level */
#if defined(CONFIG_ARM_PA_SIZE_BITS_44)
#define seL4_UserTop 0x00000fffffffffff
#elif defined(CONFIG_ARM_PA_SIZE_BITS_40)
@ -253,7 +253,7 @@ SEL4_SIZE_SANITY(seL4_VSpaceEntryBits, seL4_VSpaceIndexBits, seL4_VSpaceBits);
#endif
#else
/* Last address in the virtual address space that is accessible to user level */
/* (Deprecated) Last address in the virtual address space that is accessible to user level */
#define seL4_UserTop 0x00007fffffffffff
#endif

2
libsel4/sel4_arch_include/ia32/sel4/sel4_arch/constants.h
View file

@ -143,7 +143,7 @@ typedef enum {
/* IPC buffer is 512 bytes, giving size bits of 9 */
#define seL4_IPCBufferSizeBits 9
/* First address in the virtual address space that is not accessible to user level */
/* (Deprecated) First address in the virtual address space that is not accessible to user level */
#define seL4_UserTop 0xe0000000
/* Last address in the virtual address space that is accessible to user level */

2
libsel4/sel4_arch_include/riscv32/sel4/sel4_arch/constants.h
View file

@ -124,7 +124,7 @@ typedef enum {
#endif
#endif /* __ASSEMBLER__ */
/* First address in the virtual address space that is not accessible to user level */
/* (Deprecated) First address in the virtual address space that is not accessible to user level */
#define seL4_UserTop 0x80000000lu
/* Last address in the virtual address space that is accessible to user level */

2
libsel4/sel4_arch_include/riscv64/sel4/sel4_arch/constants.h
View file

@ -125,7 +125,7 @@ typedef enum {
#endif
#endif /* __ASSEMBLER__ */
/* First address in the virtual address space that is not accessible to user level */
/* (Deprecated) First address in the virtual address space that is not accessible to user level */
#define seL4_UserTop 0x0000003ffffff000
/* Last address in the virtual address space that is accessible to user level */

2
libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/constants.h
View file

@ -153,7 +153,7 @@ typedef enum {
/* IPC buffer is 1024 bytes, giving size bits of 10 */
#define seL4_IPCBufferSizeBits 10
/* First address in the virtual address space that is not accessible to user level */
/* (Deprecated) First address in the virtual address space that is not accessible to user level */
#define seL4_UserTop 0x00007ffffffff000
/* Last address in the virtual address space that is accessible to user level */

2
libsel4/sel4_plat_include/allwinnerA20/sel4/plat/api/constants.h
View file

@ -9,7 +9,7 @@
#include <sel4/config.h>
#include <sel4/arch/constants_cortex_a7.h>
/* First address in the virtual address space that is not accessible to user level */
/* (Deprecated) First address in the virtual address space that is not accessible to user level */
#define seL4_UserTop 0xa0000000
/* Last address in the virtual address space that is accessible to user level */

2
libsel4/sel4_plat_include/am335x/sel4/plat/api/constants.h
View file

@ -9,7 +9,7 @@
#include <sel4/config.h>
#include <sel4/arch/constants_cortex_a8.h>
/* First address in the virtual address space that is not accessible to user level */
/* (Deprecated) First address in the virtual address space that is not accessible to user level */
#define seL4_UserTop 0xe0000000
/* Last address in the virtual address space that is accessible to user level */

2
libsel4/sel4_plat_include/apq8064/sel4/plat/api/constants.h
View file

@ -9,7 +9,7 @@
#include <sel4/config.h>
#include <sel4/arch/constants_cortex_a15.h>
/* First address in the virtual address space that is not accessible to user level */
/* (Deprecated) First address in the virtual address space that is not accessible to user level */
#define seL4_UserTop 0xe0000000
/* Last address in the virtual address space that is accessible to user level */

2
libsel4/sel4_plat_include/bcm2711/sel4/plat/api/constants.h
View file

@ -11,7 +11,7 @@
#include <sel4/arch/constants_cortex_a72.h>
#if CONFIG_WORD_SIZE == 32
/* First address in the virtual address space that is not accessible to user level */
/* (Deprecated) First address in the virtual address space that is not accessible to user level */
#define seL4_UserTop 0xa0000000
/* Last address in the virtual address space that is accessible to user level */

2
libsel4/sel4_plat_include/bcm2837/sel4/plat/api/constants.h
View file

@ -11,7 +11,7 @@
#include <sel4/arch/constants_cortex_a53.h>
#if CONFIG_WORD_SIZE == 32
/* First address in the virtual address space that is not accessible to user level */
/* (Deprecated) First address in the virtual address space that is not accessible to user level */
#define seL4_UserTop 0xe0000000
/* Last address in the virtual address space that is accessible to user level */

2
libsel4/sel4_plat_include/exynos4/sel4/plat/api/constants.h
View file

@ -9,7 +9,7 @@
#include <sel4/config.h>
#include <sel4/arch/constants_cortex_a9.h>
/* First address in the virtual address space that is not accessible to user level */
/* (Deprecated) First address in the virtual address space that is not accessible to user level */
#define seL4_UserTop 0xe0000000
/* Last address in the virtual address space that is accessible to user level */

2
libsel4/sel4_plat_include/exynos5/sel4/plat/api/constants.h
View file

@ -22,7 +22,7 @@
#error "unsupported core"
#endif
/* First address in the virtual address space that is not accessible to user level */
/* (Deprecated) First address in the virtual address space that is not accessible to user level */
#define seL4_UserTop 0xe0000000
/* Last address in the virtual address space that is accessible to user level */

2
libsel4/sel4_plat_include/hikey/sel4/plat/api/constants.h
View file

@ -11,7 +11,7 @@
#include <sel4/arch/constants_cortex_a53.h>
#if CONFIG_WORD_SIZE == 32
/* First address in the virtual address space that is not accessible to user level */
/* (Deprecated) First address in the virtual address space that is not accessible to user level */
#define seL4_UserTop 0xe0000000
/* Last address in the virtual address space that is accessible to user level */

2
libsel4/sel4_plat_include/imx6/sel4/plat/api/constants.h
View file

@ -9,7 +9,7 @@
#include <sel4/config.h>
#include <sel4/arch/constants_cortex_a9.h>
/* First address in the virtual address space that is not accessible to user level */
/* (Deprecated) First address in the virtual address space that is not accessible to user level */
#define seL4_UserTop 0xe0000000
/* Last address in the virtual address space that is accessible to user level */

2
libsel4/sel4_plat_include/imx7/sel4/plat/api/constants.h
View file

@ -9,7 +9,7 @@
#include <sel4/config.h>
#include <sel4/arch/constants_cortex_a7.h>
/* First address in the virtual address space that is not accessible to user level */
/* (Deprecated) First address in the virtual address space that is not accessible to user level */
#define seL4_UserTop 0xe0000000
/* Last address in the virtual address space that is accessible to user level */

2
libsel4/sel4_plat_include/imx8mm-evk/sel4/plat/api/constants.h
View file

@ -10,7 +10,7 @@
#include <sel4/arch/constants_cortex_a53.h>
#if CONFIG_WORD_SIZE == 32
/* First address in the virtual address space that is not accessible to user level */
/* (Deprecated) First address in the virtual address space that is not accessible to user level */
#define seL4_UserTop 0xe0000000
/* Last address in the virtual address space that is accessible to user level */

2
libsel4/sel4_plat_include/imx8mp-evk/sel4/plat/api/constants.h
View file

@ -10,7 +10,7 @@
#include <sel4/arch/constants_cortex_a53.h>
#if CONFIG_WORD_SIZE == 32
/* First address in the virtual address space that is not accessible to user level */
/* (Deprecated) First address in the virtual address space that is not accessible to user level */
#define seL4_UserTop 0xe0000000
/* Last address in the virtual address space that is accessible to user level */

2
libsel4/sel4_plat_include/imx8mq-evk/sel4/plat/api/constants.h
View file

@ -10,7 +10,7 @@
#include <sel4/arch/constants_cortex_a53.h>
#if CONFIG_WORD_SIZE == 32
/* First address in the virtual address space that is not accessible to user level */
/* (Deprecated) First address in the virtual address space that is not accessible to user level */
#define seL4_UserTop 0xe0000000
/* Last address in the virtual address space that is accessible to user level */

2
libsel4/sel4_plat_include/maaxboard/sel4/plat/api/constants.h
View file

@ -11,7 +11,7 @@
#include <sel4/arch/constants_cortex_a53.h>
#if CONFIG_WORD_SIZE == 32
/* First address in the virtual address space that is not accessible to user level */
/* (Deprecated) First address in the virtual address space that is not accessible to user level */
#define seL4_UserTop 0xe0000000
/* Last address in the virtual address space that is accessible to user level */

2
libsel4/sel4_plat_include/omap3/sel4/plat/api/constants.h
View file

@ -9,7 +9,7 @@
#include <sel4/config.h>
#include <sel4/arch/constants_cortex_a8.h>
/* First address in the virtual address space that is not accessible to user level */
/* (Deprecated) First address in the virtual address space that is not accessible to user level */
#define seL4_UserTop 0xf0000000
/* Last address in the virtual address space that is accessible to user level */

2
libsel4/sel4_plat_include/qemu-arm-virt/sel4/plat/api/constants.h
View file

@ -23,7 +23,7 @@
#if CONFIG_WORD_SIZE == 32
/* First address in the virtual address space that is not accessible to user level */
/* (Deprecated) First address in the virtual address space that is not accessible to user level */
#define seL4_UserTop CONFIG_USER_TOP
/* Last address in the virtual address space that is accessible to user level */

2
libsel4/sel4_plat_include/tk1/sel4/plat/api/constants.h
View file

@ -9,7 +9,7 @@
#include <sel4/config.h>
#include <sel4/arch/constants_cortex_a15.h>
/* First address in the virtual address space that is not accessible to user level */
/* (Deprecated) First address in the virtual address space that is not accessible to user level */
#define seL4_UserTop 0xe0000000
/* Last address in the virtual address space that is accessible to user level */

2
libsel4/sel4_plat_include/zynq7000/sel4/plat/api/constants.h
View file

@ -9,7 +9,7 @@
#include <sel4/config.h>
#include <sel4/arch/constants_cortex_a9.h>
/* First address in the virtual address space that is not accessible to user level */
/* (Deprecated) First address in the virtual address space that is not accessible to user level */
#define seL4_UserTop 0xe0000000
/* Last address in the virtual address space that is accessible to user level */

2
libsel4/sel4_plat_include/zynqmp/sel4/plat/api/constants.h
View file

@ -15,7 +15,7 @@
#include <sel4/arch/constants_cortex_a53.h>
#if CONFIG_WORD_SIZE == 32
/* First address in the virtual address space that is not accessible to user level */
/* (Deprecated) First address in the virtual address space that is not accessible to user level */
#define seL4_UserTop 0xe0000000
/* Last address in the virtual address space that is accessible to user level */