> So a solution would be to pad and align the data structure to be a
> multiple of 16MiB or you could declare the backing dataport to be a
> 64MiB sized buffer and then cast it to be whatever you want in the C
> source code. E.g.
>
> component Foo {
> dataport Buf(67108864) bar;
> }
>
We're going to be putting out a patch to be fixing this issue instead.
The patch will change it so that instead of rounding up to a multiple
of 4K all the time, it will be rounded up to a larger page size if the
buffer's size is a multiple of that larger page size.
Sincerely,
Damon
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel
