[Prev][Next][Index][Thread]

Re: failures

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 
http://java.sun.com/people/gbracha/classloaders.ps

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 
http://www.cs.umd.edu/~pugh/java/memoryModel/

Best,
Vijay

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 
> isolation.
> 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.
>
> Martin
>
>
> 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
>> generalizations?
>> 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
>>
>>
>
>
>