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?