Subject: [seL4] TimeServer "IRQ already mapped" error
Maybe the irq of Time exist in vm and TimeServer meanwhile.
Try delete the tree node of time in your devices.camkes of you platform, like
this:
assembly {
vm0.dtb = dtb([{}]);
/*vm0.dtb = dtb([{"path": "/soc/serial@0xA5000000"}]);*/
-----only delete the conflict part
}
-----邮件原件-----
发件人: Devel [mailto:devel-bounces@sel4.systems] 代表 devel-request@sel4.systems
发送时间: 2020年4月10日 10:00
收件人: devel@sel4.systems
主题: Devel Digest, Vol 71, Issue 10
Send Devel mailing list submissions to
devel@sel4.systems
To subscribe or unsubscribe via the World Wide Web, visit
https://sel4.systems/lists/listinfo/devel
or, via email, send a message with subject or body 'help' to
devel-request@sel4.systems
You can reach the person managing the list at
devel-owner@sel4.systems
When replying, please edit your Subject line so it is more specific than "Re:
Contents of Devel digest..."
Today's Topics:
1. Re: setConsumed() in seL4_SchedContext_YieldTo
(=?utf-8?B?bGFva3o=?=)
2. TimeServer "IRQ already mapped" error (Grant Jurgensen)
----------------------------------------------------------------------
Message: 1
Date: Thu, 9 Apr 2020 19:11:14 +0800
From: "=?utf-8?B?bGFva3o=?=" <la...@foxmail.com>
To: "=?utf-8?B?QW5uYSBMeW9ucw==?=" <a...@gh.st>,
"=?utf-8?B?ZGV2ZWw=?=" <devel@sel4.systems>
Subject: Re: [seL4] setConsumed() in seL4_SchedContext_YieldTo
Message-ID: <tencent_c27271a3f0a40cf84a7fdbb4f299eb059...@qq.com>
Content-Type: text/plain; charset="utf-8"
Hello Anna,
With your point, I am cleared - activateThread() does the completeYieldTo
assurance before A yield to B again. Can I conclude that YieldTo() method is
limited to 1:1 relationship?
Thanks,
laokz
------------------ Original ------------------
From: "Anna Lyons"<a...@gh.st>;
Date: Thu, Apr 9, 2020 07:12 AM
To: "laokz"<la...@foxmail.com>;"devel"<devel@sel4.systems>;
Subject: Re: [seL4] setConsumed() in seL4_SchedContext_YieldTo
P {margin-top:0;margin-bottom:0;} Hi laokz,
Yes, that scenario cannot happen. If B runs to block, and A is scheduled, the
kernel will complete A's initial yieldTo call and clear the appropriate values
before resuming A.
Cheers
Anna.
From: laokz <la...@foxmail.com>
Sent: Wednesday, 8 April 2020 11:32 PM
To: Anna Lyons <a...@gh.st>; devel <devel@sel4.systems>
Subject: Re: [seL4] setConsumed() in seL4_SchedContext_YieldTo
Hello Anna,
Thanks for the reply. Maybe I'v imagined an impractical scenario:
1. A yield to B. B->sc->scYieldFrom=A
2. B run then block.
3. A run then yield to B again.
4. Now at the beginning, setConsumed() called; because B is not runnable, so
return_now=true and setConsumed() called again at the end.
For cooperative threads, this indeed shouldn't happen but it depends. For
example if B can block, then great care should be taken to forbid this edge
case.
Regards,
laokz
------------------ Original ------------------
From: "Anna Lyons"<a...@gh.st>;
Date: Mon, Apr 6, 2020 12:16 PM
To: "laokz"<la...@foxmail.com>;"devel"<devel@sel4.systems>;
Subject: Re: [seL4] setConsumed() in seL4_SchedContext_YieldTo
P {margin-top:0;margin-bottom:0;} Hi,
Thanks for the observation! It's true that setConsumed should only be called
once per kernel entry, and it's not obvious just from the code snippets to
observe that this is true.
However, the semantics of YieldTo mean that both of these code paths cannot be
executed in the same kernel entry.
If return_now is true, this means that the current thread will be switched to
and sc->scYieldFrom should be NULL (as the YieldTo call has completed). This is
usually the case if the calling thread YieldTo a lower priority thread, or a
thread that is not runnable. On the other hand if return_now is false, the
YieldTo resulted in the thread being YieldedTo being switched to, so we return
the result of the YieldTo on a different kernel entry (when we run the thread
that called YieldTo again).
With this context, take a look at the if block here:
https://github.com/seL4/seL4/blob/master/src/object/schedcontext.c#L191
Where you can see that we only set sc->scYieldFrom when we also set return_now
to false.
Glad to see someone looking at the MCS kernel.
Anna.
------------------------------
Message: 2
Date: Thu, 9 Apr 2020 09:48:49 -0500
From: Grant Jurgensen <gajurgen...@gmail.com>
To: devel@sel4.systems
Subject: [seL4] TimeServer "IRQ already mapped" error
Message-ID:
<CAGJ6_3Cdhk9BrMD0roaCZvi7QZr1M7U3GA1jQ3=m0tmhath...@mail.gmail.com>
Content-Type: text/plain; charset="UTF-8"
Hi all,
I'm trying to add a timer to my CAmkES component (all I need is a timestamp).
I've been using this example component as a reference:
https://github.com/seL4/camkes/tree/master/apps/timeserver
My problem is that when I declare an instance of the global TimeServer
component in my ".camkes" file, I get an error at build-time: "parse-capDL:
IRQ already mapped: 68".
I'm not sure what to make of this error. The only major difference between my
project and the reference above is that I am building atop the camkes-arm-vm
project. Could the VM be interfering here?
Thanks,
Grant Jurgensen
------------------------------
Subject: Digest Footer
_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel
------------------------------
End of Devel Digest, Vol 71, Issue 10
*************************************
_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel
