Re: [abc] Concrete operational semantics

I think I agree with the point you are making: that the OOPSLA
semantics is not sufficiently detailed and not sufficiently close to
the implementation to describe your work. I think you miss my point:
that what is needed is a bridge from the OOPSLA semantics to your more
detailed semantics and/or the implementation. (We could argue about
whether such a bridge should have been included in the OOPSLA paper;
there was no room...) Even if you get us to agree that the two semantics
are consistent, you will have difficulty convincing your readers without
a proof, and such a proof would be much easier (possibly even obvious)
if your presentation started with the OOPSLA semantics as a starting
point. This does not necessarily mean forcing your reader to read the
OOPSLA paper: you can repeat the necessary parts of the OOPSLA
semantics. However, a reader who has read the OOPSLA paper won't be
starting from scratch, and wondering whether the two are consistent or
not.

On Fri, Oct 06, 2006 at 10:21:56AM -0400, Eric Bodden wrote:
> 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:42:01 2006