sel4 / sel4_libs Goto Github PK

(Imported from https://sel4.atlassian.net/browse/SELFOUR-2440)
It directly assumes it is managing a sel4 userlevel virtual address space with a kernel window at the top and rejects any mappings that would normally fall into the kernel window, but isn't a valid constraint for guests. So on ia32 trying to create devices above 0xe0000000 in the guest fails.

Commit 9152ea9 introduced a generic sel4utils_elf_get_section() function and made sel4utils_elf_get_vsyscall() a wrapper for it.

Prior to this commit, the result of elf_getSectionNamed() was compared to NULL before it was dereferenced:

After the change, the pointer is dereferenced regardless of whether it is NULL, leading to a crash if the section is not present:

There is still an attic branch 'spdx' in this repo. It should be deleted, all this seem to be merged by now.

I'm so confused that when I try to use open() as I did in Linux but it seems like the open() call only supports O_RDONLY.
Is there a way to do normal read and write like in Linux? What library should i look at? Or do I need to implement it manually?

ARMv7 currently disables cycle counters while reading the cycle counter values. If the task reading the values is preempted during the read than all time during the preemption is not included in the cycle counts.

Fix needed should be similar to #32

Is this code considered production ready?

My main interest in seL4 comes from potential use as a general purpose microhypervisor in highly dynamic systems.

I get the following compiler warning in libsel4debug. I'm not sure the write fix, presumably simply using %ld will cause errors on other platforms.

/home/benno/sel4test2/projects/seL4_libs/libsel4debug/src/caps.c: In function ‘debug_cap_identify’:
/home/benno/sel4test2/projects/seL4_libs/libsel4debug/src/caps.c:19:57: warning: format ‘%d’ expects argument of type ‘int’, but argument 2 has type ‘seL4_CPtr {aka long unsigned int}’ [-Wformat=]
     printf("DEBUG_BUILD not set, can't get type of cap %d", cap);
                                                        ~^
                                                        %ld

See my pull request #19 why this would be a useful. Is there a ways that parts of it could be made available in the seL4 API headers?

hi
In sync_cv_broadcast_release it will call sync_bin_sem_post before seL4_Signal.
But In sync_cv_wait, sync_bin_sem_wait(lock) is called after seL4_Wait,
when call sync_bin_sem_post in sync_cv_broadcast_release, it will make "lock->value == 2", it will make sync_bin_sem_bare_post trigger assert " assert(*value <= 1)"

static inline int sync_bin_sem_bare_post(seL4_CPtr notification, volatile int *value) { /* We can do an "unsafe" increment here because we know we are the only * lock holder. */ int val = sync_atomic_increment(value, __ATOMIC_RELEASE); assert(*value <= 1); // if (val <= 0) { seL4_Signal(notification); } return 0; }
I do not this function can work for performance reasons

It seems the commit from the branch df-public (https://github.com/seL4/seL4_libs/tree/df-public) has been merged at 7501c84, so the branch should be moved there or deleted.

hello:
i found a memory leak bug in libsel4utils/src/elf.c

static int load_segment(vspace_t *loadee_vspace, vspace_t *loader_vspace,
                        vka_t *loadee_vka, vka_t *loader_vka,
                        const char *src, size_t file_size, int num_regions,
                        sel4utils_elf_region_t regions[num_regions], int region_index)
{
    seL4_CPtr loader_slot;
    cspacepath_t loader_frame_cap;

    error = vka_cspace_alloc(loader_vka, &loader_slot);   // [1]
    while (pos < segment_size && error == seL4_NoError) {
        reservation_t reservation;
        if (loadee_vaddr < region.reservation_vstart) {
            if ((region_index - 1) < 0) {
                ZF_LOGE("Invalid regions: bad elf file.");
                return 1;                                                            // [2]
            }
}

if [2] happned, it not free the prev alloc memory, and then it's memory
will be leaked.
i think the correct way is invoke vka_cspace_free() before return.

seL4/seL4@5b611a0 from @bennoleslie added basic support for the Cortex-A35. We need a libsel4bench/arch_include/arm/cpu/cortex-a35/sel4bench/cpu/events.h then also.
Maybe we can just copy the Cortex A72 file that #27 adds.
Note that as long as libsel4bench is not used on an Cortex-A35 platform, there is no problem. However, when using the CAmkES global components, one can't cherry-pick things there. BenchUtiliz is always built (even if not used) and this pulls in libsel4bench then, which triggers an error then that the file is missing.

(Imported from https://sel4.atlassian.net/browse/SELFOUR-2421)
When a process is configured to use 2 level page table the following occurs:

error = sel4utils_configure_process(&p_app->process, &vka, &vspace, image_name)

Fails with.

<<seL4(CPU 0) [decodeCNodeInvocation/111 T0xffffff801ffca400 "host" @421b31]: CNode Copy/Mint/Move/Mutate: Sourc>
host: [email protected]:137 Failed to copy cap
Assertion failed: slot == SEL4UTILS_SCHED_CONTEXT_SLOT (../projects/seL4_libs/libsel4utils/src/process.c: sel4ut)
seL4 root server abort()ed
Debug halt syscall from user thread 0xffffff801ffca400 "host"

(Moved from https://sel4.atlassian.net/browse/SELFOUR-2429)
A vspace_t manages memory allocations for a virtual address space and also handles mapping frames into these allocations.

libsel4utils provides a vspace implementation that can be bootstrapped within an existing address space (self-hosted) or alternatively manage a different vspace (as a loader). In both cases it must perform internal book keeping. In the self-hosted case there is a circular dependency for memory allocation that may need to extend the virtual address space. To handle this the implementation performs it's own memory management, IE it will allocate new book keeping memory by mapping some new pages in itself.

The issue is that it also tries to do this when allocating book-keeping data for a different vspace. Therefore in order to create a vspace for a different address space you must have an existing vspace for your current address space just to perform memory allocation for book keeping data. It would be great to be able to create a vspace that just uses malloc or an alternative memory allocator for its book keeping data.