Help me!
I am running sel4test on my TX1 according to the official tutorial, but I get a problem again and again. For the newly purchased TX1, I directly connected my Ubuntu host with UART serial port.
At the same time, I follow this instruction ( https://docs.sel4.systems/Hardware/jetsontx1.html ), pulled the latest sel4test project code, successfully ran ninja command and built images "sel4test-driver-image-arm-tx1". Everything seemed to be going very smoothly. I use the newly purchased SanDisk 64GB SD card to boot my image, which has been formatted in ext4 format.
Then I use command `sudo screen / dev / ttyusb0 115200` to open the UART serial port. After pressing and holding the power key for 1 second, and TX1 starts. Then I hit the Enter key to make TX1 cancel the auto boot default image and enter the u-boot interactive command line.
Then, according to the instruction, under uboot, I typed the following command to load the image and start from the address 0x82000000:
```
ext4load mmc 1 0x82000000 sel4test-driver-image-arm-tx1
go 0x82000000
```
Finally, I failed to start sel4test as I wanted. After many repetitions, I got the same error. This is my output：
------------------------------------------------------------------------------------------------------------------------------------------
Tegra210 (P2371-2180) # ext4load mmc 1 0x82000000 sel4test-driver-image-arm-tx1
5247256 bytes read in 260 ms (19.2 MiB/s)
Tegra210 (P2371-2180) # go 0x82000000
## Starting application at 0x82000000 ...
ELF-loader started on CPU: ARM Ltd. Cortex-A57 r1p1
paddr=[80a57000..80f58117]
No DTB passed in from boot loader.
Looking for DTB in CPIO archive...found at 80b825e0.
Loaded DTB from 80b825e0.
paddr=[8023d000..8024afff]
ELF-loading image 'kernel' to 80000000
paddr=[80000000..8023cfff]
vaddr=[ffffff8080000000..ffffff808023cfff]
virt_entry=ffffff8080000000
ELF-loading image 'sel4test-driver' to 8024b000
paddr=[8024b000..80661fff]
vaddr=[400000..816fff]
virt_entry=40f0b8
Enabling MMU and paging
Jumping to kernel-image entry point...
Warning: gpt_cntfrq 19200000, expected 12000000
Bootstrapping kernel
available phys memory regions: 2
[80000000..ff000000]
[100000000..180000000]
reserved virt address space regions: 3
[ffffff8080000000..ffffff808023d000]
[ffffff808023d000..ffffff808024b000]
[ffffff808024b000..ffffff8080662000]
seL4 failed assertion 'cap_get_capType(destSlot->cap) == cap_null_cap' at /home/yjy/Desktop/sel4-rpi/sel4test_newv2/kernel/src/object/cnode.c:426 in function cteInsert
halting...
Kernel entry via Interrupt, irq 0
------------------------------------------------------------------------------------------------------------------------------------------
I'm about to collapse. I really need your help. How can I solve this problem?
1. Why did I get this warning？ "Warning: gpt_cntfrq 19200000, expected 12000000" , It exists in this file "/sel4test/kernel/src/drivers/timer/generic_timer.c:21"
2. About reporting errors "failed assertion 'cap_get_capType(destSlot->cap) == cap_null_cap'". I found that the variable "(slot_ptr_t) (rootserver.tcb) ) -> cap.words[0] " is equals to 0xffffffffffffffff, so that the cap_get_capType(destSlot->cap) <=> (slot_ptr_t) (rootserver.tcb) ) -> cap.words[0] & 0x1full != 0 . I guess it caused the mistake, but i don't know why.
I'm about to collapse. I really need your help. How can I solve this problem?
I'm sorry for sending this email again!
Help me!
I am running sel4test on my TX1 according to the official tutorial, but I get a problem again and again. For the newly purchased TX1, I directly connected my Ubuntu host with UART serial port.
At the same time, I follow this instruction ( https://docs.sel4.systems/Hardware/jetsontx1.html ), pulled the latest sel4test project code, successfully ran ninja command and built images "sel4test-driver-image-arm-tx1". Everything seemed to be going very smoothly. I use the newly purchased SanDisk 64GB SD card to boot my image, which has been formatted in ext4 format.
Then I use command `sudo screen / dev / ttyusb0 115200` to open the UART serial port. After pressing and holding the power key for 1 second, and TX1 starts. Then I hit the Enter key to make TX1 cancel the auto boot default image and enter the u-boot interactive command line.
Then, according to the instruction, under uboot, I typed the following command to load the image and start from the address 0x82000000:
```
ext4load mmc 1 0x82000000 sel4test-driver-image-arm-tx1
go 0x82000000
```
Finally, I failed to start sel4test as I wanted. After many repetitions, I got the same error. This is my output：
------------------------------------------------------------------------------------------------------------------------------------------
Tegra210 (P2371-2180) # ext4load mmc 1 0x82000000 sel4test-driver-image-arm-tx1
5247256 bytes read in 260 ms (19.2 MiB/s)
Tegra210 (P2371-2180) # go 0x82000000
## Starting application at 0x82000000 ...
ELF-loader started on CPU: ARM Ltd. Cortex-A57 r1p1
paddr=[80a57000..80f58117]
No DTB passed in from boot loader.
Looking for DTB in CPIO archive...found at 80b825e0.
Loaded DTB from 80b825e0.
paddr=[8023d000..8024afff]
ELF-loading image 'kernel' to 80000000
paddr=[80000000..8023cfff]
vaddr=[ffffff8080000000..ffffff808023cfff]
virt_entry=ffffff8080000000
ELF-loading image 'sel4test-driver' to 8024b000
paddr=[8024b000..80661fff]
vaddr=[400000..816fff]
virt_entry=40f0b8
Enabling MMU and paging
Jumping to kernel-image entry point...
Warning: gpt_cntfrq 19200000, expected 12000000
Bootstrapping kernel
available phys memory regions: 2
[80000000..ff000000]
[100000000..180000000]
reserved virt address space regions: 3
[ffffff8080000000..ffffff808023d000]
[ffffff808023d000..ffffff808024b000]
[ffffff808024b000..ffffff8080662000]
seL4 failed assertion 'cap_get_capType(destSlot->cap) == cap_null_cap' at /home/yjy/Desktop/sel4-rpi/sel4test_newv2/kernel/src/object/cnode.c:426 in function cteInsert
halting...
Kernel entry via Interrupt, irq 0
------------------------------------------------------------------------------------------------------------------------------------------
Help me!
I am running sel4test on my TX1 according to the official tutorial, but I get a problem again and again. For the newly purchased TX1, I directly connected my Ubuntu host with UART serial port.
At the same time, I follow this instruction ( https://docs.sel4.systems/Hardware/jetsontx1.html ), pulled the latest sel4test project code, successfully ran ninja command and built images "sel4test-driver-image-arm-tx1". Everything seemed to be going very smoothly. I use the newly purchased SanDisk 64GB SD card to boot my image, which has been formatted in ext4 format.
Then I use command `sudo screen / dev / ttyusb0 115200` to open the UART serial port. After pressing and holding the power key for 1 second, and TX1 starts. Then I hit the Enter key to make TX1 cancel the auto boot default image and enter the u-boot interactive command line.
Then, according to the instruction, under uboot, I typed the following command to load the image and start from the address 0x82000000:
```
ext4load mmc 1 0x82000000 sel4test-driver-image-arm-tx1
go 0x82000000
```
Finally, I failed to start sel4test as I wanted. After many repetitions, I got the same error. This is my output：
------------------------------------------------------------------------------------------------------------------------------------------
Tegra210 (P2371-2180) # ext4load mmc 1 0x82000000 sel4test-driver-image-arm-tx1
5247256 bytes read in 260 ms (19.2 MiB/s)
Tegra210 (P2371-2180) # go 0x82000000
## Starting application at 0x82000000 ...
ELF-loader started on CPU: ARM Ltd. Cortex-A57 r1p1
paddr=[80a57000..80f58117]
No DTB passed in from boot loader.
Looking for DTB in CPIO archive...found at 80b825e0.
Loaded DTB from 80b825e0.
paddr=[8023d000..8024afff]
ELF-loading image 'kernel' to 80000000
paddr=[80000000..8023cfff]
vaddr=[ffffff8080000000..ffffff808023cfff]
virt_entry=ffffff8080000000
ELF-loading image 'sel4test-driver' to 8024b000
paddr=[8024b000..80661fff]
vaddr=[400000..816fff]
virt_entry=40f0b8
Enabling MMU and paging
Jumping to kernel-image entry point...
Warning: gpt_cntfrq 19200000, expected 12000000
Bootstrapping kernel
available phys memory regions: 2
[80000000..ff000000]
[100000000..180000000]
reserved virt address space regions: 3
[ffffff8080000000..ffffff808023d000]
[ffffff808023d000..ffffff808024b000]
[ffffff808024b000..ffffff8080662000]
seL4 failed assertion 'cap_get_capType(destSlot->cap) == cap_null_cap' at /home/yjy/Desktop/sel4-rpi/sel4test_newv2/kernel/src/object/cnode.c:426 in function cteInsert
halting...
Kernel entry via Interrupt, irq 0
------------------------------------------------------------------------------------------------------------------------------------------
I'm about to collapse. I really need your help. How can I solve this problem?
1. Why did I get this warning？ "Warning: gpt_cntfrq 19200000, expected 12000000" , It exists in this file "/sel4test/kernel/src/drivers/timer/generic_timer.c:21"
2. About reporting errors "failed assertion 'cap_get_capType(destSlot->cap) == cap_null_cap'". I found that the variable "(slot_ptr_t) (rootserver.tcb) ) -> cap.words[0] " is equals to 0xffffffffffffffff, so that the cap_get_capType(destSlot->cap) <=> (slot_ptr_t) (rootserver.tcb) ) -> cap.words[0] & 0x1full != 0 . I guess it caused the mistake, but i don't know why.
I'm about to collapse. I really need your help. How can I solve this problem?
Hello all! If you’re reading this at the time it was sent, then the developer hangout is in roughly an hour. See you there!
>
> On Jan 25, 2022, at 8:02 PM, devel-request(a)sel4.systems wrote:
>
> Send Devel mailing list submissions to
> devel(a)sel4.systems
>
> To subscribe or unsubscribe via email, send a message with subject or
> body 'help' to
> devel-request(a)sel4.systems
>
> You can reach the person managing the list at
> devel-owner(a)sel4.systems
>
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of Devel digest..."
>
> Today's Topics:
>
> 1. Re: seL4 developer hangout/video call (Gerwin Klein)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Tue, 25 Jan 2022 06:52:21 +0000
> From: Gerwin Klein <kleing(a)unsw.edu.au>
> Subject: [seL4] Re: seL4 developer hangout/video call
> To: devel <devel(a)sel4.systems>
> Message-ID: <7F36F76C-E596-4A51-9419-785AB723CC03(a)unsw.edu.au>
> Content-Type: text/plain; charset="us-ascii"
>
> Just a reminder that seL4 dev hangout is not tomorrow, but shifted by one day.
>
> Cheers,
> Gerwin
>
>> On 23 Jan 2022, at 18:13, Gerwin Klein <kleing(a)unsw.edu.au> wrote:
>>
>> An earlier-than-usual heads-up that the seL4 developer hangout this week will be shifted by one day, because of the public holiday in Australia.
>>
>> This means, we're meeting on Wed for Europe/US and on Thu for Australia:
>>
>> - Sydney: Thu, Jan 27, 8am
>> - Central Europe: Wed, Jan 26, 10pm
>> - US West Coast: Wed, Jan 26, 1pm
>>
>> Zoom link: https://unsw.zoom.us/j/82640784431
>>
>> Cheers,
>> Gerwin
>>
>
>
> ------------------------------
>
> Subject: Digest Footer
>
> _______________________________________________
> Devel mailing list -- devel(a)sel4.systems
> To unsubscribe send an email to devel-leave(a)sel4.systems
>
>
> ------------------------------
>
> End of Devel Digest, Vol 135, Issue 2
> *************************************
Hi seL4 devs,
a few of us thought it might be nice to talk more directly from time to time rather than only via pull requests, so we're trialling a seL4 developer hangout/video chat.
The idea for this is to be:
- informal, about 1h
- for technical discussions about seL4 and related repositories
- anyone can join
- every two weeks, initially for 3 times, then we can decide how we like it
At least one or two technical steering committee (TSC) members will try to be at every one of these, but these are not TSC meetings where formal decisions are made, just technical discussions about whatever people have on their minds.
To provide a starting topic, one thing we'd be interested in is:
seL4 boot code
There have been quite a few pull requests in that area, and it'd be nice to know what people's plans are and how we can keep this part of seL4 high assurance while making it more flexible. Other topics for future meetings could be better support for other language bindings (e.g. Rust), any RFCs that are open or people are thinking about opening, or just discussions about current pull requests or issues.
The first hangout is on
- Sydney: Wed, Nov 3, 8am
- Central Europe: Tue, Nov 2, 10pm
- US East Coast: Tue, Nov 2, 2pm
Zoom link: https://unsw.zoom.us/j/82640784431
Cheers,
Gerwin
Other US time zones:
PST (West Coast): 1pm
MST (Mountain Time): 2pm
CST (Central Time): 3pm
EST (East Coast): 4pm
We have a lot of time zones here, it’s a bit of a pain sometimes.
>
> On Jan 23, 2022, at 8:01 PM, devel-request(a)sel4.systems wrote:
>
> Send Devel mailing list submissions to
> devel(a)sel4.systems
>
> To subscribe or unsubscribe via email, send a message with subject or
> body 'help' to
> devel-request(a)sel4.systems
>
> You can reach the person managing the list at
> devel-owner(a)sel4.systems
>
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of Devel digest..."
>
> Today's Topics:
>
> 1. Re: seL4 developer hangout/video call (Gerwin Klein)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Sun, 23 Jan 2022 07:13:27 +0000
> From: Gerwin Klein <kleing(a)unsw.edu.au>
> Subject: [seL4] Re: seL4 developer hangout/video call
> To: devel <devel(a)sel4.systems>
> Message-ID: <678C2D4C-EEE5-4D79-82BD-256BC78B3BFC(a)unsw.edu.au>
> Content-Type: text/plain; charset="us-ascii"
>
> An earlier-than-usual heads-up that the seL4 developer hangout this week will be shifted by one day, because of the public holiday in Australia.
>
> This means, we're meeting on Wed for Europe/US and on Thu for Australia:
>
> - Sydney: Thu, Jan 27, 8am
> - Central Europe: Wed, Jan 26, 10pm
> - US West Coast: Wed, Jan 26, 1pm
>
> Zoom link: https://unsw.zoom.us/j/82640784431
>
> Cheers,
> Gerwin
>
>
> ------------------------------
>
> Subject: Digest Footer
>
> _______________________________________________
> Devel mailing list -- devel(a)sel4.systems
> To unsubscribe send an email to devel-leave(a)sel4.systems
>
>
> ------------------------------
>
> End of Devel Digest, Vol 134, Issue 1
> *************************************
Hi Sel4:
While portinging Android Guest based on Sel4 Vmm project, I met some problems .In my porting steps, I increased the reserved memory for Android Guest to 2G on my platform. Then there were some parts of Sel4 Vmm project that confused me.
1. the principle to determin the static pool size for bootstrap with allocman
n In bootstrap.h, I found your explanation for the value that it is based on the work with trial and error.Is that still the case?
n If I incease this size, the frame_vm0_group_bin showed in vm_minimal.cdl file will obviously increase together.What’s the relationship of the two value?
2. How is the staic memory pool created?
Is this memory pool created from untyped memory, so as treated untyped object?
3. the principle to determin the vm.simple_untyped24_pool size and nums
n What’s the usage of the untyped_pool memory?
n How can I make sure a reasonable size and nums of this value ?
Much apprecitated, if you can give some feedbacks.
Tao Heng | Taoer
* +8618800230581
* taoheng(a)saicmotor.com<mailto:taoheng@saicmotor.com>
Basic Software Platform
SAIC Motor Z-ONE Software Company
Auto Innovation Park | 201 Anyan Road, Jiading, Shanghai
邮件免责申明
Email Disclaimer
本邮件仅供本邮件指定收件人使用，其所载内容可能因含有保密信息或其它原因而不得披露。除本公司及本邮件指定收件人外，任何人不得公开、传播、分发、复制、印刷或使用本邮件之任何部分或其所载之任何内容。如您误收到本邮件，请立即通知本公司，并将原始邮件、附件及其所有复本从系统中删除，切勿使用。
This email is for the use of the designated receivers only，and the content is not allowed to be disclosed due to the confidential information or other reasons. Except for the Company and the designated receivers of this email, no one shall disclose, disseminate, distribute, copy, print or use any part of this email or any content contained therein. If you receive this email by mistake, please notify the Company immediately, and delete the original email, attachments and all copies from the system. Do not use it.
网络通信可能含有计算机病毒或其它缺陷，可能无法准确和/或及时送达其它系统，亦可能受阻而不为本公司或本邮件指定收件人所知。本公司对此类错误或遗漏以及任何因使用本邮件而引致之任何损失概不承担责任。
Network communication may contain computer viruses or other defects, which may not be delivered to other systems accurately and / or in time, or may be blocked by the Company or the designated receivers of this email. The Company shall not be liable for such errors or omissions and for any loss arising from this email.
本邮件所载任何内容仅作为业务层面交流与参考，除非明确说明，本公司不对邮件所载内容之准确性、完整性或公平性等承担任何法律责任。
Any contents contained in this email are only for the purpose of business communication and reference only. Unless explicitly stated otherwise, the Company shall not assume any legal responsibility for the accuracy, completeness or fairness of the content contained in the email.
本邮件指定收件人应特别注意：本邮件所载任何内容不构成本公司对本邮件指定收件人和/或其所属商业实体的任何要约、要约邀请或承诺，任何权利义务皆以双方签字盖章的书面文件为准。除经本公司以签字盖章的书面文件确认外，收件人和/或其所属商业实体不得以本邮件所载任何内容作为其向本公司主张任何权利或利益的正式依据。
The designated receivers should pay special attention to the fact that nothing contained in this email shall constitute an offer, invitation or acceptance by the Company to the designated receivers of this email and/or its affiliated business entities, and any rights and obligations are subject to the written documents signed and sealed by both parties. Except from the written document signed ,sealed and confirmed by the Company, the receivers and / or its affiliated business entity shall not rely on anything contained in this email as the formal basis for claiming any rights or interests to the Company.
Hi,
I am a 2nd-year grad student at the Systopia Lab in UBC. I am using seL4
for the OS research project at I have a few independent questions:
1. Virtual Machines can be implemented with different levels of
support from the hardware. If we talk about x86_64, in the most basic
terms, you could have VMs without or without VT-X extensions. Looking at
the resources available on the seL4 site, I think the given VMM libraries
assume VT-X. Is there an example that does not use VT-X?
2. The scheduler inside seL4 is relatively simple. I have heard(Thanks
Nick!) that if a complicated scheduling policy is desired, it can be
done in userspace. A user-level component that has the capabilities to all
the TCB's can play with the priority, resume/pause, and achieve any
arbitrary scheduling. Is there an example available which I could look at?
3. I would like to implement a new functionality of memory quota,
where different user-apps can be assigned memory quota and not just the
physical pages. Does such a functionality belong in the kernel or
the userspace component(say memory quota manager)? In the latter case, it
would be just an endPoint capability to the quota manager service, so how
does one split it - say split a quota of 100MB into two separate 50MB
quotas. This is more a generic micro-kernel query rather than seL4
specific, but any insights would help.
Thanks,
Sid
sid-agrawal.ca
Hi,
I have tried running sel4test built for AARCH64 (https://docs.sel4.systems/Hardware/imx8mm.html) on my imx8mm-evk dev board. I am on the 12.1.0 branch of sel4test-manifest.git.
Firstly I have to add "set(KernelAArch64SErrorIgnore ON)" to my build config in order to get the tests running and unfortunately things go awry during the test run
...
Starting test 47: FRAMEEXPORTS0001
Running test FRAMEEXPORTS0001 (Test that we can access all exported frames)
Pagefault from [FRAMEEXPORTS0001]: read fault at PC: 0x41c4ec vaddr: 0x11000000, FSR 0x92000210
Register of root thread in test (may not be the thread that faulted)
Register dump:
pc: 0x41c4ec
sp: 0x100118a0
spsr: 0x80000040
x0: 0x11000000
x1: 0x11000000
x2: 0x55
x3: 0x15
x4: 0xe6
x5: 0x0
x6: 0x0
x7: 0xffffffffffffffff
x8: 0x10011a48
x16: 0x0
x17: 0x0
x18: 0x0
x29: 0x100118a0
x30: 0x41c9f0
x9: 0x2b
x10: 0x2b
x11: 0xffffffff
x12: 0x0
x13: 0x0
x14: 0x0
x15: 0x0
x19: 0xe7
x20: 0x8
x21: 0x11000000
x22: 0x0
x23: 0x0
x24: 0x0
x25: 0x0
x26: 0x0
x27: 0x0
x28: 0x0
tpidr_el0: 0x616f60
tpidrro_el0: 0x0
Failure: result == SUCCESS at line 291 of file /host/projects/sel4test/apps/sel4test-driver/src/testtypes.c
Error: result == SUCCESS at line 217 of file /host/projects/sel4test/apps/sel4test-driver/src/main.c
...
Starting test 55: IPC1001
Running test IPC1001 (Test SMP inter-AS seL4_Send + seL4_Recv)
KERNEL DATA ABORT!
Faulting instruction: 0xffffff804001e2ac
FAR: 0xffffff80bf800020 ESR (DFSR): 0x96000210
halting...
Kernel entry via Syscall, number: 1, Call
Cap type: 10, Invocation tag: 20
Is this something that should just work? Or am I missing something.
Cheers,
Zippy
