Using symbolic execution for analyzing scheduler performance?

[arrowdodger]

On Sat, Dec 31, 2011 at 4:32 AM, Julian Elischer <julian at freebsd.org> wrote:

> On 12/30/11 9:52 AM, arrowdodger wrote:
>
>> - OS kernel calls scheduler functions in some defined order.
>>
>
> The OS doesn't really call the scheduler in that way.
> all sorts of threads of execution jump into the scheduler from all sorts
> of places and
> the internal state of the scheduler changes with these calls.  Sometimes
> those calls
> never return, and sometimes they return a long time later..  As I said,
> it's a very
> complicated interface.
>

Oh, threads. Yes, this imposes unimaginable complexity on what i'm
proposing.


>  What do you think? Does it make any sence, or i should just return under
>> my
>> rock?
>>
>
> no, come out from your rock..  If you are interested in the scheduler,  by
> all means
> go and read it and try and understand it, and then come back  to us if you
> do have  ideas.
>

Yeah, i think it's what i should've done in first place, before dumping by
brain to ML.
Okay, i will try to get an idea of how schedulers work in detail and after
that will try to find parts of it, which can be automatically verified.

BTW, is there any documentation on how write schedulers for FreeBSD, or at
least, ULE specification?

I don't think your idea is really bad but I think you underestimate the
> difficulty of the task.
>
>  PS: Sorry for my english, i hope you understood what i've been trying to
>> say.
>>
> your english is fine.. what do you normally speak?
>

Russian.

(and you are not really 6 years old, are you? :-)
>

Yeah, i've grown up a little, since then.

Thanks for your insight!