From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Tue, 22 Sep 2009 12:13:32 -1000 From: Tim Newsham To: Fans of the OS Plan 9 from Bell Labs <9fans@9fans.net> In-Reply-To: Message-ID: References: <> MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed Subject: Re: [9fans] linux stats in last year from linuxcon Topicbox-Message-UUID: 75c57dfa-ead5-11e9-9d60-3106f5b1d025 > 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/