To: Martin Abadi <firstname.lastname@example.org>
Subject: Re: failures
From: Vijay Saraswat <email@example.com>
Date: Tue, 03 Dec 2002 11:00:28 -0500
CC: Matthias Felleisen <firstname.lastname@example.org>, email@example.com
References: <200212030144.gB31iWwc012911@saul.cis.upenn.edu> <200212031152.gB3BqkEx006860@saul.cis.upenn.edu>
User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:1.0.1) Gecko/20020823 Netscape/7.0
The original Java classloader design had a major bug -- arising
basically (in my opinion) because of some naive reasoning by the
language designers. See http://www.research.att.com/~vj/bug.html
After some careful thinking, this was subsequently fixed. See
One could similarly argue that the entire Java Thread design (Chapter
17) is substantially flawed. I have not personally spent time on it, but
I know that Doug Lea and Bill Pugh are leading a major effort to
redesign the Java Memory Model, see
Martin Abadi wrote:
> [----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]
> Another example, with a somewhat similar flavor, is the combination
> of subroutines and object initialization in the Java bytecode language.
> Both subroutines and object initialization are delicate even in
> Freund and Mitchell found that the Java bytecode verifier (in Sun's
> JDK 1.1.4) did not treat their interactions correctly. More specifically,
> exploiting some loopholes related to subroutines, one could use an
> object before its initialization, contradicting the intended properties
> of the verifier.
> There might be a third example in the work of Gordon and Syme
> on typing the intermediate language in Microsoft's Common Language
> Runtime. Their paper says "The process of writing this specification,
> deploying the executable specification as a test oracle, and
> applying theorem proving techniques, helped us identify several
> security critical bugs during development." I don't remember seeing
> published details of those bugs.
> Matthias Felleisen wrote:
>> [----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]
>> Okay, this didn't work out. Let's try again.
>> Are examples out there that show how naive reasoning about languages
>> (not individual programs) is a major problem?
>> The canonical example is to combine polymorphic let without
>> restrictions with naive generalizations for references, exceptions,
>> continuations, and channels.
>> For what else have we needed *any* form of semantics to dispute naive
>> I for one would find it really neat if we had such a list of examples
>> on-line for use in courses at all levels and program officers at
>> funding agencies, too.
>> Any other examples than the one above? One is a random hit, two is a
>> coincidence, three makes a pattern. -- Matthias