- Devel - lists.sel4.systems

CAmkES 3.7.0 bug?
by Zippy Maniac 11 Sep '19

11 Sep '19

Hi, I am porting an old application from CAmkES 2.x to CAmkES 3.7.0. But I am having an issue with a very large dataport. The data structure mapped between components needs to be about 25 MiB. I have defined the size of the connection to be 64 MiB. But compilation fails. Looking at the generated code for the shared data I see this struct { char content[ROUND_UP_UNSAFE(sizeof(ui_config_t), PAGE_SIZE_4K)]; } to_0_ui_configbuf_data ALIGN(16777216) SECTION("align_24bit") USED; extern typeof(to_0_ui_configbuf_data) to_0_ui_configbuf_data ALIGN(67108864) VISIBLE; static_assert(sizeof(to_0_ui_configbuf_data) <= 67108864, "typeof(to_0_ui_configbuf_data) size greater than dataport size."); static_assert(sizeof(to_0_ui_configbuf_data) % 16777216 == 0, "to_0_ui_configbuf_data not page-sized. Template bug in its declaration? Suggested formulation: `char to_0_ui_configbuf_data[ROUND_UP_UNSAFE(sizeof(...), PAGE_SIZE_4K)];`"); But compilation fails with projects/musllibc/build-temp/stage/include/assert.h:12:23: error: static assertion failed: "to_0_ui_configbuf_data not page-sized. Template bug in its declaration? Suggested formulation: `char to_0_ui_configbuf_data[ROUND_UP_UNSAFE(sizeof(...), PAGE_SIZE_4K)];`" The assert is looking for the buffer to be a multiple of 16MiB but the ROUND_UP_UNSAFE is only doing working to a multiple of 4KiB. PAGE_SIZE_4K is hard coded in the template but the alignment has changed from 12bit to 24bit so CAmkES is aware of the large data structure. I guess I could pad and align my data structure to a multiple of 16MiB. Also, having hard coded numbers in my top level CAmkES configuration for the dataport size is a bit of a maintenance nightmare. Being able to use a #define from the code base would be ideal but this doesn't work. It does work for paddr and irq_number specifications! Cheers, Zippy

2 2

Error with the file handling in camkes tutorial
by Akshat Garg 11 Sep '19

11 Sep '19

