Tuesday, April 13, 2010

Proof of Soundness for a Typestate Checker with Locks

Right now I am working on (what I hope will be) the last major theoretical effort of my thesis. I need to do another proof. Way back when I wrote this paper for OOPSLA in 2008, I did a proof of soundness for my language, a language that used atomic blocks for mutual exclusion. Right now, I'm doing the same thing but for a language that uses synchronized blocks. In other words, a language that is more Java-like.

Proofs are pretty painful for me, and the last one I did was really complicated, so rather than merely update the old proof to add locks, I am actually rewriting and simplifying (I think?) a whole bunch of stuff.

One of the biggest questions for me is a question that is important whenever you are doing a proof for a language with references; how will I define a well-typed heap? A well-typed heap means a runtime heap that is consistent with the type-checking facts that were known statically. In my system, every thread is an expression, and each one has its own type-checking context. They all much be consistent with the heap. Furthermore, in anticipation of my proof of preservation (where I have to show that after a step, the heap will still be well-typed) I think that my definition of a well-typed heap will have to include the following condition:
At most one thread can know statically the exact state of an object.
In my last proof I had a similar condition, but it was really unweildy to work with. I wonder how I can simplify this desire?


  1. If you define a heap as a mapping from addresses to expressions (or values), then a well-typed heap is a heap that is associated with a mapping from addresses to types, where each value at an address has the corresponding type in the "heap typing".

    Your preservation proof should state that the resulting heap after the step has the same "heap tying" or has a "heap typing" that is an extension of the previous one.

  2. Thanks, yes this will all be true of my heap invariant, since at it's core my language is Java-like. But my heap invariant will preserve additional properties as well (e.g., the locks that are currently held, the abstract state an object is in) because of the additional properties our type system enforces.