doc: add detailed scheduler documentation

We should at least mention that threads with the same priority will still run until a higher prioritized thread is runnable again. Calling it round-robing could give the impression of a fair scheduling for equally prioritized threads. Actually, I'm not quite sure if we should really use the term round-robin.