Re: [seL4] SMC in seL4

2018-08-28 Thread Dongxu Ji
Hi Yanyan, According to your advice,I modified the avail_p_regs[] in hardware.h file as tk1. 1 MiB starting from 0x37f0 is reserved for monitor mode. { /* .start = */ 0x1000, /* .end = */ 0x37f0} And then #define MON_PA_START (0x1000 + 0x27f0) #define MON_PA_SIZE

Re: [seL4] SMC in seL4

2018-08-28 Thread Yanyan.Shen
Hi Dongxu, As you can see, the arm_monitor_vector uses PC-relative addressing so that the code can be moved around in memory. I think ldr pc, =smc_handler breaks this. Also, please set the NS bit in SCR to 1 before returning. To reserve a memory region for the monitor-mode code and data, I

[seL4] Fwd: SMC in seL4

2018-08-28 Thread Dongxu Ji
Hi Yanyan, 1. It doesn't set the NS bit to 1 in SCR(I just want it to return without do anything). The arm_monitor_vector and the smc_handler(): arm_monitor_vector: ldr pc, [pc, #28] ldr pc, [pc, #24] ldr pc, =smc_handler ldr pc, [pc, #16] ldr pc, [pc, #12] ldr pc, [pc,

Re: [seL4] SMC in seL4

2018-08-28 Thread Yanyan.Shen
Hi, The smc_handle() in monitor.S, it does nothing but "movs pc, lr". Does it set the NS bit to 1 in SCR? Also, what did you do to ensure that 0x1100 is not used by the kernel? Could you share the code (if possible) so that I could better understand the problem. Regards, Yanyan