- Devel - lists.sel4.systems

Invalid package ID: "array-0.5.1.1 base-4.9.0.0 binary-0.8.3.0 bytestring-0.10.8.1"
by tj5527 23 Jul '17

23 Jul '17

Another problem when making sel4. The make program complains Invalid package ID: "array-0.5.1.1 base-4.9.0.0 binary-0.8.3.0 bytestring-0.10.8.1". [parse-capDL] building... make: Entering directory '/path/to/sel4/projects/capdl/capDL-tool' stack setup stack will use a locally installed GHC For more information on paths, see 'stack path' and 'stack exec env' To use this GHC and packages outside of a project, consider using: stack ghc, stack ghci, stack runghc, or stack exec stack build --only-dependencies Invalid package ID: "array-0.5.1.1 base-4.9.0.0 binary-0.8.3.0 bytestring-0.10.8.1" Makefile:39: recipe for target 'sandbox' failed make: *** [sandbox] Error 1 How can I fix this? Thank you. Ubuntu 16.04 LTS GNU Make 4.1 gcc version 5.4.0 20160609

3 4

Sydney `taste of seL4' miniconference/developer day
by Peter.Chubb＠data61.csiro.au 19 Jul '17

19 Jul '17

Hi Folks, Next January 22--26, linux.conf.au will be in Sydney, Australia. We're planning on submitting a proposal for a one-day miniconference to be held in conjunction with the main conference. We'd like to line up potential speakers now, before submitting. If you are doing something cool and open source with seL4, and would like to speak at that miniconference, please let me know. linux.conf.au is one of the best grass-roots open-source and Linux conferences around; if you're doing anything cool that's open source with seL4 (or with Linux), then I'd encourage you to submit a proposal to the main conference as well, at https://linux.conf.au/ Peter Chubb -- Dr Peter Chubb Tel: +61 2 9490 5852 http://ts.data61.csiro.au/ Trustworthy Systems Group Data61 (formerly NICTA)

1 0

Question on endpoint cap write permission
by Jimmy Brush 13 Jul '17

13 Jul '17

Hello, in the 6.0 manual section 3.1.4 the table shows that Write permission on an endpoint cap permits sending to the endpoint. however, in section 4.2.2 it says without the Write permission on the RECEIVING endpoint cap, any cap sent over IPC gets diminished. Am I missing something? It seems the Write permission is overloaded to mean two different things. This would seem to imply that to receive an undiminished capability via IPC you must have both send and receive permission to the endpoint you are receiving against. Which would mean if you wanted to limit someone to only receiving and never sending against an endpoint by giving them an endpoint cap with only Read permission, they would necessarily also NEVER be able to receive an undiminished capability. Thanks, JB

4 5

Compile problems about camkes-vm project
by deng.chao1＠zte.com.cn 11 Jul '17

11 Jul '17

SGkgZXZlcnlvbmU6DQoNCiAgSSB0cnkgdG8gcnVuIHZtIG9uIHNlTDQuIA0KDQogIEkgaGF2ZSBk b3dubG9hZGVkIFZNIHByb2plY3QgdXNpbmcgInJlcG8gaW5pdCAtdSBodHRwczovL2dpdGh1Yi5j b20vc2VMNC9jYW1rZXMtdm0tbWFuaWZlc3QuZ2l0Ii4gDQoNCiAgSSB1c2UgY29tbWFuZHM6DQoN CiAgICAgIG1ha2UgY21hMzRjcl90d292bV9kZWZjb25maWcNCg0KICAgICAgbWFrZSBzaWxlbnRv bGRjb25maWcNCg0KICAgICAgbWFrZSANCg0KdG8gY29tcGlsZSB0aGUgcHJvamVjdCwgYnV0IGhl cmUgcmVwb3J0cyBwcm9ibGVtcy4NCg0KICBUaGUgZmlyc3QgcHJvYmxlbSBpcywgaXQgY2FuIG5v dCBmaW5kIGxpYnBpY290Y3AuIEkgaGF2ZSBjaGVjayB0aGUgc291cmNlIGNvZGUsIGl0IGRvZXNu J3QgaW5jbHVkZSBkaXJlY3RvcnkgbGlicy9saWJwaWNvdGNwLy4NCg0KU28gSSBnZXQgcmlkIG9m IHRoZSBsaWJwaWNvdGNwIHBhcnQgYnkgY29tbWVudCBpdCBpbiB0aGUgS2NvbmZpZyBmaWxlLg0K DQogIE5leHQsIHRoZSBvdGhlciBwcm9ibGVtIGFjY3VycyBhcyBibG93aW5nOg0KDQoJIi9ob21l L2RlbmdjaGFvL21qL2NhbWtlcy12bS90b29scy9jYW1rZXMvY2Fta2VzLm1rOjEzNzogL2hvbWUv ZGVuZ2NoYW8vbWovY2Fta2VzLXZtL2J1aWxkL3g4Ni9wYzk5L2NtYTM0Y3JfdHdvdm0vY2Fta2Vz LWdlbi5tazogTm8gc3VjaCBmaWxlIG9yIGRpcmVjdG9yeQ0KDQogCVtHRU5dIGNhbWtlcy1nZW4u bWsNCg0KCUVSUk9SOkNBbWtFUzovaG9tZS9kZW5nY2hhby9tai9jYW1rZXMtdm0vYXBwcy9jbWEz NGNyX3R3b3ZtL3ZtLmNhbWtlczoyMzoxOTogICAgICAgICBjb21wb25lbnQgRWNobyBlY2hvDQoN CglFUlJPUjpDQW1rRVM6ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIF5eXl5eXg0KDQoJRVJST1I6 Q0Fta0VTOm5vbi1vcHRpb25hbCBpbnRlcmZhY2UgZWNoby50aW1lciBpcyBub3QgY29ubmVjdGVk DQoNCgltYWtlWzFdOiAqKiogWy9ob21lL2RlbmdjaGFvL21qL2NhbWtlcy12bS9idWlsZC94ODYv cGM5OS9jbWEzNGNyX3R3b3ZtL2NhbWtlcy1nZW4ubWtdIGVycm9yIDI1NSINCg0KICANCg0KICBJ IGhhdmUgdHJpZWQgY29uZmlnIHRoZSBwcm9qZWN0IHRvIGNtYTM0Y3Jfc2luZ2xldm1fZGVmY29u ZmlnIG9yIGNtYTM0Y3JfdWJ1bnR1X2RlZmNvbmZpZywgYWxzbyByZXBvcnMgdGhlIHNhbWUgZXJy b3IuDQoNCiAgQW5kIHRoZSBjMTYyX3R3b3ZtIGNvbmZpZywgc2VlbXMgaXQgaGFkIGFsc28gYmVl biByZW1vdmVkIGZvciB0aGUgY2Fta2VzLXZtIHByb2plY3Q/DQoNCiAgQ291bGQgYW55b25lIHJl bHkgbWUgb24gdGhlIGtpbmRuZXNzPw0KDQoJCQkJCQkJCSAgICAgICAgICAgICAgICAgICAgICAg ICAgICAgICAgICAgICAgICAgICAgICAgIHlvdXJzIERlbmdDaGFv

2 1

L4Re IPC share memory that share file in one Linux filesystem and be visible to other Linuxes
by Joyce Peng(彭美僑) 05 Jul '17

05 Jul '17

Hi L4, I want to share a file in one Linux filesystem and be visible to other Linuxes that all run on top Fiasco.OC. It seems an IPC communication between L4re vm tasks. And access a file in Linux filesystem is a mechanism with kernel block device driver. But I only notice two char device drivers that use L4re library l4shmc in L4linux. It is l4ser_shm and l4shmnet. May you give some information about this work how to work. Thanks. Joyce Peng(彭美僑)

2 1

malloc & errno
by Fabrizio Bertocci 05 Jul '17

05 Jul '17

Hi all, I am facing a puzzling problem related to muslc. While running some tests with the ia32 simulator (qemu), have noticed that whenever I call malloc() and I run out of memory (because my morecore buffer is too small), I am getting some kernel crash. I have traced the issue to the place where errno is set to -ENOMEM. Referencing to errno is platform-dependent and end up calling a function that retrieve the struct pthread associated and access errno as one of the field of the struct pthread. What is the correct process to set up a heap from the root task in such a way that we can call malloc() and correctly handle error conditions through errno? I am pretty sure I am doing something wrong in my initialization code (I have based my main(0 on the code from the tutorials), because I am also having other problems with malloc(). (even after I increase my heap area). For example, in some cases a call to malloc() end up calling a cascade of functions that eventually (from inside muslc) end up calling again malloc(). As consequence it enters in an infinite loop that stop only after it exhaust the initial stack. I could not find any clear example that show how to correctly set up a system to use muslc. Can anyone point me to a good example that shows how to bootstrap a system for the 5.2.0 branch? Regards, Fabrizio Bertocci Real-Time Innovations, Inc. Sunnyvale, CA

2 1

make: stack: Command not found
by tj5527 04 Jul '17

04 Jul '17

A newbie question. I follow the link [1] trying to build sel4 with qemu. But when `make`ing the binary, it throws error message `make: stack: Command not found`. I `apt-get install stacks` but it still fails with the same error. What packages should I install for making sel4 with Ubuntu 16.04 LTS, GNU Make 4.1, and gcc version 5.4.0 20160609? Thanks [Error Message] -- Build files have been written to: /path/to/sel4/stage/x86/pc99/accelerator ninja: no work to do. [apps/vm] building... [HEADERS] [STAGE] autoconf.h [apps/vm] done. [parse-capDL] building... make: Entering directory '/path/to/sel4/projects/capdl/capDL-tool' stack setup make: stack: Command not found Makefile:39: recipe for target 'sandbox' failed make: *** [sandbox] Error 127 make: Leaving directory '/path/to/sel4/projects/capdl/capDL-tool' Makefile:53: recipe for target '/path/to/sel4/stage/x86/pc99/parse-capDL/parse-capDL' failed make: *** [/path/to/sel4/stage/x86/pc99/parse-capDL/parse-capDL] Error 2 [1] https://wiki.sel4.systems/Hardware/Qemu

1 1

elfloader-tool
by Yevgeny Lavrov 30 Jun '17

30 Jun '17

Hi Is there any instruction on how to compile and use elfloader-tool? More specifically: I want to link seL4 image with other image to try out on i.MX6 platform. Thanks

2 1

vmm documentation
by Mike Clark 29 Jun '17

29 Jun '17

Is there any documentation on how the VMM works? If I wanted to start hacking on the VMM and extend its capability, where should I start looking to learn how it works, etc? That might be a pretty broad topic, because there are lots of ways the VMM can be extended, I'm sure. Broad is fine, until I get things more figured out.

4 17

Why armel for the seL4 ARM VMM?
by John Backes 27 Jun '17

27 Jun '17

I was curious why the ARM VMM for the TK1 only seems to support the use of armel based distributions? Does special care need to be taken in the VMM to handle guest floating point instructions if the OS is armhf based? - John

2 1