Question about the proof of Theorem 2.8.1

106 views
Skip to first unread message

Andrew Nguyen

unread,
Apr 25, 2015, 8:39:59 PM4/25/15
to art-of-multiproc...@googlegroups.com
I am stuck on understanding the proof of Theorem 2.8.1. Midway down page 38 in the proof, the text states that "the state s' is inconsistent because no thread can tell whether C is in the critical section...". I'm not sure how this follows by itself- although C is in the critical section, the state of the locations written to by A and B aren't necessarily "compatible with a global state in which no thread is in the critical section or is trying to enter the critical section." (definition 2.8.1) I gather that there's something about the fact that the lock object was previously in a covering state that makes the previous statement true for the current state (otherwise why even bother to require a covering state) but I can't figure out why. As far as I can tell the fact that the lock object's "locations 'look' like the critical section is empty'" is now irrelevant in state s'. Any hints here? 

I also find it strange that Figure 2.13 offers a way to conclude the (subsection of the) proof that doesn't appeal to the inconsistency of the resulting state but to the violation of mutual exclusion (and here also I'm not sure why a covering state is required). Am I mistaken and the figure and the text are essentially saying the same thing?

Hopefully the question(s) makes sense and thanks for any help.

Jingguo Yao

unread,
May 18, 2015, 10:47:12 AM5/18/15
to art-of-multiproc...@googlegroups.com
To answer your first question. Whether C is in CS, the state of location A and location B is the same
after A's write to location A and B's write to location B.
Reply all
Reply to author
Forward
0 new messages