August 2019 - Devel - lists.sel4.systems

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