Hello everyone, Currently I'm going through the source code of seL4. I find function in seL4\src\object\Tcb.c that I can't find it's definition. In line 59, tcbSchedEnqueue calls a function 'thread_state_ptr_set_tcbQueued(&tcb->tcbState, true)'. However, even with the help of Source Insight I still can't locate the definition of 'thread_state_ptr_set_tcbQueued' . Does anyone know where it is ? Thanks in advance. Best regards, Kenneth.
Hi Kenneth, After you build the kernel, you can find its definition in build/kernelkernel_final.c file. But I do no know how it is generated. I guess it is generated by some scripts or preprocessor. I also hope the answer from sel4 expert. Best, Yuxin On Tue, Oct 28, 2014 at 3:59 AM, chengkunck@gmail.com <chengkunck@gmail.com> wrote:
Hello everyone,
Currently I'm going through the source code of seL4. I find function in seL4\src\object\Tcb.c that I can't find it's definition.
In line 59, *tcbSchedEnqueue* calls a function '*thread_state_ptr_set_tcbQueued(&tcb->tcbState, true)*'. However, even with the help of Source Insight I still can't locate the definition of '*thread_state_ptr_set_tcbQueued' .* Does anyone know where it is ?
Thanks in advance.
Best regards, Kenneth.
_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
Hi, This function, and many others, is generated by a tool called the 'bitfield generator' in tools/bitfield_gen.py It takes as input files ending in .bf, and can produce both C code and proofs said code. If you were to look in include/arch/arm/arch/object/structures.bf you would find a block structure called 'thread_state' with a field member called 'tcbQueued'. The bitfield generator takes this data structure description and generates all the relevant getter, setter and construction methods. So during the build a file called 'arch/object/structures_gen.h' will get generated from this .bf file using the bitfield_gen.py tool in the Makefile rule '%_gen.h:' that contains all the functions. This file gets removed after compilation when doing standalone kernel builds. Adrian On 29/10/14 03:10, Yuxin Ren wrote: Hi Kenneth, After you build the kernel, you can find its definition in build/kernelkernel_final.c file. But I do no know how it is generated. I guess it is generated by some scripts or preprocessor. I also hope the answer from sel4 expert. Best, Yuxin On Tue, Oct 28, 2014 at 3:59 AM, chengkunck@gmail.com<mailto:chengkunck@gmail.com> <chengkunck@gmail.com<mailto:chengkunck@gmail.com>> wrote: Hello everyone, Currently I'm going through the source code of seL4. I find function in seL4\src\object\Tcb.c that I can't find it's definition. In line 59, tcbSchedEnqueue calls a function 'thread_state_ptr_set_tcbQueued(&tcb->tcbState, true)'. However, even with the help of Source Insight I still can't locate the definition of 'thread_state_ptr_set_tcbQueued' . Does anyone know where it is ? Thanks in advance. Best regards, Kenneth. _______________________________________________ Devel mailing list Devel@sel4.systems<mailto:Devel@sel4.systems> https://sel4.systems/lists/listinfo/devel _______________________________________________ Devel mailing list Devel@sel4.systems<mailto:Devel@sel4.systems> https://sel4.systems/lists/listinfo/devel ________________________________ 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.
Thank you, Adrian. That helps me. chengkunck@gmail.com From: Adrian Danis Date: 2014-10-29 08:13 To: Yuxin Ren; chengkunck@gmail.com CC: devel Subject: Re: [seL4] A missing function? Hi, This function, and many others, is generated by a tool called the 'bitfield generator' in tools/bitfield_gen.py It takes as input files ending in .bf, and can produce both C code and proofs said code. If you were to look in include/arch/arm/arch/object/structures.bf you would find a block structure called 'thread_state' with a field member called 'tcbQueued'. The bitfield generator takes this data structure description and generates all the relevant getter, setter and construction methods. So during the build a file called 'arch/object/structures_gen.h' will get generated from this .bf file using the bitfield_gen.py tool in the Makefile rule '%_gen.h:' that contains all the functions. This file gets removed after compilation when doing standalone kernel builds. Adrian On 29/10/14 03:10, Yuxin Ren wrote: Hi Kenneth, After you build the kernel, you can find its definition in build/kernelkernel_final.c file. But I do no know how it is generated. I guess it is generated by some scripts or preprocessor. I also hope the answer from sel4 expert. Best, Yuxin On Tue, Oct 28, 2014 at 3:59 AM, chengkunck@gmail.com <chengkunck@gmail.com> wrote: Hello everyone, Currently I'm going through the source code of seL4. I find function in seL4\src\object\Tcb.c that I can't find it's definition. In line 59, tcbSchedEnqueue calls a function 'thread_state_ptr_set_tcbQueued(&tcb->tcbState, true)'. However, even with the help of Source Insight I still can't locate the definition of 'thread_state_ptr_set_tcbQueued' . Does anyone know where it is ? Thanks in advance. Best regards, Kenneth. _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel 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.
Oh, thank you so much. I never thought of that, lol. chengkunck@gmail.com From: Yuxin Ren Date: 2014-10-29 00:10 To: chengkunck@gmail.com CC: devel Subject: Re: [seL4] A missing function? Hi Kenneth, After you build the kernel, you can find its definition in build/kernelkernel_final.c file. But I do no know how it is generated. I guess it is generated by some scripts or preprocessor. I also hope the answer from sel4 expert. Best, Yuxin On Tue, Oct 28, 2014 at 3:59 AM, chengkunck@gmail.com <chengkunck@gmail.com> wrote: Hello everyone, Currently I'm going through the source code of seL4. I find function in seL4\src\object\Tcb.c that I can't find it's definition. In line 59, tcbSchedEnqueue calls a function 'thread_state_ptr_set_tcbQueued(&tcb->tcbState, true)'. However, even with the help of Source Insight I still can't locate the definition of 'thread_state_ptr_set_tcbQueued' . Does anyone know where it is ? Thanks in advance. Best regards, Kenneth. _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
participants (3)
-
Adrian Danis -
chengkunck＠gmail.com -
Yuxin Ren