Re: [seL4] General Questions

Hi Steve, 1. Not sure what you count as simple, but assuming the initial thread knows it's own address space layout then it can easily work out which frame number this corresponds to in bootinfo. Typically this would be something like seL4_CPtr frame = bootinfo->userImageFrames.stat + ((uintptr

Re: [seL4] developing a Ethernet card server for seL4

Hi Peng, We at Data61 have not written any ethernet driver code for the TK1. Perhaps somebody else has? Adrian On Thu 15-Sep-2016 7:32 AM, PX wrote: Hi, all, We want to develop a networking service on top of seL4, which works as a hypervisor, on Jetson TK1. We know that there is source code fo

Re: [seL4] How to run seL4 as a hypervisor?

Hi Dan, Unfortunately we do not have yet have a real tutorial or documentation for using seL4 as a hypervisor. I can only recommend checking out one of our VM projects https://github.com/seL4proj/camkes-arm-vm-manifest or https://github.com/seL4/camkes-vm-manifest and looking at it to see how i

Re: [seL4] quesion about TK1 Linux irq

On Tue 27-Sep-2016 7:38 AM, PX wrote: 1. The linux_pt_irqs[] defined in tk1_vmlinux.h lists all the IRQs for I/O devices, but why they are different from TK1 manual? Does seL4 perform some mapping for guest Linux? Interrupts 0-31 are reserved by ARM, so we offset the interrupt numbers by 32.

Re: [seL4] questions about the device driver in virtual machine on ARM seL4 (TK1 board)

Hi Peng, I would prefer to say that the RAM used by the VM starts at physical address 0xb000, and is just one of many physical memory regions on the device. I'm not sure why you refer to a 'VM memory boundary' as no such thing exists, there are just many physical memory regions that are giv

Re: [seL4] questions about the device driver in virtual machine on ARM seL4 (TK1 board)

The default configuration for the TK1 is to lazily map in devices as the VMM detects faults. This setting can be seen by make menuconfig -> Libraries -> VMM Library for ARM -> Allow on demand installation This will cause the VMM to interpret any fault from Linux as an attempted device access and

Re: [seL4] sel4 hypervisor communication

Hi Horace, 1) Is there a mechanism for inter VM communication with seL4 as a hypervisor? There is a vchan (virtual channel) mechanism that, in our example VMM, is used to communicate between the VM and other components. If you had configured two VMMs to have two VMs then if you connected both o

Re: [seL4] endpoint.c

Hi Vasily, The kernel differentiates between fault instruction and next instruction in some cases. Might make more sense to just explain some different cases * If a thread is interrupted by a hardware interrupt, then it should start running again at the address of the next instruction that shou

Re: [seL4] adding code to the main.c for ARM VMM

On Tue 18-Oct-2016 8:36 AM, PX wrote: Hi, I have posted this question before and my problem is not totally solved because I am not familiar with Makefile. I try to make my question more specific as follows. I want to add new code, which is already organized under a directory, say, test. I want

Re: [seL4] Missing untypeds on x86?

Hi Jeff, What you are experiencing is a long standing set of limitations of seL4: * Limited (currently 512mb on ia32) kernel window * Static kernel window (i.e. memory cannot be swapped in and out) * Simple offset translation of kernel virtual addresses to physical addresses The result of these i

Re: [seL4] Larger badges on 64-bit?

On x86-64 I elected to keep badges at 28 bits initially just to provide a consistent kernel API. Aside from that there is no reason the badge size cannot be increased. Adrian On Thu 20-Oct-2016 7:32 AM, Corey Richardson wrote: Is there a future in which we recover the extra 32+ bits of padding

Re: [seL4] Allocman Error

