RE: [abc] Concrete operational semantics

Hi, everybody. Thanks for your comments!

Julian: I will try what's going on there and send a possibly corrected
version ASAP. Such issues were exactly what I was looking for.

Regarding Ondrej's comments: It is correct that you do give some
operational semantics in the OOPSLA paper. However, IMHO they are still
fairly far away from what is actually going on in the TM implementation,
in particular when it comes down to how the tracematch actually binds
values internally. When you look at section 4.6 and 4.7 there, you will
find that constraints are being updated in a more or less algebraic
style, using functions "and" and "or" and "not, etc. This shows a nice
semantic equivalence to your declarative semantics (because it is very
close to them) but it is not very close to the implementation. In the
implementation we for example have this clear distinction between
updating negative and positive bindings, which differ a lot from each
other (as you can see in the definitions of neg and pos in my work
here). Now it turns out that exactly those differences are important for
the PLDI paper.

For example, at the moment we cannot handle skip-loops in a meaningful
way because we have no must-alias analysis. We might understand this,
but how shall I tell the reader? If you now look (in my proposal) at the
definition of "neg" (right before section 5), you will see that there we
only return "false", i.e. discard a partial match, when we know that the
negative binding we pass in is *the same* object as we have stored.
This, we cannot prove statically without must-alias analysis.

Another reason is that the implementation of my analysis is also very
close to the tracematch code. It uses very similar methods for updating
positive and negative bindings.

So in a nutshell, to me the semantics in the OOPSLA paper are some good
intermediate representation but it is just too coarse-grained for our
purposes here. I could, as you propose, refer to the OOPSLA semantics at
some parts and so safe a few lines here. But on the other hand I think
having a complete semantics in one paper, without the reader requiring
to browse through another one, is something I am not really willing to
give up if not necessary. I think the semantics will take up about two,
maximally two and a half pages, and all the remainder of the paper will
build up on it and benefit from it.

Does that make sense to you?

Eric

> -----Original Message-----
> From: Majordomo list server [mailto:majordomo@comlab.ox.ac.uk] On
> Behalf Of Ondrej Lhotak
> Sent: Friday, October 06, 2006 8:40 AM
> To: abc@comlab.ox.ac.uk
> Subject: Re: [abc] Concrete operational semantics
>
> Hi Eric...
>
> You have defined a semantics fully, from the beginning. If I
understand
> correctly, you are asking us to confirm that it is semantically
> equivalent to the abc tracematch implementation, whose (intended)
> operational semantics is given in the OOPSLA 05 paper. Since you want
> them to be equivalent, why not just use the semantics from the OOPSLA
> paper? I see that there are some differences, such as the multiple
> labelled skip loops. It would be much easier to see what is the same
> and what is different (and to prove that the differences do not change
> the behaviour) if the OOPSLA semantics were presented first, and then
> the differences were presented as changes to the original, using the
> original notation.
>
> Ondrej
>
> On Wed, Oct 04, 2006 at 12:10:07PM -0400, Eric Bodden wrote:
> > Hi all.
> >
> > In the svn repository
> > (https://svn.sable.mcgill.ca/sable/papers/pldi07tmstat) there is now
> > an updated version, which holds a commented version of the concrete
> > operational semantics for tracematches. (PDF copy attached for your
> > convenience) The plan is to use this as a sort of baseline for what
> > follows in the paper, i.e. the program abstraction and the actual
> > analysis, which is actually really close to those operational
> semantics.
> >
> >
> > I would be very grateful if everybody who was involved with the
> > implementation of TMs could please try to verify that what I wrote
is
> > correct. In my opinion it should reflect pretty much what is
actually
> > going on, under the following assumptions:
> >
> > - Indexing and leak detection (including weak bindings) are
disabled.
> > (no need to bother the reader with this here)
> > - Instead of a generic skip-loop we have labelled skip-loops as
> > mentioned some weeks (months?) ago. See paper for details.
> > - The updates in the semantics are no in-place updates but purely
> > functional. Hence, we need no real "temp" data structure as in the
> > actual implementation.
> >
> > For your convenience, I have temporarily enabled numbering of the
> > equations. So if you find anything wrong, please refer to the
> location
> > by those numbers if possible. Everything in the boxes are comments
> for
> > you and will be replaced by an appropriate less informal filling in
> > the final paper.
> >
> >
> > Thanks a lot in advance!
> >
> > Cheers,
> > Eric
>
>
Received on Fri Oct 06 15:22:14 2006