From owner-freebsd-hackers@FreeBSD.ORG Sat Dec 31 07:34:34 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 00AB5106564A for ; Sat, 31 Dec 2011 07:34:34 +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 C51778FC0A for ; Sat, 31 Dec 2011 07:34:33 +0000 (UTC) Received: by pbcc3 with SMTP id c3so12310192pbc.13 for ; Fri, 30 Dec 2011 23:34:33 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; bh=VQqDthIErpdzRwjs9LvMLzgmA07marpRg8VOftj+848=; b=BM4S+8YepBgwjYKCy+if0rIab97uOL0HjMG9esGC33nSHorXRKPzqsG9hP4wy4bqWf jP/YbICjs/6OiZ7x+RendFDFlEnVsQrck7DLvUveJmPW5hprzjdjfzEW2lSp5aECw8bu nLRQQKUneYnqXXrnhDNXrHOkmGvFl1WX7EDq8= Received: by 10.68.213.68 with SMTP id nq4mr13897195pbc.126.1325316873239; Fri, 30 Dec 2011 23:34:33 -0800 (PST) MIME-Version: 1.0 Received: by 10.143.77.16 with HTTP; Fri, 30 Dec 2011 23:34:02 -0800 (PST) In-Reply-To: <4EFE5806.3090000@freebsd.org> References: <4EFE5806.3090000@freebsd.org> From: arrowdodger <6yearold@gmail.com> Date: Sat, 31 Dec 2011 10:34:02 +0300 Message-ID: To: Julian Elischer Content-Type: text/plain; charset=UTF-8 X-Content-Filtered-By: Mailman/MimeDel 2.1.5 Cc: freebsd-hackers Subject: Re: 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: Sat, 31 Dec 2011 07:34:34 -0000 On Sat, Dec 31, 2011 at 4:32 AM, Julian Elischer 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!