Hi all, I am trying to understand how the camkes system works. I get stuck up on a problem where I tried to change the code of camkes 1 tutorial ( https://docs.sel4.systems/Tutorials/hello-camkes-1.html) a bit. In a simple sender receiver code, I tried to write the contents, received by the receiver, in a file. But, while doing it I got the following error message. The error message was not letting me to create a file in any mode. When using read mode with FILE *fptr = fopen("xxxyyyzzz", "r"); I encountered the following message: sys_open_impl@sys_io.c:205 Failed to open file xxxyyyzzz FAULT HANDLER: data fault from client1.control (ID 0x1) on address 0, pc = 0x411754, fsr = 0x4 FAULT HANDLER: rip = 0x411754 FAULT HANDLER: rsp = 0x528ae8 When using write mode with FILE *fptr = fopen("xxxyyyzzz", "w"); I encountered the following message: sys_open_impl@sys_io.c:191 Open only supports O_RDONLY, not 0x241 on xxxyyyzzz Assertion failed: flags == O_RDONLY (../projects/seL4_libs/libsel4muslcsys/src/sys_io.c: sys_open_impl: 192) Kindly, suggest me a way out or let me know the reason if not possible. -Akshat

2 1

Compiling Error for Hello World
by Shahnewaz Sakib 11 Sep '19

11 Sep '19

Hi, I was trying to compile hello world using the tutorial here <https://docs.sel4.systems/Tutorials/#get-the-code>. I was able to compile sel4test before and I built the dependencies using docker. For running hello world, I used the command "../init --plat pc99 --tut hello-world". Then I got the following error message: Traceback (most recent call last): File "../init", line 16, in <module> import common File "/home/bikas/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 16, in <module> import sh ModuleNotFoundError: No module named 'sh' I have looked into my machine and I do have sh in "/usr/bin/sh". I am not sure what is the source of the error. Please let me know. Thanks! -- Shahnewaz Karim Sakib

2 1

Muen
by Gergely Buday 07 Sep '19

07 Sep '19

Hi, how does Muen relate to seL4? https://muen.codelabs.ch/ e.g. it claims to be the first verified microkernel. - Gergely

2 1

Issues about compile C program
by Zhonghao Liao 03 Sep '19

03 Sep '19

Hi, I am a graduate student and I am doing ainformation security related research project using SEL4. I installed the SEL4 kernel on a raspberry pie 3. The problem is that I can't compile C programs on this Raspberry Pi. Any suggestions for solving this problem? Thank you! Best, Zhonghao Liao

2 1

seL4 UART input (on RISC-V)?
by Ortiz, Baltazar 21 Aug '19

21 Aug '19

Hi all, I've been looking through the seL4 libraries and examples, and it seems to me that serial input should in some way be possible - the refos example appears to have a terminal, and I would imagine that debugging via GDB requires input in addition to output. However, the code to do this is unclear to me. Calling getchar() or similar leads to the unimplemented readv syscall, and calling __arch_getchar or similar causes a cap error even after running platsupport_serial_setup_simple(). Is there a step I'm missing? I'm specifically trying to get this working on RISC-V. Thanks, Baltazar ________________________________ Notice: This email and any attachments may contain proprietary (Draper non-public) and/or export-controlled information of Draper. If you are not the intended recipient of this email, please immediately notify the sender by replying to this email and immediately destroy all copies of this email. ________________________________

2 4

CapDL output to isabelle file
by Norrathep Rattanavipanon 20 Aug '19

20 Aug '19

Hello, I have been trying to generate Isabelle file from CapDL specification. But I run into an error when I'm running the command: ./parse-capDL --isabelle=out.thy --object-sizes=object_sizes.yaml example-arm.cdl warning: specifying untyped child multiple times is deprecated: ut = a, child = name warning: specifying untyped child multiple times is deprecated: ut = b, child = name warning: specifying untyped child multiple times is deprecated: ut = something, child = rm_ut parse-capDL: CapDL/PrintIsabelle.hs:180:15-71: Irrefutable pattern failed for pattern ut@(Untyped {maybePaddr = Just utPaddr}) where example-arm.cdl is the example I got from CapDL repo ( https://github.com/seL4/capdl/blob/master/capDL-tool/example-arm.cdl) And object_sizes.yaml contains: seL4_TCBObject: 10 seL4_EndpointObject: 4 seL4_NotificationObject: 4 seL4_SmallPageObject: 12 seL4_LargePageObject: 16 seL4_ASID_Pool: 12 seL4_ASID_Table: 10 seL4_Slot: 4 seL4_Value_MinUntypedBits: 4 seL4_Value_MaxUntypedBits: 29 seL4_PageTableObject: 10 seL4_PageDirectoryObject: 14 seL4_ARM_SectionObject: 20 seL4_ARM_SuperSectionObject: 24 seL4_IOPageTableObject: 12 seL4_IOPorts: 0 seL4_IODevice: 0 seL4_ARMIODevice: 0 seL4_IRQ: 0 seL4_IOAPICIRQ: 0 seL4_MSIIRQ: 0 The same error also occurs when I used parse-capdL executable generated by Camkes repo. Is there any step I'm missing? Or does the tool not support the conversion to Isabelle? Best, Norrathep -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

1 0

Shared memory in CapDL
by Norrathep Rattanavipanon 12 Aug '19

12 Aug '19

Hi, I have been reading Andrew Boyton's thesis about CapDL and realized that CapDL does not support a shared memory page. Is it still a limitation in CapDL/Camkes? Or has it somehow been addressed? Does this limitation include the case where a page is mapped/shared with different access rights? e.g., a page is mapped writable to one process and the same page is mapped only readable to another process? Best, Norrathep -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 5

How to use sel4runtime
by Ortiz, Baltazar 09 Aug '19

09 Aug '19

Hi all, Another (less exclusively RISC-V related, though I am targeting RISC-V still) question - I've been trying to figure out the sel4runtime repo, but I'm a bit confused on how to set it up. Specifically: * How much of a "minimal seL4 environment" do I need to initialize first? * Do does my program with main() also need to specify a root task, or is that part of the minimal environment? * Is there a specific recommended location for the sel4runtime repo? Thanks! Baltazar ________________________________ Notice: This email and any attachments may contain proprietary (Draper non-public) and/or export-controlled information of Draper. If you are not the intended recipient of this email, please immediately notify the sender by replying to this email and immediately destroy all copies of this email. ________________________________

1 0

SeL4 on 32 bit RISC-V
by Ortiz, Baltazar 09 Aug '19

09 Aug '19

Hi all, I'm looking into getting seL4 booting on 32 bit RISC-V. Currently working with seL4test 10.1.1, QEMU 4.0.0, and an upstream copy of riscv-gnu-toolchain (is there a specific release I should try?). I'm able to get seL4 to build after deleting a few CONST labels that the compiler was complaining about, but when I try to run the simulation script, I get the following output: > ./simulate -b /home/baltazar/qemu/build/riscv32-softmmu/qemu-system-riscv32 > /home/baltazar/qemu/build/riscv32-softmmu/qemu-system-riscv32 -machine spike_v1.10 -nographic -s -serial mon:stdio -m size=2000M -kernel images/sel4test-driver-image-riscv-spike > bbl loader > /host/sel4test-upstream-riscv/tools/riscv-pk/machine/minit.c:74: assertion failed: !(read_csr(misa) & fd_mask) > Power off Are there any tricks for getting this working right now? Thanks, Baltazar ________________________________ Notice: This email and any attachments may contain proprietary (Draper non-public) and/or export-controlled information of Draper. If you are not the intended recipient of this email, please immediately notify the sender by replying to this email and immediately destroy all copies of this email. ________________________________

3 5