Re: Proposal to restore synchronous abort semantics

all,

>In any case there seems to be something fishy about the informal
>semantics of abort that is somewhat orthogonal to what we are
>discussing.
>...
>I think
>this is an issue for the extension/lrm committees to reformulate that.

in order to address johan's concern above as well as the one raised by
erich regarding asynchronicity, i propose adding the two phrases "with
respect to the base clock" and "before that " as positioned below to the
informal semantics of abort:

# An abort property holds in the current cycle of a given path iff:
#
# -- the FL Property that is the left operand holds, or
# -- the series of cycles, with respect to the base clock, starting from
the current cycle and ending
# with the cycle before that in which the Boolean condition that is the
right
# operand holds does not contradict the FL Property that is the left
# operand.

cindy.

--------------------------------------------------------------------
Cindy Eisner
Formal Methods Group
IBM Haifa Research Laboratory
Haifa 31905, Israel
Tel: +972-4-8296-266
Fax: +972-4-8296-114
e-mail: eisner@il.ibm.com

Johan Mårtensson <johan.martensson@safelogic.se>@eda.org on 11/01/2005
10:13:34

Sent by: owner-ieee-1850-extensions@eda.org

To: ieee-1850-extensions@eda.org
cc:
Subject: Re: Proposal to restore synchronous abort semantics

Erich

On Mon, Jan 10, 2005 at 09:23:43AM -0800, Erich Marschner wrote:

 [snip]
>
> All of the PSL properties written prior to release of the PSL v1.1 LRM
> (and probably many that were written afterward) were most likely
> written with the abort semantics of PSL v1.01 in mind, in which the
> abort condition was sensitive to the clock. It would be nice if we
> could maintain backward compatibility with the original version of
> PSL, but I guess that's not an issue for anyone else.

It is an issue for me at least. The problem from a backwards
compatibility point of view is that there are two conflicting historic
semantics for abort to conform to, the immediate one for PSL1.1 and the
more distant one for PSL1.01. Shouldn't we publicly acknowledge this in
some way and then provide two operators one with the synchronous and one
with the asynchronous semantics? This would result in minimal damage.
Old problems would have to be rewritten, but it would be a a simple
search and replace.

[snip]

>
> If we are going to keep the PSL v1.1 fixed-asynchronous semantics for
> abort, then I would at least recommend that someone (other than me)
> propose some changes to the informal semantics of abort, and perhaps
> also to the examples in the LRM that use abort, to make it clear to
> readers that the abort condition is asynchronous. There is no
> indication of this in the current LRM.

[snip]

Admittedly the text in section 6.2.1.5.1 of the LRM is rather vague but
at least it talks about asynchronicity. The explanatory text in the
example at the very end of the section says this:

# Using abort to model an asychronous interrupt: "A request is always
# followed by an acknowledge, unless an cancellation occurs."

Interestingly this text is already present in the PSL1.0 LRM (Section
6.2.1.4.1). This indicates to me that the intention was for abort to be
asynchronous already at that point although for some reason the formal
definition in that LRM defines a synchronous abort.

In any case there seems to be something fishy about the informal
semantics of abort that is somewhat orthogonal to what we are
discussing.

The informal semantics says this:

# An abort property holds in the current cycle of a given path iff:
#
# -- the FL Property that is the left operand holds, or
# -- the series of cycles starting from the current cycle and ending
# with the cycle in which the Boolean condition that is the right
# operand holds does not contradict the FL Property that is the left
# operand

What does "ending with" a cycle mean? Is inclusive or exclusive.

'(always a) abort not a' is true on all traces but it is not true on
some traces if "ending with" is taken in an inclusive sense. I think
this is an issue for the extension/lrm committees to reformulate that.

Best Regards, Johan M.

>
> Regards,
>
> Erich
>

--
------------------------------------------------------------
Johan Martensson, PhD            Office: +46 31 7451913
R&D                              Mobile: +46 703749681
Safelogic AB                     Fax: +46 31 7451939
Arvid Hedvalls Backe 4           johan.martensson@safelogic.se
SE-411 33 Gothenburg, SWEDEN
PGP key ID A8857A60
www.safelogic.se
------------------------------------------------------------