9fans - fans of the OS Plan 9 from Bell Labs
 help / color / mirror / Atom feed
From: Tim Newsham <newsham@lava.net>
To: Fans of the OS Plan 9 from Bell Labs <9fans@9fans.net>
Subject: Re: [9fans] linux stats in last year from linuxcon
Date: Tue, 22 Sep 2009 12:13:32 -1000	[thread overview]
Message-ID: <Pine.BSI.4.64.0909221210020.23231@malasada.lava.net> (raw)
In-Reply-To: <e001949c63cb98e8a8de5710b41904af@brasstown.quanstro.net>

> i'm not clear on what all functional correctness entails.  can
> a functionally correct program suffer from deadlock or livelock?

Yes.  It depends on if that property was stated as part of the
specification of what correctness means.
That is definitely something that can be stated and proven.
I'm not sure if their spec stated that correctness means no
deadlocks or if they explicitely stated that as a property
and then proved it.  The spec is publically available but I havent
studied it.  The proofs are not yet available.  There are some
papers that talk about some of what they have done.

> - erik

Tim Newsham
http://www.thenewsh.com/~newsham/



  parent reply	other threads:[~2009-09-22 22:13 UTC|newest]

Thread overview: 46+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
     [not found] <<Pine.BSI.4.64.0909220654020.23231@malasada.lava.net>
2009-09-22 17:13 ` erik quanstrom
2009-09-22 18:27   ` David Leimbach
2009-09-22 22:13   ` Tim Newsham [this message]
2009-09-22 22:25     ` Tim Newsham
2009-09-22 22:44       ` Jason Catena
     [not found] <<012201ca3fec$c58f6020$50ae2060$@com>
2009-09-28  3:38 ` erik quanstrom
2009-09-21 16:22 ron minnich
2009-09-21 16:44 ` Patrick Kelly
2009-09-21 17:04   ` erik quanstrom
2009-09-21 17:29     ` Patrick Kelly
2009-09-21 17:02 ` tlaronde
2009-09-21 17:20   ` Patrick Kelly
2009-09-30 13:22   ` Ethan Grammatikidis
2009-09-21 17:41 ` Jack Norton
2009-09-21 17:53   ` Patrick Kelly
2009-09-21 19:32     ` David Leimbach
2009-09-21 19:42       ` Patrick Kelly
2009-09-22  1:12         ` andrey mirtchovski
2009-09-22  1:26           ` Patrick Kelly
2009-09-22  2:33             ` erik quanstrom
2009-09-22  2:52               ` andrey mirtchovski
2009-09-22  2:58               ` Patrick Kelly
2009-09-22  3:02                 ` erik quanstrom
2009-09-22  6:15               ` Tim Newsham
2009-09-22 14:23                 ` erik quanstrom
2009-09-22 16:57                   ` Tim Newsham
2009-09-22 13:48               ` Eric Van Hensbergen
2009-09-22 14:44                 ` David Leimbach
2009-09-22 14:39               ` David Leimbach
2009-09-22 14:47                 ` erik quanstrom
2009-09-22 15:04                   ` David Leimbach
2009-09-22 15:14                     ` erik quanstrom
2009-09-22 16:26                       ` David Leimbach
2009-09-22  3:36           ` ron minnich
2009-09-22  3:38             ` ron minnich
2009-09-22 14:17           ` J.R. Mauro
2009-09-22 14:47             ` David Leimbach
2009-09-22 20:14             ` Richard Uhtenwoldt
2009-09-22 20:47               ` Jack Norton
2009-09-22 22:31                 ` Patrick Kelly
2009-09-23  1:55                 ` David Arnold
2009-09-24 14:21                   ` Patrick Kelly
2009-09-24 15:46                     ` Jacob Todd
2009-09-24 15:56                     ` Iruata Souza
2009-09-28  3:35                       ` Patrick Kelly
2009-09-22 20:55             ` Chad Brown

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=Pine.BSI.4.64.0909221210020.23231@malasada.lava.net \
    --to=newsham@lava.net \
    --cc=9fans@9fans.net \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).