I have been measuring the performance of my application and doing some comparisons with other kernels. I had a couple of queries.

I am running seL4 on zynq device. I am using the given timer driver in libplatsupport to measure the clock cycles. 

Queries:

1) I have found the sample benchmark numbers for seL4 IPC from http://l4hq.org/docs/performance.php. Since I am running on Armv7 Cortex A9 , the time for one half way trip is 316 ns. Is this measured from system call to system call or from process to process?

2) I am trying to compare the performance on FreeRTOS and Linux, is there any such comparison on where seL4 stands?

3) Does the IPC time vary with the different api of ReplyRecv, Reply, seL4_NBRecv? I have this question because I am seeing that Reply is taking about twice the amount of clock cycles compared to Recv.

In terms of my application, I am majorly looking at measuring one whole cycle which includes:

1) 1st Process sends message to 2nd Process

2) 2nd Process Reads from AXI device space

3) 2nd Process replies with Reply and waits for another command from 1st process

4) 1st process sends another message to 2nd Process

5) 2nd Process writes to the hardware

6) Time from step 1 to step 5 is measured.

Results for this on 

seL4 :  3180 clock cycles

FreeRTOS: 2414 clock cycles

I am sure there is possibility of unnecessary overheads involved in my measurement, but I expected seL4 to be faster. Can someone help me in this regard.

Regards

Neelesh Vemula