[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Mixing TLA+ and SOS

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.