Re: [abc] Concrete operational semantics

Hi All,

Eric will work on answering Julian's query right after he finishes
a course assignment today. Let's sort that out first.

As for making the correspondance between the OOPSLA semantics and the
one that Eric has given, I am not sure that we have room for
this in our 10 page limit. I believe that Eric worked out the
semantics as he describes from the implementation and has set it up
so that at key places he can talk about what is abstracted in the
static analysis. I think that if we agree that Eric's operational
semantics does correspond to the implementation, then we are
fairly firm ground.

Thus, I propose that we first establish if his semantics does
correctly represent the implementation. Is that ok?

CHeers, Laurie

+-----------------------------------------------------------------
| Laurie Hendren --- laurie.hendren@mcgill.ca
| Associate Dean (Academic), Faculty of Science,
| Dawson Hall, McGill University, 853 Sherbrooke St W,
| Montreal QC H3A 2T6 Canada, 514-398-7179, fax 514-398-1774
+----------------------------------------------------------------
| For contact and home page info as Professor, Computer Science:
| http://www.sable.mcgill.ca/~hendren --- hendren@cs.mcgill.ca
| Research: http://www.sable.mcgill.ca http://aspectbench.org
+----------------------------------------------------------------

Ondrej Lhotak wrote:
> 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 19:00:24 2006