Closed castlecowrice closed 4 years ago
Yes, you need to think of every possible interleaving. It's fundamentally necessary due to the inherent nondeterminism of concurrency.
Yes, in order to promise to write X=1, you need to consider all possible memories that's filled with arbitrary interfering additional messages. In some memories, there'll be a Y=1 message, and with the memory, you should be able to fulfill the promise. But in any case, you don't need to read the new Y=1 message because you can always read the initial Y=0 message and still fulfill the promise.
Regarding the faithfulness of the promising semantics for complex programs: yes, it's known to be faithful also to complex programs. As explained in the slides, promise adequately models speculative writes and their semantics dependencies. As such, the promising semantics is compatible with compiler optimizations and observable behaviors in hardware.
So in this case, the condition for the thread to promise X = 1 is that under any circumstances, there exists a message which would make that thread able to write X = 1 in the future, right? Also the reason is because we only have to know whether it is always possible to write X = 1 in the future. Did I understand correctly?
Yes, possible is the key here.
Thank you professor, I appreciate your help.
It seems like depending on how threads are interleaved, final results can be changed with promising semantics. Therefore, should I have to manually think about every possible interleaving to get the behavior that I want to observe? Also, when should a thread promise a value? I'm not sure whether promising a value must precede any instruction execution.
In the slides pp.58~60, according to the lecture, before the first instruction of the second thread, the second thread can promise X=1 because it will take the else branch and execute X=1. However, in some circumstances, there may be Y=1 in the memory and the second thread may read Y=1 and take the if-then branch. Although it does not invalidate the promise, I think that case should also be included when promising X=1. Am I correct? Also, I think that promising a value can be difficult if the program gets more complex. Does promising semantics works well in this case?