Hi Neelesh, You need to give some untyped memory objects to allocman before it can create kernel objects. I would encourage you to try and use the 'bootstrap_use_current_simple' if possible (this is what we do in sel4test for example https://github.com/seL4/sel4test/blob/master/apps/sel4test-d

[seL4] Does anyone use recycle?

Hi All, If you do not know what recycle is and/or have not used it then you can probably ignore this e-mail. We are considering removing the recycle operation from cnodes, and replacing it with a 'revoke badges' operation. Currently the semantics of recycle are ill defined but can generally be

Re: [seL4] Does anyone use recycle?

Hi Jeff, The difference is that recycle does not require you to keep around (or be given) the untyped in order to then be able to perform the retype. Recycle is also a single syscall, and thus has better performance, than revoke + retype. Adrian On Wed 26-Oct-2016 3:11 PM, Jeff Waugh wrote: On

Re: [seL4] Does anyone use recycle?

Right. I don't think we have measured the performance recently so I cannot comment off the top of my head, but at the same time I cannot think of a reason for why it would have changed. Adrian On Wed 26-Oct-2016 3:46 PM, Jeff Waugh wrote: On Wed, Oct 26, 2016 at 3:37 PM, mailto:adrian.da...@da

Re: [seL4] CallWithMRs is an unexercised code path

Hi Jeff, We really like the *WithMRs functions and there is no plan to get rid of them. Support for the syscall stub generator using them was removed here (https://github.com/seL4/seL4/commit/5271925ba54639b849261e652e73ab56ee243fb2). Not being able to get error information after doing an invoc

Re: [seL4] CallWithMRs is an unexercised code path

To give a bit more detailed explanation. Take the Page_Map invocation, more concretely let's look at seL4_ARM_Page_Map in the case where we do not pass --buffer LIBSEL4_INLINE long seL4_ARM_Page_Map(seL4_X86_Page service, seL4_CPtr vroot, seL4_Word vaddr, seL4_CapRights rights, seL4_ARM_VMAttri

Re: [seL4] CallWithMRs is an unexercised code path

On Thu 27-Oct-2016 1:12 PM, Jeff Waugh wrote: On Thu, Oct 27, 2016 at 12:08 PM, mailto:adrian.da...@data61.csiro.au>> wrote: Now here's the problem. We want message register two. But on ARM, the first 4 message registers are done actually in register (not the IPC buffer). When we called seL4_C

Re: [seL4] need ideas

On Tue 01-Nov-2016 7:37 AM, Vasily A. Sartakov wrote: as you might see, this is little bit modified version of trivial.c tests. Usual, when I am testing all tests, there is no problem with this test. But when I am running this file alone, I have a problem. Also, you might see, that there are

Re: [seL4] malloc and SCHED0004

Hi Vasily, We have made some changes to muslc. If you diff against changeset '615629bd6fcd6ddb69ad762e679f088c7bd878e2' you can see them. In particular there are some changes to malloc that you could try reverting. Adrian On Fri 04-Nov-2016 8:58 AM, Vasily A. Sartakov wrote: Greetings. I am

Re: [seL4] malloc and SCHED0004

I don't understand what you are saying. If you're on a recent version of seL4 then that commit should definitely be there, as it's a merge from december last year. Also don't see how MCP is relevant, it caused zero changes to muslc. Adrian On Fri 04-Nov-2016 10:19 AM, Vasily A. Sartakov wrote:

Re: [seL4] malloc and SCHED0004

So a git diff 615629bd6fcd6ddb69ad762e679f088c7bd878e2 b5c66eef4a8bb274d7a4b9b5b82bce412224dbf9 will let you see all the changes we have made from the base muslc, or just git diff 615629bd6fcd6ddb69ad762e679f088c7bd878e2 b5c66eef4a8bb274d7a4b9b5b82bce412224dbf9 -- src/malloc/malloc.c to see t

Re: [seL4] Will seL4_Word ever be anything but uintptr_t?

Yep the size of a word_t (the equivalent of seL4_Word in the kernel) has many assumptions being large enough to hold a pointer. As a result you can rely on seL4_Word always being the size of a pointer. This isn't a guarantee that it will be the same type as uintptr_t, but it will be at least the

Re: [seL4] IPC measurements

On Mon 28-Nov-2016 9:20 AM, Neelesh Vemula wrote: Queries: 1) I have found the sample benchmark numbers for seL4 IPC from http://l4hq.org/docs/performance.php. Since I am running on Armv7 Cortex A9 , the time for one half way trip is 316 ns. Is this measured from system call to system call or

Re: [seL4] contiguous physical memory allocation for seL4

There is a fairly simplistic memory allocator in the form of a DMA allocator in libsel4utils that operates basically as you describe. See: https://github.com/seL4/seL4_libs/blob/master/libsel4utils/include/sel4utils/page_dma.h It requires you to be using various other abstractions for allocation

Re: [seL4] Huge kernel images no more

Bit embarrassing that it was so large for so long. I feel like 1M is still a bit large, although nothing jumped out at me when I looked at the symbol list so maybe it's fine. Don't be discouraged from more poking though. Adrian On Tue 06-Dec-2016 9:24 AM, Jeff Waugh wrote: Hurrah, I was curiou

Re: [seL4] Virtio on camkes-vm

Answers inline On Thu 08-Dec-2016 1:32 AM, Robert VanVossen wrote: Hello, We are looking to add another virtio device to camkes-vm for guests to use. I have been looking through the code at how virtio_net works and I have a pretty decent understanding of how it is configured and used. I have a

Re: [seL4] Exposing ticks to the rt API

Hi Corey, I will attempt to provide you with what answers I can, although I'm not the expert in this so Anna may say that all of this is wrong later One important thing to consider for Real Time is not just the accuracy of the timer, but the Worst Case Execution Time of the kernel and any paddi

Re: [seL4] pic/no-pic and some other questions

Hi Vasily, I've put replies inline On Mon 26-Dec-2016 9:37 AM, Vasily A. Sartakov wrote: Greetings. I have merged MIPS port with 4.0.0 release. Now I would like to clean up my code and need to remove many small issues that I did not fix during the porting before making the code public. In fac

Re: [seL4] Exposing TSD on x86

I think the only concern with this is it still adds more checks and conditionals to the thread switching code. Whilst minimal, these can add up with enough features like these, so would want some decent motivation. That said, having the support be a build time option would somewhat circumvent t

Re: [seL4] seL4test on Odroid-XU4

Hi Yevgeny, We cannot provide much assistance as you are developing on a platform that we simply do not have. You say the 'test suite failed for some reason' but you do not elaborate. Did the test suite fail to produce any output, did one of the tests report a failure, did the test suit pause m

Re: [seL4] questions about the address translation for a DMA driver in the ARM VM

Hi Peng, I do not fully understand all your questions, so will provide some generic responses. Our example ARM VMM runs on two platforms, which have different kinds of support for DMA. On the odroid-xu the VMM sets up the guest such that it has a 1-to-1 mapping, that is the IPA mappings are se

Re: [seL4] questions about the address translation for a DMA driver in the ARM VM

Hi Peng, If you want to find user level code that deals with the SMMU then looking for code guarded by the kernel config option for the SMMU (CONFIG_ARM_SMMU) would be the place to start. Adrian On Thu 05-Jan-2017 11:58 AM, PX wrote: Adrain, You answer is exactly what I want to know. For the T

Re: [seL4] xsave region size for haswell/broadwell?

Hi Corey, On a haswell machine here with AVX+SEE+FPU state I get an xsave region size of 832 Adrian On Fri 06-Jan-2017 12:55 PM, Corey Richardson wrote: Does anyone have a "maximal" xsave region size big enough for all the xsave-supporting features seL4 enables on Broadwell or Haswell? I don't

Re: [seL4] Overly eager xsave size rejection

Hi Corey, The original intention of the 'aggressive' check was to somewhat prevent your case where the user has set the size higher than required and may be inadvertently be wasting memory by having the TCBBits end up larger than needed. I agree that it can be a little inconvenient, so will cha

Re: [seL4] seL4 as Xen guest / AWS

Hi Tony, My tongue in cheek response would be to say that you are doing this backwards and you should be wanting to run Xen on seL4. More seriously though, what is the value that seL4 is providing in this setup? What are the specific threat scenarios that seL4 is mitigating against? If you are

Re: [seL4] Overly eager xsave size rejection

On Tue 10-Jan-2017 2:20 PM, Corey Richardson wrote: On 01/09/2017 12:37 AM, adrian.da...@data61.csiro.au wrote: Hi Corey, The original intention of the 'aggressive' check was to somewhat prevent your case where the user has set the size higher than requir

Re: [seL4] config-independent object type numbers

The reason the numbers are not fixed is that the kernel knows whether or not an object type is valid by checking a range. For example one of the first checks in the decode untyped path is /* Is the requested object type valid? */ if (newType >= seL4_ObjectTypeCount) { userError("U

Re: [seL4] Kernel won't boot on Qemu/KVM Ivy Bridge

On Tue 10-Jan-2017 3:52 PM, Corey Richardson wrote: This kernel doesn't even seem to boot at all with -cpu host -enable-kvm (or -cpu IvyBridge), regardless of the configuration. Curiously, with -cpu SandyBridge -enable-kvm, it does boot. It seems to be a qemu bug. It seems to be stuck in some s

Re: [seL4] ARM LPAE?

Hi Wladislav, The short answer is that LPAE is not currently used or supported by seL4 and so you will not be able to describe physical memory that resides above 4gb to it. Adrian On Fri 13-Jan-2017 12:20 AM, Wladislav Wiebe wrote: Hello, I am trying to integrate TI Keystone 2 platform to seL

Re: [seL4] questions about PCIE SMMU for tk1 vmm

Hi Peng, The ASIDs defined in smmu.h are arbitrary and defined by the kernel. They get loaded into the different SMMUs as the IOASID for the particular SMMU. Can you explain in what way the PCIE device has the 0 IOASID? Adrian On Mon 16-Jan-2017 10:00 AM, PX wrote: Hi, I am confused by the SMM

Re: [seL4] seL4 System Utilization / Benchmark

Hi Andrew, There is some code already in the kernel to help you do this, although it is tested and fixed on an as used basis so may or may not work as I describe. You can enable the the thread utilization tracking with make menuconfig -> seL4 Kernel -> Build Options -> Enable benchmarks -> Track

Re: [seL4] seL4 System Utilization / Benchmark

Unfortunately the kernel does not have a way of finding all the TCBs that have been created in the system. You would have to manipulate the TCB creation/deletion code to maintain a linked list of all the created TCBs. To call raw system calls just make sure you #include and then yes, you can j

Re: [seL4] questions about SMMU on TK1 VMM

On Wed 18-Jan-2017 7:55 AM, PX wrote: Hi, I have some questions about the SMMU on the new version of TK1 VMM as follows: 1. In the source code, smmu.c, the IO ASID 1 is assigned to hardware engine, AFI, which is supposed to connect with PCIE devices. However, when I add 1 to vm.smmu in vm.

Re: [seL4] CAmkES Templates

Hi Chris, For the 'pbuf_alloc' linker error can you confirm that the component is having 'lwip' added as a LIBS dependency. For example in the camkes-vm in projects/vm/components/UDPServer/UDPServer.mk there is the line UDPServer_LIBS := sel4camkes ethdrivers lwip sel4vspace This is what actuall

Re: [seL4] SDHC drivers (cont.)

Hi Oak, I don't know much about SD cards or this driver but it seems to me like passing it a physical address of 0 isn't what you want, and whilst I know nothing about the mmc hardware it seems reasonable to me that it might hang trying to DMA to memory that doesn't exist. There is also the add

Re: [seL4] strange code in thread.c

Us here at Data61 watch github, I suspect many other people on the mailing list don't though. With that in mind feel free to use whichever you feel is most appropriate. Bear in mind that despite our best efforts there will be sometimes be delays in our ability to respond on either. Adrian On

Re: [seL4] Deriving and Revoking IRQControl caps

I have done hunting in both the kernel and the capDL-loader and can shed some light on what is going on. On the kernel side there is implicit knowledge that an IRQHandler is the child of an IRQControl cap, so the single bit of depth does not get used up here. As a result you should be able to ta

Re: [seL4] Boot Hyp mode in elfloader

Hi Yao, Can you confirm in the build configuration that 'seL4 mode' is set to 'Load the seL4 kernel in hypervisor mode (NS))' and 'Install hooks in monitor mode' in set? These should be set by the provided defconfigs. Also you can elaborate on what 'died here' means? Is there anything else outp

Re: [seL4] Boot Hyp mode in elfloader

Hi Yao, Glad you got it working and thanks for discovering that. We will look into what is going on. Adrian On Mon 27-Feb-2017 3:27 PM, SHI, Yao wrote: I was using u-boot 2017-03-rc1. After flashing back to 2015-10-rc5, camkes-arm-vm works. So the problem is the new u-boot...though I don't kno

Re: [seL4] Questions about userspace memory allocation

Hi Daniel On Tue 11-Apr-2017 1:33 AM, Daniel (Xiaolong) Wang wrote: Hi all, I have a couple questions hope someone can help me clear it out. I understand that after booting up, the kernel keep tracking of all physical memory as Untyped and hand it over to the init thread. It seems like the ker

Re: [seL4] sel4test failing TEST_SCHED0004 on iMX6

Hi Robert, I am unable to reproduce this failure. Can I ask what host system and toolchain you are using? Also which of the configs in sel4test? Adrian On Mon 17-Apr-2017 6:03 PM, Robert Kaiser wrote: Hi all, I just tried to run the test suite on iMX6. Using the current version from github, I

Re: [seL4] questions about TK1 VM

Hi Peng, 1. TLB status is irrelevant 2. Contents of registers from seL4_UserContext are always just literally what that thread had in its registers, no translation in any direction is done by the kernel Adrian On Thu 27-Apr-2017 7:05 AM, PX wrote: Hi, all I have some questions about TK1 VM. I

Re: [seL4] Change Access Right to Memory Pages

Hi Oak, 1. Looks fine to me. You can test the permissions yourself though by attempting to write to that page before and after the Remap 2. Unfortunately no, there is no more efficient way in seL4. Only suggestion I can make is use larger pages where possible 3. Since you have not specified I wi

Re: [seL4] Can I running camkes-arm-vm on HiKey board

Hi, I'm not sure what you mean by 'possible'. A port is definitely possible, but so is just about anything. Are you asking if it will require kernel changes? That I'm not sure of. Certainly if you want SMMU support you will need to provide an implementation of that for the HiKey platform (if it

Re: [seL4] CapDL Spec Error

Hi Chris, Sorry for not replying earlier, but glad you found a solution. Can I ask if you're using a particular version of CAmkES, or the tip of master? We noticed this problem previously on CAmkES a bit after adding that configuration option, but thought we fixed it. So curious if this is from

Re: [seL4] CapDL Spec Error

Hi Chris, Looks like the seL4MultiSharedData template didn't get updated. It's missing a call to `keep_symbol` in the template. See https://github.com/seL4/camkes-tool/blob/next/camkes/templates/seL4SharedData-from.template.c#L32 in the seL4SharedData template. Something similar should be at h

Re: [seL4] About timer tests (CONFIG_HAVE_TIMER) in sel4test testsuites

Hi Jesse, The ARM generic timer is typically used by the kernel as its timer source for scheduling preemption. The CONFIG_HAVE_TIMER require an additional timer that is passed to user level. On the TK1 this is TMR1, on the hikey its the DMTIMER, on other platforms it's the EPIT etc. What timer

Re: [seL4] Running multiple VMs under ARM and C++ under SeL4?

Hi John, The ARM VMM does not currently support multiple virtual machines, this is something we are working on adding. To properly use the C++ standard template library you would need to build a cross compiler for a CAmkES system based seL4 system. This is something we have never done. Whether

Re: [seL4] Running Linux on top of seL4

Hi Dan, We use both the Jetson TK1 and TK1-SOM internally. Adrian On Sat 03-Jun-2017 6:38 AM, Daniel Wang wrote: Sorry one more question: Can the Jetson TK1 (or other cheaper board) being used for running Linux Virtualization on top of seL4? I’m not familiar with TK1 board, it is kind of costl

Re: [seL4] Temporally disable write-access on memory pages

Hi Oak, The seL4 kernel does not have such primitives. You would need to build something with those semantics at user level. Typically you would do this by revoking authority and then granting it again. I don't understand how your system is structured if your initial process (which I guess is t

Re: [seL4] vmm documentation

Hi Mike, Unfortunately we haven't yet written any documentation on the VMM internals or how it works. You are actually the first person to express interest in this. Will try to make it a higher priority to write at least a brief overview of the structure. For now my advice is to be familiar wit

Re: [seL4] seL4_Fault_t and friends seems to be missing in user libsel4

Hi Alexander, They get generated as part of the compilation of the libsel4 library, which is separate to the kernel compilation. See the libsel4 Makefile (https://github.com/seL4/seL4/blob/master/libsel4/Makefile) Adrian On Wed 14-Jun-2017 1:32 AM, Alexander Boettcher wrote: Hello, if I comp

Re: [seL4] Compilation of seL4 kernel 5.2.0

Hi Alexander, Building the kernel standalone is not really supported at the moment except for the few configurations where the kernel has been or is intending to be verified. x86-64 is a verification target, and so has a working standalone build, ia32 is not. In particular the standalone build

Re: [seL4] seL4_Fault_t and friends seems to be missing in user libsel4

Hi Alex, Yes libsel4 assumes it is being built as part of our larger common project build environment (https://github.com/seL4/seL4_tools/tree/master/common-tool). Again the build system improvements that I said were coming should also solve this, so if you've managed to find a work around for

Re: [seL4] seL4test with 4.0, 5.1 failed on Ubuntu

Hi Dan, Can you please be more precise as to which configuration you are trying to build, as there are several configurations that start with the name kzm_simulation. I tried a few different configurations on a few different versions but was unable to reproduce your specific build error, althou

Re: [seL4] Questions about TK1-SOM Memory Management

Hi Daniel, The physical memory is indeed a bit strange. This is for two reasons 1. As described in the comment directly above '1 MiB starting from 0xa7f0 is reserved by the elfloader for monitor mode hooks', so a continuous region from 0x8000 - 0x could not legally be given 2.

Re: [seL4] network on seL4

Hi Gabor, This is a bit a late reply so not sure if it's still helpful but with LWiP I would suggest looking at LWiP Bare Metal and its Native API http://lwip.wikia.com/wiki/Porting_For_Bare_Metal http://lwip.wikia.com/wiki/Raw/native_API You can also see an example of a raw UDP setup here http

Re: [seL4] Recursive call to malloc crash system

Stepping back slightly I am going to argue that fundamentally the issue here is that the heap is being used in a place where the stack should be. In this case due to vspace_new_pages having to allocate a reservation to do the mapping, only to immediately free the reservation in the same function

Re: [seL4] VGA buffer as stdout

Assuming you are talking about text mode VGA then having the kernel render to such a buffer is not particularly difficult. Instead of the 0xB8000 address though I would consider using the supposed multiboot video mode, and perhaps falling back to the buffer at 0xB8000 if no multiboot video mode

Re: [seL4] UEFI support for x86

Hi Edward, In the near future? Unfortunately not. UEFI support is definitely something that we talk about every so often, but just never makes it high enough up the priority list for us internally. A configuration option for overriding the RSDP search doesn't so too unreasonable in cases where

Re: [seL4] x86_64 kernel crash

Hi Alex, Many thanks for the detailed report. I should point out that the x86-64 version of the kernel is presently undergoing verification and so is not yet up to the same guarantees as the verified ARM platforms. I will look into this right away and let you know how I go. Adrian On Fri 25-

Re: [seL4] benchmark - idle utilization

Hi Alex, The benchmarking infrastructure is very much a 'add what we need when we need it' style. As it's not part of the verified set of code can change it to be and do anything you want. For the first change you mention, it probably does make more sense to return the idle time of the request

Re: [seL4] UEFI support for x86

Hi Alex, I think this is a good direction to move in, and supporting MBI2 definitely makes sense. In an ideal world, yes we would try and cut out grub2 and be pure UEFI booted, but given current resources I cannot see that happening any time soon, and so I see no reason not to welcome MBI2 supp

Re: [seL4] x86_64 kernel crash

Hi Alex, I have tracked this down to the kernel failing to unmap pages in some cases when deleting frame caps, specifically it would only unmap if deleting the last capability to a frame, which is clearly wrong. As you say, this was only able to manifest as a problem because your user space was

Re: [seL4] benchmark - idle utilization

Periodically sampling without resetting is fine, it just exposes the issue you noticed where if nothing is ever run on a core then its utilization will be incorrect. But I think the incorrect idle utilization should be easily fixed separately, and you can keep sampling how you are. For a quick

Re: [seL4] Problem making the manual

Hi Raymond, Can you please say what commit of the seL4 repository you are using. Adrian On Wed 13-Sep-2017 2:48 PM, Raymond Jennings wrote: I got an error log when I tried "make" in the manual directory. I got this: > Generating doxygen-output/xml/group__GeneralSystemCalls.xml > Genera

Re: [seL4] Some questions regarding seL4, U-Boot, and Raspberry Pi 3 patches

Hi Austin, Thanks for the detective work! seL4 (or more specifically in this case the elfloader-tool) should be able to tolerate being started with either the cache enabled or disabled. In fact if you look in the mmu code (https://github.com/seL4/seL4_tools/blob/master/elfloader-tool/src/arch-

Re: [seL4] Some questions regarding seL4, U-Boot, and Raspberry Pi 3 patches

Hi Austin, In terms of workarounds right now you can obviously still use older U-boot, or use the `mkimage` as suggested by you. For the medium term I am in favor of telling people to use `mkimage`, as it's also available right now and there's no 'clean up' to be done once there is a proper fix

Re: [seL4] Raspberry pi 3 compilation error

Hi Parthamesh, Can I ask what version of the arm-linux-gnueabi toolchain you are using? Or if you changed it from the default, the version of whichever toolchain you are using. Adrian On Fri 22-Sep-2017 7:11 PM, Prathamesh Rahate wrote: > Hi, > I am trying to cross-compile seL4 for rapsberry p

Re: [seL4] General question about software

Hi Raymond, seL4 is a general purpose microkernel, which means that it supports any architecture you wish to put on top of it. These architectures can vary on many axis of dynamism, componentisation etc. The 'typical' architecture therefore is hard to pin down, as it depends upon how you want t

Re: [seL4] Sel4 compilation error for RasperryPi-3

Hi Ashok, It looks like you are trying to perform an in tree 'make' build directly in a seL4 kernel checkout. This is not a recommended way to build the kernel in general, and is only meant to be used for some very specific configurations right now. Standalone kernel compilation support is bein

Re: [seL4] Integer overflow bug in capdl-loader

Hi Jeff, The change looks good to me. Have applied it internally and will let it go through CI. Thanks! Adrian On Thu 28-Sep-2017 6:08 AM, Jeff Kubascik wrote: > Hello, > > I am working with seL4 7.0.0 on the zynq7000 platform. I have come across a > bug > that occurs when a device physical

Re: [seL4] ARM 64-bit Support in seL4

You can also run sel4test (https://wiki.sel4.systems/Getting%20started#Get_acquainted_with_seL4Test) on two aarch64 platforms (hikey and jetson tx1), with the tx1_aarch64_* and hikey_aarch64_* defconfigs. Adrian On Fri 29-Sep-2017 9:29 AM, kofidoku.at...@data61.csiro.au wrote: > Hey Keith, >

Re: [seL4] CAmkES mutex Question

Hi Brandon Sorry for the delay, have put some answers inline. Hope they are still of some use to you On Thu 26-Oct-2017 7:30 AM, Brandon, Jeffrey - 0553 - MITLL wrote: > Hi, > > > > I've been taking a look at mutex implementations in the camkes-app example > and I had a question. > > >

Re: [seL4] seL4SharedData

Hi Zippy, I appreciate what you are trying to do and the problems with the currently available solutions. Unfortunately I do not see any solutions beyond those you have already identified. Whilst I would love to provide you with a workable solution, we do not have the resources to develop addit

Re: [seL4] camkes-gen.mk generated prerequisites

Hi Gordon, There is no way you can structure things right now to avoid recompiling as currently all generated files just depend upon every CAmkES input file. As you have noticed, this means if you change any part of your system specification, you must regenerate every file. However, if you are

Re: [seL4] seL4 bring up on inmate cell of jailhouse.

Hi Munees, My understanding is that you cannot run unmodified guest operating systems as inmates under jailhouse. In my brief look at jailhouse I did not find any documentation of the platform that jailhouse presents to the inmates and the corresponding binary interface beyond "install this ker

Re: [seL4] Questions about Tx1 Physical Memory usage

Hi Munees, I'm not sure why the TX1 has such a small amount of memory specified. Presumably it was just copied from the TK1 and no one got around to updating it. Certainly more memory can be specified, although I would take into account a couple of things * Whilst we do not currently setup a

Re: [seL4] Questions concerning the capability management system

Hi Timotej, The source code of Aurora probably exists somewhere and could be dug up, but I personally have never seen it, and it has not been used by this group in any systems after the author. That presentation presents a core problem of resource management in seL4, this three way problem can

Re: [seL4] Dynamic Loading of application

Hi Vishal, The elfloader is designed to run with full hardware access in the way it allocates memory whilst unpacking the elf image. It also has a lot of code to place the machine into a known state (manipulating caches and MMUs etc) prior to the kernel running. A seL4 application must talk to

Re: [seL4] x86 kernel address space side channels

Hi Corey, It is definitely an interesting problem, although only occurs since Linux 'relies' on ASLR in the kernel for security due to running untrustworthy code in kernel mode. seL4 does not implement KASLR, as seL4 does not have the classes of bugs that ASLR attempts to mitigate the exploitab

Re: [seL4] python-capdl sets incorrect permissions on elf setions

Hi Joseph, This is not incorrect behaviour. The permissions describe how the program will use these different sections, and is not a requirement that they be mapped this way. For example saying a section is "read only" allows an OS to know the data in that section isn't modified and share the s

Re: [seL4] CamkesVM: EthDriver and Firewall

Hi Michal, The EthDriver returns and takes raw ethernet frames and is essentially acting as a fairly thin wrapper around the hardware descriptor rings. The Firewall component has been used and works, although it currently does not act much as a firewall due to just passing through all packets in

Re: [seL4] Fwd: CamkesVM CMA34CR_centos app

Hi Michal, It is strange that there is no further output, although I am worried about the IOMMU faults that happen just prior to that. On some systems certain devices (notably USB controllers) can lock parts of the system if they are unable to function correctly. My suggestion would be to resol

Re: [seL4] Questions about Allocman

Hi Daniel, The physical address is not necessarily stored anywhere, as this is dependent on the specific untyped manager. There is an interface function `allocman_utspace_paddr` (https://github.com/seL4/seL4_libs/blob/master/libsel4allocman/include/allocman/allocman.h#L410) that will call into

Re: [seL4] CapDL spec for Camkes-ARM-VM

Hi Daniel, The camkes-arm-vm project is built on CAmkES, which has a high level system assembly specification that gets compiled down into capDL. If you search your build directory you can find the 'vm.cdl' file that CAmkES generates. It is very much *not* recommended that you attempt to manual

Re: [seL4] Compilation Error with version

Hi Thad, Can you please provide steps to reproduce this. Adrian On Thu 08-Mar-2018 4:01 AM, Thad Seeberger wrote: > Good day. I am getting hung up compiling the CAmkES compiles. I'm getting > following error which I believe is because the version.h.d does not exist. > Where is the version set? >

Re: [seL4] Compilation Error with version

Hi Daniel, The accelerator was changed in a way that requires some newer cmake features, but the cmake minimum required version (https://github.com/seL4/camkes-tool/blob/master/tools/accelerator/CMakeLists.txt#L15) was not updated resulting in this non-intuitive failure. The minimal cmake vers

Re: [seL4] Questions about Allocman

Sorry aside from the comments scattered through various files there is no other documentation. Adrian On Sat 10-Mar-2018 7:06 AM, Vasily A. Sartakov wrote: > Hello > >> >> The physical address is not necessarily stored anywhere, as this is >> dependent on the specific untyped manager. There is

  1   2   >