August 2016 - Devel - lists.sel4.systems

up-to-date formal verification
by Horace Blanc 09 Aug '16

09 Aug '16

Hi, I would like to know if the verification of the seL4 is up-to-date with the newest version of the sel4 microkernel (3.2.0). If so, how do I access it? When I run make ASpec in l4v, I get a pdf with the Abstract Formal Specification in version 1.3. Does it refer to the seL4 microkernel version 1.3 or has the Abstract Formal Specification its own versions? Also, what is the best way to explore this specification in Isabelle/jedit? thanks in advance Horace Blanc

2 1

on Zynq
by Neelesh Vemula 08 Aug '16

08 Aug '16

Hi all, I am completely new with seL4, embedded systems as well as the fpga world. I am working on installing seL4 on Zynq fpga and use it. I have successfully able to boot up a "hello world" application using uboot(sd card bootup) on the zynq device. However, I have no clue as in how to setup communication between the sel4 logic and the PL(fpga fabric). If I am correct some sort of device driver has to be written or is there anything that is inbuilt or someone else who has worked on a similar project. Any guidance in this regard will be utmost helpful. Thanks a ton! Neelesh Vemula

2 1

capDL configuration file
by Norrathep Rattanavipanon 03 Aug '16

03 Aug '16

So I was reading capDL paper and it mentions about having a human-readable XML file for configuration of the initial thread which allows the system initialize into a know state. I assume this is not specific to camkes. so is there any way I can see/get the XML file and the code that generates it in the regular seL4? Thanks, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 1

memory map/unmap performance
by Yuxin Ren 02 Aug '16

02 Aug '16

Hi all, I am curious memory mapping/unmapping performance. Are there any applications that stress the memory mapping and unmapping utility? Thanks a lot! Yuxin

4 4