Skip to content

Fix RPi4 failing sel4test in Release mode #150

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Indanz merged 3 commits into from
Dec 5, 2025
Merged

Fix RPi4 failing sel4test in Release mode #150

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
916789f
Fix RPi4 failing sel4test in Release mode
JDuchniewicz Dec 4, 2025
e5365af
Address review comments
JDuchniewicz Dec 4, 2025
85cd708
Fix missing rename changes
JDuchniewicz Dec 5, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 7 additions & 6 deletions apps/sel4test-driver/src/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -484,10 +484,11 @@ void *main_continued(void *arg UNUSED)

/* Note that the following globals are place here because it is not expected that
* this function be refactored out of sel4test-driver in its current form. */
/* Number of objects to track allocation of. Currently all serial devices are
* initialised with a single Frame object. Future devices may need more than 1.
/* Number of objects to track allocation of. Currently all serial devices but
* bcm2711 and bcm2837 are initialised with a single Frame object. In future
* devices some other devices may need more than two, so keep some margin.
*/
#define NUM_ALLOC_AT_TO_TRACK 1
#define MAX_ALLOC_AT_TO_TRACK 4
/* Static global to store the original vka_utspace_alloc_at function. It
* isn't expected for this to dynamically change after initialisation.*/
static vka_utspace_alloc_at_fn vka_utspace_alloc_at_base;
Expand All @@ -503,15 +504,15 @@ typedef struct uspace_alloc_at_args {
cspacepath_t dest;
} uspace_alloc_at_args_t;
/* This instance of vka_utspace_alloc_at_fn will keep a record of allocations up
* to NUM_ALLOC_AT_TO_TRACK while serial_utspace_record is set. When serial_utspace_record
* to MAX_ALLOC_AT_TO_TRACK while serial_utspace_record is set. When serial_utspace_record
* is unset, any allocations matching recorded allocations will instead copy the cap
* that was originally allocated. These subsequent allocations cannot be freed using
* vka_utspace_free and instead the caps would have to be manually deleted.
* Freeing these objects via vka_utspace_free would require also wrapping that function.*/
static int serial_utspace_alloc_at_fn(void *data, const cspacepath_t *dest, seL4_Word type, seL4_Word size_bits,
uintptr_t paddr, seL4_Word *cookie)
{
static uspace_alloc_at_args_t args_prev[NUM_ALLOC_AT_TO_TRACK] = {};
static uspace_alloc_at_args_t args_prev[MAX_ALLOC_AT_TO_TRACK] = {};
static size_t num_alloc = 0;

ZF_LOGF_IF(!vka_utspace_alloc_at_base, "vka_utspace_alloc_at_base not initialised.");
Expand All @@ -525,7 +526,7 @@ static int serial_utspace_alloc_at_fn(void *data, const cspacepath_t *dest, seL4
}
return vka_utspace_alloc_at_base(data, dest, type, size_bits, paddr, cookie);
} else {
ZF_LOGF_IF(num_alloc >= NUM_ALLOC_AT_TO_TRACK, "Trying to allocate too many utspace objects");
ZF_LOGF_IF(num_alloc >= MAX_ALLOC_AT_TO_TRACK, "Trying to allocate too many utspace objects");
int ret = vka_utspace_alloc_at_base(data, dest, type, size_bits, paddr, cookie);
if (ret) {
return ret;
Expand Down