headers
Matthias Felleisen | 3 Dec 2002 01:53
Favicon

failures


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
Permalink | Reply | 0 comments |
headers
Martin Abadi | 3 Dec 2002 06:49
Favicon

Re: failures

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,
(Continue reading)

Permalink | Reply | 0 comments |
headers
Olivier Ridoux | 3 Dec 2002 09:55
Picon
Favicon

Re: failures

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.
...
> Any other examples than the one above? One is a random hit, two is
> a coincidence, three makes a pattern. -- Matthias

A cousin example is type isomorphism.  How far can we go in the idea
that a function of type A->B->C can be a match for a function of type
B->A->C?  A semantic notion of type isomorphism helps.

Ok, this is very close to the first example; it may count for only a
half hit.

Olivier Ridoux

--

-- 
Docendo discimus
Permalink | Reply | 0 comments |
headers
Martin Odersky | 3 Dec 2002 09:59
Picon
Picon
Favicon

Re: failures


Matthias Felleisen <matthias@...> writes:

>   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? 
> 
To dispute a generalization, a counter-example suffices. Generally a
naive understanding of the evaluation of a program is good enough to
realize that the counter-example is really one. So you don't even need
semantics to explain the problem of polymorphic let without
restrictions in the presence of references.

I think semantics comes into play if one wants to convince oneself
that a solution is really what it claims to be. Restricted polymorphic
let is such a case.

> Any other examples than the one above? One is a random hit, two is 
> a coincidence, three makes a pattern. 

Here are two others:

- Covariant vs contravariant overriding in object-oriented languages
  (more generally known as the binary method problem).  Eiffel got that
  one wrong. I need semnatics to convince myself that (for instance) mytype and
  matching is a solution.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Xavier Leroy | 3 Dec 2002 10:11
Picon
Picon
Favicon

Re: failures

Matthias asks:

> 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? 

Another example of unsoundness resulting from the careless combination
of features that make sense each on its own is the famous
"Inheritance is not subtyping" problem (Cook, Hill, Canning, POPL 89).

- Xavier
Permalink | Reply | 0 comments |
headers
Philip Wadler | 3 Dec 2002 15:29

Re: failures

If you want to add to the list of industrial-strength applications
of semantics, look at:

  XQuery 1.0 and XPath 2.0 Formal Semantics 
  W3C Working Draft 15 November 2002
  http://www.w3.org/TR/query-semantics/

A summary of part of this work is contained in:

  The Essence of XML
  Jerome Simeon and Philip Wadler
  POPL 2003, New Orleans, January 2003. 
  http://www.research.avayalabs.com/user/wadler/topics/xml.html#xml-essence
  [NB: Final POPL version will not be at this URL until tomorrow]

Here are two quotes from the paper:

  The act of preparing the formal semantics has uncovered a number of
  errors or omissions in the prose specification.  In particular,
  developing the material on the formal semantics of named typing led to
  the formulation of ten issues for consideration by the XQuery working
  group, each dealing with a point that was omitted in the prose
  specification of XQuery.

  ...

  In October 2002 the XQuery working group decided to adopt pure named
  typing.  The final step before adoption was a presentation describing
  how pure named typing simplifies the formal semantics.  (Pure named
  typing was adopted after this paper was accepted to POPL but before
(Continue reading)

Permalink | Reply | 0 comments |
headers
Vijay Saraswat | 3 Dec 2002 17:00
Gravatar

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.
>
(Continue reading)

Permalink | Reply | 0 comments |
headers
Robert Harper | 3 Dec 2002 18:18
Picon
Favicon

RE: failures

A while back Stephan Kahrs uncovered an unsoundness in the 1990 version of
Standard ML having to do with datatype's escaping their scope.
Specifically, it was allowed that a datatype could be introduced via a let,
but to have a value of that type (say, a constructor) returned from the let.
This was "obviously wrong" by comparison with abstype's, but it took a bit
of work to show that the semantics as given originally was, in fact,
unsound.
Martin has a good point about the role of semantics helping us to be sure.
But I would also say that in my experience a semantics can also be useful in
finding errors.  For example, we found the let/callcc bug by trying to push
through a soundness proof, and discovering that the proof didn't work.  It
didn't take long from there to discover a counterexample.
A similar example came up recently in connection with the notion of
applicative and generative functors in ML.  Moscow ML allows one to convert
a generative functor into an applicative functor by eta expansion.  Although
it made me uncomfortable we could find nothing concretely wrong with this,
until we undertook a thorough semantic analysis.  By examining the issue
from the point of view of abstract computational effects we observed that
this "feature" amounted to turning a partial function into a total function
by simply eta-expanding it.  This seemed more concretely wrong, and, as it
turns out, uncovers an unsoundness in the implementation.  (This is all
explained in a forthcoming POPL 2003 paper.)
Bob
Permalink | Reply | 0 comments |
headers
David Walker | 3 Dec 2002 20:43
Picon

POPL 03 Second Call for Participation

The updated call for participation to POPL 03 has several pieces of new
information that Types readers should beware of:

-- Two New Invited Speakers

-- A reception the evening before the conference begins,
   Jan. 14, 6PM - 9PM.

-- A dinner at the Aquarium of the Americas on Jan. 16.

-- To receive the special conference rate ($149/night) at the
   conference hotel, be sure to mention POPL 03 when registering.

-- Early registration deadline is December 25, 2002.

                             Call for Participation

                    30th Annual ACM SIGPLAN-SIGACT Symposium

                                      on

                       Principles of Programming Languages

                                   (POPL 03)

                              January 15-17, 2003
                 Conference Reception:  Evening of January 14

                            New Orleans, Louisiana
(Continue reading)

Permalink | Reply | 0 comments |
headers
Uwe.Nestmann | 4 Dec 2002 10:49
Picon
Picon
Favicon

Re: failures


>>>>> "MF" == Matthias Felleisen <matthias@...> writes:

MF> Are examples out there that show how naive reasoning
MF> about languages (not individual programs) is a major
MF> problem?

In the context of Obliq, Luca Cardelli suggested that object
migration could be derivable from object _cloning_ followed
by object _aliasing_ (basically, proxy-like redirection to a
copy of itself at another site).

While trying to prove that this indeed works, proving a
suitably simple equation on programs according to which an
object before and after migration should not be
distinguishable (ignoring potential site failures):

(1) we uncovered counterexamples that tell that it can only
    work under the quite strong restriction that migration
    calls are only external (which is not decidable!)

(2) we uncovered counterexamples that tell that even when
    regarding only external migration calls, the
    implementation of Obliq is such that the simple equation
    does not hold.

(3) we proposed an improved semantics (both directly and by
    translation into a localized pi-calculus) for which we
    proved that (external) object migration is indeed safe,
    according to some notions of testing equivalence.
(Continue reading)

Permalink | Reply | 0 comments |

Gmane