Date: Fri, 30 Dec 2011 16:32:06 -0800 From: Julian Elischer <julian@freebsd.org> To: arrowdodger <6yearold@gmail.com> Cc: freebsd-hackers <freebsd-hackers@freebsd.org> Subject: Re: Using symbolic execution for analyzing scheduler performance? Message-ID: <4EFE5806.3090000@freebsd.org> In-Reply-To: <CALH631=v690XayAix=vX7NTyj%2BSnML%2BMpzFC6i0Ms0Bg%2BEaKTw@mail.gmail.com> References: <CALH631=v690XayAix=vX7NTyj%2BSnML%2BMpzFC6i0Ms0Bg%2BEaKTw@mail.gmail.com>
next in thread | previous in thread | raw e-mail | index | archive | help
On 12/30/11 9:52 AM, arrowdodger wrote: > Hi. First, let me put a little disclaimer: > I have absolutely no CS education and any degree in science, no idea on how > OS kernels and CPU schedulers are implemented and working. Moreover, i > haven't even know math at the level needed to talk about what i'm > proposing. What i'm going to propose may be just nonsence. > > I've assumed that: > - Scheduler in FreeBSD is just a bunch of code, which implemens some > interface. yes, though it is very complicated interface, and some of it is not explicit. > - This implementation is self-contained - it doesn't call any other kernel > functions and do not depend on other state except itself. That is not really true. There are all sorts of interactions. Not all of them are as simple as a call. > - 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. > If these assumptions are true, it may be possible to compile scheduler > code as userland code and link it with sort-of driver, which would call > scheduler functions in same way as real kernel does. So we get a > statically-linked executable, which would emulate working kernel for the > scheduler. yes that would certainly be true from some perspective. But it would be quite a bit of work. > Now we will be using KLEE [1] - a virtual machine for symbolic execution. > It uses SAT solvers to reason about veriables values. > In our driver code we insert calls to klee_assert() after every call to > scheduler function to make KLEE dump current symbolic restrictions on > scheduler's internal state values. Finally, we mark all data, describing > scheduler state as symbolic and run program on KLEE. > As result, we get (i hope so) a set of all possible states in which > scheduler can ever be in form of KLEE test file (.ktest). A test is > represented by descriptions of what value each variable can have in the > current context. So, any of generated states is not intersecting with each > other. It is a nice goal but I can't see it happening.. I think that the scheduler is probably a bit too complicated.. the automatic testing and verification woudl be nice but my head hurts thinking about it :-) > Now it's possible to concretize symbolic values for each test and save it > as normal executable. You may think of it as a model of how our scheduler > is functioning. Now we can symbolically execute these binaries again, but > for now marking as symbolic all "external" data from scheduler point of > view. This way we can track and debug scheduler decisions in any > circumstance. > > In other words: > 1. All possible scheduler states are being found. > 2. Identical states are being thrown away. // done by KLEE > 3. For each state model scheduler behavior for every input (and skipping > modellings, which yields same results). > > I'm not sure if it can help to solve current ULE problems, but it should > really help debugging scheduler during development. I don't think that the scheduler needs debugging so much as the specification of it needs thinking.. The scheduler has teh problem of trying to make decisions about what to do in the future from imperfect knowledge of the past, and no knowledge of the future. > 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. 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? (and you are not really 6 years old, are you? :-) > [1] http://klee.llvm.org/ > _______________________________________________ > freebsd-hackers@freebsd.org mailing list > http://lists.freebsd.org/mailman/listinfo/freebsd-hackers > To unsubscribe, send any mail to "freebsd-hackers-unsubscribe@freebsd.org" >
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?4EFE5806.3090000>