Devel

devel@sel4.systems

20 participants
1383 discussions

root task executable memory changed
by Leonid Meyerovich 08 Feb '24

08 Feb '24

Hello, I have a seL4 project that creates a number of processes with multiple threads. An application works fine. Every process periodically calculates the checksum of the executable segment and the system (Monitor process) keeps track that these values should be the same over the time. Some time when I change (add) some code in amu process I have an error that Monitor process prints CHECKSUM ERROR -------- Someone modified executable memory process=Startup 0x400000 8868997 last->10daf436f961b809 this->95ebd3119aee7736!!!! It always complains about the root (Startup) task. Checksum value changes every time the Startup process calculates it. The code that calculate executable segment are: typedef struct { unsigned char e_ident[EI_NIDENT]; /* Magic number and other info */ Elf64_Half e_type; /* Object file type */ Elf64_Half e_machine; /* Architecture */ Elf64_Word e_version; /* Object file version */ Elf64_Addr e_entry; /* Entry point virtual address */ Elf64_Off e_phoff; /* Program header table file offset */ Elf64_Off e_shoff; /* Section header table file offset */ Elf64_Word e_flags; /* Processor-specific flags */ Elf64_Half e_ehsize; /* ELF header size in bytes */ Elf64_Half e_phentsize; /* Program header table entry size */ Elf64_Half e_phnum; /* Program header table entry count */ Elf64_Half e_shentsize; /* Section header table entry size */ Elf64_Half e_shnum; /* Section header table entry count */ Elf64_Half e_shstrndx; /* Section header string table index */ } Elf64_Ehdr; extern char __executable_start[]; // function returns executable segment start address and size int initStartupElfSegsParams(Elf64_Ehdr *pELFHeader, uintptr_t *startAddr, uintptr_t *size) { seL4_Word phoff = pELFHeader->e_phoff; Elf_Phdr *currentPH = (Elf_Phdr *)((void *)pELFHeader + phoff); for (int i=0; i<pELFHeader->e_phnum; i++) { ZF_LOGD("ELF: p_type=%x p_flags=%x p_vaddr=%p p_memsz=%lu", currentPH[i].p_type, currentPH[i].p_flags, (void *)currentPH[i].p_vaddr, currentPH[i].p_memsz); if ( ((currentPH[i].p_type & 1) == 1) && ((currentPH[i].p_flags & 1) == 1)) // p_flags & 1 == 1 - executable { *startAddr = (uintptr_t)currentPH[i].p_vaddr; *size = (uintptr_t)currentPH[i].p_memsz / sizeof(uint64_t); return 0; } } return -1; }; initStartupElfSegsParams((Elf64_Ehdr *)__executable_start, &proc_validate_params[STARTUP_INDEX].p_addr, &proc_validate_params[STARTUP_INDEX].p_size); Any help will be appreciated. Thanks

2 6

Reminder seL4 developer hangout
by Birgit Brecknell 05 Feb '24

05 Feb '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Feb 7, 6pm For your time zone, please see the calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Birgit Brecknell Project Coordinator, seL4 Foundation birgit(a)sel4.systems<mailto:birgit@sel4.systems> birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> Mon 9am-5pm Wed 2pm-5pm Fri 9am-5pm

1 0

fault processing
by Leonid Meyerovich 27 Jan '24

27 Jan '24

I am working on fault processing. When I am a fault I am calling void sel4utils_print_fault_message(seL4_MessageInfo_t tag, const char *thread_name) from sel4libsutils library I have tested it for "page fault" condition and it works fine - I am getting seL4_Fault_VMFault fault type But in certain case I have got seL4_Fault_VCPUFault type, which is not implemented sel4libsutils library I try to process this fault similar to seL4_Fault_VMFault to get all neccessary registers, but the kernel does not have functions like seL4_Fault_VCPUFault_get_IP. What is the message format for VCPU fault? Thanks

