HelenOS: portable microkernel-based multiserver operating system

Re:HelenOS: portable microkernel-based multiserver operating... by aidenn0 on Friday August 18, 2017 @02:24PM (#15048543)

Are those really WCET? A L3 miss on an i7 4770 is ~60ns and they show 90ns total execution time. If that's true it's incredibly impressive.

[edit]

Also formal WCET analysis for various IPCs is really great and not something you can "bolt on" to a kernel not designed for it.

[ Parent | on HN ]

Re:HelenOS: portable microkernel-based multiserver operating... by snvzz on Friday August 18, 2017 @02:45PM (#15048718)

You might want to look into: http://ts.data61.csiro.au/projects/seL4/

Specifically:

Bernard Blackham, Yao Shi, Sudipta Chattopadhyay, Abhik Roychoudhury and Gernot Heiser

Timing analysis of a protected operating system kernel

IEEE Real-Time Systems Symposium, pp. 339-348, Vienna, Austria, November, 2011

---

TL;DR: They assume worst case for cache misses.

e.g.: "The latency of a read or write to physical memory on this platform was measured to be 80–100 cycles; in the static analysis we assume a 100-cycle penalty for all cache misses."

[ Parent | on HN ]

Re:HelenOS: portable microkernel-based multiserver operating... by aidenn0 on Sunday August 20, 2017 @04:59PM (#15060230)

That would mean ~2 cache lines are accessed for an IPC call, plus another 130 cycles for instructions. That's very impressive.

[ Parent | on HN ]