Comments requested on paper: functional purity in Joe-E

[David Wagner-3]

Toby Murray writes:

>"In particular, there cannot be any cycles in immutable data
>structures." I don't get this.. What about
>
>public class Bar implements Immutable{
>   private Foo _foo;
>   public Bar(Foo foo){
>      _foo = foo;
>   }
>}
>public class Foo implements Immutable{
>   private Bar _bar;
>   public Foo(){
>      _bar = new Bar(this);
>   }
>}
>
>Would Foo not be considered Immutable?

Great example.  No, Foo doesn't qualify as an Immutable class, because
it violates some of Joe-E's rules.  Let me try to explain.

First, you'd need to add a "final" keyword to all of the fields.
The Joe-E verifier needs to know that you cannot change the value of the
fields once they have been initialized, and it does that by requiring
you to use the "final" keyword.

Second, the Joe-E verifier should flag an error in the Foo() constructor,
because the call "new Bar(this)" allows the this-pointer to escape.
We must prohibit that, for reasons that may seem a bit crazy at first.

The crazy reason is that, in Java, the "final" keyword does not actually
make a field final (i.e., doesn't make the field a constant throughout the
lifetime of the object).  Huh?  Yes, that's right.  The "final" keyword
does ensure that a field may be assigned to only once.  However Java
allows you to read the value of a field that has not yet been assigned
to, in which case the field has its default value (0, null, or false,
depending upon its type).  So if someone reads the value of this._bar
before it is assigned, and then reads it after this._bar has been
assigned, they will see two different values -- in violation of what
we'd expect from an immutable object.

You might not be familiar with this oddity of the Java language, because
Java makes a best-effort (but imperfect) attempt to prevent this kind
of unexpected behavior.  In particular, Java has something called the
"definite assignment" rules which are intended to ensure that a final
field is assigned at least once and at most once.

Unfortunately, the definite assignment rules have a hole: Java only does
intraprocedural analysis (inside the constructor), and Java does not
try to prevent other methods from reading a field that has not yet been
assigned.  The bad case can only happen if you allow the this-pointer
to escape from the constructor, because then other methods might be
able to get a reference to an incompletely-initialized instance (i.e.,
one where the constructor has not yet finished running) of the class.

So, to fix up the hole in Java's definite assignment rules, Joe-E
introduces restrictions which suffice to ensure that the this-pointer
cannot escape from the constructor.  As a result, if you run the Joe-E
verifier on the above example, I expect it to complain about the body
of the Foo() constructor.  (Give it a try and see if I've predicted
correctly!)

As a result, I believe it is correct that one cannot create cyclic
immutable data structures in Joe-E -- which is a shame.

We didn't really want to go into this in this paper, because we felt the
mechanism for verifying Immutability is a bit out of scope.  We plan
to write another paper focusing on the overlay type system and on the
mechanisms we use for enforcing Immutable types, including the issues
with the "final" keyword and some other peculiarities we ran across.
_______________________________________________
e-lang mailing list
e-lang@...
http://www.eros-os.org/mailman/listinfo/e-lang

[Toby Murray-4]

On Wed, 2008-06-04 at 10:10 -0700, David Wagner wrote:
> Toby Murray writes:
> >"In particular, there cannot be any cycles in immutable data
> >structures." I don't get this..

>  Let me try to explain.

> The crazy reason is that, in Java, the "final" keyword does not actually
> make a field final.
> Java makes a best-effort (but imperfect) attempt to prevent this kind
> of unexpected behavior.  In particular, Java has something called the
> "definite assignment" rules which are intended to ensure that a final
> field is assigned at least once and at most once.
> Unfortunately, the definite assignment rules have a hole: Java only does
> intraprocedural analysis (inside the constructor), and Java does not
> try to prevent other methods from reading a field that has not yet been
> assigned.  
> So, to fix up the hole in Java's definite assignment rules, Joe-E
> introduces restrictions which suffice to ensure that the this-pointer
> cannot escape from the constructor.
>
> As a result, I believe it is correct that one cannot create cyclic
> immutable data structures in Joe-E -- which is a shame.

Thanks for the lucid explanation. Makes perfect sense now and I agree
with the assertion in the paper.


> We didn't really want to go into this in this paper, because we felt the
> mechanism for verifying Immutability is a bit out of scope.

Fair enough indeed. This paper's focus is elsewhere I understand.

>   We plan
> to write another paper focusing on the overlay type system and on the
> mechanisms we use for enforcing Immutable types, including the issues
> with the "final" keyword and some other peculiarities we ran across.

Cool. Looking forward to it.

Thanks again

Toby
_______________________________________________
e-lang mailing list
e-lang@...
http://www.eros-os.org/mailman/listinfo/e-lang