Hello,
I have tried to build sel4test following 'running SEL4' instruction.
It was successful for x86 platform, but when I try to build it for 'zyncmp' I've got an error:
gcc: error: unrecognized command line option '-marm'; did you mean '-mabm'?
gcc: error: unrecognized command line option '-mfloat-abi=soft'
Thank you,
Leonid
-- Build files have been written to: /home/lm/sel4test/build-zynqmp
lm@u-18:~/sel4test/build-zynqmp$ ninja
[2/235] Generating linker.lds_pp
FAILED: elfloader-tool/…
[View More]linker.lds_pp
cd /home/lm/sel4test/build-zynqmp/elfloader-tool && /usr/bin/gcc -march=armv8-a -marm -D__KERNEL_32__ -I/home/lm/sel4test/build-zynqmp/autoconf -I/home/lm/sel4test/build-zynqmp/kernel/gen_config -I/home/lm/sel4test/build-zynqmp/elfloader-tool/gen_config -I/home/lm/sel4test/build-zynqmp/libsel4/gen_config -I/home/lm/sel4test/build-zynqmp/projects/seL4_libs/libsel4vka/gen_config -I/home/lm/sel4test/build-zynqmp/projects/seL4_libs/libsel4utils/gen_config -I/home/lm/sel4test/build-zynqmp/projects/seL4_libs/libsel4platsupport/gen_config -I/home/lm/sel4test/build-zynqmp/projects/seL4_libs/libsel4serialserver/gen_config -I/home/lm/sel4test/build-zynqmp/projects/seL4_libs/libsel4debug/gen_config -I/home/lm/sel4test/build-zynqmp/projects/seL4_libs/libsel4test/gen_config -I/home/lm/sel4test/build-zynqmp/projects/seL4_libs/libsel4muslcsys/gen_config -I/home/lm/sel4test/build-zynqmp/projects/seL4_libs/libsel4vmm/gen_config -I/home/lm/sel4test/build-zynqmp/projects/sel4test/apps/sel4test-driver/gen_config -I/home/lm/sel4test/build-zynqmp/projects/util_libs/libutils/gen_config -I/home/lm/sel4test/build-zynqmp/projects/util_libs/libplatsupport/gen_config -I/home/lm/sel4test/build-zynqmp/projects/util_libs/libethdrivers/gen_config -P -E -o linker.lds_pp -x c /home/lm/sel4test/tools/seL4/elfloader-tool/src/arch-arm/linker.lds
gcc: error: unrecognized command line option '-marm'; did you mean '-mabm'?
[3/235] Building C object kernel/CMakeFiles/kernel_bf_gen_target_1_pbf_temp_lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj
FAILED: kernel/CMakeFiles/kernel_bf_gen_target_1_pbf_temp_lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj
ccache /usr/bin/gcc --sysroot=/home/lm/sel4test/build-zynqmp -I../kernel/include -I../kernel/include/32 -I../kernel/include/arch/arm -I../kernel/include/arch/arm/arch/32 -I../kernel/include/plat/zynqmp -I../kernel/include/plat/zynqmp/plat/32 -I../kernel/include/arch/arm/armv/armv8-a -I../kernel/include/arch/arm/armv/armv8-a/32 -Ikernel/gen_config -Ikernel/autoconf -Ikernel/gen_headers -march=armv8-a -marm -D__KERNEL_32__ -O2 -g -DNDEBUG -nostdinc -nostdlib -O2 -DHAVE_AUTOCONF -DDEBUG -g -ggdb -mfloat-abi=soft -fno-pic -fno-pie -fno-stack-protector -fno-asynchronous-unwind-tables -std=c99 -Wall -Werror -Wstrict-prototypes -Wmissing-prototypes -Wnested-externs -Wmissing-declarations -Wundef -Wpointer-arith -Wno-nonnull -ffreestanding -E -P -MD -MT kernel/CMakeFiles/kernel_bf_gen_target_1_pbf_temp_lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj -MF kernel/CMakeFiles/kernel_bf_gen_target_1_pbf_temp_lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj.d -o kernel/CMakeFiles/kernel_bf_gen_target_1_pbf_temp_lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj -c kernel/kernel_bf_gen_target_1_pbf_temp.c
gcc: error: unrecognized command line option '-marm'; did you mean '-mabm'?
gcc: error: unrecognized command line option '-mfloat-abi=soft'
[4/235] Creating C input file for preprocessor
ninja: build stopped: subcommand failed.
________________________________
This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.
[View Less]
Hi Chris,
For your ia32 issue, it appears that you are missing the package libx32gcc-5-dev which provides 32-bit versions of libgcc and libgcc_eh. It is normally installed automatically by gcc-5-multilib.
With regards to cpio --reproducible, what version of cpio are you using? The release notes indicate that it was added in version 2.12
(https://www.gnu.org/software/cpio/) but I had it in my Debian package from version 2.11 so I assumed that it was more universally available now.
Kent
…
[View More]
From: Mcleod, Kent (Data61, Kensington NSW)
Sent: Thursday, August 23, 2018 11:28 AM
To: Chris Rothrock; Lyons, Anna (Data61, Kensington NSW)
Cc: devel(a)sel4.systems
Subject: Re: [seL4] Demo build
Hi Chris,
For your ia32 issue, it appears that you are missing the package libx32gcc-5-dev which provides 32-bit versions of libgcc and libgcc_eh. It is normally installed automatically by gcc-5-multilib.
With regards to cpio --reproducible, what version of cpio are you using? The release notes indicate that it was added in version 2.12
(https://www.gnu.org/software/cpio/) but I had it in my Debian package from version 2.11 so I assumed that it was more universally available now.
Kent
From: Devel <devel-bounces(a)sel4.systems> on behalf of Chris Rothrock <cgrothrock(a)gmail.com>
Sent: Thursday, August 23, 2018 10:22 AM
To: Lyons, Anna (Data61, Kensington NSW)
Cc: devel(a)sel4.systems
Subject: Re: [seL4] Demo build
I am using a newly initialized build directory for ia32. I can get a good, successful build for v 9.0.0 but not 10.0.0.
As for x86_64, I was able to get a good build of x86_64 on 10.0.0 before but now I can't. It seems that there is a switch for cpio that is being set in the build that is invalid for that command. Possibly the latest version of cpio no longer support --reproducable switch since this is where it errors.
On Wed, Aug 22, 2018 at 7:33 PM <Anna.Lyons(a)data61.csiro.au> wrote:
Hi Chris,
For the first issue - just making sure you initialised a new build directory for building ia32?
The second issue - our HPET driver is very bare and doesn't support the full gamut of features. If you want to continue with this platform you'll need to improve the driver.
Thanks,
Anna.
From: Chris Rothrock <cgrothrock(a)gmail.com>
Sent: Thursday, 23 August 2018 3:56 AM
To: Lyons, Anna (Data61, Kensington NSW)
Cc: devel(a)sel4.systems
Subject: Re: [seL4] Demo build
So my initial problem is actually resolved - it turns out I had the package 'ninja' installed, not 'ninja-build' which threw everything into a fit when I tried to actually use ninja. That being resolved, I was able to get a clean build of the 64 bit kernel (for x86) and made a simulated run. All looked well during the simulation. I do have 2 problems following up from this, however. When trying to use this build for a hardware boot (not simulated boot) I get an error (listed below). Also, for lengthy reasons, I also need to build a 32 bit version but when I do, this build fails.
This is the build output from the ia32 build:
Desktop:~/sel4test/build-ia32$ ninja
[5/32] Linking CXX executable projects/sel4test/apps/sel4test-tests/sel4test-tests
FAILED: : && ccache /usr/bin/g++ --sysroot=/home/jennifer/sel4test/build-ia32 -m32 -march=nehalem -D__KERNEL_32__ -nostdinc++ -g -march=nehalem -D__KERNEL_32__ -Wl,-m -Wl,elf_i386 -static -nostdlib -z max-page-size=0x1000 -u __vsyscall_ptr /home/jennifer/sel4test/build-ia32/lib/crt1.o /home/jennifer/sel4test/build-ia32/lib/crti.o /usr/lib/gcc/x86_64-linux-gnu/5/crtbegin.o projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/arch/x86/arch.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/arch/x86/tests/alignment.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/arch/x86/tests/alignment_asm.S.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/arch/x86/tests/breakpoints.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/helpers.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/main.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/benchmark_api.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/binding.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/breakpoints.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/cache.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/cnodeops.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/cspace.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/domains.cxx.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/endpoints.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/ept.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/faults.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/fpu.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/frames.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/inc_untyped.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/interrupt.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/ioports.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/iopt.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/ipc.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/multicore.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/nbwait.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/pagetables.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/preempt.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/regressions.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/schedcontext.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/scheduler.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/serial_server.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/sync.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/threads.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/trivial.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/vspace.c.obj -lgcc -lgcc_eh libsel4/libsel4.a projects/seL4_libs/libsel4allocman/libsel4allocman.a projects/seL4_libs/libsel4vka/libsel4vka.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/seL4_libs/libsel4test/libsel4test.a projects/seL4_libs/libsel4sync/libsel4sync.a projects/seL4_libs/libsel4muslcsys/libsel4muslcsys.a projects/sel4test/libsel4testsupport/libsel4testsupport.a projects/seL4_libs/libsel4serialserver/libsel4serialserver.a projects/seL4_libs/libsel4test/libsel4test.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/util_libs/libelf/libelf.a projects/util_libs/libcpio/libcpio.a projects/seL4_libs/libsel4sync/libsel4sync.a projects/seL4_libs/libsel4platsupport/libsel4platsupport.a projects/util_libs/libplatsupport/libplatsupport.a projects/seL4_libs/libsel4simple-default/libsel4simple-default.a projects/seL4_libs/libsel4vspace/libsel4vspace.a projects/seL4_libs/libsel4simple/libsel4simple.a projects/seL4_libs/libsel4vka/libsel4vka.a projects/seL4_libs/libsel4debug/libsel4debug.a libsel4/libsel4.a projects/util_libs/libutils/libutils.a projects/musllibc/build-temp/lib/libc.a -lgcc -lgcc_eh libsel4/libsel4.a projects/seL4_libs/libsel4allocman/libsel4allocman.a projects/seL4_libs/libsel4vka/libsel4vka.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/seL4_libs/libsel4test/libsel4test.a projects/seL4_libs/libsel4sync/libsel4sync.a projects/seL4_libs/libsel4muslcsys/libsel4muslcsys.a projects/sel4test/libsel4testsupport/libsel4testsupport.a projects/seL4_libs/libsel4serialserver/libsel4serialserver.a projects/seL4_libs/libsel4test/libsel4test.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/util_libs/libelf/libelf.a projects/util_libs/libcpio/libcpio.a projects/seL4_libs/libsel4sync/libsel4sync.a projects/seL4_libs/libsel4platsupport/libsel4platsupport.a projects/util_libs/libplatsupport/libplatsupport.a projects/seL4_libs/libsel4simple-default/libsel4simple-default.a projects/seL4_libs/libsel4vspace/libsel4vspace.a projects/seL4_libs/libsel4simple/libsel4simple.a projects/seL4_libs/libsel4vka/libsel4vka.a projects/seL4_libs/libsel4debug/libsel4debug.a libsel4/libsel4.a projects/util_libs/libutils/libutils.a projects/musllibc/build-temp/lib/libc.a /usr/lib/gcc/x86_64-linux-gnu/5/crtend.o /home/jennifer/sel4test/build-ia32/lib/crtn.o -o projects/sel4test/apps/sel4test-tests/sel4test-tests && :
/usr/bin/ld: skipping incompatible /usr/lib/gcc/x86_64-linux-gnu/5/libgcc.a when searching for -lgcc
/usr/bin/ld: cannot find -lgcc
/usr/bin/ld: skipping incompatible /usr/lib/gcc/x86_64-linux-gnu/5/libgcc_eh.a when searching for -lgcc_eh
/usr/bin/ld: cannot find -lgcc_eh
/usr/bin/ld: skipping incompatible /usr/lib/gcc/x86_64-linux-gnu/5/libgcc.a when searching for -lgcc
/usr/bin/ld: cannot find -lgcc
/usr/bin/ld: skipping incompatible /usr/lib/gcc/x86_64-linux-gnu/5/libgcc_eh.a when searching for -lgcc_eh
/usr/bin/ld: cannot find -lgcc_eh
collect2: error: ld returned 1 exit status
[5/32] Generating from generated/plat_mode/machine/hardware.bf.pbf
ninja: build stopped: subcommand failed.
Here is the serial output of the x86_64 build boot:
Boot config: parsing cmdline ''
Boot config: console_port = 0x3f8
Boot config: debug_port = 0x3f8
Boot config: disable_iommu = false
Detected 1 boot module(s):
module #0: start=0xa11000 end=0xd054f0 size=0x2f44f0 name=''
Parsing GRUB physical memory map
Physical Memory Region from 0 size 9e800 type 1
Physical Memory Region from 9e800 size 1800 type 2
Physical Memory Region from e0000 size 20000 type 2
Physical Memory Region from 100000 size ac722000 type 1
Adding physical memory region 0x100000-0xac822000
Physical Memory Region from ac822000 size a23000 type 2
Physical Memory Region from ad245000 size 69000 type 3
Physical Memory Region from ad2ae000 size 4b5000 type 4
Physical Memory Region from ad763000 size 430000 type 2
Physical Memory Region from adb93000 size 1000 type 1
Adding physical memory region 0xadb93000-0xadb94000
Physical Memory Region from adb94000 size 206000 type 4
Physical Memory Region from add9a000 size 156000 type 1
Adding physical memory region 0xadd9a000-0xadef0000
Physical Memory Region from adef0000 size 935000 type 2
Physical Memory Region from ae825000 size 4b000 type 1
Adding physical memory region 0xae825000-0xae870000
Physical Memory Region from ae870000 size 781000 type 2
Physical Memory Region from aeff1000 size f000 type 1
Adding physical memory region 0xaeff1000-0xaf000000
Physical Memory Region from e0000000 size 10000000 type 2
Physical Memory Region from feb80000 size 82000 type 2
Physical Memory Region from fec10000 size 1000 type 2
Physical Memory Region from fed00000 size 1000 type 2
Physical Memory Region from fed40000 size 5000 type 2
Physical Memory Region from fed80000 size 10000 type 2
Physical Memory Region from ff000000 size 1000000 type 2
Physical Memory Region from 100000000 size 40000000 type 1
Adding physical memory region 0x100000000-0x140000000
Got VBE info in multiboot. Current video mode is 3
ACPI: RSDP paddr=0xf0490
ACPI: RSDP vaddr=0xf0490
ACPI: RSDT paddr=0xad269028
ACPI: RSDT vaddr=0xad269028
Warning: Your kernel was not compiled for the current microarchitecture.
SKIM window for mitigating Meltdown (https://www.meltdownattack.com) not necessary for AMD and performance is being needlessly affected, consider disabling
Kernel loaded to: start=0x100000 end=0xa11000 size=0x911000 entry=0x10123e
ACPI: RSDT paddr=0xad269028
ACPI: RSDT vaddr=0xad269028
ACPI: FADT paddr=0xad269148
ACPI: FADT vaddr=0xad269148
ACPI: FADT flags=0x385a5
ACPI: MADT paddr=0xad2764a8
ACPI: MADT vaddr=0xad2764a8
ACPI: MADT apic_addr=0xfee00000
ACPI: MADT flags=0x1
ACPI: MADT_APIC apic_id=0x10
ACPI: MADT_APIC apic_id=0x11
ACPI: Not recording this APIC, only support 1
ACPI: MADT_APIC apic_id=0x12
ACPI: Not recording this APIC, only support 1
ACPI: MADT_APIC apic_id=0x13
ACPI: Not recording this APIC, only support 1
ACPI: MADT_IOAPIC ioapic_id=0 ioapic_addr=0xfec00000 gsib=0
ACPI: MADT_IOAPIC ioapic_id=1 ioapic_addr=0xfec01000 gsib=24
ACPI: Not recording this IOAPIC, only support 1
ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x0
ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xf
ACPI: 1 CPU(s) detected
ELF-loading userland images from boot modules:
size=0x35b000 v_entry=0x436000 v_start=0x400000 v_end=0x75b000 p_start=0xd06000 p_end=0x1061000
Moving loaded userland images to final location: from=0xd06000 to=0xa11000 size=0x35b000
Starting node #0 with APIC ID 16
Mapping kernel window is done
Booting all finished, dropped to user space
Received reserved IRQ: 7Skipping table FPDTD, unknown
Skipping table FIDT▒, unknown
Skipping table TCPA2, unknown
Skipping table MSDMU, unknown
Skipping table UEFIB, unknown
Skipping table IVRSx, unknown
Skipping table BGRT8, unknown
Skipping table CRAT(, unknown
Skipping table LUFT▒), unknown
Warning: skipping table ACPI XSDT
hpet_init@hpet.c:223 This driver expects hpet timer0 to be 64bit
init_timer@main.c:192 [Cond failed: error]
Failed to initialise default timer
seL4 root server abort()ed
Debug halt syscall from user thread 0xffffff80aeff5400 "sel4test-driver"
halting...
Kernel entry via Unknown syscall, word: 52
On Wed, Aug 15, 2018 at 8:30 PM <Anna.Lyons(a)data61.csiro.au> wrote:
Hi Chris,
That's strange, the build system definitely should not hang.
However I need more information to help at all. Which OS version are you using (host and seL4)? Which gcc version and cmake version? Is there any output from the init-build script at all? Also, have you used a clean build directory after the initial failure?
Cheers,
Anna.
From: Devel <devel-bounces(a)sel4.systems> on behalf of Chris Rothrock <cgrothrock(a)gmail.com>
Sent: Thursday, 16 August 2018 3:16 AM
To: devel(a)sel4.systems
Subject: [seL4] Demo build
Most of my experience with the seL5 microkernel has been through the Genode framework, but now I am attempting to build the demo test of seL4 without Genode using the instructions on the "Getting Started" page of seL4.systems but this seems to not be working for me. I have the latest version of repo, ninja and CMake (originally, I was given an error that I needed 3.9.x so I upgraded CMake manually). When I get to the instruction of "../init-build.sh -DPLATFORM=x86_64 -DSIMULATION=TRUE" demo build, the script only hangs. Nothing gets built and no demo is run. Is there something missing that I should be doing?
Thanks,
Chris
--
Thank You,
Chris Rothrock
Senior System Administrator
(315) 308-1637
--
Thank You,
Chris Rothrock
Senior System Administrator
(315) 308-1637
--
Thank You,
Chris Rothrock
Senior System Administrator
(315) 308-1637
[View Less]
Most of my experience with the seL5 microkernel has been through the Genode
framework, but now I am attempting to build the demo test of seL4 without
Genode using the instructions on the "Getting Started" page of seL4.systems
but this seems to not be working for me. I have the latest version of
repo, ninja and CMake (originally, I was given an error that I needed 3.9.x
so I upgraded CMake manually). When I get to the instruction of
"../init-build.sh
-DPLATFORM=x86_64 -DSIMULATION=TRUE" demo …
[View More]build, the script only hangs.
Nothing gets built and no demo is run. Is there something missing that I
should be doing?
Thanks,
Chris
--
Thank You,
Chris Rothrock
Senior System Administrator
(315) 308-1637
[View Less]
I have been reading the following paper for some time:
Klein, Gerwin, June Andronick, Kevin Elphinstone, Toby Murray, Thomas
Sewell, Rafal Kolanski, and Gernot Heiser. “Comprehensive Formal
Verification of an OS Microkernel.” *Trustworthy Sytems*, 2014.
https://ts.data61.csiro.au/publications/nictaabstracts/Klein_AEMSKH_14.abst…
This is fantastic work and provides powerful guarantees about kernel
behavior. However, I am confused about the guarantees about the behavior of
user programs.
The …
[View More]paper seems to suggest that in the abstract model of sel4, the user
transitions are nondeterministic.
page 21 bottom: "User transitions are specified as nondeterministically
changing arbitrary user-accessible parts of the state space"
Does this mean that the refinement theorem of sel4 (Theorem 3 in the above
paper: the C implementation refines the abstract model) provides no
guarantee about what the user program does, except that the user program
does not mess up with the kernel state?
Is it fair to say that the refinement theorem does not preclude the sel4
implementation from incorrectly changing the behavior of the user programs,
e.g. by messing up the user state?
I was expecting the abstract model in Isabelle to concretely specify how
the user programs behave, perhaps according to x86/arm/riscv semantics
extended with syscalls.
Sorry if I misunderstood the paper.
Thanks in advance for any clarification,
Abhishek
--
-- Abhishek
http://www.cs.cornell.edu/~aa755/
[View Less]
Hi folks,
I'm currently porting over a project from the Kbuild/Kconfig build system
to the new CMake based build system and am having some issues.
I'm trying trying to spawn additional processes (2+) and I am encountering
an error when I attempt to call 'process_config_default_simple'. The
message reads:
Caught cap fault in send phase at address 0x0
while trying to handle:
vm fault on data at address 0x0 with status 0x4
in thread 0xffffff801ffb5400 "PRIMARY" at address 0x4252ba
I loaded the …
[View More]executables which I am trying to spawn into the new processes
into the cpio using a variation of the call
MakeCPIO(archive.o $<TARGET_FILE:SECONDARY>;$<TARGET_FILE:TERTIARY>;...)
where SECONDARY and TERTIARY are the executables which I am using later to
spawn the new processes.
The source code in question worked previously when using Kbuild, so I'm
wondering if I'm doing something wrong with the CMake.
Does anyone have any ideas? I've gone through the tutorials, but I'm still
fairly new to seL4, so any help would be very much appreciated.
[View Less]
Hi guys,
When I try to run some application tests(written by myself) on sel4test
(x86-qemu environment), I found the following errors.
*Starting test suite sel4test*
*Starting test 0: Test that there are tests*
*Starting test 1: APPTEST1*
*vka_alloc_object_at_maybe_dev@object.h:59 Failed to allocate object of
size 4096, error 1*
*new_pages_at_vaddr@vspace.c:330 Failed to allocate page number: 0 out of 1*
*load_segment@elf.c:103 ERROR: failed to allocate frame by loadee vka: 10*
*…
[View More]sel4utils_elf_load_record_regions@elf.c:519 Failed to load segments*
*sel4utils_configure_process_custom@process.c:596 Failed to load elf file*
It seems seL4test's driver can not load tests with very large size?
I also tried to change the "DRIVER_UNTYPED_MEMORY" size from "(1 << 25)" to
"(1 << 27)", but it also failed.
Any advices about the issue?
Dong
[View Less]
Hello,
Is there any way to define untyped size while creating process using library functions?
process_config_default_simple(simple_t *simple, const char *image_name, uint8_t prio)
sel4utils_configure_process_custom(sel4utils_process_t *process, vka_t *vka, vspace_t *spawner_vspace, sel4utils_process_config_t config)
The second question is how to initialize allocator (probably I should use bootstrap_use_current_1level, but how where should I get parameters?) in created process to support …
[View More]memory allocation operations?
Thank you,
Leonid
________________________________
This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.
[View Less]
Hi Experts,
We are trying to port sel4 to Shakti FPGA. It is similar to Rocket FPGA.
The memory footprint is 256 mb [0x80000000 - 0x8fffffff]. Shakti support
-march=imafd. A single core 64 bit design.
The run in FPGA stops at *"memcpy((char *)dest_vaddr + phys_virt_offset,
(char *)elf + data_offset, data_size);*" called in the function "
*unpack_elf_to_paddr()".* Earlier it stopped just at the memset (one line
above). I manually commented out memset part and made it to run till
memcpy. So I …
[View More]doubt it has something to do with wrong memory access. can
someone please explain me the above said function (blue color) ? what could
be reasons for memcpy to hung ?
Can someone please guide me to the area in code where memory related
interrupts are coded ?
We have the latest upstream of SEL4 (Aug 10). It has the dornerworks
upstream changes. We are trying to load at 0x88000000. The image works well
in spike simulation.
*Commands to build:*
../init-build.sh -DPLATFORM=spike -DKernelPlatformSpikeRocketChip=ON
-DSIMULATION=FALSE -DRISCV64=TRUE
ninja
*Snapshot of the run in FPGA:*
DTB
{
#address-cells = <0x00000002>;
#size-cells = <0x00000002>;
compatible = "shakti,spike-bare-dev";
model = "shakti,spike-bare";
cpus {
#address-cells = <0x00000001>;
#size-cells = <0x00000000>;
timebase-frequency = <0x00989680>;
cpu@0 {
device_type = "cpu";
reg = <0x00000000>;
status = "okay";
compatible = "riscv";
riscv,isa = "rv64imafd";
mmu-type = "riscv,sv39";
clock-frequency = <0x3b9aca00>;
interrupt-controller {
#interrupt-cells = <0x00000001>;
interrupt-controller;
compatible = "riscv,cpu-intc";
linux,phandle = <0x00000001>;
phandle = <0x00000001>;
}
}
}
memory@80000000 {
device_type = "memory";
reg = <0x00000000 0x80000000 0x00000000 0x10000000>;
}
soc {
#address-cells = <0x00000002>;
#size-cells = <0x00000002>;
compatible = "shakti,spike-bare-soc", "simple-bus";
ranges;
}
uart {
compatible = "shakti,uart0";
reg = <0x00000000 0x00011200 0x00000000 0x00001000>;
}
htif {
compatible = "ucb,htif0";
}
}
ELF-loader started on
paddr=[80200000..8060e7d7]
elf check file returned 1
elf check file returned 1
ELF-loading image 'kernel'
paddr=[88000000..8802bfff]
vaddr=[ffffffff80000000..ffffffff8002bfff]
virt_entry=ffffffff80000000
configured page table levels = 3......
elf check file returned 1
image size 2b350
*(char *)dest_vaddr + phys_virt_offset = ffffffff88000000 *
*phys_virt_offset = 8000000 *
*(char *)elf + data_offset, = ffffffff8020f854*
*started memcpy*
------------------------------------------------------------> *Hangs*
--
regards,
Sathya
[View Less]
Hi, I have question about sel4 benchmark cache unable.
I want to benchmark sel4 without cache but I don't know where is the
location that configures cache.
Would you give advice?
