The paper is available here: https://groups.csail.mit.edu/tds/papers/Lynch/jacm85.pdf

The 1st paragraph of lemma 3's proof says

enter image description here

In other words,if event e is applicable to config C,and E is any config reachable from C without applying e,then e is applicable to E.

I can follow the whole proof except the above claim. In real,practical systems, the claim isn't necessarily true. Here is an example:

suppose process p has a code fragment like this:

open 2 udp sockets,f1 and f2,respectively,in nonblocking mode

s1: read a message m from f1,depending on m,do some local processing,then send a finite set of messages to other processes //m could be null

s2: read a message m' from f2,depending on m',do some local processing,then send a finite set of messages to other processes //m' could be null

The label s1 and s2 in the code are steps("In one atomic step, a process can attempt to receive a message, perform local computation on the basis of whether or not a messagewas delivered to it (and if so, which one), and send an arbitrary but finite set of messagesto other processe",quoted from the final paragraph of page 2 of the paper).

Use C and E to denote the system config when process p's program counter was pointing to s1 and s2,respectively. Obviously,E is reachable from C. Suppose another process q sent udp datagrams m1 and m2 to sockets f1 and f2,respectively,right before the system reached config C. Therefore,in config C,events (p,m1),(p,null) are both applicable.Suppose (p,null) was applied in config C,making the system reach config E.Obviously,event (p,m1) is not applicable in config E,because process p was unable to read socket f1 in config E.

Now we've seen (p,m1) was applicable in config C, config E was reachable from C, and along the path from C to E,(p,m1) was never applied, but (p,m1) was not applicable to E,violating the claim in lemma 3's 1st paragraph.


Your Answer

By clicking "Post Your Answer", you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.