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

Re: failures


>>>>> "MF" == Matthias Felleisen <matthias@ccs.neu.edu> 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.

(4) and the implementation could be adjusted accordingly.

For the general problem and the counterexamples:

    Aliasing Models for Mobile Objects 
    (with Hans Hüttel, Josva Kleist, and Massimo Merro).
    I&C 175(1): 3-33 (May 2002).

For the proofs using pi-calculus:

    Mobile Objects as Mobile Processes 
    (with Massimo Merro and Josva Kleist).
    I&C 177(2): 195-241 (October 2002).

For the proofs using a direct operational semantics:

    Mobile Objects "Must" Move Safely (with Sébastien Briais).
    In: Proceedings of FMOODS 2002, pages 129-146. 
    Kluwer Academic Publishers. (March 2002).

Overall information from:

    http://www.cs.auc.dk/research/FS/ojeblik/

== Uwe ==