Re: [tlaplus] Re: Mixing TLA+ and SOS

Thanks for the explanation and hints to start.

The work that I am following to start is actually about a modeling language that is designed for

concurrent objects/systems. In this language, there's a principle of Run-To-Completion which I

think will prevent the example in Java. But, more interestingly, there's great interest in translating

the models into equivalent Java which brings back the question.

The language is ABS, http://link.springer.com/10.1007%2F978-3-642-25271-6_8

On Fri, Jul 15, 2016 at 7:36 PM, Leslie Lamport <tlapl...@xxxxxxxxx> wrote:

FL is correct that it's easy to encode an SOS semantics in TLA+. But
if you're talking about a real language with concurrency, I'd be
surprised if it has an SOS semantics. For example, in Java, if b is a
boolean variable that can be accessed by multiple threads, I have no
idea what the meaning is of the statement

b = ! b ;

If the people who designed the semantics of Java did anything like the
designers of two memory systems I've looked at--Alpha and Itanium--the
semantics is quite complicated, almost impossible to understand,
and unlikely to be describable with SOS.

Leslie

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

-- Behrooz Nobakht