2 3

seL4 fault processing
by Leonid Meyerovich 25 Jan '24

25 Jan '24

My root task (root thread created by kernel) checks for fault from the other threads, which are created in root thread with badged fault_ep seL4_Word badge; seL4_MessageInfo_t messageInfo = seL4_NBRecv(init_objects.fault_cap, &badge); if (seL4_MessageInfo_get_label(messageInfo) != seL4_Fault_NullFault ) { process_fault(messageInfo, badge); } Normally I don't have any faults, but every time I have seL4_MessageInfo_get_label(messageInfo) == 4, which is not in seL4_Fault_tag enumeration type enum seL4_Fault_tag { seL4_Fault_NullFault = 0, seL4_Fault_CapFault = 1, seL4_Fault_UnknownSyscall = 2, seL4_Fault_UserException = 3, seL4_Fault_VMFault = 5, seL4_Fault_VGICMaintenance = 6, seL4_Fault_VCPUFault = 7, seL4_Fault_VPPIEvent = 8 }; Could somebody explain? Thanks,

4 5

seL4 root task executable memory region
by Leonid Meyerovich 25 Jan '24

25 Jan '24

I assume that the code segment of the root task starts from __executable_start address. Does it point to ELF header? Or code starts directly from this address? Thank you,

1 0

seL4 fault handling
by Leonid Meyerovich 24 Jan '24

24 Jan '24

Hello, Where can I find a comprehensive description of fault message registers for every of the following faults enum seL4_Fault_tag { seL4_Fault_NullFault = 0, seL4_Fault_CapFault = 1, seL4_Fault_UnknownSyscall = 2, seL4_Fault_UserException = 3, seL4_Fault_VMFault = 5, seL4_Fault_VGICMaintenance = 6, seL4_Fault_VCPUFault = 7, seL4_Fault_VPPIEvent = 8 }; Thanks, LM

3 3

Reminder seL4 developer hangout
by Birgit Brecknell 22 Jan '24

22 Jan '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Jan 24, 8am For your time zone, please see the calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Birgit Brecknell Project Coordinator, seL4 Foundation birgit(a)sel4.systems<mailto:birgit@sel4.systems> birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> Mon 9am-5pm Wed 2pm-5pm Fri 9am-5pm

1 0

Reminder seL4 developer hangout
by Gerwin Klein 09 Jan '24

09 Jan '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Jan 10, 6pm For your time zone, please see the calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 Cheers, Gerwin

1 0

CAmkES VMM custom OS
by Hugo V.C. 18 Dec '23

18 Dec '23

Hi all, I'm wondering if someone could forward me to the path I must follow to achieve booting a Hermit unikernel (https://github.com/hermit-os/hermit-rs) via CAmkES VMM. I know CAmkES VMM are "virtualised Linux guests on seL4 for ARM and x86 platforms" but I think that being able to boot a Rust based unikernel opens the door to a fascinating World... (no more dependency on "fat/buggy" Linux kernel). Any help where I need to start? Does it require to modify CAmkES VMM to add such functionality? Best,

2 2

get interrupts in x86
by os.team.1992＠gmail.com 14 Dec '23

14 Dec '23

Hi I am trying to run linux OS on camkes seL4 hypervisor. The hardware I use is x86-64. But I do not receive the interrupts from the devices that I have passthrough, and Linux is managing the interrupts in the form of pooling. This problem exists at the kernel level. Where the IO/APIC settings should be applied to the system but are not applied correctly. Is this problem solved in internal versions? For example, physical interrupt 10 is defined for network hardware. Vector 58 is defined for this interval. The IO/APIC information used for this device is also specified. However, interrupts are not received correctly. (In fact, because the level trigger is set, interrupts are sent quickly, this is not true and causes a destructive effect on the performance of the guest OS)

1 0

← Newer
1
2
3
4
5
6
7
...
139
Older →

Jump to page:

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel