4
$\begingroup$

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.

$\endgroup$
0
$\begingroup$

The crucial understanding here is the notion applicability of an event in some configuration versus the effect of applying the event to that configuration.

If an event e applies to configuration C, it follows that e applies to all C, where C is the set of all configurations reachable from C (all admissible extensions of C). This is a simple consequence of the model assumptions. If I can theoretically receive e now, and e can be delayed indefinitely, then I can apply e at any point in the future, perhaps applied e', e'', and so on.

There is a myriad of conceivable scenarios where, in practice, either e will not be applied by the program (because the program counter has advanced beyond the point where this is possible, as per your example) or where the message in e will be rejected by the program because of some other condition (i.e. internal state that forbids the processing of e). An example of the latter is the receipt of phase 1a and 2a messages in Paxos: they may be silently discarded by an acceptor that has already promised a higher ballot number.

Now we come to the notion of effect, which was omitted from FLP. (One of the reasons that FLP is obscure.) Applying e in some configuration does not imply a measurable transition. A process p could conceivably pop a message from its receive queue and discard it immediately. FLP does not forbid this, provided p behaves deterministically at all times and does not rely on the notion of time. Perhaps, p has received some other message m', which has 'locked out' m, so to speak; ergo, the late delivery of m has no measurable effect on p. This is entirely possible.

The reasoning behind FLP is to only induce a contradiction. If applying e to any configuration in C results in a configuration in D, and if we can prove that D does not solely comprise univalent configurations, then we have shown that there is an ever-admissible schedule that spans bivalent states. Lemma 3 does not state that C and D are disjoint: some configurations in C may conceivably be in D. In the case where applying e to some state C' in C has no effect, then C' is in D by the assumption of the lemma.

In summary, applies simply means that an event may be delivered. It does not mean that it is acted upon in a transition-inducing way.

$\endgroup$

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.