Hi Vasily,

I've put replies inline

On Mon 26-Dec-2016 9:37 AM, Vasily A. Sartakov wrote:
Greetings. 

I have merged MIPS port with 4.0.0 release. Now I would like to clean up my code and need to remove many small issues that I did not fix during the porting before making the code public. In fact, most of the current problems are related to toolchains:

1. The first problem is a position independent code. Could you please describe me seL4' vision about it? muclibs is building with -fPIC, but everything else doesn't, right? I have a very tricky set of GCC’ flags, related to MIPS’ GOT, small data, abicalls, pic/non-pic, etc, and many of them are not working together.
We do not have a particular vision for it, although if people want it we will try and support it. Currently this amounts to our ia32 syscall stubs having the option to be built to support PIC.

Is 'muclibs' muslc? As far as I can tell it only builds a couple of the crt files explicitly with PIC.

I don't know much about MIPS, but for x86 as long as you are writing C and not assembly then the compiler can built it as PIC or not. If MIPS is similar then the choice to support PIC will just come down to what you want to do.
2. MIPS assembler has several features, one of them is that the -O0 code requires having an addition space above the top of the stack for 4 registers: 

43b610: 27bdffe8 addiu sp,sp,-24  <— start of the function
43b614: afbf0014 sw ra,20(sp)
43b618: afbe0010 sw s8,16(sp)
43b61c: afb0000c sw s0,12(sp)
43b620: 03a0f021 move s8,sp     <— frame stack
43b624: afc40018 sw a0,24(s8)   <— save 1st arg for a subroutine call
43b628: afc5001c sw a1,28(s8)   <— save 2nd arg for the subroutine
43b62c: afc60020 sw a2,32(s8)   <— save 3rd arg for  the subroutine

So, each time when I am allocating new stack I should return not top of the stack, but top_of_the_stack - 4*sizeof(seL4_Word). As result, sel4utils_configure_thread_config becomes platform specific. Could you please consider a possibility to put it into the «arch» as sel4utils_arch_init_context, or add something like «sel4utils_arch_configure». Also, it is important: this is an issue only for -O0 code, as far I see, -O2 uses different methods for arguments passing. I am trying to build toolchains which do not use frame pointer this style for -O0 code, but I am not sure about the result. 
Isn't this what 'sel4utils_arch_init_context_with_args', called from 'sel4utils_start_thread' is for?
3. I really like how you redesigned declaration syscalls. Now I have a freedom to modify syscalls and do not care about the mainline declarations because now there are syscall wrappers. However, my toolchain generates very poor code for CONFIG_LIB_SEL4_PUBLIC_SYMBOLS  and «DEFAULT» — I have proper working code only for CONFIG_LIB_SEL4_INLINE_INVOCATIONS. What is the conceptual difference of these declaration attributes, what they affect?
CONFIG_LIB_SEL4_PUBLIC_SYMBOLS is for when you would like the syscall functions to end up in libsel4.a, such that you can link against it and call them from, usually, languages other than C.

Not enabling CONFIG_LIB_SEL4_INLINE_INVOCATIONS results in kernel invocations not being inlined, although the actual syscall stubs themselves should still be inlined. The ability to not inline invocations was to allow for some verification analysis to be done at one point in the past.
4. Could you please tell me what was the C equivalent of this asm code: 

.global __syscall
.type __syscall,%function
__syscall:
    sub sp, sp, #4
    push {r5,r6}
    adr r5, 1f
    ldr r6, 1f
    ldr r5, [r5,r6]
    str r5, [sp, #8]
    pop {r5, r6}
    pop {pc}

.hidden __sysinfo
1:  .word __sysinfo-1b

something similar to __syscall6 from libmuslc/arch/<arch>_sel4/syscall_arch.h, right? 
I believe that is correct, yes.

Adrian