Proving invalid case using promising semantic

[mekty2012]

This question is about http://www.cs.umd.edu/~pugh/java/memoryModel/CausalityTestCases.html/
By promising semantics, problems in above link is quite easy to solve when behavior is allowed. However, I found that it is quite hard to prove in cases that behavior is disallowed. Do we need to check every ordering of execution in threads to show that the behavior is disallowed? Or is there any better way of showing that behavior is disallowed?

Also, one of term that was mentioned in previous lecture was interleaving semantic. Will it be covered in later lectures? If not, is there some sources to learn about interleaving semantic?

[jeehoonkang]

• Yes, you need to check every ordering of executions for our purposes. Usually, it's more difficult to prove the absence of something than to prove the existence of something...

• "Interleaving semantics" is a semantics in which threads take turns and only one thread is executed at any given moment. In this semantics, the executed instructions are totally ordered and executed one-by-one. The reason it's "interleaving" is the threads of execution are interleaved into one.

[jeehoonkang]

@mekty2012 closing this as you've read the comments. Feel free to reopen it if you have further questions or comments!