Hi, Your website(https://sel4.systems/About/Performance/home.pml) lists the IPC benchmark result, and I wonder is the x64 result for both fastpath, or both slowpath, or one fastpath and the other slowpath?
According to the evaluation of my own on x64 kabylake, the fastpath client->server takes about 600 cycles, and slow path client->serve takes over 1100 cycles. But the website data is 1465 and 780, but it does not show whether it is fastpath or slow path. It looks like that the website data has client->server goes into slowpath(maybe because of lower priority), and the server->client goes into fastpath. Is it so? Thanks, Zihan _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
