Hello Gerwin,
On 2024-09-24 08:24, Gerwin Klein wrote:
(Apart from the whole discussion whether the concept of untyped object
makes sense — for me, there are no untyped objects, only untyped caps
and allocatable memory, but with the uniqueness constraint it doesn’t
really matter, they are the
Hello Gerwin,
On 2024-09-23 12:58, Gerwin Klein wrote:
The other cap state is also not for
properties of the object the cap points to. That’s probably where
the main confusion is, because it sounds like object state. Maybe one
analogy is that it is state of a "view" of the object.
What does ma
Hi Gerwin,
Thanks for the answer.
On 2024-09-23 09:53, Gerwin Klein wrote:
While the manual currently is attempting to shortcut this difference
and mostly just talks about objects, I think it is important to make
the difference explicit even though it does sound cumbersome to spell
it out eac
Hello Hugo,
The thing is, to fully understand how things work on a low level you can
read the seL4 source, it's not that much, it's open and available to
everyone. And it's really the best way to find out specific details.
So the door is wide open already.
People are welcome to ask questions to
Hello T,
Great to hear it clicked!
Now that you understand this, I'd like to mention that seL4 kernel
"objects"
are not as clear-cut as they seem. This is currently not very well
explained
in the manual and only something you will run into when actually using
seL4,
mostly manifesting as pecu
Hello T,
"Object methods" are just system calls in the technical sense,
they are fully executed in kernel mode.
You can find the (generated) syscall numbers in your build directory:
build/libsel4/include/sel4/syscall.h
It's generated from libsel4/include/api/syscall.xml by a script.
The start
Hello Ben,
On 2024-09-05 01:12, Ben McCart wrote:
I have read the manual in section 9.2 about userImageFrames and how to
infer the virtual address range for the pages being used for the
userland image, which I frankly do not concretely understand. For
example, I can take the address of main()
Hello Liam,
On 2024-07-22 14:56, liam.vervec...@gmail.com wrote:
But it seems instead only the first thread gets scheduled, and it never
allows the second thread to get any CPU time.
This could happen if the port is broken and you don't get any timer
interrupts.
To verify if this is happeni
Hello David,
On 2024-06-05 15:40, David Martin wrote:
that sounds like a real plan for me to test tomorrow :)
and if I'm not mistaken, inside each kernel now, the function
"seL4_Untyped_Retype" should be called twice (one on each core)
pointing to the same "free memory" declared previously so it
Hello David,
On 2024-06-05 14:56, David Martin wrote:
If I'm not mistaken, that could be done using a chunk of memory
defined as device untyped and then used by each kernel (for my
tests, I'll use 2 harts) to write/read. --> Is that a good
understanding on how shared memory is suppose to be use
Hello Linh,
On 2024-05-11 00:36, Linh Pham wrote:
Our sel4test image is large because we're using a static heap. Note
that the relevant region from the log output is [262000..6cd7fff], the
exception occurs when trying to write into memory in this range. After
some investigation, writing to phy
ation. I have removed BOOT_BSS and it is booted
properly now
Thanks,
Leonid
On Fri, May 3, 2024 at 8:13 AM Indan Zupancic wrote:
Hello Leonid,
On 2024-04-25 21:37, Leonid Meyerovich wrote:
I run my seL4 application on 4 core ARMv8.
Still the new platform port I assume?
Recently I have d
Hello Leonid,
On 2024-04-25 21:37, Leonid Meyerovich wrote:
I run my seL4 application on 4 core ARMv8.
Still the new platform port I assume?
Recently I have developed some more application code (I mention it
because
file system size is increased an I believe it may change boot time) and
fro
Hello Hugo,
On 2024-04-19 13:59, Hugo V.C. wrote:
I talked about "vendors" in general. Never specified about any
particular vendor. It is a generalization.
The context was browsers, there are not many browser vendors.
Furthermore, you used it as an argument to propose your idea.
If you didn't
Hello Andrew,
On 2024-04-19 12:40, Andrew Warkentin wrote:
On Fri, Apr 19, 2024 at 4:22 AM Indan Zupancic wrote:
Because it is asynchronous: You do 10k system calls which queue some
data, QNX can do one context switch to the server to handle all 10k of
them in one go.
The client needs to
be a little bit
surprised if it were.
You're right it's not buffered in user space, but it is buffered
in kernel space though.
On Fri, Apr 19, 2024 at 3:12 AM Indan Zupancic wrote:
Yes, you are running it in a virtual machine, remember? Any timing is
suspect.
Wouldn't that affect timi
Hello Hugo,
On 2024-04-19 10:06, Hugo V.C. wrote:
1) Let's forget the naive idea of users changing behavior or vendors
making
secure software. Users are "ignorant" and vendors are unethical. That's
raw
reality.
Both Chromium and Firefox are open-source. Calling Mozilla and all the
volunteers
Hello Andrew,
On 2024-04-19 05:00, Andrew Warkentin wrote:
Here's the exact code for the benchmark loop I'm using on seL4:
void c_test_client(seL4_CPtr endpoint)
{
struct seL4_MessageInfo info = seL4_MessageInfo_new(0, 0, 0, 2);
int j;
for (j = 0; j < 1; j++){
seL4_Call(
Hello Leonid,
On 2024-03-28 20:18, Leonid Meyerovich wrote:
I run sel4test on the aarch64 platform.
What CPU are you testing on?
My CACHEFLUSH0001 test in sel4test failed
/* Clean makes data observable to non-cached page */
*ptr = 0xC0FFEE;
*ptrc = 0xDEADBEEF;
test_assert(*ptr == 0xC0FFEE);
Hello Jeff,
On 2024-03-08 19:17, Jeff wrote:
*Description:* Starting from the VSpace, map the page table object at
any unpopulated level
for the provided virtual address. If all paging structures and mappings
are present for
this virtual address, return an seL4_DeleteFirst error.
It says it m
Hello,
After some introspection, I sincerely apologise for my rude reply
yesterday.
I was tired and put off balance by all the discrepancies. I thought the
message was a stupid prank by students or something and acted
accordingly.
Even so, that does not excuse my behaviour. I should have sen
Hello Marc,
On 2024-02-09 20:14, i...@wolffgames.com wrote:
My name is Marc Wolff, currently located in Portland, Oregon, USA.
I'm CEO of Leyline Nexus, an R&D team primarily for game development,
but also some other things.
Would some of the "other things" be AI? Perchance training it via pu
Hello Leonid,
On 2024-02-07 20:19, Leonid Meyerovich wrote:
Yes I see all my other tasks have different flags for segment 0 - RE,
Startup flag is RWI
Is there any document that describes this limitation?
I don't think the ABI between the kernel and Elfloader/root task is
documented anywhere. O
Hello Leonid,
On 2024-02-07 18:15, Leonid Meyerovich wrote:
Using readelf helps, but I think there is some difference between
running readelf on the file and
parsing elf header in the memory (because my root process is already
in the memory)
As you can see below size of executable segment is dif
Hello Leonid,
On 2024-02-06 19:48, Leonid Meyerovich wrote:
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
0x40 8868997 last->10daf436f961b809 this->95ebd3119a
Hello Leonid,
On 2024-01-26 16:35, Leonid Meyerovich wrote:
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
Hello Leonid,
On 2024-01-24 21:16, Leonid Meyerovich wrote:
I don't have any faults if I use seL4_Recv instead (in a separate
thread).
It happens only if I use seL4_NBRecv and check the tag after it
returns.
If there is no message or fault pending, seL4_NBRecv() will return
immediately.
W
Hello,
On 2023-12-05 11:40, chenpingyuan--- via Devel wrote:
Thanks Indan for your detail reply.
By ready queue, I did mean the scheduling queue since the code named it
as ksReadyQueues.
Oh, good, I wasn't sure any more.
For threads unbound from a SC, this thread will be removed from both
Hello,
On 2023-12-05 01:47, chenpingyuan--- via Devel wrote:
By saying " threads that are blocked waiting in an endpoint or
notification queue will remain in the queue and can still recieve
messages and signals.", does it mean that those threads blocked waiting
in an endpoint or notification q
Hello,
On 2023-12-04 13:18, chenpingyuan--- via Devel wrote:
Still one thing to confirm: Threads which are blocked waiting for
notification/endpoint without schedule context will remain in the ready
queue, right?
It does not matter whether the thread returns a scheduling context,
when it bloc
Hello,
On 2023-12-01 03:23, chenpingyuan--- via Devel wrote:
When the notification status is NtfnState_Active, the kernel will try
to donate the notification's schedule context to the thread by calling
maybeDonateSchedContext.
My confusion point is that: If the thread doesn't have a valid sched
Hello Hesham,
On 2023-11-22 14:48, Hesham Almatary wrote:
Cheers! Is there an FVP command line showing how to boot u-boot
itself with any additional required flags?
Follow FVP's documentation for that:
https://developer.arm.com/documentation/100966/1123/Getting-Started-with-Fixed-Virtual-Plat
Hello Hesham,
On 2023-11-22 14:18, Hesham Almatary wrote:
I can build sel4test for FVP, how do I run it there? I couldn't find
any documentation on that, would be great if someone could drop a
command line and any required dependencies.
This page may be helpful:
https://docs.sel4.systems/Hard
On 2023-11-09 01:11, chenpingyuan--- via Devel wrote:
And will interrupts be enabled again automatically after exiting
trapping?
(Is this done automatically by the CPU? So invisible from the source
code.)
That depends on the platform, but usually yes, as the hardware state is
restored to what
Hello Chen Ping Yuan,
On 2023-11-08 13:16, chenpingyuan--- via Devel wrote:
But I didn't find the code which disabled interrupts when entering
kernel mode, for example, when a syscall is triggered.
Interrupts are disabled automatically when trapping, so there is no need
to explicitly do that.
Hello Jason,
On 2023-08-21 23:46, Jason Long via Devel wrote:
Hello,I want to learn seL4 deeply. So that I can figure it out
and develop it. Where should I start?
Start with:
https://sel4.systems/Learn/
https://sel4.systems/Info/Docs/seL4-manual-latest.pdf
Greetings,
Indan
_
Hello Sid,
On 2023-08-08 05:20, Sid Agrawal wrote:
1. Looking at the DTS files for tqma8xqp-1gb in the seL4 repo. I see
one big file and another overlay. Why are there two for the same
board? I would have understood if one was for the SoC and another
for the board.
- tools/dts/tqma8xqp1gb.dts
-
Hello Sid,
On 2023-08-05 02:47, Sid Agrawal wrote:
I have a rspi4 and a Toradex Colibri iMX8X module with the aster
carrier
board. This Toradex has the same SoC ( iMX8X) as the tqma8xqp-1gb
mentioned
on the sel4cp website. Do you folks have any thoughts on how much
effort it
is getting seL4 wo
Hello Sid,
On 2023-08-05 03:05, Sid Agrawal wrote:
I have a scenario and would like to understand how the kernel is
expected
to behave when I change the CSpace of a TCB when it is blocked on an
EP.
CSpace matters when system calls are done. That is, all access checks
are
done at the start o
Hello,
I had the same issue and solved it by installing gcc-riscv64-unknown-elf
instead of gcc-riscv64-linux-gnu.
Hope that helps,
Indan
On 2023-07-13 09:48, suebox...@gmail.com wrote:
Hi, I met a problem when building seL4test project with riscv
toolchain, with the float operations compiled
Hello Li,
On 2023-05-30 05:06, yadong.li wrote:
I have one question about sel4 kernel preemptionPoint on smp
platform such as ARMv8.
Take an example, when kernel takes long time to clear memory
when UntypedRetype kernel object on core1, it will check
preemptionPoint,
when pending
Hello,
On 2023-03-11 10:56, Sam Leffler via Devel wrote:
I've got a stress test that forces lots of memory recycling by
creating,
running & tearing down applications. I repeatedly see a particular
point
in the test (after memory starts being recycled) where an app gets an
instruction fault. Na
Hello,
Just replying to what would be, for me, unexpected behaviour:
On 2022-09-14 11:54, Gerwin Klein wrote:
On 13 Sep 2022, at 7:01 pm, Demi Marie Obenour wrote:
It is. An PPC callee is allowed to block for as long as it desires,
and doing so will block the caller too. There is no way (that
Hello Williams,
On 2022-06-09 17:10, WILLIAMS Stephen via Devel wrote:
Any suggestions as to the possible cause of the page fault or hints on
how to progress with debugging this issue would be greatly
appreciated.
Although we don't use camkes' VMM, we had to change our VMM for recent
Linux ker
Hello Williams,
On 2022-06-09 17:10, WILLIAMS Stephen via Devel wrote:
We’re currently working on formalising VM support for an iMX8 platform
(the Avnet MaaXBoard) building upon the existing sylvain/imx8 and
sylvain/gicv3 branches.
Mainline seL4 already has support for maaxboard.
AFAIK only t
Hello Sid,
On 2022-04-30 20:23, Sid Agrawal wrote:
I can hand out badged EP of the same original endpoint to all the
server's
clients. Now unwrapping will reveal the badge of any badged EP cap
since
they are badged versions of the EP via which the message arrives.
How is this different than
Hello Peter,
On 2022-04-08 11:43, wtliang785 via Devel wrote:
My question is that what is the status for supporting the v3
virtulization in lastest sel4 kernel master branch?
Does the lastest master branch support gic v3 virtulization?
Yes, since 3 September 2021, see:
https://github.com/seL
Hi Zippy,
On 2021-12-14 15:32, Zippy Manaic via Devel wrote:
Firstly I have to add "set(KernelAArch64SErrorIgnore ON)" to my build
config in order to get the tests running and unfortunately things go
awry during the test run
Sadly, since commit 7b0602c5 setting KernelAArch64SErrorIgnore must b
Hello Michael,
On 2021-10-19 22:46, Michael Neises wrote:
I want to be able to retrieve data from seL4's virtual
Linux machine, in order to store it in a persistent way.
[...]
If you have a different idea how I might achieve my goal,
I would be similarly effusive in my thanks.
If it is just
Hi Alex,
On 2021-07-08 23:56, Alex Ling wrote:
Do you know if anyone is working on GICv3 support in libsel4vm? Thanks.
I don't know, but I'm not an insider, sorry.
We're not using CAmkES, nor libsel4vm ourselves.
Good luck,
Indan
___
Devel mailing
Hello, Alex
On 2021-07-08 11:01, alex.lin wrote:
What is the status of virtualization support on ARM SOCs with GICv3?
According to section “FAQ and Implementation Notes” of [1], seems it
is still under development. Any plan or progress on this? Thank you
very much.
Second attempt to get it mer
Hello,
On 2021-05-27 13:43, Indan Zupancic wrote:
I'll just create a Github account, that is the easiest solution
long-term.
Seems like I already had an old Github account laying around.
There is exists an issue about SError handling, so I just added a
comment there instead of creating
Hello,
On 2021-05-26 23:24, Axel Heider wrote:
GitHub offers a convenient platform here. So I wonder, what is
preventing
you from creating an account there and doing pull requests?
In the past I had DNS based ad/tracking filtering and that utterly
broke the Github website. Since then I have a
Hello,
By default any SError interrupt will halt the kernel.
SErrors may be caused by e.g. writes to read-only device registers or
ECC errors.
With this patch SErrors can instead be reported as a VM data fault for
the
currently running task. Because SError is asynchronous it is not assured
Hello,
On 2020-12-03 03:51, Andrew Warkentin wrote:
On 12/2/20, Indan Zupancic [] wrote:
Please don't quote full e-mail addresses on public mailing lists,
bots can find those.
The main problem is that you don't want VM user space to block
the whole VM by doing a blocking
Hello,
On 2020-12-02 05:07, Andrew Warkentin wrote:
support for (presumably limited) direct system calls from VMs,
bypassing any user-mode VMM (using something like Xen's trampoline
page) wouldn't be accepted into seL4?
Actually, at least for ARM64, it seems you can already do seL4
system call
56 matches
Mail list logo
