From owner-freebsd-hackers@FreeBSD.ORG Fri Dec 30 17:53:11 2011 Return-Path: Delivered-To: freebsd-hackers@freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2001:4f8:fff6::34]) by hub.freebsd.org (Postfix) with ESMTP id 061F6106566B for ; Fri, 30 Dec 2011 17:53:11 +0000 (UTC) (envelope-from 6yearold@gmail.com) Received: from mail-pw0-f54.google.com (mail-pw0-f54.google.com [209.85.160.54]) by mx1.freebsd.org (Postfix) with ESMTP id D4CF18FC12 for ; Fri, 30 Dec 2011 17:53:10 +0000 (UTC) Received: by pbcc3 with SMTP id c3so12003121pbc.13 for ; Fri, 30 Dec 2011 09:53:10 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=mime-version:from:date:message-id:subject:to:content-type; bh=YtCVTkO39bvxEoKMrg5P7bPEQF9cidxEx3/GDLYBt3Y=; b=pVtkoHM5MSPcZx77yfcBVX3vavxbyZqJ5B2UlLoGkudCvBoSj2f4AdX7+ww5r4nJg8 nA439DZx+Np2xYXRCVZHqKPOKbr9TgHUWbdSh7qAALhPCBZGIQNcASUZBODgmxifWwh7 SWbD6zOEkJ2FGu94Nv4XasWYMRQ7t5Km8dBMM= Received: by 10.68.192.74 with SMTP id he10mr11988705pbc.24.1325267590285; Fri, 30 Dec 2011 09:53:10 -0800 (PST) MIME-Version: 1.0 Received: by 10.143.77.16 with HTTP; Fri, 30 Dec 2011 09:52:39 -0800 (PST) From: arrowdodger <6yearold@gmail.com> Date: Fri, 30 Dec 2011 20:52:39 +0300 Message-ID: To: freebsd-hackers Content-Type: text/plain; charset=UTF-8 X-Content-Filtered-By: Mailman/MimeDel 2.1.5 Subject: Using symbolic execution for analyzing scheduler performance? X-BeenThere: freebsd-hackers@freebsd.org X-Mailman-Version: 2.1.5 Precedence: list List-Id: Technical Discussions relating to FreeBSD List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Fri, 30 Dec 2011 17:53:11 -0000 Hi. First, let me put a little disclaimer: I have absolutely no CS education and eny 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. - This implementation is self-contained - it doesn't call any other kernel functions and do not depend on other state except itself. - OS kernel calls scheduler functions in some defined order. I've 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. 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. 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. What do you think? Does it make any sence, or i should just return under my rock? PS: Sorry for my english, i hope you understood what i've been trying to say. [1] http://klee.llvm.org/