Hi All, I think, on IA-32, sel4 supports multi-core machine. But I do not how to use that. Here I have two specfic questions. 1. How to assign a specific core to a process/thread? And can I change this affinity? 2. How to two process/threads communicate via IPC on different cores? I want to know some implementation details in kernel to support cross-core IPC. Could anyone explain its logic or tell me the code for it in the kernel? Thank you very much. Best, Yuxin
“supports” is too strong a word ☺ We have some internal research prototypes we use for exploring the research challenge of concurrency versus verification tractability, in addition to currency models for microkernels in general. Some of that code is probably what you have found. The code is likely to be highly experimental, and not what we are actively working on. We have more mature research prototypes (still prototypes) internally that we a working towards releasing when time allows. I can’t give an accurate estimate, but it is likely to be in terms of weeks, not months. - Kevin From: Devel [mailto:devel-bounces@sel4.systems] On Behalf Of Yuxin Ren Sent: Tuesday, 21 October 2014 1:05 AM To: devel@sel4.systems Subject: [seL4] sel4 on multi-core Hi All, I think, on IA-32, sel4 supports multi-core machine. But I do not how to use that. Here I have two specfic questions. 1. How to assign a specific core to a process/thread? And can I change this affinity? 2. How to two process/threads communicate via IPC on different cores? I want to know some implementation details in kernel to support cross-core IPC. Could anyone explain its logic or tell me the code for it in the kernel? Thank you very much. Best, Yuxin ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Security and IPC is hard.... Shared memory is difficult. Network sockets (localhost.localdomain) is a good bet. Asking about assigning a specific core to a process/thread is difficult. A system needs a lot of control to be stable. Giving control away risks instability because interrupt and other core functions are not negotiable. Threads are also very difficult yet easy to abuse. What specific user space parallel IPC programming model is interesting? There are many? What object reuse policy is expected? On Mon, Oct 20, 2014 at 2:36 PM, Kevin Elphinstone < Kevin.Elphinstone@nicta.com.au> wrote:
“supports” is too strong a word J
We have some internal research prototypes we use for exploring the research challenge of concurrency versus verification tractability, in addition to currency models for microkernels in general. Some of that code is probably what you have found. The code is likely to be highly experimental, and not what we are actively working on.
We have more mature research prototypes (still prototypes) internally that we a working towards releasing when time allows. I can’t give an accurate estimate, but it is likely to be in terms of weeks, not months.
- Kevin
*From:* Devel [mailto:devel-bounces@sel4.systems] *On Behalf Of *Yuxin Ren *Sent:* Tuesday, 21 October 2014 1:05 AM *To:* devel@sel4.systems *Subject:* [seL4] sel4 on multi-core
Hi All,
I think, on IA-32, sel4 supports multi-core machine.
But I do not how to use that. Here I have two specfic questions.
1. How to assign a specific core to a process/thread? And can I change this affinity?
2. How to two process/threads communicate via IPC on different cores?
I want to know some implementation details in kernel to support cross-core IPC.
Could anyone explain its logic or tell me the code for it in the kernel?
Thank you very much.
Best,
Yuxin
------------------------------
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
-- T o m M i t c h e l l
In our project, we build the control system with some machine running seL4, some means more than 2, seL4 is the base kernel of these system, and the upper is platform like Android framework developed by ourself, we call it Elastos, it is written in c++. seL4 communicate with others through TCP/IP. 发件人: Devel [mailto:devel-bounces@sel4.systems] 代表 Tom Mitchell 发送时间: 2014年10月21日 9:42 收件人: Kevin Elphinstone 抄送: devel@sel4.systems 主题: Re: [seL4] sel4 on multi-core Security and IPC is hard.... Shared memory is difficult. Network sockets (localhost.localdomain) is a good bet. Asking about assigning a specific core to a process/thread is difficult. A system needs a lot of control to be stable. Giving control away risks instability because interrupt and other core functions are not negotiable. Threads are also very difficult yet easy to abuse. What specific user space parallel IPC programming model is interesting? There are many? What object reuse policy is expected? On Mon, Oct 20, 2014 at 2:36 PM, Kevin Elphinstone <Kevin.Elphinstone@nicta.com.au> wrote: “supports” is too strong a word J We have some internal research prototypes we use for exploring the research challenge of concurrency versus verification tractability, in addition to currency models for microkernels in general. Some of that code is probably what you have found. The code is likely to be highly experimental, and not what we are actively working on. We have more mature research prototypes (still prototypes) internally that we a working towards releasing when time allows. I can’t give an accurate estimate, but it is likely to be in terms of weeks, not months. - Kevin From: Devel [mailto:devel-bounces@sel4.systems] On Behalf Of Yuxin Ren Sent: Tuesday, 21 October 2014 1:05 AM To: devel@sel4.systems Subject: [seL4] sel4 on multi-core Hi All, I think, on IA-32, sel4 supports multi-core machine. But I do not how to use that. Here I have two specfic questions. 1. How to assign a specific core to a process/thread? And can I change this affinity? 2. How to two process/threads communicate via IPC on different cores? I want to know some implementation details in kernel to support cross-core IPC. Could anyone explain its logic or tell me the code for it in the kernel? Thank you very much. Best, Yuxin _____ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel -- T o m M i t c h e l l
Thank you all for your replies. But those replies are confusing to me. My understanding is, IPC provided by current sel4 kernel does not support communication between two process on different cores. Is this true? Best, Yuxin On Mon, Oct 20, 2014 at 10:06 PM, XilongPei(裴喜龙) <pei_xilong@tongji.edu.cn> wrote:
In our project, we build the control system with some machine running seL4, some means more than 2, seL4 is the base kernel of these system, and the upper is platform like Android framework developed by ourself, we call it Elastos, it is written in c++. seL4 communicate with others through TCP/IP.
*发件人:* Devel [mailto:devel-bounces@sel4.systems] *代表 *Tom Mitchell *发送时间:* 2014年10月21日 9:42 *收件人:* Kevin Elphinstone *抄送:* devel@sel4.systems *主题:* Re: [seL4] sel4 on multi-core
Security and IPC is hard....
Shared memory is difficult.
Network sockets (localhost.localdomain) is a good bet.
Asking about assigning a specific core to a process/thread is difficult.
A system needs a lot of control to be stable. Giving control away risks
instability because interrupt and other core functions are not negotiable.
Threads are also very difficult yet easy to abuse.
What specific user space parallel IPC programming model is interesting?
There are many?
What object reuse policy is expected?
On Mon, Oct 20, 2014 at 2:36 PM, Kevin Elphinstone < Kevin.Elphinstone@nicta.com.au> wrote:
“supports” is too strong a word J
We have some internal research prototypes we use for exploring the research challenge of concurrency versus verification tractability, in addition to currency models for microkernels in general. Some of that code is probably what you have found. The code is likely to be highly experimental, and not what we are actively working on.
We have more mature research prototypes (still prototypes) internally that we a working towards releasing when time allows. I can’t give an accurate estimate, but it is likely to be in terms of weeks, not months.
- Kevin
*From:* Devel [mailto:devel-bounces@sel4.systems] *On Behalf Of *Yuxin Ren *Sent:* Tuesday, 21 October 2014 1:05 AM *To:* devel@sel4.systems *Subject:* [seL4] sel4 on multi-core
Hi All,
I think, on IA-32, sel4 supports multi-core machine.
But I do not how to use that. Here I have two specfic questions.
1. How to assign a specific core to a process/thread? And can I change this affinity?
2. How to two process/threads communicate via IPC on different cores?
I want to know some implementation details in kernel to support cross-core IPC.
Could anyone explain its logic or tell me the code for it in the kernel?
Thank you very much.
Best,
Yuxin
------------------------------
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
--
T o m M i t c h e l l
_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
"Yuxin" == Yuxin Ren <ryx@gwmail.gwu.edu> writes:
Yuxin> Thank you all for your replies. But those Yuxin> replies are confusing to me. My understanding is, IPC provided Yuxin> by current sel4 kernel does not support communication between Yuxin> two process on different cores. Is this true? Yes. The released verified seL4 kernel is single-core only. -- Dr Peter Chubb peter.chubb AT nicta.com.au http://www.ssrg.nicta.com.au Software Systems Research Group/NICTA
On 21 Oct 2014, at 20:22 , Peter Chubb <peter.chubb@nicta.com.au> wrote:
"Yuxin" == Yuxin Ren <ryx@gwmail.gwu.edu> writes:
Yuxin> Thank you all for your replies. But those Yuxin> replies are confusing to me. My understanding is, IPC provided Yuxin> by current sel4 kernel does not support communication between Yuxin> two process on different cores. Is this true?
Yes. The released verified seL4 kernel is single-core only.
And, as Kevin said, any multicore support in the experimental branch is *very* experimental and may not be fully functional. A proper implementation isn’t far off, you’re probably better off waiting for that than wasting time with what’s in there right now. Gernot ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
participants (6)
-
Gernot Heiser -
Kevin Elphinstone -
Peter Chubb -
Tom Mitchell -
XilongPei(裴喜龙) -
Yuxin Ren