Thanks Damon for your help!
I've added the required "simple" attribute to the assembly configuration:
assembly {
composition {
[...]
component Client client;
}
configuration {
[....]
client.simple = true;
}
}
But the usage generates:
implicit declaration of function ‘camkes_make_simple’
and I don't know what header(s) I should include and/or any library I
should link to get ‘camkes_make_simple’ decl/def.
camkes_make_simple() function does not exist in any of simple
camkes tutorials to figure out the required headers, while your example has
too many headers to figure out what headers are really needed.
Further help with it is greatly appreciated. Thanks.
Chris
On Thu, Oct 29, 2020 at 4:36 PM <devel-request@sel4.systems> wrote:
> 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. seL4_BootInfo in Camkes environment (Chris Koziarz)
> 2. Re: seL4_BootInfo in Camkes environment
> (Lee, Damon (Data61, Kensington NSW))
> 3. Re: raspberry pi 4 (Jose A. Pascual)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Thu, 29 Oct 2020 13:39:12 +1100
> From: Chris Koziarz <ch...@breakawayconsulting.com.au>
> To: devel@sel4.systems
> Subject: [seL4] seL4_BootInfo in Camkes environment
> Message-ID:
> <CAMuEnL6VH8xYxK9SR64Sc65onK7By=
> 66xkiphhgmzu4rjdg...@mail.gmail.com>
> Content-Type: text/plain; charset="UTF-8"
>
> In a regular seL4 PD, I always have seL4_BootInfo available
> via platsupport_get_bootinfo(), and all goodies that I can learn from
> therein are available.
>
> But it appears that the camkes components (probably we should talk about
> "client components", i.e. the ones with "control;" attribute and an entry
> point: int run(void)),
> are started as a typical root task, with a call:
> void __sel4_start_root(seL4_BootInfo *boot_info)
> however boot_info is passed herein as NULL.
> At least boot_info appears NULL for me on ARM64.
> So, is the access to seL4_BootInfo disallowed in camkes env? Or how can I
> access seL4_BootInfo in camkes?
>
> Chris
>
>
> ------------------------------
>
> Message: 2
> Date: Thu, 29 Oct 2020 04:28:56 +0000
> From: "Lee, Damon (Data61, Kensington NSW)"
> <damon....@data61.csiro.au>
> To: "devel@sel4.systems" <devel@sel4.systems>
> Subject: Re: [seL4] seL4_BootInfo in Camkes environment
> Message-ID: <tfbft5x4pve....@coopers.keg.data61.csiro.au>
> Content-Type: text/plain; charset="iso-8859-1"
>
> Hi Chris,
>
> > In a regular seL4 PD, I always have seL4_BootInfo available
> > via platsupport_get_bootinfo(), and all goodies that I can learn
> > from
> > therein are available.
> >
> > But it appears that the camkes components (probably we should
> > talk about
> > "client components", i.e. the ones with "control;" attribute and
> > an entry
> > point: int run(void)),
> > are started as a typical root task, with a call:
> > void __sel4_start_root(seL4_BootInfo *boot_info)
> > however boot_info is passed herein as NULL.
> > At least boot_info appears NULL for me on ARM64.
> > So, is the access to seL4_BootInfo disallowed in camkes env? Or
> > how can I
> > access seL4_BootInfo in camkes?
>
> The bootinfo isn't disallowed in a CAmkES environment but parts of
> it
> is gutted out (untyped information, IRQ control cap etc.)
> depending on
> the configuration of the CAmkES application. To access the
> bootinfo,
> you could append this configuration option for a specific
> component in
> the "configuration" block in the ".camkes" file of your
> application:
>
> <component_name>.simple = true;
>
> The simple_t interface which abstracts the bootinfo can then be
> grabbed via the 'camkes_make_simple()' function.
>
> There are examples of the bootinfo usage in our CAmkES VM
> repositories
> that you can checkout here:
>
> https://github.com/seL4/camkes-vm/blob/master/components/VM_Arm/src/main.c#L429
>
> Regards,
> Damon
>
>
> ------------------------------
>
> Message: 3
> Date: Thu, 29 Oct 2020 06:45:16 +0100
> From: "Jose A. Pascual" <joseantonio.pasc...@ehu.eus>
> To: Nick Spinale <nick.spin...@arm.com>
> Cc: Sachin More <sachinsureshm...@gmail.com>, "devel@sel4.systems"
> <devel@sel4.systems>
> Subject: Re: [seL4] raspberry pi 4
> Message-ID:
> <CAK8ti4+QiFTDnBKRfZYWQ-XXAT_=
> mntr_+jhjrfmwzq-w6w...@mail.gmail.com>
> Content-Type: text/plain; charset="UTF-8"
>
> Hi,
> We are also running seL4 on the RPI4 and we managed to run "sel4test"
> passing all the tests.
> Basically, you can build the sel4test project and execute all the tests
> without errors as in the Rpi3.
> We are using it in an OS course to build a very simple OS on top of seL4.
> I'll try to open a PR in the following days.
> Nick, if you don't mind, I'll compare our patch with yours to check if we
> are doing everything the same way.
> I'll keep you informed.
>
> Jose (& Mikel)
>
>
> On Thu, Oct 29, 2020 at 1:29 AM Nick Spinale <nick.spin...@arm.com> wrote:
>
> > > Can I prepare, say seL4 11.0 and then apply your patches and then
> > compile using seL4's build system (or your build system if it is in
> public
> > domain)?
> >
> > At the moment, I?m unable to share the rest of the code for this
> > particular project. I have, however, published our Raspberry Pi 4-related
> > patches to public branches of 'seL4' [1] and ?seL4_tools' [2]. These
> > patches, which are the extent of our Raspberry Pi 4-related patches for
> > upstream seL4 repositories, only encompasses the bootloader (?elfloader?)
> > and the seL4 kernel itself. The projects that you might use for getting
> > started, such as ?sel4test? [3], depend on platform support for userland
> > libraries such as those found in ?seL4_libs? [4].
> >
> > If you decide to add Raspberry Pi 4 support to those userland libraries,
> > I?d be happy to help out with that.
> >
> >
> > [1] https://github.com/nspin/seL4/tree/rpi4
> > [2] https://github.com/nspin/seL4_tools/tree/rpi4
> > [3] https://github.com/seL4/sel4test-manifest
> > [4] https://github.com/seL4/seL4_libs
> >
> >
> > - - - -
> > Nick Spinale (nickspinale.com)
> > Arm Research, Cambridge UK
> > - - - -
> >
> > IMPORTANT NOTICE: The contents of this email and any attachments are
> > confidential and may also be privileged. If you are not the intended
> > recipient, please notify the sender immediately and do not disclose the
> > contents to any other person, use it for any purpose, or store or copy
> the
> > information in any medium. Thank you.
> > _______________________________________________
> > Devel mailing list
> > Devel@sel4.systems
> > https://sel4.systems/lists/listinfo/devel
> >
>
>
> ------------------------------
>
> Subject: Digest Footer
>
> _______________________________________________
> Devel mailing list
> Devel@sel4.systems
> https://sel4.systems/lists/listinfo/devel
>
>
> ------------------------------
>
> End of Devel Digest, Vol 77, Issue 11
> *************************************
>
_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel
