from:"Leonid Meyerovich"

[seL4] Re: seL4 multicore boot failed on arm64

2024-05-09 Thread Leonid Meyerovich

Hi Indian,

-BOOT_BSS static volatile int node_boot_lock;
+static volatile int node_boot_lock;

In seL4 kernel code try_init_kernel_secondary_core every core waits on
node_boot_lock to start initialization. As you can see above node_boot_lock
has been defined as BOOT_BSS is a specific usage context of the .bss
section during the boot process. Apparently, the Morello processor
introduces some unique features and behaviors that might affect how memory
regions like the BOOT_BSS section handles cache coherence in a
multi-threaded environment. My research shows that sometimes threads don't
see node_boot_lock changes and don't start initialization. I have removed
BOOT_BSS and it is booted properly now

Thanks,
Leonid

On Fri, May 3, 2024 at 8:13 AM Indan Zupancic  wrote:

> Hello Leonid,
>
> On 2024-04-25 21:37, Leonid Meyerovich wrote:
> > I run my seL4 application on 4 core ARMv8.
>
> Still the new platform port I assume?
>
> > Recently I have developed some more application code (I mention it
> > because
> > file system size is increased an I believe it may change boot time) and
> > from time to time I observed that boot process failed (stuck after the
> > following print)
>
> Does this only happen with a bigger application? And is it always stuck
> for a specific binary, or does the same binary sometimes work?
>
> The application isn't started until after the kernel is done booting,
> so its size should not affect cores coming up or not. If it does, it
> may be a bug in Elfloader. If that is the case, it should either
> always succeed or always fail.
>
> > Some time I see that only 2 CPU have been booted (like CPU1 and CPU3,
> > or CPU2 and CPU3)
> > Last print is the last one in init_kernel() function
>
> Core 0 will only finish if all other cores have done their init too.
>
> I recommend adding some debugging to try_init_kernel_secondary_core()
> and init_cpu() to see what where it gets stuck.
>
> Also be aware that debug printing may disappear if multiple cores
> print at exactly the same time, depending on the UART driver.
>
> Greetings,
>
> Indan
>
___
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems

[seL4] seL4 multicore boot failed on arm64

2024-04-25 Thread Leonid Meyerovich

Hello,

I run my seL4 application on 4 core ARMv8.

Recently I have developed some more application code (I mention it because
file system size is increased an I believe it may change boot time) and
from time to time I observed that boot process failed (stuck after the
following print)

calling schedule
calling  activate thread
kernel boot done.. CPU=1
calling schedule
calling  activate thread
kernel boot done.. CPU=2
calling schedule
calling  activate thread
kernel boot done.. CPU=3
Booting all finished, dropped to user space
calling schedule
calling  activate thread
kernel boot done.. CPU=0

Some time I see that only 2 CPU have been booted (like CPU1 and CPU3, or
CPU2 and CPU3)
Last print is the last one in init_kernel() function

Thanks you,
Leonid
___
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems

[seL4] Re: sel4test CACHEFLUSH0001 failed

2024-03-29 Thread Leonid Meyerovich

HI Indan,

*ptr = 0xC0FFEE;
__asm volatile("dmb sy" ::: "memory");
*ptrc = 0xDEADBEEF;

test_assert(*ptr == 0xC0FFEE);   < failed
test_assert(*ptrc == 0xDEADBEEF);

In this case 0xC0FFEE assertion failed.

Leonid


On Thu, Mar 28, 2024 at 5:39 PM Indan Zupancic  wrote:

> Hello Leonid,
>
> On 2024-03-28 20:18, Leonid Meyerovich wrote:
> > I run sel4test on the aarch64 platform.
>
> What CPU are you testing on?
>
> > My CACHEFLUSH0001 test in sel4test failed
> >  /* Clean makes data observable to non-cached page */
> > *ptr = 0xC0FFEE;
> > *ptrc = 0xDEADBEEF;
> > test_assert(*ptr == 0xC0FFEE);
> > test_assert(*ptrc == 0xDEADBEEF);
>
> The problem is that the test is not reliable, it assumes
> things it can't safely assume, even though they're usually
> correct. In this case it assumes that the cache line
> containing ptrc doesn't get evicted and that no memory
> reordering happened between the ptr and ptrc writes.
> See also https://github.com/seL4/sel4test/issues/80.
>
> That said, it should usually pass. Is it consistently
> failing for you?
>
> > I have tried to make to 'improve' memory/cache coherence,
> > but the last assertion still failed
>
> It's more likely that the 0xC0FFEE assertion fails,
> but for you the 0xDEADBEEF one fails?
>
> >  /* Clean makes data observable to non-cached page */
> > *ptr = 0xC0FFEE;
> > *ptrc = 0xDEADBEEF;
> >
> > error = seL4_ARM_Page_Clean_Data(framec, 0, PAGE_SIZE_4K);
> > error = seL4_ARM_Page_Invalidate_Data(framec, 0, PAGE_SIZE_4K);
> >
> > __asm volatile("dmb sy" ::: "memory");
>
> Try putting this after the *ptr = 0xC0FFEE; write.
>
> Tip for anyone needing cache maintenance on Aarch64:
> There is no need to use the seL4 system calls, you can
> do (non-invalidating) cache maintenance instructions
> from user space.
>
> Greetings,
>
> Indan
>
___
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems

[seL4] sel4test CACHEFLUSH0001 failed

2024-03-28 Thread Leonid Meyerovich

Hello,

I run sel4test on the aarch64 platform.

My CACHEFLUSH0001 test in sel4test failed
 /* Clean makes data observable to non-cached page */
*ptr = 0xC0FFEE;
*ptrc = 0xDEADBEEF;
test_assert(*ptr == 0xC0FFEE);
test_assert(*ptrc == 0xDEADBEEF);


I have tried to make to 'improve' memory/cache coherence, but the last
assertion still failed

 /* Clean makes data observable to non-cached page */
*ptr = 0xC0FFEE;
*ptrc = 0xDEADBEEF;

error = seL4_ARM_Page_Clean_Data(framec, 0, PAGE_SIZE_4K);
error = seL4_ARM_Page_Invalidate_Data(framec, 0, PAGE_SIZE_4K);

__asm volatile("dmb sy" ::: "memory");

test_assert(*ptr == 0xC0FFEE);
test_assert(*ptrc == 0xDEADBEEF);

Thank you,
Leonid
___
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems

[seL4] Re: root task executable memory changed

2024-02-08 Thread Leonid Meyerovich

Thank you Indan.

On Thu, Feb 8, 2024 at 7:47 AM Indan Zupancic  wrote:

> Hello Leonid,
>
> On 2024-02-07 20:19, Leonid Meyerovich wrote:
> > Yes I see all my other tasks have different flags for segment 0 - RE,
> > Startup flag is RWI
> > Is there any document that describes this limitation?
>
> I don't think the ABI between the kernel and Elfloader/root task is
> documented anywhere. Only bootinfo is documented, but that's only
> one part of the boot ABI. That said, because it's all part of the
> same project, I don't think this is fixed or guaranteed to stay
> the same, so users shouldn't assume more than what is provided by
> bootinfo. Anyway, e.g. for aarch64 it's somewhat described here:
>
> https://github.com/seL4/seL4/blob/master/src/arch/arm/64/head.S#L127
>
> Greetings,
>
> Indan
>
___
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems

[seL4] Re: root task executable memory changed

2024-02-07 Thread Leonid Meyerovich

Thanks Indan,

Yes I see all my other tasks have different flags for segment 0 - RE,
Startup flag is RWI
Is there any document that describes this limitation?

Thanks,
Leonid


readelf -l Logger

Elf file type is EXEC (Executable file)
Entry point 0x40018c
There are 5 program headers, starting at offset 64

Program Headers:
  Type   Offset VirtAddr   PhysAddr
 FileSizMemSiz  Flags  Align
  LOAD   0x 0x0040 0x0040
 0x000a5e94 0x000a5e94 * R E*0x1000
  LOAD   0x000a5f90 0x004a6f90 0x004a6f90
 0x13e8 0x00219310  RW 0x1000
  TLS0x000a5f90 0x004a6f90 0x004a6f90
 0x 0x000c  R  0x8
  GNU_STACK  0x 0x 0x
 0x 0x  RW 0x10
  GNU_RELRO  0x000a5f90 0x004a6f90 0x004a6f90
 0x0070 0x0070  R  0x1

 Section to Segment mapping:
  Segment Sections...
   00 .init .text .fini .rodata .eh_frame
   01 .init_array .fini_array .got .got.plt .data __vsyscall
_ps_irqchips .bss
   02 .tbss
   03
   04 .init_array .fini_array .got .got.plt

On Wed, Feb 7, 2024 at 2:57 PM Indan Zupancic  wrote:

> Hello Leonid,
>
> On 2024-02-07 18:15, Leonid Meyerovich wrote:
> > Using readelf helps, but I think there is some difference between
> > running readelf on the file and
> > parsing elf header in the memory (because my root process is already
> > in the memory)
> > As you can see below size of executable segment is different: readelf
> > =3923cb0, mycode=3923EB0
> > Also Entry point is different
>
> This is unexpected, are you sure you are comparing the same binary?
>
> > Second segment starting address and size are the same (?)
> > I use __executable_start to parse ELF header in the memory
>
> I don't think you can count on the ELF header being there though.
>
> > readelf -l Startup
> >
> > Elf file type is EXEC (Executable file)
> > Entry point 0x40ef88
> > There are 4 program headers, starting at offset 64
> >
> > Program Headers:
> >   Type   Offset VirtAddr   PhysAddr
> >  FileSizMemSiz  Flags  Align
> >   LOAD   0x 0x0040
> > 0x0040
> >  0x03923cb0 0x03923cb0  RWE0x1000
> >   LOAD   0x 0x03d3
> > 0x03d3
> >  0x 0x00aca428  RW 0x1000
> >   TLS0x000cb490 0x004cb490
> > 0x004cb490
> >  0x 0x000c  R  0x8
> >   GNU_STACK  0x 0x
> > 0x
> >  0x 0x  RW 0x10
> >
> >  Section to Segment mapping:
> >   Segment Sections...
> >00 .init .text .fini .rodata .eh_frame .init_array .fini_array
> > .got .got.plt .data ._archive_cpio __vsyscall _ps_irqchips
>
> Anyway, writeable sections are put into segment 0 too, like .data,
> so you can't just checksum the whole segment.
>
> If you want to do these kind of things it's better to do with your
> own linker script, then you have full control and can also let the
> linker define section start and end symbols so you don't need to
> parse ELF headers.
>
> That said, the seL4 kernel has limitations, which is the reason
> everything is put in the same segment for the startup task.
>
> In your case just checksum between __executable_start and __etext,
> which marks the end of the executable section.
>
> (If you worry that your program is being modified, you can
> just load your own program with proper memory protection
> where you do everything and do as little as possible in
> the startup task.)
>
> Greetings,
>
> Indan
>
___
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems

[seL4] Re: root task executable memory changed

2024-02-07 Thread Leonid Meyerovich

Thank you Indan,

Using readelf helps, but I think there is some difference between running
readelf on the file and
parsing elf header in the memory (because my root process is already in the
memory)
As you can see below size of executable segment is different: readelf
=*3923cb0,
*mycode=*3923EB0*
Also Entry point is different

Second segment starting address and size are the same (?)
I use __executable_start to parse ELF header in the memory

Thanks,
Leonid

readelf -l Startup

Elf file type is EXEC (Executable file)
Entry point 0x40ef88
There are 4 program headers, starting at offset 64

Program Headers:
  Type   Offset VirtAddr   PhysAddr
 FileSizMemSiz  Flags  Align
  LOAD   0x 0x0040 0x0040
 0x03923cb0 *0x03923cb0  *RWE0x1000
  LOAD   0x 0x03d3 0x03d3
 0x 0x00aca428  RW 0x1000
  TLS0x000cb490 0x004cb490 0x004cb490
 0x 0x000c  R  0x8
  GNU_STACK  0x 0x 0x
 0x 0x  RW 0x10

 Section to Segment mapping:
  Segment Sections...
   00 .init .text .fini .rodata .eh_frame .init_array .fini_array .got
.got.plt .data ._archive_cpio __vsyscall _ps_irqchips
   01 .bss
   02 .tbss
   03
 my code 
ELF Header:
  Type: 2
  Machine: 183
  Version: 1
  Entry point address: 0x40f218
  Start of program headers: 64 bytes into file
  Number of program headers: 4
  Size of program header: 56 bytes
Segment 0:
  Type: 1
  Flags: 7
  Virtual address: 0x40
  Physical address: 0x40
  Size in file: 59915952 bytes(*3923EB0*)
  Size in memory: 59915952 bytes
  Alignment: 4096
Segment 1:
  Type: 1
  Flags: 6
  Virtual address: 0x3d3
  Physical address: 0x3d3
  Size in file: 0 bytes
  Size in memory: 11314216 bytes  ( *aca428*)
  Alignment: 4096
Segment 2:
  Type: 7
  Flags: 4
  Virtual address: 0x4cb990
  Physical address: 0x4cb990
  Size in file: 0 bytes
  Size in memory: 12 bytes
  Alignment: 8
Segment 3:
  Type: 1685382481
  Flags: 6
  Virtual address: 0x0
  Physical address: 0x0
  Size in file: 0 bytes
  Size in memory: 0 bytes
  Alignment: 16

On Wed, Feb 7, 2024 at 9:24 AM Indan Zupancic  wrote:

> Hello Leonid,
>
> On 2024-02-06 19:48, Leonid Meyerovich wrote:
> > Some time when I change (add) some code in amu process I have an error
> > that
> > Monitor process prints
> >
> > CHECKSUM ERROR  Someone modified executable memory
> > process=Startup
> >   0x40 8868997 last->10daf436f961b809 this->95ebd3119aee7736
> >
> > It always complains about the root (Startup) task. Checksum value
> > changes
> > every time the Startup process calculates it.
>
> Sounds like it may depend on whether the file size is odd or even.
> Are you accidentally checksumming past the end of the section?
>
> > The code that calculate executable segment are:
>
> You can check if you're checking the right segment by comparing
> what your code finds with `readelf -l` output on your binary
> (not on the final image, but on the root task's binary).
>
> Greetings,
>
> Indan
>
___
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems

[seL4] root task executable memory changed

2024-02-06 Thread Leonid Meyerovich

Hello,

I have a seL4 project that creates a number of processes with multiple
threads. An application works fine. Every process periodically calculates
the checksum of the executable segment and the system (Monitor process)
keeps track that these values should be the same over the time.
Some time when I change (add) some code in amu process I have an error that
Monitor process prints

CHECKSUM ERROR  Someone modified executable memory process=Startup
  0x40 8868997 last->10daf436f961b809 this->95ebd3119aee7736

It always complains about the root (Startup) task. Checksum value changes
every time the Startup process calculates it.

The code that calculate executable segment are:

typedef struct
{
  unsigned char e_ident[EI_NIDENT]; /* Magic number and other info */
  Elf64_Half e_type; /* Object file type */
  Elf64_Half e_machine; /* Architecture */
  Elf64_Word e_version; /* Object file version */
  Elf64_Addr e_entry; /* Entry point virtual address */
  Elf64_Off e_phoff; /* Program header table file offset */
  Elf64_Off e_shoff; /* Section header table file offset */
  Elf64_Word e_flags; /* Processor-specific flags */
  Elf64_Half e_ehsize; /* ELF header size in bytes */
  Elf64_Half e_phentsize; /* Program header table entry size */
  Elf64_Half e_phnum; /* Program header table entry count */
  Elf64_Half e_shentsize; /* Section header table entry size */
  Elf64_Half e_shnum; /* Section header table entry count */
  Elf64_Half e_shstrndx; /* Section header string table index */
} Elf64_Ehdr;


extern char __executable_start[];

// function returns executable segment start address and size
int initStartupElfSegsParams(Elf64_Ehdr *pELFHeader, uintptr_t *startAddr,
uintptr_t *size)
{
seL4_Word phoff = pELFHeader->e_phoff;
Elf_Phdr *currentPH = (Elf_Phdr *)((void *)pELFHeader + phoff);
for (int i=0; ie_phnum; i++)
{
ZF_LOGD("ELF:  p_type=%x p_flags=%x p_vaddr=%p p_memsz=%lu",
currentPH[i].p_type, currentPH[i].p_flags, (void *)currentPH[i].p_vaddr,
currentPH[i].p_memsz);
if ( ((currentPH[i].p_type & 1) == 1) && ((currentPH[i].p_flags & 1) == 1))
// p_flags & 1 == 1 - executable
{
*startAddr = (uintptr_t)currentPH[i].p_vaddr;
*size = (uintptr_t)currentPH[i].p_memsz / sizeof(uint64_t);
return 0;
}
}

return -1;
};

initStartupElfSegsParams((Elf64_Ehdr *)__executable_start,
_validate_params[STARTUP_INDEX].p_addr,
_validate_params[STARTUP_INDEX].p_size);

Any help will be appreciated.
Thanks
___
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems

[seL4] Fwd: fault processing

2024-01-26 Thread Leonid Meyerovich

Even some more information:

These is a function
word_t Arch_setMRs_fault(tcb_t *sender, tcb_t *receiver, word_t
*receiveIPCBuffer, word_t faultType)
which populate a message and send it to fault handler.
In this function
   case seL4_Fault_VCPUFault:
return setMR(receiver, receiveIPCBuffer, seL4_VCPUFault_HSR,
seL4_Fault_VCPUFault_get_hsr(sender->tcbFault));
This is only information that sent to fault handler, but
for seL4_Fault_VMFault it provides nuch more

  case seL4_Fault_VMFault: {
if (config_set(CONFIG_ARM_HYPERVISOR_SUPPORT)) {
word_t ipa, va;
va = getRestartPC(sender);
ipa = (addressTranslateS1CPR(va) & ~MASK(PAGE_BITS)) | (va &
MASK(PAGE_BITS));
setMR(receiver, receiveIPCBuffer, seL4_VMFault_IP, ipa);



Just some addition: I have found function
seL4_Fault_VCPUFault_get_HSR(seL4_Fault_t seL4_Fault)
It gives me the value of HSR register, but how can I get fault address and
some other (if exist) information?

Thanks,

-- Forwarded message -
From: Leonid Meyerovich 
Date: Fri, Jan 26, 2024 at 11:35 AM
Subject: fault processing
To: 


I am working on fault processing.
When I am a fault I am calling
void sel4utils_print_fault_message(seL4_MessageInfo_t tag, const char
*thread_name) from sel4libsutils library
I have tested it for "page fault" condition and it works fine - I am
getting seL4_Fault_VMFault fault type

But in certain case I have got seL4_Fault_VCPUFault type, which is not
implemented sel4libsutils library

I try to process this fault similar to seL4_Fault_VMFault to get all
neccessary registers, but
the kernel does not have functions like seL4_Fault_VCPUFault_get_IP.

What is the message format for VCPU fault?
Thanks
___
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems

[seL4] Fwd: fault processing

2024-01-26 Thread Leonid Meyerovich

Just some addition: I have found function
seL4_Fault_VCPUFault_get_HSR(seL4_Fault_t seL4_Fault)
It gives me the value of HSR register, but how can I get fault address and
some other (if exist) information?

Thanks,

-- Forwarded message -
From: Leonid Meyerovich 
Date: Fri, Jan 26, 2024 at 11:35 AM
Subject: fault processing
To: 

I am working on fault processing.
When I am a fault I am calling
void sel4utils_print_fault_message(seL4_MessageInfo_t tag, const char
*thread_name) from sel4libsutils library
I have tested it for "page fault" condition and it works fine - I am
getting seL4_Fault_VMFault fault type

But in certain case I have got seL4_Fault_VCPUFault type, which is not
implemented sel4libsutils library

I try to process this fault similar to seL4_Fault_VMFault to get all
neccessary registers, but
the kernel does not have functions like seL4_Fault_VCPUFault_get_IP.

What is the message format for VCPU fault?
Thanks
___
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems

[seL4] fault processing

2024-01-26 Thread Leonid Meyerovich

I am working on fault processing.
When I am a fault I am calling
void sel4utils_print_fault_message(seL4_MessageInfo_t tag, const char
*thread_name) from sel4libsutils library
I have tested it for "page fault" condition and it works fine - I am
getting seL4_Fault_VMFault fault type

But in certain case I have got seL4_Fault_VCPUFault type, which is not
implemented sel4libsutils library

I try to process this fault similar to seL4_Fault_VMFault to get all
neccessary registers, but
the kernel does not have functions like seL4_Fault_VCPUFault_get_IP.

What is the message format for VCPU fault?
Thanks
___
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems

[seL4] Re: seL4 fault processing

2024-01-25 Thread Leonid Meyerovich

Thank you

On Thu, Jan 25, 2024 at 7:09 AM Indan Zupancic  wrote:

> Hello Leonid,
>
> On 2024-01-24 21:16, Leonid Meyerovich wrote:
> > I don't have any faults if I use   seL4_Recv instead (in a separate
> > thread).
> > It happens only if I use  seL4_NBRecv and check the tag after it
> > returns.
>
> If there is no message or fault pending, seL4_NBRecv() will return
> immediately.
> When that happens, the badge value will be zero and no messageInfo will
> be
> returned. That is, whatever was in register X1 at the time of the call
> will
> be returned.
>
> You have to use non-zero badges and check the badge value for
> non-blocking
> system calls, assuming you actually want non-blocking behaviour, which
> is
> unlikely.
>
> The only way to find this out is by reading the code, it's not
> documented
> in the manual as it should have been.
>
> Greetings,
>
> Indan
>
___
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems

[seL4] Re: seL4 fault processing

2024-01-24 Thread Leonid Meyerovich

I don't have any faults if I use   seL4_Recv instead (in a separate thread).
It happens only if I use  seL4_NBRecv and check the tag after it returns.
I use AARCH64

On Wed, Jan 24, 2024 at 3:59 PM Alwin Joshy  wrote:

> Which architecture are you on and are you using the hardware debug API? I
> think 4 is for debug exceptions.
>
> - Alwin
>
___
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems

[seL4] seL4 root task executable memory region

2024-01-24 Thread Leonid Meyerovich

I assume that the code segment of the root task starts
from __executable_start address. Does it point to ELF header? Or code
starts directly from this address?

Thank you,
___
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems

[seL4] seL4 fault processing

2024-01-24 Thread Leonid Meyerovich

My root task (root thread created by kernel) checks for fault from the
other threads, which are created in root thread with badged fault_ep

seL4_Word badge;
seL4_MessageInfo_t messageInfo = seL4_NBRecv(init_objects.fault_cap,
);
if (seL4_MessageInfo_get_label(messageInfo) != seL4_Fault_NullFault )
{
process_fault(messageInfo, badge);
}

Normally I don't have any faults, but every time I have
seL4_MessageInfo_get_label(messageInfo) == 4, which is not in
seL4_Fault_tag enumeration type

enum seL4_Fault_tag {
seL4_Fault_NullFault = 0,
seL4_Fault_CapFault = 1,
seL4_Fault_UnknownSyscall = 2,
seL4_Fault_UserException = 3,
seL4_Fault_VMFault = 5,
seL4_Fault_VGICMaintenance = 6,
seL4_Fault_VCPUFault = 7,
seL4_Fault_VPPIEvent = 8
};

Could somebody explain?

Thanks,
___
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems

[seL4] Re: seL4 fault handling

2024-01-23 Thread Leonid Meyerovich

Thank you, links are very helpful

On Mon, Jan 22, 2024 at 4:36 PM Alwin Joshy  wrote:

> Hi Leonid,
>
> Not sure if/where there is complete documentation for what you're asking,
> but the reference manual has register descriptions for some of the
> mentioned faults in chapter 6.2. For the ones that don't have full register
> descriptions there, you might find the following files useful
>
>
> https://github.com/seL4/seL4/blob/cc3205ea486f6ce3da3a64d8a99e166f047b8419/libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/constants.h
> <https://github.com/seL4/seL4/blob/cc3205ea486f6ce3da3a64d8a99e166f047b8419/libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/constants.h#L48>
>
> https://github.com/seL4/seL4/blob/master/libsel4/include/sel4/shared_types.h#L23
>
> https://github.com/seL4/seL4/blob/master/src/api/faults.c#L191
>
> https://github.com/seL4/seL4/blob/master/include/arch/arm/arch/64/mode/machine/registerset.h#L177
> https://github.com/seL4/seL4/blob/master/src/arch/arm/api/faults.c#L33
>
> - Alwin
>
> --
> *From:* Leonid Meyerovich 
> *Sent:* Tuesday, January 23, 2024 7:03 AM
> *To:* devel@sel4.systems 
> *Subject:* [seL4] seL4 fault handling
>
> [Some people who received this message don't often get email from
> leo...@trustedst.com. Learn why this is important at
> https://aka.ms/LearnAboutSenderIdentification ]
>
> Hello,
>
> Where can I find a comprehensive description of fault message registers for
> every of the following faults
>
> enum seL4_Fault_tag {
> seL4_Fault_NullFault = 0,
> seL4_Fault_CapFault = 1,
> seL4_Fault_UnknownSyscall = 2,
> seL4_Fault_UserException = 3,
> seL4_Fault_VMFault = 5,
> seL4_Fault_VGICMaintenance = 6,
> seL4_Fault_VCPUFault = 7,
> seL4_Fault_VPPIEvent = 8
> };
>
> Thanks,
> LM
> ___
> Devel mailing list -- devel@sel4.systems
> To unsubscribe send an email to devel-leave@sel4.systems
>
___
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems

[seL4] seL4 fault handling

2024-01-22 Thread Leonid Meyerovich

Hello,

Where can I find a comprehensive description of fault message registers for
every of the following faults

enum seL4_Fault_tag {
seL4_Fault_NullFault = 0,
seL4_Fault_CapFault = 1,
seL4_Fault_UnknownSyscall = 2,
seL4_Fault_UserException = 3,
seL4_Fault_VMFault = 5,
seL4_Fault_VGICMaintenance = 6,
seL4_Fault_VCPUFault = 7,
seL4_Fault_VPPIEvent = 8
};

Thanks,
LM
___
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems

Re: [seL4] Zynq UltraScale+ locks up after hours running

2019-10-04 Thread Leonid Meyerovich

Hi Yanyan,

I thought about just long integer variable, incremented inside clh_lock_acquire 
loop.
I may also try to enable CONFIG_ENABLE_BENCHMARKS and to use timestamp() 
function.

Thanks,
Leonid


From: Shen, Yanyan (Data61, Kensington NSW) 
Sent: Friday, October 4, 2019 11:23 AM
To: Leonid Meyerovich ; devel@sel4.systems
Subject: Re: [seL4] Zynq UltraScale+ locks up after hours running

Hi Leonid,
Yes I mean CPU cycle counters.

Regards,
Yanyan

From: Leonid Meyerovich mailto:lmeyerov...@i-a-i.com>>
Sent: Friday, October 4, 2019 11:00:31 PM
To: Shen, Yanyan (Data61, Kensington NSW) 
mailto:yanyan.s...@data61.csiro.au>>; 
devel@sel4.systems<mailto:devel@sel4.systems> 
mailto:devel@sel4.systems>>
Subject: RE: [seL4] Zynq UltraScale+ locks up after hours running

Hi Yanyan,

Actually I do have JTAG, but I am not sure how I can use it without any 
development environment. Is there any JTAG application that I can use while 
connected to my device through JTAG interface?

The second method is also looks promising. What is CPU timestamp? I can use 
simple counter to estimate the time waiting for big lock.

Thanks,
Leonid


-Original Message-
From: Shen, Yanyan (Data61, Kensington NSW) 
mailto:yanyan.s...@data61.csiro.au>>
Sent: Friday, October 4, 2019 10:35 AM
To: Leonid Meyerovich mailto:lmeyerov...@i-a-i.com>>; 
devel@sel4.systems<mailto:devel@sel4.systems>
Subject: RE: [seL4] Zynq UltraScale+ locks up after hours running

Hi Leonid,

It would be helpful if you could use JTAG, so you can observe the instruction 
pointers of the cores. If it is the case, three cores should execute several 
instructions repeatedly.

If  you do not have access to JTAG, maybe you could read CPU timestamps in the 
while loop of the inline function clh_lock_acqure in kernel/include/smp/lock.h. 
If a core has spent too much time in the loop (e.g. several seconds), and three 
cores report the same condition, we probably hit the scenario.


Regards,
Yanyan


-Original Message-
From: Leonid Meyerovich mailto:lmeyerov...@i-a-i.com>>
Sent: Friday, 4 October 2019 10:19 PM
To: Shen, Yanyan (Data61, Kensington NSW) 
mailto:yanyan.s...@data61.csiro.au>>; 
devel@sel4.systems<mailto:devel@sel4.systems>
Subject: RE: [seL4] Zynq UltraScale+ locks up after hours running

Hi Yanyan,

It would explain everything.
How to proof/disprove it?

Thanks,
Leonid

-Original Message-
From: Shen, Yanyan (Data61, Kensington NSW) 
mailto:yanyan.s...@data61.csiro.au>>
Sent: Friday, October 4, 2019 10:11 AM
To: Leonid Meyerovich mailto:lmeyerov...@i-a-i.com>>; 
devel@sel4.systems<mailto:devel@sel4.systems>
Subject: RE: [seL4] Zynq UltraScale+ locks up after hours running

HI Leonid,

For the big lock kernel, a possibility is that one core is in kernel mode, and 
for some reasons, it does not release the kernel big lock. Other cores keep 
trying to grab the lock when they need to handle interrupts or system calls, 
but they fail because the lock is not released.


Regards,
Yanyan


-Original Message-
From: Leonid Meyerovich mailto:lmeyerov...@i-a-i.com>>
Sent: Friday, 4 October 2019 10:00 PM
To: Shen, Yanyan (Data61, Kensington NSW) 
mailto:yanyan.s...@data61.csiro.au>>; 
devel@sel4.systems<mailto:devel@sel4.systems>
Subject: RE: [seL4] Zynq UltraScale+ locks up after hours running

Hi Yanyan,

Yes, our VMM is based on the libsel4armvmm.
My prints is implemented in ISR and it is printing until the system receives 
timer interrupt. That is how I understand that I don't have a timer interrupt 
anymore.
Usually I print from timer interrupt every second (the log below was 
implemented for different purpose).

BTW, kernel is running on every core, how it is possible that all cores stop 
receiving a timer interrupt (actually not just timer, but also IPI)?

Thanks,
Leonid




-Original Message-
From: Shen, Yanyan (Data61, Kensington NSW) 
mailto:yanyan.s...@data61.csiro.au>>
Sent: Friday, October 4, 2019 9:49 AM
To: Leonid Meyerovich mailto:lmeyerov...@i-a-i.com>>; 
devel@sel4.systems<mailto:devel@sel4.systems>
Subject: RE: [seL4] Zynq UltraScale+ locks up after hours running

Hi Leonid,

It looks like the seL4 v8.0.0 does not include Armv8 virtualization extension 
support yet ...
So basically you wrote the VMM based on the libsel4armvmm?

I am a bit confused by the interrupt log you provided.

It looks like the log output depends on getting kernel timer interrupts.

case IRQTimer:
timerTick();
resetTimer();
if ((++tickCount % 200) == 0)
{
printInt(0);
printf("- - - \n");
printInt(1);
printf("- - - \n");
printInt(2);
printf("- - - \n");
printInt(3);
printf("- - - - - - -  \n");
cleanIntStat();
}
break;


 ---irq stat: cpu=0 (

Re: [seL4] Zynq UltraScale+ locks up after hours running

2019-10-04 Thread Leonid Meyerovich

Hi Yanyan,

Actually I do have JTAG, but I am not sure how I can use it without any 
development environment. Is there any JTAG application that I can use while 
connected to my device through JTAG interface?

The second method is also looks promising. What is CPU timestamp? I can use 
simple counter to estimate the time waiting for big lock.

Thanks,
Leonid


-Original Message-
From: Shen, Yanyan (Data61, Kensington NSW) 
Sent: Friday, October 4, 2019 10:35 AM
To: Leonid Meyerovich ; devel@sel4.systems
Subject: RE: [seL4] Zynq UltraScale+ locks up after hours running

Hi Leonid,

It would be helpful if you could use JTAG, so you can observe the instruction 
pointers of the cores. If it is the case, three cores should execute several 
instructions repeatedly.

If  you do not have access to JTAG, maybe you could read CPU timestamps in the 
while loop of the inline function clh_lock_acqure in kernel/include/smp/lock.h. 
If a core has spent too much time in the loop (e.g. several seconds), and three 
cores report the same condition, we probably hit the scenario.


Regards,
Yanyan


-Original Message-
From: Leonid Meyerovich 
Sent: Friday, 4 October 2019 10:19 PM
To: Shen, Yanyan (Data61, Kensington NSW) ; 
devel@sel4.systems
Subject: RE: [seL4] Zynq UltraScale+ locks up after hours running

Hi Yanyan,

It would explain everything.
How to proof/disprove it?

Thanks,
Leonid

-Original Message-
From: Shen, Yanyan (Data61, Kensington NSW) 
Sent: Friday, October 4, 2019 10:11 AM
To: Leonid Meyerovich ; devel@sel4.systems
Subject: RE: [seL4] Zynq UltraScale+ locks up after hours running

HI Leonid,

For the big lock kernel, a possibility is that one core is in kernel mode, and 
for some reasons, it does not release the kernel big lock. Other cores keep 
trying to grab the lock when they need to handle interrupts or system calls, 
but they fail because the lock is not released.


Regards,
Yanyan


-Original Message-
From: Leonid Meyerovich 
Sent: Friday, 4 October 2019 10:00 PM
To: Shen, Yanyan (Data61, Kensington NSW) ; 
devel@sel4.systems
Subject: RE: [seL4] Zynq UltraScale+ locks up after hours running

Hi Yanyan,

Yes, our VMM is based on the libsel4armvmm.
My prints is implemented in ISR and it is printing until the system receives 
timer interrupt. That is how I understand that I don't have a timer interrupt 
anymore.
Usually I print from timer interrupt every second (the log below was 
implemented for different purpose).

BTW, kernel is running on every core, how it is possible that all cores stop 
receiving a timer interrupt (actually not just timer, but also IPI)?

Thanks,
Leonid




-Original Message-
From: Shen, Yanyan (Data61, Kensington NSW) 
Sent: Friday, October 4, 2019 9:49 AM
To: Leonid Meyerovich ; devel@sel4.systems
Subject: RE: [seL4] Zynq UltraScale+ locks up after hours running

Hi Leonid,

It looks like the seL4 v8.0.0 does not include Armv8 virtualization extension 
support yet ...
So basically you wrote the VMM based on the libsel4armvmm?

I am a bit confused by the interrupt log you provided.

It looks like the log output depends on getting kernel timer interrupts.

case IRQTimer:
timerTick();
resetTimer();
if ((++tickCount % 200) == 0)
{
printInt(0);
printf("- - - \n");
printInt(1);
printf("- - - \n");
printInt(2);
printf("- - - \n");
printInt(3);
printf("- - - - - - -  \n");
cleanIntStat();
}
break;


 ---irq stat: cpu=0 (2) 26_50_500_258_258
- - -
---irq stat: cpu=1 (2) 26_50_500_258_258
- - -
---irq stat: cpu=2 (2) 26_50_500_258_258
- - -
---irq stat: cpu=3 (3) 26_50_5065_1_159_1_1
- - - - - - -
---irq stat: cpu=0 (2) 26_50_500_257_257
- - -
---irq stat: cpu=1 (2) 26_50_500_280_280
- - -
---irq stat: cpu=2 (2) 26_50_500_280_280


I am a bit confused, and correct me if I am wrong.  If you do not get kernel 
timer interrupts, how could you get the output above? I guess at least one core 
got kernel timer interrupts to get the output?


Regards,
Yanyan


-Original Message-
From: Leonid Meyerovich 
Sent: Friday, 4 October 2019 9:11 PM
To: Shen, Yanyan (Data61, Kensington NSW) ; 
devel@sel4.systems
Subject: RE: [seL4] Zynq UltraScale+ locks up after hours running

Hi Yanyan,

I am running seL4 version 8.0.0.0.
Core 3 is running 7 processes which intensively communicate to each other, 
sending a messages.
One of this process sends/receives a lot of message to both VMs ("virtual 
channels"), another sends/receives a lot messages (~1000 per sec) to R5 
(openAmp).

VMM is running on core 0 and VMs are running on core 1 and 2.

Thanks,
Leonid


-Original Message-
From: Shen, Yanyan (Data61, Kensington NSW) 
Sent: Friday, October 4, 2019 8:58 AM
To: Leonid Meyerovich ; devel@sel4.systems
Subject: RE: [seL4] Zynq UltraScale+ locks up after hou

Re: [seL4] Zynq UltraScale+ locks up after hours running

2019-10-04 Thread Leonid Meyerovich

Hi Yanyan,

It would explain everything.
How to proof/disprove it?

Thanks,
Leonid

-Original Message-
From: Shen, Yanyan (Data61, Kensington NSW) 
Sent: Friday, October 4, 2019 10:11 AM
To: Leonid Meyerovich ; devel@sel4.systems
Subject: RE: [seL4] Zynq UltraScale+ locks up after hours running

HI Leonid,

For the big lock kernel, a possibility is that one core is in kernel mode, and 
for some reasons, it does not release the kernel big lock. Other cores keep 
trying to grab the lock when they need to handle interrupts or system calls, 
but they fail because the lock is not released.


Regards,
Yanyan


-Original Message-
From: Leonid Meyerovich 
Sent: Friday, 4 October 2019 10:00 PM
To: Shen, Yanyan (Data61, Kensington NSW) ; 
devel@sel4.systems
Subject: RE: [seL4] Zynq UltraScale+ locks up after hours running

Hi Yanyan,

Yes, our VMM is based on the libsel4armvmm.
My prints is implemented in ISR and it is printing until the system receives 
timer interrupt. That is how I understand that I don't have a timer interrupt 
anymore.
Usually I print from timer interrupt every second (the log below was 
implemented for different purpose).

BTW, kernel is running on every core, how it is possible that all cores stop 
receiving a timer interrupt (actually not just timer, but also IPI)?

Thanks,
Leonid




-Original Message-
From: Shen, Yanyan (Data61, Kensington NSW) 
Sent: Friday, October 4, 2019 9:49 AM
To: Leonid Meyerovich ; devel@sel4.systems
Subject: RE: [seL4] Zynq UltraScale+ locks up after hours running

Hi Leonid,

It looks like the seL4 v8.0.0 does not include Armv8 virtualization extension 
support yet ...
So basically you wrote the VMM based on the libsel4armvmm?

I am a bit confused by the interrupt log you provided.

It looks like the log output depends on getting kernel timer interrupts.

case IRQTimer:
timerTick();
resetTimer();
if ((++tickCount % 200) == 0)
{
printInt(0);
printf("- - - \n");
printInt(1);
printf("- - - \n");
printInt(2);
printf("- - - \n");
printInt(3);
printf("- - - - - - -  \n");
cleanIntStat();
}
break;


 ---irq stat: cpu=0 (2) 26_50_500_258_258
- - -
---irq stat: cpu=1 (2) 26_50_500_258_258
- - -
---irq stat: cpu=2 (2) 26_50_500_258_258
- - -
---irq stat: cpu=3 (3) 26_50_5065_1_159_1_1
- - - - - - -
---irq stat: cpu=0 (2) 26_50_500_257_257
- - -
---irq stat: cpu=1 (2) 26_50_500_280_280
- - -
---irq stat: cpu=2 (2) 26_50_500_280_280


I am a bit confused, and correct me if I am wrong.  If you do not get kernel 
timer interrupts, how could you get the output above? I guess at least one core 
got kernel timer interrupts to get the output?


Regards,
Yanyan


-Original Message-
From: Leonid Meyerovich 
Sent: Friday, 4 October 2019 9:11 PM
To: Shen, Yanyan (Data61, Kensington NSW) ; 
devel@sel4.systems
Subject: RE: [seL4] Zynq UltraScale+ locks up after hours running

Hi Yanyan,

I am running seL4 version 8.0.0.0.
Core 3 is running 7 processes which intensively communicate to each other, 
sending a messages.
One of this process sends/receives a lot of message to both VMs ("virtual 
channels"), another sends/receives a lot messages (~1000 per sec) to R5 
(openAmp).

VMM is running on core 0 and VMs are running on core 1 and 2.

Thanks,
Leonid


-Original Message-
From: Shen, Yanyan (Data61, Kensington NSW) 
Sent: Friday, October 4, 2019 8:58 AM
To: Leonid Meyerovich ; devel@sel4.systems
Subject: RE: [seL4] Zynq UltraScale+ locks up after hours running

Hi Leonid,

I forgot to ask, what seL4 version are you using? Is it from the Data61 Github 
repo? If you also use CAmkES, which version is it? It would be helpful if you 
could isolate the 2 VMs, so we could have a smaller system to understand. Based 
on your description, my understanding is you use one VMM running on core 0 to 
manage two VMs running on core 1 and core 2?

R5 is the always-on core? What does the application do?

Regards,
Yanyan


-Original Message-
From: Leonid Meyerovich 
Sent: Friday, 4 October 2019 8:26 PM
To: Shen, Yanyan (Data61, Kensington NSW) ; 
devel@sel4.systems
Subject: RE: [seL4] Zynq UltraScale+ locks up after hours running

Hi Yanyan,

Yes, VMM is running on core 0, creates 2 VM and run them on core 1 and core2. 
VM don't have any access to hardware and they receive virtual timer and 
maintenance interrupts.
I am not sure I can stop running all processes on core 3, I should think about 
it, but in this case the whole condition will change. Also I probably didn't 
mention that R5 also runs an application and communicates to the application, 
which is running on core3 through openAmp.

Thanks,
Leonid

-Original Message-
From: Shen, Yanyan (Data61, Kensington NSW) 
Sent: Friday, October 4, 2019 8:16 AM
To: Leonid Meyerovich ; devel@sel4.systems
S

Re: [seL4] Zynq UltraScale+ locks up after hours running

2019-10-04 Thread Leonid Meyerovich

Hi Yanyan,

Yes, our VMM is based on the libsel4armvmm.
My prints is implemented in ISR and it is printing until the system receives 
timer interrupt. That is how I understand that I don't have a timer interrupt 
anymore.
Usually I print from timer interrupt every second (the log below was 
implemented for different purpose).

BTW, kernel is running on every core, how it is possible that all cores stop 
receiving a timer interrupt (actually not just timer, but also IPI)?

Thanks,
Leonid




-Original Message-
From: Shen, Yanyan (Data61, Kensington NSW) 
Sent: Friday, October 4, 2019 9:49 AM
To: Leonid Meyerovich ; devel@sel4.systems
Subject: RE: [seL4] Zynq UltraScale+ locks up after hours running

Hi Leonid,

It looks like the seL4 v8.0.0 does not include Armv8 virtualization extension 
support yet ...
So basically you wrote the VMM based on the libsel4armvmm?

I am a bit confused by the interrupt log you provided.

It looks like the log output depends on getting kernel timer interrupts.

case IRQTimer:
timerTick();
resetTimer();
if ((++tickCount % 200) == 0)
{
printInt(0);
printf("- - - \n");
printInt(1);
printf("- - - \n");
printInt(2);
printf("- - - \n");
printInt(3);
printf("- - - - - - -  \n");
cleanIntStat();
}
break;


 ---irq stat: cpu=0 (2) 26_50_500_258_258
- - -
---irq stat: cpu=1 (2) 26_50_500_258_258
- - -
---irq stat: cpu=2 (2) 26_50_500_258_258
- - -
---irq stat: cpu=3 (3) 26_50_5065_1_159_1_1
- - - - - - -
---irq stat: cpu=0 (2) 26_50_500_257_257
- - -
---irq stat: cpu=1 (2) 26_50_500_280_280
- - -
---irq stat: cpu=2 (2) 26_50_500_280_280


I am a bit confused, and correct me if I am wrong.  If you do not get kernel 
timer interrupts, how could you get the output above? I guess at least one core 
got kernel timer interrupts to get the output?


Regards,
Yanyan


-Original Message-
From: Leonid Meyerovich 
Sent: Friday, 4 October 2019 9:11 PM
To: Shen, Yanyan (Data61, Kensington NSW) ; 
devel@sel4.systems
Subject: RE: [seL4] Zynq UltraScale+ locks up after hours running

Hi Yanyan,

I am running seL4 version 8.0.0.0.
Core 3 is running 7 processes which intensively communicate to each other, 
sending a messages.
One of this process sends/receives a lot of message to both VMs ("virtual 
channels"), another sends/receives a lot messages (~1000 per sec) to R5 
(openAmp).

VMM is running on core 0 and VMs are running on core 1 and 2.

Thanks,
Leonid


-Original Message-
From: Shen, Yanyan (Data61, Kensington NSW) 
Sent: Friday, October 4, 2019 8:58 AM
To: Leonid Meyerovich ; devel@sel4.systems
Subject: RE: [seL4] Zynq UltraScale+ locks up after hours running

Hi Leonid,

I forgot to ask, what seL4 version are you using? Is it from the Data61 Github 
repo? If you also use CAmkES, which version is it? It would be helpful if you 
could isolate the 2 VMs, so we could have a smaller system to understand. Based 
on your description, my understanding is you use one VMM running on core 0 to 
manage two VMs running on core 1 and core 2?

R5 is the always-on core? What does the application do?

Regards,
Yanyan


-Original Message-
From: Leonid Meyerovich 
Sent: Friday, 4 October 2019 8:26 PM
To: Shen, Yanyan (Data61, Kensington NSW) ; 
devel@sel4.systems
Subject: RE: [seL4] Zynq UltraScale+ locks up after hours running

Hi Yanyan,

Yes, VMM is running on core 0, creates 2 VM and run them on core 1 and core2. 
VM don't have any access to hardware and they receive virtual timer and 
maintenance interrupts.
I am not sure I can stop running all processes on core 3, I should think about 
it, but in this case the whole condition will change. Also I probably didn't 
mention that R5 also runs an application and communicates to the application, 
which is running on core3 through openAmp.

Thanks,
Leonid

-Original Message-
From: Shen, Yanyan (Data61, Kensington NSW) 
Sent: Friday, October 4, 2019 8:16 AM
To: Leonid Meyerovich ; devel@sel4.systems
Subject: RE: [seL4] Zynq UltraScale+ locks up after hours running

Hi Leonid,

What do you mean by "hypervisor on core 0"? Do you mean the VMM? I assume you 
create a VMM for each VM  running, and also pin the VMMs on the corresponding 
physical cores? If so, core 1 and core 2 also should receive virtual timer 
interrupts and VGIC maintenance interrupts. Is it possible that you stop 
running the processes on core 3 and just keep running the VMs on different 
cores? Do the VMs have any accesses to physical hardware, for instance, clocks 
or watchdogs?


Regards,
Yanyan


-Original Message-
From: Leonid Meyerovich 
Sent: Thursday, 3 October 2019 8:45 PM
To: Shen, Yanyan (Data61, Kensington NSW) ; 
devel@sel4.systems
Subject: RE: [seL4] Zynq UltraScale+ locks up after hours running

Hi Yanyan,

I am running in

Re: [seL4] Zynq UltraScale+ locks up after hours running

2019-10-04 Thread Leonid Meyerovich

Hi Yanyan,

The interrupts is disabled in kernel mode, is there any circumstances that it 
will not be enabled before returning to userland?

Thanks,
Leonid

-Original Message-
From: Shen, Yanyan (Data61, Kensington NSW) 
Sent: Friday, October 4, 2019 8:58 AM
To: Leonid Meyerovich ; devel@sel4.systems
Subject: RE: [seL4] Zynq UltraScale+ locks up after hours running

Hi Leonid,

I forgot to ask, what seL4 version are you using? Is it from the Data61 Github 
repo? If you also use CAmkES, which version is it? It would be helpful if you 
could isolate the 2 VMs, so we could have a smaller system to understand. Based 
on your description, my understanding is you use one VMM running on core 0 to 
manage two VMs running on core 1 and core 2?

R5 is the always-on core? What does the application do?

Regards,
Yanyan

-Original Message-
From: Leonid Meyerovich 
Sent: Friday, 4 October 2019 8:26 PM
To: Shen, Yanyan (Data61, Kensington NSW) ; 
devel@sel4.systems
Subject: RE: [seL4] Zynq UltraScale+ locks up after hours running

Hi Yanyan,

Yes, VMM is running on core 0, creates 2 VM and run them on core 1 and core2. 
VM don't have any access to hardware and they receive virtual timer and 
maintenance interrupts.
I am not sure I can stop running all processes on core 3, I should think about 
it, but in this case the whole condition will change. Also I probably didn't 
mention that R5 also runs an application and communicates to the application, 
which is running on core3 through openAmp.

Thanks,
Leonid

-Original Message-
From: Shen, Yanyan (Data61, Kensington NSW) 
Sent: Friday, October 4, 2019 8:16 AM
To: Leonid Meyerovich ; devel@sel4.systems
Subject: RE: [seL4] Zynq UltraScale+ locks up after hours running

Hi Leonid,

What do you mean by "hypervisor on core 0"? Do you mean the VMM? I assume you 
create a VMM for each VM  running, and also pin the VMMs on the corresponding 
physical cores? If so, core 1 and core 2 also should receive virtual timer 
interrupts and VGIC maintenance interrupts. Is it possible that you stop 
running the processes on core 3 and just keep running the VMs on different 
cores? Do the VMs have any accesses to physical hardware, for instance, clocks 
or watchdogs?

Regards,
Yanyan

-Original Message-----
From: Leonid Meyerovich 
Sent: Thursday, 3 October 2019 8:45 PM
To: Shen, Yanyan (Data61, Kensington NSW) ; 
devel@sel4.systems
Subject: RE: [seL4] Zynq UltraScale+ locks up after hours running

Hi Yanyan,

I am running initial task and hypervisor on core 0.
Hypervisor creates 2 VM and running them on core 1 and 2 Core 3 runs 7 
processes that communicate through notification objects and shared memory (in 
pairs) On process on core 3 implements UART based connection (, this is PL 
uart, Rx use  interrupt). On of core 3 process also runs SADA driver (also uses 
interrupt)

VMs communicate to the rest of the system through 'virtual channels' - 
exceptions and shared memory.

All hardware interrupts are processed by core 0 (please, correct me if I am 
wrong). But as far as I understand PL2 physical timer interrupt runs on every 
core.

Every processes prints some messages on terminal. I have never seen that these 
messages have been printed partially what the system lock up, process completes 
printing the message and has never scheduled again.
I have also printed some messages from inside of ISR after getting time 
interrupt (print interrupt counter once a second) and I don't see these 
messages when the system locks up.

Thank you,
Leonid

-Original Message-
From: Shen, Yanyan (Data61, Kensington NSW) 
Sent: Thursday, October 3, 2019 2:44 AM
To: Leonid Meyerovich ; devel@sel4.systems
Subject: Re: [seL4] Zynq UltraScale+ locks up after hours running

Hi Leonid,

Could you provide a bit more about your software configuration? For instance, 
do you have multiple VMs running on dedicated hardware cores?
How are the VM and processes configured?

Also, you mean there were no interrupts at all on all the four cores?

Regards,
Yanyan

On Wed, 2019-10-02 at 16:01 +0000, Leonid Meyerovich wrote:
> Hello,
>
> We are running seL4 microkernel on 4 cores Zynq UltraScale+ (zcu102
> board). The implementation includes multiple processes, hypervisor and
> virtual machine running on dedicated core. After several hours running
> (it could be 2 or even 8 hours) the whole microkernel locks up. After
> some investigation I have found that no interrupts generated anymore -
> at least there is no interrupts coming to ISR.
> Inside ISR I have monitored PL2 Physical Timer Control register, which
> feeds a scheduler and didn't find any problems - it stays enabled and
> not masked.
>
> I will appreciate any idea/direction for approaching this problem.
>
> Thank you,
>
> Leonid
>
>
>
>
> This message and all attachments are PRIVATE, and contain information
> that is PROPRIETARY to Intellig

Re: [seL4] Zynq UltraScale+ locks up after hours running

2019-10-04 Thread Leonid Meyerovich

Hi Yanyan,

I am running seL4 version 8.0.0.0.
Core 3 is running 7 processes which intensively communicate to each other, 
sending a messages.
One of this process sends/receives a lot of message to both VMs ("virtual 
channels"), another sends/receives a lot messages (~1000 per sec) to R5 
(openAmp).

VMM is running on core 0 and VMs are running on core 1 and 2.

Thanks,
Leonid

-Original Message-
From: Shen, Yanyan (Data61, Kensington NSW) 
Sent: Friday, October 4, 2019 8:58 AM
To: Leonid Meyerovich ; devel@sel4.systems
Subject: RE: [seL4] Zynq UltraScale+ locks up after hours running

Hi Leonid,

I forgot to ask, what seL4 version are you using? Is it from the Data61 Github 
repo? If you also use CAmkES, which version is it? It would be helpful if you 
could isolate the 2 VMs, so we could have a smaller system to understand. Based 
on your description, my understanding is you use one VMM running on core 0 to 
manage two VMs running on core 1 and core 2?

R5 is the always-on core? What does the application do?

Regards,
Yanyan

-Original Message-----
From: Leonid Meyerovich 
Sent: Friday, 4 October 2019 8:26 PM
To: Shen, Yanyan (Data61, Kensington NSW) ; 
devel@sel4.systems
Subject: RE: [seL4] Zynq UltraScale+ locks up after hours running

Hi Yanyan,

Yes, VMM is running on core 0, creates 2 VM and run them on core 1 and core2. 
VM don't have any access to hardware and they receive virtual timer and 
maintenance interrupts.
I am not sure I can stop running all processes on core 3, I should think about 
it, but in this case the whole condition will change. Also I probably didn't 
mention that R5 also runs an application and communicates to the application, 
which is running on core3 through openAmp.

Thanks,
Leonid

-Original Message-
From: Shen, Yanyan (Data61, Kensington NSW) 
Sent: Friday, October 4, 2019 8:16 AM
To: Leonid Meyerovich ; devel@sel4.systems
Subject: RE: [seL4] Zynq UltraScale+ locks up after hours running

Hi Leonid,

What do you mean by "hypervisor on core 0"? Do you mean the VMM? I assume you 
create a VMM for each VM  running, and also pin the VMMs on the corresponding 
physical cores? If so, core 1 and core 2 also should receive virtual timer 
interrupts and VGIC maintenance interrupts. Is it possible that you stop 
running the processes on core 3 and just keep running the VMs on different 
cores? Do the VMs have any accesses to physical hardware, for instance, clocks 
or watchdogs?

Regards,
Yanyan

-Original Message-
From: Leonid Meyerovich 
Sent: Thursday, 3 October 2019 8:45 PM
To: Shen, Yanyan (Data61, Kensington NSW) ; 
devel@sel4.systems
Subject: RE: [seL4] Zynq UltraScale+ locks up after hours running

Hi Yanyan,

I am running initial task and hypervisor on core 0.
Hypervisor creates 2 VM and running them on core 1 and 2 Core 3 runs 7 
processes that communicate through notification objects and shared memory (in 
pairs) On process on core 3 implements UART based connection (, this is PL 
uart, Rx use  interrupt). On of core 3 process also runs SADA driver (also uses 
interrupt)

VMs communicate to the rest of the system through 'virtual channels' - 
exceptions and shared memory.

All hardware interrupts are processed by core 0 (please, correct me if I am 
wrong). But as far as I understand PL2 physical timer interrupt runs on every 
core.

Every processes prints some messages on terminal. I have never seen that these 
messages have been printed partially what the system lock up, process completes 
printing the message and has never scheduled again.
I have also printed some messages from inside of ISR after getting time 
interrupt (print interrupt counter once a second) and I don't see these 
messages when the system locks up.

Thank you,
Leonid

-Original Message-
From: Shen, Yanyan (Data61, Kensington NSW) 
Sent: Thursday, October 3, 2019 2:44 AM
To: Leonid Meyerovich ; devel@sel4.systems
Subject: Re: [seL4] Zynq UltraScale+ locks up after hours running

Hi Leonid,

Could you provide a bit more about your software configuration? For instance, 
do you have multiple VMs running on dedicated hardware cores?
How are the VM and processes configured?

Also, you mean there were no interrupts at all on all the four cores?

Regards,
Yanyan

On Wed, 2019-10-02 at 16:01 +0000, Leonid Meyerovich wrote:
> Hello,
>
> We are running seL4 microkernel on 4 cores Zynq UltraScale+ (zcu102
> board). The implementation includes multiple processes, hypervisor and
> virtual machine running on dedicated core. After several hours running
> (it could be 2 or even 8 hours) the whole microkernel locks up. After
> some investigation I have found that no interrupts generated anymore -
> at least there is no interrupts coming to ISR.
> Inside ISR I have monitored PL2 Physical Timer Control register, which
> feeds a scheduler and didn't find any problems - it stays enabled and
> not masked.
>
> I will

Re: [seL4] Zynq UltraScale+ locks up after hours running

2019-10-04 Thread Leonid Meyerovich

Hi Yanyan,

Yes, VMM is running on core 0, creates 2 VM and run them on core 1 and core2. 
VM don't have any access to hardware and they receive virtual timer and 
maintenance interrupts.
I am not sure I can stop running all processes on core 3, I should think about 
it, but in this case the whole condition will change. Also I probably didn't 
mention that R5 also runs an application and communicates to the application, 
which is running on core3 through openAmp.

Thanks,
Leonid

-Original Message-
From: Shen, Yanyan (Data61, Kensington NSW) 
Sent: Friday, October 4, 2019 8:16 AM
To: Leonid Meyerovich ; devel@sel4.systems
Subject: RE: [seL4] Zynq UltraScale+ locks up after hours running

Hi Leonid,

What do you mean by "hypervisor on core 0"? Do you mean the VMM? I assume you 
create a VMM for each VM  running, and also pin the VMMs on the corresponding 
physical cores? If so, core 1 and core 2 also should receive virtual timer 
interrupts and VGIC maintenance interrupts. Is it possible that you stop 
running the processes on core 3 and just keep running the VMs on different 
cores? Do the VMs have any accesses to physical hardware, for instance, clocks 
or watchdogs?

Regards,
Yanyan

-Original Message-----
From: Leonid Meyerovich 
Sent: Thursday, 3 October 2019 8:45 PM
To: Shen, Yanyan (Data61, Kensington NSW) ; 
devel@sel4.systems
Subject: RE: [seL4] Zynq UltraScale+ locks up after hours running

Hi Yanyan,

I am running initial task and hypervisor on core 0.
Hypervisor creates 2 VM and running them on core 1 and 2 Core 3 runs 7 
processes that communicate through notification objects and shared memory (in 
pairs) On process on core 3 implements UART based connection (, this is PL 
uart, Rx use  interrupt). On of core 3 process also runs SADA driver (also uses 
interrupt)

VMs communicate to the rest of the system through 'virtual channels' - 
exceptions and shared memory.

All hardware interrupts are processed by core 0 (please, correct me if I am 
wrong). But as far as I understand PL2 physical timer interrupt runs on every 
core.

Every processes prints some messages on terminal. I have never seen that these 
messages have been printed partially what the system lock up, process completes 
printing the message and has never scheduled again.
I have also printed some messages from inside of ISR after getting time 
interrupt (print interrupt counter once a second) and I don't see these 
messages when the system locks up.

Thank you,
Leonid

-Original Message-
From: Shen, Yanyan (Data61, Kensington NSW) 
Sent: Thursday, October 3, 2019 2:44 AM
To: Leonid Meyerovich ; devel@sel4.systems
Subject: Re: [seL4] Zynq UltraScale+ locks up after hours running

Hi Leonid,

Could you provide a bit more about your software configuration? For instance, 
do you have multiple VMs running on dedicated hardware cores?
How are the VM and processes configured?

Also, you mean there were no interrupts at all on all the four cores?

Regards,
Yanyan

On Wed, 2019-10-02 at 16:01 +0000, Leonid Meyerovich wrote:
> Hello,
>
> We are running seL4 microkernel on 4 cores Zynq UltraScale+ (zcu102
> board). The implementation includes multiple processes, hypervisor and
> virtual machine running on dedicated core. After several hours running
> (it could be 2 or even 8 hours) the whole microkernel locks up. After
> some investigation I have found that no interrupts generated anymore -
> at least there is no interrupts coming to ISR.
> Inside ISR I have monitored PL2 Physical Timer Control register, which
> feeds a scheduler and didn't find any problems - it stays enabled and
> not masked.
>
> I will appreciate any idea/direction for approaching this problem.
>
> 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.
> ___
> Devel mailing list
> Devel@sel4.systems
> https://sel4.systems/lists/listinfo/devel

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 attachme

Re: [seL4] Zynq UltraScale+ locks up after hours running

2019-10-03 Thread Leonid Meyerovich

Thank you, Chris.
Now I understand. I was confused, because in 
kernel/include/plat/zynqmp/plat/machine.h these interrupts are commented out

Leonid


-Original Message-
From: Chris Guikema 
Sent: Thursday, October 3, 2019 3:44 PM
To: Leonid Meyerovich ; Shen, Yanyan (Data61, Kensington 
NSW) ; devel@sel4.systems
Subject: RE: [seL4] Zynq UltraScale+ locks up after hours running

Hello Leonid,

I'm assuming you're pointing to code from src/arch/arm/kernel/boot.c? If that’s 
the case, then you're right, every interrupt in the system is turned off 
initially. The kernel then turns on some PPIs for timer (and if in hypervisor 
mode, vgic maintenance). If you're running an SMP system, the 
irq_remote_call_ipi and irq_reschedule_ipi (interrupts 0 and 1) are turned back 
on such that cores can communicate with each other. See the links below.

https://github.com/seL4/seL4/blob/8234026c1fb827abee75731b2575ddb741687eff/include/arch/arm/arch/64/mode/machine.h#L4
https://github.com/seL4/seL4/blob/7798b4767dcb7bcd3699f191f685435cfa645518/src/arch/arm/kernel/boot.c#L120

Chris

-Original Message-
From: Devel  On Behalf Of Leonid Meyerovich
Sent: Thursday, October 3, 2019 2:51 PM
To: Shen, Yanyan (Data61, Kensington NSW) ; 
devel@sel4.systems
Subject: Re: [seL4] Zynq UltraScale+ locks up after hours running

CAUTION: This email originated from outside the organization. Do not click 
links or open attachments unless you recognize the sender and know the content 
is safe.

I forgot to mention: my board is zcu102, 4 cores A53

-Original Message-
From: Devel  On Behalf Of Leonid Meyerovich
Sent: Thursday, October 3, 2019 2:40 PM
To: Shen, Yanyan (Data61, Kensington NSW) ; 
devel@sel4.systems
Subject: Re: [seL4] Zynq UltraScale+ locks up after hours running

Hi Everybody,

I am not sure this is related to my previous question/e-mail, but I have 
collected some more data about an interrupts in my system.

I observe a lot of interrupts with ID=0, and later with ID=1 (see below) Both 
IDs 0 and 1 are initialized as inactive in while booting all cores

init_irqs(cap_t root_cnode_cap)
{
irq_t i;

for (i = 0; i <= maxIRQ; i++) {
setIRQState(IRQInactive, i);
}

COULD SOMEBODY EXPLAIN WHAT THESE INTERRUPTS MEANS AND WHY I AM GETTING THEM.

Thank you,
Leonid


I have printed interrupt statistic from inside of handleInterrupt(irq_t irq) 
function.

It has a following structure:

void
handleInterrupt(irq_t irq)
{
switch (intStateIRQTable[irq]) {
case IRQSignal: {
...
}

case IRQTimer:
timerTick();
resetTimer();
if ((++tickCount % 200) == 0)
{
printInt(0);
printf("- - - \n");
printInt(1);
printf("- - - \n");
printInt(2);
printf("- - - \n");
printInt(3);
printf("- - - - - - -  \n");
cleanIntStat();
}
break;

#ifdef ENABLE_SMP_SUPPORT
case IRQIPI:
handleIPI(irq, true);
break;
#endif /* ENABLE_SMP_SUPPORT */

case IRQReserved:
#ifdef CONFIG_IRQ_REPORTING
//printf("Received reserved IRQ: %d", (int)irq); #endif
handleReservedIRQ(irq);
break;

case IRQInactive:
/*
 * This case shouldn't happen anyway unless the hardware or
 * platform code is broken. Hopefully masking it again should make
 * the interrupt go away.
 */
maskInterrupt(true, irq);
#ifdef CONFIG_IRQ_REPORTING
printf("Received disabled IRQ: %d\n", (int)irq); #endif
break;

default:
/* No corresponding haskell error */
fail("Invalid IRQ state");
}

ackInterrupt(irq);
}


printInt function prints all collected interrupts for one core in the following 
format:

---irq stat: cpu=0 (2) 26_50_500_258_258   the number inside 
parentheses is the number of interrupt for particular time interval - 1 sec, 
ignore it
Every interrupt statistic: ID_(enter counter)_(exit_counter)  each counter 
is for 1 sec interval



---irq stat: cpu=0 (2) 26_50_500_258_258
- - -
---irq stat: cpu=1 (2) 26_50_500_258_258
- - -
---irq stat: cpu=2 (2) 26_50_500_258_258
- - -
---irq stat: cpu=3 (3) 26_50_5065_1_159_1_1
- - - - - - -
---irq stat: cpu=0 (2) 26_50_500_257_257
- - -
---irq stat: cpu=1 (2) 26_50_500_280_280
- - -
---irq stat: cpu=2 (2) 26_50_500_280_280

  end of the first excerpt
- - - - - - -
---irq stat: cpu=0 (1) 26_50_50
- - -
---irq stat: cpu=1 (1) 26_50_50
- - -
---irq stat: cpu=2 (1) 26_50_50
- - -
---irq stat: cpu=3 (1) 26_50_50
- - - - - - -
  end of the another excerpt
- - - - - - -
---irq stat: cpu=0 (1) 26_50_51
- - -
---irq stat: cpu=1 (2) 26_50_500_4382_4382
- - -
---irq stat: cpu=2 (2) 26_50_490_4382_4382
- - -
---irq stat: cpu=3 (2) 26_50_500_4382_4382
- - -

Re: [seL4] Zynq UltraScale+ locks up after hours running

2019-10-03 Thread Leonid Meyerovich

I forgot to mention: my board is zcu102, 4 cores A53

-Original Message-
From: Devel  On Behalf Of Leonid Meyerovich
Sent: Thursday, October 3, 2019 2:40 PM
To: Shen, Yanyan (Data61, Kensington NSW) ; 
devel@sel4.systems
Subject: Re: [seL4] Zynq UltraScale+ locks up after hours running

Hi Everybody,

I am not sure this is related to my previous question/e-mail, but I have 
collected some more data about an interrupts in my system.

I observe a lot of interrupts with ID=0, and later with ID=1 (see below) Both 
IDs 0 and 1 are initialized as inactive in while booting all cores

init_irqs(cap_t root_cnode_cap)
{
irq_t i;

for (i = 0; i <= maxIRQ; i++) {
setIRQState(IRQInactive, i);
}

COULD SOMEBODY EXPLAIN WHAT THESE INTERRUPTS MEANS AND WHY I AM GETTING THEM.

Thank you,
Leonid


I have printed interrupt statistic from inside of handleInterrupt(irq_t irq) 
function.

It has a following structure:

void
handleInterrupt(irq_t irq)
{
switch (intStateIRQTable[irq]) {
case IRQSignal: {
...
}

case IRQTimer:
timerTick();
resetTimer();
if ((++tickCount % 200) == 0)
{
printInt(0);
printf("- - - \n");
printInt(1);
printf("- - - \n");
printInt(2);
printf("- - - \n");
printInt(3);
printf("- - - - - - -  \n");
cleanIntStat();
}
break;

#ifdef ENABLE_SMP_SUPPORT
case IRQIPI:
handleIPI(irq, true);
break;
#endif /* ENABLE_SMP_SUPPORT */

case IRQReserved:
#ifdef CONFIG_IRQ_REPORTING
//printf("Received reserved IRQ: %d", (int)irq); #endif
handleReservedIRQ(irq);
break;

case IRQInactive:
/*
 * This case shouldn't happen anyway unless the hardware or
 * platform code is broken. Hopefully masking it again should make
 * the interrupt go away.
 */
maskInterrupt(true, irq);
#ifdef CONFIG_IRQ_REPORTING
printf("Received disabled IRQ: %d\n", (int)irq); #endif
break;

default:
/* No corresponding haskell error */
fail("Invalid IRQ state");
}

ackInterrupt(irq);
}


printInt function prints all collected interrupts for one core in the following 
format:

---irq stat: cpu=0 (2) 26_50_500_258_258   the number inside 
parentheses is the number of interrupt for particular time interval - 1 sec, 
ignore it
Every interrupt statistic: ID_(enter counter)_(exit_counter)  each counter 
is for 1 sec interval



---irq stat: cpu=0 (2) 26_50_500_258_258
- - -
---irq stat: cpu=1 (2) 26_50_500_258_258
- - -
---irq stat: cpu=2 (2) 26_50_500_258_258
- - -
---irq stat: cpu=3 (3) 26_50_5065_1_159_1_1
- - - - - - -
---irq stat: cpu=0 (2) 26_50_500_257_257
- - -
---irq stat: cpu=1 (2) 26_50_500_280_280
- - -
---irq stat: cpu=2 (2) 26_50_500_280_280

  end of the first excerpt
- - - - - - -
---irq stat: cpu=0 (1) 26_50_50
- - -
---irq stat: cpu=1 (1) 26_50_50
- - -
---irq stat: cpu=2 (1) 26_50_50
- - -
---irq stat: cpu=3 (1) 26_50_50
- - - - - - -
  end of the another excerpt
- - - - - - -
---irq stat: cpu=0 (1) 26_50_51
- - -
---irq stat: cpu=1 (2) 26_50_500_4382_4382
- - -
---irq stat: cpu=2 (2) 26_50_490_4382_4382
- - -
---irq stat: cpu=3 (2) 26_50_500_4382_4382
- - - - - - -
  end of the another excerpt

- - - - - - -
---irq stat: cpu=0 (2) 26_50_511_317_317
- - -
---irq stat: cpu=1 (4) 26_50_5025_34_341_132_13227_16_16
- - -
---irq stat: cpu=2 (4) 26_50_5027_17_1725_32_321_130_130
- - -
---irq stat: cpu=3 (2) 26_50_491_28_28
- - - - - - -
  end of the another excerpt

-Original Message-
From: Shen, Yanyan (Data61, Kensington NSW) 
Sent: Thursday, October 3, 2019 2:44 AM
To: Leonid Meyerovich ; devel@sel4.systems
Subject: Re: [seL4] Zynq UltraScale+ locks up after hours running

Hi Leonid,

Could you provide a bit more about your software configuration? For instance, 
do you have multiple VMs running on dedicated hardware cores?
How are the VM and processes configured?

Also, you mean there were no interrupts at all on all the four cores?


Regards,
Yanyan

On Wed, 2019-10-02 at 16:01 +, Leonid Meyerovich wrote:
> Hello,
>
> We are running seL4 microkernel on 4 cores Zynq UltraScale+ (zcu102
> board). The implementation includes multiple processes, hypervisor and
> virtual machine running on dedicated core. After several hours running
> (it could be 2 or even 8 hours) the whole microkernel locks up. After
> some investigation I have found that no interrupts generated anymore -
> at least there is no interrupts coming to ISR.
> Inside ISR I have monitored PL2 Physical Timer Control register, which
> fe

Re: [seL4] Zynq UltraScale+ locks up after hours running

2019-10-03 Thread Leonid Meyerovich

Hi Everybody,

I am not sure this is related to my previous question/e-mail, but I have 
collected some more data about an interrupts in my system.

I observe a lot of interrupts with ID=0, and later with ID=1 (see below)
Both IDs 0 and 1 are initialized as inactive in while booting all cores

init_irqs(cap_t root_cnode_cap)
{
irq_t i;

for (i = 0; i <= maxIRQ; i++) {
setIRQState(IRQInactive, i);
}

COULD SOMEBODY EXPLAIN WHAT THESE INTERRUPTS MEANS AND WHY I AM GETTING THEM.

Thank you,
Leonid


I have printed interrupt statistic from inside of handleInterrupt(irq_t irq) 
function.

It has a following structure:

void
handleInterrupt(irq_t irq)
{
switch (intStateIRQTable[irq]) {
case IRQSignal: {
...
}

case IRQTimer:
timerTick();
resetTimer();
if ((++tickCount % 200) == 0)
{
printInt(0);
printf("- - - \n");
printInt(1);
printf("- - - \n");
printInt(2);
printf("- - - \n");
printInt(3);
printf("- - - - - - -  \n");
cleanIntStat();
}
break;

#ifdef ENABLE_SMP_SUPPORT
case IRQIPI:
handleIPI(irq, true);
break;
#endif /* ENABLE_SMP_SUPPORT */

case IRQReserved:
#ifdef CONFIG_IRQ_REPORTING
//printf("Received reserved IRQ: %d", (int)irq);
#endif
handleReservedIRQ(irq);
break;

case IRQInactive:
/*
 * This case shouldn't happen anyway unless the hardware or
 * platform code is broken. Hopefully masking it again should make
 * the interrupt go away.
 */
maskInterrupt(true, irq);
#ifdef CONFIG_IRQ_REPORTING
printf("Received disabled IRQ: %d\n", (int)irq);
#endif
break;

default:
/* No corresponding haskell error */
fail("Invalid IRQ state");
}

ackInterrupt(irq);
}


printInt function prints all collected interrupts for one core in the following 
format:

---irq stat: cpu=0 (2) 26_50_500_258_258   the number inside 
parentheses is the number of interrupt for particular time interval - 1 sec, 
ignore it
Every interrupt statistic: ID_(enter counter)_(exit_counter)  each counter 
is for 1 sec interval



---irq stat: cpu=0 (2) 26_50_500_258_258
- - -
---irq stat: cpu=1 (2) 26_50_500_258_258
- - -
---irq stat: cpu=2 (2) 26_50_500_258_258
- - -
---irq stat: cpu=3 (3) 26_50_5065_1_159_1_1
- - - - - - -
---irq stat: cpu=0 (2) 26_50_500_257_257
- - -
---irq stat: cpu=1 (2) 26_50_500_280_280
- - -
---irq stat: cpu=2 (2) 26_50_500_280_280

  end of the first excerpt
- - - - - - -
---irq stat: cpu=0 (1) 26_50_50
- - -
---irq stat: cpu=1 (1) 26_50_50
- - -
---irq stat: cpu=2 (1) 26_50_50
- - -
---irq stat: cpu=3 (1) 26_50_50
- - - - - - -
  end of the another excerpt
- - - - - - -
---irq stat: cpu=0 (1) 26_50_51
- - -
---irq stat: cpu=1 (2) 26_50_500_4382_4382
- - -
---irq stat: cpu=2 (2) 26_50_490_4382_4382
- - -
---irq stat: cpu=3 (2) 26_50_500_4382_4382
- - - - - - -
  end of the another excerpt

- - - - - - -
---irq stat: cpu=0 (2) 26_50_511_317_317
- - -
---irq stat: cpu=1 (4) 26_50_5025_34_341_132_13227_16_16
- - -
---irq stat: cpu=2 (4) 26_50_5027_17_1725_32_321_130_130
- - -
---irq stat: cpu=3 (2) 26_50_491_28_28
- - - - - - -
  end of the another excerpt

-Original Message-
From: Shen, Yanyan (Data61, Kensington NSW) 
Sent: Thursday, October 3, 2019 2:44 AM
To: Leonid Meyerovich ; devel@sel4.systems
Subject: Re: [seL4] Zynq UltraScale+ locks up after hours running

Hi Leonid,

Could you provide a bit more about your software configuration? For instance, 
do you have multiple VMs running on dedicated hardware cores?
How are the VM and processes configured?

Also, you mean there were no interrupts at all on all the four cores?


Regards,
Yanyan

On Wed, 2019-10-02 at 16:01 +, Leonid Meyerovich wrote:
> Hello,
>
> We are running seL4 microkernel on 4 cores Zynq UltraScale+ (zcu102
> board). The implementation includes multiple processes, hypervisor and
> virtual machine running on dedicated core. After several hours running
> (it could be 2 or even 8 hours) the whole microkernel locks up. After
> some investigation I have found that no interrupts generated anymore -
> at least there is no interrupts coming to ISR.
> Inside ISR I have monitored PL2 Physical Timer Control register, which
> feeds a scheduler and didn't find any problems - it stays enabled and
> not masked.
>
> I will appreciate any idea/direction for approaching this problem.
>
> Thank you,
>
> Leonid
>
>
>
>
> This message and all attachments are PRIVATE, and contain infor

Re: [seL4] Zynq UltraScale+ locks up after hours running

2019-10-03 Thread Leonid Meyerovich

Hi Yanyan,

I am running initial task and hypervisor on core 0.
Hypervisor creates 2 VM and running them on core 1 and 2
Core 3 runs 7 processes that communicate through notification objects and 
shared memory (in pairs)
On process on core 3 implements UART based connection (, this is PL uart, Rx 
use  interrupt). On of core 3 process also runs SADA driver (also uses 
interrupt)

VMs communicate to the rest of the system through 'virtual channels' - 
exceptions and shared memory.

All hardware interrupts are processed by core 0 (please, correct me if I am 
wrong). But as far as I understand PL2 physical timer interrupt runs on every 
core.

Every processes prints some messages on terminal. I have never seen that these 
messages have been printed partially what the system lock up, process completes 
printing the message and has never scheduled again.
I have also printed some messages from inside of ISR after getting time 
interrupt (print interrupt counter once a second) and I don't see these 
messages when the system locks up.

Thank you,
Leonid

-Original Message-
From: Shen, Yanyan (Data61, Kensington NSW) 
Sent: Thursday, October 3, 2019 2:44 AM
To: Leonid Meyerovich ; devel@sel4.systems
Subject: Re: [seL4] Zynq UltraScale+ locks up after hours running

Hi Leonid,

Could you provide a bit more about your software configuration? For instance, 
do you have multiple VMs running on dedicated hardware cores?
How are the VM and processes configured?

Also, you mean there were no interrupts at all on all the four cores?

Regards,
Yanyan

On Wed, 2019-10-02 at 16:01 +, Leonid Meyerovich wrote:
> Hello,
>
> We are running seL4 microkernel on 4 cores Zynq UltraScale+ (zcu102
> board). The implementation includes multiple processes, hypervisor and
> virtual machine running on dedicated core. After several hours running
> (it could be 2 or even 8 hours) the whole microkernel locks up. After
> some investigation I have found that no interrupts generated anymore -
> at least there is no interrupts coming to ISR.
> Inside ISR I have monitored PL2 Physical Timer Control register, which
> feeds a scheduler and didn't find any problems - it stays enabled and
> not masked.
>
> I will appreciate any idea/direction for approaching this problem.
>
> 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.
> ___
> Devel mailing list
> Devel@sel4.systems
> https://sel4.systems/lists/listinfo/devel

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.
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

[seL4] Zynq UltraScale+ locks up after hours running

2019-10-02 Thread Leonid Meyerovich

Hello,

We are running seL4 microkernel on 4 cores Zynq UltraScale+ (zcu102 board). The 
implementation includes multiple processes, hypervisor and virtual machine 
running on dedicated core. After several hours running (it could be 2 or even 8 
hours) the whole microkernel locks up. After some investigation I have found 
that no interrupts generated anymore - at least there is no interrupts coming 
to ISR. Inside ISR I have monitored PL2 Physical Timer Control register, which 
feeds a scheduler and didn't find any problems - it stays enabled and not 
masked.

I will appreciate any idea/direction for approaching this problem.

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.
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

[seL4] xilinx ultrascale+: Spurious interrupt

2019-06-04 Thread Leonid Meyerovich

Hello Everybody,

Petalinux is running on VM on the one of the core of Xilinx Ultrascale+ (A53)

>From time to time I see Spurious Interrupt message from seL4 kernel 
>(handleInterruptEntry)


<>
<>
<>

Could somebody explain why it may happen? How to debug it?

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.
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] seL4 process memory utilization

2019-04-25 Thread Leonid Meyerovich

Thank you, I’ll look into it.

From: Matthew Fernandez 
Sent: Thursday, April 25, 2019 11:15 AM
To: Leonid Meyerovich 
Cc: Heiser, Gernot (Data61, Kensington NSW) ; 
devel@sel4.systems
Subject: Re: [seL4] seL4 process memory utilization

On 24 Apr 2019, at 07:20, Leonid Meyerovich 
mailto:lmeyerov...@i-a-i.com>> wrote:
Yes, I, probably, was not specific enough. My question was not about kernel 
memory.
I'd like to have something to support memory leak investigation, for the memory 
which is allocated by malloc (libmuslc library).
BTW, how libmuslc get memory for memory management?

Thank you,
Leonid

This isn’t quite what you want, but if it’s still functional there’s a 
rudimentary heap debugger I wrote a while back. You might be able to bend it to 
your purpose.  
https://github.com/seL4/seL4_libs/blob/master/libsel4debug/src/alloc.c

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.
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] seL4 process memory utilization

2019-04-24 Thread Leonid Meyerovich

Yes, I, probably, was not specific enough. My question was not about kernel 
memory.
I'd like to have something to support memory leak investigation, for the memory 
which is allocated by malloc (libmuslc library).
BTW, how libmuslc get memory for memory management?

Thank you,
Leonid

-Original Message-
From: Devel  On Behalf Of Heiser, Gernot (Data61, 
Kensington NSW)
Sent: Wednesday, April 24, 2019 2:18 AM
To: devel@sel4.systems
Subject: Re: [seL4] seL4 process memory utilization

Banden’s answer is correct, tl;dr you cannot check the available space in the 
kernel heap as there is no kernel heap.

However, Leonid's initial question was somewhat ambiguous. The various seL4 
userland frameworks inevitably provide their own (usually pretty 
unsophisticated) memory managers, which maybe global (in which case you lose 
most of the kernel-enforced isolation) or per-process. If you’re using one of 
those then they may or may not provide a method for checking the amount of 
remaining free memory (and if they don’t it would probably be pretty easy to 
add).

Leonid, you may want to clarify what you meant.

Gernot

> On 24 Apr 2019, at 04:33, G. Branden Robinson  
> wrote:
>
> Signed PGP part
> At 2019-04-17T12:21:41+, Leonid Meyerovich wrote:
>> Is there any way in seL4 (library function?) to check free heap memory?
>
> My understanding is that there is not, because the seL4 microkernel
> does not implement a memory manager.  A malloc()-style memory manager
> is not considered an essential service for a microkernel, so seL4
> leaves the provision of such a service up to the implementation.
>
> The seL4 FAQ says the following:
>
> "How can usermode manage kernel memory safely?
>
> The kernel puts userland in control of system resources by handing all
> free memory (called ‘‘Untyped’’) after booting to the first user
> process (called the ‘‘root task’’) by depositing the respective caps
> in the root tasks’s Cspace. The root task can then implement its
> resource management policies, e.g. by partitioning the system into
> security domains and handing each domain a disjoint subset of Untyped memory.
>
> If a system call requires memory for the kernel’s metadata, such as
> the thread control block when creating a thread, userland must provide
> this memory explicitly to the kernel. This is done by ‘‘retyping’’
> some Untyped memory into the corresponding kernel object type. Eg. for
> thread creation, userland must retype some Untyped into ‘‘TCB
> Objects’’. This memory then becomes kernel memory, in the sense that
> only the kernel can read or write it. Userland can still revoke it,
> which implicitly destroys the objects (eg threads) represented by the object.
>
> The only objects directly accessible by userland are ‘‘Frame Objects’’:
> These can be mapped into an ‘‘Address Space Object’’ (essentially a
> page table), after which userland can write to the physical memory
> represented by the Frame Objects."
>
> https://docs.sel4.systems/FrequentlyAskedQuestions.html
>
> A "memory server" that hands out chunks of "heap memory" to threads
> requesting it would likely be a part of any even vaguely Unix-like
> kernel running on top of seL4.  Even better, the memory server you
> implement (or otherwise obtain) can implement a policy that avoids
> over-commitment of memory, which is a notorious source of reliability
> problems on Linux and other Unix kernels.  If you search LWN.net for
> the term "OOM killer" [out-of-memory process killer], you will find
> articles documenting Linux's struggle with the consequences of memory
> over-commitment going back at least 15 years.  It is an active
> struggle today; see, for example, https://lwn.net/Articles/761118/ .
>
> A quick glance suggests to me that there isn't a ready-made heap-like
> memory server available as a CAmkES component[1], but if I'm mistaken
> I urge someone to speak up and correct me.
>
> Regards,
> Branden
>
> [1] https://github.com/seL4/camkes/tree/master/apps
>
>

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.
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

[seL4] seL4 process memory utilization

2019-04-18 Thread Leonid Meyerovich

Hello,

Is there any way in seL4 (library function?) to check free heap memory?

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.
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] Network lwip for imx6

2018-12-10 Thread Leonid Meyerovich

Hi Chris,

I have downloaded http-server example for imx6 (I am working on zynqmp), just 
to use it as a reference to see how  did you implement a synchronization  
functions, but I didn’t find these function to be implemented. Is this example 
not complete?
Thanks you,
Leonid

From: Devel  On Behalf Of Chris Guikema
Sent: Thursday, August 9, 2018 2:06 PM
To: Fabrizio Bertocci ; xuguo.w...@gmail.com
Cc: devel@sel4.systems
Subject: Re: [seL4] Network lwip for imx6

Xuguo,

To add on, DornerWorks has also created an example http-server application that 
uses lwIP and the Ethernet drivers to host an http-server on an imx6.

It’s on an older version of seL4 (7.0.0), but you can download it and try it 
out for yourself.

$ repo init -u https://github.com/dornerworks/dw-camkes-manifests -m 
http_server.xml
$ repo sync

You’ll need to go to the FileSystem component directory and run the makefs 
python script.

$ python apps/camkes_http/components/FileSystem/makefs.py
$ make http_server_defconfig
$ make

There is a readme document in the camkes_http application that overviews 
exactly how the system is setup, and how the Ethdriver and Router components 
work.

In order to make an echo server, you would just need to create an interface to 
echo the messages back and forth.

Let me know if you have any other questions,

Chris Guikema
DornerWorks Ltd

From: Devel [mailto:devel-bounces@sel4.systems] On Behalf Of Fabrizio Bertocci
Sent: Wednesday, August 8, 2018 9:30 PM
To: xuguo.w...@gmail.com
Cc: devel@sel4.systems
Subject: Re: [seL4] Network lwip for imx6

CAUTION: This email originated from outside the organization. Do no click links 
or open attachments unless you recognize the sender and know the content is 
safe.
Xuguo,
lwip on IMX6 is already available on seL4 (I have been using it in my project).
Look at the seL4/util_libs repository. There you can find the ethernet driver 
and the lwip.
Make sure to use the latest version (from master) that contains important fixes 
to the driver.

Regards,
Fabrizio

On Wed, Aug 8, 2018 at 9:19 PM wong xuguo 
mailto:xuguo.w...@gmail.com>> wrote:
Hi,
I am a student fron Nanjing university, a fresh man of microkernel, 
specially,
know very little about the seL4.
Recently I accept a chellange about porting the lwip to sel4, on arch of 
imx6,
does any one could give me a clue?
I found the source of camkes does have this code, could I do something to 
port,
to make the lwip work? What my aim is make a tcp echo server.
Thank you for all of you help.

Best regards
from Xuguo Wang
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel




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.
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

[seL4] building sel4test for zynqmp platform

2018-08-25 Thread Leonid Meyerovich

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/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.
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] create process in seL4

2018-08-16 Thread Leonid Meyerovich

Hi Anna,

I’d like to create process with particular size of CSpace and VSpace.
CSpace size is defined in ‘config’ structure, I can set 
config.one_level_cspace_size_bits member.

I am not sure how to set up VSpace size through ‘reservations’ and 
‘num_reservations’ values? Let’s say I need to give to new process 10Mb virtual 
space.

static inline sel4utils_process_config_t
process_config_create_vspace(sel4utils_process_config_t config, 
sel4utils_elf_region_t *reservations,  int num_reservations)
{
config.create_vspace = true;
config.reservations = reservations;
config.num_reservations = num_reservations;
return config;
}

Thank you,
Leonid

From: anna.ly...@data61.csiro.au 
Sent: Wednesday, August 15, 2018 8:37 PM
To: Leonid Meyerovich ; devel@sel4.systems
Subject: Re: create process in seL4


Hi Leonid,



I don't understand your first question, which untyped are you wanting to adjust 
the size of?



As for the second question, you can take a look at the sel4bench project, where 
all created processes use the same function to get a working allocator through 
the libsel4benchsupport library bundled with the project [1].



We're aware we need more tutorials and I'll add this to the list of desired 
seL4 tutorials.



Thanks

Anna.



[1] 
https://github.com/seL4/sel4bench/blob/master/libsel4benchsupport/src/support.c#L390


From: Devel mailto:devel-bounces@sel4.systems>> on 
behalf of Leonid Meyerovich 
mailto:lmeyerov...@i-a-i.com>>
Sent: Thursday, 16 August 2018 6:43 AM
To: devel@sel4.systems<mailto:devel@sel4.systems>
Subject: [seL4] create process in seL4

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 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.




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.
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

[seL4] create process in seL4

2018-08-15 Thread Leonid Meyerovich

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 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.
___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Re: [seL4] sel4 thread creation problem

2018-08-09 Thread Leonid Meyerovich

Hi Anna,
Thank you for your prompt response.

I have tried to set a guard value as you have suggested but still there is no 
success.
I have got a guard value = 43
initSleep@time.c:146 seL4_WordBits=64,  cnode_size_bits=21  guard=43

I am not sure what I am doing wrong.
Thank you,
Leonid

Result (and crash)

initSleep@time.c:146 seL4_WordBits=64,  cnode_size_bits=21  guard=43

setup_irq@timer.c:81 Setting up IRQ 8000
<>
Caught cap fault in send phase at address 0x0
while trying to handle:
cap fault in send phase at address 0x2e7ffe0
in thread 0xff800200 "child of: 'rootserver'" at address 0x4216dc
With stack:



My new thread creation:
void initSleep(env_t penv) //seL4_BootInfo *info)
{
_penv = penv;

vka_object_t tcb_object = {0};
int error = vka_alloc_tcb(>vka, _object);

seL4_CPtr cspace_cap;
cspace_cap = simple_get_cnode(>simple);
seL4_CPtr pd_cap;
pd_cap = simple_get_pd(>simple);
seL4_CPtr ipc_page;
seL4_Word ipc_buffer = 
(seL4_Word)vspace_new_ipc_buffer(>vspace, _page);

vka_object_t ep_object = {0};
   error = vka_alloc_endpoint(>vka, _object);
assert(error == 0);
//error = seL4_TCB_Configure(tcb_object.cptr, ep_object.cptr, 
cspace_cap, seL4_NilData, pd_cap, seL4_NilData, ipc_buffer, ipc_page);

int cnode_size_bits = simple_get_cnode_size_bits(>simple);
seL4_Word guard = seL4_CNode_CapData_new(0,  seL4_WordBits - 
simple_get_cnode_size_bits(>simple)).words[0];
ZF_LOGD("seL4_WordBits=%lu,  cnode_size_bits=%lu  guard=%lu\n", 
seL4_WordBits, cnode_size_bits, guard);
error = seL4_TCB_Configure(tcb_object.cptr, seL4_NilData, 
cspace_cap, guard, pd_cap, seL4_NilData, ipc_buffer, ipc_page);
error = seL4_TCB_SetPriority(tcb_object.cptr, 
simple_get_tcb(>simple), seL4_MaxPrio);

seL4_UserContext regs = {
.pc = (seL4_Word)time_thread,
.sp = 
(seL4_Word)thread_time_stack
};
error = seL4_TCB_WriteRegisters(tcb_object.cptr, 0, 0, 2, 
);

for (int i=0; ihandler_path.capPtr, 
irq->badged_ntfn_path.capPtr);
  4216bc:   f85c8340ldurx0, [x26,#-56]
arm_sys_send_recv():
/home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:165
register seL4_Word msg1 asm("x3") = *in_out_mr1;
  4216c0:   d283mov x3, #0x0// #0
seL4_SetCap():
/home/lm/sel4vm/stage/arm/zynqmp/include/sel4/arch/functions.h:59
  4216c4:   f901e8c1str x1, [x6,#976]
arm_sys_send_recv():
/home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:166
register seL4_Word msg2 asm("x4") = *in_out_mr2;
  4216c8:   d284mov x4, #0x0// #0
/home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:167
register seL4_Word msg3 asm("x5") = *in_out_mr3;
  4216cc:   d285mov x5, #0x0// #0
/home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:170
register seL4_Word scno asm("x7") = sys;
  4216d0:   9287mov x7, #0x // #-1
/home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:161
register seL4_Word info asm("x1") = info_arg;
  4216d4:   d2941001mov x1, #0xa080 // 
#41088
  4216d8:   f2a00021movkx1, #0x1, lsl #16
/home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:171
asm volatile (
  4216dc:   d402hvc #0x0
seL4_MessageInfo_get_label():



From: anna.ly...@data61.csiro.au 
Sent: Tuesday, August 7, 2018 7:39 PM
To: Leonid Meyerovich ; devel@sel4.systems
Subject: Re: sel4 thread creation problem


Hi Leonid,



It looks like you haven't set the cspace guard correctly in the new tcb, which 
means that cptr look ups will fail.



This should fix it:



- error = seL4_TCB_Configure(tcb_object.cptr, , seL4_NilData, cspace_cap, 
seL4_NilData, pd_cap, seL4_NilData, ipc_buffer, ipc_page);

+ seL4_Word guard = seL4_CNode_CapData_new(0,  seL4_WordBits - 
simple_get_cnode_size_bits(>simple).words[0]);

+ error = seL4_TCB_Configure(tcb_object.cptr, , seL4_NilData, cspace_cap, 
guard, pd_cap, seL4_NilData, ipc_buffer, ipc_page);



Cheers,

Anna.



____
From: Devel mailto:devel-bounces@sel4.systems>> on 
behalf of Leonid Meyerovich 
mailto:lmeyerov...@i-a-i.com>>
Sent: Wednesday, 8 August 2018 1:47 AM
To: devel@sel4.systems<mailto:devel@sel4.systems>
Subject: [seL4] sel4 thread creation problem

Hello,

My platform is ARM (zynqmp), seL4 v8. I have created a timer in simple initial 
thread:

int err;
seL4_timer_t tim

Re: [seL4] sel4 thread creation problem

2018-08-08 Thread Leonid Meyerovich

Hi Anna,

I have found the problem - SP for a newly created thread was wrong.

Thanks you,
Leonid

From: anna.ly...@data61.csiro.au 
Sent: Tuesday, August 7, 2018 7:39 PM
To: Leonid Meyerovich ; devel@sel4.systems
Subject: Re: sel4 thread creation problem


Hi Leonid,



It looks like you haven't set the cspace guard correctly in the new tcb, which 
means that cptr look ups will fail.



This should fix it:



- error = seL4_TCB_Configure(tcb_object.cptr, , seL4_NilData, cspace_cap, 
seL4_NilData, pd_cap, seL4_NilData, ipc_buffer, ipc_page);

+ seL4_Word guard = seL4_CNode_CapData_new(0,  seL4_WordBits - 
simple_get_cnode_size_bits(>simple).words[0]);

+ error = seL4_TCB_Configure(tcb_object.cptr, , seL4_NilData, cspace_cap, 
guard, pd_cap, seL4_NilData, ipc_buffer, ipc_page);



Cheers,

Anna.




From: Devel mailto:devel-bounces@sel4.systems>> on 
behalf of Leonid Meyerovich 
mailto:lmeyerov...@i-a-i.com>>
Sent: Wednesday, 8 August 2018 1:47 AM
To: devel@sel4.systems<mailto:devel@sel4.systems>
Subject: [seL4] sel4 thread creation problem

Hello,

My platform is ARM (zynqmp), seL4 v8. I have created a timer in simple initial 
thread:

int err;
seL4_timer_t timer;
vka_object_t ntfn_object;
ntfn_object.cptr = 0;
err = vka_alloc_notification(&_env.vka, _object);
assert(err == 0);

err = sel4platsupport_init_default_timer(&_env.vka, &_env.vspace, 
&_env.simple, ntfn_object.cptr, );
err = ltimer_set_timeout(, NS_IN_MS * 20, 
TIMEOUT_PERIODIC);
assert(err == 0);

int count = 0;
int count_s = 0;
while (1) {
/* Handle the timer interrupt */
seL4_Word badge;
seL4_Wait(ntfn_object.cptr, );
printf("time_thread: badge=%lx\n", badge);
sel4platsupport_handle_timer_irq(, badge);
count++;
if ((count / 50) * 50 == count)
{
   count_s++;
   printf("-timer=%d  %d\n", count, count_s);
}
}

It works fine (I am not sure why TIMESTAMP timer interrupt coming every ~40 
sec, but it's not an issue right now)

Now I am trying to move all this timer code into a new thread, which I have 
created in the same vspace

// create thread
void initSleep(env_t penv) //seL4_BootInfo *info)
{
_penv = penv;

vka_object_t tcb_object = {0};
int error = vka_alloc_tcb(>vka, _object);

seL4_CPtr cspace_cap;
cspace_cap = simple_get_cnode(>simple);
seL4_CPtr pd_cap;
pd_cap = simple_get_pd(>simple);
seL4_CPtr ipc_page;
seL4_Word ipc_buffer = 
(seL4_Word)vspace_new_ipc_buffer(>vspace, _page);
error = seL4_TCB_Configure(tcb_object.cptr, , seL4_NilData, 
cspace_cap, seL4_NilData, pd_cap, seL4_NilData, ipc_buffer, ipc_page);
error = seL4_TCB_SetPriority(tcb_object.cptr, 
simple_get_tcb(>simple), seL4_MaxPrio);
seL4_UserContext regs = {
.pc = (seL4_Word)time_thread,
.sp = 
(seL4_Word)thread_time_stack
};
error = seL4_TCB_WriteRegisters(tcb_object.cptr, 0, 0, 2, 
);
error = seL4_TCB_Resume(tcb_object.cptr);
}

And this is thread function

static void time_thread(void)
{
_tick_number = 0;
int count_s = 0;
init_timer();
while (1)
{
/* Handle the timer interrupt */
seL4_Word badge;
seL4_Wait(timer_ntfn_object.cptr, );
printf("time_thread: badge=%lx\n", badge);
sel4platsupport_handle_timer_irq(, badge);
_tick_number++;
if ((_tick_number / 50) * 50 == _tick_number)
{
   count_s++;
   printf("-timer=%lu  %d\n", _tick_number, 
count_s);
}
}

The system crashed:
setup_irq@timer.c:81<mailto:setup_irq@timer.c:81> Setting up IRQ 
8000
<>

Here is dump:


/home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/functions.h:23
  421938:   d53bd066mrs x6, tpidrro_el0
setup_irq():
/home/lm/sel4vm/libs/libsel4platsupport/src/timer.c:85
error =  seL4_IRQHandler_SetNotification(irq->handler_path.capPtr, 
irq->badged_ntfn_path.capPtr);
  42193c:   f85c8340ldurx0, [x26,#-56]
arm_sys_send_recv():
/home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:165
register seL4_Word msg1 asm("x3") = *in_out_mr1;
  421940:   d283mov x3, #0x0// #0
seL4_SetCap():
/home/lm/sel4vm/stage/arm/zynqmp/include/sel4/arch/functions.h:59
  421944:   f901e8c1str x1, [x6,#976]
arm_sys_send_recv():
/home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_a

[seL4] sel4 thread creation problem

2018-08-07 Thread Leonid Meyerovich

Hello,

My platform is ARM (zynqmp), seL4 v8. I have created a timer in simple initial 
thread:

int err;
seL4_timer_t timer;
vka_object_t ntfn_object;
ntfn_object.cptr = 0;
err = vka_alloc_notification(&_env.vka, _object);
assert(err == 0);

err = sel4platsupport_init_default_timer(&_env.vka, &_env.vspace, 
&_env.simple, ntfn_object.cptr, );
err = ltimer_set_timeout(, NS_IN_MS * 20, 
TIMEOUT_PERIODIC);
assert(err == 0);

int count = 0;
int count_s = 0;
while (1) {
/* Handle the timer interrupt */
seL4_Word badge;
seL4_Wait(ntfn_object.cptr, );
printf("time_thread: badge=%lx\n", badge);
sel4platsupport_handle_timer_irq(, badge);
count++;
if ((count / 50) * 50 == count)
{
   count_s++;
   printf("-timer=%d  %d\n", count, count_s);
}
}

It works fine (I am not sure why TIMESTAMP timer interrupt coming every ~40 
sec, but it's not an issue right now)

Now I am trying to move all this timer code into a new thread, which I have 
created in the same vspace

// create thread
void initSleep(env_t penv) //seL4_BootInfo *info)
{
_penv = penv;

vka_object_t tcb_object = {0};
int error = vka_alloc_tcb(>vka, _object);

seL4_CPtr cspace_cap;
cspace_cap = simple_get_cnode(>simple);
seL4_CPtr pd_cap;
pd_cap = simple_get_pd(>simple);
seL4_CPtr ipc_page;
seL4_Word ipc_buffer = 
(seL4_Word)vspace_new_ipc_buffer(>vspace, _page);
error = seL4_TCB_Configure(tcb_object.cptr, , seL4_NilData, 
cspace_cap, seL4_NilData, pd_cap, seL4_NilData, ipc_buffer, ipc_page);
error = seL4_TCB_SetPriority(tcb_object.cptr, 
simple_get_tcb(>simple), seL4_MaxPrio);
seL4_UserContext regs = {
.pc = (seL4_Word)time_thread,
.sp = 
(seL4_Word)thread_time_stack
};
error = seL4_TCB_WriteRegisters(tcb_object.cptr, 0, 0, 2, 
);
error = seL4_TCB_Resume(tcb_object.cptr);
}

And this is thread function

static void time_thread(void)
{
_tick_number = 0;
int count_s = 0;
init_timer();
while (1)
{
/* Handle the timer interrupt */
seL4_Word badge;
seL4_Wait(timer_ntfn_object.cptr, );
printf("time_thread: badge=%lx\n", badge);
sel4platsupport_handle_timer_irq(, badge);
_tick_number++;
if ((_tick_number / 50) * 50 == _tick_number)
{
   count_s++;
   printf("-timer=%lu  %d\n", _tick_number, 
count_s);
}
}

The system crashed:
setup_irq@timer.c:81 Setting up IRQ 8000
<>

Here is dump:


/home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/functions.h:23
  421938:   d53bd066mrs x6, tpidrro_el0
setup_irq():
/home/lm/sel4vm/libs/libsel4platsupport/src/timer.c:85
error =  seL4_IRQHandler_SetNotification(irq->handler_path.capPtr, 
irq->badged_ntfn_path.capPtr);
  42193c:   f85c8340ldurx0, [x26,#-56]
arm_sys_send_recv():
/home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:165
register seL4_Word msg1 asm("x3") = *in_out_mr1;
  421940:   d283mov x3, #0x0// #0
seL4_SetCap():
/home/lm/sel4vm/stage/arm/zynqmp/include/sel4/arch/functions.h:59
  421944:   f901e8c1str x1, [x6,#976]
arm_sys_send_recv():
/home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:166
register seL4_Word msg2 asm("x4") = *in_out_mr2;
  421948:   d284mov x4, #0x0// #0
/home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:167
register seL4_Word msg3 asm("x5") = *in_out_mr3;
  42194c:   d285mov x5, #0x0// #0
/home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:170
register seL4_Word scno asm("x7") = sys;
  421950:   9287mov x7, #0x // #-1
/home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:161
register seL4_Word info asm("x1") = info_arg;
  421954:   d2941001mov x1, #0xa080 // 
#41088
  421958:   f2a00021movkx1, #0x1, lsl #16
/home/lm/sel4vm/stage/arm/zynqmp/include/sel4/sel4_arch/syscalls.h:171
asm volatile (
  42195c:   d402hvc #0x0
seL4_MessageInfo_get_label():
/home/lm/sel4vm/stage/arm/zynqmp/include/sel4/shared_types_gen.h:49

I suspect that  my thread initialization is not right, can somebody see any 
problem?
Thank you,
Leonid





This message and all attachments are PRIVATE, and contain

[seL4] using libmuslc library question

2018-08-03 Thread Leonid Meyerovich

Hello,

I have tried to call usleep() function from seL4 'main' thread and it crashes 
the system with error:

Caught cap fault in send phase at address 0x0
while trying to handle:
vm fault on code at address 0x200 with status 0x8206
in thread 0xff807bfe2200 "rootserver" at address 0x200
With stack:

How to use this library?
Thank you,
Leonid

___
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

41 matches

Mail list logo