Dear sel4 community,
yesterday I've started to develop a low-level platform test to stress several
multi-processor aspects on top of the Genode API. Thereby, I've
recognized that on sel4/x86_64 the TLB is practically not always
cleaned properly in SMP systems.
The test spawns threads of one protection domain on each available cpu.
Each thread accesses one of the first words of a shared dataspace.
Afterwards the main thread on CPU 0 detaches and destroys the
dataspace. Unfortunately, the threads on other CPUs still successfully
access the corresponding memory instead of triggering a fault.
To be able to reproduce the problem, you might investigate the simple
test case here:
https://github.com/skalk/genode/commit/2d2d7f982555f551227ad5dcbf9df46705d7…
My colleague Alexander Boettcher already investigated the problem in
part, and might share his insights with you.
Best regards
Stefan
--
Stefan Kalkowski
Genode labs
https://github.com.skalk | https://genode.org
Hi,
I have a Camkes app (app1) which depends on another Camkes app (app2),
which means my app1 must start only after app2 is completely initialized.
For this currently I use a signal RPC wait in app1 and the corresponding
RPC emit from app2 after app2 is completely initialized.
Is there any other way in CamkES which will ensure that app1 starts only
after app2 is completely initialized without using RPC signalling (emit and
wait) ?
How can this dependency be built ?
Regards
yk
Hello
I set up VMware according to this guide https://docs.sel4.systems/Hardware/VMware/ (using serial output to file) and compiled the picoserver CAmkES application (for x86_64) to run inside the VMware machine.
However, I do encounter a seL4_FailedLookup error. I understand the error message but cannot figure out why it occurs nor how to fix it (probably my pci configuration is wrong). Attached you find the serial_output file.
For the ethernet configuration I used linux in the same VM to figure out the details:
1) ip addr:
2: ens32: <BROADCAST,MULTICAST,UP,LOWER_UP> mtu 1500 qdisc fq_codel state UNKNOWN group default qlen 1000
link/ether 00:0c:29:90:a7:4a brd ff:ff:ff:ff:ff:ff
2) lspci -vvv:
02:00.0 Ethernet controller: Advanced Micro Devices, Inc. [AMD] 79c970 [PCnet32 LANCE] (rev 10)
Subsystem: Advanced Micro Devices, Inc. [AMD] PCnet - Fast 79C971
Physical Slot: 32
Control: I/O+ Mem+ BusMaster+ SpecCycle- MemWINV- VGASnoop- ParErr- Stepping- SERR- FastB2B- DisINTx-
Status: Cap- 66MHz- UDF- FastB2B+ ParErr- DEVSEL=medium >TAbort- <TAbort- <MAbort- >SERR- <PERR- INTx-
Latency: 64 (1500ns min, 63750ns max)
Interrupt: pin A routed to IRQ 18
Region 0: I/O ports at 2000 [size=128]
[virtual] Expansion ROM at fd500000 [disabled] [size=64K]
Kernel driver in use: pcnet32
Kernel modules: pcnet32
3) dmesg | grep "02:00.0":
...
[ 0.378516] pci 0000:02:00.0: BAR 6: assigned [mem 0xfd500000-0xfd50ffff pref]
...
4) lspci -nn:
02:00.0 Ethernet controller [0200]: Advanced Micro Devices, Inc. [AMD] 79c970 [PCnet32 LANCE] [1022:2000] (rev 10)
And here the configuration part inside picoserver.camkes (anything else NOT pasted here is unmodified):
picoserver.ethdriver_mac = [0x00, 0x0c, 0x29, 0x90, 0xa7, 0x4a];
....
hwethdriver.mmio_paddr = 0xfd500000
hwethdriver.mmio_size = 0x10000
hwethdriver.irq_irq_type = "pci";
hwethdriver.irq_irq_ioapic = 0;
hwethdriver.irq_irq_ioapic_pin = 18;
hwethdriver.irq_irq_vector = 18;
ethdriver.iospaces = "0x0:0x02:0x00:0";
ethdriver.iospace_id = 0x0200;
ethdriver.pci_bdf = "0x02:0x00.0";
I am sorry to bother you with this; I am fairly new to low level stuff.
Any help would be very much appreciated.
Best regards,
Benjamin
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
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.
________________________________
Hello,
I am able to generate, build, and execute the majority of tutorials using init, ninja, qemu, etc. within sel4-tutorials-manifest. However, I am having issues generating the tutorials specifically for the CamkES tutorials.
I have installed all of the system requirements and I am running on Ubuntu 18. The output I get is the following:
# ./init --tut hello-camkes-0
loading initial cache file ../settings.cmake
-- The C compiler identification is GNU 7.4.0
-- Check for working C compiler: /usr/bin/gcc
-- Check for working C compiler: /usr/bin/gcc -- works
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Detecting C compile features
-- Detecting C compile features - done
-- The CXX compiler identification is GNU 7.4.0
-- Check for working CXX compiler: /usr/bin/g++
-- Check for working CXX compiler: /usr/bin/g++ -- works
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- The ASM compiler identification is GNU
-- Found assembler: /usr/bin/gcc
-- CPIO test cpio_reproducible_flag FAILED
-- Performing Test compiler_arch_test
-- Performing Test compiler_arch_test - Success
-- /root/sel4-tutorials-manifest/hello-camkes-0_build/hello-camkes-0/ast.pickle is out of date. Regenerating...
-- /root/sel4-tutorials-manifest/hello-camkes-0_build/hello-camkes-0/camkes-gen.cmake is out of date. Regenerating...
CAmkES uses UTF-8 encoding, but your locale's preferred encoding is ansi_x3.4-1968. You can override your locale with the LANG environment variable.
CMake Error at tools/seL4/cmake-tool/helpers/make.cmake:19 (file):
file failed to open for reading (No such file or directory):
/root/sel4-tutorials-manifest/hello-camkes-0_build/hello-camkes-0/camkes_gen/deps_1
Call Stack (most recent call first):
tools/seL4/cmake-tool/helpers/make.cmake:77 (MakefileDepsToList)
tools/camkes/camkes.cmake:460 (execute_process_with_stale_check)
hello-camkes-0/CMakeLists.txt:13 (GenerateCAmkESRootserver)
CMake Error at tools/camkes/camkes.cmake:480 (message):
Failed to generate
/root/sel4-tutorials-manifest/hello-camkes-0_build/hello-camkes-0/camkes-gen.cmake
Call Stack (most recent call first):
hello-camkes-0/CMakeLists.txt:13 (GenerateCAmkESRootserver)
-- Configuring incomplete, errors occurred!
See also "/root/sel4-tutorials-manifest/hello-camkes-0_build/CMakeFiles/CMakeOutput.log".
Traceback (most recent call last):
File "./init", line 96, in <module>
File "./init", line 85, in main
File "/root/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 107, in init_directories
return _init_build_directory(config, initialised, build_directory, tute_directory, output, config_dict=config_dict)
File "/root/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 75, in _init_build_directory
return sh.cmake(args + ['..'], _cwd=directory, _out=output, _err=output)
File "/usr/local/lib/python3.6/dist-packages/sh.py", line 1427, in __call__
return RunningCommand(cmd, call_args, stdin, stdout, stderr)
File "/usr/local/lib/python3.6/dist-packages/sh.py", line 774, in __init__
self.wait()
File "/usr/local/lib/python3.6/dist-packages/sh.py", line 792, in wait
self.handle_command_exit_code(exit_code)
File "/usr/local/lib/python3.6/dist-packages/sh.py", line 815, in handle_command_exit_code
raise exc
sh.ErrorReturnCode_1:
RAN: /usr/local/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-0 -C ../settings.cmake ..
STDOUT:
STDERR:
I am not sure if ast.pickle and camkes-gen.cmake being out of date has anything to do with deps_1 file not being present. It's not possible to copy the deps_0 file to deps_1 since calling the './init --tut hello-camkes-0' command again creates a new project directory. Is there something obvious that I am missing?
Thanks,
Austin
Hello,
I have been trying to study how seL4's C code is formally verified. So I
looked into Autocorres tool and had a bit of hard time understanding how to
use the tool to generate Isabelle definitions from C code. I tried to
follow Autocorres' quickstart but I was confused since I do not know much
about Isabelle/HOL.
I simply ran ``make AutoCorresTest" in l4v/tools/autocorres folder and it
gave me this output:
```
Session Pure/Pure
Session FOL/FOL
Session HOL/HOL (main)
Session HOL/HOL-Eisbach
Session HOL/HOL-Library (main timing)
Session HOL/HOL-Computational_Algebra (main timing)
Session HOL/HOL-Algebra (main timing)
Session HOL/HOL-Number_Theory (main timing)
Session HOL/HOL-Statespace
Session HOL/HOL-Word (main timing)
Session Lib/Word_Lib (lib)
Session Lib/Lib (lib)
Session C-Parser/Simpl-VCG
Session C-Parser/CParser
Session Lib/CLib (lib)
Session Unsorted/AutoCorres
Session Unsorted/AutoCorresTest
Building AutoCorresTest ...
AutoCorresTest: theory AutoCorresTest.CustomWordAbs
AutoCorresTest: theory AutoCorresTest.Test_Spec_Translation
...
Finished AutoCorresTest (0:02:33 elapsed time, 0:08:14 cpu time, factor
3.23)
```
But I couldnt find any Isabelle definitions as output except "thy" files
that contain:
```
theory somefile
imports "AutoCorres.AutoCorres"
begin
external_file "somefile.c"
install_C_file "somefile.c"
autocorres "somefile.c"
end
```
I suppose I need to invoke this file somehow using Isabelle in order to
generate the definition but I'm not sure how to do that. Any help would be
very appreciated.
Best Regards,
Norrathep
--
Norrathep (Oak) Rattanavipanon
M.S. in Computer Science
University of California - Irvine
Hi,
I'm interested in running sel4 on a Xilinx Zynq UltraScale+ MPSoC evaluation board. I read the great blog post about the port from DornerWorks [1] and checked the sel4 hardware support page here [2].
Since the Zynq ZCU102 Evaluation Kit listed is quite expensive, I wanted to ask if anyone tried the procedure described in the blog post on the much cheaper Xilinx US+ ZCU104 Evaluation Kit. Might this work as well?
Thanks!
Kind regards,
- derek
[1] - https://dornerworks.com/blog/hardware-security-growing-concern-sel4-ecosyst…
[2] - https://docs.sel4.systems/Hardware/
Hello ,
I would like to know if the CamkES has support for wait on multiple signal
events ?
I need to wait for 3 different events (say write, read and timer),
I need to wait until one of these events occur. As soon as I get an event,
I need to call a common function. I cannot use emitter/consumer signal
events concept of CamKES here as it allows only one to one connection and
not many to one connection.
So in other words a single consumer_wait() for 3 different emitter events
is not possible in CamkES.
Any suggestions how can this be achieved using CamkES?
Regards
yk
